Safe Haskell	None

Language.Syntactic.Constructs.Binding.HigherOrder

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

Documentation

data Variable a Source

Variables

Instances

Equality Variable	`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
StringTree Variable
Render Variable
Constrained Variable
EvalBind Variable
Optimize Variable
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env
IsHODomain (HODomain dom p pVar) p pVar

data Let a whereSource

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

Equality Let
StringTree Let
Render Let
Eval Let
Constrained Let
EvalBind Let
Optimize Let
AlphaEq dom dom dom env => AlphaEq Let Let dom env

data HOLambda dom p pVar a whereSource

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

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

Adding support for higher-order abstract syntax to a domain

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

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 whereSource

An abstraction of HODomain

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

reifyM :: forall dom p pVar a. AST (HODomain dom p pVar) a -> State VarId (AST (FODomain dom p pVar) a)Source

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

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