DDC.Base.Env

Generic environment that handles both named and anonymous de-bruijn binders.

Types

data Bind n

A binding occurrence of a variable.

Constructors

BNone

No binding, or alternatively, bind a fresh name that has no bound uses.

BAnon

Anonymous binder.

BName !n

Named binder.

Instances

Eq n => Eq (Bind n)

Ord n => Ord (Bind n)

Show n => Show (Bind n)

data Bound n

A bound occurrence of a variable.

Constructors

UIx !Int

Index an anonymous binder.

UName !n

Named variable.

Instances

Eq n => Eq (Bound n)

Ord n => Ord (Bound n)

Show n => Show (Bound n)

data Env n a

Generic environment that maps a variable to a thing of type a.

Constructors

Env

Fields

envMap :: !(Map n a)

Named things.

envStack :: ![a]

Anonymous things.

envStackLength :: !Int

Length of the stack.

Conversion

fromList :: Ord n => [(Bind n, a)] -> Env n a

Convert a list of Binds to an environment.

fromNameList :: Ord n => [(n, a)] -> Env n a

Convert a list of Binds to an environment.

fromNameMap :: Map n a -> Env n a

Convert a map of things to an environment.

Constructors

empty :: Env n a

An empty environment, with nothing in it.

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

Construct a singleton environment.

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

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

extends :: Ord n => [(Bind n, a)] -> Env n a -> Env n a

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

union :: Ord n => Env n a -> Env n a -> Env n a

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 a] -> Env n a

Combine multiple environments, with the latter ones taking preference.

Lookup

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

Check whether a bound variable is present in an environment.

lookup :: Ord n => Bound n -> Env n a -> Maybe a

Lookup a bound variable from an environment.

lookupName :: Ord n => n -> Env n a -> Maybe a

Lookup a value from the environment based on its name.

lookupIx :: Ord n => Int -> Env n a -> Maybe a

Lookup a value from the environment based on its index.

depth :: Env n a -> Int

Yield the total depth of the anonymous stack.