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 EnvX n = EnvX {
- envxEnvT :: EnvT n
- envxPrimFun :: !(n -> Maybe (Type n))
- envxDataDefs :: !(DataDefs n)
- envxMap :: !(Map n (Type n))
- envxStack :: ![Type n]
- envxStackLength :: !Int
- 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 :: EnvX n
- fromPrimEnvs :: Ord n => KindEnv n -> TypeEnv n -> DataDefs n -> EnvX n
- singleton :: Ord n => Bind n -> EnvX n
- extendX :: Ord n => Bind n -> EnvX n -> EnvX n
- extendsX :: Ord n => [Bind n] -> EnvX n -> EnvX n
- extendT :: Ord n => Bind n -> EnvX n -> EnvX n
- extendsT :: Ord n => [Bind n] -> EnvX n -> EnvX n
- union :: Ord n => EnvX n -> EnvX n -> EnvX n
- unions :: Ord n => [EnvX n] -> EnvX n
- fromList :: Ord n => [Bind n] -> EnvX n
- fromListNT :: Ord n => [(n, Type n)] -> EnvX n
- fromTypeMap :: Map n (Type n) -> EnvX n
- kindEnvOfEnvX :: Ord n => EnvX n -> KindEnv n
- typeEnvOfEnvX :: Ord n => EnvX n -> TypeEnv n
- depth :: EnvX n -> Int
- lookupT :: Ord n => Bound n -> EnvX n -> Maybe (Kind n)
- lookupX :: Ord n => Bound n -> EnvX n -> Maybe (Type n)
- lookupNameX :: Ord n => n -> EnvX n -> Maybe (Type n)
- memberX :: Ord n => Bound n -> EnvX n -> Bool
- memberBindX :: Ord n => Bind n -> EnvX n -> Bool
- setPrimFun :: (n -> Maybe (Type n)) -> EnvX n -> EnvX n
- isPrim :: EnvX n -> n -> Bool
- lift :: Ord n => Int -> EnvX n -> EnvX n
Documentation
Environment of term expressions.
EnvX | |
|
A type environment.
EnvT | |
|
Construction
:: Ord n | |
=> KindEnv n | Primitive kind environment. |
-> TypeEnv n | Primitive type environment. |
-> DataDefs n | Primitive data type definitions. |
-> EnvX n |
Build an EnvX
from prim environments.
extendX :: Ord n => Bind n -> EnvX n -> EnvX n Source #
Extend an environment with a new binding. Replaces bindings with the same name already in the environment.
extendsX :: Ord n => [Bind n] -> EnvX n -> EnvX n Source #
Extend an environment with a list of new bindings. Replaces bindings with the same name already in the environment.
extendT :: Ord n => Bind n -> EnvX n -> EnvX n Source #
Extend the environment with the kind of a new type variable.
extendsT :: Ord n => [Bind n] -> EnvX n -> EnvX n Source #
Extend the environment with some new type bindings.
union :: Ord n => EnvX n -> EnvX n -> EnvX 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 => [EnvX n] -> EnvX n Source #
Combine multiple environments, with the latter ones taking preference.
Conversion
fromListNT :: Ord n => [(n, Type n)] -> EnvX n Source #
Convert a list of name and types into an environment
Projections
lookupT :: Ord n => Bound n -> EnvX n -> Maybe (Kind n) Source #
Lookup a bound variable from an environment.
lookupX :: Ord n => Bound n -> EnvX n -> Maybe (Type n) Source #
Lookup a bound variable from an environment.
lookupNameX :: Ord n => n -> EnvX n -> Maybe (Type n) Source #
Lookup a bound name from an environment.
memberX :: Ord n => Bound n -> EnvX n -> Bool Source #
Check whether a bound variable is present in an environment.
memberBindX :: Ord n => Bind n -> EnvX 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.
Primitives
setPrimFun :: (n -> Maybe (Type n)) -> EnvX n -> EnvX n Source #
Set the function that knows the types of primitive things.