LAM-0.1.0.0

Safe Haskell	Safe-Inferred
Language	Haskell2010

LAM.Types.Generic

Description

Generic term type and functions.

Synopsis

type Name = Text
type family XVar a
type family XLet a
type family XExt a
data ETerm d
- = Var (XVar d)
- | Lam Name (ETerm d)
- | App (ETerm d) (XVar d)
- | XLet (XLet d) [(Name, ETerm d)] (ETerm d)
- | Ext !(XExt d)
pattern Let :: XLet d ~ () => [(Name, ETerm d)] -> ETerm d -> ETerm d
showTermWithCtx :: (XVar d ~ Name, XLet d ~ ()) => (XExt d -> String) -> (Name -> String) -> ETerm d -> String
fromDBTermCtx :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ ()) => (XExt d2 -> XExt d1) -> [Name] -> ETerm d2 -> ETerm d1
fromDBTerm :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ (), XExt d1 ~ XExt d2) => ETerm d2 -> ETerm d1
toDBTermCtx :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ ()) => (XExt d1 -> XExt d2) -> [Name] -> ETerm d1 -> ETerm d2
toDBTerm :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ ()) => (XExt d1 -> XExt d2) -> ETerm d1 -> ETerm d2

Documentation

type Name = Text #

Variable names.

type family XVar a #

Type family for variable names.

Instances

Instances details

type XVar Trim0 #
Instance details Defined in LAM.Trim type XVar Trim0 = Int
type XVar BV #
Instance details Defined in LAM.Types.BV type XVar BV = Name
type XVar BVDB #
Instance details Defined in LAM.Types.BV type XVar BVDB = Int
type XVar Base #
Instance details Defined in LAM.Types.Pure type XVar Base = Name
type XVar DB #
Instance details Defined in LAM.Types.Pure type XVar DB = Int

type family XLet a #

Type family for extra information at let bindings (usually trimmers).

Instances

Instances details

type XLet Trim0 #
Instance details Defined in LAM.Trim type XLet Trim0 = (Trimmer0, [Trimmer0])
type XLet BV #
Instance details Defined in LAM.Types.BV type XLet BV = ()
type XLet BVDB #
Instance details Defined in LAM.Types.BV type XLet BVDB = ()
type XLet Base #
Instance details Defined in LAM.Types.Pure type XLet Base = ()
type XLet DB #
Instance details Defined in LAM.Types.Pure type XLet DB = ()

type family XExt a #

Type family for extra constructors (like base values).

Instances

Instances details

type XExt Trim0 #
Instance details Defined in LAM.Trim type XExt Trim0 = Void
type XExt BV #
Instance details Defined in LAM.Types.BV type XExt BV = BVCtrs
type XExt BVDB #
Instance details Defined in LAM.Types.BV type XExt BVDB = BVDBCtrs
type XExt Base #
Instance details Defined in LAM.Types.Pure type XExt Base = Void
type XExt DB #
Instance details Defined in LAM.Types.Pure type XExt DB = Void

data ETerm d #

Generic term datatype.

Constructors

Var (XVar d)
Lam Name (ETerm d)
App (ETerm d) (XVar d)
XLet (XLet d) [(Name, ETerm d)] (ETerm d)
Ext !(XExt d)

Instances

Instances details

Show BVDBTerm #

Instance details

Defined in LAM.Types.BV

Methods

showsPrec :: Int -> BVDBTerm -> ShowS #

show :: BVDBTerm -> String #

showList :: [BVDBTerm] -> ShowS #

Instance details

Defined in LAM.Types.BV

Methods

showsPrec :: Int -> BVTerm -> ShowS #

show :: BVTerm -> String #

showList :: [BVTerm] -> ShowS #

Instance details

Defined in LAM.Types.Pure

Methods

showsPrec :: Int -> DBTerm -> ShowS #

show :: DBTerm -> String #

showList :: [DBTerm] -> ShowS #

Instance details

Defined in LAM.Types.Pure

Methods

showsPrec :: Int -> Term -> ShowS #

show :: Term -> String #

showList :: [Term] -> ShowS #

CanTrim DBTerm NamedList #

Instance details

Defined in LAM.CanTrim

Methods

trim :: Closure DBTerm NamedList -> Closure DBTerm NamedList #

CanTrim DBTerm Seq #

Instance details

Defined in LAM.Exec.DBNoTrimPure

Methods

trim :: Closure DBTerm Seq -> Closure DBTerm Seq #

CanTrim DBTerm Vector #

Instance details

Defined in LAM.Exec.DBNoTrimPure

Methods

trim :: Closure DBTerm Vector -> Closure DBTerm Vector #

CanTrim DBTerm [] #

Instance details

Defined in LAM.Exec.DBNoTrimPure

Methods

trim :: Closure DBTerm [] -> Closure DBTerm [] #

CanTrim Term NamedList #

Instance details

Defined in LAM.CanTrim

Methods

trim :: Closure Term NamedList -> Closure Term NamedList #

CanTrim Term Trie #

Instance details

Defined in LAM.CanTrim

Methods

trim :: Closure Term Trie -> Closure Term Trie #

Generic (ETerm d) #

Instance details

Defined in LAM.Types.Generic

Associated Types

type Rep (ETerm d)

Instance details

Defined in LAM.Types.Generic

type Rep (ETerm d) = D1 ('MetaData "ETerm" "LAM.Types.Generic" "LAM-0.1.0.0-inplace" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (XVar d))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ETerm d)))) :+: (C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ETerm d)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (XVar d))) :+: (C1 ('MetaCons "XLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (XLet d)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, ETerm d)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ETerm d)))) :+: C1 ('MetaCons "Ext" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (XExt d))))))

Methods

from :: ETerm d -> Rep (ETerm d) x #

to :: Rep (ETerm d) x -> ETerm d #

(Eq (XVar a), Eq (XLet a), Eq (XExt a)) => Eq (ETerm a) #

Instance details

Defined in LAM.Types.Generic

Methods

(==) :: ETerm a -> ETerm a -> Bool #

(/=) :: ETerm a -> ETerm a -> Bool #

(Ord (XVar a), Ord (XLet a), Ord (XExt a)) => Ord (ETerm a) #

Instance details

Defined in LAM.Types.Generic

Methods

compare :: ETerm a -> ETerm a -> Ordering #

(<) :: ETerm a -> ETerm a -> Bool #

(<=) :: ETerm a -> ETerm a -> Bool #

(>) :: ETerm a -> ETerm a -> Bool #

(>=) :: ETerm a -> ETerm a -> Bool #

max :: ETerm a -> ETerm a -> ETerm a #

min :: ETerm a -> ETerm a -> ETerm a #

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) #

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 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) #

type Rep (ETerm d) #

Instance details

Defined in LAM.Types.Generic

type Rep (ETerm d) = D1 ('MetaData "ETerm" "LAM.Types.Generic" "LAM-0.1.0.0-inplace" 'False) ((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (XVar d))) :+: C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ETerm d)))) :+: (C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ETerm d)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (XVar d))) :+: (C1 ('MetaCons "XLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (XLet d)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Name, ETerm d)]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ETerm d)))) :+: C1 ('MetaCons "Ext" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (XExt d))))))

pattern Let :: XLet d ~ () => [(Name, ETerm d)] -> ETerm d -> ETerm d #

Without extra data on XLet, we can have a simplified pattern.

showTermWithCtx :: (XVar d ~ Name, XLet d ~ ()) => (XExt d -> String) -> (Name -> String) -> ETerm d -> String #

Show a term, with a special function to show free variables.

fromDBTermCtx :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ ()) => (XExt d2 -> XExt d1) -> [Name] -> ETerm d2 -> ETerm d1 #

Convert from DeBruijn to named representation in a context.

fromDBTerm :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ (), XExt d1 ~ XExt d2) => ETerm d2 -> ETerm d1 #

Convert from DeBruijn to named representation.

toDBTermCtx :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ ()) => (XExt d1 -> XExt d2) -> [Name] -> ETerm d1 -> ETerm d2 #

Convert from named to DeBruijn representation in a context.

toDBTerm :: (XVar d1 ~ Name, XVar d2 ~ Int, XLet d2 ~ (), XLet d1 ~ ()) => (XExt d1 -> XExt d2) -> ETerm d1 -> ETerm d2 #

Convert from named to DeBruijn representation.