syntactic-1.15.1: Generic abstract syntax, and utilities for embedded languages

Safe HaskellNone
LanguageHaskell2010

Language.Syntactic.Constraint

Contents

Description

Type-constrained syntax trees

Synopsis

Type predicates

class (c1 a, c2 a) => (c1 :/\: c2) a infixr 5 Source

Intersection of type predicates

Instances

(c1 a, c2 a) => (c1 :/\: c2) a Source 
(:<) ps q => ((:/\:) p ps) :< q Source 
((:/\:) p ps) :< p Source 

class Top a Source

Universal type predicate

Instances

pTop :: P Top Source

pTypeable :: P Typeable Source

type Sub sub sup = forall a. Dict (sub a) -> Dict (sup a) Source

Evidence that the predicate sub is a subset of sup

weakL :: Sub (c1 :/\: c2) c1 Source

Weaken an intersection

weakR :: Sub (c1 :/\: c2) c2 Source

Weaken an intersection

class sub :< sup where Source

Subset relation on type predicates

Methods

sub :: Sub sub sup Source

Compute evidence that sub is a subset of sup (i.e. that (sup a) implies (sub a))

Instances

p :< p Source 
(:<) ps q => ((:/\:) p ps) :< q Source 
((:/\:) p ps) :< p Source 

Constrained syntax

data (:|) :: (* -> *) -> (* -> Constraint) -> * -> * where infixl 4 Source

Constrain the result type of the expression by the given predicate

Constructors

C :: pred (DenResult sig) => expr sig -> (expr :| pred) sig 

Instances

Project sub sup => Project sub ((:|) sup pred) Source 
(InjectC sub sup a, pred a) => InjectC sub ((:|) sup pred) a Source 
Equality dom => Equality ((:|) dom pred) Source 
StringTree dom => StringTree ((:|) dom pred) Source 
Render dom => Render ((:|) dom pred) Source 
Eval dom => Eval ((:|) dom pred) Source 
Constrained dom => Constrained ((:|) dom pred) Source 
EvalBind dom => EvalBind ((:|) dom pred) Source 
Optimize dom => Optimize ((:|) dom p) Source 
TupleSat dom p => TupleSat ((:|) dom q) p Source 
AlphaEq sub sub dom env => AlphaEq ((:|) sub pred) ((:|) sub pred) dom env Source 
type Sat ((:|) dom pred) = (:/\:) pred (Sat dom) Source 

data (:||) :: (* -> *) -> (* -> Constraint) -> * -> * where infixl 4 Source

Constrain the result type of the expression by the given predicate

The difference between :|| and :| is seen in the instances of the Sat type:

type Sat (dom :|  pred) = pred :/\: Sat dom
type Sat (dom :|| pred) = pred

Constructors

C' :: pred (DenResult sig) => expr sig -> (expr :|| pred) sig 

Instances

Project sub sup => Project sub ((:||) sup pred) Source 
(InjectC sub sup a, pred a) => InjectC sub ((:||) sup pred) a Source 
Equality dom => Equality ((:||) dom pred) Source 
StringTree dom => StringTree ((:||) dom pred) Source 
Render dom => Render ((:||) dom pred) Source 
Eval dom => Eval ((:||) dom pred) Source 
Constrained ((:||) dom pred) Source 
EvalBind dom => EvalBind ((:||) dom pred) Source 
Optimize dom => Optimize ((:||) dom p) Source 
TupleSat ((:+:) ((:||) Tuple p) dom2) p Source 
TupleSat ((:+:) ((:||) Select p) dom2) p Source 
TupleSat dom p => TupleSat ((:||) dom q) p Source 
TupleSat ((:||) Tuple p) p Source 
TupleSat ((:||) Select p) p Source 
AlphaEq sub sub dom env => AlphaEq ((:||) sub pred) ((:||) sub pred) dom env Source 
IsHODomain (HODomain dom p pVar) p pVar Source 
type Sat ((:||) dom pred) = pred Source 

class Constrained expr where Source

Expressions that constrain their result types

Associated Types

type Sat expr :: * -> Constraint Source

Returns a predicate that is satisfied by the result type of all expressions of the given type (see exprDict).

Methods

exprDict :: expr a -> Dict (Sat expr (DenResult a)) Source

Compute a constraint on the result type of an expression

Instances

type ConstrainedBy expr p = (Constrained expr, Sat expr :< p) Source

exprDictSub :: ConstrainedBy expr p => P p -> expr a -> Dict (p (DenResult a)) Source

A version of exprDict that returns a constraint for a particular predicate p as long as (p :< Sat dom) holds

exprDictPlus :: (Constrained dom1, Constrained dom2, Sat dom1 ~ Sat dom2) => AST (dom1 :+: dom2) a -> Dict (Sat dom1 (DenResult a)) Source

A version of exprDict that works for domains of the form (dom1 :+: dom2) as long as (Sat dom1 ~ Sat dom2) holds

class (Project sub sup, Sat sup a) => InjectC sub sup a where Source

Symbol injection (like :<:) with constrained result types

Methods

injC :: (DenResult sig ~ a) => sub sig -> sup sig Source

Instances

Sat expr a => InjectC expr expr a Source 
InjectC sub sup a => InjectC sub (AST sup) a Source 
InjectC expr1 expr3 a => InjectC expr1 ((:+:) expr2 expr3) a Source 
InjectC expr1 ((:+:) expr1 expr2) a Source 
(InjectC sub sup a, pred a) => InjectC sub ((:||) sup pred) a Source 
(InjectC sub sup a, pred a) => InjectC sub ((:|) sup pred) a Source 

appSymC :: (ApplySym sig f dom, InjectC sym (AST dom) (DenResult sig)) => sym sig -> f Source

Generic symbol application

appSymC has any type of the form:

appSymC :: InjectC expr (AST dom) x
    => expr (a :-> b :-> ... :-> Full x)
    -> (ASTF dom a -> ASTF dom b -> ... -> ASTF dom x)

data SubConstr1 :: (* -> *) -> (* -> *) -> (* -> Constraint) -> * -> * where Source

Similar to :||, but rather than constraining the whole result type, it assumes a result type of the form c a and constrains the a.

Constructors

SubConstr1 :: (p a, DenResult sig ~ c a) => dom sig -> SubConstr1 c dom p sig 

Instances

Project sub sup => Project sub (SubConstr1 c sup p) Source 
Equality dom => Equality (SubConstr1 c dom p) Source 
StringTree dom => StringTree (SubConstr1 c dom p) Source 
Render dom => Render (SubConstr1 c dom p) Source 
Eval dom => Eval (SubConstr1 c dom p) Source 
Constrained dom => Constrained (SubConstr1 c dom p) Source 
EvalBind dom => EvalBind (SubConstr1 c dom p) Source 
Optimize dom => Optimize (SubConstr1 c dom p) Source 
AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env Source 
type Sat (SubConstr1 c dom p) = Sat dom Source 

data SubConstr2 :: (* -> * -> *) -> (* -> *) -> (* -> Constraint) -> (* -> Constraint) -> * -> * where Source

Similar to SubConstr1, but assumes a result type of the form c a b and constrains both a and b.

Constructors

SubConstr2 :: (DenResult sig ~ c a b, pa a, pb b) => dom sig -> SubConstr2 c dom pa pb sig 

Instances

Project sub sup => Project sub (SubConstr2 c sup pa pb) Source 
Equality dom => Equality (SubConstr2 c dom pa pb) Source 
StringTree dom => StringTree (SubConstr2 c dom pa pb) Source 
Render dom => Render (SubConstr2 c dom pa pb) Source 
Eval dom => Eval (SubConstr2 c dom pa pb) Source 
Constrained dom => Constrained (SubConstr2 c dom pa pb) Source 
EvalBind dom => EvalBind (SubConstr2 c dom pa pb) Source 
Optimize dom => Optimize (SubConstr2 c dom pa pb) Source 
AlphaEq sub sub dom env => AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env Source 
type Sat (SubConstr2 c dom pa pb) = Sat dom Source 

Existential quantification

data ASTE :: (* -> *) -> * where Source

AST with existentially quantified result type

Constructors

ASTE :: ASTF dom a -> ASTE dom 

liftASTE :: (forall a. ASTF dom a -> b) -> ASTE dom -> b Source

liftASTE2 :: (forall a b. ASTF dom a -> ASTF dom b -> c) -> ASTE dom -> ASTE dom -> c Source

data ASTB :: (* -> *) -> (* -> Constraint) -> * where Source

AST with bounded existentially quantified result type

Constructors

ASTB :: p a => ASTF dom a -> ASTB dom p 

Instances

(~) (* -> Constraint) p (Sat dom) => NodeEqEnv dom (EqEnv dom p) Source 
VarEqEnv (EqEnv dom p) Source 

liftASTB :: (forall a. p a => ASTF dom a -> b) -> ASTB dom p -> b Source

liftASTB2 :: (forall a b. (p a, p b) => ASTF dom a -> ASTF dom b -> c) -> ASTB dom p -> ASTB dom p -> c Source

type ASTSAT dom = ASTB dom (Sat dom) Source

Misc.

data Empty :: * -> * Source

Empty symbol type

Use-case:

data A a
data B a

test :: AST (A :+: (B:||Eq) :+: Empty) a
test = injC (undefined :: (B :|| Eq) a)

Without Empty, this would lead to an overlapping instance error due to the instances

InjectC (B :|| Eq) (B :|| Eq) (DenResult a)

and

InjectC sub sup a, pred a) => InjectC sub (sup :|| pred) a

Instances

universe :: ASTF dom a -> [ASTE dom] Source