diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs index 2648a6620f..6d200ae35d 100644 --- a/src/Juvix/Compiler/Builtins.hs +++ b/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 diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs index 7b3fff0af1..f6c0df50c7 100644 --- a/src/Juvix/Compiler/Builtins/Anoma.hs +++ b/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" diff --git a/src/Juvix/Compiler/Builtins/Bool.hs b/src/Juvix/Compiler/Builtins/Bool.hs index d9cf8a3779..07b6763b33 100644 --- a/src/Juvix/Compiler/Builtins/Bool.hs +++ b/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" diff --git a/src/Juvix/Compiler/Builtins/Byte.hs b/src/Juvix/Compiler/Builtins/Byte.hs index 7b9097ac54..d99defd739 100644 --- a/src/Juvix/Compiler/Builtins/Byte.hs +++ b/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" diff --git a/src/Juvix/Compiler/Builtins/Cairo.hs b/src/Juvix/Compiler/Builtins/Cairo.hs index 44409f9bec..6c762abe3c 100644 --- a/src/Juvix/Compiler/Builtins/Cairo.hs +++ b/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" diff --git a/src/Juvix/Compiler/Builtins/Control.hs b/src/Juvix/Compiler/Builtins/Control.hs index 46fb5703c8..157be65deb 100644 --- a/src/Juvix/Compiler/Builtins/Control.hs +++ b/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 diff --git a/src/Juvix/Compiler/Builtins/Debug.hs b/src/Juvix/Compiler/Builtins/Debug.hs index 5b5bb76917..9b149300bb 100644 --- a/src/Juvix/Compiler/Builtins/Debug.hs +++ b/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" diff --git a/src/Juvix/Compiler/Builtins/Effect.hs b/src/Juvix/Compiler/Builtins/Effect.hs deleted file mode 100644 index c41f1f116f..0000000000 --- a/src/Juvix/Compiler/Builtins/Effect.hs +++ /dev/null @@ -1,59 +0,0 @@ -module Juvix.Compiler.Builtins.Effect - ( module Juvix.Compiler.Builtins.Effect, - module Juvix.Compiler.Builtins.Error, - ) -where - -import Juvix.Compiler.Builtins.Error -import Juvix.Compiler.Concrete.Data.Builtins -import Juvix.Compiler.Concrete.Data.ScopedName -import Juvix.Prelude - -data Builtins :: Effect where - GetBuiltinSymbol' :: Interval -> BuiltinPrim -> Builtins m Symbol - RegisterBuiltin' :: BuiltinPrim -> Symbol -> Builtins m () - -makeSem ''Builtins - -registerBuiltin :: (IsBuiltin a, Member Builtins r) => a -> Symbol -> Sem r () -registerBuiltin = registerBuiltin' . toBuiltinPrim - -getBuiltinSymbol :: (IsBuiltin a, Member Builtins r) => Interval -> a -> Sem r Symbol -getBuiltinSymbol i = getBuiltinSymbol' i . toBuiltinPrim - -type BuiltinsTable = HashMap BuiltinPrim Symbol - -runBuiltins :: - forall r a. - (Member (Error BuiltinsError) r) => - BuiltinsTable -> - Sem (Builtins ': r) a -> - Sem r (BuiltinsTable, a) -runBuiltins ini = reinterpret (runState ini) $ \case - GetBuiltinSymbol' i b -> fromMaybeM notDefined (gets @BuiltinsTable (^. at b)) - where - notDefined :: Sem (State BuiltinsTable ': r) x - notDefined = - throw $ - ErrNotDefined - NotDefined - { _notDefinedBuiltin = b, - _notDefinedLoc = i - } - RegisterBuiltin' b n -> do - s <- gets @BuiltinsTable (^. at b) - case s of - Nothing -> modify @BuiltinsTable (set (at b) (Just n)) - Just {} -> alreadyDefined - where - alreadyDefined :: Sem (State BuiltinsTable ': r) x - alreadyDefined = - throw $ - ErrAlreadyDefined - AlreadyDefined - { _alreadyDefinedBuiltin = b, - _alreadyDefinedLoc = getLoc n - } - -evalBuiltins :: (Member (Error BuiltinsError) r) => BuiltinsTable -> Sem (Builtins ': r) a -> Sem r a -evalBuiltins s = fmap snd . runBuiltins s diff --git a/src/Juvix/Compiler/Builtins/Error.hs b/src/Juvix/Compiler/Builtins/Error.hs deleted file mode 100644 index d3ef677834..0000000000 --- a/src/Juvix/Compiler/Builtins/Error.hs +++ /dev/null @@ -1,32 +0,0 @@ -module Juvix.Compiler.Builtins.Error - ( module Juvix.Compiler.Builtins.Error, - module Juvix.Compiler.Builtins.Error.Types, - ) -where - -import Juvix.Compiler.Builtins.Error.Types -import Juvix.Prelude -import Juvix.Prelude.Pretty - -data BuiltinsError - = ErrAlreadyDefined AlreadyDefined - | ErrNotDefined NotDefined - | ErrBuiltinsErrorMessage BuiltinsErrorMessage - -instance ToGenericError BuiltinsError where - genericError = \case - ErrAlreadyDefined e -> genericError e - ErrNotDefined e -> genericError e - ErrBuiltinsErrorMessage e -> genericError e - -builtinsErrorMsg :: (Members '[Error BuiltinsError] r) => Interval -> AnsiText -> Sem r a -builtinsErrorMsg loc msg = - throw $ - ErrBuiltinsErrorMessage - BuiltinsErrorMessage - { _builtinsErrorMessageLoc = loc, - _builtinsErrorMessage = msg - } - -builtinsErrorText :: (Members '[Error BuiltinsError] r) => Interval -> Text -> Sem r a -builtinsErrorText loc = builtinsErrorMsg loc . mkAnsiText diff --git a/src/Juvix/Compiler/Builtins/Error/Types.hs b/src/Juvix/Compiler/Builtins/Error/Types.hs deleted file mode 100644 index 1b529c31d1..0000000000 --- a/src/Juvix/Compiler/Builtins/Error/Types.hs +++ /dev/null @@ -1,61 +0,0 @@ -module Juvix.Compiler.Builtins.Error.Types where - -import Juvix.Compiler.Concrete.Data.Builtins -import Juvix.Data.PPOutput -import Juvix.Prelude - -data AlreadyDefined = AlreadyDefined - { _alreadyDefinedBuiltin :: BuiltinPrim, - _alreadyDefinedLoc :: Interval - } - -makeLenses ''AlreadyDefined - -instance ToGenericError AlreadyDefined where - genericError e = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = ppOutput msg, - _genericErrorIntervals = [i] - } - where - i = e ^. alreadyDefinedLoc - msg = "The builtin" <+> code (pretty (e ^. alreadyDefinedBuiltin)) <+> "has already been defined" - -data NotDefined = NotDefined - { _notDefinedBuiltin :: BuiltinPrim, - _notDefinedLoc :: Interval - } - -makeLenses ''NotDefined - -instance ToGenericError NotDefined where - genericError e = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = ppOutput msg, - _genericErrorIntervals = [i] - } - where - i = e ^. notDefinedLoc - msg = "The builtin" <+> code (pretty (e ^. notDefinedBuiltin)) <+> "has not been defined" - --- | Generic error message related to builtins -data BuiltinsErrorMessage = BuiltinsErrorMessage - { _builtinsErrorMessage :: AnsiText, - _builtinsErrorMessageLoc :: Interval - } - -instance ToGenericError BuiltinsErrorMessage where - genericError BuiltinsErrorMessage {..} = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = _builtinsErrorMessage, - _genericErrorIntervals = [i] - } - where - i :: Interval - i = _builtinsErrorMessageLoc diff --git a/src/Juvix/Compiler/Builtins/Field.hs b/src/Juvix/Compiler/Builtins/Field.hs index aba6615f67..acd5b3f649 100644 --- a/src/Juvix/Compiler/Builtins/Field.hs +++ b/src/Juvix/Compiler/Builtins/Field.hs @@ -4,52 +4,52 @@ import Juvix.Compiler.Internal.Builtins import Juvix.Compiler.Internal.Extra import Juvix.Prelude -checkField :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkField :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkField d = do unless (isSmallUniverse' (d ^. axiomType)) $ builtinsErrorText (getLoc d) "String should be in the small universe" -checkFieldEq :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldEq :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldEq f = do - field_ <- getBuiltinName (getLoc f) BuiltinField - bool_ <- getBuiltinName (getLoc f) BuiltinBool + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField + bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool unless (f ^. axiomType === (field_ --> field_ --> bool_)) $ builtinsErrorText (getLoc f) "field equality has the wrong type signature" -checkFieldAdd :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldAdd :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldAdd f = do - field_ <- getBuiltinName (getLoc f) BuiltinField + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField unless (f ^. axiomType === (field_ --> field_ --> field_)) $ builtinsErrorText (getLoc f) "field addition has the wrong type signature" -checkFieldSub :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldSub :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldSub f = do - field_ <- getBuiltinName (getLoc f) BuiltinField + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField unless (f ^. axiomType === (field_ --> field_ --> field_)) $ builtinsErrorText (getLoc f) "field subtraction has the wrong type signature" -checkFieldMul :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldMul :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldMul f = do - field_ <- getBuiltinName (getLoc f) BuiltinField + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField unless (f ^. axiomType === (field_ --> field_ --> field_)) $ builtinsErrorText (getLoc f) "field multiplication has the wrong type signature" -checkFieldDiv :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldDiv :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldDiv f = do - field_ <- getBuiltinName (getLoc f) BuiltinField + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField unless (f ^. axiomType === (field_ --> field_ --> field_)) $ builtinsErrorText (getLoc f) "field division has the wrong type signature" -checkFieldFromInt :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldFromInt :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldFromInt f = do - field_ <- getBuiltinName (getLoc f) BuiltinField - int_ <- getBuiltinName (getLoc f) BuiltinInt + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField + int_ <- getBuiltinNameScoper (getLoc f) BuiltinInt unless (f ^. axiomType === (int_ --> field_)) $ builtinsErrorText (getLoc f) "integer to field conversion has the wrong type signature" -checkFieldToNat :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkFieldToNat :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkFieldToNat f = do - field_ <- getBuiltinName (getLoc f) BuiltinField - nat_ <- getBuiltinName (getLoc f) BuiltinNat + field_ <- getBuiltinNameScoper (getLoc f) BuiltinField + nat_ <- getBuiltinNameScoper (getLoc f) BuiltinNat unless (f ^. axiomType === (field_ --> nat_)) $ builtinsErrorText (getLoc f) "field to nat conversion has the wrong type signature" diff --git a/src/Juvix/Compiler/Builtins/IO.hs b/src/Juvix/Compiler/Builtins/IO.hs index 26c49b4ef7..81b66ca791 100644 --- a/src/Juvix/Compiler/Builtins/IO.hs +++ b/src/Juvix/Compiler/Builtins/IO.hs @@ -4,13 +4,13 @@ import Juvix.Compiler.Internal.Builtins import Juvix.Compiler.Internal.Extra import Juvix.Prelude -checkIO :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkIO :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkIO d = unless (isSmallUniverse' (d ^. axiomType)) $ builtinsErrorText (getLoc d) "IO should be in the small universe" -checkIOSequence :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkIOSequence :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkIOSequence d = do - io <- getBuiltinName (getLoc d) BuiltinIO + io <- getBuiltinNameScoper (getLoc d) BuiltinIO unless (d ^. axiomType === (io --> io --> io)) $ builtinsErrorText (getLoc d) "IO sequence has type IO → IO" diff --git a/src/Juvix/Compiler/Builtins/Int.hs b/src/Juvix/Compiler/Builtins/Int.hs index 0df90ab7dc..c23b04c2fd 100644 --- a/src/Juvix/Compiler/Builtins/Int.hs +++ b/src/Juvix/Compiler/Builtins/Int.hs @@ -4,7 +4,7 @@ import Juvix.Compiler.Internal.Builtins import Juvix.Compiler.Internal.Extra import Juvix.Prelude -checkIntDef :: (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r () +checkIntDef :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () checkIntDef d = do let err msg = builtinsErrorText (getLoc d) msg unless (null (d ^. inductiveParameters)) (err "Int should have no type parameters") @@ -13,24 +13,24 @@ checkIntDef d = do [c1, c2] -> checkIntCtor BuiltinIntOfNat c1 >> checkIntCtor BuiltinIntNegSuc c2 _ -> err "Int should have exactly two constructors" -checkIntCtor :: (Members '[Builtins, Error BuiltinsError] r) => BuiltinConstructor -> ConstructorDef -> Sem r () +checkIntCtor :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => BuiltinConstructor -> ConstructorDef -> Sem r () checkIntCtor _ctor d@ConstructorDef {..} = do let ctorName = _inductiveConstructorName ty = _inductiveConstructorType loc = getLoc d - int <- getBuiltinName loc BuiltinInt - nat <- getBuiltinName loc BuiltinNat + int <- getBuiltinNameScoper loc BuiltinInt + nat <- getBuiltinNameScoper loc BuiltinNat unless (ty === (nat --> int)) $ builtinsErrorText (getLoc d) (ctorName ^. nameText <> " has the wrong type") -checkIntToString :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkIntToString :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkIntToString f = do - string_ <- getBuiltinName (getLoc f) BuiltinString - int <- getBuiltinName (getLoc f) BuiltinInt + string_ <- getBuiltinNameScoper (getLoc f) BuiltinString + int <- getBuiltinNameScoper (getLoc f) BuiltinInt unless (f ^. axiomType === (int --> string_)) $ builtinsErrorText (getLoc f) "intToString has the wrong type signature" -checkIntEq :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntEq :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntEq f = do int <- builtinName BuiltinInt ofNat <- toExpression <$> builtinName BuiltinIntOfNat @@ -65,25 +65,25 @@ checkIntEq f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntSubNat :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntSubNat :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntSubNat f = do let loc = getLoc f - int <- getBuiltinName loc BuiltinInt - nat <- getBuiltinName loc BuiltinNat + int <- getBuiltinNameScoper loc BuiltinInt + nat <- getBuiltinNameScoper loc BuiltinNat unless (f ^. funDefType === (nat --> nat --> int)) $ builtinsErrorText (getLoc f) "int-sub-nat has the wrong type signature" -checkIntPlus :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntPlus :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntPlus f = do let loc = getLoc f - int <- getBuiltinName loc BuiltinInt - ofNat <- toExpression <$> getBuiltinName loc BuiltinIntOfNat - negSuc <- toExpression <$> getBuiltinName loc BuiltinIntNegSuc - suc <- toExpression <$> getBuiltinName loc BuiltinNatSuc - natPlus <- toExpression <$> getBuiltinName loc BuiltinNatPlus - intSubNat <- toExpression <$> getBuiltinName loc BuiltinIntSubNat + int <- getBuiltinNameScoper loc BuiltinInt + ofNat <- toExpression <$> getBuiltinNameScoper loc BuiltinIntOfNat + negSuc <- toExpression <$> getBuiltinNameScoper loc BuiltinIntNegSuc + suc <- toExpression <$> getBuiltinNameScoper loc BuiltinNatSuc + natPlus <- toExpression <$> getBuiltinNameScoper loc BuiltinNatPlus + intSubNat <- toExpression <$> getBuiltinNameScoper loc BuiltinIntSubNat let plus = f ^. funDefName l = getLoc f varn <- freshVar l "m" @@ -109,7 +109,7 @@ checkIntPlus f = do _funInfoFreeTypeVars = [] } -checkIntNegNat :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntNegNat :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntNegNat f = do int <- builtinName BuiltinInt nat <- builtinName BuiltinNat @@ -137,9 +137,9 @@ checkIntNegNat f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntNeg :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntNeg :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntNeg f = do int <- builtinName BuiltinInt ofNat <- toExpression <$> builtinName BuiltinIntOfNat @@ -166,9 +166,9 @@ checkIntNeg f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntMul :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntMul :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntMul f = do int <- builtinName BuiltinInt ofNat <- toExpression <$> builtinName BuiltinIntOfNat @@ -200,9 +200,9 @@ checkIntMul f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntDiv :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntDiv :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntDiv f = do int <- builtinName BuiltinInt ofNat <- toExpression <$> builtinName BuiltinIntOfNat @@ -234,9 +234,9 @@ checkIntDiv f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntMod :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntMod :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntMod f = do int <- builtinName BuiltinInt ofNat <- toExpression <$> builtinName BuiltinIntOfNat @@ -268,9 +268,9 @@ checkIntMod f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntSub :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntSub :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntSub f = do int <- builtinName BuiltinInt neg <- toExpression <$> builtinName BuiltinIntNeg @@ -296,9 +296,9 @@ checkIntSub f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntNonNeg :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntNonNeg :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntNonNeg f = do int <- builtinName BuiltinInt bool_ <- builtinName BuiltinBool @@ -328,16 +328,16 @@ checkIntNonNeg f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntPrint :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkIntPrint :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkIntPrint f = do - int <- getBuiltinName (getLoc f) BuiltinInt - io <- getBuiltinName (getLoc f) BuiltinIO + int <- getBuiltinNameScoper (getLoc f) BuiltinInt + io <- getBuiltinNameScoper (getLoc f) BuiltinIO unless (f ^. axiomType === (int --> io)) $ builtinsErrorText (getLoc f) "Int print has the wrong type signature" -checkIntLe :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntLe :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntLe f = do int <- builtinName BuiltinInt bool_ <- builtinName BuiltinBool @@ -365,15 +365,15 @@ checkIntLe f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) -checkIntLt :: forall r. (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkIntLt :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkIntLt f = do int <- builtinName BuiltinInt bool_ <- builtinName BuiltinBool ofNat <- toExpression <$> builtinName BuiltinIntOfNat - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero intLe <- toExpression <$> builtinName BuiltinIntLe intPlus <- toExpression <$> builtinName BuiltinIntPlus let l = getLoc f @@ -401,7 +401,7 @@ checkIntLt f = do } where builtinName :: (IsBuiltin a) => a -> Sem r Name - builtinName = getBuiltinName (getLoc f) + builtinName = getBuiltinNameScoper (getLoc f) checkFromInt :: FunctionDef -> Sem r () checkFromInt = const (return ()) diff --git a/src/Juvix/Compiler/Builtins/List.hs b/src/Juvix/Compiler/Builtins/List.hs index ade75342f6..7caf2a619f 100644 --- a/src/Juvix/Compiler/Builtins/List.hs +++ b/src/Juvix/Compiler/Builtins/List.hs @@ -5,7 +5,7 @@ import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty import Juvix.Prelude -checkListDef :: forall r. (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r () +checkListDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () checkListDef d = do let err :: forall a. Text -> Sem r a err = builtinsErrorText (getLoc d) @@ -18,18 +18,18 @@ checkListDef d = do [c1, c2] -> checkNil param c1 >> checkCons param c2 _ -> err "List should have exactly two constructors" -checkNil :: (Members '[Builtins, Error BuiltinsError] r) => VarName -> ConstructorDef -> Sem r () +checkNil :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => VarName -> ConstructorDef -> Sem r () checkNil a d@ConstructorDef {..} = do let ty = _inductiveConstructorType - list_ <- getBuiltinName (getLoc d) BuiltinList + list_ <- getBuiltinNameScoper (getLoc d) BuiltinList let nilty = list_ @@ a unless (ty === nilty) $ builtinsErrorMsg (getLoc d) ("nil has the wrong type " <> ppOutDefault ty <> " | " <> ppOutDefault nilty) -checkCons :: (Members '[Builtins, Error BuiltinsError] r) => VarName -> ConstructorDef -> Sem r () +checkCons :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => VarName -> ConstructorDef -> Sem r () checkCons a d@ConstructorDef {..} = do let ty = _inductiveConstructorType - list_ <- getBuiltinName (getLoc d) BuiltinList + list_ <- getBuiltinNameScoper (getLoc d) BuiltinList let consty = a --> list_ @@ a --> list_ @@ a unless (ty === consty) $ builtinsErrorText (getLoc d) "cons has the wrong type" diff --git a/src/Juvix/Compiler/Builtins/Maybe.hs b/src/Juvix/Compiler/Builtins/Maybe.hs index fb208aa3a5..5ca0d48284 100644 --- a/src/Juvix/Compiler/Builtins/Maybe.hs +++ b/src/Juvix/Compiler/Builtins/Maybe.hs @@ -5,7 +5,7 @@ import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty import Juvix.Prelude -checkMaybeDef :: forall r. (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r () +checkMaybeDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () checkMaybeDef d = do let err :: forall a. Text -> Sem r a err = builtinsErrorText (getLoc d) @@ -17,19 +17,19 @@ checkMaybeDef d = do [c1, c2] -> checkNothing param c1 >> checkJust param c2 _ -> err "Maybe should have exactly two constructors" -checkNothing :: (Members '[Builtins, Error BuiltinsError] r) => VarName -> ConstructorDef -> Sem r () +checkNothing :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => VarName -> ConstructorDef -> Sem r () checkNothing a d@ConstructorDef {..} = do let ty = _inductiveConstructorType - maybe_ <- getBuiltinName (getLoc d) BuiltinMaybe + maybe_ <- getBuiltinNameScoper (getLoc d) BuiltinMaybe let nothingty = maybe_ @@ a unless (ty === nothingty) $ builtinsErrorMsg (getLoc d) $ "nothing has the wrong type " <> ppOutDefault ty <> " | " <> ppOutDefault nothingty -checkJust :: (Members '[Builtins, Error BuiltinsError] r) => VarName -> ConstructorDef -> Sem r () +checkJust :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => VarName -> ConstructorDef -> Sem r () checkJust a d@ConstructorDef {..} = do let ty = _inductiveConstructorType - maybe_ <- getBuiltinName (getLoc d) BuiltinMaybe + maybe_ <- getBuiltinNameScoper (getLoc d) BuiltinMaybe let justty = a --> maybe_ @@ a unless (ty === justty) $ builtinsErrorText (getLoc d) "just has the wrong type" diff --git a/src/Juvix/Compiler/Builtins/Nat.hs b/src/Juvix/Compiler/Builtins/Nat.hs index 6dc4b90f32..0fde2f0360 100644 --- a/src/Juvix/Compiler/Builtins/Nat.hs +++ b/src/Juvix/Compiler/Builtins/Nat.hs @@ -6,7 +6,7 @@ import Juvix.Compiler.Internal.Pretty import Juvix.Data.Effect.NameIdGen import Juvix.Prelude -checkNatDef :: forall r. (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r () +checkNatDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () checkNatDef d = do let err :: forall a. Text -> Sem r a err = builtinsErrorText (getLoc d) @@ -16,33 +16,33 @@ checkNatDef d = do [c1, c2] -> checkZero c1 >> checkSuc c2 _ -> err "Nat numbers should have exactly two constructors" -checkZero :: (Members '[Builtins, Error BuiltinsError] r) => ConstructorDef -> Sem r () +checkZero :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r () checkZero d@ConstructorDef {..} = do let ty = _inductiveConstructorType - nat <- getBuiltinName (getLoc d) BuiltinNat + nat <- getBuiltinNameScoper (getLoc d) BuiltinNat unless (ty === nat) $ builtinsErrorMsg (getLoc d) $ "zero has the wrong type " <> ppOutDefault ty <> " | " <> ppOutDefault nat -checkSuc :: (Members '[Builtins, Error BuiltinsError] r) => ConstructorDef -> Sem r () +checkSuc :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => ConstructorDef -> Sem r () checkSuc d@ConstructorDef {..} = do let ty = _inductiveConstructorType - nat <- getBuiltinName (getLoc d) BuiltinNat + nat <- getBuiltinNameScoper (getLoc d) BuiltinNat unless (ty === (nat --> nat)) $ builtinsErrorText (getLoc d) "suc has the wrong type" -checkNatPrint :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkNatPrint :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkNatPrint f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - io <- getBuiltinName (getLoc f) BuiltinIO + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + io <- getBuiltinNameScoper (getLoc f) BuiltinIO unless (f ^. axiomType === (nat --> io)) $ builtinsErrorText (getLoc f) "Nat print has the wrong type signature" -checkNatPlus :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatPlus :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatPlus f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc let plus = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -66,12 +66,12 @@ checkNatPlus f = do _funInfoFreeTypeVars = [] } -checkNatMul :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatMul :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatMul f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - plus <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatPlus + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + plus <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatPlus let mul = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -96,11 +96,11 @@ checkNatMul f = do _funInfoFreeTypeVars = [] } -checkNatSub :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatSub :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatSub f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc let sub = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -126,12 +126,12 @@ checkNatSub f = do _funInfoFreeTypeVars = [] } -checkNatUDiv :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatUDiv :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatUDiv f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - sub <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSub + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + sub <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSub let divop = f ^. funDefName l = getLoc l varn <- freshVar l "n" @@ -156,12 +156,12 @@ checkNatUDiv f = do _funInfoFreeTypeVars = [] } -checkNatDiv :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatDiv :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatDiv f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - udiv <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatUDiv - sub <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSub + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + udiv <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatUDiv + sub <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSub let divop = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -184,12 +184,12 @@ checkNatDiv f = do _funInfoFreeTypeVars = [] } -checkNatMod :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatMod :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatMod f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - sub <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSub - divop <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatDiv - mul <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatMul + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + sub <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSub + divop <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatDiv + mul <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatMul let modop = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -209,14 +209,14 @@ checkNatMod f = do _funInfoFreeTypeVars = [] } -checkNatLe :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatLe :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatLe f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - tybool <- getBuiltinName (getLoc f) BuiltinBool - true <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue - false <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + tybool <- getBuiltinNameScoper (getLoc f) BuiltinBool + true <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolTrue + false <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolFalse let le = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -242,12 +242,12 @@ checkNatLe f = do _funInfoFreeTypeVars = [] } -checkNatLt :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatLt :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatLt f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - le <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatLe - tybool <- getBuiltinName (getLoc f) BuiltinBool + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + le <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatLe + tybool <- getBuiltinNameScoper (getLoc f) BuiltinBool let lt = f ^. funDefName l = getLoc f varn <- freshVar l "n" @@ -268,14 +268,14 @@ checkNatLt f = do _funInfoFreeTypeVars = [] } -checkNatEq :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => FunctionDef -> Sem r () +checkNatEq :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => FunctionDef -> Sem r () checkNatEq f = do - nat <- getBuiltinName (getLoc f) BuiltinNat - zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero - suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc - tybool <- getBuiltinName (getLoc f) BuiltinBool - true <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue - false <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat + zero <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatZero + suc <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinNatSuc + tybool <- getBuiltinNameScoper (getLoc f) BuiltinBool + true <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolTrue + false <- toExpression <$> getBuiltinNameScoper (getLoc f) BuiltinBoolFalse let eq = f ^. funDefName l = getLoc f varn <- freshVar l "n" diff --git a/src/Juvix/Compiler/Builtins/Pair.hs b/src/Juvix/Compiler/Builtins/Pair.hs index 310480d5e1..1421cc24a9 100644 --- a/src/Juvix/Compiler/Builtins/Pair.hs +++ b/src/Juvix/Compiler/Builtins/Pair.hs @@ -5,7 +5,7 @@ import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty import Juvix.Prelude -checkPairDef :: (Members '[Builtins, Error BuiltinsError] r) => InductiveDef -> Sem r () +checkPairDef :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r () checkPairDef d = do unless (isSmallUniverse' (d ^. inductiveType)) (error "Pair should be in the small universe") (p1, p2) <- case d ^. inductiveParameters of @@ -15,10 +15,10 @@ checkPairDef d = do [c] -> checkPairConstr p1 p2 c _ -> builtinsErrorText (getLoc d) "Pair should have exactly one constructor" -checkPairConstr :: (Members '[Builtins, Error BuiltinsError] r) => VarName -> VarName -> ConstructorDef -> Sem r () +checkPairConstr :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => VarName -> VarName -> ConstructorDef -> Sem r () checkPairConstr a b d@ConstructorDef {..} = do let ty = _inductiveConstructorType - pair_ <- getBuiltinName (getLoc d) BuiltinPair + pair_ <- getBuiltinNameScoper (getLoc d) BuiltinPair let prty = a --> b --> pair_ @@ a @@ b unless (ty === prty) $ builtinsErrorMsg (getLoc d) $ diff --git a/src/Juvix/Compiler/Builtins/String.hs b/src/Juvix/Compiler/Builtins/String.hs index ff3918384a..cd763f7ded 100644 --- a/src/Juvix/Compiler/Builtins/String.hs +++ b/src/Juvix/Compiler/Builtins/String.hs @@ -4,48 +4,48 @@ import Juvix.Compiler.Internal.Builtins import Juvix.Compiler.Internal.Extra import Juvix.Prelude -checkString :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkString :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r () checkString d = do unless (isSmallUniverse' (d ^. axiomType)) $ builtinsErrorText (getLoc d) "String should be in the small universe" -checkStringPrint :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkStringPrint :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkStringPrint f = do - string_ <- getBuiltinName (getLoc f) BuiltinString - io <- getBuiltinName (getLoc f) BuiltinIO + string_ <- getBuiltinNameScoper (getLoc f) BuiltinString + io <- getBuiltinNameScoper (getLoc f) BuiltinIO unless (f ^. axiomType === (string_ --> io)) $ builtinsErrorText (getLoc f) "String print has the wrong type signature" -checkIOReadline :: (Members '[Builtins, Error BuiltinsError, NameIdGen] r) => AxiomDef -> Sem r () +checkIOReadline :: (Members '[Reader BuiltinsTable, Error ScoperError, NameIdGen] r) => AxiomDef -> Sem r () checkIOReadline d = do - string_ <- getBuiltinName (getLoc d) BuiltinString - io <- getBuiltinName (getLoc d) BuiltinIO + string_ <- getBuiltinNameScoper (getLoc d) BuiltinString + io <- getBuiltinNameScoper (getLoc d) BuiltinIO unless (((string_ --> io) --> io) === d ^. axiomType) $ builtinsErrorText (getLoc d) "readline must be of type (string -> IO) -> IO" -checkNatToString :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkNatToString :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkNatToString f = do - string_ <- getBuiltinName (getLoc f) BuiltinString - nat <- getBuiltinName (getLoc f) BuiltinNat + string_ <- getBuiltinNameScoper (getLoc f) BuiltinString + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat unless (f ^. axiomType === (nat --> string_)) $ builtinsErrorText (getLoc f) "natToString has the wrong type signature" -checkStringToNat :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkStringToNat :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkStringToNat f = do - string_ <- getBuiltinName (getLoc f) BuiltinString - nat <- getBuiltinName (getLoc f) BuiltinNat + string_ <- getBuiltinNameScoper (getLoc f) BuiltinString + nat <- getBuiltinNameScoper (getLoc f) BuiltinNat unless (f ^. axiomType === (string_ --> nat)) $ builtinsErrorText (getLoc f) "stringToNat has the wrong type signature" -checkStringConcat :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkStringConcat :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkStringConcat f = do - string_ <- getBuiltinName (getLoc f) BuiltinString + string_ <- getBuiltinNameScoper (getLoc f) BuiltinString unless (f ^. axiomType === (string_ --> string_ --> string_)) $ builtinsErrorText (getLoc f) "++str has the wrong type signature" -checkStringEq :: (Members '[Builtins, Error BuiltinsError] r) => AxiomDef -> Sem r () +checkStringEq :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r () checkStringEq f = do - string_ <- getBuiltinName (getLoc f) BuiltinString - bool_ <- getBuiltinName (getLoc f) BuiltinBool + string_ <- getBuiltinNameScoper (getLoc f) BuiltinString + bool_ <- getBuiltinNameScoper (getLoc f) BuiltinBool unless (f ^. axiomType === (string_ --> string_ --> bool_)) $ builtinsErrorText (getLoc f) "string equality has the wrong type signature" diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index a84c085502..373ae63c14 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -6,7 +6,7 @@ import Juvix.Compiler.Concrete.Data.Highlight.Input import Juvix.Compiler.Concrete.Data.Scope import Juvix.Compiler.Concrete.Data.ScopedName import Juvix.Compiler.Concrete.Data.ScopedName qualified as S -import Juvix.Compiler.Concrete.Language +import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Store.Scoped.Language import Juvix.Prelude @@ -28,14 +28,21 @@ data InfoTableBuilder :: Effect where RegisterRecordInfo :: S.NameId -> RecordInfo -> InfoTableBuilder m () RegisterAlias :: S.NameId -> PreSymbolEntry -> InfoTableBuilder m () GetInfoTable :: InfoTableBuilder m InfoTable + GetBuiltinSymbol' :: Interval -> BuiltinPrim -> InfoTableBuilder m S.Symbol + RegisterBuiltin' :: BuiltinPrim -> S.Symbol -> InfoTableBuilder m () makeSem ''InfoTableBuilder +registerBuiltin :: (IsBuiltin a, Member InfoTableBuilder r) => a -> S.Symbol -> Sem r () +registerBuiltin = registerBuiltin' . toBuiltinPrim + +getBuiltinSymbol :: (IsBuiltin a, Member InfoTableBuilder r) => Interval -> a -> Sem r S.Symbol +getBuiltinSymbol i = getBuiltinSymbol' i . toBuiltinPrim + registerDoc :: forall r. (Members '[HighlightBuilder, State InfoTable] r) => NameId -> Maybe (Judoc 'Scoped) -> Sem r () -registerDoc k md = do - modify (set (highlightDoc . at k) md) +registerDoc k md = modify (set (highlightDoc . at k) md) -runInfoTableBuilder :: (Member HighlightBuilder r) => InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a) +runInfoTableBuilder :: (Members '[Error ScoperError, HighlightBuilder] r) => InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a) runInfoTableBuilder ini = reinterpret (runState ini) $ \case RegisterAxiom d -> let j = d ^. axiomDoc @@ -87,11 +94,35 @@ runInfoTableBuilder ini = reinterpret (runState ini) $ \case modify (over infoScoperAlias (HashMap.insert uid a)) GetInfoTable -> get + GetBuiltinSymbol' i b -> fromMaybeM notDefined (gets (^. infoBuiltins . at b)) + where + notDefined :: forall r' x. (Members '[Error ScoperError] r') => Sem r' x + notDefined = + throw $ + ErrBuiltinNotDefined + BuiltinNotDefined + { _notDefinedBuiltin = b, + _notDefinedLoc = i + } + RegisterBuiltin' b n -> do + s <- gets (^. infoBuiltins . at b) + case s of + Nothing -> modify (set (infoBuiltins . at b) (Just n)) + Just {} -> alreadyDefined + where + alreadyDefined :: forall r' x. (Members '[Error ScoperError] r') => Sem r' x + alreadyDefined = + throw $ + ErrBuiltinAlreadyDefined + BuiltinAlreadyDefined + { _builtinAlreadyDefined = b, + _builtinAlreadyDefinedLoc = getLoc n + } -runInfoTableBuilderRepl :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a) +runInfoTableBuilderRepl :: (Members '[Error ScoperError] r) => InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a) runInfoTableBuilderRepl tab = ignoreHighlightBuilder . runInfoTableBuilder tab . raiseUnder -ignoreInfoTableBuilder :: (Member HighlightBuilder r) => Sem (InfoTableBuilder ': r) a -> Sem r a +ignoreInfoTableBuilder :: (Members '[Error ScoperError, HighlightBuilder] r) => Sem (InfoTableBuilder ': r) a -> Sem r a ignoreInfoTableBuilder = fmap snd . runInfoTableBuilder mempty anameFromScopedIden :: ScopedIden -> AName diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 3d94853389..24fa82676f 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -10,7 +10,6 @@ import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Data.List.NonEmpty qualified as NonEmpty import GHC.Base (maxInt, minInt) -import Juvix.Compiler.Builtins.Effect import Juvix.Compiler.Concrete.Data.Highlight.Input import Juvix.Compiler.Concrete.Data.InfoTableBuilder import Juvix.Compiler.Concrete.Data.Name qualified as N @@ -39,7 +38,6 @@ scopeCheck :: Sem r ScoperResult scopeCheck pkg importMap pr = mapError (JuvixError @ScoperError) - . mapError (JuvixError @BuiltinsError) . runReader pkg $ scopeCheck' importMap pr m where @@ -59,7 +57,7 @@ iniScoperState tab = } scopeCheck' :: - (Members '[HighlightBuilder, Error BuiltinsError, Error ScoperError, NameIdGen, Reader Package] r) => + (Members '[HighlightBuilder, Error ScoperError, NameIdGen, Reader Package] r) => ScopedModuleTable -> Parser.ParserResult -> Module 'Parsed 'ModuleTop -> @@ -94,9 +92,9 @@ scopeCheck' importTab pr m = do scopeCheckRepl :: forall r a b. - (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState, Builtins] r) => + (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState] r) => ( forall r'. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader BindingStrategy, Reader Package, Builtins] r') => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader BindingStrategy, Reader Package] r') => a -> Sem r' b ) -> @@ -124,7 +122,7 @@ scopeCheckRepl check importTab tab a = mapError (JuvixError @ScoperError) $ do -- TODO refactor to have less code duplication scopeCheckExpressionAtoms :: forall r. - (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState, Builtins] r) => + (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState] r) => ScopedModuleTable -> InfoTable -> ExpressionAtoms 'Parsed -> @@ -133,7 +131,7 @@ scopeCheckExpressionAtoms = scopeCheckRepl checkExpressionAtoms scopeCheckExpression :: forall r. - (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState, Builtins] r) => + (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState] r) => ScopedModuleTable -> InfoTable -> ExpressionAtoms 'Parsed -> @@ -142,7 +140,7 @@ scopeCheckExpression = scopeCheckRepl checkParseExpressionAtoms scopeCheckImport :: forall r. - (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState, Builtins] r) => + (Members '[Error JuvixError, NameIdGen, Reader Package, State Scope, State ScoperState] r) => ScopedModuleTable -> InfoTable -> Import 'Parsed -> @@ -161,7 +159,7 @@ freshVariable = freshSymbol KNameLocal KNameLocal checkProjectionDef :: forall r. - (Members '[Error ScoperError, InfoTableBuilder, Reader Package, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax, Builtins] r) => + (Members '[Error ScoperError, InfoTableBuilder, Reader Package, Reader ScopeParameters, Reader InfoTable, Reader BindingStrategy, State Scope, State ScoperState, NameIdGen, State ScoperSyntax] r) => ProjectionDef 'Parsed -> Sem r (ProjectionDef 'Scoped) checkProjectionDef p = do @@ -217,7 +215,7 @@ freshSymbol _nameKind _nameKindPretty _nameConcrete = do reserveSymbolSignatureOfNameSpace :: forall r d ns. - ( Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r, + ( Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r, HasNameSignature 'Parsed d, SingI ns ) => @@ -234,7 +232,7 @@ reserveSymbolSignatureOfNameSpace ns kind kindPretty d builtin s = do reserveSymbolSignatureOf :: forall (k :: NameKind) r d. - ( Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r, + ( Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r, HasNameSignature 'Parsed d, SingI (NameKindNameSpace k) ) => @@ -276,7 +274,6 @@ reserveSymbolOfNameSpace :: State ScoperState, Reader BindingStrategy, InfoTableBuilder, - Builtins, Reader InfoTable ] r, @@ -347,8 +344,7 @@ reserveSymbolOf :: State ScoperState, Reader BindingStrategy, InfoTableBuilder, - Reader InfoTable, - Builtins + Reader InfoTable ] r, SingI (NameKindNameSpace nameKind) @@ -380,13 +376,13 @@ ignoreSyntax = evalState emptyScoperSyntax -- | Variables are assumed to never be infix operators bindVariableSymbol :: - (Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState] r) => Symbol -> Sem r S.Symbol bindVariableSymbol = localBindings . ignoreSyntax . reserveSymbolOf SKNameLocal Nothing Nothing reserveInductiveSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => InductiveDef 'Parsed -> Sem r S.Symbol reserveInductiveSymbol d = @@ -397,7 +393,7 @@ reserveInductiveSymbol d = (d ^. inductiveName) reserveAliasSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, State ScoperState, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, State ScoperState] r) => AliasDef 'Parsed -> Sem r S.Symbol reserveAliasSymbol a = do @@ -406,7 +402,7 @@ reserveAliasSymbol a = do return (set S.nameDefined locAliasDef s) reserveProjectionSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, State ScoperState, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, State ScoperState] r) => ProjectionDef 'Parsed -> Sem r S.Symbol reserveProjectionSymbol d = @@ -417,7 +413,7 @@ reserveProjectionSymbol d = (d ^. projectionField) reserveConstructorSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => InductiveDef 'Parsed -> ConstructorDef 'Parsed -> Maybe BuiltinConstructor -> @@ -426,14 +422,14 @@ reserveConstructorSymbol d c b = do reserveSymbolSignatureOf SKNameConstructor (d, c) (toBuiltinPrim <$> b) (c ^. constructorName) reserveFunctionSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => FunctionDef 'Parsed -> Sem r S.Symbol reserveFunctionSymbol f = reserveSymbolSignatureOf SKNameFunction f (toBuiltinPrim <$> f ^. signBuiltin) (f ^. signName) reserveAxiomSymbol :: - (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r) => + (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => AxiomDef 'Parsed -> Sem r S.Symbol reserveAxiomSymbol a = @@ -488,8 +484,7 @@ checkImport :: Reader InfoTable, NameIdGen, Reader BindingStrategy, - Reader Package, - Builtins + Reader Package ] r ) => @@ -511,8 +506,7 @@ checkImportPublic :: NameIdGen, HighlightBuilder, Reader BindingStrategy, - Reader Package, - Builtins + Reader Package ] r ) => @@ -947,7 +941,7 @@ getModuleId path = do checkFixitySyntaxDef :: forall r. - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, State ScoperSyntax, NameIdGen, InfoTableBuilder, Reader InfoTable, Reader Package, Builtins] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, State ScoperSyntax, NameIdGen, InfoTableBuilder, Reader InfoTable, Reader Package] r) => FixitySyntaxDef 'Parsed -> Sem r (FixitySyntaxDef 'Scoped) checkFixitySyntaxDef FixitySyntaxDef {..} = topBindings $ do @@ -967,7 +961,7 @@ checkFixitySyntaxDef FixitySyntaxDef {..} = topBindings $ do resolveFixitySyntaxDef :: forall r. - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, State ScoperSyntax, NameIdGen, InfoTableBuilder, Reader InfoTable, Builtins] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, State ScoperSyntax, NameIdGen, InfoTableBuilder, Reader InfoTable] r) => FixitySyntaxDef 'Parsed -> Sem r () resolveFixitySyntaxDef fdef@FixitySyntaxDef {..} = topBindings $ do @@ -1081,7 +1075,7 @@ resolveIteratorSyntaxDef s@IteratorSyntaxDef {..} = do checkFunctionDef :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, State ScoperSyntax, Reader BindingStrategy, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, State ScoperSyntax, Reader BindingStrategy] r) => FunctionDef 'Parsed -> Sem r (FunctionDef 'Scoped) checkFunctionDef FunctionDef {..} = do @@ -1148,7 +1142,7 @@ checkFunctionDef FunctionDef {..} = do checkInductiveParameters :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => InductiveParameters 'Parsed -> Sem r (InductiveParameters 'Scoped) checkInductiveParameters params = do @@ -1164,7 +1158,7 @@ checkInductiveParameters params = do checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, State ScoperSyntax, Reader BindingStrategy, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, State ScoperSyntax, Reader BindingStrategy] r) => InductiveDef 'Parsed -> Sem r (InductiveDef 'Scoped) checkInductiveDef InductiveDef {..} = do @@ -1288,7 +1282,7 @@ localBindings = runReader BindingLocal checkTopModule :: forall r. - (Members '[HighlightBuilder, Error BuiltinsError, Error ScoperError, Reader ScopeParameters, State ScoperState, Reader InfoTable, NameIdGen, Reader Package] r) => + (Members '[HighlightBuilder, Error ScoperError, Reader ScopeParameters, State ScoperState, Reader InfoTable, NameIdGen, Reader Package] r) => Module 'Parsed 'ModuleTop -> Sem r (Module 'Scoped 'ModuleTop, ScopedModule, Scope) checkTopModule m@Module {..} = checkedModule @@ -1322,18 +1316,15 @@ checkTopModule m@Module {..} = checkedModule checkedModule :: Sem r (Module 'Scoped 'ModuleTop, ScopedModule, Scope) checkedModule = do ( sc :: Scope, - ( tab0 :: InfoTable, - ( builtins :: BuiltinsTable, - ( e :: ExportInfo, - body' :: [Statement 'Scoped], - path' :: S.TopModulePath, - doc' :: Maybe (Judoc 'Scoped) - ) + ( tab :: InfoTable, + ( e :: ExportInfo, + body' :: [Statement 'Scoped], + path' :: S.TopModulePath, + doc' :: Maybe (Judoc 'Scoped) ) ) ) <- runState iniScope . runInfoTableBuilder mempty - . runBuiltins mempty $ do path' <- freshTopModulePath withTopScope $ do @@ -1343,8 +1334,7 @@ checkTopModule m@Module {..} = checkedModule return (e, body', path', doc') localModules <- getLocalModules e _moduleId <- getModuleId (topModulePathKey (path' ^. S.nameConcrete)) - let tab = set infoBuiltins builtins tab0 - md = + let md = Module { _modulePath = path', _moduleBody = body', @@ -1409,7 +1399,7 @@ syntaxBlock m = checkModuleBody :: forall r. - (Members '[HighlightBuilder, InfoTableBuilder, Reader InfoTable, Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, NameIdGen, Reader Package, Reader BindingStrategy, Builtins] r) => + (Members '[HighlightBuilder, InfoTableBuilder, Reader InfoTable, Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, NameIdGen, Reader Package, Reader BindingStrategy] r) => [Statement 'Parsed] -> Sem r (ExportInfo, [Statement 'Scoped]) checkModuleBody body = do @@ -1452,7 +1442,7 @@ checkModuleBody body = do checkSections :: forall r. - (Members '[HighlightBuilder, Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader Package] r) => StatementSections 'Parsed -> Sem r (StatementSections 'Scoped) checkSections sec = topBindings helper @@ -1768,7 +1758,7 @@ mkSections = \case StatementOpenModule o -> Right (NonDefinitionOpenModule o) reserveLocalModuleSymbol :: - (Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Reader BindingStrategy, Builtins] r) => + (Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Reader BindingStrategy] r) => Symbol -> Sem r S.Symbol reserveLocalModuleSymbol = @@ -1786,8 +1776,7 @@ checkLocalModule :: Reader InfoTable, NameIdGen, Reader BindingStrategy, - Reader Package, - Builtins + Reader Package ] r ) => @@ -2077,7 +2066,7 @@ filterExportInfo pub openModif = alterEntries . filterScope Nothing -> id checkAxiomDef :: - (Members '[HighlightBuilder, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperSyntax, Reader BindingStrategy, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperSyntax, Reader BindingStrategy, Reader Package] r) => AxiomDef 'Parsed -> Sem r (AxiomDef 'Scoped) checkAxiomDef AxiomDef {..} = do @@ -2093,7 +2082,7 @@ entryToSymbol sentry csym = set S.nameConcrete csym (sentry ^. nsEntry) checkFunction :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Function 'Parsed -> Sem r (Function 'Scoped) checkFunction f = do @@ -2112,7 +2101,7 @@ checkFunction f = do -- | for now functions defined in let clauses cannot be infix operators checkLetStatements :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => NonEmpty (LetStatement 'Parsed) -> Sem r (NonEmpty (LetStatement 'Scoped)) checkLetStatements = @@ -2159,7 +2148,7 @@ checkLetStatements = checkRecordPattern :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => RecordPattern 'Parsed -> Sem r (RecordPattern 'Scoped) checkRecordPattern r = do @@ -2181,7 +2170,7 @@ checkRecordPattern r = do noFields = ErrConstructorNotARecord . ConstructorNotARecord checkItem :: forall r'. - (Members '[Reader (RecordNameSignature 'Parsed), Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r') => + (Members '[Reader (RecordNameSignature 'Parsed), Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r') => RecordPatternItem 'Parsed -> Sem r' (RecordPatternItem 'Scoped) checkItem = \case @@ -2219,7 +2208,7 @@ checkRecordPattern r = do checkListPattern :: forall r. - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => ListPattern 'Parsed -> Sem r (ListPattern 'Scoped) checkListPattern l = do @@ -2230,7 +2219,7 @@ checkListPattern l = do checkList :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => List 'Parsed -> Sem r (List 'Scoped) checkList l = do @@ -2241,7 +2230,7 @@ checkList l = do checkLet :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Let 'Parsed -> Sem r (Let 'Scoped) checkLet Let {..} = @@ -2267,8 +2256,7 @@ checkRhsExpression :: InfoTableBuilder, Reader InfoTable, NameIdGen, - Reader Package, - Builtins + Reader Package ] r ) => @@ -2294,8 +2282,7 @@ checkSideIfBranch :: InfoTableBuilder, Reader InfoTable, NameIdGen, - Reader Package, - Builtins + Reader Package ] r ) => @@ -2326,8 +2313,7 @@ checkSideIfs :: InfoTableBuilder, Reader InfoTable, NameIdGen, - Reader Package, - Builtins + Reader Package ] r ) => @@ -2344,7 +2330,7 @@ checkSideIfs SideIfs {..} = do checkCaseBranchRhs :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => CaseBranchRhs 'Parsed -> Sem r (CaseBranchRhs 'Scoped) checkCaseBranchRhs = \case @@ -2353,7 +2339,7 @@ checkCaseBranchRhs = \case checkCaseBranch :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => CaseBranch 'Parsed -> Sem r (CaseBranch 'Scoped) checkCaseBranch CaseBranch {..} = withLocalScope $ do @@ -2367,7 +2353,7 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do } checkCase :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Case 'Parsed -> Sem r (Case 'Scoped) checkCase Case {..} = do @@ -2383,7 +2369,7 @@ checkCase Case {..} = do checkIfBranch :: forall r k. - (SingI k, Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (SingI k, Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => IfBranch 'Parsed k -> Sem r (IfBranch 'Scoped k) checkIfBranch IfBranch {..} = withLocalScope $ do @@ -2399,7 +2385,7 @@ checkIfBranch IfBranch {..} = withLocalScope $ do } checkIf :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => If 'Parsed -> Sem r (If 'Scoped) checkIf If {..} = do @@ -2413,7 +2399,7 @@ checkIf If {..} = do } checkLambda :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Lambda 'Parsed -> Sem r (Lambda 'Scoped) checkLambda Lambda {..} = do @@ -2426,7 +2412,7 @@ checkLambda Lambda {..} = do } checkLambdaClause :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => LambdaClause 'Parsed -> Sem r (LambdaClause 'Scoped) checkLambdaClause LambdaClause {..} = withLocalScope $ do @@ -2499,7 +2485,7 @@ resolveShadowing es = go [(e, e ^. nsEntry . S.nameWhyInScope) | e <- es] checkPatternName :: forall r. - (Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder, Reader InfoTable, Builtins] r) => + (Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder, Reader InfoTable] r) => Name -> Sem r PatternScopedIden checkPatternName n = do @@ -2553,7 +2539,7 @@ lookupNameOfKind nameKind n = do return (e, e') checkPatternBinding :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => PatternBinding -> Sem r PatternArg checkPatternBinding PatternBinding {..} = do @@ -2564,19 +2550,19 @@ checkPatternBinding PatternBinding {..} = do | otherwise -> return (set patternArgName (Just n') p') checkPatternAtoms :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => PatternAtoms 'Parsed -> Sem r (PatternAtoms 'Scoped) checkPatternAtoms (PatternAtoms s i) = (`PatternAtoms` i) <$> mapM checkPatternAtom s checkParsePatternAtoms :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => PatternAtoms 'Parsed -> Sem r PatternArg checkParsePatternAtoms = checkPatternAtoms >=> parsePatternAtoms checkPatternAtom :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => PatternAtom 'Parsed -> Sem r (PatternAtom 'Scoped) checkPatternAtom = \case @@ -2616,7 +2602,7 @@ checkScopedIden :: checkScopedIden n = checkName n >>= entryToScopedIden n checkExpressionAtom :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => ExpressionAtom 'Parsed -> Sem r (NonEmpty (ExpressionAtom 'Scoped)) checkExpressionAtom e = case e of @@ -2640,14 +2626,14 @@ checkExpressionAtom e = case e of AtomNamedApplicationNew i -> pure . AtomNamedApplicationNew <$> checkNamedApplicationNew i AtomRecordUpdate i -> pure . AtomRecordUpdate <$> checkRecordUpdate i -reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable, Builtins] r) => NamedArgumentNew 'Parsed -> Sem r () +reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgumentNew 'Parsed -> Sem r () reserveNamedArgumentName a = case a of NamedArgumentNewFunction f -> void (reserveFunctionSymbol (f ^. namedArgumentFunctionDef)) NamedArgumentItemPun {} -> return () checkNamedApplicationNew :: forall r. - (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => NamedApplicationNew 'Parsed -> Sem r (NamedApplicationNew 'Scoped) checkNamedApplicationNew napp = do @@ -2692,7 +2678,7 @@ checkNamedApplicationNew napp = do scopePun = checkScopedIden . NameUnqualified checkNamedArgumentNew :: - (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => HashMap Symbol ScopedIden -> NamedArgumentNew 'Parsed -> Sem r (NamedArgumentNew 'Scoped) @@ -2711,7 +2697,7 @@ checkNamedArgumentItemPun puns NamedArgumentPun {..} = } checkNamedArgumentFunctionDef :: - (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => NamedArgumentFunctionDef 'Parsed -> Sem r (NamedArgumentFunctionDef 'Scoped) checkNamedArgumentFunctionDef NamedArgumentFunctionDef {..} = do @@ -2721,7 +2707,7 @@ checkNamedArgumentFunctionDef NamedArgumentFunctionDef {..} = do { _namedArgumentFunctionDef = def } -checkRecordUpdate :: forall r. (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped) +checkRecordUpdate :: forall r. (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => RecordUpdate 'Parsed -> Sem r (RecordUpdate 'Scoped) checkRecordUpdate RecordUpdate {..} = do tyName' <- getNameOfKind KNameInductive _recordUpdateTypeName info <- getRecordInfo tyName' @@ -2750,7 +2736,7 @@ checkRecordUpdate RecordUpdate {..} = do return (_nameItemImplicit, v) checkUpdateField :: - (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Error ScoperError, State Scope, State ScoperState, Reader ScopeParameters, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => RecordNameSignature 'Parsed -> RecordUpdateField 'Parsed -> Sem r (RecordUpdateField 'Scoped) @@ -2770,7 +2756,7 @@ checkUpdateField sig f = do checkNamedApplication :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => NamedApplication 'Parsed -> Sem r (NamedApplication 'Scoped) checkNamedApplication napp = do @@ -2787,7 +2773,7 @@ checkNamedApplication napp = do checkNamedArgumentAssign :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => NamedArgumentAssign 'Parsed -> Sem r (NamedArgumentAssign 'Scoped) checkNamedArgumentAssign n = do @@ -2828,7 +2814,7 @@ getNameSignature s = do lookupNameSignature s' = gets (^. scoperScopedSignatures . at s') checkIterator :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Iterator 'Parsed -> Sem r (Iterator 'Scoped) checkIterator iter = do @@ -2871,7 +2857,7 @@ checkIterator iter = do return Iterator {..} checkInitializer :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Initializer 'Parsed -> Sem r (Initializer 'Scoped) checkInitializer ini = do @@ -2884,7 +2870,7 @@ checkInitializer ini = do } checkRange :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Range 'Parsed -> Sem r (Range 'Scoped) checkRange rng = do @@ -2909,7 +2895,7 @@ checkHole h = do } checkParens :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => ExpressionAtoms 'Parsed -> Sem r Expression checkParens e@(ExpressionAtoms as _) = case as of @@ -2925,13 +2911,13 @@ checkParens e@(ExpressionAtoms as _) = case as of checkExpressionAtoms :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => ExpressionAtoms 'Parsed -> Sem r (ExpressionAtoms 'Scoped) checkExpressionAtoms (ExpressionAtoms l i) = (`ExpressionAtoms` i) <$> sconcatMap checkExpressionAtom l checkJudoc :: - (Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => Judoc 'Parsed -> Sem r (Judoc 'Scoped) checkJudoc (Judoc groups) = @@ -2940,7 +2926,7 @@ checkJudoc (Judoc groups) = $ Judoc <$> mapM checkJudocGroup groups checkJudocGroup :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => JudocGroup 'Parsed -> Sem r (JudocGroup 'Scoped) checkJudocGroup = \case @@ -2948,26 +2934,26 @@ checkJudocGroup = \case JudocGroupLines l -> JudocGroupLines <$> mapM checkJudocBlock l checkJudocBlock :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => JudocBlock 'Parsed -> Sem r (JudocBlock 'Scoped) checkJudocBlock = \case JudocLines l -> JudocLines <$> mapM checkJudocLine l checkJudocBlockParagraph :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => JudocBlockParagraph 'Parsed -> Sem r (JudocBlockParagraph 'Scoped) checkJudocBlockParagraph = traverseOf judocBlockParagraphBlocks (mapM checkJudocBlock) checkJudocLine :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => JudocLine 'Parsed -> Sem r (JudocLine 'Scoped) checkJudocLine (JudocLine delim atoms) = JudocLine delim <$> mapM (mapM checkJudocAtom) atoms checkJudocAtom :: - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => JudocAtom 'Parsed -> Sem r (JudocAtom 'Scoped) checkJudocAtom = \case @@ -2976,19 +2962,19 @@ checkJudocAtom = \case checkParseExpressionAtoms :: forall r. - (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, Builtins] r) => + (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package] r) => ExpressionAtoms 'Parsed -> Sem r Expression checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms checkParsePatternAtom :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Builtins] r) => + (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen] r) => PatternAtom 'Parsed -> Sem r PatternArg checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom checkSyntaxDef :: - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, State ScoperSyntax, Builtins] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader Package, State ScoperSyntax] r) => SyntaxDef 'Parsed -> Sem r (SyntaxDef 'Scoped) checkSyntaxDef = \case @@ -3012,13 +2998,13 @@ checkAliasDef AliasDef {..} = do } reserveAliasDef :: - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader BindingStrategy, Builtins] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader BindingStrategy] r) => AliasDef 'Parsed -> Sem r () reserveAliasDef = void . reserveAliasSymbol resolveSyntaxDef :: - (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader BindingStrategy, Builtins] r) => + (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, State ScoperSyntax, Reader BindingStrategy] r) => SyntaxDef 'Parsed -> Sem r () resolveSyntaxDef = \case diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 3434c2433a..3dcd846058 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -10,7 +10,7 @@ import Juvix.Compiler.Concrete.Data.NameSignature.Error import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments.Error -import Juvix.Prelude.Base.Foundation +import Juvix.Prelude data ScoperError = ErrInfixParser InfixError @@ -56,6 +56,9 @@ data ScoperError | ErrWrongDefaultValue WrongDefaultValue | ErrUnsupported Unsupported | ErrDefaultArgCycle DefaultArgCycle + | ErrBuiltinAlreadyDefined BuiltinAlreadyDefined + | ErrBuiltinNotDefined BuiltinNotDefined + | ErrBuiltinErrorMessage BuiltinErrorMessage deriving stock (Generic) instance ToGenericError ScoperError where @@ -103,3 +106,18 @@ instance ToGenericError ScoperError where ErrWrongDefaultValue e -> genericError e ErrUnsupported e -> genericError e ErrDefaultArgCycle e -> genericError e + ErrBuiltinAlreadyDefined e -> genericError e + ErrBuiltinNotDefined e -> genericError e + ErrBuiltinErrorMessage e -> genericError e + +builtinsErrorMsg :: (Members '[Error ScoperError] r) => Interval -> AnsiText -> Sem r a +builtinsErrorMsg loc msg = + throw $ + ErrBuiltinErrorMessage + BuiltinErrorMessage + { _builtinErrorMessageLoc = loc, + _builtinErrorMessage = msg + } + +builtinsErrorText :: (Members '[Error ScoperError] r) => Interval -> Text -> Sem r a +builtinsErrorText loc = builtinsErrorMsg loc . mkAnsiText diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index ee0b28c3a6..380d4b0bde 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -16,6 +16,7 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pre import Juvix.Compiler.Concrete.Translation.ImportScanner.Base import Juvix.Compiler.Store.Scoped.Language (FixitySymbolEntry, ModuleSymbolEntry, PreSymbolEntry) import Juvix.Data.CodeAnn +import Juvix.Data.PPOutput import Juvix.Prelude data MultipleDeclarations = MultipleDeclarations @@ -1054,3 +1055,59 @@ instance ToGenericError DefaultArgCycle where where i :: Interval i = getLoc (head _defaultArgCycle) + +data BuiltinAlreadyDefined = BuiltinAlreadyDefined + { _builtinAlreadyDefined :: BuiltinPrim, + _builtinAlreadyDefinedLoc :: Interval + } + +makeLenses ''BuiltinAlreadyDefined + +instance ToGenericError BuiltinAlreadyDefined where + genericError e = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = [i] + } + where + i = e ^. builtinAlreadyDefinedLoc + msg = "The builtin" <+> code (pretty (e ^. builtinAlreadyDefined)) <+> "has already been defined" + +data BuiltinNotDefined = BuiltinNotDefined + { _notDefinedBuiltin :: BuiltinPrim, + _notDefinedLoc :: Interval + } + +makeLenses ''BuiltinNotDefined + +instance ToGenericError BuiltinNotDefined where + genericError e = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = [i] + } + where + i = e ^. notDefinedLoc + msg = "The builtin" <+> code (pretty (e ^. notDefinedBuiltin)) <+> "has not been defined" + +-- | Generic error message related to builtins +data BuiltinErrorMessage = BuiltinErrorMessage + { _builtinErrorMessage :: AnsiText, + _builtinErrorMessageLoc :: Interval + } + +instance ToGenericError BuiltinErrorMessage where + genericError BuiltinErrorMessage {..} = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = _builtinErrorMessage, + _genericErrorIntervals = [i] + } + where + i :: Interval + i = _builtinErrorMessageLoc diff --git a/src/Juvix/Compiler/Internal/Builtins.hs b/src/Juvix/Compiler/Internal/Builtins.hs index 6ea3797b1b..2cfb1ea65d 100644 --- a/src/Juvix/Compiler/Internal/Builtins.hs +++ b/src/Juvix/Compiler/Internal/Builtins.hs @@ -1,13 +1,16 @@ module Juvix.Compiler.Internal.Builtins ( module Juvix.Compiler.Internal.Builtins, - module Juvix.Compiler.Builtins.Effect, + module Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error, + BuiltinsTable, ) where -import Juvix.Compiler.Builtins.Effect hiding (getBuiltinSymbol, registerBuiltin) -import Juvix.Compiler.Builtins.Effect qualified as B +import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error (BuiltinNotDefined (..), ScoperError (ErrBuiltinNotDefined), builtinsErrorMsg, builtinsErrorText) import Juvix.Compiler.Internal.Extra import Juvix.Compiler.Internal.Pretty +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error (TypeCheckerError) +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error qualified as TypeChecker +import Juvix.Compiler.Store.Scoped.Data.InfoTable (BuiltinsTable) import Juvix.Prelude data FunInfo = FunInfo @@ -21,12 +24,40 @@ data FunInfo = FunInfo makeLenses ''FunInfo -getBuiltinName :: (IsBuiltin a, Members '[Builtins] r) => Interval -> a -> Sem r Name -getBuiltinName loc p = fromConcreteSymbol <$> (B.getBuiltinSymbol loc p) +getBuiltinNameScoper :: + (IsBuiltin a, Members '[Error ScoperError, Reader BuiltinsTable] r) => + Interval -> + a -> + Sem r Name +getBuiltinNameScoper loc = + mapError ErrBuiltinNotDefined + . getBuiltinName loc + +getBuiltinNameTypeChecker :: (IsBuiltin a, Members '[Reader BuiltinsTable, Error TypeCheckerError] r) => Interval -> a -> Sem r Name +getBuiltinNameTypeChecker loc = + mapError TypeChecker.ErrBuiltinNotDefined + . getBuiltinName loc + +getBuiltinName :: + (IsBuiltin a, Members '[Error BuiltinNotDefined, Reader BuiltinsTable] r) => + Interval -> + a -> + Sem r Name +getBuiltinName loc p = do + let b = toBuiltinPrim p + m <- asks @BuiltinsTable (^. at b) + case m of + Nothing -> + throw $ + BuiltinNotDefined + { _notDefinedBuiltin = b, + _notDefinedLoc = loc + } + Just x -> return (fromConcreteSymbol x) checkBuiltinFunctionInfo :: forall r. - (Members '[Error BuiltinsError] r) => + (Members '[Error ScoperError] r) => FunInfo -> Sem r () checkBuiltinFunctionInfo fi = do @@ -34,13 +65,7 @@ checkBuiltinFunctionInfo fi = do ty = fi ^. funInfoDef . funDefType sig = fi ^. funInfoSignature err :: forall a. AnsiText -> Sem r a - err msg = - throw $ - ErrBuiltinsErrorMessage - BuiltinsErrorMessage - { _builtinsErrorMessageLoc = getLoc (fi ^. funInfoDef), - _builtinsErrorMessage = msg - } + err = builtinsErrorMsg (getLoc (fi ^. funInfoDef)) unless ((sig ==% ty) (hashSet (fi ^. funInfoFreeTypeVars))) (err "builtin has the wrong type signature") let freeVars = hashSet (fi ^. funInfoFreeVars) a =% b = (a ==% b) freeVars diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs index 4c259d6831..9da5ee0bf2 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs @@ -72,7 +72,6 @@ fromConcrete _resultScoper = do . runReader @ExportsTable exportTbl . runReader tab . mapError (JuvixError @ScoperError) - . mapError (JuvixError @BuiltinsError) . evalState @ConstructorInfos mempty . runReader @DefaultArgsStack mempty $ goTopModule m @@ -83,8 +82,7 @@ fromConcrete _resultScoper = do fromConcreteExpression :: (Members '[Error JuvixError, NameIdGen, Termination, Reader S.InfoTable] r) => Scoper.Expression -> Sem r Internal.Expression fromConcreteExpression e = do e' <- - mapError (JuvixError @BuiltinsError) - . mapError (JuvixError @ScoperError) + mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . runReader @DefaultArgsStack mempty . goExpression @@ -149,13 +147,13 @@ buildMutualBlocks ss = do CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p) goLocalModule :: - (Members '[Reader EntryPoint, Error BuiltinsError, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => Module 'Scoped 'ModuleLocal -> Sem r [Internal.PreStatement] goLocalModule = concatMapM goAxiomInductive . (^. moduleBody) goTopModule :: - (Members '[Reader DefaultArgsStack, Error BuiltinsError, Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Termination, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Termination, Reader S.InfoTable] r) => Module 'Scoped 'ModuleTop -> Sem r Internal.Module goTopModule m = do @@ -208,7 +206,7 @@ traverseM' f x = sequence <$> traverse f x toPreModule :: forall r. - (Members '[Reader EntryPoint, Error BuiltinsError, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => Module 'Scoped 'ModuleTop -> Sem r Internal.PreModule toPreModule Module {..} = do @@ -268,7 +266,7 @@ fromPreModuleBody b = do goModuleBody :: forall r. - (Members '[Reader EntryPoint, Error BuiltinsError, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, Reader ExportsTable, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => [Statement 'Scoped] -> Sem r Internal.PreModuleBody goModuleBody stmts = do @@ -330,7 +328,7 @@ goImport Import {..} = -- | Ignores functions goAxiomInductive :: forall r. - (Members '[Reader EntryPoint, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable, Error BuiltinsError] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, Error ScoperError, NameIdGen, Reader Pragmas, State ConstructorInfos, Reader S.InfoTable] r) => Statement 'Scoped -> Sem r [Internal.PreStatement] goAxiomInductive = \case @@ -345,7 +343,7 @@ goAxiomInductive = \case goProjectionDef :: forall r. - (Members '[NameIdGen, Error ScoperError, Error BuiltinsError, State ConstructorInfos, Reader S.InfoTable] r) => + (Members '[NameIdGen, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => ProjectionDef 'Scoped -> Sem r Internal.FunctionDef goProjectionDef ProjectionDef {..} = do @@ -366,7 +364,7 @@ goProjectionDef ProjectionDef {..} = do goFunctionDef :: forall r. - (Members '[Reader DefaultArgsStack, Reader Pragmas, Error BuiltinsError, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => FunctionDef 'Scoped -> Sem r Internal.FunctionDef goFunctionDef FunctionDef {..} = do @@ -479,7 +477,7 @@ goFunctionDef FunctionDef {..} = do goInductiveParameters :: forall r. - (Members '[Reader EntryPoint, Error BuiltinsError, Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => InductiveParameters 'Scoped -> Sem r [Internal.InductiveParameter] goInductiveParameters params@InductiveParameters {..} = do @@ -498,7 +496,7 @@ goInductiveParameters params@InductiveParameters {..} = do Just rhs -> goExpression (rhs ^. inductiveParametersType) checkBuiltinInductive :: - (Members '[Error BuiltinsError, Reader S.InfoTable] r) => + (Members '[Error ScoperError, Reader S.InfoTable] r) => Internal.InductiveDef -> BuiltinInductive -> Sem r () @@ -512,13 +510,13 @@ checkBuiltinInductive d b = localBuiltins $ case b of BuiltinPoseidonState -> checkPoseidonStateDef d BuiltinEcPoint -> checkEcPointDef d -localBuiltins :: (Members '[Error BuiltinsError, Reader S.InfoTable] r) => Sem (Builtins ': r) a -> Sem r a +localBuiltins :: (Members '[Reader S.InfoTable] r) => Sem (Reader BuiltinsTable ': r) a -> Sem r a localBuiltins m = do t <- asks (^. S.infoBuiltins) - evalBuiltins t m + runReader t m checkBuiltinFunction :: - (Members '[Error BuiltinsError, NameIdGen, Reader S.InfoTable] r) => + (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => Internal.FunctionDef -> BuiltinFunction -> Sem r () @@ -552,7 +550,7 @@ checkBuiltinFunction d f = localBuiltins $ case f of BuiltinSeq -> checkSeq d checkBuiltinAxiom :: - (Members '[Error BuiltinsError, NameIdGen, Reader S.InfoTable] r) => + (Members '[Error ScoperError, NameIdGen, Reader S.InfoTable] r) => Internal.AxiomDef -> BuiltinAxiom -> Sem r () @@ -596,7 +594,7 @@ checkBuiltinAxiom d b = localBuiltins $ case b of BuiltinByteFromNat -> checkByteFromNat d goInductive :: - (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Error ScoperError, State ConstructorInfos, Reader S.InfoTable, Error BuiltinsError] r) => + (Members '[Reader EntryPoint, Reader DefaultArgsStack, NameIdGen, Reader Pragmas, Error ScoperError, State ConstructorInfos, Reader S.InfoTable] r) => InductiveDef 'Scoped -> Sem r Internal.InductiveDef goInductive ty@InductiveDef {..} = do @@ -632,7 +630,7 @@ checkInductiveConstructors indDef = do goConstructorDef :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Internal.Expression -> ConstructorDef 'Scoped -> Sem r Internal.ConstructorDef @@ -703,10 +701,10 @@ goLiteral = fmap go LitString s -> Internal.LitString s LitIntegerWithBase i -> Internal.LitNumeric (i ^. integerWithBaseValue) -goListPattern :: (Members '[Error ScoperError, Error BuiltinsError, NameIdGen, Reader S.InfoTable] r) => Concrete.ListPattern 'Scoped -> Sem r Internal.Pattern +goListPattern :: (Members '[Error ScoperError, NameIdGen, Reader S.InfoTable] r) => Concrete.ListPattern 'Scoped -> Sem r Internal.Pattern goListPattern l = localBuiltins $ do - nil_ <- getBuiltinName loc BuiltinListNil - cons_ <- getBuiltinName loc BuiltinListCons + nil_ <- getBuiltinNameScoper loc BuiltinListNil + cons_ <- getBuiltinNameScoper loc BuiltinListCons let mkcons :: Internal.Pattern -> Internal.Pattern -> Internal.Pattern mkcons a as = Internal.PatternConstructorApp @@ -791,7 +789,7 @@ createArgumentBlocks appargs = goExpression :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Expression -> Sem r Internal.Expression goExpression = \case @@ -980,8 +978,8 @@ goExpression = \case goList :: Concrete.List 'Scoped -> Sem r Internal.Expression goList l = localBuiltins $ do - nil_ <- getBuiltinName loc BuiltinListNil - cons_ <- getBuiltinName loc BuiltinListCons + nil_ <- getBuiltinNameScoper loc BuiltinListNil + cons_ <- getBuiltinNameScoper loc BuiltinListCons items <- mapM goExpression (l ^. Concrete.listItems) return (foldr (\a b -> cons_ Internal.@@ a Internal.@@ b) (Internal.toExpression nil_) items) where @@ -989,7 +987,7 @@ goExpression = \case goIf :: Concrete.If 'Scoped -> Sem r Internal.Expression goIf e@Concrete.If {..} = do - if_ <- localBuiltins $ getBuiltinName (getLoc e) BuiltinBoolIf + if_ <- localBuiltins $ getBuiltinNameScoper (getLoc e) BuiltinBoolIf go if_ _ifBranches where go :: Internal.Name -> [Concrete.IfBranch 'Scoped 'BranchIfBool] -> Sem r Internal.Expression @@ -1106,7 +1104,7 @@ goExpression = \case mkApp :: Internal.Expression -> Internal.Expression -> Internal.Expression mkApp a1 a2 = Internal.ExpressionApplication $ Internal.Application a1 a2 Explicit -goCase :: forall r. (Members '[Error BuiltinsError, Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Case 'Scoped -> Sem r Internal.Case +goCase :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Case 'Scoped -> Sem r Internal.Case goCase c = do _caseExpression <- goExpression (c ^. caseExpression) _caseBranches <- mapM goBranch (c ^. caseBranches) @@ -1122,14 +1120,14 @@ goCase c = do gRhsExpression :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => RhsExpression 'Scoped -> Sem r Internal.Expression gRhsExpression RhsExpression {..} = goExpression _rhsExpression goSideIfBranch :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => SideIfBranch 'Scoped 'BranchIfBool -> Sem r Internal.SideIfBranch goSideIfBranch s = do @@ -1143,14 +1141,14 @@ goSideIfBranch s = do goSideIfBranchElse :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => SideIfBranch 'Scoped 'BranchIfElse -> Sem r Internal.Expression goSideIfBranchElse s = goExpression (s ^. sideIfBranchBody) goSideIfs :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => SideIfs 'Scoped -> Sem r Internal.SideIfs goSideIfs s = do @@ -1164,14 +1162,14 @@ goSideIfs s = do goCaseBranchRhs :: forall r. - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => CaseBranchRhs 'Scoped -> Sem r Internal.CaseBranchRhs goCaseBranchRhs = \case CaseBranchRhsExpression e -> Internal.CaseBranchRhsExpression <$> gRhsExpression e CaseBranchRhsIf s -> Internal.CaseBranchRhsIf <$> goSideIfs s -goLambda :: forall r. (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Lambda 'Scoped -> Sem r Internal.Lambda +goLambda :: forall r. (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Lambda 'Scoped -> Sem r Internal.Lambda goLambda l = do clauses' <- mapM goClause (l ^. lambdaClauses) return @@ -1191,7 +1189,7 @@ goUniverse u | isSmallUniverse u = SmallUniverse (getLoc u) | otherwise = error "only small universe is supported" -goFunction :: (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Function 'Scoped -> Sem r Internal.Function +goFunction :: (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Function 'Scoped -> Sem r Internal.Function goFunction f = do headParam :| tailParams <- goFunctionParameters (f ^. funParameters) ret <- goExpression (f ^. funReturn) @@ -1202,7 +1200,7 @@ goFunction f = do } goFunctionParameters :: - (Members '[Reader DefaultArgsStack, Error BuiltinsError, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => + (Members '[Reader DefaultArgsStack, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => FunctionParameters 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter) goFunctionParameters FunctionParameters {..} = do @@ -1229,7 +1227,7 @@ mkConstructorApp :: Internal.ConstrName -> [Internal.PatternArg] -> Internal.Con mkConstructorApp a b = Internal.ConstructorApp a b Nothing goPatternApplication :: - (Members '[NameIdGen, Error BuiltinsError, Error ScoperError, Reader S.InfoTable] r) => + (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => PatternApp -> Sem r Internal.ConstructorApp goPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternApplication a) @@ -1240,24 +1238,24 @@ goWildcardConstructor :: goWildcardConstructor a = Internal.WildcardConstructor (goScopedIden (a ^. wildcardConstructor)) goPatternConstructor :: - (Members '[NameIdGen, Error BuiltinsError, Error ScoperError, Reader S.InfoTable] r) => + (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => ScopedIden -> Sem r Internal.ConstructorApp goPatternConstructor a = uncurry mkConstructorApp <$> viewApp (PatternConstructor a) goInfixPatternApplication :: - (Members '[NameIdGen, Error BuiltinsError, Error ScoperError, Reader S.InfoTable] r) => + (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => PatternInfixApp -> Sem r Internal.ConstructorApp goInfixPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternInfixApplication a) goPostfixPatternApplication :: - (Members '[NameIdGen, Error BuiltinsError, Error ScoperError, Reader S.InfoTable] r) => + (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => PatternPostfixApp -> Sem r Internal.ConstructorApp goPostfixPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternPostfixApplication a) -viewApp :: forall r. (Members '[Error BuiltinsError, NameIdGen, Error ScoperError, Reader S.InfoTable] r) => Pattern -> Sem r (Internal.ConstrName, [Internal.PatternArg]) +viewApp :: forall r. (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => Pattern -> Sem r (Internal.ConstrName, [Internal.PatternArg]) viewApp p = case p of PatternConstructor c -> return (goScopedIden c, []) PatternWildcardConstructor c -> return (goScopedIden (c ^. wildcardConstructor), []) @@ -1283,7 +1281,7 @@ viewApp p = case p of | otherwise = viewApp (l ^. patternArgPattern) err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p)) -goPatternArg :: (Members '[Error BuiltinsError, NameIdGen, Error ScoperError, Reader S.InfoTable] r) => PatternArg -> Sem r Internal.PatternArg +goPatternArg :: (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => PatternArg -> Sem r Internal.PatternArg goPatternArg p = do pat' <- goPattern (p ^. patternArgPattern) return @@ -1293,7 +1291,7 @@ goPatternArg p = do _patternArgPattern = pat' } -goPattern :: (Members '[Error BuiltinsError, NameIdGen, Error ScoperError, Reader S.InfoTable] r) => Pattern -> Sem r Internal.Pattern +goPattern :: (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => Pattern -> Sem r Internal.Pattern goPattern p = case p of PatternVariable a -> return $ Internal.PatternVariable (goSymbol a) PatternList a -> goListPattern a @@ -1306,7 +1304,7 @@ goPattern p = case p of PatternRecord i -> goRecordPattern i PatternEmpty {} -> error "unsupported empty pattern" -goRecordPattern :: forall r. (Members '[Error BuiltinsError, NameIdGen, Error ScoperError, Reader S.InfoTable] r) => RecordPattern 'Scoped -> Sem r Internal.Pattern +goRecordPattern :: forall r. (Members '[NameIdGen, Error ScoperError, Reader S.InfoTable] r) => RecordPattern 'Scoped -> Sem r Internal.Pattern goRecordPattern r = do params' <- mkPatterns return @@ -1376,7 +1374,7 @@ goRecordPattern r = do output (Internal.patternArgFromVar Internal.Explicit v) go maxIdx (idx + 1) args -goAxiom :: (Members '[Reader DefaultArgsStack, Error BuiltinsError, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef +goAxiom :: (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef goAxiom a = do _axiomType' <- goExpression (a ^. axiomType) _axiomPragmas' <- goPragmas (a ^. axiomPragmas) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs index 08121a90e1..17b69b2067 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal.hs @@ -41,7 +41,7 @@ typeCheckingNew a = do } fmap (res,) . runReader table - . runReader stable + . runReader (stable ^. Scoped.infoBuiltins) . runResultBuilder importCtx . mapError (JuvixError @TypeCheckerError) $ checkTopModule (res ^. Internal.resultModule) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 5cd4dad5d1..a76a13483f 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -9,8 +9,8 @@ where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Data.List.NonEmpty qualified as NonEmpty -import Juvix.Compiler.Builtins.Error (NotDefined (..)) import Juvix.Compiler.Concrete.Data.Highlight +import Juvix.Compiler.Internal.Builtins (BuiltinsTable, getBuiltinNameTypeChecker) import Juvix.Compiler.Internal.Data.Cast import Juvix.Compiler.Internal.Data.LocalVars import Juvix.Compiler.Internal.Data.TypedHole @@ -29,7 +29,6 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Traits.Resolver import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Traits.Termination import Juvix.Compiler.Pipeline.EntryPoint -import Juvix.Compiler.Store.Scoped.Data.InfoTable qualified as S import Juvix.Data.Effect.NameIdGen import Juvix.Prelude hiding (fromEither) @@ -141,7 +140,7 @@ checkCoercionCycles = do -- TODO consider passing only builtin information instead of the whole S.InfoTable checkTopModule :: - (Members '[HighlightBuilder, Reader S.InfoTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => Module -> Sem r Module checkTopModule md = do @@ -149,7 +148,7 @@ checkTopModule md = do checkModule md checkModule :: - (Members '[HighlightBuilder, Reader S.InfoTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination] r) => Module -> Sem r Module checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do @@ -166,7 +165,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do } checkModuleBody :: - (Members '[HighlightBuilder, Reader S.InfoTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -182,14 +181,14 @@ checkImport :: Import -> Sem r Import checkImport = return checkMutualBlock :: - (Members '[HighlightBuilder, Reader S.InfoTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s) checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader S.InfoTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => InductiveDef -> Sem r InductiveDef checkInductiveDef InductiveDef {..} = runInferenceDef $ do @@ -249,7 +248,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do ) checkTopMutualBlock :: - (Members '[HighlightBuilder, Reader S.InfoTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkTopMutualBlock (MutualBlock ds) = @@ -257,7 +256,7 @@ checkTopMutualBlock (MutualBlock ds) = resolveCastHoles :: forall a r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Reader InsertedArgsStack] r) => Sem (Output CastHole ': r) a -> Sem r a resolveCastHoles s = do @@ -277,7 +276,7 @@ resolveCastHoles s = do void (matchTypes (ExpressionHole _castHoleHole) ty) mkBuiltinInductive :: BuiltinInductive -> Interval -> Sem r Expression - mkBuiltinInductive b i = fmap (ExpressionIden . IdenInductive) (getBuiltinName i b) + mkBuiltinInductive b i = fmap (ExpressionIden . IdenInductive) (getBuiltinNameTypeChecker i b) getIntTy :: Interval -> Sem r Expression getIntTy = mkBuiltinInductive BuiltinInt @@ -286,7 +285,7 @@ resolveCastHoles s = do getNatTy = mkBuiltinInductive BuiltinNat checkMutualStatement :: - (Members '[HighlightBuilder, Reader S.InfoTable, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualStatement -> Sem r MutualStatement checkMutualStatement = \case @@ -314,7 +313,7 @@ unfoldFunType' e = do checkFunctionDef :: forall r. - (Members '[Reader LocalVars, Reader S.InfoTable, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader LocalVars, Reader BuiltinsTable, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionDef -> Sem r FunctionDef checkFunctionDef FunctionDef {..} = do @@ -362,7 +361,7 @@ checkFunctionDef FunctionDef {..} = do withLocalTypeMaybe (p ^. paramName) (p ^. paramType) (go rest) checkIsType :: - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> Expression -> Sem r Expression @@ -370,7 +369,7 @@ checkIsType = checkExpression . smallUniverseE checkDefType :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Sem r Expression checkDefType ty = checkIsType loc ty @@ -462,7 +461,7 @@ checkCoercionType FunctionDef {..} = do checkCaseBranchRhs :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> CaseBranchRhs -> Sem r CaseBranchRhs @@ -481,7 +480,7 @@ checkSideIfs :: Inference, Output TypedHole, Termination, - Reader S.InfoTable, + Reader BuiltinsTable, Output CastHole, Reader InsertedArgsStack ] @@ -501,7 +500,7 @@ checkSideIfs expectedTy SideIfs {..} = do checkSideIfBranch :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> SideIfBranch -> Sem r SideIfBranch @@ -515,12 +514,12 @@ checkSideIfBranch expectedTy SideIfBranch {..} = do _sideIfBranchBody = body' } -getBoolType :: (Members '[Reader InfoTable, Reader S.InfoTable, Error TypeCheckerError] r) => Interval -> Sem r Expression -getBoolType loc = toExpression <$> getBuiltinName loc BuiltinBool +getBoolType :: (Members '[Reader InfoTable, Reader BuiltinsTable, Error TypeCheckerError] r) => Interval -> Sem r Expression +getBoolType loc = toExpression <$> getBuiltinNameTypeChecker loc BuiltinBool checkExpression :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -552,7 +551,7 @@ checkExpression expectedTy e = do resolveInstanceHoles :: forall a r. ( HasExpressions a, - Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r + Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r ) => Sem (Output TypedHole ': r) a -> Sem r a @@ -571,7 +570,7 @@ resolveInstanceHoles s = do $ checkExpression _typedHoleType t checkFunctionParameter :: - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => FunctionParameter -> Sem r FunctionParameter checkFunctionParameter FunctionParameter {..} = do @@ -588,7 +587,7 @@ checkFunctionParameter FunctionParameter {..} = do } inferExpression :: - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Termination, Reader InsertedArgsStack] r) => -- | type hint Maybe Expression -> Expression -> @@ -603,7 +602,7 @@ lookupVar v = do err = error $ "internal error: could not find var " <> ppTrace v <> " at " <> ppTrace (getLoc v) checkFunctionBody :: - (Members '[Reader LocalVars, Reader S.InfoTable, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output TypedHole, ResultBuilder, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader LocalVars, Reader BuiltinsTable, Reader InfoTable, NameIdGen, Error TypeCheckerError, Output TypedHole, ResultBuilder, Inference, Termination, Output CastHole, Reader InsertedArgsStack] r) => Expression -> Expression -> Sem r Expression @@ -628,7 +627,7 @@ checkFunctionBody expectedTy body = checkClauseExpression :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> -- | Type Expression -> @@ -646,7 +645,7 @@ checkClauseExpression clauseLoc clauseType clausePats body = do -- | helper function for lambda functions and case branches checkClause :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack] r) => Interval -> -- | Type Expression -> @@ -918,7 +917,7 @@ checkPattern = go inferExpression' :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -927,7 +926,7 @@ inferExpression' = holesHelper -- | Checks anything but an Application. Does not insert holes inferLeftAppExpression :: forall r. - (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => + (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression @@ -1093,7 +1092,7 @@ inferLeftAppExpression mhint e = case e of _typedExpression = ExpressionLiteral lit } LitString {} -> do - str <- getBuiltinName i BuiltinString + str <- getBuiltinNameTypeChecker i BuiltinString return TypedExpression { _typedExpression = ExpressionLiteral lit, @@ -1107,7 +1106,7 @@ inferLeftAppExpression mhint e = case e of where typedLit :: (Integer -> Literal) -> BuiltinFunction -> Expression -> Sem r TypedExpression typedLit litt blt ty = do - from <- getBuiltinName i blt + from <- getBuiltinNameTypeChecker i blt ihole <- freshHoleImpl i ImplicitInstance let ty' = fromMaybe ty mhint inferExpression' (Just ty') $ @@ -1119,7 +1118,7 @@ inferLeftAppExpression mhint e = case e of ] mkBuiltinInductive :: BuiltinInductive -> Sem r Expression - mkBuiltinInductive = fmap (ExpressionIden . IdenInductive) . getBuiltinName i + mkBuiltinInductive = fmap (ExpressionIden . IdenInductive) . getBuiltinNameTypeChecker i getIntTy :: Sem r Expression getIntTy = mkBuiltinInductive BuiltinInt @@ -1159,7 +1158,7 @@ inferLeftAppExpression mhint e = case e of return (TypedExpression kind (ExpressionIden i)) -- | The hint is used for trailing holes only -holesHelper :: forall r. (Members '[Reader InfoTable, Reader S.InfoTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression +holesHelper :: forall r. (Members '[Reader InfoTable, Reader BuiltinsTable, ResultBuilder, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output TypedHole, Termination, Output CastHole, Reader InsertedArgsStack] r) => Maybe Expression -> Expression -> Sem r TypedExpression holesHelper mhint expr = do let (f, args) = unfoldExpressionApp expr hint @@ -1743,21 +1742,5 @@ newHoleImplicit loc = ExpressionHole . mkHole loc <$> freshNameId newHoleInstance :: (Member NameIdGen r) => Interval -> Sem r Expression newHoleInstance loc = ExpressionInstanceHole . mkInstanceHole loc <$> freshNameId -getBuiltinName :: - (Members '[Reader InfoTable, Reader S.InfoTable, Error TypeCheckerError] r, IsBuiltin a) => - Interval -> - a -> - Sem r Name -getBuiltinName i b = fromConcreteSymbol <$> fromMaybeM notDefined (asks (^. S.infoBuiltins . at b')) - where - b' = toBuiltinPrim b - notDefined = - throw $ - ErrBuiltinNotDefined - NotDefined - { _notDefinedBuiltin = b', - _notDefinedLoc = i - } - withEmptyInsertedArgsStack :: Sem (Reader InsertedArgsStack ': r) a -> Sem r a withEmptyInsertedArgsStack = runReader (mempty @InsertedArgsStack) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs index d6b020e6f2..2f38e57bc3 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -6,7 +6,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Er ) where -import Juvix.Compiler.Builtins.Error (NotDefined) +import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types (BuiltinNotDefined) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty @@ -36,7 +36,7 @@ data TypeCheckerError | ErrSubsumedInstance SubsumedInstance | ErrExplicitInstanceArgument ExplicitInstanceArgument | ErrTraitNotTerminating TraitNotTerminating - | ErrBuiltinNotDefined NotDefined + | ErrBuiltinNotDefined BuiltinNotDefined | ErrArityCheckerError ArityCheckerError | ErrDefaultArgLoop DefaultArgLoop | ErrBadScope BadScope diff --git a/src/Juvix/Compiler/Internal/Translation/Repl.hs b/src/Juvix/Compiler/Internal/Translation/Repl.hs index 4d2b8835ab..d4ab9aefa1 100644 --- a/src/Juvix/Compiler/Internal/Translation/Repl.hs +++ b/src/Juvix/Compiler/Internal/Translation/Repl.hs @@ -11,6 +11,7 @@ import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking import Juvix.Compiler.Pipeline.Artifacts +import Juvix.Compiler.Store.Scoped.Data.InfoTable (infoBuiltins) import Juvix.Prelude typeCheckExpressionType :: @@ -22,10 +23,10 @@ typeCheckExpressionType exp = do table <- extendedTableReplArtifacts exp stable <- gets (^. artifactScopeTable) runResultBuilderArtifacts - . runBuiltinsArtifacts . runNameIdGenArtifacts . ignoreHighlightBuilder . runReader table + . runReader (stable ^. infoBuiltins) . runReader stable . withEmptyLocalVars . withEmptyInsertedArgsStack diff --git a/src/Juvix/Compiler/Pipeline/Artifacts.hs b/src/Juvix/Compiler/Pipeline/Artifacts.hs index 612cc94aaf..e63ac8f90a 100644 --- a/src/Juvix/Compiler/Pipeline/Artifacts.hs +++ b/src/Juvix/Compiler/Pipeline/Artifacts.hs @@ -9,9 +9,9 @@ module Juvix.Compiler.Pipeline.Artifacts ) where -import Juvix.Compiler.Builtins import Juvix.Compiler.Concrete.Data.InfoTableBuilder qualified as Scoped import Juvix.Compiler.Concrete.Data.Scope qualified as S +import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error import Juvix.Compiler.Core.Data.InfoTableBuilder qualified as Core import Juvix.Compiler.Core.Data.Module qualified as Core import Juvix.Compiler.Internal.Language qualified as Internal @@ -48,15 +48,12 @@ tmpCoreInfoTableBuilderArtifacts m = do modify' (set artifactCoreModule md) return a -runBuiltinsArtifacts :: forall r a. (Members '[Error JuvixError, State Artifacts] r) => Sem (Builtins ': r) a -> Sem r a -runBuiltinsArtifacts = - mapError (JuvixError @BuiltinsError) - . runStateLikeArtifacts runBuiltins artifactBuiltins +runScoperInfoTableBuilderArtifacts :: (Members '[Error JuvixError, State Artifacts] r) => Sem (Scoped.InfoTableBuilder ': r) a -> Sem r a +runScoperInfoTableBuilderArtifacts = + mapError (JuvixError @ScoperError) + . runStateLikeArtifacts Scoped.runInfoTableBuilderRepl artifactScopeTable . inject -runScoperInfoTableBuilderArtifacts :: (Members '[State Artifacts] r) => Sem (Scoped.InfoTableBuilder ': r) a -> Sem r a -runScoperInfoTableBuilderArtifacts = runStateLikeArtifacts Scoped.runInfoTableBuilderRepl artifactScopeTable - runScoperScopeArtifacts :: (Members '[State Artifacts] r) => Sem (State S.Scope ': r) a -> Sem r a runScoperScopeArtifacts m = do s <- fromJust <$> gets (^. artifactMainModuleScope) diff --git a/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs b/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs index 9f92567a3c..b29408989f 100644 --- a/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs +++ b/src/Juvix/Compiler/Pipeline/Artifacts/Base.hs @@ -1,6 +1,5 @@ module Juvix.Compiler.Pipeline.Artifacts.Base where -import Juvix.Compiler.Builtins import Juvix.Compiler.Concrete.Data.Scope import Juvix.Compiler.Concrete.Data.Scope qualified as Scoped import Juvix.Compiler.Concrete.Translation.FromSource.Data.ParserState diff --git a/src/Juvix/Compiler/Pipeline/Repl.hs b/src/Juvix/Compiler/Pipeline/Repl.hs index c6e4f05f45..5fd0c3efb7 100644 --- a/src/Juvix/Compiler/Pipeline/Repl.hs +++ b/src/Juvix/Compiler/Pipeline/Repl.hs @@ -40,8 +40,7 @@ upToInternalExpression p = do scopeTable <- gets (^. artifactScopeTable) mtab <- gets (^. artifactModuleTable) pkg <- asks (^. entryPointPackage) - runBuiltinsArtifacts - . runScoperScopeArtifacts + runScoperScopeArtifacts . runStateArtifacts artifactScoperState . runReader pkg $ runNameIdGenArtifacts (Scoper.scopeCheckExpression (Store.getScopedModuleTable mtab) scopeTable p) @@ -55,9 +54,8 @@ expressionUpToAtomsParsed :: Text -> Sem r (ExpressionAtoms 'Parsed) expressionUpToAtomsParsed fp txt = - runNameIdGenArtifacts - . runBuiltinsArtifacts - $ Parser.expressionFromTextSource fp txt + runNameIdGenArtifacts $ + Parser.expressionFromTextSource fp txt expressionUpToAtomsScoped :: (Members '[Reader EntryPoint, State Artifacts, Error JuvixError] r) => @@ -68,8 +66,7 @@ expressionUpToAtomsScoped fp txt = do scopeTable <- gets (^. artifactScopeTable) mtab <- gets (^. artifactModuleTable) pkg <- asks (^. entryPointPackage) - runBuiltinsArtifacts - . runScoperScopeArtifacts + runScoperScopeArtifacts . runStateArtifacts artifactScoperState . runNameIdGenArtifacts . runReader pkg @@ -85,7 +82,6 @@ scopeCheckExpression p = do mtab <- gets (^. artifactModuleTable) pkg <- asks (^. entryPointPackage) runNameIdGenArtifacts - . runBuiltinsArtifacts . runScoperScopeArtifacts . runStateArtifacts artifactScoperState . runReader pkg @@ -138,7 +134,6 @@ registerImport i = do pkg <- asks (^. entryPointPackage) void . runNameIdGenArtifacts - . runBuiltinsArtifacts . runScoperScopeArtifacts . runStateArtifacts artifactScoperState . runReader pkg diff --git a/src/Juvix/Compiler/Pipeline/Run.hs b/src/Juvix/Compiler/Pipeline/Run.hs index 6fe05abb4f..3255c9ebbb 100644 --- a/src/Juvix/Compiler/Pipeline/Run.hs +++ b/src/Juvix/Compiler/Pipeline/Run.hs @@ -219,7 +219,6 @@ runReplPipelineIOEither' lockMode entry = do . ignoreHighlightBuilder . runError . runState initialArtifacts - . runBuiltinsArtifacts . runNameIdGenArtifacts . runFilesIO . runReader entry diff --git a/src/Juvix/Compiler/Store/Extra.hs b/src/Juvix/Compiler/Store/Extra.hs index ebe2a16520..26c25634f0 100644 --- a/src/Juvix/Compiler/Store/Extra.hs +++ b/src/Juvix/Compiler/Store/Extra.hs @@ -1,7 +1,6 @@ module Juvix.Compiler.Store.Extra where import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Concrete.Data.Builtins import Juvix.Compiler.Concrete.Data.Name qualified as C import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Core.Data.InfoTable qualified as Core @@ -48,7 +47,7 @@ computeCombinedCoreInfoTable :: ModuleTable -> Core.InfoTable computeCombinedCoreInfoTable mtab = mconcatMap (toCore . (^. moduleInfoCoreTable)) (HashMap.elems (mtab ^. moduleTable)) -computeCombinedBuiltins :: ModuleTable -> HashMap BuiltinPrim S.Symbol +computeCombinedBuiltins :: ModuleTable -> BuiltinsTable computeCombinedBuiltins mtab = mconcatMap (^. moduleInfoScopedModule . scopedModuleInfoTable . infoBuiltins) diff --git a/src/Juvix/Compiler/Store/Scoped/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Scoped/Data/InfoTable.hs index 0eb527a4b1..7b07eaeb29 100644 --- a/src/Juvix/Compiler/Store/Scoped/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Store/Scoped/Data/InfoTable.hs @@ -2,7 +2,6 @@ module Juvix.Compiler.Store.Scoped.Data.InfoTable where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet -import Juvix.Compiler.Builtins.Effect (BuiltinsTable) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Store.Scoped.Data.SymbolEntry @@ -13,6 +12,8 @@ type DocTable = HashMap NameId (Judoc 'Scoped) type PrecedenceGraph = HashMap S.NameId (HashSet S.NameId) +type BuiltinsTable = HashMap BuiltinPrim S.Symbol + data InfoTable = InfoTable { _infoFixities :: HashMap S.NameId FixityDef, _infoPrecedenceGraph :: PrecedenceGraph,