Language.Syntactic.Constraint

Type constrained syntax trees

Type predicates

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

Intersection of type predicates

Instances

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

class Top a

Universal type predicate

Instances

Top a

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

Evidence that the predicate sub is a subset of sup

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

Weaken an intersection

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

Weaken an intersection

class sub :< sup where

Subset relation on type predicates

Methods

sub :: Sub sub sup

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 (expr :| pred) sig where

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)

(Project sub (:| sup pred), Sat (:| sup pred) sig, InjectC sub sup sig, pred sig) => InjectC sub (:| sup pred) sig

Equality dom => Equality (:| dom pred)

(Render (:| dom pred), ToTree dom) => ToTree (:| 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)

AlphaEq sub sub dom env => AlphaEq (:| sub pred) (:| sub pred) dom env

data (expr :|| pred) sig where

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)

(Project sub (:|| sup pred), Sat (:|| sup pred) sig, InjectC sub sup sig, pred sig) => InjectC sub (:|| sup pred) sig

Equality dom => Equality (:|| dom pred)

(Render (:|| dom pred), ToTree dom) => ToTree (:|| 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)

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

AlphaEq sub sub dom env => AlphaEq (:|| sub pred) (:|| sub pred) dom env

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

class Constrained expr where

Expressions that constrain their result types

Associated Types

type Sat expr :: * -> Constraint

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

Compute a constraint on the result type of an expression

Instances

Constrained Condition

Constrained Construct

Constrained Identity

Constrained Literal

Constrained Select

Constrained Tuple

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

type ConstrainedBy expr c = (Constrained expr, Sat expr :< c)

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

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

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

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

Methods

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

Instances

(Project expr expr, Sat expr sig) => InjectC expr expr sig

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

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

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

(Project sub (:|| sup pred), Sat (:|| sup pred) sig, InjectC sub sup sig, pred sig) => InjectC sub (:|| sup pred) sig

(Project sub (:| sup pred), Sat (:| sup pred) sig, InjectC sub sup sig, pred sig) => InjectC sub (:| sup pred) sig

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

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 ASTE dom where

AST with existentially quantified result type

Constructors

ASTE :: ASTF dom a -> ASTE dom

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

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

data ASTB dom where

AST with bounded existentially quantified result type

Constructors

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

Instances

NodeEqEnv dom (EqEnv dom)

VarEqEnv (EqEnv dom)

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

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