Language.PiSigma.Evaluate

Documentation

newtype Eval e a

Constructors

Eval

Fields

unEval :: StateT e (ErrorT EvalErr Identity) a

Instances

MonadState e (Eval e)

MonadError EvalErr (Eval e)

Monad (Eval e)

catchE :: Eval e a -> (EvalErr -> Eval e a) -> Eval e a

decl :: Env e => Name -> PrtInfo -> Scope -> Maybe (Clos Type) -> Eval e (Id, Scope)

Takes a name, a scope, and potentially a type. It extends the environment and the scope with that name.

decl' :: Env e => Name -> Scope -> Eval e (Id, Scope)

defn' :: Env e => Id -> Clos Type -> Eval e ()

force :: Env e => Val -> Eval e Val

eval :: Env e => Clos Term -> Eval e Val

evalProg :: Env e => Clos Prog -> Eval e Scope

getEnv :: Eval e e

getId :: Loc -> Name -> Scope -> Eval e Id

letn :: Env e => Id -> EnvEntry -> Eval e a -> Eval e a

Locally updates the environment.

letn' :: Env e => Id -> Clos Type -> Eval e a -> Eval e a

lookupId :: Env e => Id -> Eval e EnvEntry

run :: e -> Eval e a -> Either EvalErr (a, e)

subst :: Env e => Bind (Clos Term) -> Clos Term -> Eval e (Clos Term)

tdecl :: Env e => Name -> Scope -> Clos Type -> Eval e (Id, Scope)