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

Safe HaskellNone

Language.Syntactic.Constraint

Contents

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 

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 :: * -> ConstraintSource

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

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

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