Safe Haskell	None
Language	Haskell2010

LAM.IsDBEnv

Description

Environments for DeBruijn terms.

Synopsis

class IsDBEnv (t :: Type -> Type) where
- fromList :: [(Name, a)] -> t a
- length :: t a -> Int
- cons :: Name -> a -> t a -> t a
- uncons :: t a -> Maybe (Name, a, t a)
- app :: t a -> t a -> t a
- lookupI :: Eq a => Int -> t a -> Maybe a
- trimEnv :: [Int] -> t a -> Maybe (t a)
toClosure :: forall (t :: Type -> Type) r. IsDBEnv t => Trie (RHeapPointer r DBTerm t) -> Term -> RClosure r DBTerm t
addToEnv :: forall (t :: Type -> Type). IsDBEnv t => Name -> Term -> Trie (RHeapPointer IORef DBTerm t) -> IO (Trie (RHeapPointer IORef DBTerm t))

Documentation

class IsDBEnv (t :: Type -> Type) where #

A container that can be used as an environment for DeBruijn terms. The key component is the indexing function lookupI.

Minimal complete definition

Methods

fromList :: [(Name, a)] -> t a #

length :: t a -> Int #

cons :: Name -> a -> t a -> t a #

uncons :: t a -> Maybe (Name, a, t a) #

app :: t a -> t a -> t a #

lookupI :: Eq a => Int -> t a -> Maybe a #

trimEnv :: [Int] -> t a -> Maybe (t a) #

Instances details

IsDBEnv NamedList #
Instance details Defined in LAM.IsDBEnv Methods fromList :: [(Name, a)] -> NamedList a # length :: NamedList a -> Int # cons :: Name -> a -> NamedList a -> NamedList a # uncons :: NamedList a -> Maybe (Name, a, NamedList a) # app :: NamedList a -> NamedList a -> NamedList a # lookupI :: Eq a => Int -> NamedList a -> Maybe a # trimEnv :: [Int] -> NamedList a -> Maybe (NamedList a) #
IsDBEnv Seq #
Instance details Defined in LAM.IsDBEnv Methods fromList :: [(Name, a)] -> Seq a # length :: Seq a -> Int # cons :: Name -> a -> Seq a -> Seq a # uncons :: Seq a -> Maybe (Name, a, Seq a) # app :: Seq a -> Seq a -> Seq a # lookupI :: Eq a => Int -> Seq a -> Maybe a # trimEnv :: [Int] -> Seq a -> Maybe (Seq a) #
IsDBEnv Vector #
Instance details Defined in LAM.IsDBEnv Methods fromList :: [(Name, a)] -> Vector a # length :: Vector a -> Int # cons :: Name -> a -> Vector a -> Vector a # uncons :: Vector a -> Maybe (Name, a, Vector a) # app :: Vector a -> Vector a -> Vector a # lookupI :: Eq a => Int -> Vector a -> Maybe a # trimEnv :: [Int] -> Vector a -> Maybe (Vector a) #
IsDBEnv [] #
Instance details Defined in LAM.IsDBEnv Methods fromList :: [(Name, a)] -> [a] # length :: [a] -> Int # cons :: Name -> a -> [a] -> [a] # uncons :: [a] -> Maybe (Name, a, [a]) # app :: [a] -> [a] -> [a] # lookupI :: Eq a => Int -> [a] -> Maybe a # trimEnv :: [Int] -> [a] -> Maybe [a] #

Convert a (named) term together with named environment that contains DeBruijn heap pointers to a closure. Useful for evaluating open terms.

Add top-level terms to a named environment for DeBruijn heap pointers.