Safe Haskell	None
Language	Haskell2010

Language.Syntactic.Constructs.Binding.HigherOrder

Contents

Orphan instances

Description

This module provides binding constructs using higher-order syntax and a function (reify) for translating to first-order syntax. Expressions constructed using the exported interface (specifically, not introducing Variables explicitly) are guaranteed to have well-behaved translation.

Synopsis

data Variable a
data Let a where
- Let :: Let (a :-> ((a -> b) :-> Full b))
data HOLambda dom p pVar a where
- HOLambda :: (p a, pVar a) => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b) -> HOLambda dom p pVar (Full (a -> b))
type HODomain dom p pVar = (HOLambda dom p pVar :+: ((Variable :|| pVar) :+: dom)) :|| p
type FODomain dom p pVar = (CLambda pVar :+: ((Variable :|| pVar) :+: dom)) :|| p
type CLambda pVar = SubConstr2 (->) Lambda pVar Top
class IsHODomain dom p pVar | dom -> p pVar where
reifyM :: forall dom p pVar m a. MonadState VarId m => AST (HODomain dom p pVar) a -> m (AST (FODomain dom p pVar) a)
reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) a
reify :: (Syntactic a, Domain a ~ HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a)

Documentation

data Variable a Source #

Variables

Instances

StringTree Variable Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods stringTreeSym :: [Tree String] -> Variable a -> Tree String Source #
Render Variable Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods renderSym :: Variable sig -> String Source # renderArgs :: [String] -> Variable sig -> String Source #
Equality Variable Source #	`equal` does strict identifier comparison; i.e. no alpha equivalence. `exprHash` assigns the same hash to all variables. This is a valid over-approximation that enables the following property: `alphaEq` a b ==> `exprHash` a == `exprHash` b
Instance details Defined in Language.Syntactic.Constructs.Binding Methods equal :: Variable a -> Variable b -> Bool Source # exprHash :: Variable a -> Hash Source #
Constrained Variable Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Associated Types type Sat Variable :: * -> Constraint Source # Methods exprDict :: Variable a -> Dict (Sat Variable (DenResult a)) Source #
EvalBind Variable Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => Variable sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig) Source #
Optimize Variable Source #
Instance details Defined in Language.Syntactic.Constructs.Binding.Optimize Methods optimizeSym :: Optimize' dom => ConstFolder dom -> (Variable sig -> AST dom sig) -> Variable sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig)) Source #
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods alphaEqSym :: Variable a -> Args (AST dom) a -> Variable b -> Args (AST dom) b -> Reader env Bool Source #
IsHODomain (HODomain dom p pVar) p pVar Source #
Instance details 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) Source #
type Sat Variable Source #
Instance details Defined in Language.Syntactic.Constructs.Binding type Sat Variable = Top

data Let a where Source #

Let binding

Let is just an application operator with flipped argument order. The argument (a -> b) is preferably constructed by Lambda.

Constructors

Let :: Let (a :-> ((a -> b) :-> Full b))

Instances

StringTree Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods stringTreeSym :: [Tree String] -> Let a -> Tree String Source #
Render Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods renderSym :: Let sig -> String Source # renderArgs :: [String] -> Let sig -> String Source #
Eval Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods evaluate :: Let a -> Denotation a Source #
Equality Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods equal :: Let a -> Let b -> Bool Source # exprHash :: Let a -> Hash Source #
Constrained Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Associated Types type Sat Let :: * -> Constraint Source # Methods exprDict :: Let a -> Dict (Sat Let (DenResult a)) Source #
EvalBind Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => Let sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig) Source #
Optimize Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding.Optimize Methods optimizeSym :: Optimize' dom => ConstFolder dom -> (Let sig -> AST dom sig) -> Let sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig)) Source #
AlphaEq dom dom dom env => AlphaEq Let Let dom env Source #
Instance details Defined in Language.Syntactic.Constructs.Binding Methods alphaEqSym :: Let a -> Args (AST dom) a -> Let b -> Args (AST dom) b -> Reader env Bool Source #
type Sat Let Source #
Instance details Defined in Language.Syntactic.Constructs.Binding type Sat Let = Top

data HOLambda dom p pVar a where Source #

Higher-order lambda binding

Constructors

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

Instances

IsHODomain (HODomain dom p pVar) p pVar Source #
Instance details 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) Source #

type HODomain dom p pVar = (HOLambda dom p pVar :+: ((Variable :|| pVar) :+: dom)) :|| p Source #

Adding support for higher-order abstract syntax to a domain

type FODomain dom p pVar = (CLambda pVar :+: ((Variable :|| pVar) :+: dom)) :|| p Source #

Equivalent to HODomain (including type constraints), but using a first-order representation of binding

type CLambda pVar = SubConstr2 (->) Lambda pVar Top Source #

Lambda with a constraint on the bound variable type

class IsHODomain dom p pVar | dom -> p pVar where Source #

An abstraction of HODomain

Minimal complete definition

lambda

Methods

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

Instances

IsHODomain (HODomain dom p pVar) p pVar Source #
Instance details 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) Source #

reifyM :: forall dom p pVar m a. MonadState VarId m => AST (HODomain dom p pVar) a -> m (AST (FODomain dom p pVar) a) Source #

reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) a Source #

Translating expressions with higher-order binding to corresponding expressions using first-order binding

reify :: (Syntactic a, Domain a ~ HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a) Source #

Reify an n-ary syntactic function

Orphan instances

(Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, IsHODomain dom p pVar, p (Internal a -> Internal b), p (Internal a), pVar (Internal a)) => Syntactic (a -> b) Source #
Instance details Associated Types type Domain (a -> b) :: * -> * Source # type Internal (a -> b) :: * Source # Methods desugar :: (a -> b) -> ASTF (Domain (a -> b)) (Internal (a -> b)) Source # sugar :: ASTF (Domain (a -> b)) (Internal (a -> b)) -> a -> b Source #