DDC.Core.Env.EnvX

Environment of a type expression.

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

Documentation

data EnvX n

Environment of term expressions.

Constructors

EnvX

Fields

• envxEnvT :: EnvT n

  Environment of type expressions.

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

  Types of baked in, primitive names.

• envxDataDefs :: !(DataDefs n)

  Data type definitions.

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

  Types of named variables and constructors.

• envxStack :: ![Type n]

  Types of anonymous deBruijn variables.

• envxStackLength :: !Int

  The length of the above stack.

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 :: EnvX n

An empty environment.

fromPrimEnvs

Arguments

:: 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.

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

Construct a singleton type environment.

extendX :: Ord n => Bind n -> EnvX n -> EnvX n

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

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

Extend the environment with the kind of a new type variable.

extendsT :: Ord n => [Bind n] -> EnvX n -> EnvX n

Extend the environment with some new type bindings.

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

Combine multiple environments, with the latter ones taking preference.

Conversion

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

Convert a list of Binds to an environment.

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

Convert a list of name and types into an environment

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

Convert a map of names to types to a environment.

kindEnvOfEnvX :: Ord n => EnvX n -> KindEnv n

Extract a KindEnv from an EnvX.

typeEnvOfEnvX :: Ord n => EnvX n -> TypeEnv n

Extract TypeEnv from an `EnvX.

Projections

depth :: EnvX n -> Int

Yield the total depth of the deBruijn stack.

lookupT :: Ord n => Bound n -> EnvX n -> Maybe (Kind n)

Lookup a bound variable from an environment.

lookupX :: Ord n => Bound n -> EnvX n -> Maybe (Type n)

Lookup a bound variable from an environment.

lookupNameX :: Ord n => n -> EnvX n -> Maybe (Type n)

Lookup a bound name from an environment.

memberX :: Ord n => Bound n -> EnvX n -> Bool

Check whether a bound variable is present in an environment.

memberBindX :: Ord n => Bind n -> EnvX 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.

Primitives

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

Set the function that knows the types of primitive things.

isPrim :: EnvX n -> n -> Bool

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

Lifting

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

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