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 (binder :: S -> S -> Type) (sig :: Type -> Type -> Type) (n :: S) where
- ScopedAST :: forall (binder :: S -> S -> Type) (n :: S) (l :: S) (sig :: Type -> Type -> Type). binder n l -> AST binder sig l -> ScopedAST binder sig n
data AST (binder :: S -> S -> Type) (sig :: Type -> Type -> Type) (n :: S) where
- Var :: forall (n :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). Name n -> AST binder sig n
- Node :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S). sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n
substitute :: forall (sig :: Type -> Type -> Type) (o :: S) (binder :: S -> S -> Type) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder) => Scope o -> Substitution (AST binder sig) i o -> AST binder sig i -> AST binder sig o
substituteRefreshed :: forall (sig :: Type -> Type -> Type) (o :: S) (binder :: S -> S -> Type) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder) => Scope o -> Substitution (AST binder sig) i o -> AST binder sig i -> AST binder sig o
refreshAST :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Distinct n, CoSinkable binder) => Scope n -> AST binder sig n -> AST binder sig n
refreshScopedAST :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Distinct n, CoSinkable binder) => Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
alphaEquivRefreshed :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquivScoped :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool
unsafeEqAST :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n, Distinct l) => AST binder sig n -> AST binder sig l -> Bool
unsafeEqScopedAST :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n, Distinct l) => ScopedAST binder sig n -> ScopedAST binder 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 binder rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) -> (forall (x :: S) z. Distinct x => Scope x -> Map rawIdent (Name x) -> rawPattern -> (forall (y :: S). DExt x y => binder x y -> Map rawIdent (Name y) -> z) -> z) -> (rawScopedTerm -> rawTerm) -> Scope n -> Map rawIdent (Name n) -> rawTerm -> AST binder sig n
convertToScopedAST :: forall (n :: S) sig rawIdent binder rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder) => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) -> (forall (x :: S) z. Distinct x => Scope x -> Map rawIdent (Name x) -> rawPattern -> (forall (y :: S). DExt x y => binder x y -> Map rawIdent (Name y) -> z) -> z) -> (rawScopedTerm -> rawTerm) -> Scope n -> Map rawIdent (Name n) -> (rawPattern, rawScopedTerm) -> ScopedAST binder sig n
convertFromAST :: forall sig rawPattern rawScopedTerm rawTerm rawIdent binder (n :: S). Bifunctor sig => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) -> (rawIdent -> rawTerm) -> (forall (x :: S) (y :: S). (Int -> rawIdent) -> binder x y -> rawPattern) -> (rawTerm -> rawScopedTerm) -> (Int -> rawIdent) -> AST binder sig n -> rawTerm
convertFromScopedAST :: forall sig rawPattern rawScopedTerm rawTerm rawIdent binder (n :: S). Bifunctor sig => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) -> (rawIdent -> rawTerm) -> (forall (x :: S) (y :: S). (Int -> rawIdent) -> binder x y -> rawPattern) -> (rawTerm -> rawScopedTerm) -> (Int -> rawIdent) -> ScopedAST binder sig n -> (rawPattern, rawScopedTerm)

Documentation

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

Scoped term under a (single) name binder.

Constructors

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

Instances

Instances details

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

data AST (binder :: S -> S -> Type) (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) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). Name n -> AST binder sig n	A (free) variable in scope `n`.
Node :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S). sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n	A non-variable syntactic construction specified by the signature `Bifunctor` `sig`.

Instances

Instances details

(Bifunctor sig, CoSinkable binder) => RelMonad Name (AST binder 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 binder sig a Source #

rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> AST binder sig a -> (Name a -> AST binder sig b) -> AST binder 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 binder sig) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

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

(Bifunctor sig, CoSinkable binder) => Sinkable (AST binder sig) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

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

Generic (AST binder sig n) Source #

Instance details

Defined in Control.Monad.Free.Foil

Associated Types

type Rep (AST binder sig n)

Instance details

Defined in Control.Monad.Free.Foil

type Rep (AST binder sig n) = D1 ('MetaData "AST" "Control.Monad.Free.Foil" "free-foil-0.1.0-7PHOjgygGpg7q7SlKctZqC" '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 binder sig n) (AST binder sig n)))))

Methods

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

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

(forall (x :: S) (y :: S). NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST binder sig n) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

rnf :: AST binder sig n -> () #

type Rep (AST binder sig n) Source #

Instance details

Defined in Control.Monad.Free.Foil

type Rep (AST binder sig n) = D1 ('MetaData "AST" "Control.Monad.Free.Foil" "free-foil-0.1.0-7PHOjgygGpg7q7SlKctZqC" '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 binder sig n) (AST binder sig n)))))

Substitution

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

Substitution for free (scoped monads).

substituteRefreshed :: forall (sig :: Type -> Type -> Type) (o :: S) (binder :: S -> S -> Type) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder) => Scope o -> Substitution (AST binder sig) i o -> AST binder sig i -> AST binder 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) (binder :: S -> S -> Type). (Bifunctor sig, Distinct n, CoSinkable binder) => Scope n -> AST binder sig n -> AST binder sig n Source #

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

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

Similar to refreshAST, but for scoped terms.

alphaEquivRefreshed :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> AST binder sig n -> AST binder 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) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> AST binder sig n -> AST binder 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) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool Source #

Same as alphaEquiv but for scoped terms.

Unsafe equality checks

unsafeEqAST :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n, Distinct l) => AST binder sig n -> AST binder 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) (binder :: S -> S -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n, Distinct l) => ScopedAST binder sig n -> ScopedAST binder 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 binder rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))	Unpeel one syntax node (or a variable) from a raw term.
-> (forall (x :: S) z. Distinct x => Scope x -> Map rawIdent (Name x) -> rawPattern -> (forall (y :: S). DExt x y => binder x y -> Map rawIdent (Name y) -> z) -> z)	Convert raw pattern into a scope-safe pattern.
-> (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 binder sig n

Convert a raw term into a scope-safe term.

convertToScopedAST Source #

Arguments

:: forall (n :: S) sig rawIdent binder rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))	Unpeel one syntax node (or a variable) from a raw term.
-> (forall (x :: S) z. Distinct x => Scope x -> Map rawIdent (Name x) -> rawPattern -> (forall (y :: S). DExt x y => binder x y -> Map rawIdent (Name y) -> z) -> z)	Convert raw pattern into a scope-safe pattern.
-> (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 binder sig n

Same as convertToAST but for scoped terms.

Convert from free foil

convertFromAST Source #

Arguments

:: forall sig rawPattern rawScopedTerm rawTerm rawIdent binder (n :: S). Bifunctor sig
=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)	Peel back one layer of syntax.
-> (rawIdent -> rawTerm)	Convert identifier into a raw variable term.
-> (forall (x :: S) (y :: S). (Int -> rawIdent) -> binder x y -> rawPattern)	Convert scope-safe pattern into a raw 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 binder 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 binder (n :: S). Bifunctor sig
=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)	Peel back one layer of syntax.
-> (rawIdent -> rawTerm)	Convert identifier into a raw variable term.
-> (forall (x :: S) (y :: S). (Int -> rawIdent) -> binder x y -> rawPattern)	Convert scope-safe pattern into a raw 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 binder sig n	Scope-safe scoped term.
-> (rawPattern, rawScopedTerm)

Same as convertFromAST but for scoped terms.