ddc-core-0.4.3.1: Disciplined Disciple Compiler core language and type checker.

DDC.Data.Env

Description

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

Synopsis

# Types

data Bind n Source #

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) Source # Methods(==) :: Bind n -> Bind n -> Bool #(/=) :: Bind n -> Bind n -> Bool # Ord n => Ord (Bind n) Source # Methodscompare :: Bind n -> Bind n -> Ordering #(<) :: Bind n -> Bind n -> Bool #(<=) :: Bind n -> Bind n -> Bool #(>) :: Bind n -> Bind n -> Bool #(>=) :: Bind n -> Bind n -> Bool #max :: Bind n -> Bind n -> Bind n #min :: Bind n -> Bind n -> Bind n # Show n => Show (Bind n) Source # MethodsshowsPrec :: Int -> Bind n -> ShowS #show :: Bind n -> String #showList :: [Bind n] -> ShowS #

data Bound n Source #

A bound occurrence of a variable.

Constructors

 UIx !Int Index an anonymous binder. UName !n Named variable.

Instances

 Eq n => Eq (Bound n) Source # Methods(==) :: Bound n -> Bound n -> Bool #(/=) :: Bound n -> Bound n -> Bool # Ord n => Ord (Bound n) Source # Methodscompare :: Bound n -> Bound n -> Ordering #(<) :: Bound n -> Bound n -> Bool #(<=) :: Bound n -> Bound n -> Bool #(>) :: Bound n -> Bound n -> Bool #(>=) :: Bound n -> Bound n -> Bool #max :: Bound n -> Bound n -> Bound n #min :: Bound n -> Bound n -> Bound n # Show n => Show (Bound n) Source # MethodsshowsPrec :: Int -> Bound n -> ShowS #show :: Bound n -> String #showList :: [Bound n] -> ShowS #

data Env n a Source #

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

Constructors

 Env FieldsenvMap :: !(Map n a)Named things.envStack :: ![a]Anonymous things.envStackLength :: !IntLength of the stack.

# Conversion

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

Convert a list of Binds to an environment.

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

Convert a list of Binds to an environment.

fromNameMap :: Map n a -> Env n a Source #

Convert a map of things to an environment.

# Constructors

empty :: Env n a Source #

An empty environment, with nothing in it.

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

Construct a singleton environment.

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

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

Combine multiple environments, with the latter ones taking preference.

# Lookup

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

Check whether a bound variable is present in an environment.

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

Lookup a bound variable from an environment.

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

Lookup a value from the environment based on its name.

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

Lookup a value from the environment based on its index.

depth :: Env n a -> Int Source #

Yield the total depth of the anonymous stack.