DDC.Core.Env.EnvT

Environment of a type expression.

An environment contains the types named bound variables, named primitives, and a deBruijn stack for anonymous variables.

Documentation

data EnvT n

A type environment.

Constructors

EnvT

Fields

• envtPrimFun :: !(n -> Maybe (Type n))

  Types of baked in, primitive names.

• envtEquations :: !(Map n (Type n))

  Map of constructor name to bound type for type equations.

• envtCapabilities :: !(Map n (Type n))

  Map of globally available capabilities.

• envtMap :: !(Map n (Type n))

  Kinds of named variables and constructors.

• envtStack :: ![Type n]

  Types of anonymous deBruijn variables.

• envtStackLength :: !Int

  The length of the above stack.

Construction

empty :: EnvT n

An empty environment.

singleton :: Ord n => Bind n -> EnvT n

Construct a singleton type environment.

extend :: Ord n => Bind n -> EnvT n -> EnvT n

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

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

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

Combine multiple environments, with the latter ones taking preference.

Conversion

fromList :: Ord n => [Bind n] -> EnvT n

Convert a list of Binds to an environment.

fromListNT :: Ord n => [(n, Type n)] -> EnvT n

Convert a list of name and types into an environment

fromTypeMap :: Map n (Type n) -> EnvT n

Convert a map of names to types to a environment.

kindEnvOfEnvT :: Ord n => EnvT n -> KindEnv n

Extract a KindEnv from an EnvT.

Projections

depth :: EnvT n -> Int

Yield the total depth of the deBruijn stack.

member :: Ord n => Bound n -> EnvT n -> Bool

Check whether a bound variable is present in an environment.

memberBind :: Ord n => Bind n -> EnvT n -> Bool

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)

Lookup a bound variable from an environment.

lookupName :: Ord n => n -> EnvT n -> Maybe (Type n)

Lookup a bound name from an environment.

Primitives

setPrimFun :: (n -> Maybe (Type n)) -> EnvT n -> EnvT n

Set the function that knows the types of primitive things.

isPrim :: EnvT n -> n -> Bool

Check if the type of a name is defined by the envPrimFun.

Lifting

lift :: Ord n => Int -> EnvT n -> EnvT n

Lift all free deBruijn indices in the environment by the given number of steps.