Safe Haskell	Safe-Inferred
Language	Haskell2010

LAM.Base

Description

This module contains all sorts of general definitions for working with terms

Synopsis

module LAM.Types.BV
module LAM.Types.Generic
module LAM.Types.Pure
freeIxs :: DBTerm -> [Int]
appT :: Term -> Term -> Term
substName :: Term -> Name -> Name -> Term
isClosed :: Term -> Bool
isFree :: Term -> Name -> Bool
freshName :: String -> Term -> Name
class IsNamedEnv (t :: Type -> Type) where
- eToList :: t a -> [(Name, a)]
- eFromList :: [(Name, a)] -> t a
- eLookup :: Name -> t a -> Maybe a
- addToEnv :: Name -> a -> t a -> t a
newtype NamedList a = NamedList [(Name, a)]
data RClosure (r :: Type -> Type) term (t :: Type -> Type) = Closure {
- t :: term
- env :: t (RHeapPointer r term t)
}
data Tag a
- = P a
- | H a
type RState (r :: Type -> Type) term (t :: Type -> Type) = (RClosure r term t, RStack r term t)
type State = RState IORef Term Trie
type RStack (r :: Type -> Type) term (t :: Type -> Type) = [Tag (RHeapPointer r term t)]
type REnvironment (r :: Type -> Type) term (t :: Type -> Type) = t (RHeapPointer r term t)
type RHeapPointer (r :: Type -> Type) term (t :: Type -> Type) = r (Maybe (RClosure r term t))
type HeapRefs term (t :: Type -> Type) = [IORef (Maybe (RClosure IORef term t))]
type Closure term (t :: Type -> Type) = RClosure IORef term t
freeVars :: Term -> [Name]
convStateRef :: forall m (t :: Type -> Type) r' r term. (Monad m, Traversable t, Traversable r') => (r (Maybe (RClosure r term t)) -> m (r' (Maybe (RClosure r term t)))) -> RState r term t -> m (RState r' term t)
convClosureRef :: forall m (t :: Type -> Type) r' r term. (Monad m, Traversable t, Traversable r') => (r (Maybe (RClosure r term t)) -> m (r' (Maybe (RClosure r term t)))) -> RClosure r term t -> m (RClosure r' term t)
withFix :: Term -> Term
toTerm :: Term -> Term
unsafeLookupNs :: [Name] -> Trie a -> [(Name, a)]
mapFree :: (Int -> Int) -> DBTerm -> DBTerm
collectHeap :: forall (t :: Type -> Type) term. Traversable t => RState IORef term t -> IO (HeapRefs term t)

Documentation

module LAM.Types.BV

module LAM.Types.Generic

module LAM.Types.Pure

freeIxs :: DBTerm -> [Int] #

DeBruijn version of freeVars.

length (freeIxs (toDBTerm id t)) = length (freeVars t)

length ctx = maximum (freeIxs t) + 1 => freeVars (fromDBTermCtx id ctx t) = ctx

appT :: Term -> Term -> Term #

Emulate application.

substName :: Term -> Name -> Name -> Term #

substName t n n' is t[n/n'], i.e. replace every free occurence of n' by n.

isClosed :: Term -> Bool #

Whether a term is closed.

isFree :: Term -> Name -> Bool #

freshName :: String -> Term -> Name #

Generate a name that doesn't appear in a Term.

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

An environment

Minimal complete definition

eToList, eFromList

Methods

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

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

eLookup :: Name -> t a -> Maybe a #

addToEnv :: Name -> a -> t a -> t a #

Instances

Instances details

IsNamedEnv NamedList #
Instance details Defined in LAM.Base Methods eToList :: NamedList a -> [(Name, a)] # eFromList :: [(Name, a)] -> NamedList a # eLookup :: Name -> NamedList a -> Maybe a # addToEnv :: Name -> a -> NamedList a -> NamedList a #
IsNamedEnv Trie #
Instance details Defined in LAM.Base Methods eToList :: Trie a -> [(Name, a)] # eFromList :: [(Name, a)] -> Trie a # eLookup :: Name -> Trie a -> Maybe a # addToEnv :: Name -> a -> Trie a -> Trie a #
IsNamedEnv Seq #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods eToList :: Seq a -> [(Name, a)] # eFromList :: [(Name, a)] -> Seq a # eLookup :: Name -> Seq a -> Maybe a # addToEnv :: Name -> a -> Seq a -> Seq a #
IsNamedEnv Vector #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods eToList :: Vector a -> [(Name, a)] # eFromList :: [(Name, a)] -> Vector a # eLookup :: Name -> Vector a -> Maybe a # addToEnv :: Name -> a -> Vector a -> Vector a #
IsNamedEnv [] #
Instance details Defined in LAM.Base Methods eToList :: [a] -> [(Name, a)] # eFromList :: [(Name, a)] -> [a] # eLookup :: Name -> [a] -> Maybe a # addToEnv :: Name -> a -> [a] -> [a] #

newtype NamedList a #

A basic environment for DeBruijn terms, including names for converting to a named representation.

Constructors

NamedList [(Name, a)]

Instances

Instances details

IsNamedEnv NamedList #
Instance details Defined in LAM.Base Methods eToList :: NamedList a -> [(Name, a)] # eFromList :: [(Name, a)] -> NamedList a # eLookup :: Name -> NamedList a -> Maybe a # addToEnv :: Name -> a -> NamedList a -> NamedList a #
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) #
Foldable NamedList #
Instance details Defined in LAM.Base Methods fold :: Monoid m => NamedList m -> m # foldMap :: Monoid m => (a -> m) -> NamedList a -> m # foldMap' :: Monoid m => (a -> m) -> NamedList a -> m # foldr :: (a -> b -> b) -> b -> NamedList a -> b # foldr' :: (a -> b -> b) -> b -> NamedList a -> b # foldl :: (b -> a -> b) -> b -> NamedList a -> b # foldl' :: (b -> a -> b) -> b -> NamedList a -> b # foldr1 :: (a -> a -> a) -> NamedList a -> a # foldl1 :: (a -> a -> a) -> NamedList a -> a # toList :: NamedList a -> [a] # null :: NamedList a -> Bool # length :: NamedList a -> Int # elem :: Eq a => a -> NamedList a -> Bool # maximum :: Ord a => NamedList a -> a # minimum :: Ord a => NamedList a -> a # sum :: Num a => NamedList a -> a # product :: Num a => NamedList a -> a #
Traversable NamedList #
Instance details Defined in LAM.Base Methods traverse :: Applicative f => (a -> f b) -> NamedList a -> f (NamedList b) # sequenceA :: Applicative f => NamedList (f a) -> f (NamedList a) # mapM :: Monad m => (a -> m b) -> NamedList a -> m (NamedList b) # sequence :: Monad m => NamedList (m a) -> m (NamedList a) #
Functor NamedList #
Instance details Defined in LAM.Base Methods fmap :: (a -> b) -> NamedList a -> NamedList b # (<$) :: a -> NamedList b -> NamedList a #
CanTrim DBTTerm0 NamedList #
Instance details Defined in LAM.Exec.DBTrimPure Methods trim :: Closure DBTTerm0 NamedList -> Closure DBTTerm0 NamedList #
CanTrim DBTerm NamedList #
Instance details Defined in LAM.CanTrim Methods trim :: Closure DBTerm NamedList -> Closure DBTerm NamedList #
CanTrim Term NamedList #
Instance details Defined in LAM.CanTrim Methods trim :: Closure Term NamedList -> Closure Term NamedList #
Show a => Show (NamedList a) #
Instance details Defined in LAM.Base Methods showsPrec :: Int -> NamedList a -> ShowS # show :: NamedList a -> String # showList :: [NamedList a] -> ShowS #
ToPureState (State NamedList) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State NamedList -> IO (PState NamedList) #
ToPureState (State NamedList) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State NamedList -> IO (PState Trie) #
ToPureState (State Seq) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Seq -> IO (PState NamedList) #
ToPureState (State Vector) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Vector -> IO (PState NamedList) #
ToPureState (State []) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State [] -> IO (PState NamedList) #
ToPureState (State NamedList) NamedList #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State NamedList -> IO (PState NamedList) #
ToPureState (State NamedList) Trie #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State NamedList -> IO (PState Trie) #

data RClosure (r :: Type -> Type) term (t :: Type -> Type) #

Closure with a pointer type r.

Constructors

Closure
Fields t :: term env :: t (RHeapPointer r term t)

Instances

Instances details

ToPureState (State NamedList) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State NamedList -> IO (PState NamedList) #
ToPureState (State NamedList) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State NamedList -> IO (PState Trie) #
ToPureState (State Seq) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Seq -> IO (PState NamedList) #
ToPureState (State Seq) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Seq -> IO (PState Trie) #
ToPureState (State Vector) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Vector -> IO (PState NamedList) #
ToPureState (State Vector) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Vector -> IO (PState Trie) #
ToPureState (State []) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State [] -> IO (PState NamedList) #
ToPureState (State []) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State [] -> IO (PState Trie) #
ToPureState (State NamedList) NamedList #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State NamedList -> IO (PState NamedList) #
ToPureState (State NamedList) Trie #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State NamedList -> IO (PState Trie) #
ToPureState (State []) Trie #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State [] -> IO (PState Trie) #
IsNamedEnv t => ToPureState (PState t) t #
Instance details Defined in LAM.Pure Methods toPureState :: PState t -> IO (PState t) #
(IsNamedEnv t1, IsNamedEnv t2) => ToPureState (PState t1) t2 #
Instance details Defined in LAM.Pure Methods toPureState :: PState t1 -> IO (PState t2) #
Show (Closure DBTTerm0 t) #
Instance details Defined in LAM.Exec.DBTrimPure Methods showsPrec :: Int -> Closure DBTTerm0 t -> ShowS # show :: Closure DBTTerm0 t -> String # showList :: [Closure DBTTerm0 t] -> ShowS #
Show (Closure DBTerm t) #
Instance details Defined in LAM.Pure Methods showsPrec :: Int -> Closure DBTerm t -> ShowS # show :: Closure DBTerm t -> String # showList :: [Closure DBTerm t] -> ShowS #
Show (Closure Term Trie) #
Instance details Defined in LAM.Pure Methods showsPrec :: Int -> Closure Term Trie -> ShowS # show :: Closure Term Trie -> String # showList :: [Closure Term Trie] -> ShowS #
(Traversable t1, CanTrim Term t1, IsNamedEnv t1, IsNamedEnv t2) => ToPureState (RState IORef Term t1) t2 #
Instance details Defined in LAM.Pure Methods toPureState :: RState IORef Term t1 -> IO (PState t2) #

data Tag a #

Tags for storing things on the stack.

Constructors

P a
H a

Instances

Instances details

Foldable Tag #
Instance details Defined in LAM.Base Methods fold :: Monoid m => Tag m -> m # foldMap :: Monoid m => (a -> m) -> Tag a -> m # foldMap' :: Monoid m => (a -> m) -> Tag a -> m # foldr :: (a -> b -> b) -> b -> Tag a -> b # foldr' :: (a -> b -> b) -> b -> Tag a -> b # foldl :: (b -> a -> b) -> b -> Tag a -> b # foldl' :: (b -> a -> b) -> b -> Tag a -> b # foldr1 :: (a -> a -> a) -> Tag a -> a # foldl1 :: (a -> a -> a) -> Tag a -> a # toList :: Tag a -> [a] # null :: Tag a -> Bool # length :: Tag a -> Int # elem :: Eq a => a -> Tag a -> Bool # maximum :: Ord a => Tag a -> a # minimum :: Ord a => Tag a -> a # sum :: Num a => Tag a -> a # product :: Num a => Tag a -> a #
Traversable Tag #
Instance details Defined in LAM.Base Methods traverse :: Applicative f => (a -> f b) -> Tag a -> f (Tag b) # sequenceA :: Applicative f => Tag (f a) -> f (Tag a) # mapM :: Monad m => (a -> m b) -> Tag a -> m (Tag b) # sequence :: Monad m => Tag (m a) -> m (Tag a) #
Functor Tag #
Instance details Defined in LAM.Base Methods fmap :: (a -> b) -> Tag a -> Tag b # (<$) :: a -> Tag b -> Tag a #
Show a => Show (Tag a) #
Instance details Defined in LAM.Base Methods showsPrec :: Int -> Tag a -> ShowS # show :: Tag a -> String # showList :: [Tag a] -> ShowS #
Eq a => Eq (Tag a) #
Instance details Defined in LAM.Base Methods (==) :: Tag a -> Tag a -> Bool # (/=) :: Tag a -> Tag a -> Bool #
ToPureState (State NamedList) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State NamedList -> IO (PState NamedList) #
ToPureState (State NamedList) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State NamedList -> IO (PState Trie) #
ToPureState (State Seq) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Seq -> IO (PState NamedList) #
ToPureState (State Seq) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Seq -> IO (PState Trie) #
ToPureState (State Vector) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Vector -> IO (PState NamedList) #
ToPureState (State Vector) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State Vector -> IO (PState Trie) #
ToPureState (State []) NamedList #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State [] -> IO (PState NamedList) #
ToPureState (State []) Trie #
Instance details Defined in LAM.Exec.DBNoTrimPure Methods toPureState :: State [] -> IO (PState Trie) #
ToPureState (State NamedList) NamedList #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State NamedList -> IO (PState NamedList) #
ToPureState (State NamedList) Trie #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State NamedList -> IO (PState Trie) #
ToPureState (State []) Trie #
Instance details Defined in LAM.Exec.DBTrimPure Methods toPureState :: State [] -> IO (PState Trie) #
IsNamedEnv t => ToPureState (PState t) t #
Instance details Defined in LAM.Pure Methods toPureState :: PState t -> IO (PState t) #
(IsNamedEnv t1, IsNamedEnv t2) => ToPureState (PState t1) t2 #
Instance details Defined in LAM.Pure Methods toPureState :: PState t1 -> IO (PState t2) #
(Traversable t1, CanTrim Term t1, IsNamedEnv t1, IsNamedEnv t2) => ToPureState (RState IORef Term t1) t2 #
Instance details Defined in LAM.Pure Methods toPureState :: RState IORef Term t1 -> IO (PState t2) #

type RState (r :: Type -> Type) term (t :: Type -> Type) = (RClosure r term t, RStack r term t) #

The state is a pair of a closure and a stack.

type State = RState IORef Term Trie #

Same as above.

type RStack (r :: Type -> Type) term (t :: Type -> Type) = [Tag (RHeapPointer r term t)] #

Since we only ever interact with the stack via the top element, this can just be a list.

type REnvironment (r :: Type -> Type) term (t :: Type -> Type) = t (RHeapPointer r term t) #

An environment is a container of heap pointers. Does not specify how to index into the environment, so this works for named or DeBruijn.

type RHeapPointer (r :: Type -> Type) term (t :: Type -> Type) = r (Maybe (RClosure r term t)) #

Pointer to a closure or black hole

type HeapRefs term (t :: Type -> Type) = [IORef (Maybe (RClosure IORef term t))] #

A type for collecting heap pointers.

type Closure term (t :: Type -> Type) = RClosure IORef term t #

The most common pointer type is IORef.

freeVars :: Term -> [Name] #

The free variables of a term.

freeVars (λ x. t) = freeVars t \ [x]

convStateRef :: forall m (t :: Type -> Type) r' r term. (Monad m, Traversable t, Traversable r') => (r (Maybe (RClosure r term t)) -> m (r' (Maybe (RClosure r term t)))) -> RState r term t -> m (RState r' term t) #

Convert the pointer type in a state.

convClosureRef :: forall m (t :: Type -> Type) r' r term. (Monad m, Traversable t, Traversable r') => (r (Maybe (RClosure r term t)) -> m (r' (Maybe (RClosure r term t)))) -> RClosure r term t -> m (RClosure r' term t) #

Convert the pointer type in a closure.

withFix :: Term -> Term #

Add a fix point operator to a term.

toTerm :: Term -> Term #

Convert a general lambda term to a representation for our abstract machines.

unsafeLookupNs :: [Name] -> Trie a -> [(Name, a)] #

Lookup a subset of a trie.

mapFree :: (Int -> Int) -> DBTerm -> DBTerm #

Apply some transformation to the free variables.

map f (freeIxs t) = freeIxs (mapFree f t)

collectHeap :: forall (t :: Type -> Type) term. Traversable t => RState IORef term t -> IO (HeapRefs term t) #

Resolve all heap pointers (i.e. IORefs) of a RState.