Register builtins during scoping and report proper errors instead of crashing

app/App.hs

@@ -260,15 +260,14 @@ runPipelineHtml ::
   Bool ->
   Maybe (AppPath File) ->
   Sem r (InternalTypedResult, [InternalTypedResult])
-runPipelineHtml bNonRecursive input_ =
-  if
-      | bNonRecursive -> do
-          r <- runPipelineNoOptions input_ upToInternalTyped
-          return (r, [])
-      | otherwise -> do
-          args <- askArgs
-          entry <- getEntryPoint' args input_
-          runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError
+runPipelineHtml bNonRecursive input_
+  | bNonRecursive = do
+      r <- runPipelineNoOptions input_ upToInternalTyped
+      return (r, [])
+  | otherwise = do
+      args <- askArgs
+      entry <- getEntryPoint' args input_
+      runReader defaultPipelineOptions (runPipelineHtmlEither entry) >>= fromRightJuvixError
 
 runPipelineOptions :: (Members '[App] r) => Sem (Reader PipelineOptions ': r) a -> Sem r a
 runPipelineOptions m = do

src/Juvix/Compiler/Builtins.hs

@@ -1,6 +1,5 @@
 module Juvix.Compiler.Builtins
-  ( module Juvix.Compiler.Builtins.Effect,
-    module Juvix.Compiler.Builtins.Nat,
+  ( module Juvix.Compiler.Builtins.Nat,
     module Juvix.Compiler.Builtins.IO,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
@@ -24,7 +23,6 @@ import Juvix.Compiler.Builtins.ByteArray
 import Juvix.Compiler.Builtins.Cairo
 import Juvix.Compiler.Builtins.Control
 import Juvix.Compiler.Builtins.Debug
-import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Builtins.Field
 import Juvix.Compiler.Builtins.IO
 import Juvix.Compiler.Builtins.Int

src/Juvix/Compiler/Builtins/Anoma.hs

@@ -1,119 +1,109 @@
 module Juvix.Compiler.Builtins.Anoma where
 
 import Data.HashSet qualified as HashSet
-import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-registerAnomaGet :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaGet f = do
+checkAnomaGet :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaGet f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   keyT <- freshVar l "keyT"
   valueT <- freshVar l "valueT"
-  let freeVars = HashSet.fromList [keyT, valueT]
-  unless
-    ((ftype ==% (u <>--> u <>--> keyT --> valueT)) freeVars)
-    (error "anomaGet must be of type {Value Key : Type} -> Key -> Value")
-  registerBuiltin BuiltinAnomaGet (f ^. axiomName)
+  let freeVars = hashSet [keyT, valueT]
+  unless ((ftype ==% (u <>--> u <>--> keyT --> valueT)) freeVars) $
+    builtinsErrorText (getLoc f) "anomaGet must be of type {Value Key : Type} -> Key -> Value"
 
-registerAnomaEncode :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaEncode f = do
+checkAnomaEncode :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaEncode f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   encodeT <- freshVar l "encodeT"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
-  let freeVars = HashSet.fromList [encodeT]
-  unless
-    ((ftype ==% (u <>--> encodeT --> nat)) freeVars)
-    (error "anomaEncode must be of type {A : Type} -> A -> Nat")
-  registerBuiltin BuiltinAnomaEncode (f ^. axiomName)
+  nat <- getBuiltinNameScoper (getLoc f) BuiltinNat
+  let freeVars = hashSet [encodeT]
+  unless ((ftype ==% (u <>--> encodeT --> nat)) freeVars) $
+    builtinsErrorText (getLoc f) "anomaEncode must be of type {A : Type} -> A -> Nat"
 
-registerAnomaDecode :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaDecode f = do
+checkAnomaDecode :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaDecode f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   decodeT <- freshVar l "decodeT"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  nat <- getBuiltinNameScoper (getLoc f) BuiltinNat
   let freeVars = HashSet.fromList [decodeT]
-  unless
-    ((ftype ==% (u <>--> nat --> decodeT)) freeVars)
-    (error "anomaEncode must be of type {A : Type} -> Nat -> A")
-  registerBuiltin BuiltinAnomaDecode (f ^. axiomName)
+  unless ((ftype ==% (u <>--> nat --> decodeT)) freeVars) $
+    builtinsErrorText (getLoc f) "anomaEncode must be of type {A : Type} -> Nat -> A"
 
-registerAnomaVerifyDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaVerifyDetached f = do
+checkAnomaVerifyDetached :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaVerifyDetached f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   decodeT <- freshVar l "signedDataT"
-  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  byteArray <- getBuiltinNameScoper (getLoc f) BuiltinByteArray
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
   let freeVars = HashSet.fromList [decodeT]
   unless
     ((ftype ==% (u <>--> byteArray --> decodeT --> byteArray --> bool_)) freeVars)
-    (error "anomaVerifyDetached must be of type {A : Type} -> ByteArray -> A -> ByteArray -> Bool")
-  registerBuiltin BuiltinAnomaVerifyDetached (f ^. axiomName)
+    $ builtinsErrorText (getLoc f) "anomaVerifyDetached must be of type {A : Type} -> ByteArray -> A -> ByteArray -> Bool"
 
-registerAnomaSign :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaSign f = do
+checkAnomaSign :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaSign f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
-  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
+  byteArray <- getBuiltinNameScoper (getLoc f) BuiltinByteArray
   let freeVars = HashSet.fromList [dataT]
   unless
     ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
-    (error "anomaSign must be of type {A : Type} -> A -> ByteArray -> ByteArray")
-  registerBuiltin BuiltinAnomaSign (f ^. axiomName)
+    $ builtinsErrorText (getLoc f) "anomaSign must be of type {A : Type} -> A -> ByteArray -> ByteArray"
 
-registerAnomaVerifyWithMessage :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaVerifyWithMessage f = do
+checkAnomaVerifyWithMessage :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaVerifyWithMessage f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
-  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
-  maybe_ <- getBuiltinName (getLoc f) BuiltinMaybe
+  byteArray <- getBuiltinNameScoper (getLoc f) BuiltinByteArray
+  maybe_ <- getBuiltinNameScoper (getLoc f) BuiltinMaybe
   let freeVars = HashSet.fromList [dataT]
   unless
     ((ftype ==% (u <>--> byteArray --> byteArray --> maybe_ @@ dataT)) freeVars)
-    (error "anomaVerify must be of type {A : Type} -> byteArray -> byteArray -> Maybe A")
-  registerBuiltin BuiltinAnomaVerifyWithMessage (f ^. axiomName)
+    $ builtinsErrorText (getLoc f) "anomaVerify must be of type {A : Type} -> byteArray -> byteArray -> Maybe A"
 
-registerAnomaSignDetached :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerAnomaSignDetached f = do
+checkAnomaSignDetached :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaSignDetached f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   dataT <- freshVar l "dataT"
-  byteArray <- getBuiltinName (getLoc f) BuiltinByteArray
+  byteArray <- getBuiltinNameScoper (getLoc f) BuiltinByteArray
   let freeVars = HashSet.fromList [dataT]
   unless
     ((ftype ==% (u <>--> dataT --> byteArray --> byteArray)) freeVars)
-    (error "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray")
-  registerBuiltin BuiltinAnomaSignDetached (f ^. axiomName)
+    $ builtinsErrorText (getLoc f) "anomaSignDetached must be of type {A : Type} -> A -> ByteArray -> ByteArray"
 
-registerByteArrayToAnomaContents :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerByteArrayToAnomaContents f = do
-  let loc = getLoc f
-  byteArray <- getBuiltinName loc BuiltinByteArray
-  nat_ <- getBuiltinName loc BuiltinNat
+checkAnomaByteArrayToAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaByteArrayToAnomaContents f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
   unless
-    (f ^. axiomType == (byteArray --> nat_))
-    (error "toAnomaContents must be of type ByteArray -> Nat")
-  registerBuiltin BuiltinAnomaByteArrayToAnomaContents (f ^. axiomName)
+    (ftype == (byteArray --> nat_))
+    $ builtinsErrorText l "toAnomaContents must be of type ByteArray -> Nat"
 
-registerByteArrayFromAnomaContents :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
-registerByteArrayFromAnomaContents f = do
-  let loc = getLoc f
-  byteArray <- getBuiltinName loc BuiltinByteArray
-  nat_ <- getBuiltinName loc BuiltinNat
+checkAnomaByteArrayFromAnomaContents :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkAnomaByteArrayFromAnomaContents f = do
+  let ftype = f ^. axiomType
+      l = getLoc f
+  byteArray <- getBuiltinNameScoper l BuiltinByteArray
+  nat_ <- getBuiltinNameScoper l BuiltinNat
   unless
-    (f ^. axiomType == (nat_ --> nat_ --> byteArray))
-    (error "fromAnomaContents must be of type Nat -> Nat -> ByteArray")
-  registerBuiltin BuiltinAnomaByteArrayFromAnomaContents (f ^. axiomName)
+    (ftype == (nat_ --> nat_ --> byteArray))
+    $ builtinsErrorText l "fromAnomaContents must be of type Nat -> Nat -> ByteArray"

src/Juvix/Compiler/Builtins/Bool.hs

@@ -1,40 +1,40 @@
 module Juvix.Compiler.Builtins.Bool where
 
-import Juvix.Compiler.Builtins.Effect
+import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Prelude
 
-registerBoolDef :: (Member Builtins r) => InductiveDef -> Sem r ()
-registerBoolDef d = do
-  unless (null (d ^. inductiveParameters)) (error "Bool should have no type parameters")
-  unless (isSmallUniverse' (d ^. inductiveType)) (error "Bool should be in the small universe")
-  registerBuiltin BuiltinBool (d ^. inductiveName)
+checkBoolDef :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkBoolDef d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "Bool should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "Bool should be in the small universe")
   case d ^. inductiveConstructors of
-    [c1, c2] -> registerTrue c1 >> registerFalse c2
-    _ -> error "Bool should have exactly two constructors"
+    [c1, c2] -> checkTrue c1 >> checkFalse c2
+    _ -> err "Bool should have exactly two constructors"
 
-registerTrue :: (Member Builtins r) => ConstructorDef -> Sem r ()
-registerTrue d@ConstructorDef {..} = do
-  let ctorTrue = _inductiveConstructorName
-      ctorTy = _inductiveConstructorType
-  boolTy <- getBuiltinName (getLoc d) BuiltinBool
-  unless (ctorTy === boolTy) (error $ "true has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
-  registerBuiltin BuiltinBoolTrue ctorTrue
+checkTrue :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkTrue d@ConstructorDef {..} = do
+  let ctorTy = _inductiveConstructorType
+  boolTy <- getBuiltinNameScoper (getLoc d) BuiltinBool
+  unless (ctorTy === boolTy) $
+    builtinsErrorMsg (getLoc d) $
+      "true has the wrong type " <> ppOutDefault ctorTy <> " | " <> ppOutDefault boolTy
 
-registerFalse :: (Member Builtins r) => ConstructorDef -> Sem r ()
-registerFalse d@ConstructorDef {..} = do
-  let ctorFalse = _inductiveConstructorName
-      ctorTy = _inductiveConstructorType
-  boolTy <- getBuiltinName (getLoc d) BuiltinBool
-  unless (ctorTy === boolTy) (error $ "false has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
-  registerBuiltin BuiltinBoolFalse ctorFalse
+checkFalse :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
+checkFalse d@ConstructorDef {..} = do
+  let ctorTy = _inductiveConstructorType
+  boolTy <- getBuiltinNameScoper (getLoc d) BuiltinBool
+  unless (ctorTy === boolTy) $
+    builtinsErrorMsg (getLoc d) $
+      "false has the wrong type " <> ppOutDefault ctorTy <> " | " <> ppOutDefault boolTy
 
-registerIf :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
-registerIf f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
+checkIf :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkIf f = do
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
+  true_ <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolTrue
+  false_ <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolFalse
   let if_ = f ^. funDefName
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
@@ -47,7 +47,7 @@ registerIf f = do
         [ (if_ @@ true_ @@ e @@ hole, e),
           (if_ @@ false_ @@ hole @@ e, e)
         ]
-  registerFun
+  checkBuiltinFunctionInfo
     FunInfo
       { _funInfoDef = f,
         _funInfoBuiltin = BuiltinBoolIf,
@@ -57,11 +57,11 @@ registerIf f = do
         _funInfoFreeTypeVars = [vart]
       }
 
-registerOr :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
-registerOr f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
+checkOr :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkOr f = do
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
+  true_ <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolTrue
+  false_ <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolFalse
   let or_ = f ^. funDefName
       l = getLoc f
   vare <- freshVar l "e"
@@ -72,7 +72,7 @@ registerOr f = do
         [ (or_ @@ true_ @@ hole, true_),
           (or_ @@ false_ @@ e, e)
         ]
-  registerFun
+  checkBuiltinFunctionInfo
     FunInfo
       { _funInfoDef = f,
         _funInfoBuiltin = BuiltinBoolOr,
@@ -82,11 +82,11 @@ registerOr f = do
         _funInfoFreeTypeVars = []
       }
 
-registerAnd :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
-registerAnd f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
+checkAnd :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkAnd f = do
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
+  true_ <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolTrue
+  false_ <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolFalse
   let and_ = f ^. funDefName
       l = getLoc f
   vare <- freshVar l "e"
@@ -97,7 +97,7 @@ registerAnd f = do
         [ (and_ @@ true_ @@ e, e),
           (and_ @@ false_ @@ hole, false_)
         ]
-  registerFun
+  checkBuiltinFunctionInfo
     FunInfo
       { _funInfoDef = f,
         _funInfoBuiltin = BuiltinBoolAnd,
@@ -107,9 +107,9 @@ registerAnd f = do
         _funInfoFreeTypeVars = []
       }
 
-registerBoolPrint :: (Members '[Builtins] r) => AxiomDef -> Sem r ()
-registerBoolPrint f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  io <- getBuiltinName (getLoc f) BuiltinIO
-  unless (f ^. axiomType === (bool_ --> io)) (error "Bool print has the wrong type signature")
-  registerBuiltin BuiltinBoolPrint (f ^. axiomName)
+checkBoolPrint :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkBoolPrint f = do
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
+  io <- getBuiltinNameScoper (getLoc f) BuiltinIO
+  unless (f ^. axiomType === (bool_ --> io)) $
+    builtinsErrorText (getLoc f) "Bool print has the wrong type signature"