Safe Haskell	None
Language	Haskell2010

Language.Syntactic.Syntax

Contents

Syntax trees
Symbol domains
Type inference

Description

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

Synopsis

Syntax trees

data AST dom sig where Source

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) Source
Project sub sup => Project sub (AST sup) Source
InjectC sub sup a => InjectC sub (AST sup) a Source
Functor dom => Functor (AST dom) Source
Equality dom => Equality (AST dom) Source
Eval dom => Eval (AST dom) Source
Constrained dom => Constrained (AST dom) Source
ApplySym (Full a) (ASTF dom a) dom Source
Syntactic (ASTF dom a) Source
(Syntactic a, (~) (* -> ) (Domain a) dom, (~) ia (Internal a), SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) Source
ApplySym sig f dom => ApplySym ((:->) a sig) (ASTF dom a -> f) dom Source
type Sat (AST dom) = Sat dom Source
type Domain (ASTF dom a) = dom Source
type Internal (ASTF dom a) = a Source

type ASTF dom a = AST dom (Full a) Source

Fully applied abstract syntax tree

newtype Full a Source

Signature of a fully applied symbol

Constructors

Full
Fields result :: a

Instances

Functor Full Source
Eq a => Eq (Full a) Source
Show a => Show (Full a) Source
ApplySym (Full a) (ASTF dom a) dom Source
Syntactic (ASTF dom a) Source
(Syntactic a, (~) (* -> ) (Domain a) dom, (~) ia (Internal a), SyntacticN b ib) => SyntacticN (a -> b) (AST dom (Full ia) -> ib) Source
ApplySym sig f dom => ApplySym ((:->) a sig) (ASTF dom a -> f) dom Source
type DenResult (Full a) = a Source
type Denotation (Full a) = a Source
type Domain (ASTF dom a) = dom Source
type Internal (ASTF dom a) = a Source

newtype a :-> sig infixr 9 Source

Signature of a partially applied (or unapplied) symbol

Constructors

Partial (a -> sig)

Instances

Functor ((:->) a) Source
ApplySym sig f dom => ApplySym ((:->) a sig) (ASTF dom a -> f) dom Source
type DenResult ((:->) a sig) = DenResult sig Source
type Denotation ((:->) a sig) = a -> Denotation sig Source

size :: AST dom sig -> Int Source

Count the number of symbols in an expression

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

Class for the type-level recursion needed by appSym

Methods

appSym' :: AST dom sig -> f Source

Instances

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

type family DenResult sig Source

The result type of a symbol with the given signature

Instances

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

Symbol domains

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

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) Source
expr1 :<: ((:+:) expr1 expr2) Source
Project expr1 expr3 => Project expr1 ((:+:) expr2 expr3) Source
Project expr1 ((:+:) expr1 expr2) Source
InjectC expr1 expr3 a => InjectC expr1 ((:+:) expr2 expr3) a Source
InjectC expr1 ((:+:) expr1 expr2) a Source
(Functor dom1, Functor dom2) => Functor ((:+:) dom1 dom2) Source
(Equality expr1, Equality expr2) => Equality ((:+:) expr1 expr2) Source
(StringTree dom1, StringTree dom2) => StringTree ((:+:) dom1 dom2) Source
(Render expr1, Render expr2) => Render ((:+:) expr1 expr2) Source
(Eval expr1, Eval expr2) => Eval ((:+:) expr1 expr2) Source
Constrained ((:+:) sub1 sub2) Source
(EvalBind sub1, EvalBind sub2) => EvalBind ((:+:) sub1 sub2) Source
(Optimize sub1, Optimize sub2) => Optimize ((:+:) sub1 sub2) Source
TupleSat dom2 p => TupleSat ((:+:) dom1 dom2) p Source
TupleSat ((:+:) ((:\|\|) Tuple p) dom2) p Source
TupleSat ((:+:) ((:\|\|) Select p) dom2) p Source
(AlphaEq subA1 subB1 dom env, AlphaEq subA2 subB2 dom env) => AlphaEq ((:+:) subA1 subA2) ((:+:) subB1 subB2) dom env Source
IsHODomain (HODomain dom p pVar) p pVar Source
type Sat ((:+:) sub1 sub2) = Top Source

class Project sub sup where Source

Symbol projection

Methods

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

Partial projection from sup to sub

Instances

Project expr expr Source
Project sub sup => Project sub (AST sup) Source
Project expr1 expr3 => Project expr1 ((:+:) expr2 expr3) Source
Project expr1 ((:+:) expr1 expr2) Source
Project sub sup => Project sub ((:\|\|) sup pred) Source
Project sub sup => Project sub ((:\|) sup pred) Source
Project sub sup => Project sub (Decor info sup) Source
Project sub sup => Project sub (SubConstr1 c sup p) Source
Project sub sup => Project sub (SubConstr2 c sup pa pb) Source

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

Symbol subsumption

Methods

inj :: sub a -> sup a Source

Injection from sub to sup

Instances

expr :<: expr Source
(:<:) sub sup => sub :<: (AST sup) Source
(:<:) expr1 expr3 => expr1 :<: ((:+:) expr2 expr3) Source
expr1 :<: ((:+:) expr1 expr2) Source

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

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 Source

Constrain a symbol to a specific type

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

Projection to a specific symbol type