From 1afcda345a01d867179117c4e4e566ddd8d7c771 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 2 Dec 2024 16:25:28 +0300 Subject: [PATCH 01/16] [ base ] Replace `believe_me` with proof in `Cast Int ExitCode` --- libs/base/System.idr | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/libs/base/System.idr b/libs/base/System.idr index e44ee5f4c3..2315965f6b 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -292,12 +292,13 @@ data ExitCode : Type where ||| ||| @errNo A non-zero numerical value indicating failure. ||| @prf Proof that the int value is non-zero. - ExitFailure : (errNo : Int) -> (So (not $ errNo == 0)) => ExitCode + ExitFailure : (errNo : Int) -> (So $ errNo /= 0) => ExitCode export Cast Int ExitCode where - cast 0 = ExitSuccess - cast code = ExitFailure code @{believe_me Oh} + cast code with (code == 0) proof prf + _ | True = ExitSuccess + _ | False = ExitFailure code @{rewrite prf in Oh} export Cast ExitCode Int where From 39f155bb1e6c4cbd1782d04df8403d4d4c66b5b0 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 13:47:17 +0300 Subject: [PATCH 02/16] [ refactor ] Improve error handling in `Core` --- src/Compiler/Common.idr | 8 +-- src/Compiler/ES/Javascript.idr | 2 +- src/Compiler/ES/Node.idr | 12 ++--- src/Compiler/Interpreter/VMCode.idr | 4 +- src/Compiler/RefC/CC.idr | 17 +++---- src/Compiler/RefC/RefC.idr | 31 +++++------ src/Compiler/Scheme/Chez.idr | 61 ++++++++-------------- src/Compiler/Scheme/ChezSep.idr | 42 +++++++-------- src/Compiler/Scheme/Gambit.idr | 12 ++--- src/Compiler/Scheme/Racket.idr | 52 +++++++------------ src/Core/Binary.idr | 11 ++-- src/Core/Context.idr | 16 +++--- src/Core/Core.idr | 79 +++++++++++++++++++++++------ src/Core/Directory.idr | 19 ++----- src/Core/Metadata.idr | 10 ++-- src/Core/SchemeEval/Compile.idr | 3 +- src/Idris/Driver.idr | 3 +- src/Idris/Error.idr | 4 ++ src/Idris/IDEMode/CaseSplit.idr | 3 +- src/Idris/ModTree.idr | 3 +- src/Idris/Package.idr | 23 ++++----- src/Idris/ProcessIdr.idr | 3 +- src/Idris/REPL.idr | 39 +++++++------- src/Idris/SetOptions.idr | 6 +-- src/TTImp/ProcessDecls.idr | 3 +- src/Yaffle/Main.idr | 8 +-- src/Yaffle/REPL.idr | 47 +++++++++-------- tests/chez/chez037/expected | 2 +- 28 files changed, 245 insertions(+), 278 deletions(-) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index e113a34d0a..f1ba3539ba 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -221,9 +221,7 @@ natHackNames = dumpIR : Show def => String -> List (Name, def) -> Core () dumpIR fn lns = do let cstrs = map dumpDef lns - Right () <- coreLift $ writeFile fn (fastConcat cstrs) - | Left err => throw (FileErr fn err) - pure () + writeFile fn (fastConcat cstrs) where fullShow : Name -> String fullShow (DN _ n) = show n @@ -533,9 +531,7 @@ copyLib (lib, fullname) then pure () else do Right bin <- coreLift $ readFromFile fullname | Left err => pure () -- assume a system library installed globally - Right _ <- coreLift $ writeToFile lib bin - | Left err => throw (FileErr lib err) - pure () + handleFileError lib $ writeToFile lib bin -- parses `--directive extraRuntime=/path/to/defs.scm` options for textual inclusion in generated diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index edd564d8de..557a5d171a 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -61,7 +61,7 @@ compileExpr c s tmpDir outputDir tm outfile = do es <- compileToJS c s tm let res = addHeaderAndFooter outfile es let out = outputDir outfile - Core.writeFile out res + writeFile out res pure (Just out) ||| Node implementation of the `executeExpr` interface. diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index 3203856474..b5e337d582 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -54,8 +54,8 @@ compileExpr : compileExpr c s tmpDir outputDir tm outfile = do es <- compileToNode c s tm let out = outputDir outfile - Core.writeFile out es - coreLift_ $ chmodRaw out 0o755 + writeFile out es + handleFileError out $ chmodRaw out 0o755 pure (Just out) ||| Node implementation of the `executeExpr` interface. @@ -64,12 +64,10 @@ executeExpr : Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm = - do let outn = tmpDir "_tmp_node.js" - js <- compileToNode c s tm - Core.writeFile outn js + do Just out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js" + | Nothing => throw (InternalError "compileExpr returned Nothing") node <- coreLift findNode - quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path. - coreLift_ $ system (quoted_node ++ " " ++ outn) + ignore $ system [node, out] ||| Codegen wrapper for Node implementation. export diff --git a/src/Compiler/Interpreter/VMCode.idr b/src/Compiler/Interpreter/VMCode.idr index b5279d6176..1334504bfd 100644 --- a/src/Compiler/Interpreter/VMCode.idr +++ b/src/Compiler/Interpreter/VMCode.idr @@ -151,7 +151,7 @@ knownForeign = fromList world stk o = interpError stk $ "expected %MkWorld or Null, got \{show o}" prim_putChar : Ref State InterpState => Stack -> Vect 2 Object -> Core Object - prim_putChar stk [Const (Ch c), w] = world stk w *> (ioRes unit <$ coreLift_ (putChar c)) + prim_putChar stk [Const (Ch c), w] = world stk w *> (ioRes unit <$ coreLift (putChar c)) prim_putChar stk as = argError stk as prim_getChar : Ref State InterpState => Stack -> Vect 1 Object -> Core Object @@ -163,7 +163,7 @@ knownForeign = fromList prim_getStr stk as = argError stk as prim_putStr : Ref State InterpState => Stack -> Vect 2 Object -> Core Object - prim_putStr stk [Const (Str s), w] = world stk w *> (ioRes unit <$ coreLift_ (putStr s)) + prim_putStr stk [Const (Str s), w] = world stk w *> (ioRes unit <$ coreLift (putStr s)) prim_putStr stk as = argError stk as knownExtern : NameMap (ar ** (Ref State InterpState => Stack -> Vect ar Object -> Core Object)) diff --git a/src/Compiler/RefC/CC.idr b/src/Compiler/RefC/CC.idr index ec425e0eba..9b4ab92e6b 100644 --- a/src/Compiler/RefC/CC.idr +++ b/src/Compiler/RefC/CC.idr @@ -63,7 +63,7 @@ compileCObjectFile : {auto c : Ref Ctxt Defs} -> {default False asLibrary : Bool} -> (sourceFile : String) -> (objectFile : String) - -> Core (Maybe String) + -> Core String compileCObjectFile {asLibrary} sourceFile objectFile = do cc <- coreLift findCC cFlags <- coreLift findCFLAGS @@ -81,19 +81,16 @@ compileCObjectFile {asLibrary} sourceFile objectFile = "-I" ++ cDir]) ++ " " ++ cppFlags ++ " " ++ cFlags - log "compiler.refc.cc" 10 runccobj - 0 <- coreLift $ system runccobj - | _ => pure Nothing - - pure (Just objectFile) + safeSystem runccobj + pure objectFile export compileCFile : {auto c : Ref Ctxt Defs} -> {default False asShared : Bool} -> (objectFile : String) -> (outFile : String) - -> Core (Maybe String) + -> Core String compileCFile {asShared} objectFile outFile = do cc <- coreLift findCC cFlags <- coreLift findCFLAGS @@ -117,7 +114,5 @@ compileCFile {asShared} objectFile outFile = ++ " " ++ (unwords [cFlags, ldFlags, ldLibs]) log "compiler.refc.cc" 10 runcc - 0 <- coreLift $ system runcc - | _ => pure Nothing - - pure (Just outFile) + safeSystem runcc + pure outFile diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 5d32882111..fe38da8be1 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -979,45 +979,38 @@ generateCSourceFile defs outn = fileContent <- get OutfileText let code = fastConcat (map (++ "\n") (reify fileContent)) - coreLift_ $ writeFile outn code + writeFile outn code log "compiler.refc" 10 $ "Generated C file " ++ outn export -compileExpr : UsePhase - -> Ref Ctxt Defs +compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> ClosedTerm -> (outfile : String) -> Core (Maybe String) -compileExpr ANF c s _ outputDir tm outfile = - do let outn = outputDir outfile ++ ".c" - let outobj = outputDir outfile ++ ".o" +compileExpr c s _ outputDir tm outfile = + do let outn = outputDir outfile <.> "c" + let outobj = outputDir outfile <.> "o" let outexec = outputDir outfile - coreLift_ $ mkdirAll outputDir + handleFileError outputDir $ mkdirAll outputDir cdata <- getCompileData False ANF tm let defs = anf cdata generateCSourceFile defs outn - Just _ <- compileCObjectFile outn outobj - | Nothing => pure Nothing - compileCFile outobj outexec - -compileExpr _ _ _ _ _ _ _ = pure Nothing - - + obj <- compileCObjectFile outn outobj + Just <$> compileCFile obj outexec export executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (execDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm = do - do let outfile = "_tmp_refc" - Just _ <- compileExpr ANF c s tmpDir tmpDir tm outfile - | Nothing => do coreLift_ $ putStrLn "Error: failed to compile" - coreLift_ $ system (tmpDir outfile) + do Just sh <- compileExpr c s tmpDir tmpDir tm "_tmp_refc" + | Nothing => coreLift $ putStrLn "Error: failed to compile" + ignore $ system sh export codegenRefC : Codegen -codegenRefC = MkCG (compileExpr ANF) executeExpr Nothing Nothing +codegenRefC = MkCG compileExpr executeExpr Nothing Nothing diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index e90707568e..3b53d65543 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -518,9 +518,8 @@ compileToSS c prof appdir tm outfile , main , schFooter prof True ] - Right () <- coreLift $ writeFile outfile $ build scm - | Left err => throw (FileErr outfile err) - coreLift_ $ chmodRaw outfile 0o755 + writeFile outfile $ build scm + handleFileError outfile $ chmodRaw outfile 0o755 ||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off. compileToSO : {auto c : Ref Ctxt Defs} -> @@ -533,12 +532,9 @@ compileToSO prof chez appDirRel outSsAbs else "") ++ "[compile-file-message #f]) (compile-program " ++ show outSsAbs ++ "))" - Right () <- coreLift $ writeFile tmpFileAbs build - | Left err => throw (FileErr tmpFileAbs err) - coreLift_ $ chmodRaw tmpFileAbs 0o755 - 0 <- coreLift $ system [chez, "--script", tmpFileAbs] - | status => throw (InternalError "Chez exited with return code \{show status}") - pure () + writeFile tmpFileAbs build + handleFileError tmpFileAbs $ chmodRaw tmpFileAbs 0o755 + safeSystem [chez, "--script", tmpFileAbs] ||| Compile a TT expression to Chez Scheme using incremental module builds compileToSSInc : Ref Ctxt Defs -> @@ -563,27 +559,19 @@ compileToSSInc c mods libs appdir tm outfile collectRequestHandler ++ "\n" ++ main ++ schFooter False False - Right () <- coreLift $ writeFile outfile $ build scm - | Left err => throw (FileErr outfile err) - coreLift_ $ chmodRaw outfile 0o755 - pure () + writeFile outfile $ build scm + handleFileError outfile $ chmodRaw outfile 0o755 makeSh : String -> String -> String -> Core () -makeSh outShRel appdir outAbs - = do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs) - | Left err => throw (FileErr outShRel err) - pure () +makeSh outShRel appdir outAbs = writeFile outShRel (startChez appdir outAbs) ||| Make Windows start scripts, one for bash environments and one batch file makeShWindows : String -> String -> String -> String -> String -> Core () makeShWindows chez outShRel appdir outAbs progType = do let cmdFile = outShRel ++ ".cmd" - Right () <- coreLift $ writeFile cmdFile (startChezCmd chez appdir outAbs progType) - | Left err => throw (FileErr cmdFile err) - Right () <- coreLift $ writeFile outShRel (startChezWinSh chez appdir outAbs progType) - | Left err => throw (FileErr outShRel err) - pure () + writeFile cmdFile (startChezCmd chez appdir outAbs progType) + writeFile outShRel (startChezWinSh chez appdir outAbs progType) compileExprWhole : Bool -> @@ -594,9 +582,8 @@ compileExprWhole : compileExprWhole makeitso c s tmpDir outputDir tm outfile = do let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here - coreLift_ $ mkdirAll appDirGen - Just cwd <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") + handleFileError appDirGen $ mkdirAll appDirGen + cwd <- currentDir let outSsFile = appDirRel outfile <.> "ss" let outSoFile = appDirRel outfile <.> "so" let outSsAbs = cwd outputDir outSsFile @@ -604,13 +591,13 @@ compileExprWhole makeitso c s tmpDir outputDir tm outfile chez <- coreLift $ findChez let prof = profile !getSession logTime 2 "Compile to scheme" $ compileToSS c (makeitso && prof) appDirGen tm outSsAbs - logTime 2 "Make SO" $ when makeitso $ + when makeitso $ logTime 2 "Make SO" $ compileToSO prof chez appDirGen outSsAbs let outShRel = outputDir outfile if isWindows then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) "--program" else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile) - coreLift_ $ chmodRaw outShRel 0o755 + handleFileError outShRel $ chmodRaw outShRel 0o755 pure (Just outShRel) compileExprInc : @@ -627,20 +614,19 @@ compileExprInc makeitso c s tmpDir outputDir tm outfile compileExprWhole makeitso c s tmpDir outputDir tm outfile let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here - coreLift_ $ mkdirAll appDirGen - Just cwd <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") + handleFileError appDirGen $ mkdirAll appDirGen + cwd <- currentDir let outSsFile = appDirRel outfile <.> "ss" let outSoFile = appDirRel outfile <.> "so" let outSsAbs = cwd outputDir outSsFile let outSoAbs = cwd outputDir outSoFile - chez <- coreLift $ findChez + chez <- coreLift findChez compileToSSInc c mods libs appDirGen tm outSsAbs let outShRel = outputDir outfile if isWindows then makeShWindows chez outShRel appDirRel outSsFile "--script" else makeSh outShRel appDirRel outSsFile - coreLift_ $ chmodRaw outShRel 0o755 + handleFileError outShRel $ chmodRaw outShRel 0o755 pure (Just outShRel) ||| Chez Scheme implementation of the `compileExpr` interface. @@ -665,7 +651,7 @@ executeExpr : executeExpr c s tmpDir tm = do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpchez" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift_ $ system [sh] + ignore $ system sh incCompile : Ref Ctxt Defs -> @@ -695,18 +681,15 @@ incCompile c s sourceFile (sortedDefs, constants) <- sortDefs ndefs compdefs <- traverse (getScheme empty (chezExtPrim empty defaultLaziness) chezString defaultLaziness) sortedDefs let code = concat $ map snd fgndefs ++ compdefs - Right () <- coreLift $ writeFile ssFile $ build code - | Left err => throw (FileErr ssFile err) + writeFile ssFile $ build code -- Compile to .so let tmpFileAbs = outputDir "compileChez" let build = "(parameterize ([optimize-level 3] " ++ "[compile-file-message #f]) (compile-file " ++ show ssFile ++ "))" - Right () <- coreLift $ writeFile tmpFileAbs build - | Left err => throw (FileErr tmpFileAbs err) - 0 <- coreLift $ system [chez, "--script", tmpFileAbs] - | status => throw (InternalError "Chez exited with return code \{show status}") + writeFile tmpFileAbs build + safeSystem [chez, "--script", tmpFileAbs] pure (Just (soFilename, mapMaybe fst fgndefs)) ||| Codegen wrapper for Chez scheme implementation. diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index 4af002a03e..552afb0d4b 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -99,7 +99,7 @@ startChezWinSh chez appDirSh targetSh = """ -- TODO: parallelise this compileChezLibraries : (chez : String) -> (libDir : String) -> (ssFiles : List String) -> Core () -compileChezLibraries chez libDir ssFiles = coreLift_ $ system +compileChezLibraries chez libDir ssFiles = safeSystem [ "echo" , unwords [ "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-library " ++ build (chezString ssFile) ++ "))'" @@ -112,7 +112,7 @@ compileChezLibraries chez libDir ssFiles = coreLift_ $ system ] compileChezLibrary : (chez : String) -> (libDir : String) -> (ssFile : String) -> Core () -compileChezLibrary chez libDir ssFile = coreLift_ $ system +compileChezLibrary chez libDir ssFile = safeSystem [ "echo" , "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-library " ++ build (chezString ssFile) ++ "))'" , "'(delete-file " ++ build (chezString ssFile) ++ ")'" @@ -120,7 +120,7 @@ compileChezLibrary chez libDir ssFile = coreLift_ $ system ] compileChezProgram : (chez : String) -> (libDir : String) -> (ssFile : String) -> Core () -compileChezProgram chez libDir ssFile = coreLift_ $ system +compileChezProgram chez libDir ssFile = safeSystem [ "echo" , "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-program " ++ build (chezString ssFile) ++ "))'" , "'(delete-file " ++ build (chezString ssFile) ++ ")'" @@ -138,7 +138,7 @@ chezLibraryName : CompilationUnit def -> String chezLibraryName cu = chezNS (foldl1 min cu.namespaces) touch : String -> Core () -touch s = coreLift_ $ system ["touch", s] +touch s = safeSystem ["touch", s] record ChezLib where constructor MkChezLib @@ -168,8 +168,8 @@ compileToSS c chez appdir tm = do Left err => pure True Right fileHash => pure (fileHash /= supportHash) when supportChanged $ do - Core.writeFile (appdir "support.ss") support - Core.writeFile (appdir "support.hash") supportHash + writeFile (appdir "support.ss") support + writeFile (appdir "support.hash") supportHash -- TODO: add extraRuntime -- the problem with this is that it's unclear what to put in the (export) clause of the library @@ -222,20 +222,20 @@ compileToSS c chez appdir tm = do -- write the files log "compiler.scheme.chez" 3 $ "Generating code for " ++ chezLib - Core.writeFile (appdir chezLib <.> "ss") $ build $ concat $ + writeFile (appdir chezLib <.> "ss") $ build $ concat $ [header] ++ map snd fgndefs -- definitions using foreign libs ++ compdefs ++ loadlibs -- foreign library load statements ++ [footer] - Core.writeFile (appdir chezLib <.> "hash") cuHash + writeFile (appdir chezLib <.> "hash") cuHash pure (MkChezLib chezLib hashChanged) -- main module main <- schExp empty (Chez.chezExtPrim empty defaultLaziness) Chez.chezString defaultLaziness 0 ctm - Core.writeFile (appdir "mainprog.ss") $ build $ sepBy "\n" + writeFile (appdir "mainprog.ss") $ build $ sepBy "\n" [ schHeader (map snd libs) [lib.name | lib <- chezLibs] , collectRequestHandler , main @@ -246,14 +246,17 @@ compileToSS c chez appdir tm = do makeSh : String -> String -> String -> String -> Core () makeSh chez outShRel appDirSh targetSh = - Core.writeFile outShRel (startChez chez appDirSh targetSh) + writeFile outShRel (startChez chez appDirSh targetSh) ||| Make Windows start scripts, one for bash environments and one batch file makeShWindows : String -> String -> String -> String -> Core () makeShWindows chez outShRel appDirSh targetSh = do let cmdFile = outShRel ++ ".cmd" - Core.writeFile cmdFile (startChezCmd chez appDirSh targetSh) - Core.writeFile outShRel (startChezWinSh chez appDirSh targetSh) + writeFile cmdFile (startChezCmd chez appDirSh targetSh) + writeFile outShRel (startChezWinSh chez appDirSh targetSh) + +makeShPlatform : Bool -> String -> String -> String -> String -> Core () +makeShPlatform isWindows = if isWindows then makeShWindows else makeSh ||| Chez Scheme implementation of the `compileExpr` interface. compileExpr : @@ -264,15 +267,14 @@ compileExpr : ClosedTerm -> (outfile : String) -> Core (Maybe String) compileExpr makeitso c s tmpDir outputDir tm outfile = do -- set up paths - Just cwd <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") + cwd <- currentDir let appDirSh = outfile ++ "_app" -- relative to the launcher shell script let appDirRel = outputDir appDirSh -- relative to CWD let appDirAbs = cwd appDirRel - coreLift_ $ mkdirAll appDirRel + handleFileError appDirRel $ mkdirAll appDirRel -- generate the code - chez <- coreLift $ findChez + chez <- coreLift findChez (supportChanged, chezLibs) <- compileToSS c chez appDirRel tm -- compile the code @@ -298,10 +300,8 @@ compileExpr makeitso c s tmpDir outputDir tm outfile = do -- generate the launch script let outShRel = outputDir outfile let launchTargetSh = appDirSh "mainprog" <.> (if makeitso then "so" else "ss") - if isWindows - then makeShWindows chez outShRel appDirSh launchTargetSh - else makeSh chez outShRel appDirSh launchTargetSh - coreLift_ $ chmodRaw outShRel 0o755 + makeShPlatform isWindows chez outShRel appDirSh launchTargetSh + handleFileError outShRel $ chmodRaw outShRel 0o755 pure (Just outShRel) ||| Chez Scheme implementation of the `executeExpr` interface. @@ -313,7 +313,7 @@ executeExpr : executeExpr c s tmpDir tm = do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpchez" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift_ $ system [sh] + ignore $ system sh ||| Codegen wrapper for Chez scheme implementation. export diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index d73ca7962e..0a9f5061b8 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -379,8 +379,7 @@ compileToSCM c tm outfile extraRuntime <- getExtraRuntime ds foreign <- readDataFile "gambit/foreign.scm" let scm = sepBy "\n" [schHeader, fromString support, fromString extraRuntime, fromString foreign, code, main] - Right () <- coreLift $ writeFile outfile $ build scm - | Left err => throw (FileErr outfile err) + writeFile outfile $ build scm pure $ mapMaybe fst fgndefs compileExpr : @@ -401,10 +400,8 @@ compileExpr c s tmpDir outputDir tm outfile Nothing => gscBackend ++ ["-exe", "-cc-options", "-Wno-implicit-function-declaration", "-ld-options"] ++ libsfile Just _ => ["-c"] let cmd = gsc ++ gscCompileOpts ++ ["-o", execPath, srcPath] - ok <- coreLift $ system cmd - if ok == 0 - then pure (Just execPath) - else pure Nothing + safeSystem cmd + pure (Just execPath) executeExpr : Ref Ctxt Defs -> @@ -413,8 +410,7 @@ executeExpr : executeExpr c s tmpDir tm = do Just sh <- compileExpr c s tmpDir tmpDir tm "_tmpgambit" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift_ $ system [sh] -- TODO: on windows, should add exe extension - pure () + ignore $ system sh -- TODO: on windows, should add exe extension export codegenGambit : Codegen diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index af71b351a6..8092f69ff3 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -411,26 +411,22 @@ compileToRKT c appdir tm outfile let scm = schHeader prof (concat (map fst fgndefs)) ++ fromString support ++ fromString extraRuntime ++ code ++ runmain ++ schFooter - Right () <- coreLift $ writeFile outfile $ build scm - | Left err => throw (FileErr outfile err) - coreLift_ $ chmodRaw outfile 0o755 - pure () + writeFile outfile $ build scm + handleFileError outfile $ chmodRaw outfile 0o755 makeSh : String -> String -> String -> String -> Core () makeSh racket outShRel appdir outAbs - = do Right () <- coreLift $ writeFile outShRel (startRacket racket appdir outAbs) - | Left err => throw (FileErr outShRel err) - pure () + = writeFile outShRel (startRacket racket appdir outAbs) ||| Make Windows start scripts, one for bash environments and one batch file makeShWindows : String -> String -> String -> String -> Core () makeShWindows racket outShRel appdir outAbs = do let cmdFile = outShRel ++ ".cmd" - Right () <- coreLift $ writeFile cmdFile (startRacketCmd racket appdir outAbs) - | Left err => throw (FileErr cmdFile err) - Right () <- coreLift $ writeFile outShRel (startRacketWinSh racket appdir outAbs) - | Left err => throw (FileErr outShRel err) - pure () + writeFile cmdFile (startRacketCmd racket appdir outAbs) + writeFile outShRel (startRacketWinSh racket appdir outAbs) + +makeShPlatform : Bool -> String -> String -> String -> String -> Core () +makeShPlatform isWindows = if isWindows then makeShWindows else makeSh compileExpr : Bool -> @@ -441,9 +437,8 @@ compileExpr : compileExpr mkexec c s tmpDir outputDir tm outfile = do let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here - coreLift_ $ mkdirAll appDirGen - Just cwd <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") + handleFileError appDirGen $ mkdirAll appDirGen + cwd <- currentDir let ext = if isWindows then ".exe" else "" let outRktFile = appDirRel outfile <.> "rkt" @@ -455,23 +450,14 @@ compileExpr mkexec c s tmpDir outputDir tm outfile raco <- coreLift findRacoExe racket <- coreLift findRacket - ok <- the (Core Int) $ if mkexec - then logTime 1 "Build racket" $ - coreLift $ system $ raco ++ ["-o", outBinAbs, outRktAbs] - else pure 0 - if ok == 0 - then do -- TODO: add launcher script - let outShRel = outputDir outfile - if isWindows - then if mkexec - then makeShWindows "" outShRel appDirRel outBinFile - else makeShWindows (racket ++ " ") outShRel appDirRel outRktFile - else if mkexec - then makeSh "" outShRel appDirRel outBinFile - else makeSh (racket ++ " ") outShRel appDirRel outRktFile - coreLift_ $ chmodRaw outShRel 0o755 - pure (Just outShRel) - else pure Nothing + when mkexec $ logTime 1 "Build racket" $ + safeSystem $ raco ++ ["-o", outBinAbs, outRktAbs] + + -- TODO: add launcher script + let outShRel = outputDir outfile + makeShPlatform isWindows (if mkexec then "" else racket ++ " ") outShRel appDirRel outRktFile + handleFileError outShRel $ chmodRaw outShRel 0o755 + pure (Just outShRel) executeExpr : Ref Ctxt Defs -> @@ -480,7 +466,7 @@ executeExpr : executeExpr c s tmpDir tm = do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpracket" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift_ $ system [sh] + ignore $ system sh export codegenRacket : Codegen diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index e242cc777b..acc126ead8 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -334,9 +334,7 @@ writeToTTC extradata sourceFileName ttcFileName (NameMap.toList (foreignExports defs)) extradata) - Right ok <- coreLift $ writeToFile ttcFileName !(get Bin) - | Left err => throw (InternalError (ttcFileName ++ ": " ++ show err)) - pure () + handleFileError ttcFileName $ writeToFile ttcFileName !(get Bin) addGlobalDef : {auto c : Ref Ctxt Defs} -> (modns : ModuleIdent) -> Namespace -> @@ -477,12 +475,9 @@ readFromTTC nestedns loc reexp fname modNS importAs | True => pure Nothing put Ctxt ({ allImported $= ((fname, (modNS, reexp, importAs)) :: ) } defs) - Right buffer <- coreLift $ readFromFile fname - | Left err => throw (InternalError (fname ++ ": " ++ show err)) + buffer <- handleFileError fname $ readFromFile fname bin <- newRef Bin buffer -- for reading the file into - let as = if importAs == miAsNamespace modNS - then Nothing - else Just importAs + let as = toMaybe (importAs /= miAsNamespace modNS) importAs -- If it's already imported, but without reexporting, then all we're -- interested in is returning which other modules to load. diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 3215555b34..b75f2d39ea 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -799,6 +799,8 @@ HasNames Error where full gam (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z) full gam (TTCError x) = pure (TTCError x) full gam (FileErr x y) = pure (FileErr x y) + full gam (NonZeroExitCode x y) = pure (NonZeroExitCode x y) + full gam (SystemError x) = pure (SystemError x) full gam (CantFindPackage x) = pure (CantFindPackage x) full gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc) full gam (LazyPatternVar fc) = pure (LazyPatternVar fc) @@ -897,6 +899,8 @@ HasNames Error where resolved gam (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z) resolved gam (TTCError x) = pure (TTCError x) resolved gam (FileErr x y) = pure (FileErr x y) + resolved gam (NonZeroExitCode x y) = pure (NonZeroExitCode x y) + resolved gam (SystemError x) = pure (SystemError x) resolved gam (CantFindPackage x) = pure (CantFindPackage x) resolved gam (LazyImplicitFunction fc) = pure (LazyImplicitFunction fc) resolved gam (LazyPatternVar fc) = pure (LazyPatternVar fc) @@ -2181,17 +2185,13 @@ setSourceDir mdir = update Ctxt { options->dirs->source_dir := mdir } export setWorkingDir : {auto c : Ref Ctxt Defs} -> String -> Core () setWorkingDir dir - = do coreLift_ $ changeDir dir - Just cdir <- coreLift $ currentDir - | Nothing => throw (InternalError "Can't get current directory") + = do unsafeChangeDir dir + cdir <- currentDir update Ctxt { options->dirs->working_dir := cdir } export getWorkingDir : Core String -getWorkingDir - = do Just d <- coreLift $ currentDir - | Nothing => throw (InternalError "Can't get current directory") - pure d +getWorkingDir = currentDir export setExtraDirs : {auto c : Ref Ctxt Defs} -> List String -> Core () @@ -2207,7 +2207,7 @@ withCtxt = wrapRef Ctxt resetCtxt where resetCtxt : Defs -> Core () resetCtxt defs = do let dir = defs.options.dirs.working_dir - coreLift_ $ changeDir dir + changeDir dir export setPrefix : {auto c : Ref Ctxt Defs} -> String -> Core () diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 8658f819d6..35adbae0c3 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -14,6 +14,8 @@ import Libraries.Text.PrettyPrint.Prettyprinter.Doc import Libraries.Data.Tap import public Data.IORef +import System +import System.Directory import System.File %default covering @@ -171,6 +173,8 @@ data Error : Type where (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error + NonZeroExitCode : String -> Int -> Error + SystemError : String -> Error CantFindPackage : String -> Error LazyImplicitFunction : FC -> Error LazyPatternVar : FC -> Error @@ -360,6 +364,8 @@ Show Error where show (GenericMsgSol fc msg solutionHeader sols) = show fc ++ ":" ++ msg ++ " \{solutionHeader}: " ++ show sols show (TTCError msg) = "Error in TTC file: " ++ show msg show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err + show (NonZeroExitCode cmd status) = "Command '\{cmd}' exited with return code \{show status}" + show (SystemError msg) = "System error: '\{msg}'" show (CantFindPackage fname) = "Can't find package " ++ fname show (LazyImplicitFunction fc) = "Implicit lazy functions are not yet supported" show (LazyPatternVar fc) = "Defining lazy functions via pattern matching is not yet supported" @@ -476,6 +482,8 @@ getErrorLoc (GenericMsg loc _) = Just loc getErrorLoc (GenericMsgSol loc _ _ _) = Just loc getErrorLoc (TTCError _) = Nothing getErrorLoc (FileErr _ _) = Nothing +getErrorLoc (NonZeroExitCode _ _) = Nothing +getErrorLoc (SystemError _) = Nothing getErrorLoc (CantFindPackage _) = Nothing getErrorLoc (LazyImplicitFunction loc) = Just loc getErrorLoc (LazyPatternVar loc) = Just loc @@ -566,6 +574,8 @@ killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x killErrorLoc (GenericMsgSol fc x y z) = GenericMsgSol emptyFC x y z killErrorLoc (TTCError x) = TTCError x killErrorLoc (FileErr x y) = FileErr x y +killErrorLoc (NonZeroExitCode x y) = NonZeroExitCode x y +killErrorLoc (SystemError x) = SystemError x killErrorLoc (CantFindPackage x) = CantFindPackage x killErrorLoc (LazyImplicitFunction fc) = LazyImplicitFunction emptyFC killErrorLoc (LazyPatternVar fc) = LazyPatternVar emptyFC @@ -642,14 +652,12 @@ export %inline (<$) = (<$>) . const export %inline -ignore : Core a -> Core () -ignore = map (\ _ => ()) +($>) : Core a -> b -> Core b +($>) = flip (<$) --- This would be better if we restrict it to a limited set of IO operations -export -%inline -coreLift_ : IO a -> Core () -coreLift_ op = ignore (coreLift op) +export %inline +ignore : Core a -> Core () +ignore = map (const ()) -- Monad (specialised) export %inline @@ -943,19 +951,60 @@ condC [] def = def condC ((x, y) :: xs) def = if !x then y else condC xs def +export +currentDir : Core String +currentDir = maybe (throw $ SystemError "Failed to get the current directory") pure !(coreLift currentDir) + +||| Change the current working directory to the specified path. +||| Throws `SystemError` if the operation did not succeed. +export +changeDir : String -> Core () +changeDir dir = + unless !(coreLift $ changeDir dir) $ + throw $ SystemError "Failed to change directory to '\{dir}'" + +||| Change the current working directory to the specified path. Ignores errors. +export +unsafeChangeDir : String -> Core () +unsafeChangeDir = ignore . coreLift . changeDir + +export +handleFileError : (fname : String) -> IO (Either FileError a) -> Core a +handleFileError fname res = either (throw . FileErr fname) pure !(coreLift res) + +||| Write the given string to the file at the specified name. +||| Throws `FileErr` when errors occur. export writeFile : (fname : String) -> (content : String) -> Core () -writeFile fname content = - coreLift (writeFile fname content) >>= \case - Right () => pure () - Left err => throw $ FileErr fname err +writeFile fname content = handleFileError fname $ writeFile fname content +||| Read the entire file at the given name. Throws `FileErr` when errors occur. export readFile : (fname : String) -> Core String -readFile fname = - coreLift (readFile fname) >>= \case - Right content => pure content - Left err => throw $ FileErr fname err +readFile fname = handleFileError fname $ readFile fname + +handleExitCode : String -> ExitCode -> Core () +handleExitCode _ ExitSuccess = pure () +handleExitCode cmd (ExitFailure status) = throw $ NonZeroExitCode cmd status + +export +system : String -> Core ExitCode +system = map cast . coreLift . system + +||| Execute a shell command. Throws `NonZeroExitCode` if the command returns +||| non-zero exit code. +export +safeSystem : String -> Core () +safeSystem cmd = system cmd >>= handleExitCode cmd + +namespace Escaped + export + system : List String -> Core ExitCode + system = map cast . coreLift . system + + export + safeSystem : List String -> Core () + safeSystem cmd = system cmd >>= handleExitCode (escapeCmd cmd) namespace Functor diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index 938006d2d9..e024b43026 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -35,8 +35,7 @@ export pkgLocalDirectory : {auto c : Ref Ctxt Defs} -> Core String pkgLocalDirectory = do d <- getDirs - Just srcdir <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") + srcdir <- currentDir pure $ srcdir depends_dir d ------------------------------------------------------------------------ @@ -167,11 +166,7 @@ export covering readDataFile : {auto c : Ref Ctxt Defs} -> String -> Core String -readDataFile fname - = do f <- findDataFile fname - Right d <- coreLift $ readFile f - | Left err => throw (FileErr f err) - pure d +readDataFile fname = readFile !(findDataFile fname) ||| Look for a library file required by a code generator. Look in the ||| library directories, and in the lib/ subdirectory of all the 'extra import' @@ -282,17 +277,13 @@ makeBuildDirectory ns = do bdir <- ttcBuildDirectory let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name let ndir = joinPath ns - Right _ <- coreLift $ mkdirAll (bdir ndir) - | Left err => throw (FileErr (bdir ndir) err) - pure () + let path = bdir ndir + handleFileError path $ mkdirAll path export covering ensureDirectoryExists : String -> Core () -ensureDirectoryExists dir - = do Right _ <- coreLift $ mkdirAll dir - | Left err => throw (FileErr dir err) - pure () +ensureDirectoryExists dir = handleFileError dir $ mkdirAll dir -- Given a source file, return the name of the ttc file to generate export diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index cb7d867b48..4a0a369278 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -435,17 +435,14 @@ writeToTTM fname meta <- get MD defs <- get Ctxt toBuf buf (MkTTMFile ttcVersion !(full (gamma defs) meta)) - Right ok <- coreLift $ writeToFile fname !(get Bin) - | Left err => throw (InternalError (fname ++ ": " ++ show err)) - pure () + handleFileError fname $ writeToFile fname !(get Bin) export readFromTTM : {auto m : Ref MD Metadata} -> (fname : String) -> Core () readFromTTM fname - = do Right buf <- coreLift $ readFromFile fname - | Left err => throw (InternalError (fname ++ ": " ++ show err)) + = do buf <- handleFileError fname $ readFromFile fname bin <- newRef Bin buf ttm <- fromBuf bin put MD (metadata ttm) @@ -454,8 +451,7 @@ readFromTTM fname export readMetadata : (fname : String) -> Core Metadata readMetadata fname - = do Right buf <- coreLift $ readFromFile fname - | Left err => throw (InternalError (fname ++ ": " ++ show err)) + = do buf <- handleFileError fname $ readFromFile fname bin <- newRef Bin buf MkTTMFile _ md <- fromBuf bin pure md diff --git a/src/Core/SchemeEval/Compile.idr b/src/Core/SchemeEval/Compile.idr index 2f98457acd..bca7f655f1 100644 --- a/src/Core/SchemeEval/Compile.idr +++ b/src/Core/SchemeEval/Compile.idr @@ -606,8 +606,7 @@ initEvalWith "racket" | Nothing => pure False put Ctxt ({ schemeEvalLoaded := True } defs) pure True) - (\err => do coreLift $ printLn err - pure False) + (\err => coreLift (printLn err) $> False) initEvalWith _ = pure False -- only works on Chez for now -- Initialise the internal functions we need to build/extend blocked diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index 6c6435d576..a5a11a8fd6 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -88,8 +88,7 @@ updateEnv ("idris2-" ++ showVersion False version) "support") addLibDir (prefix_dir (dirs (options defs)) ("idris2-" ++ showVersion False version) "lib") - Just cwd <- coreLift $ currentDir - | Nothing => throw (InternalError "Can't get current directory") + cwd <- currentDir addLibDir cwd updateREPLOpts : {auto o : Ref ROpts REPLOpts} -> diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 0b358f200a..a75a5c9135 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -711,6 +711,10 @@ perrorRaw (TTCError msg) perrorRaw (FileErr fname err) = pure $ errorDesc (reflow "File error in" <++> pretty0 fname <++> colon) <++> byShow err +perrorRaw (NonZeroExitCode cmd status) + = pure $ errorDesc (reflow "Command" <++> enclose "'" "'" (reflow cmd) <++> "exited with return code" <++> byShow status) +perrorRaw (SystemError msg) + = pure $ errorDesc (reflow "System error" <+> colon) <++> pretty0 msg perrorRaw (CantFindPackage fname) = pure $ errorDesc (reflow "Can't find package " <++> pretty0 fname) perrorRaw (LazyImplicitFunction fc) diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr index 9e772d4c44..e6f63f1274 100644 --- a/src/Idris/IDEMode/CaseSplit.idr +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -293,8 +293,7 @@ updateCase splits line col case mainfile opts of Nothing => throw (InternalError "No file loaded") Just f => - do Right file <- coreLift $ readFile f - | Left err => throw (FileErr f err) + do file <- readFile f let thisline = elemAt (lines file) (integerToNat (cast line)) case thisline of Nothing => throw (InternalError "File too short!") diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index ba918e90f7..6e50284eb8 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -221,8 +221,7 @@ needsBuilding sourceFile ttcFile depFiles | False => pure False -- if it needs rebuilding then remove the buggy .ttc file to avoid going -- into an infinite loop! - Right () <- coreLift $ removeFile ttcFile - | Left err => throw (FileErr ttcFile err) + handleFileError ttcFile $ removeFile ttcFile pure True diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 349b01aee4..c06f8007c7 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -651,7 +651,7 @@ install pkg opts installSrc -- not used but might be in the future let pkgStr = String.renderString $ layoutUnbounded $ pretty $ savePkgMetadata pkg log "package.depends" 25 $ " package file:\n\{pkgStr}" - coreLift_ $ writeFile pkgFile pkgStr + writeFile pkgFile pkgStr runScript (postinstall pkg) where @@ -756,24 +756,21 @@ makeDoc pkg opts = let modExports = map (map (reAnnotate Syntax . prettyImport)) mreexports - Right () <- do doc <- renderModuleDoc mod modDoc modExports - (allDecls <$ guard (not $ null allDocs)) - coreLift $ writeFile outputFilePath doc - | Left err => fileError (docBase "index.html") err + doc <- renderModuleDoc mod modDoc modExports + (allDecls <$ guard (not $ null allDocs)) + writeFile outputFilePath doc pure $ the (List Error) [] ) | errs => pure errs - Right () <- do syn <- get Syn - coreLift $ writeFile (docBase "index.html") $ renderDocIndex pkg (modDocstrings syn) - | Left err => fileError (docBase "index.html") err + syn <- get Syn + writeFile (docBase "index.html") $ renderDocIndex pkg (modDocstrings syn) errs <- for cssFiles $ \ cssFile => do let fn = cssFile.filename ++ ".css" css <- readDataFile ("docs/" ++ fn) - Right () <- coreLift $ writeFile (docBase fn) css - | Left err => fileError (docBase fn) err + writeFile (docBase fn) css pure (the (List Error) []) let [] = concat errs @@ -926,9 +923,7 @@ processPackage opts (cmd, mfile) let fp = fromMaybe (pkg.name ++ ".ipkg") mfile False <- coreLift (exists fp) | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists")) - Right () <- coreLift $ writeFile fp (show $ pretty pkg) - | Left err => throw (FileErr fp err) - pure () + writeFile fp (show $ pretty pkg) _ => do file <- localPackageFile mfile let Just (dir, filename) = splitParent file @@ -1060,7 +1055,7 @@ findIpkg : {auto c : Ref Ctxt Defs} -> findIpkg fname = do Just (dir, ipkgn, up) <- coreLift findIpkgFile | Nothing => pure fname - coreLift_ $ changeDir dir + changeDir dir setWorkingDir dir pkg <- parsePkgFile True ipkgn maybe (pure ()) setBuildDir (builddir pkg) diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 66968e1980..4a55029ded 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -219,8 +219,7 @@ readHeader : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> (path : String) -> (origin : ModuleIdent) -> Core Module readHeader path origin - = do Right res <- coreLift (readFile path) - | Left err => throw (FileErr path err) + = do res <- readFile path -- Stop at the first :, that's definitely not part of the header, to -- save lexing the whole file unnecessarily setCurrentElabSource res -- for error printing purposes diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 1234cda893..ca71f45017 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -87,24 +87,24 @@ import System.File showInfo : {auto c : Ref Ctxt Defs} -> (Name, Int, GlobalDef) -> Core () showInfo (n, idx, d) - = do coreLift_ $ putStrLn (show (fullname d) ++ " ==> " ++ + = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++ show !(toFullNames (definition d))) - coreLift_ $ putStrLn (show (multiplicity d)) - coreLift_ $ putStrLn ("Erasable args: " ++ show (eraseArgs d)) - coreLift_ $ putStrLn ("Detaggable arg types: " ++ show (safeErase d)) - coreLift_ $ putStrLn ("Specialise args: " ++ show (specArgs d)) - coreLift_ $ putStrLn ("Inferrable args: " ++ show (inferrable d)) + coreLift $ putStrLn (show (multiplicity d)) + coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d)) + coreLift $ putStrLn ("Detaggable arg types: " ++ show (safeErase d)) + coreLift $ putStrLn ("Specialise args: " ++ show (specArgs d)) + coreLift $ putStrLn ("Inferrable args: " ++ show (inferrable d)) whenJust (compexpr d) $ \ expr => - coreLift_ $ putStrLn ("Compiled: " ++ show expr) - coreLift_ $ putStrLn ("Refers to: " ++ + coreLift $ putStrLn ("Compiled: " ++ show expr) + coreLift $ putStrLn ("Refers to: " ++ show !(traverse getFullName (keys (refersTo d)))) - coreLift_ $ putStrLn ("Refers to (runtime): " ++ + coreLift $ putStrLn ("Refers to (runtime): " ++ show !(traverse getFullName (keys (refersToRuntime d)))) - coreLift_ $ putStrLn ("Flags: " ++ show (flags d)) + coreLift $ putStrLn ("Flags: " ++ show (flags d)) when (not (isNil (sizeChange d))) $ let scinfo = map (\s => show (fnCall s) ++ ": " ++ show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in - coreLift_ $ putStrLn $ + coreLift $ putStrLn $ "Size change: " ++ showSep ", " scinfo prettyInfo : {auto c : Ref Ctxt Defs} -> @@ -246,10 +246,9 @@ updateFile update = do opts <- get ROpts let Just f = mainfile opts | Nothing => pure (DisplayEdit emptyDoc) -- no file, nothing to do - Right content <- coreLift $ readFile f - | Left err => throw (FileErr f err) - coreLift_ $ writeFile (f ++ "~") content - coreLift_ $ writeFile f (unlines (update (lines content))) + content <- readFile f + writeFile (f ++ "~") content + writeFile f (unlines (update (lines content))) pure (DisplayEdit emptyDoc) rtrim : String -> String @@ -974,7 +973,7 @@ process Edit Nothing => pure NoFileLoaded Just f => do let line = maybe [] (\i => ["+" ++ show (i + 1)]) (errorLine opts) - coreLift_ $ system $ [editor opts, f] ++ line + safeSystem $ [editor opts, f] ++ line loadMainFile f process (Compile ctm outfile) = compileExp ctm outfile @@ -1072,7 +1071,7 @@ process (CGDirective str) = do setSession ({ directives $= (str::) } !getSession) pure Done process (RunShellCommand cmd) - = do coreLift_ (system cmd) + = do safeSystem cmd pure Done process Quit = pure Exited @@ -1181,14 +1180,14 @@ mutual repl = do ns <- getNS opts <- get ROpts - coreLift_ (putStr (prompt (evalMode opts) ++ show ns ++ "> ")) - coreLift_ (fflush stdout) + coreLift (putStr (prompt (evalMode opts) ++ show ns ++ "> ")) + coreLift (fflush stdout) inp <- coreLift getLine end <- coreLift $ fEOF stdin if end then do -- start a new line in REPL mode (not relevant in IDE mode) - coreLift_ $ putStrLn "" + coreLift $ putStrLn "" iputStrLn "Bye for now!" else do res <- interpret inp handleResult res diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 679cdd88f5..ef088105bc 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -228,10 +228,8 @@ dirOption dirs Prefix findIpkg : {auto c : Ref Ctxt Defs} -> Core (List String) findIpkg = - do Just srcdir <- coreLift currentDir - | Nothing => throw (InternalError "Can't get current directory") - Right fs <- coreLift $ listDir srcdir - | Left err => pure [] + do srcdir <- currentDir + fs <- handleFileError srcdir $ listDir srcdir pure $ filter (".ipkg" `isSuffixOf`) fs -- keep only those Strings, of which `x` is a prefix diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 9caad56208..739edbf2fe 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -216,5 +216,4 @@ processTTImpFile fname Nothing <- checkDelayedHoles | Just err => throw err pure True) - (\err => do coreLift_ (printLn err) - pure False) + (\err => coreLift (printLn err) $> False) diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index 60800bb226..b773be3b6d 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -49,16 +49,16 @@ yaffleMain sourceFileName args whenJust t $ setLogTimings addPrimitives case extension sourceFileName of - Just "ttc" => do coreLift_ $ putStrLn "Processing as TTC" + Just "ttc" => do coreLift $ putStrLn "Processing as TTC" ignore $ readFromTTC {extra = ()} True emptyFC True sourceFileName (nsAsModuleIdent emptyNS) emptyNS - coreLift_ $ putStrLn "Read TTC" - _ => do coreLift_ $ putStrLn "Processing as TTImp" + coreLift $ putStrLn "Read TTC" + _ => do coreLift $ putStrLn "Processing as TTImp" ok <- processTTImpFile sourceFileName when ok $ do makeBuildDirectory modIdent ttcFileName <- getTTCFileName sourceFileName "ttc" writeToTTC () sourceFileName ttcFileName - coreLift_ $ putStrLn "Written TTC" + coreLift $ putStrLn "Written TTC" repl {c} {u} {s} {o} ymain : IO () diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr index e6f06415df..c888cfcb3f 100644 --- a/src/Yaffle/REPL.idr +++ b/src/Yaffle/REPL.idr @@ -30,9 +30,9 @@ import Parser.Source showInfo : (Name, Int, GlobalDef) -> Core () showInfo (n, _, d) - = coreLift_ $ putStrLn (show n ++ " ==>\n" ++ - "\t" ++ show (definition d) ++ "\n" ++ - "\t" ++ show (sizeChange d) ++ "\n") + = coreLift $ putStrLn (show n ++ " ==>\n" ++ + "\t" ++ show (definition d) ++ "\n" ++ + "\t" ++ show (sizeChange d) ++ "\n") -- Returns 'True' if the REPL should continue process : {auto c : Ref Ctxt Defs} -> @@ -45,7 +45,7 @@ process (Eval ttimp) = do (tm, _) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing defs <- get Ctxt tmnf <- normalise defs [] tm - coreLift_ (printLn !(unelab [] tmnf)) + coreLift (printLn !(unelab [] tmnf)) pure True process (Check (IVar _ n)) = do defs <- get Ctxt @@ -57,14 +57,14 @@ process (Check (IVar _ n)) printName (n, _, tyh) = do defs <- get Ctxt ty <- normaliseHoles defs [] tyh - coreLift_ $ putStrLn $ show n ++ " : " ++ - show !(unelab [] ty) + coreLift $ putStrLn $ show n ++ " : " ++ + show !(unelab [] ty) process (Check ttimp) = do (tm, gty) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing defs <- get Ctxt tyh <- getTerm gty ty <- normaliseHoles defs [] tyh - coreLift_ (printLn !(unelab [] ty)) + coreLift (printLn !(unelab [] ty)) pure True process (ProofSearch n_in) = do defs <- get Ctxt @@ -73,7 +73,7 @@ process (ProofSearch n_in) def <- search (justFC defaultFC) top False 1000 n ty [] defs <- get Ctxt defnf <- normaliseHoles defs [] def - coreLift_ (printLn !(toFullNames defnf)) + coreLift (printLn !(toFullNames defnf)) pure True process (ExprSearch n_in) = do defs <- get Ctxt @@ -85,18 +85,18 @@ process (ExprSearch n_in) process (GenerateDef line name) = do defs <- get Ctxt Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p) - | Nothing => do coreLift_ (putStrLn ("Can't find declaration for " ++ show name)) + | Nothing => do coreLift (putStrLn ("Can't find declaration for " ++ show name)) pure True case !(lookupDefExact n' (gamma defs)) of Just None => catch (do ((fc, cs) :: _) <- logTime 0 "Generation" $ makeDefN (\p, n => onLine line p) 1 n' - | _ => coreLift_ (putStrLn "Failed") - coreLift_ $ putStrLn (show cs)) - (\err => coreLift_ $ putStrLn $ "Can't find a definition for " ++ show n') - Just _ => coreLift_ $ putStrLn "Already defined" - Nothing => coreLift_ $ putStrLn $ "Can't find declaration for " ++ show name + | _ => coreLift (putStrLn "Failed") + coreLift $ putStrLn (show cs)) + (\err => coreLift $ putStrLn $ "Can't find a definition for " ++ show n') + Just _ => coreLift $ putStrLn "Already defined" + Nothing => coreLift $ putStrLn $ "Can't find declaration for " ++ show name pure True process (Missing n_in) = do defs <- get Ctxt @@ -106,15 +106,15 @@ process (Missing n_in) do tot <- getTotality emptyFC fn case isCovering tot of MissingCases cs => - coreLift_ (putStrLn (show fn ++ ":\n" ++ - showSep "\n" (map show cs))) + coreLift (putStrLn (show fn ++ ":\n" ++ + showSep "\n" (map show cs))) NonCoveringCall ns => - coreLift_ (putStrLn + coreLift (putStrLn (show fn ++ ": Calls non covering function" ++ case ns of [fn] => " " ++ show fn _ => "s: " ++ showSep ", " (map show ns))) - _ => coreLift_ $ putStrLn (show fn ++ ": All cases covered")) + _ => coreLift $ putStrLn (show fn ++ ": All cases covered")) (map fst ts) pure True process (CheckTotal n) @@ -124,7 +124,7 @@ process (CheckTotal n) ts => do traverse_ (\fn => do ignore $ checkTotal emptyFC fn tot <- getTotality emptyFC fn - coreLift_ (putStrLn (show fn ++ " is " ++ show tot))) + coreLift (putStrLn (show fn ++ " is " ++ show tot))) (map fst ts) pure True process (DebugInfo n) @@ -132,7 +132,7 @@ process (DebugInfo n) traverse_ showInfo !(lookupCtxtName n (gamma defs)) pure True process Quit - = do coreLift_ $ putStrLn "Bye for now!" + = do coreLift $ putStrLn "Bye for now!" pure False processCatch : {auto c : Ref Ctxt Defs} -> @@ -143,8 +143,7 @@ processCatch : {auto c : Ref Ctxt Defs} -> ImpREPL -> Core Bool processCatch cmd = catch (process cmd) - (\err => do coreLift_ (putStrLn (show err)) - pure True) + (\err => coreLift (putStrLn $ show err) $> True) export repl : {auto c : Ref Ctxt Defs} -> @@ -154,9 +153,9 @@ repl : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> Core () repl - = do coreLift_ (putStr "Yaffle> ") + = do coreLift (putStr "Yaffle> ") inp <- coreLift getLine case runParser (Virtual Interactive) Nothing inp command of - Left err => do coreLift_ (printLn err) + Left err => do coreLift (printLn err) repl Right (_, _, cmd) => when !(processCatch cmd) repl diff --git a/tests/chez/chez037/expected b/tests/chez/chez037/expected index eecae810fc..7ad0e81ce9 100644 --- a/tests/chez/chez037/expected +++ b/tests/chez/chez037/expected @@ -1 +1 @@ -Error: INTERNAL ERROR: Chez exited with return code 1 +Error: Command '"false" "--script" "build/exec/hello_app/compileChez"' exited with return code 1 From 234fb60ecadc0f32c5fb7e4a0c1da05258e7c335 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 14:33:18 +0300 Subject: [PATCH 03/16] [ refactor ] Remove `Maybe` from `compileExpr` and `incCompileFile` signatures --- src/Compiler/Common.idr | 8 ++++---- src/Compiler/ES/Javascript.idr | 4 ++-- src/Compiler/ES/Node.idr | 7 +++---- src/Compiler/Interpreter/VMCode.idr | 2 +- src/Compiler/RefC/RefC.idr | 8 +++----- src/Compiler/Scheme/Chez.idr | 20 +++++++++----------- src/Compiler/Scheme/ChezSep.idr | 8 +++----- src/Compiler/Scheme/Gambit.idr | 8 +++----- src/Compiler/Scheme/Racket.idr | 8 +++----- src/Idris/REPL.idr | 5 +---- 10 files changed, 32 insertions(+), 46 deletions(-) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index f1ba3539ba..9154c10bea 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -40,7 +40,7 @@ record Codegen where ||| Compile an Idris 2 expression, saving it to a file. compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String ||| Execute an Idris 2 expression directly. executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () @@ -52,7 +52,7 @@ record Codegen where ||| directory as the associated TTC. incCompileFile : Maybe (Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (sourcefile : String) -> - Core (Maybe (String, List String))) + Core (String, List String)) ||| If incremental compilation is supported, get the output file extension incExt : Maybe String @@ -105,7 +105,7 @@ export compile : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> Codegen -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compile {c} {s} cg tm out = do d <- getDirs let tmpDir = execBuildDir d @@ -135,7 +135,7 @@ incCompile : {auto c : Ref Ctxt Defs} -> incCompile {c} {s} cg src = do let Just inc = incCompileFile cg | Nothing => pure Nothing - inc c s src + Just <$> inc c s src -- If an entry isn't already decoded, get the minimal entry we need for -- compilation, and record the Binary so that we can put it back when we're diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index 557a5d171a..cb8f5a19cc 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -56,13 +56,13 @@ compileExpr : (outputDir : String) -> ClosedTerm -> (outfile : String) -> - Core (Maybe String) + Core String compileExpr c s tmpDir outputDir tm outfile = do es <- compileToJS c s tm let res = addHeaderAndFooter outfile es let out = outputDir outfile writeFile out res - pure (Just out) + pure out ||| Node implementation of the `executeExpr` interface. executeExpr : diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index b5e337d582..82c5fadfec 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -50,13 +50,13 @@ compileExpr : (outputDir : String) -> ClosedTerm -> (outfile : String) -> - Core (Maybe String) + Core String compileExpr c s tmpDir outputDir tm outfile = do es <- compileToNode c s tm let out = outputDir outfile writeFile out es handleFileError out $ chmodRaw out 0o755 - pure (Just out) + pure out ||| Node implementation of the `executeExpr` interface. executeExpr : @@ -64,8 +64,7 @@ executeExpr : Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm = - do Just out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js" - | Nothing => throw (InternalError "compileExpr returned Nothing") + do out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js" node <- coreLift findNode ignore $ system [node, out] diff --git a/src/Compiler/Interpreter/VMCode.idr b/src/Compiler/Interpreter/VMCode.idr index 1334504bfd..96caf05453 100644 --- a/src/Compiler/Interpreter/VMCode.idr +++ b/src/Compiler/Interpreter/VMCode.idr @@ -287,7 +287,7 @@ parameters {auto c : Ref Ctxt Defs} compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - String -> String -> ClosedTerm -> String -> Core (Maybe String) + String -> String -> ClosedTerm -> String -> Core String compileExpr _ _ _ _ _ _ = throw (InternalError "compile not implemeted for vmcode-interp") executeExpr : diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index fe38da8be1..48d93b77c2 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -989,7 +989,7 @@ compileExpr : Ref Ctxt Defs -> (outputDir : String) -> ClosedTerm -> (outfile : String) - -> Core (Maybe String) + -> Core String compileExpr c s _ outputDir tm outfile = do let outn = outputDir outfile <.> "c" let outobj = outputDir outfile <.> "o" @@ -1001,15 +1001,13 @@ compileExpr c s _ outputDir tm outfile = generateCSourceFile defs outn obj <- compileCObjectFile outn outobj - Just <$> compileCFile obj outexec + compileCFile obj outexec export executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (execDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm = do - do Just sh <- compileExpr c s tmpDir tmpDir tm "_tmp_refc" - | Nothing => coreLift $ putStrLn "Error: failed to compile" - ignore $ system sh + do ignore . system =<< compileExpr c s tmpDir tmpDir tm "_tmp_refc" export codegenRefC : Codegen diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 3b53d65543..697f056b70 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -578,7 +578,7 @@ compileExprWhole : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compileExprWhole makeitso c s tmpDir outputDir tm outfile = do let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here @@ -598,14 +598,14 @@ compileExprWhole makeitso c s tmpDir outputDir tm outfile then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) "--program" else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile) handleFileError outShRel $ chmodRaw outShRel 0o755 - pure (Just outShRel) + pure outShRel compileExprInc : Bool -> Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compileExprInc makeitso c s tmpDir outputDir tm outfile = do defs <- get Ctxt let Just (mods, libs) = lookup Chez (allIncData defs) @@ -627,7 +627,7 @@ compileExprInc makeitso c s tmpDir outputDir tm outfile then makeShWindows chez outShRel appDirRel outSsFile "--script" else makeSh outShRel appDirRel outSsFile handleFileError outShRel $ chmodRaw outShRel 0o755 - pure (Just outShRel) + pure outShRel ||| Chez Scheme implementation of the `compileExpr` interface. compileExpr : @@ -635,7 +635,7 @@ compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compileExpr makeitso c s tmpDir outputDir tm outfile = do sesh <- getSession if not (wholeProgram sesh) && (Chez `elem` incrementalCGs sesh) @@ -649,14 +649,12 @@ executeExpr : Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm - = do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpchez" - | Nothing => throw (InternalError "compileExpr returned Nothing") - ignore $ system sh + = ignore . system =<< compileExpr False c s tmpDir tmpDir tm "_tmpchez" incCompile : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (sourceFile : String) -> Core (Maybe (String, List String)) + (sourceFile : String) -> Core (String, List String) incCompile c s sourceFile = do ssFile <- getTTCFileName sourceFile "ss" @@ -669,7 +667,7 @@ incCompile c s sourceFile let ndefs = namedDefs cdata if isNil ndefs - then pure (Just ("", [])) + then pure ("", []) -- ^ no code to generate, but still recored that the -- module has been compiled, with no output needed. else do @@ -690,7 +688,7 @@ incCompile c s sourceFile show ssFile ++ "))" writeFile tmpFileAbs build safeSystem [chez, "--script", tmpFileAbs] - pure (Just (soFilename, mapMaybe fst fgndefs)) + pure (soFilename, mapMaybe fst fgndefs) ||| Codegen wrapper for Chez scheme implementation. export diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index 552afb0d4b..0e5d1237c6 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -264,7 +264,7 @@ compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compileExpr makeitso c s tmpDir outputDir tm outfile = do -- set up paths cwd <- currentDir @@ -302,7 +302,7 @@ compileExpr makeitso c s tmpDir outputDir tm outfile = do let launchTargetSh = appDirSh "mainprog" <.> (if makeitso then "so" else "ss") makeShPlatform isWindows chez outShRel appDirSh launchTargetSh handleFileError outShRel $ chmodRaw outShRel 0o755 - pure (Just outShRel) + pure outShRel ||| Chez Scheme implementation of the `executeExpr` interface. ||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it. @@ -311,9 +311,7 @@ executeExpr : Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm - = do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpchez" - | Nothing => throw (InternalError "compileExpr returned Nothing") - ignore $ system sh + = ignore . system =<< compileExpr False c s tmpDir tmpDir tm "_tmpchez" ||| Codegen wrapper for Chez scheme implementation. export diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 0a9f5061b8..0687aec593 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -386,7 +386,7 @@ compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compileExpr c s tmpDir outputDir tm outfile = do let srcPath = tmpDir outfile <.> "scm" let execPath = outputDir outfile @@ -401,16 +401,14 @@ compileExpr c s tmpDir outputDir tm outfile Just _ => ["-c"] let cmd = gsc ++ gscCompileOpts ++ ["-o", execPath, srcPath] safeSystem cmd - pure (Just execPath) + pure execPath executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm - = do Just sh <- compileExpr c s tmpDir tmpDir tm "_tmpgambit" - | Nothing => throw (InternalError "compileExpr returned Nothing") - ignore $ system sh -- TODO: on windows, should add exe extension + = ignore . system =<< compileExpr c s tmpDir tmpDir tm "_tmpgambit" -- TODO: on windows, should add exe extension export codegenGambit : Codegen diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 8092f69ff3..2ae21e4998 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -433,7 +433,7 @@ compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (outputDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compileExpr mkexec c s tmpDir outputDir tm outfile = do let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here @@ -457,16 +457,14 @@ compileExpr mkexec c s tmpDir outputDir tm outfile let outShRel = outputDir outfile makeShPlatform isWindows (if mkexec then "" else racket ++ " ") outShRel appDirRel outRktFile handleFileError outShRel $ chmodRaw outShRel 0o755 - pure (Just outShRel) + pure outShRel executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c s tmpDir tm - = do Just sh <- compileExpr False c s tmpDir tmpDir tm "_tmpracket" - | Nothing => throw (InternalError "compileExpr returned Nothing") - ignore $ system sh + = ignore . system =<< compileExpr False c s tmpDir tmpDir tm "_tmpracket" export codegenRacket : Codegen diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index ca71f45017..21a2ab0836 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -813,10 +813,7 @@ compileExp ctm outfile do iputStrLn (reflow "No such code generator available") pure CompilationFailed tm_erased <- prepareExp ctm - ok <- compile cg tm_erased outfile - maybe (pure CompilationFailed) - (pure . Compiled) - ok + Compiled <$> compile cg tm_erased outfile export loadMainFile : {auto c : Ref Ctxt Defs} -> From 99b8b075dc1af1a9730107a4285e3035b9b70f2a Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 14:50:30 +0300 Subject: [PATCH 04/16] [ refactor ] Return the exit code from the `--exec` command --- src/Compiler/Common.idr | 5 +- src/Compiler/ES/Javascript.idr | 4 +- src/Compiler/ES/Node.idr | 4 +- src/Compiler/Interpreter/VMCode.idr | 5 +- src/Compiler/RefC/RefC.idr | 5 +- src/Compiler/Scheme/Chez.idr | 5 +- src/Compiler/Scheme/ChezSep.idr | 5 +- src/Compiler/Scheme/Gambit.idr | 5 +- src/Compiler/Scheme/Racket.idr | 5 +- src/Idris/Driver.idr | 145 ++++++++++++++-------------- src/Idris/IDEMode/REPL.idr | 2 +- src/Idris/REPL.idr | 8 +- src/Idris/REPL/Common.idr | 3 +- src/Idris/SetOptions.idr | 25 ++--- tests/cli/exitCode001/Main.idr | 11 +++ tests/cli/exitCode001/expected | 13 +++ tests/cli/exitCode001/run | 9 ++ 17 files changed, 146 insertions(+), 113 deletions(-) create mode 100644 tests/cli/exitCode001/Main.idr create mode 100644 tests/cli/exitCode001/expected create mode 100755 tests/cli/exitCode001/run diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 9154c10bea..a2668fad6b 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -28,6 +28,7 @@ import Libraries.Utils.Scheme import Idris.Syntax import Idris.Env +import System import System.Directory import System.Info @@ -43,7 +44,7 @@ record Codegen where ClosedTerm -> (outfile : String) -> Core String ||| Execute an Idris 2 expression directly. executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () + (tmpDir : String) -> ClosedTerm -> Core ExitCode ||| Incrementally compile definitions in the current module (toIR defs) ||| if supported ||| Takes a source file name, returns the name of the generated object @@ -121,7 +122,7 @@ compile {c} {s} cg tm out export execute : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - Codegen -> ClosedTerm -> Core () + Codegen -> ClosedTerm -> Core ExitCode execute {c} {s} cg tm = do d <- getDirs let tmpDir = execBuildDir d diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index cb8f5a19cc..50c54d4cc4 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -14,6 +14,8 @@ import Idris.Syntax import Data.String +import System + %default covering ||| Compile a TT expression to Javascript @@ -68,7 +70,7 @@ compileExpr c s tmpDir outputDir tm outfile = executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () + (tmpDir : String) -> ClosedTerm -> Core ExitCode executeExpr c s tmpDir tm = throw $ InternalError "Javascript backend is only able to compile, use Node instead" diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index 82c5fadfec..11bd7e7f2f 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -62,11 +62,11 @@ compileExpr c s tmpDir outputDir tm outfile = executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () + (tmpDir : String) -> ClosedTerm -> Core ExitCode executeExpr c s tmpDir tm = do out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js" node <- coreLift findNode - ignore $ system [node, out] + system [node, out] ||| Codegen wrapper for Node implementation. export diff --git a/src/Compiler/Interpreter/VMCode.idr b/src/Compiler/Interpreter/VMCode.idr index 96caf05453..0dde9b26c4 100644 --- a/src/Compiler/Interpreter/VMCode.idr +++ b/src/Compiler/Interpreter/VMCode.idr @@ -17,6 +17,8 @@ import Data.Nat import Data.SnocList import Data.Vect +import System + public export data Object : Type where Closure : (predMissing : Nat) -> (args : SnocList Object) -> Name -> Object @@ -293,11 +295,12 @@ compileExpr _ _ _ _ _ _ = throw (InternalError "compile not implemeted for vmcod executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - String -> ClosedTerm -> Core () + String -> ClosedTerm -> Core ExitCode executeExpr c s _ tm = do cdata <- getCompileData False VMCode tm st <- newRef State !(initInterpState cdata.vmcode) ignore $ callFunc [] (MN "__mainExpression" 0) [] + pure ExitSuccess export codegenVMCodeInterp : Codegen diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 48d93b77c2..9e7efcbe3f 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -1005,9 +1005,8 @@ compileExpr c s _ outputDir tm outfile = export executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (execDir : String) -> ClosedTerm -> Core () -executeExpr c s tmpDir tm = do - do ignore . system =<< compileExpr c s tmpDir tmpDir tm "_tmp_refc" + (execDir : String) -> ClosedTerm -> Core ExitCode +executeExpr c s tmpDir tm = system !(compileExpr c s tmpDir tmpDir tm "_tmp_refc") export codegenRefC : Codegen diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 697f056b70..5d94741594 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -647,9 +647,8 @@ compileExpr makeitso c s tmpDir outputDir tm outfile executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () -executeExpr c s tmpDir tm - = ignore . system =<< compileExpr False c s tmpDir tmpDir tm "_tmpchez" + (tmpDir : String) -> ClosedTerm -> Core ExitCode +executeExpr c s tmpDir tm = system !(compileExpr False c s tmpDir tmpDir tm "_tmpchez") incCompile : Ref Ctxt Defs -> diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index 0e5d1237c6..2b51368e24 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -309,9 +309,8 @@ compileExpr makeitso c s tmpDir outputDir tm outfile = do executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () -executeExpr c s tmpDir tm - = ignore . system =<< compileExpr False c s tmpDir tmpDir tm "_tmpchez" + (tmpDir : String) -> ClosedTerm -> Core ExitCode +executeExpr c s tmpDir tm = system !(compileExpr False c s tmpDir tmpDir tm "_tmpchez") ||| Codegen wrapper for Chez scheme implementation. export diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 0687aec593..9d5afbc878 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -406,9 +406,8 @@ compileExpr c s tmpDir outputDir tm outfile executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () -executeExpr c s tmpDir tm - = ignore . system =<< compileExpr c s tmpDir tmpDir tm "_tmpgambit" -- TODO: on windows, should add exe extension + (tmpDir : String) -> ClosedTerm -> Core ExitCode +executeExpr c s tmpDir tm = system !(compileExpr c s tmpDir tmpDir tm "_tmpgambit") -- TODO: on windows, should add exe extension export codegenGambit : Codegen diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 2ae21e4998..63a7392075 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -462,9 +462,8 @@ compileExpr mkexec c s tmpDir outputDir tm outfile executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (tmpDir : String) -> ClosedTerm -> Core () -executeExpr c s tmpDir tm - = ignore . system =<< compileExpr False c s tmpDir tmpDir tm "_tmpracket" + (tmpDir : String) -> ClosedTerm -> Core ExitCode +executeExpr c s tmpDir tm = system !(compileExpr False c s tmpDir tmpDir tm "_tmpracket") export codegenRacket : Codegen diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index a5a11a8fd6..d3dbfa7d14 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -97,13 +97,6 @@ updateREPLOpts = do ed <- coreLift $ idrisGetEnv "EDITOR" whenJust ed $ \ e => update ROpts { editor := e } -showInfo : {auto c : Ref Ctxt Defs} - -> {auto o : Ref ROpts REPLOpts} - -> List CLOpt - -> Core Bool -showInfo Nil = pure False -showInfo (_::rest) = showInfo rest - tryYaffle : List CLOpt -> Core Bool tryYaffle [] = pure False tryYaffle (Yaffle f :: _) = do yaffleMain f [] @@ -138,12 +131,12 @@ checkVerbose [] = False checkVerbose (Verbose :: _) = True checkVerbose (_ :: xs) = checkVerbose xs -stMain : List (String, Codegen) -> List CLOpt -> Core () +stMain : List (String, Codegen) -> List CLOpt -> Core ExitCode stMain cgs opts = do False <- tryYaffle opts - | True => pure () + | True => pure ExitSuccess False <- tryTTM opts - | True => pure () + | True => pure ExitSuccess defs <- initDefs let updated = foldl (\o, (s, _) => addCG (s, Other s) o) (options defs) cgs c <- newRef Ctxt ({ options := updated } defs) @@ -173,73 +166,77 @@ stMain cgs opts """ update ROpts { mainfile := fname } - finish <- showInfo opts - when (not finish) $ do - -- start by going over the pre-options, and stop if we do not need to - -- continue - True <- preOptions opts - | False => pure () + -- start by going over the pre-options, and stop if we do not need to + -- continue + True <- preOptions opts + | False => pure ExitSuccess - -- If there's a --build or --install, just do that then quit - done <- processPackageOpts opts + -- If there's a --build or --install, just do that then quit + False <- processPackageOpts opts + | True => pure ExitSuccess - when (not done) $ flip catch quitWithError $ - do when (checkVerbose opts) $ -- override Quiet if implicitly set - setOutput (REPL InfoLvl) - u <- newRef UST initUState - origin <- maybe - (pure $ Virtual Interactive) (\fname => do - modIdent <- ctxtPathToNS fname - pure (PhysicalIdrSrc modIdent) - ) fname - m <- newRef MD (initMetadata origin) - updateREPLOpts - session <- getSession - when (not $ nobanner session) $ do - iputStrLn $ pretty0 banner - when (isCons cgs) $ iputStrLn (reflow "With codegen for:" <++> hsep (pretty0 . fst <$> cgs)) - fname <- if findipkg session - then findIpkg fname - else pure fname - setMainFile fname - result <- case fname of - Nothing => logTime 1 "Loading prelude" $ do - when (not $ noprelude session) $ - readPrelude True - pure Done - Just f => logTime 1 "Loading main file" $ do - res <- loadMainFile f - displayStartupErrors res - pure res + flip catch quitWithError $ + do when (checkVerbose opts) $ -- override Quiet if implicitly set + setOutput (REPL InfoLvl) + u <- newRef UST initUState + origin <- maybe + (pure $ Virtual Interactive) (\fname => do + modIdent <- ctxtPathToNS fname + pure (PhysicalIdrSrc modIdent) + ) fname + m <- newRef MD (initMetadata origin) + updateREPLOpts + session <- getSession + when (not $ nobanner session) $ do + iputStrLn $ pretty0 banner + when (isCons cgs) $ iputStrLn (reflow "With codegen for:" <++> hsep (pretty0 . fst <$> cgs)) + fname <- if findipkg session + then findIpkg fname + else pure fname + setMainFile fname + result <- case fname of + Nothing => logTime 1 "Loading prelude" $ do + when (not $ noprelude session) $ + readPrelude True + pure Done + Just f => logTime 1 "Loading main file" $ do + res <- loadMainFile f + displayStartupErrors res + pure res - doRepl <- catch (postOptions result opts) - (\err => emitError err *> pure False) - if doRepl then - if ide || ideSocket then - if not ideSocket - then do - setOutput (IDEMode 0 stdin stdout) - replIDE {c} {u} {m} - else do - let (host, port) = ideSocketModeAddress opts - f <- coreLift $ initIDESocketFile host port - case f of - Left err => do - coreLift $ putStrLn err - coreLift $ exitWith (ExitFailure 1) - Right file => do - setOutput (IDEMode 0 file file) - replIDE {c} {u} {m} + (doRepl, status) <- catch (postOptions result opts) + (\err => emitError err $> (False, Nothing)) + if doRepl + then + if ide + then do + setOutput (IDEMode 0 stdin stdout) + replIDE {c} {u} {m} + pure ExitSuccess + else if ideSocket + then do + let (host, port) = ideSocketModeAddress opts + f <- coreLift $ initIDESocketFile host port + case f of + Left err => do + coreLift $ putStrLn err + pure $ ExitFailure 1 + Right file => do + setOutput (IDEMode 0 file file) + replIDE {c} {u} {m} + pure ExitSuccess else do - repl {c} {u} {m} - showTimeRecord - else - -- exit with an error code if there was an error, otherwise - -- just exit - do ropts <- get ROpts - showTimeRecord - whenJust (errorLine ropts) $ \ _ => - coreLift $ exitWith (ExitFailure 1) + repl {c} {u} {m} + showTimeRecord + pure ExitSuccess + else + -- exit with an error code if there was an error, otherwise + -- exit with the status if present or success + do ropts <- get ROpts + showTimeRecord + pure $ case errorLine ropts of + Nothing => fromMaybe ExitSuccess status + Just _ => ExitFailure 1 where @@ -286,4 +283,4 @@ mainWithCodegens cgs = do coreRun (stMain cgs opts) (\err : Error => do putStrLn ("Uncaught error: " ++ show err) exitWith (ExitFailure 1)) - (\res => pure ()) + exitWith diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 06d3496a6e..f03ca31b3d 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -448,7 +448,7 @@ displayIDEResult outf i (NameLocList dat) -- do not use a catchall so that we are warned about missing cases when adding a -- new construtor to the enumeration. displayIDEResult outf i (REPL Done) = printIDEResult outf i (AString "") -displayIDEResult outf i (REPL (Executed _)) = printIDEResult outf i (AString "") +displayIDEResult outf i (REPL (Executed _ _)) = printIDEResult outf i (AString "") displayIDEResult outf i (REPL (ModuleLoaded _)) = printIDEResult outf i (AString "") displayIDEResult outf i (REPL (ErrorLoadingModule _ _)) = printIDEResult outf i (AString "") displayIDEResult outf i (REPL (ColorSet _)) = printIDEResult outf i (AString "") diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 21a2ab0836..53c41cc729 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -778,9 +778,9 @@ execExp ctm do iputStrLn (reflow "No such code generator available") pure CompilationFailed tm_erased <- prepareExp ctm - logTimeWhen !getEvalTiming 0 "Execution" $ + status <- logTimeWhen !getEvalTiming 0 "Execution" $ execute cg tm_erased - pure $ Executed ctm + pure $ Executed ctm status execDecls : {auto c : Ref Ctxt Defs} -> @@ -885,7 +885,7 @@ process (Eval itm) = do opts <- get ROpts let emode = evalMode opts case emode of - Execute => do ignore (execExp itm); pure (Executed itm) + Execute => execExp itm Scheme => do (tm `WithType` ty) <- inferAndElab InExpr itm [] qtm <- logTimeWhen !getEvalTiming 0 "Evaluation" $ @@ -1284,7 +1284,7 @@ mutual -- do not use a catchall so that we are warned when a new constructor is added displayResult Done = pure () - displayResult (Executed _) = pure () + displayResult (Executed _ _) = pure () displayResult DefDeclared = pure () displayResult Exited = pure () diff --git a/src/Idris/REPL/Common.idr b/src/Idris/REPL/Common.idr index c6dd9bd4bc..4d58b20ed8 100644 --- a/src/Idris/REPL/Common.idr +++ b/src/Idris/REPL/Common.idr @@ -25,6 +25,7 @@ import Libraries.Data.ANameMap import Libraries.Data.String.Extra import Data.String +import System import System.File %default covering @@ -212,7 +213,7 @@ public export data REPLResult : Type where Done : REPLResult REPLError : Doc IdrisAnn -> REPLResult - Executed : PTerm -> REPLResult + Executed : PTerm -> ExitCode -> REPLResult RequestedHelp : REPLResult RequestedDetails : String -> REPLResult Evaluated : IPTerm -> Maybe IPTerm -> REPLResult diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index ef088105bc..4bf4bbaae0 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -504,28 +504,29 @@ postOptions : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - REPLResult -> List CLOpt -> Core Bool -postOptions _ [] = pure True + REPLResult -> List CLOpt -> Core (Bool, Maybe ExitCode) +postOptions _ [] = pure (True, Nothing) postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest) - = do ignore $ postOptions res rest - pure False + = do (_, status) <- postOptions res rest + pure (False, status) postOptions res (OutputFile outfile :: rest) = do ignore $ compileExp (PRef EmptyFC (UN $ Basic "main")) outfile - ignore $ postOptions res rest - pure False + (_, status) <- postOptions res rest + pure (False, status) postOptions res (ExecFn expr :: rest) = do setCurrentElabSource expr let Right (_, _, e) = runParser (Virtual Interactive) Nothing expr $ aPTerm <* eoi | Left err => throw err - ignore $ execExp e - ignore $ postOptions res rest - pure False + Executed _ code <- execExp e + | _ => throw $ InternalError "Failed to execute the expression" + (_, status) <- postOptions res rest + pure (False, status <|> Just code) postOptions res (CheckOnly :: rest) - = do ignore $ postOptions res rest - pure False + = do (_, status) <- postOptions res rest + pure (False, status) postOptions res (RunREPL str :: rest) = do replCmd str - pure False + pure (False, Nothing) postOptions res (_ :: rest) = postOptions res rest export diff --git a/tests/cli/exitCode001/Main.idr b/tests/cli/exitCode001/Main.idr new file mode 100644 index 0000000000..c796208329 --- /dev/null +++ b/tests/cli/exitCode001/Main.idr @@ -0,0 +1,11 @@ +module Main + +import System + +success : IO () +success = putStrLn "Success" + +fail : IO () +fail = do + putStrLn "Fail" + exitWith (ExitFailure 42) diff --git a/tests/cli/exitCode001/expected b/tests/cli/exitCode001/expected new file mode 100644 index 0000000000..5e1d667153 --- /dev/null +++ b/tests/cli/exitCode001/expected @@ -0,0 +1,13 @@ +Success +0 +------ +Fail +42 +------ +Success +Fail +42 +------ +Fail +Success +0 diff --git a/tests/cli/exitCode001/run b/tests/cli/exitCode001/run new file mode 100755 index 0000000000..ea9e1a8449 --- /dev/null +++ b/tests/cli/exitCode001/run @@ -0,0 +1,9 @@ +. ../../testutils.sh + +idris2 Main.idr --exec success; echo $? +echo "------" +idris2 Main.idr --exec fail; echo $? +echo "------" +idris2 Main.idr --exec success --exec fail; echo $? +echo "------" +idris2 Main.idr --exec fail --exec success; echo $? From 7a96358ab16345cde60bb230879c8b6a174900e6 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 15:21:41 +0300 Subject: [PATCH 05/16] [ fix ] Add cast from `Int` to `ExitCode` to Libraries --- src/Core/Core.idr | 5 +++-- src/Libraries/System.idr | 11 +++++++++++ 2 files changed, 14 insertions(+), 2 deletions(-) create mode 100644 src/Libraries/System.idr diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 35adbae0c3..4e24260b73 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -12,6 +12,7 @@ import Libraries.Text.PrettyPrint.Prettyprinter import Libraries.Text.PrettyPrint.Prettyprinter.Util import Libraries.Text.PrettyPrint.Prettyprinter.Doc import Libraries.Data.Tap +import Libraries.System import public Data.IORef import System @@ -989,7 +990,7 @@ handleExitCode cmd (ExitFailure status) = throw $ NonZeroExitCode cmd status export system : String -> Core ExitCode -system = map cast . coreLift . system +system = map (cast @{ToExitCode}) . coreLift . system ||| Execute a shell command. Throws `NonZeroExitCode` if the command returns ||| non-zero exit code. @@ -1000,7 +1001,7 @@ safeSystem cmd = system cmd >>= handleExitCode cmd namespace Escaped export system : List String -> Core ExitCode - system = map cast . coreLift . system + system = map (cast @{ToExitCode}) . coreLift . system export safeSystem : List String -> Core () diff --git a/src/Libraries/System.idr b/src/Libraries/System.idr new file mode 100644 index 0000000000..549b23b590 --- /dev/null +++ b/src/Libraries/System.idr @@ -0,0 +1,11 @@ +module Libraries.System + +import System + +-- TODO: Remove this, once `Cast` from `base` is available to the compiler + +export +[ToExitCode] Cast Int ExitCode where + cast code with (code == 0) proof prf + _ | True = ExitSuccess + _ | False = ExitFailure code @{rewrite prf in Oh} From 52d8bc0f029faefef2aab7e4b7dcf5bb549b6d5e Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 16:09:50 +0300 Subject: [PATCH 06/16] [ refactor ] Add docs to `Core.currentDir` --- src/Core/Core.idr | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 4e24260b73..663120d413 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -952,6 +952,8 @@ condC [] def = def condC ((x, y) :: xs) def = if !x then y else condC xs def +||| Get the absolute path of the current working directory. +||| Throws `SystemError` if an error occurred. export currentDir : Core String currentDir = maybe (throw $ SystemError "Failed to get the current directory") pure !(coreLift currentDir) From 6e9d90e66d848a8a662aa3d267fb6e21266663a0 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 16:29:44 +0300 Subject: [PATCH 07/16] [ test ] Add test for exit code in REPL --- tests/idris2/repl/repl008/expected | 3 +++ tests/idris2/repl/repl008/input | 1 + tests/idris2/repl/repl008/run | 3 +++ 3 files changed, 7 insertions(+) create mode 100644 tests/idris2/repl/repl008/expected create mode 100644 tests/idris2/repl/repl008/input create mode 100755 tests/idris2/repl/repl008/run diff --git a/tests/idris2/repl/repl008/expected b/tests/idris2/repl/repl008/expected new file mode 100644 index 0000000000..2dda5fb16d --- /dev/null +++ b/tests/idris2/repl/repl008/expected @@ -0,0 +1,3 @@ +Main> Error: Command 'false' exited with return code 1 +Main> +Bye for now! diff --git a/tests/idris2/repl/repl008/input b/tests/idris2/repl/repl008/input new file mode 100644 index 0000000000..0a34cb5058 --- /dev/null +++ b/tests/idris2/repl/repl008/input @@ -0,0 +1 @@ +:sh "false" diff --git a/tests/idris2/repl/repl008/run b/tests/idris2/repl/repl008/run new file mode 100755 index 0000000000..404d7d47c6 --- /dev/null +++ b/tests/idris2/repl/repl008/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +idris2 < input From 6e4049c11ce1d0f05dbf73f6a52d7f481912c53c Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 22:23:33 +0300 Subject: [PATCH 08/16] [ fix ] Fix tests and `node` execution --- CHANGELOG_NEXT.md | 7 +++++++ docs/source/backends/custom.rst | 13 ++++++++----- idris2api.ipkg | 1 + src/Compiler/ES/Node.idr | 2 +- src/Core/Core.idr | 2 +- tests/chez/chez037/expected | 2 +- tests/idris2/api/api001/LazyCodegen.idr | 11 +++++++---- tests/idris2/api/api001/expected | 1 + 8 files changed, 27 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index d50bfc635d..7edb47cb30 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -186,6 +186,13 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO That file already had a NodeJS shebang at the top, so now it is fully ready to go after compilation. +### API changes + +* Removed `Maybe` from the return types `compileExpr` and `incCompileFile`. Use + `throw` for compilation errors. + +* `executeExpr` now returns `ExitCode`. + ### Library changes #### Prelude diff --git a/docs/source/backends/custom.rst b/docs/source/backends/custom.rst index 554def8e75..9d58fed76a 100644 --- a/docs/source/backends/custom.rst +++ b/docs/source/backends/custom.rst @@ -28,19 +28,22 @@ Now create a file containing import Compiler.Common import Idris.Driver import Idris.Syntax + import System compile : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (execDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) - compile syn defs tmp dir term file + ClosedTerm -> (outfile : String) -> Core String + compile defs syn tmp dir term file = do coreLift $ putStrLn "I'd rather not." - pure Nothing + throw $ InternalError "Compile is not implemented" execute : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (execDir : String) -> ClosedTerm -> Core () - execute defs syn dir term = do coreLift $ putStrLn "Maybe in an hour." + (execDir : String) -> ClosedTerm -> Core ExitCode + execute defs syn dir term + = do coreLift $ putStrLn "Maybe in an hour." + pure ExitSuccess lazyCodegen : Codegen lazyCodegen = MkCG compile execute Nothing Nothing diff --git a/idris2api.ipkg b/idris2api.ipkg index ebb5e7c677..0e891aa982 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -207,6 +207,7 @@ modules = Libraries.Data.Version, Libraries.Data.WithDefault, + Libraries.System, Libraries.System.Directory.Tree, Libraries.Text.Bounded, diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index 11bd7e7f2f..e03d14f9a6 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -66,7 +66,7 @@ executeExpr : executeExpr c s tmpDir tm = do out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js" node <- coreLift findNode - system [node, out] + system $ "\"" ++ node ++ "\" " ++ out -- Windows often have a space in the path. ||| Codegen wrapper for Node implementation. export diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 663120d413..b8a98046ff 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -1007,7 +1007,7 @@ namespace Escaped export safeSystem : List String -> Core () - safeSystem cmd = system cmd >>= handleExitCode (escapeCmd cmd) + safeSystem cmd = system cmd >>= handleExitCode (fromMaybe "" $ head' cmd) namespace Functor diff --git a/tests/chez/chez037/expected b/tests/chez/chez037/expected index 7ad0e81ce9..8cf2a91728 100644 --- a/tests/chez/chez037/expected +++ b/tests/chez/chez037/expected @@ -1 +1 @@ -Error: Command '"false" "--script" "build/exec/hello_app/compileChez"' exited with return code 1 +Error: Command 'false' exited with return code 1 diff --git a/tests/idris2/api/api001/LazyCodegen.idr b/tests/idris2/api/api001/LazyCodegen.idr index bb60d29d18..e9dcc8068c 100644 --- a/tests/idris2/api/api001/LazyCodegen.idr +++ b/tests/idris2/api/api001/LazyCodegen.idr @@ -6,21 +6,24 @@ import Core.Context import Compiler.Common import Idris.Driver import Idris.Syntax +import System compile : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> (execDir : String) -> - ClosedTerm -> (outfile : String) -> Core (Maybe String) + ClosedTerm -> (outfile : String) -> Core String compile defs syn tmp dir term file = do coreLift $ putStrLn "I'd rather not." - pure Nothing + throw $ InternalError "Compile is not implemented" execute : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> - (execDir : String) -> ClosedTerm -> Core () -execute defs syn dir term = do coreLift $ putStrLn "Maybe in an hour." + (execDir : String) -> ClosedTerm -> Core ExitCode +execute defs syn dir term + = do coreLift $ putStrLn "Maybe in an hour." + pure ExitSuccess lazyCodegen : Codegen lazyCodegen = MkCG compile execute Nothing Nothing diff --git a/tests/idris2/api/api001/expected b/tests/idris2/api/api001/expected index 674c0a3dc1..bf6339dfdf 100644 --- a/tests/idris2/api/api001/expected +++ b/tests/idris2/api/api001/expected @@ -1 +1,2 @@ I'd rather not. +Error: INTERNAL ERROR: Compile is not implemented From 18eb8e6910adfde523630ec1b420ce795c610dbb Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 3 Dec 2024 23:35:11 +0300 Subject: [PATCH 09/16] [ fix ] Fix racket compiler --- src/Compiler/Scheme/Racket.idr | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 63a7392075..702e4768ef 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -455,7 +455,9 @@ compileExpr mkexec c s tmpDir outputDir tm outfile -- TODO: add launcher script let outShRel = outputDir outfile - makeShPlatform isWindows (if mkexec then "" else racket ++ " ") outShRel appDirRel outRktFile + if mkexec + then makeShPlatform isWindows "" outShRel appDirRel outBinFile + else makeShPlatform isWindows (racket ++ " ") outShRel appDirRel outRktFile handleFileError outShRel $ chmodRaw outShRel 0o755 pure outShRel From 3fc9066aff9ad9eb378cbdf0ba4e2b6a00c46d42 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Wed, 4 Dec 2024 00:15:26 +0300 Subject: [PATCH 10/16] [ refactor ] Rename `changeDir` and `unsafeChangeDir` to `safeChangeDir` and `changeDir` --- src/Core/Context.idr | 4 ++-- src/Core/Core.idr | 15 +++++++-------- src/Idris/Package.idr | 2 +- 3 files changed, 10 insertions(+), 11 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index b75f2d39ea..8ef4a8533d 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -2185,7 +2185,7 @@ setSourceDir mdir = update Ctxt { options->dirs->source_dir := mdir } export setWorkingDir : {auto c : Ref Ctxt Defs} -> String -> Core () setWorkingDir dir - = do unsafeChangeDir dir + = do ignore $ changeDir dir cdir <- currentDir update Ctxt { options->dirs->working_dir := cdir } @@ -2207,7 +2207,7 @@ withCtxt = wrapRef Ctxt resetCtxt where resetCtxt : Defs -> Core () resetCtxt defs = do let dir = defs.options.dirs.working_dir - changeDir dir + safeChangeDir dir export setPrefix : {auto c : Ref Ctxt Defs} -> String -> Core () diff --git a/src/Core/Core.idr b/src/Core/Core.idr index b8a98046ff..c4d3443aa9 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -958,19 +958,18 @@ export currentDir : Core String currentDir = maybe (throw $ SystemError "Failed to get the current directory") pure !(coreLift currentDir) +export +changeDir : String -> Core Bool +changeDir = coreLift . changeDir + ||| Change the current working directory to the specified path. ||| Throws `SystemError` if the operation did not succeed. export -changeDir : String -> Core () -changeDir dir = - unless !(coreLift $ changeDir dir) $ +safeChangeDir : String -> Core () +safeChangeDir dir = + unless !(changeDir dir) $ throw $ SystemError "Failed to change directory to '\{dir}'" -||| Change the current working directory to the specified path. Ignores errors. -export -unsafeChangeDir : String -> Core () -unsafeChangeDir = ignore . coreLift . changeDir - export handleFileError : (fname : String) -> IO (Either FileError a) -> Core a handleFileError fname res = either (throw . FileErr fname) pure !(coreLift res) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index c06f8007c7..f4362baa64 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -1055,7 +1055,7 @@ findIpkg : {auto c : Ref Ctxt Defs} -> findIpkg fname = do Just (dir, ipkgn, up) <- coreLift findIpkgFile | Nothing => pure fname - changeDir dir + safeChangeDir dir setWorkingDir dir pkg <- parsePkgFile True ipkgn maybe (pure ()) setBuildDir (builddir pkg) From 359c9874b323ec298446cd1a58b43bc507fb6fe8 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Wed, 4 Dec 2024 00:05:54 +0300 Subject: [PATCH 11/16] [ refactor ] Add `CodegenNotFound` error --- src/Core/Context.idr | 2 ++ src/Core/Core.idr | 40 ++++++++++++++++++++++++++++++++++++++ src/Core/Options.idr | 36 ---------------------------------- src/Idris/CommandLine.idr | 1 + src/Idris/Error.idr | 1 + src/Idris/IDEMode/REPL.idr | 2 -- src/Idris/ProcessIdr.idr | 7 +++++-- src/Idris/REPL.idr | 29 ++++++++++++++------------- src/Idris/REPL/Common.idr | 1 - src/Idris/SetOptions.idr | 3 +-- 10 files changed, 65 insertions(+), 57 deletions(-) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 8ef4a8533d..11b029c2a9 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -810,6 +810,7 @@ HasNames Error where full gam (ModuleNotFound fc x) = pure (ModuleNotFound fc x) full gam (CyclicImports xs) = pure (CyclicImports xs) full gam ForceNeeded = pure ForceNeeded + full gam (CodegenNotFound x) = pure (CodegenNotFound x) full gam (InternalError x) = pure (InternalError x) full gam (UserError x) = pure (UserError x) full gam (NoForeignCC fc xs) = pure (NoForeignCC fc xs) @@ -910,6 +911,7 @@ HasNames Error where resolved gam (ModuleNotFound fc x) = pure (ModuleNotFound fc x) resolved gam (CyclicImports xs) = pure (CyclicImports xs) resolved gam ForceNeeded = pure ForceNeeded + resolved gam (CodegenNotFound x) = pure (CodegenNotFound x) resolved gam (InternalError x) = pure (InternalError x) resolved gam (UserError x) = pure (UserError x) resolved gam (NoForeignCC fc xs) = pure (NoForeignCC fc xs) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index c4d3443aa9..681c1cfd56 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -86,6 +86,42 @@ data Warning : Type where %name Warning wrn +public export +data CG = Chez + | ChezSep + | Racket + | Gambit + | Node + | Javascript + | RefC + | VMCodeInterp + | Other String + +export +Eq CG where + Chez == Chez = True + ChezSep == ChezSep = True + Racket == Racket = True + Gambit == Gambit = True + Node == Node = True + Javascript == Javascript = True + RefC == RefC = True + VMCodeInterp == VMCodeInterp = True + Other s == Other t = s == t + _ == _ = False + +export +Show CG where + show Chez = "chez" + show ChezSep = "chez-sep" + show Racket = "racket" + show Gambit = "gambit" + show Node = "node" + show Javascript = "javascript" + show RefC = "refc" + show VMCodeInterp = "vmcode-interp" + show (Other s) = s + -- All possible errors, carrying a location public export data Error : Type where @@ -185,6 +221,7 @@ data Error : Type where ModuleNotFound : FC -> ModuleIdent -> Error CyclicImports : List ModuleIdent -> Error ForceNeeded : Error + CodegenNotFound : CG -> Error InternalError : String -> Error UserError : String -> Error ||| Contains list of specifiers for which foreign call cannot be resolved @@ -378,6 +415,7 @@ Show Error where show (CyclicImports ns) = "Module imports form a cycle: " ++ showSep " -> " (map show ns) show ForceNeeded = "Internal error when resolving implicit laziness" + show (CodegenNotFound cg) = "Codegenerator \{show cg} not found" show (InternalError str) = "INTERNAL ERROR: " ++ str show (UserError str) = "Error: " ++ str show (NoForeignCC fc specs) = show fc ++ @@ -494,6 +532,7 @@ getErrorLoc (ParseFail ((loc, _) ::: _)) = Just loc getErrorLoc (ModuleNotFound loc _) = Just loc getErrorLoc (CyclicImports _) = Nothing getErrorLoc ForceNeeded = Nothing +getErrorLoc (CodegenNotFound _) = Nothing getErrorLoc (InternalError _) = Nothing getErrorLoc (UserError _) = Nothing getErrorLoc (NoForeignCC loc _) = Just loc @@ -586,6 +625,7 @@ killErrorLoc (ParseFail xs) = ParseFail $ map ((emptyFC,) . snd) $ xs killErrorLoc (ModuleNotFound fc x) = ModuleNotFound emptyFC x killErrorLoc (CyclicImports xs) = CyclicImports xs killErrorLoc ForceNeeded = ForceNeeded +killErrorLoc (CodegenNotFound x) = CodegenNotFound x killErrorLoc (InternalError x) = InternalError x killErrorLoc (UserError x) = UserError x killErrorLoc (NoForeignCC fc xs) = NoForeignCC emptyFC xs diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 45470f3fb5..6d382bb37c 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -53,42 +53,6 @@ toString d@(MkDirs wdir sdir bdir ldir odir dfix edirs ppaths pdirs ldirs ddirs) + Data Directories :: \{ show ddirs } """ -public export -data CG = Chez - | ChezSep - | Racket - | Gambit - | Node - | Javascript - | RefC - | VMCodeInterp - | Other String - -export -Eq CG where - Chez == Chez = True - ChezSep == ChezSep = True - Racket == Racket = True - Gambit == Gambit = True - Node == Node = True - Javascript == Javascript = True - RefC == RefC = True - VMCodeInterp == VMCodeInterp = True - Other s == Other t = s == t - _ == _ = False - -export -Show CG where - show Chez = "chez" - show ChezSep = "chez-sep" - show Racket = "racket" - show Gambit = "gambit" - show Node = "node" - show Javascript = "javascript" - show RefC = "refc" - show VMCodeInterp = "vmcode-interp" - show (Other s) = s - public export record PairNames where constructor MkPairNs diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 85f5f8493b..6666ea9db6 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -6,6 +6,7 @@ import Idris.Doc.Display import Idris.Doc.String import Idris.Pretty +import Core.Core import Core.Options import Data.List diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index a75a5c9135..1ab92b36c2 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -750,6 +750,7 @@ perrorRaw (CyclicImports ns) = pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround " -> ") (pretty0 <$> ns) perrorRaw ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness") +perrorRaw (CodegenNotFound cg) = pure $ errorDesc ("Codegenerator" <++> byShow cg <++> "not found") perrorRaw (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty0 str perrorRaw (UserError str) = pure . errorDesc $ pretty0 str perrorRaw (NoForeignCC fc specs) = do diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index f03ca31b3d..91e098ed55 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -351,8 +351,6 @@ displayIDEResult outf i (REPL $ NoFileLoaded) = printIDEError outf i $ reflow "No file can be reloaded" displayIDEResult outf i (REPL $ CurrentDirectory dir) = printIDEResult outf i $ AString $ "Current working directory is \"\{dir}\"" -displayIDEResult outf i (REPL CompilationFailed) - = printIDEError outf i $ reflow "Compilation failed" displayIDEResult outf i (REPL $ Compiled f) = printIDEResult outf i $ AString "File \{f} written" displayIDEResult outf i (REPL $ ProofFound x) diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 4a55029ded..615b094ec2 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -287,10 +287,13 @@ getCG (Other s) = getCodegen s export findCG : {auto o : Ref ROpts REPLOpts} -> - {auto c : Ref Ctxt Defs} -> Core (Maybe Codegen) + {auto c : Ref Ctxt Defs} -> Core Codegen findCG = do defs <- get Ctxt - getCG (codegen (session (options defs))) + let cg = defs.options.session.codegen + Just codegen <- getCG cg + | Nothing => throw $ CodegenNotFound cg + pure codegen ||| Process everything in the module; return the syntax information which ||| needs to be written to the TTC (e.g. exported infix operators) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 53c41cc729..86f5c32f97 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -765,6 +765,19 @@ processLocal : {vars : _} -> processLocal {vars} eopts nest env nestdecls_in scope = localHelper nest env nestdecls_in $ \nest' => traverse_ (processDecl eopts nest' env) scope +export +execExpRaw : {auto c : Ref Ctxt Defs} -> + {auto u : Ref UST UState} -> + {auto s : Ref Syn SyntaxInfo} -> + {auto m : Ref MD Metadata} -> + {auto o : Ref ROpts REPLOpts} -> + PTerm -> Core ExitCode +execExpRaw ctm + = do cg <- findCG + tm_erased <- prepareExp ctm + logTimeWhen !getEvalTiming 0 "Execution" $ + execute cg tm_erased + export execExp : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -772,15 +785,7 @@ execExp : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> PTerm -> Core REPLResult -execExp ctm - = do Just cg <- findCG - | Nothing => - do iputStrLn (reflow "No such code generator available") - pure CompilationFailed - tm_erased <- prepareExp ctm - status <- logTimeWhen !getEvalTiming 0 "Execution" $ - execute cg tm_erased - pure $ Executed ctm status +execExp ctm = Executed ctm <$> execExpRaw ctm execDecls : {auto c : Ref Ctxt Defs} -> @@ -808,10 +813,7 @@ compileExp : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> PTerm -> String -> Core REPLResult compileExp ctm outfile - = do Just cg <- findCG - | Nothing => - do iputStrLn (reflow "No such code generator available") - pure CompilationFailed + = do cg <- findCG tm_erased <- prepareExp ctm Compiled <$> compile cg tm_erased outfile @@ -1258,7 +1260,6 @@ mutual displayResult NoFileLoaded = printResult (reflow "No file can be reloaded") displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> dquotes (pretty0 dir)) - displayResult CompilationFailed = printResult (reflow "Compilation failed") displayResult (Compiled f) = printResult ("File" <++> pretty0 f <++> "written") displayResult (ProofFound x) = printResult (prettyBy Syntax x) displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases) diff --git a/src/Idris/REPL/Common.idr b/src/Idris/REPL/Common.idr index 4d58b20ed8..b91284507c 100644 --- a/src/Idris/REPL/Common.idr +++ b/src/Idris/REPL/Common.idr @@ -227,7 +227,6 @@ data REPLResult : Type where ErrorsBuildingFile : String -> List Error -> REPLResult NoFileLoaded : REPLResult CurrentDirectory : String -> REPLResult - CompilationFailed: REPLResult Compiled : String -> REPLResult ProofFound : IPTerm -> REPLResult Missed : List MissedResult -> REPLResult diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 4bf4bbaae0..f190dcac2a 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -517,8 +517,7 @@ postOptions res (ExecFn expr :: rest) = do setCurrentElabSource expr let Right (_, _, e) = runParser (Virtual Interactive) Nothing expr $ aPTerm <* eoi | Left err => throw err - Executed _ code <- execExp e - | _ => throw $ InternalError "Failed to execute the expression" + code <- execExpRaw e (_, status) <- postOptions res rest pure (False, status <|> Just code) postOptions res (CheckOnly :: rest) From ad5609a226a26b0f217a018b274b9fd0e7334f1b Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Wed, 4 Dec 2024 11:18:14 +0300 Subject: [PATCH 12/16] [ refactor ] Add `UnsupportedOpertaion` Error --- docs/source/backends/custom.rst | 3 +-- src/Compiler/ES/Javascript.idr | 2 +- src/Compiler/Interpreter/VMCode.idr | 2 +- src/Core/Context.idr | 2 ++ src/Core/Core.idr | 20 ++++++++++++++++++++ src/Idris/Error.idr | 4 ++++ tests/idris2/api/api001/LazyCodegen.idr | 3 +-- tests/idris2/api/api001/expected | 3 +-- 8 files changed, 31 insertions(+), 8 deletions(-) diff --git a/docs/source/backends/custom.rst b/docs/source/backends/custom.rst index 9d58fed76a..efa08eeaf7 100644 --- a/docs/source/backends/custom.rst +++ b/docs/source/backends/custom.rst @@ -35,8 +35,7 @@ Now create a file containing (tmpDir : String) -> (execDir : String) -> ClosedTerm -> (outfile : String) -> Core String compile defs syn tmp dir term file - = do coreLift $ putStrLn "I'd rather not." - throw $ InternalError "Compile is not implemented" + = throw $ compileNotSupport (Other "lazy") "I'd rather not." execute : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> diff --git a/src/Compiler/ES/Javascript.idr b/src/Compiler/ES/Javascript.idr index 50c54d4cc4..39bf584cd8 100644 --- a/src/Compiler/ES/Javascript.idr +++ b/src/Compiler/ES/Javascript.idr @@ -72,7 +72,7 @@ executeExpr : Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core ExitCode executeExpr c s tmpDir tm = - throw $ InternalError "Javascript backend is only able to compile, use Node instead" + throw $ executeNotSupport Javascript "Javascript backend is only able to compile, use Node instead" ||| Codegen wrapper for Javascript implementation. export diff --git a/src/Compiler/Interpreter/VMCode.idr b/src/Compiler/Interpreter/VMCode.idr index 0dde9b26c4..83bc19f23a 100644 --- a/src/Compiler/Interpreter/VMCode.idr +++ b/src/Compiler/Interpreter/VMCode.idr @@ -290,7 +290,7 @@ compileExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> String -> String -> ClosedTerm -> String -> Core String -compileExpr _ _ _ _ _ _ = throw (InternalError "compile not implemeted for vmcode-interp") +compileExpr _ _ _ _ _ _ = throw $ compileNotSupport VMCodeInterp "Compile not implemeted for vmcode-interp" executeExpr : Ref Ctxt Defs -> diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 11b029c2a9..9c5c629d8d 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -811,6 +811,7 @@ HasNames Error where full gam (CyclicImports xs) = pure (CyclicImports xs) full gam ForceNeeded = pure ForceNeeded full gam (CodegenNotFound x) = pure (CodegenNotFound x) + full gam (UnsupportedOpertaion x y z) = pure (UnsupportedOpertaion x y z) full gam (InternalError x) = pure (InternalError x) full gam (UserError x) = pure (UserError x) full gam (NoForeignCC fc xs) = pure (NoForeignCC fc xs) @@ -912,6 +913,7 @@ HasNames Error where resolved gam (CyclicImports xs) = pure (CyclicImports xs) resolved gam ForceNeeded = pure ForceNeeded resolved gam (CodegenNotFound x) = pure (CodegenNotFound x) + resolved gam (UnsupportedOpertaion x y z) = pure (UnsupportedOpertaion x y z) resolved gam (InternalError x) = pure (InternalError x) resolved gam (UserError x) = pure (UserError x) resolved gam (NoForeignCC fc xs) = pure (NoForeignCC fc xs) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 681c1cfd56..89445e06e8 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -122,6 +122,14 @@ Show CG where show VMCodeInterp = "vmcode-interp" show (Other s) = s +public export +data CGOperation = Compile | Execute + +export +Show CGOperation where + show Compile = "compile" + show Execute = "execute" + -- All possible errors, carrying a location public export data Error : Type where @@ -222,6 +230,7 @@ data Error : Type where CyclicImports : List ModuleIdent -> Error ForceNeeded : Error CodegenNotFound : CG -> Error + UnsupportedOpertaion : CGOperation -> CG -> String -> Error InternalError : String -> Error UserError : String -> Error ||| Contains list of specifiers for which foreign call cannot be resolved @@ -241,6 +250,14 @@ data Error : Type where %name Error err +export +compileNotSupport : CG -> String -> Error +compileNotSupport = UnsupportedOpertaion Compile + +export +executeNotSupport : CG -> String -> Error +executeNotSupport = UnsupportedOpertaion Execute + export Show TTCErrorMsg where show (Format file ver exp) = @@ -416,6 +433,7 @@ Show Error where = "Module imports form a cycle: " ++ showSep " -> " (map show ns) show ForceNeeded = "Internal error when resolving implicit laziness" show (CodegenNotFound cg) = "Codegenerator \{show cg} not found" + show (UnsupportedOpertaion op cg msg) = "Codegenerator \{show cg} doesn't support '\{show op}: \{msg}" show (InternalError str) = "INTERNAL ERROR: " ++ str show (UserError str) = "Error: " ++ str show (NoForeignCC fc specs) = show fc ++ @@ -533,6 +551,7 @@ getErrorLoc (ModuleNotFound loc _) = Just loc getErrorLoc (CyclicImports _) = Nothing getErrorLoc ForceNeeded = Nothing getErrorLoc (CodegenNotFound _) = Nothing +getErrorLoc (UnsupportedOpertaion _ _ _) = Nothing getErrorLoc (InternalError _) = Nothing getErrorLoc (UserError _) = Nothing getErrorLoc (NoForeignCC loc _) = Just loc @@ -626,6 +645,7 @@ killErrorLoc (ModuleNotFound fc x) = ModuleNotFound emptyFC x killErrorLoc (CyclicImports xs) = CyclicImports xs killErrorLoc ForceNeeded = ForceNeeded killErrorLoc (CodegenNotFound x) = CodegenNotFound x +killErrorLoc (UnsupportedOpertaion x y z) = UnsupportedOpertaion x y z killErrorLoc (InternalError x) = InternalError x killErrorLoc (UserError x) = UserError x killErrorLoc (NoForeignCC fc xs) = NoForeignCC emptyFC xs diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 1ab92b36c2..6bd2d3d5d7 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -751,6 +751,10 @@ perrorRaw (CyclicImports ns) <++> concatWith (surround " -> ") (pretty0 <$> ns) perrorRaw ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness") perrorRaw (CodegenNotFound cg) = pure $ errorDesc ("Codegenerator" <++> byShow cg <++> "not found") +perrorRaw (UnsupportedOpertaion op cg msg) + = pure $ errorDesc (reflow "Codegenerator" <++> byShow cg <++> reflow "doesn't support" + <++> enclose "'" "'" (byShow op) <+> colon) + <++> pretty0 msg perrorRaw (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty0 str perrorRaw (UserError str) = pure . errorDesc $ pretty0 str perrorRaw (NoForeignCC fc specs) = do diff --git a/tests/idris2/api/api001/LazyCodegen.idr b/tests/idris2/api/api001/LazyCodegen.idr index e9dcc8068c..1c94bb8741 100644 --- a/tests/idris2/api/api001/LazyCodegen.idr +++ b/tests/idris2/api/api001/LazyCodegen.idr @@ -14,8 +14,7 @@ compile : (tmpDir : String) -> (execDir : String) -> ClosedTerm -> (outfile : String) -> Core String compile defs syn tmp dir term file - = do coreLift $ putStrLn "I'd rather not." - throw $ InternalError "Compile is not implemented" + = throw $ compileNotSupport (Other "lazy") "I'd rather not." execute : Ref Ctxt Defs -> diff --git a/tests/idris2/api/api001/expected b/tests/idris2/api/api001/expected index bf6339dfdf..00d6eba8e1 100644 --- a/tests/idris2/api/api001/expected +++ b/tests/idris2/api/api001/expected @@ -1,2 +1 @@ -I'd rather not. -Error: INTERNAL ERROR: Compile is not implemented +Error: Codegenerator lazy doesn't support 'compile': I'd rather not. From 6ac93011b7ac4986f9861288e1af5f5d999111ca Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Wed, 4 Dec 2024 12:25:39 +0300 Subject: [PATCH 13/16] [ fix ] Return `coreLift_` --- src/Core/Core.idr | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 89445e06e8..ade5f7363a 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -720,6 +720,12 @@ export %inline ignore : Core a -> Core () ignore = map (const ()) +-- This would be better if we restrict it to a limited set of IO operations +export +%inline +coreLift_ : IO a -> Core () +coreLift_ op = ignore (coreLift op) + -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b From ccc7adf2ee0518432c59db0862b175a20869141c Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 9 Dec 2024 17:13:43 +0300 Subject: [PATCH 14/16] [ fix ] Add escapeArg in executeExpr --- src/Compiler/ES/Node.idr | 4 +++- src/Compiler/RefC/RefC.idr | 4 +++- src/Compiler/Scheme/Chez.idr | 4 +++- src/Compiler/Scheme/ChezSep.idr | 4 +++- src/Compiler/Scheme/Gambit.idr | 4 +++- src/Compiler/Scheme/Racket.idr | 4 +++- 6 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index e03d14f9a6..8bb0b7141a 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -66,7 +66,9 @@ executeExpr : executeExpr c s tmpDir tm = do out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js" node <- coreLift findNode - system $ "\"" ++ node ++ "\" " ++ out -- Windows often have a space in the path. + system $ "\"" ++ node ++ "\" " ++ escapeArg out -- Windows often have a space in the path. + -- TODO: Replace with the following call after fix idris-lang/Idris2#3436 + -- system $ [node, out] ||| Codegen wrapper for Node implementation. export diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 9e7efcbe3f..9a3369e557 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -1006,7 +1006,9 @@ compileExpr c s _ outputDir tm outfile = export executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (execDir : String) -> ClosedTerm -> Core ExitCode -executeExpr c s tmpDir tm = system !(compileExpr c s tmpDir tmpDir tm "_tmp_refc") +executeExpr c s tmpDir tm = do + out <- compileExpr c s tmpDir tmpDir tm "_tmp_refc" + system $ escapeArg out export codegenRefC : Codegen diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 5d94741594..32070d0c14 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -648,7 +648,9 @@ executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core ExitCode -executeExpr c s tmpDir tm = system !(compileExpr False c s tmpDir tmpDir tm "_tmpchez") +executeExpr c s tmpDir tm = do + out <- compileExpr False c s tmpDir tmpDir tm "_tmpchez" + system $ escapeArg out incCompile : Ref Ctxt Defs -> diff --git a/src/Compiler/Scheme/ChezSep.idr b/src/Compiler/Scheme/ChezSep.idr index 2b51368e24..61b919e961 100644 --- a/src/Compiler/Scheme/ChezSep.idr +++ b/src/Compiler/Scheme/ChezSep.idr @@ -310,7 +310,9 @@ executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core ExitCode -executeExpr c s tmpDir tm = system !(compileExpr False c s tmpDir tmpDir tm "_tmpchez") +executeExpr c s tmpDir tm = do + out <- compileExpr False c s tmpDir tmpDir tm "_tmpchez" + system $ escapeArg out ||| Codegen wrapper for Chez scheme implementation. export diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 9d5afbc878..1f64472afc 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -407,7 +407,9 @@ executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core ExitCode -executeExpr c s tmpDir tm = system !(compileExpr c s tmpDir tmpDir tm "_tmpgambit") -- TODO: on windows, should add exe extension +executeExpr c s tmpDir tm = do + out <- compileExpr c s tmpDir tmpDir tm "_tmpgambit" -- TODO: on windows, should add exe extension + system $ escapeArg out export codegenGambit : Codegen diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 702e4768ef..bdba51fee5 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -465,7 +465,9 @@ executeExpr : Ref Ctxt Defs -> Ref Syn SyntaxInfo -> (tmpDir : String) -> ClosedTerm -> Core ExitCode -executeExpr c s tmpDir tm = system !(compileExpr False c s tmpDir tmpDir tm "_tmpracket") +executeExpr c s tmpDir tm = do + out <- compileExpr False c s tmpDir tmpDir tm "_tmpracket" + system $ escapeArg out export codegenRacket : Codegen From ab1724149e28921442efe7dcd92f21108285ab37 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 9 Dec 2024 16:40:07 +0300 Subject: [PATCH 15/16] [ cleanup ] Small cleanup `Core` code --- src/Compiler/RefC/RefC.idr | 16 ++++----- src/Core/Context.idr | 7 ++-- src/Core/Core.idr | 69 +++++++++++++------------------------- src/Idris/Driver.idr | 6 ++-- src/Idris/Package.idr | 8 ++--- 5 files changed, 38 insertions(+), 68 deletions(-) diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 9a3369e557..04be10007b 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -593,11 +593,9 @@ mutual decreaseIndentation pure "} else ") "" alts - case mDef of - Nothing => pure () - Just body => do - emit emptyFC "} else {" - concaseBody env switchReturnVar "" [] body tailPosition + whenJust mDef $ \body => do + emit emptyFC "} else {" + concaseBody env switchReturnVar "" [] body tailPosition emit emptyFC "}" pure switchReturnVar @@ -626,11 +624,9 @@ mutual pure "} else ") "" alts pure () - case def of - Nothing => pure () - Just body => do - emit emptyFC "} else {" - concaseBody env switchReturnVar "" [] body tailPosition + whenJust def $ \body => do + emit emptyFC "} else {" + concaseBody env switchReturnVar "" [] body tailPosition emit emptyFC "}" pure switchReturnVar diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 9c5c629d8d..f147b6400f 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1385,10 +1385,9 @@ updateDef n fdef = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure () - case fdef (definition gdef) of - Nothing => pure () - Just def' => ignore $ addDef n ({ definition := def', - schemeExpr := Nothing } gdef) + whenJust (fdef $ definition gdef) $ \def' => + ignore $ addDef n $ { definition := def', + schemeExpr := Nothing } gdef export updateTy : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Core.idr b/src/Core/Core.idr index ade5f7363a..48c8a61b4b 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -670,14 +670,12 @@ record Core t where runCore : IO (Either Error t) export -coreRun : Core a -> - (Error -> IO b) -> (a -> IO b) -> IO b -coreRun (MkCore act) err ok - = either err ok !act +coreRun : Core a -> (Error -> IO b) -> (a -> IO b) -> IO b +coreRun (MkCore act) err ok = either err ok !act export coreFail : Error -> Core a -coreFail e = MkCore (pure (Left e)) +coreFail = MkCore . pure . Left export wrapError : (Error -> Error) -> Core a -> Core a @@ -687,8 +685,7 @@ wrapError fe (MkCore prog) = MkCore $ mapFst fe <$> prog export %inline coreLift : IO a -> Core a -coreLift op = MkCore (do op' <- op - pure (Right op')) +coreLift = MkCore . map Right {- Monad, Applicative, Traversable are specialised by hand for Core. In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't @@ -702,11 +699,11 @@ in the next version (i.e., in this project...)! -} -- Functor (specialised) export %inline map : (a -> b) -> Core a -> Core b -map f (MkCore a) = MkCore (map (map f) a) +map f (MkCore a) = MkCore $ map (map f) a export %inline (<$>) : (a -> b) -> Core a -> Core b -(<$>) f (MkCore a) = MkCore (map (map f) a) +(<$>) = map export %inline (<$) : b -> Core a -> Core b @@ -718,7 +715,7 @@ export %inline export %inline ignore : Core a -> Core () -ignore = map (const ()) +ignore = map $ const () -- This would be better if we restrict it to a limited set of IO operations export @@ -729,11 +726,9 @@ coreLift_ op = ignore (coreLift op) -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b -(>>=) (MkCore act) f - = MkCore (act >>= - \case - Left err => pure $ Left err - Right val => runCore $ f val) +MkCore act >>= f = MkCore $ act >>= \case + Left err => pure $ Left err + Right val => runCore $ f val export %inline (>>) : Core () -> Core a -> Core a @@ -757,26 +752,25 @@ export %inline -- Applicative (specialised) export %inline pure : a -> Core a -pure x = MkCore (pure (pure x)) +pure = MkCore . pure . Right export (<*>) : Core (a -> b) -> Core a -> Core b -(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |] +MkCore f <*> MkCore a = MkCore [| f <*> a |] export (*>) : Core a -> Core b -> Core b -(*>) (MkCore a) (MkCore b) = MkCore [| a *> b |] +MkCore a *> MkCore b = MkCore [| a *> b |] export (<*) : Core a -> Core b -> Core a -(<*) (MkCore a) (MkCore b) = MkCore [| a <* b |] +MkCore a <* MkCore b = MkCore [| a <* b |] export %inline when : Bool -> Lazy (Core ()) -> Core () when True f = f when False f = pure () - export %inline unless : Bool -> Lazy (Core ()) -> Core () unless = when . not @@ -811,11 +805,9 @@ interface Catchable m t | m where export Catchable Core Error where - catch (MkCore prog) h - = MkCore ( do p' <- prog - case p' of - Left e => let MkCore he = h e in he - Right val => pure (Right val)) + catch (MkCore prog) h = MkCore $ prog >>= \case + Left e => runCore (h e) + Right val => pure (Right val) breakpoint (MkCore prog) = MkCore (pure <$> prog) throw = coreFail @@ -827,8 +819,7 @@ foldlC fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0) -- Traversable (specialised) traverse' : (a -> Core b) -> List a -> List b -> Core (List b) traverse' f [] acc = pure (reverse acc) -traverse' f (x :: xs) acc - = traverse' f xs (!(f x) :: acc) +traverse' f (x :: xs) acc = traverse' f xs (!(f x) :: acc) %inline export @@ -851,15 +842,12 @@ for = flip traverse export traverseList1 : (a -> Core b) -> List1 a -> Core (List1 b) -traverseList1 f xxs - = let x = head xxs - xs = tail xxs in - [| f x ::: traverse f xs |] +traverseList1 f (x ::: xs) = [| f x ::: traverse f xs |] export traverseSnocList : (a -> Core b) -> SnocList a -> Core (SnocList b) traverseSnocList f [<] = pure [<] -traverseSnocList f (as :< a) = (:<) <$> traverseSnocList f as <*> f a +traverseSnocList f (as :< a) = [| traverseSnocList f as :< f a |] export traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b) @@ -879,9 +867,8 @@ traversePair f (w, a) = (w,) <$> f a export traverse_ : (a -> Core b) -> List a -> Core () traverse_ f [] = pure () -traverse_ f (x :: xs) - = Core.do ignore (f x) - traverse_ f xs +traverse_ f (x :: xs) = ignore (f x) >> traverse_ f xs + %inline export for_ : List a -> (a -> Core ()) -> Core () @@ -890,20 +877,12 @@ for_ = flip traverse_ %inline export sequence : List (Core a) -> Core (List a) -sequence (x :: xs) - = do - x' <- x - xs' <- sequence xs - pure (x' :: xs') +sequence (x :: xs) = [| x :: sequence xs |] sequence [] = pure [] export traverseList1_ : (a -> Core b) -> List1 a -> Core () -traverseList1_ f xxs - = do let x = head xxs - let xs = tail xxs - ignore (f x) - traverse_ f xs +traverseList1_ f (x ::: xs) = ignore (f x) >> traverse_ f xs %inline export traverseFC : (a -> Core b) -> WithFC a -> Core (WithFC b) diff --git a/src/Idris/Driver.idr b/src/Idris/Driver.idr index d3dbfa7d14..e5c33e9910 100644 --- a/src/Idris/Driver.idr +++ b/src/Idris/Driver.idr @@ -99,8 +99,7 @@ updateREPLOpts tryYaffle : List CLOpt -> Core Bool tryYaffle [] = pure False -tryYaffle (Yaffle f :: _) = do yaffleMain f [] - pure True +tryYaffle (Yaffle f :: _) = yaffleMain f [] $> True tryYaffle (c :: cs) = tryYaffle cs ignoreMissingIpkg : List CLOpt -> Bool @@ -110,8 +109,7 @@ ignoreMissingIpkg (c :: cs) = ignoreMissingIpkg cs tryTTM : List CLOpt -> Core Bool tryTTM [] = pure False -tryTTM (Metadata f :: _) = do dumpTTM f - pure True +tryTTM (Metadata f :: _) = dumpTTM f $> True tryTTM (c :: cs) = tryTTM cs diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index f4362baa64..dc2e3b83c4 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -889,11 +889,9 @@ runRepl fname = do pure (PhysicalIdrSrc modIdent) ) fname m <- newRef MD (initMetadata origin) - case fname of - Nothing => pure () - Just fn => do - errs <- loadMainFile fn - displayStartupErrors errs + whenJust fname $ \fn => do + errs <- loadMainFile fn + displayStartupErrors errs repl {u} {s} ||| If the user did not provide a package file we can look in the working From 3f15823a4331ddc0bd188aaf9dad185a14573647 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Thu, 19 Dec 2024 18:28:22 +0300 Subject: [PATCH 16/16] [ cleanup ] Cleaning up the use of applicative syntax --- src/Compiler/Common.idr | 4 +-- src/Compiler/CompileExpr.idr | 6 ++-- src/Compiler/Scheme/Common.idr | 14 ++++------ src/Core/Binary.idr | 6 ++-- src/Core/Case/CaseBuilder.idr | 4 +-- src/Core/Core.idr | 2 +- src/Core/LinearCheck.idr | 2 +- src/Core/Normalise.idr | 2 +- src/Idris/Desugar.idr | 4 +-- src/Idris/ModTree.idr | 2 +- src/Idris/Package.idr | 2 +- src/Idris/Parser.idr | 13 ++++----- src/Idris/REPL.idr | 4 +-- src/Idris/Resugar.idr | 43 ++++++++++++++--------------- src/TTImp/Elab/App.idr | 14 ++++------ src/TTImp/Elab/Lazy.idr | 7 ++--- src/TTImp/Elab/Record.idr | 5 ++-- src/TTImp/Interactive/CaseSplit.idr | 4 +-- src/TTImp/Parser.idr | 9 ++---- 19 files changed, 64 insertions(+), 83 deletions(-) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index a2668fad6b..ccf897dece 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -354,7 +354,7 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in ldefs ++ concat lifted_in anf <- if phase >= ANF - then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted + then logTime 2 "Get ANF" $ traverse (traversePair toANF) lifted else pure [] vmcode <- if phase >= VMCode then logTime 2 "Get VM Code" $ pure (allDefs anf) @@ -440,7 +440,7 @@ getIncCompileData doLazyAnnots phase else pure [] let lifted = concat lifted_in anf <- if phase >= ANF - then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted + then logTime 2 "Get ANF" $ traverse (traversePair toANF) lifted else pure [] vmcode <- if phase >= VMCode then logTime 2 "Get VM Code" $ pure (allDefs anf) diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 249773ace0..5ad7e7ba48 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -354,9 +354,9 @@ toCExpTm n (As _ _ _ p) = toCExpTm n p -- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase toCExpTm n (TDelayed fc _ _) = pure $ CErased fc toCExpTm n (TDelay fc lr _ arg) - = pure (CDelay fc lr !(toCExp n arg)) + = CDelay fc lr <$> toCExp n arg toCExpTm n (TForce fc lr arg) - = pure (CForce fc lr !(toCExp n arg)) + = CForce fc lr <$> toCExp n arg toCExpTm n (PrimVal fc $ PrT c) = pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] -- Primitive type constant toCExpTm n (PrimVal fc c) = pure $ CPrimVal fc c -- Non-type constant toCExpTm n (Erased fc _) = pure $ CErased fc @@ -604,7 +604,7 @@ getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args] = do NPrimVal _ (Str n') <- evalClosure defs n | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct") - pure (Struct n' !(getFieldArgs defs args)) + Struct n' <$> getFieldArgs defs args getNArgs defs n args = pure $ User n args nfToCFType : {auto c : Ref Ctxt Defs} -> diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index b872f0e9ca..2a7956e31c 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -414,7 +414,7 @@ parameters (constants : SortedSet Name, !(showAlts n alts) schCaseTree i sc alts def = do tcode <- schExp (i + 1) sc - defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def + defc <- traverseOpt (schExp i) def let n = getScrutineeTemp i if var sc then pure $ "(case (vector-ref " ++ tcode ++ " 0) " @@ -446,8 +446,7 @@ parameters (constants : SortedSet Name, schListCase i sc alts def = do tcode <- schExp (i + 1) sc let n = getScrutineeTemp i - defc <- maybe (pure Nothing) - (\v => pure (Just !(schExp (i + 1) v))) def + defc <- traverseOpt (schExp (i + 1)) def nil <- getNilCode alts if var sc then do cons <- getConsCode tcode alts @@ -473,7 +472,7 @@ parameters (constants : SortedSet Name, getNilCode : List NamedConAlt -> Core (Maybe Builder) getNilCode [] = pure Nothing getNilCode (MkNConAlt _ NIL _ _ sc :: _) - = pure (Just !(schExp (i + 1) sc)) + = Just <$> schExp (i + 1) sc getNilCode (_ :: xs) = getNilCode xs getConsCode : Builder -> List NamedConAlt -> Core (Maybe Builder) @@ -496,8 +495,7 @@ parameters (constants : SortedSet Name, schMaybeCase i sc alts def = do tcode <- schExp (i + 1) sc let n = getScrutineeTemp i - defc <- maybe (pure Nothing) - (\v => pure (Just !(schExp (i + 1) v))) def + defc <- traverseOpt (schExp (i + 1)) def nothing <- getNothingCode alts if var sc then do just <- getJustCode tcode alts @@ -523,7 +521,7 @@ parameters (constants : SortedSet Name, getNothingCode : List NamedConAlt -> Core (Maybe Builder) getNothingCode [] = pure Nothing getNothingCode (MkNConAlt _ NOTHING _ _ sc :: _) - = pure (Just !(schExp (i + 1) sc)) + = Just <$> schExp (i + 1) sc getNothingCode (_ :: xs) = getNothingCode xs getJustCode : Builder -> List NamedConAlt -> Core (Maybe Builder) @@ -623,7 +621,7 @@ parameters (constants : SortedSet Name, = pure $ !(schConstAlt (i + 1) n alt) ++ " " ++ !(showConstAlts n alts) schExp i (NmConstCase fc sc alts def) - = do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def + = do defc <- traverseOpt (schExp i) def tcode <- schExp (i + 1) sc let n = getScrutineeTemp i if var sc diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index acc126ead8..24ed3bfd3c 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -345,10 +345,8 @@ addGlobalDef modns filens asm (n, def) codedentry <- lookupContextEntry n (gamma defs) -- Don't update the coded entry because some names might not be -- resolved yet - entry <- maybe (pure Nothing) - (\ p => do x <- decode (gamma defs) (fst p) False (snd p) - pure (Just x)) - codedentry + entry <- traverseOpt (\p => decode (gamma defs) (fst p) False (snd p)) + codedentry unless (completeDef entry) $ ignore $ addContextEntry filens n def diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr index 23aefedaa6..dd74b0a6ff 100644 --- a/src/Core/Case/CaseBuilder.idr +++ b/src/Core/Case/CaseBuilder.idr @@ -1080,10 +1080,10 @@ mutual Core (Maybe (CaseTree vars)) mixture fc fn phase (ConClauses cs rest) err = do fallthrough <- mixture fc fn phase rest err - pure (Just !(conRule fc fn phase cs fallthrough)) + Just <$> conRule fc fn phase cs fallthrough mixture fc fn phase (VarClauses vs rest) err = do fallthrough <- mixture fc fn phase rest err - pure (Just !(varRule fc fn phase vs fallthrough)) + Just <$> varRule fc fn phase vs fallthrough mixture fc fn {a} {todo} phase NoClauses err = pure err diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 48c8a61b4b..03bfe4555b 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -894,7 +894,7 @@ namespace PiInfo traverse f Explicit = pure Explicit traverse f Implicit = pure Implicit traverse f AutoImplicit = pure AutoImplicit - traverse f (DefImplicit t) = pure (DefImplicit !(f t)) + traverse f (DefImplicit t) = DefImplicit <$> f t namespace Binder export diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index b250f22387..3ede0d6631 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -472,7 +472,7 @@ mutual Core (List ArgUsage) getArgUsage topfc rig ty pats = do us <- traverse (getPUsage ty) pats - pure (map snd !(combine us)) + map snd <$> combine us where getCaseUsage : {vs : _} -> Term ns -> Env Term vs -> List (Term vs) -> diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 787d22dff8..a0c6fbfb3a 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -154,7 +154,7 @@ etaContract tm = do export getValArity : Defs -> Env Term vars -> NF vars -> Core Nat getValArity defs env (NBind fc x (Pi _ _ _ _) sc) - = pure (S !(getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder))))) + = S <$> getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder))) getValArity defs env val = pure 0 export diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index b1f70903b1..3bd19043bb 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -1155,9 +1155,7 @@ mutual let isb = map (\ (info, r, n, p, tm) => (info, r, n, p, doBind bnames tm)) is' let consb = map (\(n, tm) => (n, doBind bnames tm)) cons' - body' <- maybe (pure Nothing) - (\b => do b' <- traverse (desugarDecl ps) b - pure (Just (concat b'))) body + body' <- traverseOpt (map concat . traverse (desugarDecl ps)) body -- calculate the name of the implementation, if it's not explicitly -- given. let impname = maybe (mkImplName fc tn paramsb) id impln diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index 6e50284eb8..911441b9f6 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -137,7 +137,7 @@ getBuildMods loc done fname dm <- newRef DoneMod empty o <- newRef BuildOrder [] mkBuildMods {d=dm} {o} t - pure (reverse !(get BuildOrder)) + reverse <$> get BuildOrder checkTotalReq : {auto c : Ref Ctxt Defs} -> String -> String -> TotalReq -> Core Bool diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index dc2e3b83c4..e195d9b185 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -196,7 +196,7 @@ field fname depends = do name <- packageName bs <- sepBy andop bound - pure (MkDepends name !(mkBound (concat bs) anyBounds)) + MkDepends name <$> mkBound (concat bs) anyBounds strField : (FC -> String -> DescField) -> String -> Rule DescField strField fieldConstructor fieldName diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index fa962e368d..f1a4ab4520 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -71,9 +71,9 @@ decoratedNamespacedSymbol fname smb = parens : {b : _} -> OriginDesc -> BRule b a -> Rule a parens fname p - = pure id <* decoratedSymbol fname "(" - <*> p - <* decoratedSymbol fname ")" + = id <$ decoratedSymbol fname "(" + <*> p + <* decoratedSymbol fname ")" decoratedDataTypeName : OriginDesc -> Rule Name decoratedDataTypeName fname = decorate fname Typ dataTypeName @@ -1822,10 +1822,9 @@ typedArg fname indents pure $ map (\(c, n, tm) => (n.val, c, Explicit, tm)) params <|> do decoratedSymbol fname "{" commit - info <- - (pure AutoImplicit <* decoratedKeyword fname "auto" - <|> (decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents) - <|> pure Implicit) + info <- AutoImplicit <$ decoratedKeyword fname "auto" + <|> decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents + <|> pure Implicit params <- pibindListName fname indents decoratedSymbol fname "}" pure $ map (\(c, n, tm) => (n.val, c, info, tm)) params diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 86f5c32f97..5eca1d8ef0 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -1130,10 +1130,10 @@ processCatch cmd ) parseEmptyCmd : EmptyRule (Maybe REPLCmd) -parseEmptyCmd = eoi *> (pure Nothing) +parseEmptyCmd = eoi $> Nothing parseCmd : EmptyRule (Maybe REPLCmd) -parseCmd = do c <- command; eoi; pure $ Just c +parseCmd = Just <$> command <* eoi export parseRepl : String -> Either Error (Maybe REPLCmd) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 22ca606a39..7aa3ecae83 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -369,7 +369,7 @@ mutual toPTerm p (IAlternative fc _ _) = pure (PImplicit fc) toPTerm p (IRewrite fc rule tm) = pure (PRewrite fc !(toPTerm startPrec rule) - !(toPTerm startPrec tm)) + !(toPTerm startPrec tm)) toPTerm p (ICoerced fc tm) = toPTerm p tm toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c) toPTerm p (IHole fc str) = pure (PHole fc False str) @@ -378,19 +378,18 @@ mutual = let nm = UN (Basic v) in pure (PRef fc (MkKindedName (Just Bound) nm nm)) toPTerm p (IBindHere fc _ tm) = toPTerm p tm - toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat)) - toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat)) + toPTerm p (IAs fc nameFC _ n pat) = PAs fc nameFC n <$> toPTerm argPrec pat + toPTerm p (IMustUnify fc r pat) = PDotted fc <$> toPTerm argPrec pat - toPTerm p (IDelayed fc r ty) = pure (PDelayed fc r !(toPTerm argPrec ty)) - toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm)) - toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm)) - toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm)) + toPTerm p (IDelayed fc r ty) = PDelayed fc r <$> toPTerm argPrec ty + toPTerm p (IDelay fc tm) = PDelay fc <$> toPTerm argPrec tm + toPTerm p (IForce fc tm) = PForce fc <$> toPTerm argPrec tm + toPTerm p (IQuote fc tm) = PQuote fc <$> toPTerm argPrec tm toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n) toPTerm p (IQuoteDecl fc ds) - = do ds' <- traverse toPDecl ds - pure $ PQuoteDecl fc (catMaybes ds') - toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm)) - toPTerm p (IRunElab fc _ tm) = pure (PRunElab fc !(toPTerm argPrec tm)) + = PQuoteDecl fc . catMaybes <$> traverse toPDecl ds + toPTerm p (IUnquote fc tm) = PUnquote fc <$> toPTerm argPrec tm + toPTerm p (IRunElab fc _ tm) = PRunElab fc <$> toPTerm argPrec tm toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm toPTerm p (Implicit fc True) = pure (PImplicit fc) @@ -468,22 +467,22 @@ mutual flags !(traverse toPClause cs) toPClause (ImpossibleClause fc lhs) - = pure (MkImpossible fc !(toPTerm startPrec lhs)) + = MkImpossible fc <$> toPTerm startPrec lhs toPTypeDecl : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> ImpTy' KindedName -> Core (PTypeDecl' KindedName) toPTypeDecl (MkImpTy fc n ty) - = pure (MkFCVal fc $ MkPTy (pure ("", n)) "" !(toPTerm startPrec ty)) + = MkFCVal fc . MkPTy (pure ("", n)) "" <$> toPTerm startPrec ty toPData : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> ImpData' KindedName -> Core (PDataDecl' KindedName) toPData (MkImpData fc n ty opts cs) = pure (MkPData fc n !(traverseOpt (toPTerm startPrec) ty) opts - !(traverse toPTypeDecl cs)) + !(traverse toPTypeDecl cs)) toPData (MkImpLater fc n ty) - = pure (MkPLater fc n !(toPTerm startPrec ty)) + = MkPLater fc n <$> toPTerm startPrec ty toPField : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -528,11 +527,11 @@ mutual ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName)) toPDecl (IClaim (MkFCVal fc $ MkIClaimData rig vis opts ty)) = do opts' <- traverse toPFnOpt opts - pure (Just (PClaim (MkFCVal fc $ MkPClaim rig vis opts' !(toPTypeDecl ty)))) + Just . PClaim . MkFCVal fc . MkPClaim rig vis opts' <$> toPTypeDecl ty toPDecl (IData fc vis mbtot d) - = pure (Just (PData fc "" vis mbtot !(toPData d))) + = Just . PData fc "" vis mbtot <$> toPData d toPDecl (IDef fc n cs) - = pure (Just (PDef $ MkFCVal fc !(traverse toPClause cs))) + = Just . PDef . MkFCVal fc <$> traverse toPClause cs toPDecl (IParameters fc ps ds) = do ds' <- traverse toPDecl ds pure (Just (PParameters fc @@ -545,17 +544,15 @@ mutual = do (n, ps, opts, con, fs) <- toPRecord r pure (Just (PRecord fc "" vis mbtot (MkPRecord n ps opts con fs))) toPDecl (IFail fc msg ds) - = do ds' <- traverse toPDecl ds - pure (Just (PFail fc msg (catMaybes ds'))) + = Just . PFail fc msg . catMaybes <$> traverse toPDecl ds toPDecl (INamespace fc ns ds) - = do ds' <- traverse toPDecl ds - pure (Just (PNamespace fc ns (catMaybes ds'))) + = Just . PNamespace fc ns . catMaybes <$> traverse toPDecl ds toPDecl (ITransform fc n lhs rhs) = pure (Just (PTransform fc (show n) !(toPTerm startPrec lhs) !(toPTerm startPrec rhs))) toPDecl (IRunElabDecl fc tm) - = pure (Just (PRunElabDecl fc !(toPTerm startPrec tm))) + = Just . PRunElabDecl fc <$> toPTerm startPrec tm toPDecl (IPragma _ _ _) = pure Nothing toPDecl (ILog _) = pure Nothing toPDecl (IBuiltin fc type name) = pure $ Just $ PBuiltin fc type name diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index ede3102048..d44823ea62 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -543,9 +543,8 @@ mutual logNF "elab" 10 ("Full function type") env (NBind fc x (Pi fc argRig Explicit aty) sc) logC "elab" 10 - (do ety <- maybe (pure Nothing) - (\t => pure (Just !(toFullNames!(getTerm t)))) - expty + (do ety <- traverseOpt (\t => toFullNames !(getTerm t)) + expty pure ("Overall expected type: " ++ show ety)) res <- check argRig ({ topLevel := False } elabinfo) nest env arg (Just (glueClosure defs env aty)) @@ -829,11 +828,10 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp logC "elab" 10 (do defs <- get Ctxt fnty <- quote defs env nty - exptyt <- maybe (pure Nothing) - (\t => do ety <- getTerm t - etynf <- normaliseHoles defs env ety - pure (Just !(toFullNames etynf))) - exp + exptyt <- traverseOpt (\t => do ety <- getTerm t + etynf <- normaliseHoles defs env ety + toFullNames etynf) + exp pure ("Checking application of " ++ show !(getFullName n) ++ " (" ++ show n ++ ")" ++ " to " ++ show expargs ++ "\n\tFunction type " ++ diff --git a/src/TTImp/Elab/Lazy.idr b/src/TTImp/Elab/Lazy.idr index c30f6497a1..676b90d15b 100644 --- a/src/TTImp/Elab/Lazy.idr +++ b/src/TTImp/Elab/Lazy.idr @@ -91,11 +91,8 @@ checkForce : {vars : _} -> Core (Term vars, Glued vars) checkForce rig elabinfo nest env fc tm exp = do defs <- get Ctxt - expf <- maybe (pure Nothing) - (\gty => do tynf <- getNF gty - pure (Just (glueBack defs env - (NDelayed fc LUnknown tynf)))) - exp + expf <- traverseOpt (map (glueBack defs env . NDelayed fc LUnknown) . getNF) + exp (tm', gty) <- check rig elabinfo nest env tm expf tynf <- getNF gty case tynf of diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index 7cae467d75..b651b8100e 100644 --- a/src/TTImp/Elab/Record.idr +++ b/src/TTImp/Elab/Record.idr @@ -86,9 +86,8 @@ findFieldsAndTypeArgs : {auto c : Ref Ctxt Defs} -> Defs -> Name -> Core $ Maybe (List (String, Maybe Name, Maybe Name), SortedSet Name) findFieldsAndTypeArgs defs con - = case !(lookupTyExact con (gamma defs)) of - Just t => pure (Just !(getExpNames empty [] !(nf defs [] t))) - _ => pure Nothing + = traverseOpt (\t => getExpNames empty [] !(nf defs [] t)) + !(lookupTyExact con (gamma defs)) where getExpNames : SortedSet Name -> List (String, Maybe Name, Maybe Name) -> diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index e741314556..695ca960e2 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/src/TTImp/Interactive/CaseSplit.idr @@ -250,7 +250,7 @@ getUpdates : Defs -> RawImp -> RawImp -> Core (List (Name, RawImp)) getUpdates defs orig updated = do u <- newRef UPD (MkUpdates [] []) findUpdates defs orig updated - pure (updates !(get UPD)) + updates <$> get UPD mkCase : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> @@ -285,7 +285,7 @@ mkCase {c} {u} fn orig lhs_raw log "interaction.casesplit" 3 $ "Original LHS: " ++ show orig log "interaction.casesplit" 3 $ "New LHS: " ++ show lhs' - pure (Valid lhs' !(getUpdates defs orig lhs'))) + Valid lhs' <$> getUpdates defs orig lhs') (\err => do put Ctxt defs put UST ust diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index deb367ae55..a9ef5b1961 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -611,12 +611,9 @@ recordParam fname indents <|> do symbol "{" commit start <- location - info <- (pure AutoImplicit <* keyword "auto" - <|>(do - keyword "default" - t <- simpleExpr fname indents - pure $ DefImplicit t) - <|> pure Implicit) + info <- AutoImplicit <$ keyword "auto" + <|> keyword "default" *> DefImplicit <$> simpleExpr fname indents + <|> pure Implicit params <- pibindListName fname start indents symbol "}" pure $ map (\(c, n, tm) => (n, c, info, tm)) params