Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Environment of a type expression.
An environment contains the types named bound variables, named primitives, and a deBruijn stack for anonymous variables.
- data EnvT n = EnvT {
- envtPrimFun :: !(n -> Maybe (Type n))
- envtEquations :: !(Map n (Type n))
- envtCapabilities :: !(Map n (Type n))
- envtMap :: !(Map n (Type n))
- envtStack :: ![Type n]
- envtStackLength :: !Int
- empty :: EnvT n
- singleton :: Ord n => Bind n -> EnvT n
- extend :: Ord n => Bind n -> EnvT n -> EnvT n
- extends :: Ord n => [Bind n] -> EnvT n -> EnvT n
- union :: Ord n => EnvT n -> EnvT n -> EnvT n
- unions :: Ord n => [EnvT n] -> EnvT n
- fromList :: Ord n => [Bind n] -> EnvT n
- fromListNT :: Ord n => [(n, Type n)] -> EnvT n
- fromTypeMap :: Map n (Type n) -> EnvT n
- kindEnvOfEnvT :: Ord n => EnvT n -> KindEnv n
- depth :: EnvT n -> Int
- member :: Ord n => Bound n -> EnvT n -> Bool
- memberBind :: Ord n => Bind n -> EnvT n -> Bool
- lookup :: Ord n => Bound n -> EnvT n -> Maybe (Type n)
- lookupName :: Ord n => n -> EnvT n -> Maybe (Type n)
- setPrimFun :: (n -> Maybe (Type n)) -> EnvT n -> EnvT n
- isPrim :: EnvT n -> n -> Bool
- lift :: Ord n => Int -> EnvT n -> EnvT n
Documentation
A type environment.
EnvT | |
|
Construction
extend :: Ord n => Bind n -> EnvT n -> EnvT n Source #
Extend an environment with a new binding. Replaces bindings with the same name already in the environment.
extends :: Ord n => [Bind n] -> EnvT n -> EnvT n Source #
Extend an environment with a list of new bindings. Replaces bindings with the same name already in the environment.
union :: Ord n => EnvT n -> EnvT n -> EnvT n Source #
Combine two environments. If both environments have a binding with the same name, then the one in the second environment takes preference.
unions :: Ord n => [EnvT n] -> EnvT n Source #
Combine multiple environments, with the latter ones taking preference.
Conversion
fromListNT :: Ord n => [(n, Type n)] -> EnvT n Source #
Convert a list of name and types into an environment
Projections
member :: Ord n => Bound n -> EnvT n -> Bool Source #
Check whether a bound variable is present in an environment.
memberBind :: Ord n => Bind n -> EnvT n -> Bool Source #
Check whether a binder is already present in the an environment. This can only return True for named binders, not anonymous or primitive ones.
lookup :: Ord n => Bound n -> EnvT n -> Maybe (Type n) Source #
Lookup a bound variable from an environment.
lookupName :: Ord n => n -> EnvT n -> Maybe (Type n) Source #
Lookup a bound name from an environment.
Primitives
setPrimFun :: (n -> Maybe (Type n)) -> EnvT n -> EnvT n Source #
Set the function that knows the types of primitive things.