Safe Haskell	None
Language	Haskell2010

Language.Syntactic.Functional

Contents

Syntactic constructs
Free and bound variables
Alpha-equivalence
Evaluation

Description

Basics for implementing functional EDSLs

Synopsis

newtype Name = Name Integer
data Literal sig where
- Literal :: Show a => a -> Literal (Full a)
data Construct sig where
- Construct :: Signature sig => String -> Denotation sig -> Construct sig
data Binding sig where
- Var :: Name -> Binding (Full a)
- Lam :: Name -> Binding (b :-> Full (a -> b))
maxLam :: Project Binding s => AST s a -> Name
lam_template :: Project Binding sym => (Name -> sym (Full a)) -> (Name -> ASTF sym b -> ASTF sym (a -> b)) -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lam :: Binding :<: sym => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
fromDeBruijn :: Binding :<: sym => ASTF sym a -> ASTF sym a
data BindingT sig where
- VarT :: Typeable a => Name -> BindingT (Full a)
- LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b))
maxLamT :: Project BindingT sym => AST sym a -> Name
lamT_template :: Project BindingT sym => (Name -> sym (Full a)) -> (Name -> ASTF sym b -> ASTF sym (a -> b)) -> (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamT :: (BindingT :<: sym, Typeable a) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamTyped :: (sym ~ Typed s, BindingT :<: s, Typeable a, Typeable b) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
class BindingDomain sym where
- prVar :: sym sig -> Maybe Name
- prLam :: sym sig -> Maybe Name
- renameBind :: (Name -> Name) -> sym sig -> sym sig
data Let sig where
- Let :: String -> Let (a :-> ((a -> b) :-> Full b))
data MONAD m sig where
- Return :: MONAD m (a :-> Full (m a))
- Bind :: MONAD m (m a :-> ((a -> m b) :-> Full (m b)))
newtype Remon sym m a where
- Remon :: {..} -> Remon sym m a
desugarMonad :: (MONAD m :<: sym, Typeable a, Typeable m) => Remon sym m (ASTF sym a) -> ASTF sym (m a)
desugarMonadTyped :: (MONAD m :<: s, sym ~ Typed s, Typeable a, Typeable m) => Remon sym m (ASTF sym a) -> ASTF sym (m a)
freeVars :: BindingDomain sym => AST sym sig -> Set Name
allVars :: BindingDomain sym => AST sym sig -> Set Name
renameUnique' :: forall sym a. BindingDomain sym => [Name] -> ASTF sym a -> ASTF sym a
renameUnique :: BindingDomain sym => ASTF sym a -> ASTF sym a
type AlphaEnv = [(Name, Name)]
alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool
alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool
type family Denotation sig
class Eval s where
- evalSym :: s sig -> Denotation sig
evalDen :: Eval s => AST s sig -> Denotation sig
type family DenotationM (m :: * -> *) sig
liftDenotationM :: forall m sig proxy1 proxy2. Monad m => SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig
type RunEnv = [(Name, Dynamic)]
class EvalEnv sym env where
- compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig
compileSymDefault :: forall proxy env sym sig. Eval sym => SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig
evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a
evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a

Syntactic constructs

newtype Name Source #

Variable name

Constructors

Name Integer

Instances

Instances details

Enum Name Source #
Instance details Defined in Language.Syntactic.Functional Methods succ :: Name -> Name # pred :: Name -> Name # toEnum :: Int -> Name # fromEnum :: Name -> Int # enumFrom :: Name -> [Name] # enumFromThen :: Name -> Name -> [Name] # enumFromTo :: Name -> Name -> [Name] # enumFromThenTo :: Name -> Name -> Name -> [Name] #
Eq Name Source #
Instance details Defined in Language.Syntactic.Functional Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Integral Name Source #
Instance details Defined in Language.Syntactic.Functional Methods quot :: Name -> Name -> Name # rem :: Name -> Name -> Name # div :: Name -> Name -> Name # mod :: Name -> Name -> Name # quotRem :: Name -> Name -> (Name, Name) # divMod :: Name -> Name -> (Name, Name) # toInteger :: Name -> Integer #
Num Name Source #
Instance details Defined in Language.Syntactic.Functional Methods (+) :: Name -> Name -> Name # (-) :: Name -> Name -> Name # (*) :: Name -> Name -> Name # negate :: Name -> Name # abs :: Name -> Name # signum :: Name -> Name # fromInteger :: Integer -> Name #
Ord Name Source #
Instance details Defined in Language.Syntactic.Functional Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Real Name Source #
Instance details Defined in Language.Syntactic.Functional Methods toRational :: Name -> Rational #
Show Name Source #
Instance details Defined in Language.Syntactic.Functional Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
NFData Name Source #
Instance details Defined in Language.Syntactic.Functional Methods rnf :: Name -> () #
EvalEnv BindingT RunEnv Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig Source #

data Literal sig where Source #

Literal

Constructors

Literal :: Show a => a -> Literal (Full a)

Instances

Instances details

Symbol Literal Source #
Instance details Defined in Language.Syntactic.Functional Methods symSig :: Literal sig -> SigRep sig Source #
StringTree Literal Source #
Instance details Defined in Language.Syntactic.Functional Methods stringTreeSym :: [Tree String] -> Literal a -> Tree String Source #
Render Literal Source #
Instance details Defined in Language.Syntactic.Functional Methods renderSym :: Literal sig -> String Source # renderArgs :: [String] -> Literal sig -> String Source #
Equality Literal Source #
Instance details Defined in Language.Syntactic.Functional Methods equal :: Literal a -> Literal b -> Bool Source # hash :: Literal a -> Hash Source #
Eval Literal Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Literal sig -> Denotation sig Source #
EvalEnv Literal env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Literal sig -> DenotationM (Reader env) sig Source #

data Construct sig where Source #

Generic N-ary syntactic construct

Construct gives a quick way to introduce a syntactic construct by giving its name and semantic function.

Constructors

Construct :: Signature sig => String -> Denotation sig -> Construct sig

Instances

Instances details

Symbol Construct Source #
Instance details Defined in Language.Syntactic.Functional Methods symSig :: Construct sig -> SigRep sig Source #
StringTree Construct Source #
Instance details Defined in Language.Syntactic.Functional Methods stringTreeSym :: [Tree String] -> Construct a -> Tree String Source #
Render Construct Source #
Instance details Defined in Language.Syntactic.Functional Methods renderSym :: Construct sig -> String Source # renderArgs :: [String] -> Construct sig -> String Source #
Equality Construct Source #
Instance details Defined in Language.Syntactic.Functional Methods equal :: Construct a -> Construct b -> Bool Source # hash :: Construct a -> Hash Source #
Eval Construct Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Construct sig -> Denotation sig Source #
EvalEnv Construct env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Construct sig -> DenotationM (Reader env) sig Source #

data Binding sig where Source #

Variables and binders

Constructors

Var :: Name -> Binding (Full a)
Lam :: Name -> Binding (b :-> Full (a -> b))

Instances

Instances details

NFData1 Binding Source #
Instance details Defined in Language.Syntactic.Functional Methods rnf1 :: Binding a -> () Source #
Symbol Binding Source #
Instance details Defined in Language.Syntactic.Functional Methods symSig :: Binding sig -> SigRep sig Source #
StringTree Binding Source #
Instance details Defined in Language.Syntactic.Functional Methods stringTreeSym :: [Tree String] -> Binding a -> Tree String Source #
Render Binding Source #
Instance details Defined in Language.Syntactic.Functional Methods renderSym :: Binding sig -> String Source # renderArgs :: [String] -> Binding sig -> String Source #
Equality Binding Source #	`equal` does strict identifier comparison; i.e. no alpha equivalence. `hash` assigns the same hash to all variables and binders. This is a valid over-approximation that enables the following property: `alphaEq` a b ==> `hash` a == `hash` b
Instance details Defined in Language.Syntactic.Functional Methods equal :: Binding a -> Binding b -> Bool Source # hash :: Binding a -> Hash Source #
BindingDomain Binding Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: Binding sig -> Maybe Name Source # prLam :: Binding sig -> Maybe Name Source # renameBind :: (Name -> Name) -> Binding sig -> Binding sig Source #

maxLam :: Project Binding s => AST s a -> Name Source #

Get the highest name bound by the first Lam binders at every path from the root. If the term has ordered binders \[1\], maxLam returns the highest name introduced in the whole term.

\[1\] Ordered binders means that the names of Lam nodes are decreasing along every path from the root.

lam_template Source #

Arguments

:: Project Binding sym
=> (Name -> sym (Full a))	Variable symbol constructor
-> (Name -> ASTF sym b -> ASTF sym (a -> b))	Lambda constructor
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)

Higher-order interface for variable binding for domains based on Binding

Assumptions:

The body f does not inspect its argument.
Applying f to a term with ordered binders results in a term with ordered binders \[1\].

\[1\] Ordered binders means that the names of Lam nodes are decreasing along every path from the root.

See "Using Circular Programs for Higher-Order Syntax" (ICFP 2013, https://emilaxelsson.github.io/documents/axelsson2013using.pdf).

lam :: Binding :<: sym => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b) Source #

Higher-order interface for variable binding

This function is lamT_template specialized to domains sym satisfying (Binding :<: sym).

fromDeBruijn :: Binding :<: sym => ASTF sym a -> ASTF sym a Source #

Convert from a term with De Bruijn indexes to one with explicit names

In the argument term, variable Names are treated as De Bruijn indexes, and lambda Names are ignored. (Ideally, one should use a different type for De Bruijn terms.)

data BindingT sig where Source #

Typed variables and binders

Constructors

VarT :: Typeable a => Name -> BindingT (Full a)
LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b))

Instances

Instances details

NFData1 BindingT Source #
Instance details Defined in Language.Syntactic.Functional Methods rnf1 :: BindingT a -> () Source #
Symbol BindingT Source #
Instance details Defined in Language.Syntactic.Functional Methods symSig :: BindingT sig -> SigRep sig Source #
StringTree BindingT Source #
Instance details Defined in Language.Syntactic.Functional Methods stringTreeSym :: [Tree String] -> BindingT a -> Tree String Source #
Render BindingT Source #
Instance details Defined in Language.Syntactic.Functional Methods renderSym :: BindingT sig -> String Source # renderArgs :: [String] -> BindingT sig -> String Source #
Equality BindingT Source #	`equal` does strict identifier comparison; i.e. no alpha equivalence. `hash` assigns the same hash to all variables and binders. This is a valid over-approximation that enables the following property: `alphaEq` a b ==> `hash` a == `hash` b
Instance details Defined in Language.Syntactic.Functional Methods equal :: BindingT a -> BindingT b -> Bool Source # hash :: BindingT a -> Hash Source #
BindingDomain BindingT Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: BindingT sig -> Maybe Name Source # prLam :: BindingT sig -> Maybe Name Source # renameBind :: (Name -> Name) -> BindingT sig -> BindingT sig Source #
EvalEnv BindingT RunEnv Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig Source #

maxLamT :: Project BindingT sym => AST sym a -> Name Source #

Get the highest name bound by the first LamT binders at every path from the root. If the term has ordered binders \[1\], maxLamT returns the highest name introduced in the whole term.

\[1\] Ordered binders means that the names of LamT nodes are decreasing along every path from the root.

lamT_template Source #

Arguments

:: Project BindingT sym
=> (Name -> sym (Full a))	Variable symbol constructor
-> (Name -> ASTF sym b -> ASTF sym (a -> b))	Lambda constructor
-> (ASTF sym a -> ASTF sym b)
-> ASTF sym (a -> b)

Higher-order interface for variable binding

Assumptions:

The body f does not inspect its argument.
Applying f to a term with ordered binders results in a term with ordered binders \[1\].

\[1\] Ordered binders means that the names of LamT nodes are decreasing along every path from the root.

See "Using Circular Programs for Higher-Order Syntax" (ICFP 2013, https://emilaxelsson.github.io/documents/axelsson2013using.pdf).

lamT :: (BindingT :<: sym, Typeable a) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b) Source #

Higher-order interface for variable binding

This function is lamT_template specialized to domains sym satisfying (BindingT :<: sym).

lamTyped :: (sym ~ Typed s, BindingT :<: s, Typeable a, Typeable b) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b) Source #

Higher-order interface for variable binding

This function is lamT_template specialized to domains sym satisfying (sym ~ Typed s, BindingT :<: s).

class BindingDomain sym where Source #

Domains that "might" include variables and binders

Methods

prVar :: sym sig -> Maybe Name Source #

prLam :: sym sig -> Maybe Name Source #

renameBind :: (Name -> Name) -> sym sig -> sym sig Source #

Rename a variable or a lambda (no effect for other symbols)

Instances

Instances details

BindingDomain sym Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: sym sig -> Maybe Name Source # prLam :: sym sig -> Maybe Name Source # renameBind :: (Name -> Name) -> sym sig -> sym sig Source #
BindingDomain BindingT Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: BindingT sig -> Maybe Name Source # prLam :: BindingT sig -> Maybe Name Source # renameBind :: (Name -> Name) -> BindingT sig -> BindingT sig Source #
BindingDomain Binding Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: Binding sig -> Maybe Name Source # prLam :: Binding sig -> Maybe Name Source # renameBind :: (Name -> Name) -> Binding sig -> Binding sig Source #
BindingDomain sym => BindingDomain (Typed sym) Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: Typed sym sig -> Maybe Name Source # prLam :: Typed sym sig -> Maybe Name Source # renameBind :: (Name -> Name) -> Typed sym sig -> Typed sym sig Source #
BindingDomain sym => BindingDomain (AST sym) Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: AST sym sig -> Maybe Name Source # prLam :: AST sym sig -> Maybe Name Source # renameBind :: (Name -> Name) -> AST sym sig -> AST sym sig Source #
(BindingDomain sym1, BindingDomain sym2) => BindingDomain (sym1 :+: sym2) Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: (sym1 :+: sym2) sig -> Maybe Name Source # prLam :: (sym1 :+: sym2) sig -> Maybe Name Source # renameBind :: (Name -> Name) -> (sym1 :+: sym2) sig -> (sym1 :+: sym2) sig Source #
BindingDomain sym => BindingDomain (sym :&: i) Source #
Instance details Defined in Language.Syntactic.Functional Methods prVar :: (sym :&: i) sig -> Maybe Name Source # prLam :: (sym :&: i) sig -> Maybe Name Source # renameBind :: (Name -> Name) -> (sym :&: i) sig -> (sym :&: i) sig Source #

data Let sig where Source #

A symbol for let bindings

This symbol is just an application operator. The actual binding has to be done by a lambda that constructs the second argument.

The provided string is just a tag and has nothing to do with the name of the variable of the second argument (if that argument happens to be a lambda). However, a back end may use the tag to give a sensible name to the generated variable.

The string tag may be empty.

Constructors

Let :: String -> Let (a :-> ((a -> b) :-> Full b))

Instances

Instances details

Symbol Let Source #
Instance details Defined in Language.Syntactic.Functional Methods symSig :: Let sig -> SigRep sig Source #
StringTree Let Source #
Instance details Defined in Language.Syntactic.Functional Methods stringTreeSym :: [Tree String] -> Let a -> Tree String Source #
Render Let Source #
Instance details Defined in Language.Syntactic.Functional Methods renderSym :: Let sig -> String Source # renderArgs :: [String] -> Let sig -> String Source #
Equality Let Source #
Instance details Defined in Language.Syntactic.Functional Methods equal :: Let a -> Let b -> Bool Source # hash :: Let a -> Hash Source #
Eval Let Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Let sig -> Denotation sig Source #
EvalEnv Let env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Let sig -> DenotationM (Reader env) sig Source #

data MONAD m sig where Source #

Monadic constructs

See "Generic Monadic Constructs for Embedded Languages" (Persson et al., IFL 2011 https://emilaxelsson.github.io/documents/persson2011generic.pdf).

Constructors

Return :: MONAD m (a :-> Full (m a))
Bind :: MONAD m (m a :-> ((a -> m b) :-> Full (m b)))

Instances

Instances details

Symbol (MONAD m) Source #
Instance details Defined in Language.Syntactic.Functional Methods symSig :: MONAD m sig -> SigRep sig Source #
StringTree (MONAD m) Source #
Instance details Defined in Language.Syntactic.Functional Methods stringTreeSym :: [Tree String] -> MONAD m a -> Tree String Source #
Render (MONAD m) Source #
Instance details Defined in Language.Syntactic.Functional Methods renderSym :: MONAD m sig -> String Source # renderArgs :: [String] -> MONAD m sig -> String Source #
Equality (MONAD m) Source #
Instance details Defined in Language.Syntactic.Functional Methods equal :: MONAD m a -> MONAD m b -> Bool Source # hash :: MONAD m a -> Hash Source #
Monad m => Eval (MONAD m) Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: MONAD m sig -> Denotation sig Source #
Monad m => EvalEnv (MONAD m) env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> MONAD m sig -> DenotationM (Reader env) sig Source #

newtype Remon sym m a where Source #

Reifiable monad

See "Generic Monadic Constructs for Embedded Languages" (Persson et al., IFL 2011 https://emilaxelsson.github.io/documents/persson2011generic.pdf).

It is advised to convert to/from Remon using the Syntactic instance provided in the modules Language.Syntactic.Sugar.Monad or Language.Syntactic.Sugar.MonadT.

Constructors

Remon
Fields :: { unRemon :: forall r. Typeable r => Cont (ASTF sym (m r)) a } -> Remon sym m a

Instances

Instances details

Monad (Remon dom m) Source #
Instance details Defined in Language.Syntactic.Functional Methods (>>=) :: Remon dom m a -> (a -> Remon dom m b) -> Remon dom m b # (>>) :: Remon dom m a -> Remon dom m b -> Remon dom m b # return :: a -> Remon dom m a #
Functor (Remon sym m) Source #
Instance details Defined in Language.Syntactic.Functional Methods fmap :: (a -> b) -> Remon sym m a -> Remon sym m b # (<$) :: a -> Remon sym m b -> Remon sym m a #
Applicative (Remon sym m) Source #
Instance details Defined in Language.Syntactic.Functional Methods pure :: a -> Remon sym m a # (<>) :: Remon sym m (a -> b) -> Remon sym m a -> Remon sym m b # liftA2 :: (a -> b -> c) -> Remon sym m a -> Remon sym m b -> Remon sym m c # (>) :: Remon sym m a -> Remon sym m b -> Remon sym m b # (<*) :: Remon sym m a -> Remon sym m b -> Remon sym m a #
(sym ~ Typed s, Syntactic a, Domain a ~ sym, BindingT :<: s, MONAD m :<: s, Typeable m, Typeable (Internal a)) => Syntactic (Remon sym m a) Source #
Instance details Defined in Language.Syntactic.Sugar.MonadTyped Associated Types type Domain (Remon sym m a) :: Type -> Type Source # type Internal (Remon sym m a) Source # Methods desugar :: Remon sym m a -> ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a)) Source # sugar :: ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a)) -> Remon sym m a Source #
(Syntactic a, Domain a ~ sym, Binding :<: sym, MONAD m :<: sym, Typeable m, Typeable (Internal a)) => Syntactic (Remon sym m a) Source #
Instance details Defined in Language.Syntactic.Sugar.Monad Associated Types type Domain (Remon sym m a) :: Type -> Type Source # type Internal (Remon sym m a) Source # Methods desugar :: Remon sym m a -> ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a)) Source # sugar :: ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a)) -> Remon sym m a Source #
type Domain (Remon sym m a) Source #
Instance details Defined in Language.Syntactic.Sugar.MonadTyped type Domain (Remon sym m a) = sym
type Domain (Remon sym m a) Source #
Instance details Defined in Language.Syntactic.Sugar.Monad type Domain (Remon sym m a) = sym
type Internal (Remon sym m a) Source #
Instance details Defined in Language.Syntactic.Sugar.MonadTyped type Internal (Remon sym m a) = m (Internal a)
type Internal (Remon sym m a) Source #
Instance details Defined in Language.Syntactic.Sugar.Monad type Internal (Remon sym m a) = m (Internal a)

desugarMonad :: (MONAD m :<: sym, Typeable a, Typeable m) => Remon sym m (ASTF sym a) -> ASTF sym (m a) Source #

One-layer desugaring of monadic actions

desugarMonadTyped :: (MONAD m :<: s, sym ~ Typed s, Typeable a, Typeable m) => Remon sym m (ASTF sym a) -> ASTF sym (m a) Source #

One-layer desugaring of monadic actions

Free and bound variables

freeVars :: BindingDomain sym => AST sym sig -> Set Name Source #

Get the set of free variables in an expression

allVars :: BindingDomain sym => AST sym sig -> Set Name Source #

Get the set of variables (free, bound and introduced by lambdas) in an expression

renameUnique' :: forall sym a. BindingDomain sym => [Name] -> ASTF sym a -> ASTF sym a Source #

Rename the bound variables in a term

The free variables are left untouched. The bound variables are given unique names using as small names as possible. The first argument is a list of reserved names. Reserved names and names of free variables are not used when renaming bound variables.

renameUnique :: BindingDomain sym => ASTF sym a -> ASTF sym a Source #

Rename the bound variables in a term

The free variables are left untouched. The bound variables are given unique names using as small names as possible. Names of free variables are not used when renaming bound variables.

Alpha-equivalence

type AlphaEnv = [(Name, Name)] Source #

Environment used by alphaEq'

alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool Source #

alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool Source #

Alpha-equivalence

Evaluation

type family Denotation sig Source #

Semantic function type of the given symbol signature

Instances

Instances details

type Denotation (Full a) Source #
Instance details Defined in Language.Syntactic.Functional type Denotation (Full a) = a
type Denotation (a :-> sig) Source #
Instance details Defined in Language.Syntactic.Functional type Denotation (a :-> sig) = a -> Denotation sig

class Eval s where Source #

Methods

evalSym :: s sig -> Denotation sig Source #

Instances

Instances details

Eval Empty Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Empty sig -> Denotation sig Source #
Eval Let Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Let sig -> Denotation sig Source #
Eval Construct Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Construct sig -> Denotation sig Source #
Eval Literal Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: Literal sig -> Denotation sig Source #
Eval BindingWS Source #
Instance details Defined in Language.Syntactic.Functional.WellScoped Methods evalSym :: BindingWS sig -> Denotation sig Source #
Eval Tuple Source #
Instance details Defined in Language.Syntactic.Functional.Tuple Methods evalSym :: Tuple sig -> Denotation sig Source #
Monad m => Eval (MONAD m) Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: MONAD m sig -> Denotation sig Source #
Eval sym => Eval (ReaderSym sym) Source #
Instance details Defined in Language.Syntactic.Functional.WellScoped Methods evalSym :: ReaderSym sym sig -> Denotation sig Source #
(Eval s, Eval t) => Eval (s :+: t) Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: (s :+: t) sig -> Denotation sig Source #
Eval sym => Eval (sym :&: info) Source #
Instance details Defined in Language.Syntactic.Functional Methods evalSym :: (sym :&: info) sig -> Denotation sig Source #

evalDen :: Eval s => AST s sig -> Denotation sig Source #

Evaluation

type family DenotationM (m :: * -> *) sig Source #

Monadic denotation; mapping from a symbol signature

a :-> b :-> Full c

to

m a -> m b -> m c

Instances

Instances details

type DenotationM m (Full a) Source #
Instance details Defined in Language.Syntactic.Functional type DenotationM m (Full a) = m a
type DenotationM m (a :-> sig) Source #
Instance details Defined in Language.Syntactic.Functional type DenotationM m (a :-> sig) = m a -> DenotationM m sig

liftDenotationM :: forall m sig proxy1 proxy2. Monad m => SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig Source #

Lift a Denotation to DenotationM

type RunEnv = [(Name, Dynamic)] Source #

Runtime environment

class EvalEnv sym env where Source #

Evaluation

Minimal complete definition

Nothing

Methods

compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig Source #

default compileSym :: (Symbol sym, Eval sym) => proxy env -> sym sig -> DenotationM (Reader env) sig Source #

Instances

Instances details

EvalEnv Empty env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Empty sig -> DenotationM (Reader env) sig Source #
EvalEnv Let env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Let sig -> DenotationM (Reader env) sig Source #
EvalEnv BindingT RunEnv Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig Source #
EvalEnv Construct env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Construct sig -> DenotationM (Reader env) sig Source #
EvalEnv Literal env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Literal sig -> DenotationM (Reader env) sig Source #
EvalEnv Tuple env Source #
Instance details Defined in Language.Syntactic.Functional.Tuple Methods compileSym :: proxy env -> Tuple sig -> DenotationM (Reader env) sig Source #
EvalEnv sym env => EvalEnv (Typed sym) env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> Typed sym sig -> DenotationM (Reader env) sig Source #
Monad m => EvalEnv (MONAD m) env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> MONAD m sig -> DenotationM (Reader env) sig Source #
(EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv (sym1 :+: sym2) env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> (sym1 :+: sym2) sig -> DenotationM (Reader env) sig Source #
EvalEnv sym env => EvalEnv (sym :&: info) env Source #
Instance details Defined in Language.Syntactic.Functional Methods compileSym :: proxy env -> (sym :&: info) sig -> DenotationM (Reader env) sig Source #

compileSymDefault :: forall proxy env sym sig. Eval sym => SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig Source #

Simple implementation of compileSym from a Denotation

evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a Source #

Evaluation of open terms

evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a Source #

Evaluation of closed terms where RunEnv is used as the internal environment

(Note that there is no guarantee that the term is actually closed.)