[ refactor ] Add UnsupportedOpertaion Error

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

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

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

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)

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

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

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

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.