Safe Haskell	None
Language	Haskell2010

Control.Monad.Free.Foil

Contents

Substitution
\(\alpha\)-equivalence
- Unsafe equality checks
- Syntactic matching (unification)
Converting to and from free foil
- Convert to free foil
- Convert from free foil

Description

This module defines a variation of free scoped (relative) monads relying on the foil for the scope-safe efficient handling of the binders.

See description of the approach in «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax».

Synopsis

data ScopedAST (sig :: Type -> Type -> Type) (n :: S) where
- ScopedAST :: forall (n :: S) (l :: S) (sig :: Type -> Type -> Type). NameBinder n l -> AST sig l -> ScopedAST sig n
data AST (sig :: Type -> Type -> Type) (n :: S) where
- Var :: forall (n :: S) (sig :: Type -> Type -> Type). Name n -> AST sig n
- Node :: forall (sig :: Type -> Type -> Type) (n :: S). sig (ScopedAST sig n) (AST sig n) -> AST sig n
substitute :: forall (sig :: Type -> Type -> Type) (o :: S) (i :: S). (Bifunctor sig, Distinct o) => Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
substituteRefreshed :: forall (sig :: Type -> Type -> Type) (o :: S) (i :: S). (Bifunctor sig, Distinct o) => Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o
refreshAST :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Distinct n) => Scope n -> AST sig n -> AST sig n
refreshScopedAST :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Distinct n) => Scope n -> ScopedAST sig n -> ScopedAST sig n
alphaEquivRefreshed :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) => Scope n -> AST sig n -> AST sig n -> Bool
alphaEquiv :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) => Scope n -> AST sig n -> AST sig n -> Bool
alphaEquivScoped :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) => Scope n -> ScopedAST sig n -> ScopedAST sig n -> Bool
unsafeEqAST :: forall (sig :: Type -> Type -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig) => AST sig n -> AST sig l -> Bool
unsafeEqScopedAST :: forall (sig :: Type -> Type -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig) => ScopedAST sig n -> ScopedAST sig l -> Bool
class ZipMatch (sig :: Type -> Type -> Type) where
- zipMatch :: sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
convertToAST :: forall (n :: S) sig rawIdent rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent) => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) -> (rawPattern -> Maybe rawIdent) -> (rawScopedTerm -> rawTerm) -> Scope n -> Map rawIdent (Name n) -> rawTerm -> AST sig n
convertToScopedAST :: forall (n :: S) sig rawIdent rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent) => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) -> (rawPattern -> Maybe rawIdent) -> (rawScopedTerm -> rawTerm) -> Scope n -> Map rawIdent (Name n) -> (rawPattern, rawScopedTerm) -> ScopedAST sig n
convertFromAST :: forall sig rawPattern rawScopedTerm rawTerm rawIdent (n :: S). Bifunctor sig => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) -> (rawIdent -> rawTerm) -> (rawIdent -> rawPattern) -> (rawTerm -> rawScopedTerm) -> (Int -> rawIdent) -> AST sig n -> rawTerm
convertFromScopedAST :: forall sig rawPattern rawScopedTerm rawTerm rawIdent (n :: S). Bifunctor sig => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) -> (rawIdent -> rawTerm) -> (rawIdent -> rawPattern) -> (rawTerm -> rawScopedTerm) -> (Int -> rawIdent) -> ScopedAST sig n -> (rawPattern, rawScopedTerm)

Documentation

data ScopedAST (sig :: Type -> Type -> Type) (n :: S) where Source #

Scoped term under a (single) name binder.

Constructors

ScopedAST :: forall (n :: S) (l :: S) (sig :: Type -> Type -> Type). NameBinder n l -> AST sig l -> ScopedAST sig n

Instances

Instances details

(forall (l :: S). NFData (AST sig l)) => NFData (ScopedAST sig n) Source #
Instance details Defined in Control.Monad.Free.Foil Methods rnf :: ScopedAST sig n -> () #

data AST (sig :: Type -> Type -> Type) (n :: S) where Source #

A term, generated by a signature Bifunctor sig, with (free) variables in scope n.

Constructors

Var :: forall (n :: S) (sig :: Type -> Type -> Type). Name n -> AST sig n	A (free) variable in scope `n`.
Node :: forall (sig :: Type -> Type -> Type) (n :: S). sig (ScopedAST sig n) (AST sig n) -> AST sig n	A non-variable syntactic construction specified by the signature `Bifunctor` `sig`.

Instances

Instances details

Bifunctor sig => RelMonad Name (AST sig) Source #

AST sig is a monad relative to Name.

Instance details

Defined in Control.Monad.Free.Foil

Methods

rreturn :: forall (a :: S). Name a -> AST sig a Source #

rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> AST sig a -> (Name a -> AST sig b) -> AST sig b Source #

Show (Expr n) Source #

Use ppExpr to show \(\lambda\)-terms.

Instance details

Defined in Control.Monad.Free.Foil.Example

Methods

showsPrec :: Int -> Expr n -> ShowS #

show :: Expr n -> String #

showList :: [Expr n] -> ShowS #

InjectName (AST sig) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

injectName :: forall (n :: S). Name n -> AST sig n Source #

Bifunctor sig => Sinkable (AST sig) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> AST sig n -> AST sig l Source #

Generic (AST sig n) Source #

Instance details

Defined in Control.Monad.Free.Foil

Associated Types

type Rep (AST sig n)

Instance details

Defined in Control.Monad.Free.Foil

type Rep (AST sig n) = D1 ('MetaData "AST" "Control.Monad.Free.Foil" "free-foil-0.0.3-G0iH6llSubI4QtBzECk72A" 'False) (C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name n))) :+: C1 ('MetaCons "Node" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (sig (ScopedAST sig n) (AST sig n)))))

Methods

from :: AST sig n -> Rep (AST sig n) x #

to :: Rep (AST sig n) x -> AST sig n #

(forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST sig n) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

rnf :: AST sig n -> () #

type Rep (AST sig n) Source #

Instance details

Defined in Control.Monad.Free.Foil

type Rep (AST sig n) = D1 ('MetaData "AST" "Control.Monad.Free.Foil" "free-foil-0.0.3-G0iH6llSubI4QtBzECk72A" 'False) (C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name n))) :+: C1 ('MetaCons "Node" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (sig (ScopedAST sig n) (AST sig n)))))

Substitution

substitute :: forall (sig :: Type -> Type -> Type) (o :: S) (i :: S). (Bifunctor sig, Distinct o) => Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o Source #

Substitution for free (scoped monads).

substituteRefreshed :: forall (sig :: Type -> Type -> Type) (o :: S) (i :: S). (Bifunctor sig, Distinct o) => Scope o -> Substitution (AST sig) i o -> AST sig i -> AST sig o Source #

Substitution for free (scoped monads).

This is a version of substitute that forces refreshing of all name binders, resulting in a term with normalized binders:

substituteRefreshed scope subst = refreshAST scope . subtitute scope subst

In general, substitute is more efficient since it does not always refresh binders.

\(\alpha\)-equivalence

refreshAST :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Distinct n) => Scope n -> AST sig n -> AST sig n Source #

Refresh (force) all binders in a term, minimizing the used indices.

refreshScopedAST :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Distinct n) => Scope n -> ScopedAST sig n -> ScopedAST sig n Source #

Similar to refreshAST, but for scoped terms.

alphaEquivRefreshed :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) => Scope n -> AST sig n -> AST sig n -> Bool Source #

\(\alpha\)-equivalence check for two terms in one scope via normalization of bound identifiers (via refreshAST).

Compared to alphaEquiv, this function may perform some unnecessary changes of bound variables when the binders are the same on both sides.

alphaEquiv :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) => Scope n -> AST sig n -> AST sig n -> Bool Source #

\(\alpha\)-equivalence check for two terms in one scope via unification of bound variables (via unifyNameBinders).

Compared to alphaEquivRefreshed, this function might skip unnecessary changes of bound variables when both binders in two matching scoped terms coincide.

alphaEquivScoped :: forall (sig :: Type -> Type -> Type) (n :: S). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n) => Scope n -> ScopedAST sig n -> ScopedAST sig n -> Bool Source #

Same as alphaEquiv but for scoped terms.

Unsafe equality checks

unsafeEqAST :: forall (sig :: Type -> Type -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig) => AST sig n -> AST sig l -> Bool Source #

Unsafe equality check for two terms. This check ignores the possibility that two terms might have different scope extensions under binders (which might happen due to substitution under a binder in absence of name conflicts).

unsafeEqScopedAST :: forall (sig :: Type -> Type -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig) => ScopedAST sig n -> ScopedAST sig l -> Bool Source #

A version of unsafeEqAST for scoped terms.

Syntactic matching (unification)

class ZipMatch (sig :: Type -> Type -> Type) where Source #

Perform one-level matching for the two (non-variable) terms.

Methods

zipMatch Source #

Arguments

:: sig scope term	Left non-variable term.
-> sig scope' term'	Right non-variable term.
-> Maybe (sig (scope, scope') (term, term'))

Instances

Instances details

(ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) Source #
Instance details Defined in Control.Monad.Free.Foil Methods zipMatch :: Sum f g scope term -> Sum f g scope' term' -> Maybe (Sum f g (scope, scope') (term, term')) Source #

Converting to and from free foil

Convert to free foil

convertToAST Source #

Arguments

:: forall (n :: S) sig rawIdent rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))	Unpeel one syntax node (or a variable) from a raw term.
-> (rawPattern -> Maybe rawIdent)	Extract at most one binder from a pattern (or crash).
-> (rawScopedTerm -> rawTerm)	Extract a term from a scoped term (or crash).
-> Scope n	Resulting scope of the constructed term.
-> Map rawIdent (Name n)	Known names of free variables in scope `n`.
-> rawTerm	Raw term.
-> AST sig n

Convert a raw term into a scope-safe term.

convertToScopedAST Source #

Arguments

:: forall (n :: S) sig rawIdent rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))	Unpeel one syntax node (or a variable) from a raw term.
-> (rawPattern -> Maybe rawIdent)	Extract at most one binder from a pattern (or crash).
-> (rawScopedTerm -> rawTerm)	Extract a term from a scoped term (or crash).
-> Scope n	Resulting scope of the constructed term.
-> Map rawIdent (Name n)	Known names of free variables in scope `n`.
-> (rawPattern, rawScopedTerm)	A pair of a pattern and a corresponding scoped term.
-> ScopedAST sig n

Same as convertToAST but for scoped terms.

Convert from free foil

convertFromAST Source #

Arguments

:: forall sig rawPattern rawScopedTerm rawTerm rawIdent (n :: S). Bifunctor sig
=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)	Peel back one layer of syntax.
-> (rawIdent -> rawTerm)	Convert identifier into a raw variable term.
-> (rawIdent -> rawPattern)	Convert identifier into a raw variable pattern.
-> (rawTerm -> rawScopedTerm)	Wrap raw term into a scoped term.
-> (Int -> rawIdent)	Convert underlying integer identifier of a bound variable into a raw identifier.
-> AST sig n	Scope-safe term.
-> rawTerm

Convert a scope-safe term back into a raw term.

convertFromScopedAST Source #

Arguments

:: forall sig rawPattern rawScopedTerm rawTerm rawIdent (n :: S). Bifunctor sig
=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)	Peel back one layer of syntax.
-> (rawIdent -> rawTerm)	Convert identifier into a raw variable term.
-> (rawIdent -> rawPattern)	Convert identifier into a raw variable pattern.
-> (rawTerm -> rawScopedTerm)	Wrap raw term into a scoped term.
-> (Int -> rawIdent)	Convert underlying integer identifier of a bound variable into a raw identifier.
-> ScopedAST sig n	Scope-safe scoped term.
-> (rawPattern, rawScopedTerm)

Same as convertFromAST but for scoped terms.