remove builtins effect

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,
@@ -22,7 +21,6 @@ import Juvix.Compiler.Builtins.Byte
 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

@@ -5,81 +5,81 @@ import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-checkAnomaGet :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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]
+  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"
 
-checkAnomaEncode :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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]
+  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"
 
-checkAnomaDecode :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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) $
     builtinsErrorText (getLoc f) "anomaEncode must be of type {A : Type} -> Nat -> A"
 
-checkAnomaVerifyDetached :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  nat <- getBuiltinNameScoper (getLoc f) BuiltinNat
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
   let freeVars = HashSet.fromList [decodeT]
   unless ((ftype ==% (u <>--> nat --> decodeT --> nat --> bool_)) freeVars) $
     builtinsErrorText (getLoc f) "anomaVerifyDetached must be of type {A : Type} -> Nat -> A -> Nat -> Bool"
 
-checkAnomaSign :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  nat <- getBuiltinNameScoper (getLoc f) BuiltinNat
   let freeVars = HashSet.fromList [dataT]
   unless ((ftype ==% (u <>--> dataT --> nat --> nat)) freeVars) $
     builtinsErrorText (getLoc f) "anomaSign must be of type {A : Type} -> A -> Nat -> Nat"
 
-checkAnomaVerifyWithMessage :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
-  maybe_ <- getBuiltinName (getLoc f) BuiltinMaybe
+  nat <- getBuiltinNameScoper (getLoc f) BuiltinNat
+  maybe_ <- getBuiltinNameScoper (getLoc f) BuiltinMaybe
   let freeVars = HashSet.fromList [dataT]
   unless ((ftype ==% (u <>--> nat --> nat --> maybe_ @@ dataT)) freeVars) $
     builtinsErrorText (getLoc f) "anomaVerify must be of type {A : Type} -> Nat -> Nat -> Maybe A"
 
-checkAnomaSignDetached :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+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"
-  nat <- getBuiltinName (getLoc f) BuiltinNat
+  nat <- getBuiltinNameScoper (getLoc f) BuiltinNat
   let freeVars = HashSet.fromList [dataT]
   unless ((ftype ==% (u <>--> dataT --> nat --> nat)) freeVars) $
     builtinsErrorText (getLoc f) "anomaSignDetached must be of type {A : Type} -> A -> Nat -> Nat"

src/Juvix/Compiler/Builtins/Bool.hs

@@ -5,7 +5,7 @@ import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
 import Juvix.Prelude
 
-checkBoolDef :: (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r ()
+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")
@@ -14,27 +14,27 @@ checkBoolDef d = do
     [c1, c2] -> checkTrue c1 >> checkFalse c2
     _ -> err "Bool should have exactly two constructors"
 
-checkTrue :: (Members '[Builtins, Error BuiltinsError] r) => ConstructorDef -> Sem r ()
+checkTrue :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
 checkTrue d@ConstructorDef {..} = do
   let ctorTy = _inductiveConstructorType
-  boolTy <- getBuiltinName (getLoc d) BuiltinBool
+  boolTy <- getBuiltinNameScoper (getLoc d) BuiltinBool
   unless (ctorTy === boolTy) $
     builtinsErrorMsg (getLoc d) $
       "true has the wrong type " <> ppOutDefault ctorTy <> " | " <> ppOutDefault boolTy
 
-checkFalse :: (Members '[Builtins, Error BuiltinsError] r) => ConstructorDef -> Sem r ()
+checkFalse :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
 checkFalse d@ConstructorDef {..} = do
   let ctorTy = _inductiveConstructorType
-  boolTy <- getBuiltinName (getLoc d) BuiltinBool
+  boolTy <- getBuiltinNameScoper (getLoc d) BuiltinBool
   unless (ctorTy === boolTy) $
     builtinsErrorMsg (getLoc d) $
       "false has the wrong type " <> ppOutDefault ctorTy <> " | " <> ppOutDefault boolTy
 
-checkIf :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkIf :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
 checkIf f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
+  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
@@ -57,11 +57,11 @@ checkIf f = do
         _funInfoFreeTypeVars = [vart]
       }
 
-checkOr :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkOr :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
 checkOr f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
+  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"
@@ -82,11 +82,11 @@ checkOr f = do
         _funInfoFreeTypeVars = []
       }
 
-checkAnd :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkAnd :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
 checkAnd f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
-  false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
+  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"
@@ -107,9 +107,9 @@ checkAnd f = do
         _funInfoFreeTypeVars = []
       }
 
-checkBoolPrint :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r ()
+checkBoolPrint :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
 checkBoolPrint f = do
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
-  io <- getBuiltinName (getLoc f) BuiltinIO
+  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"

src/Juvix/Compiler/Builtins/Byte.hs

@@ -4,29 +4,29 @@ import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-checkByte :: (Members '[Error BuiltinsError] r) => AxiomDef -> Sem r ()
+checkByte :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
 checkByte d = do
   unless (isSmallUniverse' (d ^. axiomType)) $
     builtinsErrorText (getLoc d) "Byte should be in the small universe"
 
-checkByteEq :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r ()
+checkByteEq :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
 checkByteEq f = do
-  byte_ <- getBuiltinName (getLoc f) BuiltinByte
-  bool_ <- getBuiltinName (getLoc f) BuiltinBool
+  byte_ <- getBuiltinNameScoper (getLoc f) BuiltinByte
+  bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool
   unless (f ^. axiomType === (byte_ --> byte_ --> bool_)) $
     builtinsErrorText (getLoc f) "Byte equality has the wrong type signature"
 
-checkByteFromNat :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r ()
+checkByteFromNat :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
 checkByteFromNat d = do
   let l = getLoc d
-  byte_ <- getBuiltinName l BuiltinByte
-  nat <- getBuiltinName l BuiltinNat
+  byte_ <- getBuiltinNameScoper l BuiltinByte
+  nat <- getBuiltinNameScoper l BuiltinNat
   unless (d ^. axiomType === (nat --> byte_)) $
     builtinsErrorText (getLoc d) "byte-from-nat has the wrong type signature"
 
-checkByteToNat :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r ()
+checkByteToNat :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
 checkByteToNat f = do
-  byte_ <- getBuiltinName (getLoc f) BuiltinByte
-  nat_ <- getBuiltinName (getLoc f) BuiltinNat
+  byte_ <- getBuiltinNameScoper (getLoc f) BuiltinByte
+  nat_ <- getBuiltinNameScoper (getLoc f) BuiltinNat
   unless (f ^. axiomType === (byte_ --> nat_)) $
     builtinsErrorText (getLoc f) "byte-to-nat has the wrong type signature"

src/Juvix/Compiler/Builtins/Cairo.hs

@@ -4,7 +4,7 @@ import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-checkPoseidonStateDef :: (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r ()
+checkPoseidonStateDef :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
 checkPoseidonStateDef d = do
   let err = builtinsErrorText (getLoc d)
   unless (null (d ^. inductiveParameters)) (err "PoseidonState should have no type parameters")
@@ -13,22 +13,22 @@ checkPoseidonStateDef d = do
     [c] -> checkMkPoseidonState c
     _ -> err "PoseidonState should have exactly one constructor"
 
-checkMkPoseidonState :: (Members '[Builtins, Error BuiltinsError] r) => ConstructorDef -> Sem r ()
+checkMkPoseidonState :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
 checkMkPoseidonState d@ConstructorDef {..} = do
   let ty = _inductiveConstructorType
-  field_ <- getBuiltinName (getLoc d) BuiltinField
-  ps <- getBuiltinName (getLoc d) BuiltinPoseidonState
+  field_ <- getBuiltinNameScoper (getLoc d) BuiltinField
+  ps <- getBuiltinNameScoper (getLoc d) BuiltinPoseidonState
   unless (ty === (field_ --> field_ --> field_ --> ps)) $
     builtinsErrorText (getLoc d) "mkPoseidonState has the wrong type"
 
-checkPoseidon :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkPoseidon :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
 checkPoseidon f = do
   let ftype = f ^. axiomType
-  ps <- getBuiltinName (getLoc f) BuiltinPoseidonState
+  ps <- getBuiltinNameScoper (getLoc f) BuiltinPoseidonState
   unless (ftype === (ps --> ps)) $
     builtinsErrorText (getLoc f) "poseidon must be of type PoseidonState -> PoseidonState"
 
-checkEcPointDef :: (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r ()
+checkEcPointDef :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
 checkEcPointDef d = do
   let err = builtinsErrorText (getLoc d)
   unless (null (d ^. inductiveParameters)) (err "Ec.Point should have no type parameters")
@@ -37,25 +37,25 @@ checkEcPointDef d = do
     [c] -> checkMkEcPoint c
     _ -> err "Ec.Point should have exactly one constructor"
 
-checkMkEcPoint :: (Members '[Builtins, Error BuiltinsError] r) => ConstructorDef -> Sem r ()
+checkMkEcPoint :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r ()
 checkMkEcPoint d@ConstructorDef {..} = do
   let ty = _inductiveConstructorType
-  field_ <- getBuiltinName (getLoc d) BuiltinField
-  pt <- getBuiltinName (getLoc d) BuiltinEcPoint
+  field_ <- getBuiltinNameScoper (getLoc d) BuiltinField
+  pt <- getBuiltinNameScoper (getLoc d) BuiltinEcPoint
   unless (ty === (field_ --> field_ --> pt)) $
     builtinsErrorText (getLoc d) "EC.mkPoint has the wrong type"
 
-checkEcOp :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkEcOp :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
 checkEcOp f = do
   let ftype = f ^. axiomType
-  pt <- getBuiltinName (getLoc f) BuiltinEcPoint
-  field_ <- getBuiltinName (getLoc f) BuiltinField
+  pt <- getBuiltinNameScoper (getLoc f) BuiltinEcPoint
+  field_ <- getBuiltinNameScoper (getLoc f) BuiltinField
   unless (ftype === (pt --> field_ --> pt --> pt)) $
     builtinsErrorText (getLoc f) "ecOp must be of type Ec.Point -> Field -> Ec.Point -> Ec.Point"
 
-checkRandomEcPoint :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkRandomEcPoint :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
 checkRandomEcPoint f = do
   let ftype = f ^. axiomType
-  pt <- getBuiltinName (getLoc f) BuiltinEcPoint
+  pt <- getBuiltinNameScoper (getLoc f) BuiltinEcPoint
   unless (ftype === pt) $
     builtinsErrorText (getLoc f) "randomEcPoint must be of type Ec.Point"

src/Juvix/Compiler/Builtins/Control.hs

@@ -4,7 +4,7 @@ import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-checkSeq :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r ()
+checkSeq :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r ()
 checkSeq f = do
   let u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f

src/Juvix/Compiler/Builtins/Debug.hs

@@ -5,7 +5,7 @@ import Juvix.Compiler.Internal.Builtins
 import Juvix.Compiler.Internal.Extra
 import Juvix.Prelude
 
-checkTrace :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkTrace :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
 checkTrace f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
@@ -15,13 +15,13 @@ checkTrace f = do
   unless ((ftype ==% (u <>--> a --> a)) freeVars) $
     builtinsErrorText (getLoc f) "trace must be of type {A : Type} -> A -> A"
 
-checkFail :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r ()
+checkFail :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r ()
 checkFail f = do
   let ftype = f ^. axiomType
       u = ExpressionUniverse smallUniverseNoLoc
       l = getLoc f
   a <- freshVar l "a"
   let freeVars = HashSet.fromList [a]
-  string_ <- getBuiltinName (getLoc f) BuiltinString
+  string_ <- getBuiltinNameScoper (getLoc f) BuiltinString
   unless ((ftype ==% (u <>--> string_ --> a)) freeVars) $
     builtinsErrorText (getLoc f) "fail must be of type {A : Type} -> String -> A"