Safe Haskell | Safe |
---|---|

Language | Haskell98 |

Type environments.

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

- data Env n = Env {
- envMap :: !(Map n (Type n))
- envStack :: ![Type n]
- envStackLength :: !Int
- envPrimFun :: !(n -> Maybe (Type n))

- type SuperEnv n = Env n
- type KindEnv n = Env n
- type TypeEnv n = Env n
- empty :: Env n
- singleton :: Ord n => Bind n -> Env n
- extend :: Ord n => Bind n -> Env n -> Env n
- extends :: Ord n => [Bind n] -> Env n -> Env n
- union :: Ord n => Env n -> Env n -> Env n
- unions :: Ord n => [Env n] -> Env n
- fromList :: Ord n => [Bind n] -> Env n
- fromListNT :: Ord n => [(n, Type n)] -> Env n
- fromTypeMap :: Map n (Type n) -> Env n
- depth :: Env n -> Int
- member :: Ord n => Bound n -> Env n -> Bool
- memberBind :: Ord n => Bind n -> Env n -> Bool
- lookup :: Ord n => Bound n -> Env n -> Maybe (Type n)
- lookupName :: Ord n => n -> Env n -> Maybe (Type n)
- setPrimFun :: (n -> Maybe (Type n)) -> Env n -> Env n
- isPrim :: Env n -> n -> Bool
- lift :: Ord n => Int -> Env n -> Env n

# Documentation

A type environment.

# Construction

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

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 Source #

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 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 => [Env n] -> Env n Source #

Combine multiple environments, with the latter ones taking preference.

# Conversion

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

Convert a list of name and types into an environment

# Projections

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

Check whether a bound variable is present in an environment.

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

Lookup a bound variable from an environment.

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

Lookup a bound name from an environment.

# Primitives

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

Set the function that knows the types of primitive things.