Safe Haskell	None
Language	Haskell2010

Control.Monad.Free.Foil

Contents

Substitution
$\alpha$-equivalence
- Unsafe equality checks
Converting to and 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, SinkableK 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, SinkableK binder) => Scope o -> Substitution (AST binder sig) i o -> AST binder sig i -> AST binder sig o
substitutePattern :: forall (sig :: Type -> Type -> Type) (o :: S) binder' (binder :: S -> S -> Type) (n :: S) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder', CoSinkable binder, SinkableK binder) => Scope o -> Substitution (AST binder sig) n o -> binder' n i -> [AST binder sig 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, SinkableK 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, SinkableK binder) => Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n
alphaEquivRefreshed :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bitraversable sig, ZipMatchK sig, Distinct n, UnifiablePattern binder, SinkableK binder) => Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquiv :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bitraversable sig, ZipMatchK sig, Distinct n, UnifiablePattern binder, SinkableK binder) => Scope n -> AST binder sig n -> AST binder sig n -> Bool
alphaEquivScoped :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bitraversable sig, ZipMatchK sig, Distinct n, UnifiablePattern binder, SinkableK 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). (Bitraversable sig, ZipMatchK 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). (Bitraversable sig, ZipMatchK sig, UnifiablePattern binder, Distinct n, Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool
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). 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). binder x y -> rawPattern) -> (rawTerm -> rawScopedTerm) -> (Int -> rawIdent) -> ScopedAST binder sig n -> (rawPattern, rawScopedTerm)
unsinkAST :: forall (l :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type) (n :: S). (Distinct l, CoSinkable binder, Bifoldable sig) => Scope n -> AST binder sig l -> Maybe (AST binder sig n)
freeVarsOf :: forall (n :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). (Distinct n, CoSinkable binder, Bifoldable sig) => AST binder sig n -> [Name n]
freeVarsOfScopedAST :: forall (n :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). (Distinct n, CoSinkable binder, Bifoldable sig) => ScopedAST binder sig n -> [Name n]

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

(Bifunctor sig, CoSinkable binder, SinkableK binder) => SinkableK (ScopedAST binder sig :: S -> Type) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (ScopedAST binder sig :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (ScopedAST binder sig :@@: cs) -> r) -> r Source #

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

Instance details

Defined in Control.Monad.Free.Foil

Methods

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

GenericK (ScopedAST binder sig :: S -> Type) Source #

Instance details

Defined in Control.Monad.Free.Foil

Associated Types

type RepK (ScopedAST binder sig :: S -> Type)

Instance details

Defined in Control.Monad.Free.Foil

type RepK (ScopedAST binder sig :: S -> Type) = Exists S (Field ((('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S)) :*: Field (((('Kon AST :: Atom (S -> S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> Type)). (ScopedAST binder sig :@@: x) -> RepK (ScopedAST binder sig) x #

toK :: forall (x :: LoT (S -> Type)). RepK (ScopedAST binder sig) x -> ScopedAST binder sig :@@: x #

(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 -> () #

type RepK (ScopedAST binder sig :: S -> Type) Source #

Instance details

Defined in Control.Monad.Free.Foil

type RepK (ScopedAST binder sig :: S -> Type) = Exists S (Field ((('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S)) :*: Field (((('Kon AST :: Atom (S -> S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> S -> Type) S)))

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, SinkableK binder) => SinkableK (AST binder sig :: S -> Type) Source #

Instance details

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (AST binder sig :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (AST binder sig :@@: cs) -> r) -> r Source #

(Bifunctor sig, CoSinkable binder, SinkableK 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, SinkableK 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 #

GenericK (AST binder sig :: S -> Type) Source #

Instance details

Defined in Control.Monad.Free.Foil

Associated Types

type RepK (AST binder sig :: S -> Type)

Instance details

Defined in Control.Monad.Free.Foil

type RepK (AST binder sig :: S -> Type) = Field (Name :$: (Var0 :: Atom (S -> Type) S)) :+: Field ((sig :$: (((('Kon ScopedAST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S))) ':@: (((('Kon AST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> Type)). (AST binder sig :@@: x) -> RepK (AST binder sig) x #

toK :: forall (x :: LoT (S -> Type)). RepK (AST binder sig) x -> AST binder sig :@@: x #

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.2.0-LpJiW6MwAH15kYGYUaVUuK" '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 RepK (AST binder sig :: S -> Type) Source #

Instance details

Defined in Control.Monad.Free.Foil

type RepK (AST binder sig :: S -> Type) = Field (Name :$: (Var0 :: Atom (S -> Type) S)) :+: Field ((sig :$: (((('Kon ScopedAST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S))) ':@: (((('Kon AST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S)))

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.2.0-LpJiW6MwAH15kYGYUaVUuK" '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, SinkableK 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, SinkableK 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.

substitutePattern Source #

Arguments

:: forall (sig :: Type -> Type -> Type) (o :: S) binder' (binder :: S -> S -> Type) (n :: S) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder', CoSinkable binder, SinkableK binder)
=> Scope o	Resulting scope.
-> Substitution (AST binder sig) n o	Environment mapping names in scope `n`.
-> binder' n i	Binders that extend scope `n` to scope `i`.
-> [AST binder sig o]	A list of terms intended to serve as
-> AST binder sig i
-> AST binder sig o

Substitution for a single generalized pattern.

$\alpha$-equivalence

refreshAST :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Distinct n, CoSinkable binder, SinkableK 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, SinkableK 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). (Bitraversable sig, ZipMatchK sig, Distinct n, UnifiablePattern binder, SinkableK 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). (Bitraversable sig, ZipMatchK sig, Distinct n, UnifiablePattern binder, SinkableK 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). (Bitraversable sig, ZipMatchK sig, Distinct n, UnifiablePattern binder, SinkableK 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). (Bitraversable sig, ZipMatchK 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). (Bitraversable sig, ZipMatchK sig, UnifiablePattern binder, Distinct n, Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool Source #

A version of unsafeEqAST for scoped terms.

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). 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). 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.

Unsinking AST

unsinkAST :: forall (l :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type) (n :: S). (Distinct l, CoSinkable binder, Bifoldable sig) => Scope n -> AST binder sig l -> Maybe (AST binder sig n) Source #

Unsink an AST from a larger scope to a smaller scope.

freeVarsOf :: forall (n :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). (Distinct n, CoSinkable binder, Bifoldable sig) => AST binder sig n -> [Name n] Source #

Get the free variables of an AST.

freeVarsOfScopedAST :: forall (n :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). (Distinct n, CoSinkable binder, Bifoldable sig) => ScopedAST binder sig n -> [Name n] Source #

Get the free variables of a scoped AST.

Documentation

Instances

Instances

Substitution

\(\alpha\)-equivalence

Unsafe equality checks

Converting to and from free foil

Convert to free foil

Convert from free foil

Unsinking AST