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

Language.Syntactic.Constraint

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) 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) 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) 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) TupleSat (:+: (:|| Select p) dom2) p TupleSat (:+: (:|| Tuple p) dom2) p TupleSat dom p => TupleSat (:|| dom q) p TupleSat (:|| Select p) p TupleSat (:|| Tuple 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

Instances

 Constrained Empty 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 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) ToTree dom => ToTree (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) ToTree dom => ToTree (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 ToTree Empty Render Empty Eval Empty Constrained Empty EvalBind Empty Optimize Empty AlphaEq Empty Empty dom env