[ refactor ] Remove Maybe from compileExpr and incCompileFile s…

…ignatures

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

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 :

src/Compiler/ES/Node.idr

@@ -50,22 +50,21 @@ 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 :
   Ref Ctxt Defs ->
   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]
 

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 :

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

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,15 +627,15 @@ 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 :
   Bool ->
   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

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

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

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

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