Language.Syntactic.Constraint

Type-constrained syntax trees

Type predicates

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

Intersection of type predicates

Instances

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

Defined in Language.Syntactic.Constraint

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

Defined in Language.Syntactic.Constraint

Methods

sub :: Sub (p :/\: ps) q

(p :/\: ps) :< p

Defined in Language.Syntactic.Constraint

Methods

sub :: Sub (p :/\: ps) p

class Top a

Universal type predicate

Instances

Top a

Defined in Language.Syntactic.Constraint

pTop :: P Top

pTypeable :: P Typeable

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 :: * -> Constraint) :< (sup :: * -> Constraint) where

Subset relation on type predicates

Minimal complete definition

sub

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

Defined in Language.Syntactic.Constraint

Methods

sub :: Sub p p

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

Defined in Language.Syntactic.Constraint

Methods

sub :: Sub (p :/\: ps) q

(p :/\: ps) :< p

Defined in Language.Syntactic.Constraint

Methods

sub :: Sub (p :/\: ps) p

Constrained syntax

data (:|) :: (* -> *) -> (* -> Constraint) -> * -> * where infixl 4

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)

Defined in Language.Syntactic.Constraint

Methods

prj :: (sup :| pred) a -> Maybe (sub a)

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

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => sub sig -> (sup :| pred) sig

StringTree dom => StringTree (dom :| pred)

Defined in Language.Syntactic.Constraint

Methods

stringTreeSym :: [Tree String] -> (dom :| pred) a -> Tree String

Render dom => Render (dom :| pred)

Defined in Language.Syntactic.Constraint

Methods

renderSym :: (dom :| pred) sig -> String

renderArgs :: [String] -> (dom :| pred) sig -> String

Eval dom => Eval (dom :| pred)

Defined in Language.Syntactic.Constraint

Methods

evaluate :: (dom :| pred) a -> Denotation a

Equality dom => Equality (dom :| pred)

Defined in Language.Syntactic.Constraint

Methods

equal :: (dom :| pred) a -> (dom :| pred) b -> Bool

exprHash :: (dom :| pred) a -> Hash

Constrained dom => Constrained (dom :| pred)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (dom :| pred) :: * -> Constraint

Methods

exprDict :: (dom :| pred) a -> Dict (Sat (dom :| pred) (DenResult a))

EvalBind dom => EvalBind (dom :| pred)

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom0, ConstrainedBy dom0 Typeable, Typeable (DenResult sig)) => (dom :| pred) sig -> Args (AST dom0) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize dom => Optimize (dom :| p)

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom0 => ConstFolder dom0 -> ((dom :| p) sig -> AST dom0 sig) -> (dom :| p) sig -> Args (AST dom0) sig -> Writer (Set VarId) (ASTF dom0 (DenResult sig))

TupleSat dom p => TupleSat (dom :| q) p

Defined in Language.Syntactic.Frontend.TupleConstrained

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

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: (sub :| pred) a -> Args (AST dom) a -> (sub :| pred) b -> Args (AST dom) b -> Reader env Bool

type Sat (dom :| pred)

Defined in Language.Syntactic.Constraint

type Sat (dom :| pred) = pred :/\: Sat dom

data (:||) :: (* -> *) -> (* -> Constraint) -> * -> * where infixl 4

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)

Defined in Language.Syntactic.Constraint

Methods

prj :: (sup :|| pred) a -> Maybe (sub a)

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

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => sub sig -> (sup :|| pred) sig

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

Defined in Language.Syntactic.Constraint

Methods

stringTreeSym :: [Tree String] -> (dom :|| pred) a -> Tree String

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

Defined in Language.Syntactic.Constraint

Methods

renderSym :: (dom :|| pred) sig -> String

renderArgs :: [String] -> (dom :|| pred) sig -> String

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

Defined in Language.Syntactic.Constraint

Methods

evaluate :: (dom :|| pred) a -> Denotation a

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

Defined in Language.Syntactic.Constraint

Methods

equal :: (dom :|| pred) a -> (dom :|| pred) b -> Bool

exprHash :: (dom :|| pred) a -> Hash

Constrained (dom :|| pred)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (dom :|| pred) :: * -> Constraint

Methods

exprDict :: (dom :|| pred) a -> Dict (Sat (dom :|| pred) (DenResult a))

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

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom0, ConstrainedBy dom0 Typeable, Typeable (DenResult sig)) => (dom :|| pred) sig -> Args (AST dom0) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize dom => Optimize (dom :|| p)

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom0 => ConstFolder dom0 -> ((dom :|| p) sig -> AST dom0 sig) -> (dom :|| p) sig -> Args (AST dom0) sig -> Writer (Set VarId) (ASTF dom0 (DenResult sig))

TupleSat ((Tuple :|| p) :+: dom2) p

Defined in Language.Syntactic.Frontend.TupleConstrained

TupleSat ((Select :|| p) :+: dom2) p

Defined in Language.Syntactic.Frontend.TupleConstrained

TupleSat dom p => TupleSat (dom :|| q) p

Defined in Language.Syntactic.Frontend.TupleConstrained

TupleSat (Tuple :|| p) p

Defined in Language.Syntactic.Frontend.TupleConstrained

TupleSat (Select :|| p) p

Defined in Language.Syntactic.Frontend.TupleConstrained

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

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: (sub :|| pred) a -> Args (AST dom) a -> (sub :|| pred) b -> Args (AST dom) b -> Reader env Bool

IsHODomain (HODomain dom p pVar) p pVar

Defined in Language.Syntactic.Constructs.Binding.HigherOrder

Methods

lambda :: (p (a -> b), p a, pVar a) => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b) -> ASTF (HODomain dom p pVar) (a -> b)

type Sat (dom :|| pred)

Defined in Language.Syntactic.Constraint

type Sat (dom :|| pred) = pred

class Constrained expr where

Expressions that constrain their result types

Minimal complete definition

exprDict

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 Empty

Defined in Language.Syntactic.Constraint

Associated Types

type Sat Empty :: * -> Constraint

Methods

exprDict :: Empty a -> Dict (Sat Empty (DenResult a))

Constrained Tuple

Defined in Language.Syntactic.Constructs.Tuple

Associated Types

type Sat Tuple :: * -> Constraint

Methods

exprDict :: Tuple a -> Dict (Sat Tuple (DenResult a))

Constrained Select

Defined in Language.Syntactic.Constructs.Tuple

Associated Types

type Sat Select :: * -> Constraint

Methods

exprDict :: Select a -> Dict (Sat Select (DenResult a))

Constrained Literal

Defined in Language.Syntactic.Constructs.Literal

Associated Types

type Sat Literal :: * -> Constraint

Methods

exprDict :: Literal a -> Dict (Sat Literal (DenResult a))

Constrained Identity

Defined in Language.Syntactic.Constructs.Identity

Associated Types

type Sat Identity :: * -> Constraint

Methods

exprDict :: Identity a -> Dict (Sat Identity (DenResult a))

Constrained Construct

Defined in Language.Syntactic.Constructs.Construct

Associated Types

type Sat Construct :: * -> Constraint

Methods

exprDict :: Construct a -> Dict (Sat Construct (DenResult a))

Constrained Condition

Defined in Language.Syntactic.Constructs.Condition

Associated Types

type Sat Condition :: * -> Constraint

Methods

exprDict :: Condition a -> Dict (Sat Condition (DenResult a))

Constrained Let

Defined in Language.Syntactic.Constructs.Binding

Associated Types

type Sat Let :: * -> Constraint

Methods

exprDict :: Let a -> Dict (Sat Let (DenResult a))

Constrained Lambda

Defined in Language.Syntactic.Constructs.Binding

Associated Types

type Sat Lambda :: * -> Constraint

Methods

exprDict :: Lambda a -> Dict (Sat Lambda (DenResult a))

Constrained Variable

Defined in Language.Syntactic.Constructs.Binding

Associated Types

type Sat Variable :: * -> Constraint

Methods

exprDict :: Variable a -> Dict (Sat Variable (DenResult a))

Constrained Node

Defined in Language.Syntactic.Sharing.Graph

Associated Types

type Sat Node :: * -> Constraint

Methods

exprDict :: Node a -> Dict (Sat Node (DenResult a))

Constrained dom => Constrained (AST dom)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (AST dom) :: * -> Constraint

Methods

exprDict :: AST dom a -> Dict (Sat (AST dom) (DenResult a))

Constrained (MONAD m)

Defined in Language.Syntactic.Constructs.Monad

Associated Types

type Sat (MONAD m) :: * -> Constraint

Methods

exprDict :: MONAD m a -> Dict (Sat (MONAD m) (DenResult a))

Constrained (sub1 :+: sub2)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (sub1 :+: sub2) :: * -> Constraint

Methods

exprDict :: (sub1 :+: sub2) a -> Dict (Sat (sub1 :+: sub2) (DenResult a))

Constrained (dom :|| pred)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (dom :|| pred) :: * -> Constraint

Methods

exprDict :: (dom :|| pred) a -> Dict (Sat (dom :|| pred) (DenResult a))

Constrained dom => Constrained (dom :| pred)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (dom :| pred) :: * -> Constraint

Methods

exprDict :: (dom :| pred) a -> Dict (Sat (dom :| pred) (DenResult a))

Constrained expr => Constrained (Decor info expr)

Defined in Language.Syntactic.Constructs.Decoration

Associated Types

type Sat (Decor info expr) :: * -> Constraint

Methods

exprDict :: Decor info expr a -> Dict (Sat (Decor info expr) (DenResult a))

Constrained dom => Constrained (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (SubConstr1 c dom p) :: * -> Constraint

Methods

exprDict :: SubConstr1 c dom p a -> Dict (Sat (SubConstr1 c dom p) (DenResult a))

Constrained dom => Constrained (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (SubConstr2 c dom pa pb) :: * -> Constraint

Methods

exprDict :: SubConstr2 c dom pa pb a -> Dict (Sat (SubConstr2 c dom pa pb) (DenResult a))

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

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

Minimal complete definition

injC

Methods

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

Instances

Sat expr a => InjectC expr expr a

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => expr sig -> expr sig

(InjectC sub sup a, Sat (AST sup) a) => InjectC sub (AST sup) a

Defined in Language.Syntactic.Constraint

Methods

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

InjectC expr1 expr3 a => InjectC expr1 (expr2 :+: expr3) a

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => expr1 sig -> (expr2 :+: expr3) sig

InjectC expr1 (expr1 :+: expr2) a

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => expr1 sig -> (expr1 :+: expr2) sig

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

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => sub sig -> (sup :|| pred) sig

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

Defined in Language.Syntactic.Constraint

Methods

injC :: DenResult sig ~ a => sub sig -> (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 SubConstr1 :: (* -> *) -> (* -> *) -> (* -> Constraint) -> * -> * where

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)

Defined in Language.Syntactic.Constraint

Methods

prj :: SubConstr1 c sup p a -> Maybe (sub a)

StringTree dom => StringTree (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

Methods

stringTreeSym :: [Tree String] -> SubConstr1 c dom p a -> Tree String

Render dom => Render (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

Methods

renderSym :: SubConstr1 c dom p sig -> String

renderArgs :: [String] -> SubConstr1 c dom p sig -> String

Eval dom => Eval (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

Methods

evaluate :: SubConstr1 c dom p a -> Denotation a

Equality dom => Equality (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

Methods

equal :: SubConstr1 c dom p a -> SubConstr1 c dom p b -> Bool

exprHash :: SubConstr1 c dom p a -> Hash

Constrained dom => Constrained (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (SubConstr1 c dom p) :: * -> Constraint

Methods

exprDict :: SubConstr1 c dom p a -> Dict (Sat (SubConstr1 c dom p) (DenResult a))

EvalBind dom => EvalBind (SubConstr1 c dom p)

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom0, ConstrainedBy dom0 Typeable, Typeable (DenResult sig)) => SubConstr1 c dom p sig -> Args (AST dom0) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize dom => Optimize (SubConstr1 c dom p)

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom0 => ConstFolder dom0 -> (SubConstr1 c dom p sig -> AST dom0 sig) -> SubConstr1 c dom p sig -> Args (AST dom0) sig -> Writer (Set VarId) (ASTF dom0 (DenResult sig))

AlphaEq sub sub dom env => AlphaEq (SubConstr1 c sub p) (SubConstr1 c sub p) dom env

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: SubConstr1 c sub p a -> Args (AST dom) a -> SubConstr1 c sub p b -> Args (AST dom) b -> Reader env Bool

type Sat (SubConstr1 c dom p)

Defined in Language.Syntactic.Constraint

type Sat (SubConstr1 c dom p) = Sat dom

data SubConstr2 :: (* -> * -> *) -> (* -> *) -> (* -> Constraint) -> (* -> Constraint) -> * -> * where

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)

Defined in Language.Syntactic.Constraint

Methods

prj :: SubConstr2 c sup pa pb a -> Maybe (sub a)

StringTree dom => StringTree (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

Methods

stringTreeSym :: [Tree String] -> SubConstr2 c dom pa pb a -> Tree String

Render dom => Render (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

Methods

renderSym :: SubConstr2 c dom pa pb sig -> String

renderArgs :: [String] -> SubConstr2 c dom pa pb sig -> String

Eval dom => Eval (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

Methods

evaluate :: SubConstr2 c dom pa pb a -> Denotation a

Equality dom => Equality (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

Methods

equal :: SubConstr2 c dom pa pb a -> SubConstr2 c dom pa pb b -> Bool

exprHash :: SubConstr2 c dom pa pb a -> Hash

Constrained dom => Constrained (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

Associated Types

type Sat (SubConstr2 c dom pa pb) :: * -> Constraint

Methods

exprDict :: SubConstr2 c dom pa pb a -> Dict (Sat (SubConstr2 c dom pa pb) (DenResult a))

EvalBind dom => EvalBind (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom0, ConstrainedBy dom0 Typeable, Typeable (DenResult sig)) => SubConstr2 c dom pa pb sig -> Args (AST dom0) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize dom => Optimize (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom0 => ConstFolder dom0 -> (SubConstr2 c dom pa pb sig -> AST dom0 sig) -> SubConstr2 c dom pa pb sig -> Args (AST dom0) sig -> Writer (Set VarId) (ASTF dom0 (DenResult sig))

AlphaEq sub sub dom env => AlphaEq (SubConstr2 c sub pa pb) (SubConstr2 c sub pa pb) dom env

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: SubConstr2 c sub pa pb a -> Args (AST dom) a -> SubConstr2 c sub pa pb b -> Args (AST dom) b -> Reader env Bool

type Sat (SubConstr2 c dom pa pb)

Defined in Language.Syntactic.Constraint

type Sat (SubConstr2 c dom pa pb) = Sat dom

Existential quantification

data ASTE :: (* -> *) -> * 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 :: (* -> *) -> (* -> Constraint) -> * where

AST with bounded existentially quantified result type

Constructors

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

Instances

p ~ Sat dom => NodeEqEnv dom (EqEnv dom p)

Defined in Language.Syntactic.Sharing.Graph

Methods

prjNodeEqEnv :: EqEnv dom p -> NodeEnv dom (Sat dom)

modNodeEqEnv :: (NodeEnv dom (Sat dom) -> NodeEnv dom (Sat dom)) -> EqEnv dom p -> EqEnv dom p

VarEqEnv (EqEnv dom p)

Defined in Language.Syntactic.Sharing.Graph

Methods

prjVarEqEnv :: EqEnv dom p -> [(VarId, VarId)]

modVarEqEnv :: ([(VarId, VarId)] -> [(VarId, VarId)]) -> EqEnv dom p -> EqEnv dom p

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

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

type ASTSAT dom = ASTB dom (Sat dom)

Misc.

data Empty :: * -> *

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

StringTree Empty

Defined in Language.Syntactic.Constraint

Methods

stringTreeSym :: [Tree String] -> Empty a -> Tree String

Render Empty

Defined in Language.Syntactic.Constraint

Methods

renderSym :: Empty sig -> String

renderArgs :: [String] -> Empty sig -> String

Eval Empty

Defined in Language.Syntactic.Constraint

Methods

evaluate :: Empty a -> Denotation a

Equality Empty

Defined in Language.Syntactic.Constraint

Methods

equal :: Empty a -> Empty b -> Bool

exprHash :: Empty a -> Hash

Constrained Empty

Defined in Language.Syntactic.Constraint

Associated Types

type Sat Empty :: * -> Constraint

Methods

exprDict :: Empty a -> Dict (Sat Empty (DenResult a))

EvalBind Empty

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => Empty sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize Empty

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom => ConstFolder dom -> (Empty sig -> AST dom sig) -> Empty sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig))

AlphaEq Empty Empty dom env

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: Empty a -> Args (AST dom) a -> Empty b -> Args (AST dom) b -> Reader env Bool

type Sat Empty

Defined in Language.Syntactic.Constraint

type Sat Empty = Top

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