Safe Haskell	None

Language.Syntactic.Constraint

Contents

Type predicates
Constrained syntax
Existential quantification
Misc.

Description

Type-constrained syntax trees

Synopsis

Type predicates

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

Intersection of type predicates

Instances

(c1 a, c2 a) => (c1 :/\: c2) a

class Top a Source

Universal type predicate

Instances

Top a

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

Weaken an intersection

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

Weaken an intersection

class sub :< sup whereSource

Subset relation on type predicates

Methods

sub :: Sub sub supSource

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

Instances

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

Constrained syntax

data :| whereSource

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)
(InjectC sub sup a, pred a) => InjectC sub (:\| sup pred) a
Equality dom => Equality (:\| dom pred)
StringTree dom => StringTree (:\| dom pred)
Render dom => Render (:\| dom pred)
Eval dom => Eval (:\| dom pred)
Constrained dom => Constrained (:\| dom pred)
EvalBind dom => EvalBind (:\| dom pred)
Optimize dom => Optimize (:\| dom p)
TupleSat dom p => TupleSat (:\| dom q) p
AlphaEq sub sub dom env => AlphaEq (:\| sub pred) (:\| sub pred) dom env

data :|| whereSource

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)
(InjectC sub sup a, pred a) => InjectC sub (:\|\| sup pred) a
Equality dom => Equality (:\|\| dom pred)
StringTree dom => StringTree (:\|\| dom pred)
Render dom => Render (:\|\| dom pred)
Eval dom => Eval (:\|\| dom pred)
Constrained (:\|\| dom pred)
EvalBind dom => EvalBind (:\|\| dom pred)
Optimize dom => Optimize (:\|\| dom p)
TupleSat (:+: (:\|\| Tuple p) dom2) p
TupleSat (:+: (:\|\| Select p) dom2) p
TupleSat dom p => TupleSat (:\|\| dom q) p
TupleSat (:\|\| Tuple p) p
TupleSat (:\|\| Select p) p
AlphaEq sub sub dom env => AlphaEq (:\|\| sub pred) (:\|\| sub pred) dom env
IsHODomain (HODomain dom p pVar) p pVar

class Constrained expr whereSource

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

Constrained Empty
Constrained Condition
Constrained Construct
Constrained Identity
Constrained Literal
Constrained Tuple
Constrained Select
Constrained Let
Constrained Lambda
Constrained Variable
Constrained Node
Constrained dom => Constrained (AST dom)
Constrained (MONAD m)
Constrained (:+: sub1 sub2)
Constrained (:\|\| dom pred)
Constrained dom => Constrained (:\| dom pred)
Constrained expr => Constrained (Decor info expr)
Constrained dom => Constrained (SubConstr1 c dom p)
Constrained dom => Constrained (SubConstr2 c dom pa pb)

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 whereSource

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

Methods

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

Instances

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

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

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 whereSource

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)
Equality dom => Equality (SubConstr1 c dom p)
StringTree dom => StringTree (SubConstr1 c dom p)
Render dom => Render (SubConstr1 c dom p)
Eval dom => Eval (SubConstr1 c dom p)
Constrained dom => Constrained (SubConstr1 c dom p)
EvalBind dom => EvalBind (SubConstr1 c dom p)
Optimize dom => Optimize (SubConstr1 c dom p)
AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env

data SubConstr2 whereSource

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)
Equality dom => Equality (SubConstr2 c dom pa pb)
StringTree dom => StringTree (SubConstr2 c dom pa pb)
Render dom => Render (SubConstr2 c dom pa pb)
Eval dom => Eval (SubConstr2 c dom pa pb)
Constrained dom => Constrained (SubConstr2 c dom pa pb)
EvalBind dom => EvalBind (SubConstr2 c dom pa pb)
Optimize dom => Optimize (SubConstr2 c dom pa pb)
AlphaEq sub sub dom env => AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env

Existential quantification

data ASTE whereSource

AST with existentially quantified result type

Constructors

ASTE :: ASTF dom a -> ASTE dom

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

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

data ASTB whereSource

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)
VarEqEnv (EqEnv dom p)

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

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

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

Equality Empty
StringTree Empty
Render Empty
Eval Empty
Constrained Empty
EvalBind Empty
Optimize Empty
AlphaEq Empty Empty dom env

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

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

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