[ refactor ] Improve error handling in Core

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

docs/source/backends/custom.rst

@@ -28,19 +28,21 @@ 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
-      = do coreLift $ putStrLn "I'd rather not."
-           pure Nothing
+      ClosedTerm -> (outfile : String) -> Core String
+    compile defs syn tmp dir term file
+      = throw $ compileNotSupport (Other "lazy") "I'd rather not."
 
     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

idris2api.ipkg

@@ -207,6 +207,7 @@ modules =
     Libraries.Data.Version,
     Libraries.Data.WithDefault,
 
+    Libraries.System,
     Libraries.System.Directory.Tree,
 
     Libraries.Text.Bounded,

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

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
 
@@ -40,10 +41,10 @@ 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 ()
+                (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
@@ -52,7 +53,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 +106,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
@@ -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
@@ -135,7 +136,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
@@ -221,9 +222,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
@@ -355,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)
@@ -441,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)
@@ -533,9 +532,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

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} ->

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
@@ -56,21 +58,21 @@ 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
-     Core.writeFile out res
-     pure (Just out)
+     writeFile out res
+     pure out
 
 ||| Node implementation of the `executeExpr` interface.
 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"
+  throw $ executeNotSupport Javascript "Javascript backend is only able to compile, use Node instead"
 
 ||| Codegen wrapper for Javascript implementation.
 export

src/Compiler/ES/Node.idr

@@ -50,26 +50,25 @@ 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
-     Core.writeFile out es
-     coreLift_ $ chmodRaw out 0o755
-     pure (Just out)
+     writeFile out es
+     handleFileError out $ chmodRaw out 0o755
+     pure out
 
 ||| Node implementation of the `executeExpr` interface.
 executeExpr :
   Ref Ctxt Defs ->
   Ref Syn SyntaxInfo ->
-  (tmpDir : String) -> ClosedTerm -> Core ()
+  (tmpDir : String) -> ClosedTerm -> Core ExitCode
 executeExpr c s tmpDir tm =
-  do let outn = tmpDir </> "_tmp_node.js"
-     js <- compileToNode c s tm
-     Core.writeFile outn js
+  do out <- compileExpr c s tmpDir tmpDir tm "_tmp_node.js"
      node <- coreLift findNode
-     quoted_node <- pure $ "\"" ++ node ++ "\"" -- Windows often have a space in the path.
-     coreLift_ $ system (quoted_node ++ " " ++ outn)
+     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

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
@@ -151,7 +153,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 +165,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))
@@ -287,17 +289,18 @@ parameters {auto c : Ref Ctxt Defs}
 compileExpr :
   Ref Ctxt Defs ->
   Ref Syn SyntaxInfo ->
-  String -> String -> ClosedTerm -> String -> Core (Maybe String)
-compileExpr _ _ _ _ _ _ = throw (InternalError "compile not implemeted for vmcode-interp")
+  String -> String -> ClosedTerm -> String -> Core String
+compileExpr _ _ _ _ _ _ = throw $ compileNotSupport VMCodeInterp "Compile not implemeted for vmcode-interp"
 
 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

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