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

Instances

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

Project sub sup => Project sub (AST sup)

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

Equality dom => Equality (AST dom)

(Render (AST dom), ToTree dom) => ToTree (AST dom)

Render dom => Render (AST dom)

Eval dom => Eval (AST dom)

Constrained dom => Constrained (AST dom)

ApplySym (Full a) (ASTF dom a) dom

Equality dom => Eq (AST dom a)

Render dom => Show (AST dom a)

Syntactic (ASTF dom a) dom

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

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

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

Typeable1 Full

Eq a => Eq (Full a)

Show a => Show (Full a)

ApplySym (Full a) (ASTF dom a) dom

Syntactic (ASTF dom a) dom

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

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

newtype a :-> sig

Signature of a partially applied (or unapplied) symbol

Constructors

Partial (a -> sig)

Instances

Typeable2 :->

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

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

Methods

appSym' :: AST dom sig -> f

Instances

ApplySym (Full a) (ASTF dom a) dom

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

type family DenResult sig

The result type of a symbol with the given signature

Symbol domains

data (dom1 :+: dom2) a where

Direct sum of two symbol domains

Constructors

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

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

Instances

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

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

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

Project expr1 (:+: expr1 expr2)

(Project expr1 (:+: expr2 expr3), Sat (:+: expr2 expr3) a, InjectC expr1 expr3 a) => InjectC expr1 (:+: expr2 expr3) a

(Project expr1 (:+: expr1 expr2), Sat (:+: expr1 expr2) a) => InjectC expr1 (:+: expr1 expr2) a

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

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

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

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

Constrained (:+: sub1 sub2)

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

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

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

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

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

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

(Syntactic a (HODomain dom p pVar), Syntactic b (HODomain dom p pVar), p (Internal a -> Internal b), p (Internal a), pVar (Internal a)) => Syntactic (a -> b) (HODomain dom p pVar)

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

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

(Syntactic a (HODomain dom Typeable pVar), InjectC (MONAD m) dom (m (Internal a)), Monad m, Typeable1 m, Typeable (Internal a), pVar (Internal a)) => Syntactic (Mon dom pVar m a) (HODomain dom Typeable pVar)

class Project sub sup where

Symbol projection

Methods

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

Partial projection from sup to sub

Instances

Project expr expr

Project sub sup => Project sub (AST sup)

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

Project expr1 (:+: expr1 expr2)

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

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

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

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

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

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

Symbol subsumption

Methods

inj :: sub a -> sup a

Injection from sub to sup

Instances

Project expr expr => expr :<: expr

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

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

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

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