Language.Syntactic.Syntax

Generic representation of typed syntax trees

For details, see: A Generic Abstract Syntax Model for Embedded Languages (ICFP 2012, http://www.cse.chalmers.se/~emax/documents/axelsson2012generic.pdf).

Syntax trees

data AST dom sig where

Generic abstract syntax tree, parameterized by a symbol domain

(AST dom (a :-> b)) represents a partially applied (or unapplied) symbol, missing at least one argument, while (AST dom (Full a)) represents a fully applied symbol, i.e. a complete syntax tree.

Constructors

Sym :: dom sig -> AST dom sig

(:$) :: AST dom (a :-> sig) -> AST dom (Full a) -> AST dom sig infixl 1

Instances

sub :<: sup => sub :<: (AST sup)

Defined in Language.Syntactic.Syntax

Methods

inj :: sub a -> AST sup a

Project sub sup => Project sub (AST sup)

Defined in Language.Syntactic.Syntax

Methods

prj :: AST sup a -> Maybe (sub a)

(InjectC sub sup a, Sat (AST sup) a) => InjectC sub (AST sup) a

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => sub sig -> AST sup sig

Functor dom => Functor (AST dom)

Defined in Language.Syntactic.Syntax

Methods

fmap :: (a -> b) -> AST dom a -> AST dom b

(<$) :: a -> AST dom b -> AST dom a

Eval dom => Eval (AST dom)

Defined in Language.Syntactic.Interpretation.Evaluation

Methods

evaluate :: AST dom a -> Denotation a

Equality dom => Equality (AST dom)

Defined in Language.Syntactic.Interpretation.Equality

Methods

equal :: AST dom a -> AST dom b -> Bool

exprHash :: AST dom a -> Hash

Constrained dom => Constrained (AST dom)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (AST dom) :: * -> Constraint

Methods

exprDict :: AST dom a -> Dict (Sat (AST dom) (DenResult a))

ApplySym (Full a) (ASTF dom a) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (Full a) -> ASTF dom a

Equality dom => Eq (AST dom a)

Defined in Language.Syntactic.Interpretation.Equality

Methods

(==) :: AST dom a -> AST dom a -> Bool

(/=) :: AST dom a -> AST dom a -> Bool

Render dom => Show (ASTF dom a)

Defined in Language.Syntactic.Interpretation.Render

Methods

showsPrec :: Int -> ASTF dom a -> ShowS

show :: ASTF dom a -> String

showList :: [ASTF dom a] -> ShowS

Syntactic (ASTF dom a)

Defined in Language.Syntactic.Sugar

Associated Types

type Domain (ASTF dom a) :: * -> *

type Internal (ASTF dom a) :: *

Methods

desugar :: ASTF dom a -> ASTF (Domain (ASTF dom a)) (Internal (ASTF dom a))

sugar :: ASTF (Domain (ASTF dom a)) (Internal (ASTF dom a)) -> ASTF dom a

(Syntactic a, Domain a ~ dom, ia ~ Internal a, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib)

Defined in Language.Syntactic.Sugar

Methods

desugarN :: (a -> b) -> AST dom (Full ia) -> ib

sugarN :: (AST dom (Full ia) -> ib) -> a -> b

ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (a :-> sig) -> ASTF dom a -> f

type Sat (AST dom)

Defined in Language.Syntactic.Constraint

type Sat (AST dom) = Sat dom

type Domain (ASTF dom a)

Defined in Language.Syntactic.Sugar

type Domain (ASTF dom a) = dom

type Internal (ASTF dom a)

Defined in Language.Syntactic.Sugar

type Internal (ASTF dom a) = a

type ASTF dom a = AST dom (Full a)

Fully applied abstract syntax tree

newtype Full a

Signature of a fully applied symbol

Constructors

Full

Fields

• result :: a

Instances

Functor Full

Defined in Language.Syntactic.Syntax

Methods

fmap :: (a -> b) -> Full a -> Full b

(<$) :: a -> Full b -> Full a

Eq a => Eq (Full a)

Defined in Language.Syntactic.Syntax

Methods

(==) :: Full a -> Full a -> Bool

(/=) :: Full a -> Full a -> Bool

Show a => Show (Full a)

Defined in Language.Syntactic.Syntax

Methods

showsPrec :: Int -> Full a -> ShowS

show :: Full a -> String

showList :: [Full a] -> ShowS

ApplySym (Full a) (ASTF dom a) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (Full a) -> ASTF dom a

Render dom => Show (ASTF dom a)

Defined in Language.Syntactic.Interpretation.Render

Methods

showsPrec :: Int -> ASTF dom a -> ShowS

show :: ASTF dom a -> String

showList :: [ASTF dom a] -> ShowS

Syntactic (ASTF dom a)

Defined in Language.Syntactic.Sugar

Associated Types

type Domain (ASTF dom a) :: * -> *

type Internal (ASTF dom a) :: *

Methods

desugar :: ASTF dom a -> ASTF (Domain (ASTF dom a)) (Internal (ASTF dom a))

sugar :: ASTF (Domain (ASTF dom a)) (Internal (ASTF dom a)) -> ASTF dom a

(Syntactic a, Domain a ~ dom, ia ~ Internal a, SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib)

Defined in Language.Syntactic.Sugar

Methods

desugarN :: (a -> b) -> AST dom (Full ia) -> ib

sugarN :: (AST dom (Full ia) -> ib) -> a -> b

ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (a :-> sig) -> ASTF dom a -> f

type DenResult (Full a)

Defined in Language.Syntactic.Syntax

type DenResult (Full a) = a

type Denotation (Full a)

Defined in Language.Syntactic.Interpretation.Semantics

type Denotation (Full a) = a

type Domain (ASTF dom a)

Defined in Language.Syntactic.Sugar

type Domain (ASTF dom a) = dom

type Internal (ASTF dom a)

Defined in Language.Syntactic.Sugar

type Internal (ASTF dom a) = a

newtype a :-> sig infixr 9

Signature of a partially applied (or unapplied) symbol

Constructors

Partial (a -> sig)

Instances

Functor ((:->) a)

Defined in Language.Syntactic.Syntax

Methods

fmap :: (a0 -> b) -> (a :-> a0) -> a :-> b

(<$) :: a0 -> (a :-> b) -> a :-> a0

ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (a :-> sig) -> ASTF dom a -> f

type DenResult (a :-> sig)

Defined in Language.Syntactic.Syntax

type DenResult (a :-> sig) = DenResult sig

type Denotation (a :-> sig)

Defined in Language.Syntactic.Interpretation.Semantics

type Denotation (a :-> sig) = a -> Denotation sig

size :: AST dom sig -> Int

Count the number of symbols in an expression

class ApplySym sig f dom | sig dom -> f, f -> sig dom where

Class for the type-level recursion needed by appSym

Minimal complete definition

appSym'

Methods

appSym' :: AST dom sig -> f

Instances

ApplySym (Full a) (ASTF dom a) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (Full a) -> ASTF dom a

ApplySym sig f dom => ApplySym (a :-> sig) (ASTF dom a -> f) dom

Defined in Language.Syntactic.Syntax

Methods

appSym' :: AST dom (a :-> sig) -> ASTF dom a -> f

type family DenResult sig

The result type of a symbol with the given signature

Instances

type DenResult (Full a)

Defined in Language.Syntactic.Syntax

type DenResult (Full a) = a

type DenResult (a :-> sig)

Defined in Language.Syntactic.Syntax

type DenResult (a :-> sig) = DenResult sig

Symbol domains

data (dom1 :+: dom2) a where infixr 9

Direct sum of two symbol domains

Constructors

InjL :: dom1 a -> (dom1 :+: dom2) a

InjR :: dom2 a -> (dom1 :+: dom2) a

Instances

expr1 :<: expr3 => expr1 :<: (expr2 :+: expr3)

Defined in Language.Syntactic.Syntax

Methods

inj :: expr1 a -> (expr2 :+: expr3) a

expr1 :<: (expr1 :+: expr2)

Defined in Language.Syntactic.Syntax

Methods

inj :: expr1 a -> (expr1 :+: expr2) a

Project expr1 expr3 => Project expr1 (expr2 :+: expr3)

Defined in Language.Syntactic.Syntax

Methods

prj :: (expr2 :+: expr3) a -> Maybe (expr1 a)

Project expr1 (expr1 :+: expr2)

Defined in Language.Syntactic.Syntax

Methods

prj :: (expr1 :+: expr2) a -> Maybe (expr1 a)

InjectC expr1 expr3 a => InjectC expr1 (expr2 :+: expr3) a

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => expr1 sig -> (expr2 :+: expr3) sig

InjectC expr1 (expr1 :+: expr2) a

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => expr1 sig -> (expr1 :+: expr2) sig

(Functor dom1, Functor dom2) => Functor (dom1 :+: dom2)

Defined in Language.Syntactic.Syntax

Methods

fmap :: (a -> b) -> (dom1 :+: dom2) a -> (dom1 :+: dom2) b

(<$) :: a -> (dom1 :+: dom2) b -> (dom1 :+: dom2) a

(StringTree dom1, StringTree dom2) => StringTree (dom1 :+: dom2)

Defined in Language.Syntactic.Interpretation.Render

Methods

stringTreeSym :: [Tree String] -> (dom1 :+: dom2) a -> Tree String

(Render expr1, Render expr2) => Render (expr1 :+: expr2)

Defined in Language.Syntactic.Interpretation.Render

Methods

renderSym :: (expr1 :+: expr2) sig -> String

renderArgs :: [String] -> (expr1 :+: expr2) sig -> String

(Eval expr1, Eval expr2) => Eval (expr1 :+: expr2)

Defined in Language.Syntactic.Interpretation.Evaluation

Methods

evaluate :: (expr1 :+: expr2) a -> Denotation a

(Equality expr1, Equality expr2) => Equality (expr1 :+: expr2)

Defined in Language.Syntactic.Interpretation.Equality

Methods

equal :: (expr1 :+: expr2) a -> (expr1 :+: expr2) b -> Bool

exprHash :: (expr1 :+: expr2) a -> Hash

Constrained (sub1 :+: sub2)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (sub1 :+: sub2) :: * -> Constraint

Methods

exprDict :: (sub1 :+: sub2) a -> Dict (Sat (sub1 :+: sub2) (DenResult a))

(EvalBind sub1, EvalBind sub2) => EvalBind (sub1 :+: sub2)

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => (sub1 :+: sub2) sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

(Optimize sub1, Optimize sub2) => Optimize (sub1 :+: sub2)

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom => ConstFolder dom -> ((sub1 :+: sub2) sig -> AST dom sig) -> (sub1 :+: sub2) sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig))

TupleSat dom2 p => TupleSat (dom1 :+: dom2) p

Defined in Language.Syntactic.Frontend.TupleConstrained

TupleSat ((Tuple :|| p) :+: dom2) p

Defined in Language.Syntactic.Frontend.TupleConstrained

TupleSat ((Select :|| p) :+: dom2) p

Defined in Language.Syntactic.Frontend.TupleConstrained

(AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq (subA1 :+: subA2) (subB1 :+: subB2) dom env

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: (subA1 :+: subA2) a -> Args (AST dom) a -> (subB1 :+: subB2) b -> Args (AST dom) b -> Reader env Bool

(Equality expr1, Equality expr2) => Eq ((expr1 :+: expr2) a)

Defined in Language.Syntactic.Interpretation.Equality

Methods

(==) :: (expr1 :+: expr2) a -> (expr1 :+: expr2) a -> Bool

(/=) :: (expr1 :+: expr2) a -> (expr1 :+: expr2) a -> Bool

IsHODomain (HODomain dom p pVar) p pVar

Defined in Language.Syntactic.Constructs.Binding.HigherOrder

Methods

lambda :: (p (a -> b), p a, pVar a) => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b) -> ASTF (HODomain dom p pVar) (a -> b)

type Sat (sub1 :+: sub2)

Defined in Language.Syntactic.Constraint

type Sat (sub1 :+: sub2) = Top

class Project sub sup where

Symbol projection

Minimal complete definition

prj

Methods

prj :: sup a -> Maybe (sub a)

Partial projection from sup to sub

Instances

Project expr expr

Defined in Language.Syntactic.Syntax

Methods

prj :: expr a -> Maybe (expr a)

Project sub sup => Project sub (AST sup)

Defined in Language.Syntactic.Syntax

Methods

prj :: AST sup a -> Maybe (sub a)

Project expr1 expr3 => Project expr1 (expr2 :+: expr3)

Defined in Language.Syntactic.Syntax

Methods

prj :: (expr2 :+: expr3) a -> Maybe (expr1 a)

Project expr1 (expr1 :+: expr2)

Defined in Language.Syntactic.Syntax

Methods

prj :: (expr1 :+: expr2) a -> Maybe (expr1 a)

Project sub sup => Project sub (sup :|| pred)

Defined in Language.Syntactic.Constraint

Methods

prj :: (sup :|| pred) a -> Maybe (sub a)

Project sub sup => Project sub (sup :| pred)

Defined in Language.Syntactic.Constraint

Methods

prj :: (sup :| pred) a -> Maybe (sub a)

Project sub sup => Project sub (Decor info sup)

Defined in Language.Syntactic.Constructs.Decoration

Methods

prj :: Decor info sup a -> Maybe (sub a)

Project sub sup => Project sub (SubConstr1 c sup p)

Defined in Language.Syntactic.Constraint

Methods

prj :: SubConstr1 c sup p a -> Maybe (sub a)

Project sub sup => Project sub (SubConstr2 c sup pa pb)

Defined in Language.Syntactic.Constraint

Methods

prj :: SubConstr2 c sup pa pb a -> Maybe (sub a)

class Project sub sup => sub :<: sup where

Symbol subsumption

Minimal complete definition

inj

Methods

inj :: sub a -> sup a

Injection from sub to sup

Instances

expr :<: expr

Defined in Language.Syntactic.Syntax

Methods

inj :: expr a -> expr a

sub :<: sup => sub :<: (AST sup)

Defined in Language.Syntactic.Syntax

Methods

inj :: sub a -> AST sup a

expr1 :<: expr3 => expr1 :<: (expr2 :+: expr3)

Defined in Language.Syntactic.Syntax

Methods

inj :: expr1 a -> (expr2 :+: expr3) a

expr1 :<: (expr1 :+: expr2)

Defined in Language.Syntactic.Syntax

Methods

inj :: expr1 a -> (expr1 :+: expr2) a

appSym :: (ApplySym sig f dom, sym :<: AST dom) => sym sig -> f

Generic symbol application

appSym has any type of the form:

appSym :: (expr :<: AST dom)
    => expr (a :-> b :-> ... :-> Full x)
    -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)

Type inference

symType :: P sym -> sym sig -> sym sig

Constrain a symbol to a specific type

prjP :: Project sub sup => P sub -> sup sig -> Maybe (sub sig)

Projection to a specific symbol type