DDC.Data.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)

Methods

(==) :: Bind n -> Bind n -> Bool

(/=) :: Bind n -> Bind n -> Bool

Ord n => Ord (Bind n)

Methods

compare :: 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)

Methods

showsPrec :: Int -> Bind n -> ShowS

show :: Bind n -> String

showList :: [Bind n] -> ShowS

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)

Methods

(==) :: Bound n -> Bound n -> Bool

(/=) :: Bound n -> Bound n -> Bool

Ord n => Ord (Bound n)

Methods

compare :: 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)

Methods

showsPrec :: Int -> Bound n -> ShowS

show :: Bound n -> String

showList :: [Bound n] -> ShowS

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.