From 31930ae958105d059d66be7f0f62c16e16b5c2c8 Mon Sep 17 00:00:00 2001 From: David Binder Date: Thu, 18 Dec 2025 18:10:51 +0000 Subject: [PATCH] Fix all hlint warnings in interpreter/ --- .hlint.yaml | 3 + interpreter/src/Language/Granule/Doc.hs | 40 +++++---- .../src/Language/Granule/Interpreter.hs | 34 ++++---- .../src/Language/Granule/Interpreter/Eval.hs | 82 +++++++++---------- interpreter/tests/Golden.hs | 7 +- 5 files changed, 79 insertions(+), 87 deletions(-) diff --git a/.hlint.yaml b/.hlint.yaml index a928151ab..07a23695f 100644 --- a/.hlint.yaml +++ b/.hlint.yaml @@ -51,6 +51,9 @@ # - ignore: {name: Use let} # - ignore: {name: Use const, within: SpecialModule} # Only within certain modules - ignore: {name: Redundant do} +- ignore: {name: Avoid lambda} +- ignore: {name: Use tuple-section} +- ignore: {name: Redundant lambda} # Define some custom infix operators # - fixity: infixr 3 ~^#^~ diff --git a/interpreter/src/Language/Granule/Doc.hs b/interpreter/src/Language/Granule/Doc.hs index faee2a8e7..f33f7461e 100644 --- a/interpreter/src/Language/Granule/Doc.hs +++ b/interpreter/src/Language/Granule/Doc.hs @@ -28,8 +28,6 @@ import qualified Data.Map as M import Control.Monad (when) --- import Debug.Trace - -- Doc top-level grDoc :: (?globals::Globals) => String -> AST () () -> IO () @@ -52,7 +50,7 @@ grDoc input ast = do writeFile ("docs/modules/" <> modName <> ".html") (unpack moduleFile) -- Generate the Primitives file - when info $ putStrLn $ "Generating docs index file." + when info $ putStrLn "Generating docs index file." primFile <- generatePrimitivesPage writeFile "docs/modules/Primitives.html" (unpack primFile) -- Generate the index file @@ -78,12 +76,12 @@ generateModulePage' modName title input ast = where inputLines = lines input content = (if Text.strip preamble == "" then "" else section "Meta-data" preamble) - <> (section "Contents" ((internalNav headings') + <> section "Contents" (internalNav headings' <> (if modName == "Primitives" then anchor "Built-in Types" else "") - <> Text.concat contentDefs)) + <> Text.concat contentDefs) preamble = parsePreamble inputLines - <> if M.keys (hiddenNames ast) == [] then "" - else (tag "strong" "Module does not export: ") <> Text.intercalate ", " (map (pack . prettyDoc) $ M.keys (hiddenNames ast)) + <> if Prelude.null (M.keys (hiddenNames ast)) then "" + else tag "strong" "Module does not export: " <> Text.intercalate ", " (map (pack . prettyDoc) $ M.keys (hiddenNames ast)) (headings, contentDefs) = unzip (map prettyDef topLevelDefs) headings' = if modName == "Primitives" @@ -92,7 +90,7 @@ generateModulePage' modName title input ast = -- Combine the data type and function definitions together - topLevelDefs = sortOn startLine $ (map Left (dataTypes ast)) <> (map Right (definitions ast)) + topLevelDefs = sortOn startLine $ map Left (dataTypes ast) <> map Right (definitions ast) startLine = fst . startPos . defSpan' defSpan' (Left dataDecl) = dataDeclSpan dataDecl defSpan' (Right def) = defSpan def @@ -100,27 +98,27 @@ generateModulePage' modName title input ast = prettyDef (Left d) = let (docs, heading) = scrapeDoc inputLines (dataDeclSpan d) in (heading, - (maybe "" anchor heading) + maybe "" anchor heading <> (codeDiv . pack . prettyDoc $ d) <> (if strip docs == "" then miniBreak else descDiv docs)) prettyDef (Right d) = let (docs, heading) = scrapeDoc inputLines (defSpan d) in (heading - , (maybe "" anchor heading) - <> (codeDiv $ breakLine (internalName (defId d)) $ pack $ prettyDoc (defId d) <> " : " <> prettyDoc (defTypeScheme d)) + , maybe "" anchor heading + <> codeDiv (breakLine (internalName (defId d)) $ pack $ prettyDoc (defId d) <> " : " <> prettyDoc (defTypeScheme d)) <> (if strip docs == "" then miniBreak else descDiv docs)) breakLine id xs = if Text.length xs >= 65 && (Text.isInfixOf "forall" xs || Text.isInfixOf "exists" xs) then case Text.break (== '.') xs of (before, after) -> - before <> "\n" <> (Data.Text.replicate (length id + 1) " ") <> after + before <> "\n" <> Data.Text.replicate (length id + 1) " " <> after else xs anchor :: Text -> Text anchor x = tagWithAttributes "a" ("name = " <> toUrlName x) - (tag "h3" ((tagWithAttributes "a" ("href='#' class='toplink'") "[top]") <> x)) + (tag "h3" (tagWithAttributes "a" "href='#' class='toplink'" "[top]" <> x)) internalNav [] = "" @@ -142,7 +140,7 @@ generateIndexPage = do -- Generates the text of the primitives module generatePrimitivesPage :: (?globals::Globals) => IO Text generatePrimitivesPage = do - generateModulePage' "Primitives" "Built-in primitives" (Primitives.builtinSrc) (appendPrimitiveTys $ fst . fromRight $ parseDefs "Primitives" Primitives.builtinSrc) + generateModulePage' "Primitives" "Built-in primitives" Primitives.builtinSrc (appendPrimitiveTys $ fst . fromRight $ parseDefs "Primitives" Primitives.builtinSrc) where fromRight (Right x) = x fromRight (Left x) = error x @@ -174,7 +172,7 @@ generatePrimitivesPage = do matches tyConName (id', (ty, _, _)) = case (tyConName, resultType ty) of (internalName -> "Type", Type 0) -> True - (a, b) -> (TyCon a) == b + (a, b) -> TyCon a == b generateFromTemplate :: PageContext -> Text -> Text -> Text -> IO Text generateFromTemplate ctxt modName title content = do @@ -197,7 +195,7 @@ generateNavigatorText ctxt = do files <- return $ sort (filter (\file -> takeExtension file == ".html" && takeBaseName file /= "Primitives") files) -- Build a list of these links let prefix = if ctxt == ModulePage then "" else "modules/" - let toLi file = li $ link (pack $ takeBaseName file) (prefix <> (pack $ takeBaseName file) <> ".html") + let toLi file = li $ link (pack $ takeBaseName file) (prefix <> pack (takeBaseName file) <> ".html") -- Link to index page let indexPrefix = if ctxt == ModulePage then "../" else "" let topLevelLink = link "Top-level
" (indexPrefix <> "index.html") @@ -251,7 +249,7 @@ parsePreamble inputLines = presentPrequelLine line = if name == "Module" -- drop duplicate module info then "" - else li $ (tag "b" (pack name)) <> pack info + else li $ tag "b" (pack name) <> pack info where (name, info) = break (== ':') (drop 4 line) prequelLines = @@ -265,20 +263,20 @@ parsePreamble inputLines = -- HTML generation helpers toUrlName :: Text -> Text -toUrlName = (replace " " "-") . (Text.filter isAlpha) . Text.toLower +toUrlName = replace " " "-" . Text.filter isAlpha . Text.toLower section :: Text -> Text -> Text section "" contents = tag "section" contents section name contents = tag "section" (tag "h2" name <> contents) codeDiv :: Text -> Text -codeDiv = tagWithAttributes "div" ("class='code'") . tag "pre" +codeDiv = tagWithAttributes "div" "class='code'" . tag "pre" descDiv :: Text -> Text -descDiv = tagWithAttributes "div" ("class='desc'") +descDiv = tagWithAttributes "div" "class='desc'" navDiv :: Text -> Text -navDiv = tagWithAttributes "div" ("class='mininav'") +navDiv = tagWithAttributes "div" "class='mininav'" span :: Text -> Text -> Text span name = tagWithAttributes "span" ("class='" <> name <> "'") diff --git a/interpreter/src/Language/Granule/Interpreter.hs b/interpreter/src/Language/Granule/Interpreter.hs index 7b774611d..0fedb0c77 100755 --- a/interpreter/src/Language/Granule/Interpreter.hs +++ b/interpreter/src/Language/Granule/Interpreter.hs @@ -85,11 +85,11 @@ main = do runGrOnFiles :: [FilePath] -> GrConfig -> IO () runGrOnFiles globPatterns config = let ?globals = grGlobals config in do pwd <- getCurrentDirectory - results <- forM globPatterns $ \pattern -> do - paths <- glob pattern + results <- forM globPatterns $ \pat -> do + paths <- glob pat case paths of [] -> do - let result = Left $ NoMatchingFiles pattern + let result = Left $ NoMatchingFiles pat printResult result return [result] _ -> forM paths $ \path -> do @@ -114,7 +114,7 @@ runGrOnFiles globPatterns config = let ?globals = grGlobals config in do result <- run config src printResult result return result - if all isRight (concat results) then exitSuccess else exitFailure + if all (all isRight) results then exitSuccess else exitFailure runGrOnStdIn :: GrConfig -> IO () runGrOnStdIn config@GrConfig{..} @@ -142,7 +142,7 @@ run => GrConfig -> String -> IO (Either InterpreterError InterpreterResult) -run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrFlags input) <> ?globals in do +run config input = let ?globals = maybe mempty grGlobals (getEmbeddedGrFlags input) <> ?globals in do if grDocMode config -- Generate docs mode then do @@ -175,7 +175,7 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF let holeErrors = getHoleMessages errs if ignoreHoles && length holeErrors == length errs && not (fromMaybe False $ globalsSynthesise ?globals) then do - printSuccess $ "OK " ++ (blue $ "(but with " ++ show (length holeErrors) ++ " holes)") + printSuccess $ "OK " ++ blue ("(but with " ++ show (length holeErrors) ++ " holes)") return $ Right NoEval else case (globalsRewriteHoles ?globals, holeErrors) of @@ -209,8 +209,8 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF where getHoleMessages :: NonEmpty CheckerError -> [CheckerError] - getHoleMessages es = - NonEmpty.filter (\ e -> case e of HoleMessage{} -> True; _ -> False) es + getHoleMessages = + NonEmpty.filter (\case HoleMessage{} -> True; _ -> False) runHoleSplitter :: (?globals :: Globals) => String @@ -245,7 +245,7 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF res <- synthesiseHoles config ast holesWithEmptyMeasurements isGradedBase let (holes', measurements, _) = unzip3 res when benchmarkingRawData $ do - forM_ measurements (\m -> case m of (Just m') -> putStrLn $ show m' ; _ -> return ()) + forM_ measurements (\case (Just m') -> print m' ; _ -> return ()) return holes' @@ -257,10 +257,10 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF rest <- synthesiseHoles config astSrc holes isGradedBase gradedExpr <- if cartSynth > 0 then getGradedExpr config defId else return Nothing - let defs' = map (\(x, (Forall tSp con bind ty)) -> + let defs' = map (\(x, Forall tSp con bind ty) -> if cartSynth > 0 - then (x, (Forall tSp con bind (toCart ty))) - else (x, (Forall tSp con bind ty)) + then (x, Forall tSp con bind (toCart ty)) + else (x, Forall tSp con bind ty) ) defs let (unrestricted, restricted) = case spec of Just (Spec _ _ _ comps) -> @@ -290,7 +290,7 @@ run config input = let ?globals = fromMaybe mempty (grGlobals <$> getEmbeddedGrF Just (programs@(_:_), measurement) -> do when synthHtml $ do printSynthOutput $ uncurry synthTreeToHtml (last programs) - return $ (HoleMessage sp goal ctxt tyVars hVars synthCtxt [([], fst $ last $ programs)], measurement, attemptNo) : rest + return $ (HoleMessage sp goal ctxt tyVars hVars synthCtxt [([], fst $ last programs)], measurement, attemptNo) : rest synthesiseHoles config ast (hole:holes) isGradedBase = do @@ -309,13 +309,13 @@ synEval ast = do getGradedExpr :: (?globals :: Globals) => GrConfig -> Id -> IO (Maybe (Def () ())) getGradedExpr config def = do - let file = (fromJust $ globalsSourceFilePath ?globals) <> ".output" + let file = fromJust (globalsSourceFilePath ?globals) <> ".output" src <- preprocess (rewriter config) (keepBackup config) file (literateEnvName config) - ((AST _ defs _ _ _), _) <- parseDefsAndDoImports src + (AST _ defs _ _ _, _) <- parseDefsAndDoImports src return $ find (\(Def _ id _ _ _ _) -> id == def) defs @@ -323,9 +323,7 @@ getGradedExpr config def = do -- "-- gr --no-eval" getEmbeddedGrFlags :: String -> Maybe GrConfig getEmbeddedGrFlags - = foldr (<|>) Nothing - . map getEmbeddedGrFlagsLine - . take 3 -- only check for flags within the top 3 lines + = foldr ((<|>) . getEmbeddedGrFlagsLine) Nothing . take 3 -- only check for flags within the top 3 lines . filter (not . all isSpace) . lines where diff --git a/interpreter/src/Language/Granule/Interpreter/Eval.hs b/interpreter/src/Language/Granule/Interpreter/Eval.hs index eb3521a7a..4e76f9693 100755 --- a/interpreter/src/Language/Granule/Interpreter/Eval.hs +++ b/interpreter/src/Language/Granule/Interpreter/Eval.hs @@ -22,23 +22,21 @@ import Language.Granule.Syntax.Type import Language.Granule.Context import Language.Granule.Utils (nullSpan, Globals, globalsExtensions, entryPoint, Extension(..)) import Language.Granule.Runtime as RT - import Language.Granule.Synthesis.Deriving (makeDerivedName) import Data.Text (cons, uncons, unpack, snoc, unsnoc) -import Control.Monad (foldM) import qualified Prettyprinter as P +import Data.Functor((<&>)) +import Control.Monad (foldM, forM_) + import System.IO.Unsafe (unsafePerformIO) ---import Control.Exception (catch, throwIO, IOException) import Control.Exception (catch, IOException) ---import GHC.IO.Exception (IOErrorType( OtherError )) import qualified Control.Concurrent as C (forkIO) import qualified Control.Concurrent.Chan as CC (newChan, writeChan, readChan, dupChan, Chan) import qualified Control.Concurrent.MVar as MV import qualified System.IO as SIO ---import System.IO.Error (mkIOError) import Data.Bifunctor import Control.Monad.Extra (void) import Data.Unique @@ -111,27 +109,27 @@ readChan (BChan _ bwd _ bwdMV tag pol) = do flag <- MV.isEmptyMVar bwdMV if flag then do - debugComms tag pol $ "Read Normal" + debugComms tag pol "Read Normal" x <- CC.readChan bwd debugComms tag pol $ "READ " ++ show x return x -- short-circuit the channel because a value was read and has been memo else do - debugComms tag pol $ "Read Putback" + debugComms tag pol "Read Putback" x <- MV.takeMVar bwdMV debugComms tag pol $ "READ from put back: " ++ show x return x -putbackChan :: BinaryChannel a -> (Value (Runtime a) a) -> IO () +putbackChan :: BinaryChannel a -> Value (Runtime a) a -> IO () putbackChan (BChan _ _ _ bwdMV tag pol) x = do debugComms tag pol "Putback" MV.putMVar bwdMV x -writeChan :: Show a => BinaryChannel a -> (Value (Runtime a) a) -> IO () +writeChan :: Show a => BinaryChannel a -> Value (Runtime a) a -> IO () writeChan (BChan fwd _ _ _ tag pol) v = do debugComms tag pol $ "Try to write " ++ show v CC.writeChan fwd v - debugComms tag pol $ "written" + debugComms tag pol "written" dupChan :: BinaryChannel a -> IO (BinaryChannel a) dupChan (BChan fwd bwd m n t p) = do @@ -221,8 +219,8 @@ evalInCBNdeep ctxt (App s a b e1 e2) = do -- (cf. APP_R) -- Force eval of the parameter for primitives v2 <- evalInCBNdeep ctxt e2 - vRes <- k v2 - return vRes + k v2 + (Abs _ p _ e3) -> do -- (cf. P_BETA CBN) @@ -316,7 +314,7 @@ evalInWHNF ctxt (LetDiamond s _ _ p _ e1 e2) = do evalInWHNF ctxt (Val s a b (Var _ x)) = case lookup x ctxt of Just val@(Ext _ (PrimitiveClosure f)) -> return $ Val s a b $ Ext () $ Primitive (f ctxt) - Just val -> return $ Val s a b $ val + Just val -> return $ Val s a b val Nothing -> fail $ "Variable '" <> sourceName x <> "' is undefined in context." evalInWHNF _ e@(Val _ _ _ v) = return e @@ -355,8 +353,8 @@ evalIn ctxt e = then do e' <- evalInCBNdeep ctxt e -- finally eagerly evaluate - e'' <- evalInCBV ctxt (valExpr e') - return e'' + evalInCBV ctxt (valExpr e') + else evalInCBV ctxt e @@ -679,11 +677,10 @@ valExpr :: ExprFix2 g ExprF ev () -> ExprFix2 ExprF g ev () valExpr = Val nullSpanNoFile () False appExpr :: ExprFix2 ExprF g ev () -> ExprFix2 ExprF g ev () -> ExprFix2 ExprF g ev () -appExpr e1 e2 = App nullSpanNoFile () False e1 e2 +appExpr = App nullSpanNoFile () False multiAppExpr :: ExprFix2 ExprF g ev () -> [ExprFix2 ExprF g ev ()] -> ExprFix2 ExprF g ev () -multiAppExpr fun args = - foldl (\arg rest -> appExpr arg rest) fun args +multiAppExpr = foldl appExpr promoteExpr :: ExprFix2 ExprF ValueF ev () -> ExprFix2 ExprF ValueF ev () promoteExpr e = valExpr $ Promote () e @@ -712,16 +709,15 @@ builtIns = , (mkId "cap", Ext () $ Primitive $ \(Constr () name _) -> return $ Ext () $ Primitive $ \_ -> case internalName name of "Console" -> return $ Ext () $ Primitive $ \(StringLiteral s) -> toStdout s >> - (return $ (Constr () (mkId "()") [])) - "TimeDate" -> return $ Ext () $ Primitive $ \(Constr () (internalName -> "()") []) -> RT.timeDate () >>= - (\s -> return $ (StringLiteral s)) + return (Constr () (mkId "()") []) + "TimeDate" -> return $ Ext () $ Primitive $ \(Constr () (internalName -> "()") []) -> RT.timeDate () <&> StringLiteral _ -> error "Unknown capability") -- substrctural combinators , (mkId "moveChar", Ext () $ Primitive $ \(CharLiteral c) -> return $ Promote () (Val nullSpan () False (CharLiteral c))) , (mkId "moveInt", Ext () $ Primitive $ \(NumInt c) -> return $ Promote () (Val nullSpan () False (NumInt c))) , ( mkId "moveString" , Ext () $ Primitive $ \(StringLiteral s) -> return $ - Promote () $ valExpr $ (StringLiteral s)) + Promote () $ valExpr $ StringLiteral s) , (mkId "drop@Int", Ext () $ Primitive $ const $ return $ Constr () (mkId "()") []) , (mkId "drop@Char", Ext () $ Primitive $ const $ return $ Constr () (mkId "()") []) , (mkId "drop@Float", Ext () $ Primitive $ const $ return $ Constr () (mkId "()") []) @@ -740,10 +736,10 @@ builtIns = n -> error $ show n) , (mkId "readInt", Ext () $ Primitive $ \(StringLiteral s) -> return $ NumInt $ RT.readInt s) , (mkId "fromStdin", diamondConstr $ RT.fromStdin >>= \val -> return $ Val nullSpan () False $ StringLiteral val) - , (mkId "toStdout", Ext () $ Primitive $ \(StringLiteral s) -> return $ diamondConstr $ (toStdout s) >> - (return $ Val nullSpan () False (Constr () (mkId "()") []))) - , (mkId "toStderr", Ext () $ Primitive $ \(StringLiteral s) -> return $ diamondConstr $ (toStderr s) >> - (return $ Val nullSpan () False (Constr () (mkId "()") []))) + , (mkId "toStdout", Ext () $ Primitive $ \(StringLiteral s) -> return $ diamondConstr $ toStdout s >> + return (Val nullSpan () False (Constr () (mkId "()") []))) + , (mkId "toStderr", Ext () $ Primitive $ \(StringLiteral s) -> return $ diamondConstr $ toStderr s >> + return (Val nullSpan () False (Constr () (mkId "()") []))) , (mkId "openHandle", Ext () $ Primitive openHandle) , (mkId "readChar", Ext () $ Primitive readChar) , (mkId "writeChar", Ext () $ Primitive writeChar) @@ -828,8 +824,8 @@ builtIns = , (mkId "readRef", Ext () $ Primitive readRef) -- Additive conjunction (linear logic) , (mkId "with", Ext () $ Primitive $ \v -> return $ Ext () $ Primitive $ \w -> return $ Constr () (mkId "&") [v, w]) - , (mkId "projL", Ext () $ Primitive $ \(Constr () (Id "&" "&") [v, w]) -> return $ v) - , (mkId "projR", Ext () $ Primitive $ \(Constr () (Id "&" "&") [v, w]) -> return $ w) + , (mkId "projL", Ext () $ Primitive $ \(Constr () (Id "&" "&") [v, w]) -> return v) + , (mkId "projR", Ext () $ Primitive $ \(Constr () (Id "&" "&") [v, w]) -> return w) -- free graded monad -- call op x = Impure (op x (\o -> Pure o)) , (mkId "call", Ext () $ Primitive $ \op -> @@ -839,7 +835,7 @@ builtIns = (App nullSpan () False (valExpr op) (valExpr inp)) (valExpr $ Promote () $ valExpr $ Ext () $ Primitive $ \o -> - return (Ext () $ PureWrapper $ return $ (valExpr o)))) + return (Ext () $ PureWrapper $ return $ valExpr o))) , (mkId "handle", Ext () $ PrimitiveClosure handlePrim) , (mkId "handleGr", Ext () $ PrimitiveClosure handlePrim) ] @@ -852,9 +848,7 @@ builtIns = fmap_fun <- evalIn ctxt fmap_inner return $ Ext () $ Primitive $ \alg -> return $ Ext () $ Primitive $ \ret_handler -> - return $ Ext () $ Primitive $ \computation -> - case computation of - + return $ Ext () $ Primitive $ \case -- handler alg f (Pure x) = f x Ext _ (PureWrapper comp) -> do -- run the IO in here (should be none) @@ -905,7 +899,7 @@ builtIns = (valExpr fmap_fun) [promoteExpr $ valExpr $ Ext () (Primitive (\freefa -> evalIn ctxt (LetDiamond nullSpanNoFile () False p Nothing (valExpr freefa) rest))) - , valExpr $ comp])] + , valExpr comp])] r -> error $ "Interal bug: handle expecting a free monad but got " <> pretty r @@ -964,7 +958,7 @@ builtIns = -- make the chans receiverChans <- mapM (const newChan) [1..(natToInt n)] -- fork the waiters which then fork the servers - _ <- flip mapM receiverChans + forM_ receiverChans (\receiverChan -> C.forkIO $ void $ do -- wait to receive on the main channel x <- readChan receiverChan @@ -1046,7 +1040,7 @@ builtIns = let (Ref () v') = unsafePerformIO $ evalIn ctxt (App nullSpan () False (Val nullSpan () False f) - (Val nullSpan () False (Ref () v))) in (Nec () v') + (Val nullSpan () False (Ref () v))) in Nec () v' split :: RValue -> IO RValue split v = return $ Constr () (mkId ",") [v, v] @@ -1154,8 +1148,8 @@ builtIns = (CharLiteral c) -> do SIO.hPutChar h c return $ valExpr $ Ext () $ Handle h - _ -> error $ "Runtime exception: trying to put a non character value")) - writeChar _ = error $ "Runtime exception: trying to put from a non handle value" + _ -> error "Runtime exception: trying to put a non character value")) + writeChar _ = error "Runtime exception: trying to put from a non handle value" readChar :: RValue -> IO RValue readChar (Ext _ (Handle h)) = return $ diamondConstr $ do @@ -1176,7 +1170,7 @@ builtIns = return $ Pack nullSpan () (TyName (hashUnique name)) (valExpr $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.FA arr)) (mkId ("id" ++ show (hashUnique name))) (TyCon (mkId "Name")) (Borrow (TyCon $ mkId "Star") (TyCon $ mkId "FloatArray")) newRef :: RValue -> IO RValue - newRef = \v -> do + newRef v = do ref <- RT.newRefSafe v name <- newUnique return $ Pack nullSpan () (TyName (hashUnique name)) (valExpr $ Nec () $ Val nullSpan () False $ Ext () $ Runtime (RT.PR ref)) (mkId ("id" ++ show (hashUnique name))) (TyCon (mkId "Name")) (Borrow (TyCon $ mkId "Star") (TyCon $ mkId "Ref")) @@ -1221,16 +1215,16 @@ builtIns = lengthFloatArray :: RValue -> IO RValue lengthFloatArray (Nec () (Val _ _ _ (Ext () (Runtime (RT.FA fa))))) = let (e,fa') = RT.lengthFloatArray fa - in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False $ (NumInt e)), Nec () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))] + in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False (NumInt e)), Nec () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))] lengthFloatArray (Ref () (Val _ _ _ (Ext () (Runtime (RT.FA fa))))) = let (e,fa') = RT.lengthFloatArray fa - in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False $ (NumInt e)), Ref () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))] + in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False (NumInt e)), Ref () (Val nullSpan () False $ Ext () $ Runtime (RT.FA fa'))] lengthFloatArray _ = error "Runtime exception: trying to take the length of a non-array value" lengthFloatArrayI :: RValue -> IO RValue lengthFloatArrayI = \(Ext () (Runtime (RT.FA fa))) -> let (e,fa') = RT.lengthFloatArray fa - in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False $ (NumInt e)), Ext () $ Runtime (RT.FA fa')] + in return $ Constr () (mkId ",") [Promote () (Val nullSpan () False (NumInt e)), Ext () $ Runtime (RT.FA fa')] writeFloatArray :: RValue -> IO RValue writeFloatArray (Nec _ (Val _ _ _ (Ext _ (Runtime (RT.FA fa))))) = return $ @@ -1278,7 +1272,7 @@ evalDefs ctxt (Def _ var _ _ (EquationList _ _ _ [Equation _ _ _ rf [] e]) _ : d case extend ctxt var val of Just ctxt -> evalDefs ctxt defs Nothing -> - if '@' `elem` (internalName var) + if '@' `elem` internalName var -- ignore name clashes for derived operations -- TODO: this is somewhat a hack- we should be able to make sure we don't -- regenerated derived operations, but at least they should all be equivalent... @@ -1350,6 +1344,6 @@ evalAtEntryPoint entryPoint (AST dataDecls defs _ _ _) = do -- step semantics (either reduction scheme) isReducible :: Expr ev a -> Bool isReducible (Val _ _ _ (Var _ _)) = True -isReducible (Val _ _ _ _) = False -isReducible (Hole _ _ _ _ _) = False +isReducible Val {} = False +isReducible Hole {} = False isReducible _ = True diff --git a/interpreter/tests/Golden.hs b/interpreter/tests/Golden.hs index ca88d59b9..fc8f7f8ab 100644 --- a/interpreter/tests/Golden.hs +++ b/interpreter/tests/Golden.hs @@ -3,16 +3,15 @@ import Control.Monad (unless) import Data.Algorithm.Diff (getGroupedDiff) import Data.Algorithm.DiffOutput (ppDiff) import Data.List (sort, isInfixOf) +import Data.Functor((<&>)) import Test.Tasty (defaultMain, TestTree, testGroup) import Test.Tasty.Golden (goldenVsFile) import qualified Test.Tasty.Golden as G import Test.Tasty.Golden.Advanced (goldenTest) -import System.Directory (renameFile) +import System.Directory (renameFile, doesFileExist) import System.Exit (ExitCode) import System.FilePath (dropExtension, pathSeparator) import qualified System.IO.Strict as Strict (readFile) ---import System.Environment -import System.Directory (doesFileExist) import Language.Granule.Interpreter (InterpreterResult(..), InterpreterError(..)) import qualified Language.Granule.Interpreter as Interpreter @@ -74,7 +73,7 @@ applyConfig cfgs files = aux cfgs [] findByExtension :: Config -> [FilePath] -> FilePath -> IO [FilePath] -findByExtension config exs path = G.findByExtension exs path >>= (return . sort . applyConfig config) +findByExtension config exs path = G.findByExtension exs path <&> (sort . applyConfig config) goldenTestsNegative :: Config -> IO TestTree goldenTestsNegative config = do