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

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

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

exprDictSub :: ConstrainedBy expr 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

 (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 -> 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 ASTE dom 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 dom whereSource

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

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