DDC.Type.Env

Type environments.

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

Documentation

data Env n

A type environment.

Constructors

Env

Fields

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

  Types of named binders.

• envStack :: ![Type n]

  Types of anonymous deBruijn binders.

• envStackLength :: !Int

  The length of the above stack.

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

  Types of baked in, primitive names.

type SuperEnv n = Env n

Type synonym to improve readability.

type KindEnv n = Env n

Type synonym to improve readability.

type TypeEnv n = Env n

Type synonym to improve readability.

Construction

empty :: Env n

An empty environment.

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

Construct a singleton type environment.

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

Extend an environment with a new binding. Replaces bindings with the same name already in the environment.

extends :: Ord n => [Bind n] -> Env n -> Env n

Extend an environment with a list of new bindings. Replaces bindings with the same name already in the environment.

union :: Ord n => Env n -> Env n -> Env 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 => [Env n] -> Env n

Combine multiple environments, with the latter ones taking preference.

Conversion

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

Convert a list of Binds to an environment.

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

Convert a list of name and types into an environment

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

Convert a map of names to types to a environment.

Projections

depth :: Env n -> Int

Yield the total depth of the deBruijn stack.

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

Check whether a bound variable is present in an environment.

memberBind :: Ord n => Bind n -> Env 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 -> Env n -> Maybe (Type n)

Lookup a bound variable from an environment.

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

Lookup a bound name from an environment.

Primitives

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

Set the function that knows the types of primitive things.

isPrim :: Env n -> n -> Bool

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

Lifting

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

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