Add errors to the Core pipeline and check GEB prerequisites

app/Commands/Compile.hs

@@ -30,5 +30,8 @@ runCommand opts@CompileOptions {..} = do
 writeCoreFile :: (Members '[Embed IO, App] r) => Compile.PipelineArg -> Sem r ()
 writeCoreFile Compile.PipelineArg {..} = do
   coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  let tab = Core.toEval _pipelineArgInfoTable
-  embed $ TIO.writeFile (toFilePath coreFile) (show $ Core.ppOutDefault (Core.disambiguateNames tab))
+  r <- runError @JuvixError $ Core.toEval _pipelineArgInfoTable
+  case r of
+    Left e -> exitJuvixError e
+    Right tab ->
+      embed $ TIO.writeFile (toFilePath coreFile) (show $ Core.ppOutDefault (Core.disambiguateNames tab))

app/Commands/Dev/Core/Asm.hs

@@ -14,7 +14,8 @@ runCommand opts = do
   inputFile :: Path Abs File <- someBaseToAbs' sinputFile
   s' <- embed (readFile $ toFilePath inputFile)
   tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
-  let tab' = Asm.fromCore $ Stripped.fromCore (Core.toStripped tab)
+  r <- runError @JuvixError $ Core.toStripped tab
+  tab' <- Asm.fromCore . Stripped.fromCore <$> getRight r
   if
       | project opts ^. coreAsmPrint ->
           renderStdOut (Asm.ppOutDefault tab' tab')

app/Commands/Dev/Core/Compile/Base.hs

@@ -73,6 +73,7 @@ runGebPipeline PipelineArg {..} = do
 runAsmPipeline :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r ()
 runAsmPipeline PipelineArg {..} = do
   asmFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  let tab' = coreToAsm _pipelineArgInfoTable
-      code = Pretty.ppPrint tab' tab'
+  r <- runError @JuvixError (coreToAsm _pipelineArgInfoTable)
+  tab' <- getRight r
+  let code = Pretty.ppPrint tab' tab'
   embed $ TIO.writeFile (toFilePath asmFile) code

app/Commands/Dev/Core/FromConcrete.hs

@@ -13,13 +13,12 @@ runCommand :: forall r. Members '[Embed IO, App] r => CoreFromConcreteOptions ->
 runCommand localOpts = do
   tab <- (^. coreResultTable) <$> runPipeline (localOpts ^. coreFromConcreteInputFile) upToCore
   path :: Path Abs File <- someBaseToAbs' (localOpts ^. coreFromConcreteInputFile . pathPath)
-  let tab0 :: InfoTable = Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
-      tab' :: InfoTable = if localOpts ^. coreFromConcreteNoDisambiguate then tab0 else disambiguateNames tab0
-
+  r <- runError @JuvixError $ Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
+  tab0 :: InfoTable <- getRight r
+  let tab' :: InfoTable = if localOpts ^. coreFromConcreteNoDisambiguate then tab0 else disambiguateNames tab0
       inInputModule :: IdentifierInfo -> Bool
-      inInputModule x
-        | localOpts ^. coreFromConcreteFilter = (== Just path) . (^? identifierLocation . _Just . intervalFile) $ x
-        | otherwise = True
+      inInputModule _ | not (localOpts ^. coreFromConcreteFilter) = True
+      inInputModule x = (== Just path) . (^? identifierLocation . _Just . intervalFile) $ x
 
       mainIdens :: [IdentifierInfo] =
         sortOn

app/Commands/Dev/Core/Read.hs

@@ -22,8 +22,9 @@ runCommand opts = do
   inputFile :: Path Abs File <- someBaseToAbs' sinputFile
   s' <- embed . readFile . toFilePath $ inputFile
   tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
-  let tab0 = Core.applyTransformations (project opts ^. coreReadTransformations) tab
-      tab' = if project opts ^. coreReadNoDisambiguate then tab0 else Core.disambiguateNames tab0
+  r <- runError @JuvixError $ Core.applyTransformations (project opts ^. coreReadTransformations) tab
+  tab0 <- getRight $ mapLeft JuvixError r
+  let tab' = if project opts ^. coreReadNoDisambiguate then tab0 else Core.disambiguateNames tab0
   embed (Scoper.scopeTrace tab')
   unless (project opts ^. coreReadNoPrint) $ do
     renderStdOut (Core.ppOut opts tab')

app/Commands/Dev/Core/Strip.hs

@@ -11,8 +11,9 @@ runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Cor
 runCommand opts = do
   inputFile :: Path Abs File <- someBaseToAbs' sinputFile
   s' <- embed (readFile $ toFilePath inputFile)
-  tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
-  let tab' = Stripped.fromCore (Core.toStripped tab)
+  (tab, _) <- getRight (mapLeft JuvixError (Core.runParser inputFile Core.emptyInfoTable s'))
+  r <- runError @JuvixError (Core.toStripped tab)
+  tab' <- getRight $ mapLeft JuvixError $ mapRight Stripped.fromCore r
   unless (project opts ^. coreStripNoPrint) $ do
     renderStdOut (Core.ppOut opts tab')
   where

app/Commands/Eval.hs

@@ -11,8 +11,9 @@ import Juvix.Compiler.Core.Pipeline qualified as Core
 runCommand :: (Members '[Embed IO, App] r) => EvalOptions -> Sem r ()
 runCommand opts@EvalOptions {..} = do
   Core.CoreResult {..} <- runPipeline _evalInputFile upToCore
-  let tab = Core.toEval _coreResultTable
-      evalNode =
+  r <- runError @JuvixError $ Core.toEval _coreResultTable
+  tab <- getRight r
+  let evalNode =
         if
             | isJust (_evalSymbolName) -> getNode' tab (selInfo tab)
             | otherwise -> getNode' tab (mainInfo tab)

app/Commands/Repl.hs

@@ -175,8 +175,10 @@ runCommand opts = do
             where
               eval :: Core.Node -> Repl (Either JuvixError Core.Node)
               eval n =
-                let (tab', n') = runTransformations (Core.toEvalTransformations ++ opts ^. replTransformations) infoTable n
-                 in liftIO $
+                case run $ runError @JuvixError $ runTransformations (Core.toEvalTransformations ++ opts ^. replTransformations) infoTable n of
+                  Left err -> return $ Left err
+                  Right (tab', n') ->
+                    liftIO $
                       mapLeft
                         (JuvixError @Core.CoreError)
                         <$> doEvalIO False defaultLoc tab' n'

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -4,6 +4,7 @@ import Data.HashMap.Strict qualified as HashMap
 import Data.List qualified as List
 import Juvix.Compiler.Backend.Geb.Extra
 import Juvix.Compiler.Backend.Geb.Language
+import Juvix.Compiler.Core.Data.IdentDependencyInfo qualified as Core
 import Juvix.Compiler.Core.Data.InfoTable qualified as Core
 import Juvix.Compiler.Core.Extra qualified as Core
 import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
@@ -184,72 +185,8 @@ fromCore tab = case tab ^. Core.infoMain of
       Core.OpIntDiv -> convertBinop OpDiv _builtinAppArgs
       Core.OpIntMod -> convertBinop OpMod _builtinAppArgs
       Core.OpIntLt -> convertBinop OpLt _builtinAppArgs
-      Core.OpIntLe -> case _builtinAppArgs of
-        [arg1, arg2] -> do
-          arg1' <- convertNode arg1
-          arg2' <- convertNode arg2
-          let le =
-                MorphismLambda
-                  Lambda
-                    { _lambdaVarType = ObjectInteger,
-                      _lambdaBodyType =
-                        ObjectHom
-                          Hom
-                            { _homDomain = ObjectInteger,
-                              _homCodomain = objectBool
-                            },
-                      _lambdaBody =
-                        MorphismLambda
-                          Lambda
-                            { _lambdaVarType = ObjectInteger,
-                              _lambdaBodyType = objectBool,
-                              _lambdaBody =
-                                mkOr
-                                  ( MorphismBinop
-                                      Binop
-                                        { _binopOpcode = OpLt,
-                                          _binopLeft = MorphismVar Var {_varIndex = 1},
-                                          _binopRight = MorphismVar Var {_varIndex = 0}
-                                        }
-                                  )
-                                  ( MorphismBinop
-                                      Binop
-                                        { _binopOpcode = OpEq,
-                                          _binopLeft = MorphismVar Var {_varIndex = 1},
-                                          _binopRight = MorphismVar Var {_varIndex = 0}
-                                        }
-                                  )
-                            }
-                    }
-           in return $
-                MorphismApplication
-                  Application
-                    { _applicationDomainType = ObjectInteger,
-                      _applicationCodomainType =
-                        ObjectHom
-                          Hom
-                            { _homDomain = ObjectInteger,
-                              _homCodomain = objectBool
-                            },
-                      _applicationLeft =
-                        MorphismApplication
-                          Application
-                            { _applicationDomainType = ObjectInteger,
-                              _applicationCodomainType = objectBool,
-                              _applicationLeft = le,
-                              _applicationRight = arg2'
-                            },
-                      _applicationRight = arg1'
-                    }
-        _ ->
-          error "wrong builtin application argument number"
-      Core.OpEq ->
-        case _builtinAppArgs of
-          arg : _
-            | Info.getNodeType arg == Core.mkTypeInteger' ->
-                convertBinop OpEq _builtinAppArgs
-          _ ->
-            error "unsupported equality argument types"
+      Core.OpIntLe -> convertOpIntLe _builtinAppArgs
+      Core.OpEq -> convertOpEq _builtinAppArgs
       _ ->
         unsupported
 
@@ -268,6 +205,75 @@ fromCore tab = case tab ^. Core.infoMain of
       _ ->
         error "wrong builtin application argument number"
 
+    convertOpIntLe :: [Core.Node] -> Trans Morphism
+    convertOpIntLe = \case
+      [arg1, arg2] -> do
+        arg1' <- convertNode arg1
+        arg2' <- convertNode arg2
+        let le =
+              MorphismLambda
+                Lambda
+                  { _lambdaVarType = ObjectInteger,
+                    _lambdaBodyType =
+                      ObjectHom
+                        Hom
+                          { _homDomain = ObjectInteger,
+                            _homCodomain = objectBool
+                          },
+                    _lambdaBody =
+                      MorphismLambda
+                        Lambda
+                          { _lambdaVarType = ObjectInteger,
+                            _lambdaBodyType = objectBool,
+                            _lambdaBody =
+                              mkOr
+                                ( MorphismBinop
+                                    Binop
+                                      { _binopOpcode = OpLt,
+                                        _binopLeft = MorphismVar Var {_varIndex = 1},
+                                        _binopRight = MorphismVar Var {_varIndex = 0}
+                                      }
+                                )
+                                ( MorphismBinop
+                                    Binop
+                                      { _binopOpcode = OpEq,
+                                        _binopLeft = MorphismVar Var {_varIndex = 1},
+                                        _binopRight = MorphismVar Var {_varIndex = 0}
+                                      }
+                                )
+                          }
+                  }
+         in return $
+              MorphismApplication
+                Application
+                  { _applicationDomainType = ObjectInteger,
+                    _applicationCodomainType =
+                      ObjectHom
+                        Hom
+                          { _homDomain = ObjectInteger,
+                            _homCodomain = objectBool
+                          },
+                    _applicationLeft =
+                      MorphismApplication
+                        Application
+                          { _applicationDomainType = ObjectInteger,
+                            _applicationCodomainType = objectBool,
+                            _applicationLeft = le,
+                            _applicationRight = arg2'
+                          },
+                    _applicationRight = arg1'
+                  }
+      _ ->
+        error "wrong builtin application argument number"
+
+    convertOpEq :: [Core.Node] -> Trans Morphism
+    convertOpEq args = case args of
+      arg : _
+        | Info.getNodeType arg == Core.mkTypeInteger' ->
+            convertBinop OpEq args
+      _ ->
+        error "unsupported equality argument types"
+
     convertConstr :: Core.Constr -> Trans Morphism
     convertConstr Core.Constr {..} = do
       args <- convertProduct _constrArgs

src/Juvix/Compiler/Core/Extra/IdentDependencyInfo.hs → src/Juvix/Compiler/Core/Data/IdentDependencyInfo.hs

@@ -1,4 +1,4 @@
-module Juvix.Compiler.Core.Extra.IdentDependencyInfo where
+module Juvix.Compiler.Core.Data.IdentDependencyInfo where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet

src/Juvix/Compiler/Core/Data/TransformationId.hs

@@ -16,6 +16,7 @@ data TransformationId
   | MatchToCase
   | EtaExpandApps
   | DisambiguateNames
+  | CheckGeb
   deriving stock (Data, Bounded, Enum)
 
 data PipelineId
@@ -47,7 +48,7 @@ toStrippedTransformations =
   toEvalTransformations ++ [LambdaLetRecLifting, TopEtaExpand, MoveApps, RemoveTypeArgs]
 
 toGebTransformations :: [TransformationId]
-toGebTransformations = toEvalTransformations ++ [UnrollRecursion, ComputeTypeInfo]
+toGebTransformations = toEvalTransformations ++ [LetRecLifting, CheckGeb, UnrollRecursion, ComputeTypeInfo]
 
 toEvalTransformations :: [TransformationId]
 toEvalTransformations = [EtaExpandApps, MatchToCase, NatToInt, ConvertBuiltinTypes]

src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs

@@ -80,6 +80,7 @@ transformationText = \case
   ComputeTypeInfo -> strComputeTypeInfo
   UnrollRecursion -> strUnrollRecursion
   DisambiguateNames -> strDisambiguateNames
+  CheckGeb -> strCheckGeb
 
 parsePipeline :: MonadParsec e Text m => m PipelineId
 parsePipeline = choice [symbol (pipelineText t) $> t | t <- allElements]
@@ -137,3 +138,6 @@ strUnrollRecursion = "unroll-recursion"
 
 strDisambiguateNames :: Text
 strDisambiguateNames = "disambiguate-names"
+
+strCheckGeb :: Text
+strCheckGeb = "check-geb"

src/Juvix/Compiler/Core/Evaluator.hs

@@ -262,7 +262,7 @@ catchEvalErrorIO loc ma =
 toCoreError :: Location -> EvalError -> CoreError
 toCoreError loc (EvalError {..}) =
   CoreError
-    { _coreErrorMsg = mappend "evaluation error: " _evalErrorMsg,
+    { _coreErrorMsg = "evaluation error: " <> _evalErrorMsg,
       _coreErrorNode = _evalErrorNode,
       _coreErrorLoc = fromMaybe loc (lookupLocation =<< _evalErrorNode)
     }

src/Juvix/Compiler/Core/Extra.hs

@@ -1,8 +1,6 @@
 module Juvix.Compiler.Core.Extra
   ( module Juvix.Compiler.Core.Extra.Utils,
-    module Juvix.Compiler.Core.Extra.IdentDependencyInfo,
   )
 where
 
-import Juvix.Compiler.Core.Extra.IdentDependencyInfo
 import Juvix.Compiler.Core.Extra.Utils

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -31,6 +31,14 @@ import Juvix.Compiler.Core.Language
 isClosed :: Node -> Bool
 isClosed = not . has freeVars
 
+isTypeConstr :: InfoTable -> Type -> Bool
+isTypeConstr tab ty = case typeTarget ty of
+  NUniv {} ->
+    True
+  NIdt Ident {..} ->
+    isTypeConstr tab (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
+  _ -> False
+
 freeVarsSorted :: Node -> Set Var
 freeVarsSorted n = Set.fromList (n ^.. freeVars)
 

src/Juvix/Compiler/Core/Pipeline.hs

@@ -8,14 +8,14 @@ import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Transformation
 
 -- | Perform transformations on Core necessary for efficient evaluation
-toEval :: InfoTable -> InfoTable
+toEval :: Member (Error JuvixError) r => InfoTable -> Sem r InfoTable
 toEval = applyTransformations toEvalTransformations
 
 -- | Perform transformations on Core necessary before the translation to
 -- Core.Stripped
-toStripped :: InfoTable -> InfoTable
+toStripped :: Member (Error JuvixError) r => InfoTable -> Sem r InfoTable
 toStripped = applyTransformations toStrippedTransformations
 
 -- | Perform transformations on Core necessary before the translation to GEB
-toGeb :: InfoTable -> InfoTable
+toGeb :: Member (Error JuvixError) r => InfoTable -> Sem r InfoTable
 toGeb = applyTransformations toGebTransformations

src/Juvix/Compiler/Core/Transformation.hs

@@ -9,7 +9,9 @@ module Juvix.Compiler.Core.Transformation
 where
 
 import Juvix.Compiler.Core.Data.TransformationId
+import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.CheckGeb
 import Juvix.Compiler.Core.Transformation.ComputeTypeInfo
 import Juvix.Compiler.Core.Transformation.ConvertBuiltinTypes
 import Juvix.Compiler.Core.Transformation.DisambiguateNames
@@ -23,21 +25,22 @@ import Juvix.Compiler.Core.Transformation.RemoveTypeArgs
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
 import Juvix.Compiler.Core.Transformation.UnrollRecursion
 
-applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
-applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
+applyTransformations :: forall r. Member (Error JuvixError) r => [TransformationId] -> InfoTable -> Sem r InfoTable
+applyTransformations ts tbl = foldl' (\acc tid -> acc >>= appTrans tid) (return tbl) ts
   where
-    appTrans :: TransformationId -> InfoTable -> InfoTable
+    appTrans :: TransformationId -> InfoTable -> Sem r InfoTable
     appTrans = \case
-      LambdaLetRecLifting -> lambdaLetRecLifting
-      LetRecLifting -> letRecLifting
-      Identity -> identity
-      TopEtaExpand -> topEtaExpand
-      RemoveTypeArgs -> removeTypeArgs
-      MoveApps -> moveApps
-      NatToInt -> natToInt
-      ConvertBuiltinTypes -> convertBuiltinTypes
-      ComputeTypeInfo -> computeTypeInfo
-      UnrollRecursion -> unrollRecursion
-      MatchToCase -> matchToCase
-      EtaExpandApps -> etaExpansionApps
-      DisambiguateNames -> disambiguateNames
+      LambdaLetRecLifting -> return . lambdaLetRecLifting
+      LetRecLifting -> return . letRecLifting
+      Identity -> return . identity
+      TopEtaExpand -> return . topEtaExpand
+      RemoveTypeArgs -> return . removeTypeArgs
+      MoveApps -> return . moveApps
+      NatToInt -> return . natToInt
+      ConvertBuiltinTypes -> return . convertBuiltinTypes
+      ComputeTypeInfo -> return . computeTypeInfo
+      UnrollRecursion -> return . unrollRecursion
+      MatchToCase -> return . matchToCase
+      EtaExpandApps -> return . etaExpansionApps
+      DisambiguateNames -> return . disambiguateNames
+      CheckGeb -> mapError (JuvixError @CoreError) . checkGeb