Safe Haskell	None
Language	Haskell2010

Control.Monad.Foil.Internal

Contents

Safe types and operations
Unification of binders
- Pattern combinators
- Unifiable patterns
Safe sinking
Safe substitions
Name maps
Raw types and operations
Constraints
Kind-polymorphic sinkability
Kind-polymorphic types with binders

Description

Main definitions of the foil that can be reused for specific implementations. This is an internal module, so it also contains implementation details of the foil.

The original description of this approach is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke «The Foil: Capture-Avoiding Substitution With No Sharp Edges». This module also introduces CoSinkable class, generalizing handling of patterns, as described in «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax».

Since the representation of scopes and substitutions is either IntMap or IntSet, many of the operations have a worst-case complexity of $O(\min(n,W))$. This means that the operation can become linear in the size of the scope $n$ with a maximum of $W$ — the number of bits in an Int (32 or 64).

Synopsis

data S = VoidS
newtype Scope (n :: S) = UnsafeScope RawScope
newtype Name (n :: S) = UnsafeName RawName
nameId :: forall (l :: S). Name l -> Id
newtype NameBinder (n :: S) (l :: S) = UnsafeNameBinder (Name l)
emptyScope :: Scope 'VoidS
member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool
extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScopePattern :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Scope n -> Scope l
newtype ExtendScope (n :: S) (l :: S) (o :: S) (o' :: S) = ExtendScope (Scope n -> Scope l)
idExtendScope :: forall (n :: S) (o :: S) (o' :: S). ExtendScope n n o o'
compExtendScope :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). ExtendScope n i o o' -> ExtendScope i l o' o'' -> ExtendScope n l o o''
nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l
namesOfPattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> [Name l]
newtype NamesOf (n :: S) (l :: S) (o :: S) (o' :: S) = NamesOf [Name l]
idNamesOf :: forall (n :: S) (o :: S) (o' :: S). NamesOf n n o o'
compNamesOf :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''
withFreshBinder :: forall (n :: S) r. Scope n -> (forall (l :: S). NameBinder n l -> r) -> r
withFresh :: forall (n :: S) r. Distinct n => Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFreshPattern :: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r) -> r
withRefreshed :: forall (o :: S) (i :: S) r. Distinct o => Scope o -> Name i -> (forall (o' :: S). DExt o o' => NameBinder o o' -> r) -> r
withRefreshedPattern :: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r) -> r
withRefreshedPattern' :: forall pattern (o :: S) e (n :: S) (l :: S) r. (CoSinkable pattern, Distinct o, InjectName e, Sinkable e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r
unsafeAssertFresh :: forall (n :: S) (l :: S) (n' :: S) (l' :: S) r. NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
newtype WithRefreshedPattern (e :: S -> Type) (n :: S) (l :: S) (o :: S) (o' :: S) = WithRefreshedPattern (Substitution e n o -> Substitution e l o')
idWithRefreshedPattern :: forall (e :: S -> Type) (o :: S) (o' :: S) (n :: S). (Sinkable e, DExt o o') => WithRefreshedPattern e n n o o'
compWithRefreshedPattern :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> Type) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithRefreshedPattern e n i o o' -> WithRefreshedPattern e i l o' o'' -> WithRefreshedPattern e n l o o''
newtype WithRefreshedPattern' (e :: S -> Type) (n :: S) (l :: S) (o :: S) (o' :: S) = WithRefreshedPattern' ((Name n -> e o) -> Name l -> e o')
idWithRefreshedPattern' :: forall (e :: S -> Type) (o :: S) (o' :: S) (n :: S). (Sinkable e, DExt o o') => WithRefreshedPattern' e n n o o'
compWithRefreshedPattern' :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> Type) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithRefreshedPattern' e n i o o' -> WithRefreshedPattern' e i l o' o'' -> WithRefreshedPattern' e n l o o''
data DistinctEvidence (n :: S) where
- Distinct :: forall (n :: S). Distinct n => DistinctEvidence n
data ExtEvidence (n :: S) (l :: S) where
- Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l
assertDistinct :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l
assertExt :: forall pattern (n :: S) (l :: S). CoSinkable pattern => pattern n l -> ExtEvidence n l
unsafeDistinct :: forall (n :: S). DistinctEvidence n
unsafeExt :: forall (n :: S) (l :: S). ExtEvidence n l
unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n)
unsinkNamePattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Name l -> Maybe (Name n)
newtype UnsinkName (n :: S) (l :: S) (o :: S) (o' :: S) = UnsinkName (Name l -> Maybe (Name n))
idUnsinkName :: forall (n :: S) (o :: S) (o' :: S). UnsinkName n n o o'
compUnsinkName :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). UnsinkName n i o o' -> UnsinkName i l o' o'' -> UnsinkName n l o o''
data UnifyNameBinders (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S) where
- SameNameBinders :: forall (n :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n l -> UnifyNameBinders pattern n l l
- RenameLeftNameBinder :: forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n r -> (NameBinder n l -> NameBinder n r) -> UnifyNameBinders pattern n l r
- RenameRightNameBinder :: forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n l -> (NameBinder n r -> NameBinder n l) -> UnifyNameBinders pattern n l r
- RenameBothBinders :: forall (n :: S) (lr :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n lr -> (NameBinder n l -> NameBinder n lr) -> (NameBinder n r -> NameBinder n lr) -> UnifyNameBinders pattern n l r
- NotUnifiable :: forall (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S). UnifyNameBinders pattern n l r
unifyNameBinders :: forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). Distinct i => NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
unsafeMergeUnifyBinders :: forall (pattern :: S -> S -> Type) (a :: S) (a' :: S) (a'' :: S) (a''' :: S) (b' :: S) (b'' :: S). UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''
andThenUnifyPatterns :: forall pattern (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l') => UnifyNameBinders pattern n l l' -> (pattern l r, pattern l' r') -> UnifyNameBinders pattern n r r'
andThenUnifyNameBinders :: forall (pattern :: S -> S -> Type) (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l') => UnifyNameBinders pattern n l l' -> (NameBinder l r, NameBinder l' r') -> UnifyNameBinders pattern n r r'
newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet
unsafeMergeNameBinders :: forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S). NameBinders a b -> NameBinders c d -> NameBinders n l
emptyNameBinders :: forall (n :: S). NameBinders n n
mergeNameBinders :: forall (n :: S) (i :: S) (l :: S). NameBinders n i -> NameBinders i l -> NameBinders n l
nameBindersSingleton :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l
data NameBinderList (n :: S) (l :: S) where
- NameBinderListEmpty :: forall (n :: S). NameBinderList n n
- NameBinderListCons :: forall (n :: S) (i :: S) (l :: S). NameBinder n i -> NameBinderList i l -> NameBinderList n l
nameBindersList :: forall (n :: S) (l :: S). NameBinders n l -> NameBinderList n l
fromNameBindersList :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l
data V2 (n :: S) (l :: S)
absurd2 :: forall (n :: S) (l :: S) a. V2 n l -> a
data U2 (n :: S) (l :: S) where
- U2 :: forall (n :: S). U2 n n
class CoSinkable pattern => UnifiablePattern (pattern :: S -> S -> Type) where
- unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
class UnifiableInPattern a where
- unifyInPattern :: a -> a -> Bool
unsafeEqPattern :: forall pattern (n :: S) (l :: S) (n' :: S) (l' :: S). (UnifiablePattern pattern, Distinct n) => pattern n l -> pattern n' l' -> Bool
class Sinkable (e :: S -> Type) where
- sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> e n -> e l
sink :: forall e (n :: S) (l :: S). (Sinkable e, DExt n l) => e n -> e l
extendRenaming :: forall pattern (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern => (Name n -> Name n') -> pattern n l -> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) -> r
extendNameBinderRenaming :: forall pattern (i :: S) (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern => (NameBinder i n -> NameBinder i n') -> pattern n l -> (forall (l' :: S). (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r) -> r
composeNameBinderRenamings :: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S). (NameBinder n i -> NameBinder n i') -> (NameBinder i' l -> NameBinder i' l') -> NameBinder n l -> NameBinder n l'
fromNameBinderRenaming :: forall (n :: S) (l :: S) (l' :: S). (NameBinder n l -> NameBinder n l') -> Name l -> Name l'
extendRenamingNameBinder :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r
class CoSinkable (pattern :: S -> S -> Type) where
- coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> pattern n l -> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) -> r
- withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r) -> r
newtype WithNameBinderList (r :: S) (n :: S) (l :: S) (o :: S) (o' :: S) = WithNameBinderList (NameBinderList l r -> NameBinderList n r)
idWithNameBinderList :: forall (o :: S) (o' :: S) (r :: S) (n :: S). DExt o o' => WithNameBinderList r n n o o'
compWithNameBinderList :: forall (o :: S) (o' :: S) (o'' :: S) (r :: S) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithNameBinderList r n i o o' -> WithNameBinderList r i l o' o'' -> WithNameBinderList r n l o o''
nameBinderListOf :: forall binder (n :: S) (l :: S). CoSinkable binder => binder n l -> NameBinderList n l
newtype Substitution (e :: S -> Type) (i :: S) (o :: S) = UnsafeSubstitution (IntMap (e o))
lookupSubst :: forall e (i :: S) (o :: S). InjectName e => Substitution e i o -> Name i -> e o
identitySubst :: forall (e :: S -> Type) (i :: S). InjectName e => Substitution e i i
voidSubst :: forall (e :: S -> Type) (n :: S). Substitution e 'VoidS n
addSubst :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
addSubstPattern :: forall binder e (i :: S) (o :: S) (i' :: S). CoSinkable binder => Substitution e i o -> binder i i' -> [e o] -> Substitution e i' o
addSubstList :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinderList i i' -> [e o] -> Substitution e i' o
addRename :: forall (e :: S -> Type) (i :: S) (o :: S) (i' :: S). InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o
newtype NameMap (n :: S) a = NameMap {
- getNameMap :: IntMap a
}
emptyNameMap :: NameMap 'VoidS a
nameMapToSubstitution :: forall (i :: S) e (o :: S). NameMap i (e o) -> Substitution e i o
nameMapToScope :: forall (n :: S) a. NameMap n a -> Scope n
addNameBinders :: forall binder (n :: S) (l :: S) a. CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a
addNameBinderList :: forall (n :: S) (l :: S) a. NameBinderList n l -> [a] -> NameMap n a -> NameMap l a
lookupName :: forall (n :: S) a. Name n -> NameMap n a -> a
addNameBinder :: forall (n :: S) (l :: S) a. NameBinder n l -> a -> NameMap n a -> NameMap l a
type Id = Int
type RawName = Id
type RawScope = IntSet
rawFreshName :: RawScope -> RawName
rawMember :: RawName -> RawScope -> Bool
class ExtEndo (n :: S)
class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S)
class Distinct (n :: S)
type DExt (n :: S) (l :: S) = (Distinct l, Ext n l)
class InjectName (e :: S -> Type) where
- injectName :: forall (n :: S). Name n -> e n
data RenamingsK (as :: LoT k) (bs :: LoT k) where
- RNil :: RenamingsK 'LoT0 'LoT0
- RCons :: forall {k1} (a :: S) (b :: S) (as1 :: LoT k1) (bs1 :: LoT k1). (Name a -> Name b) -> RenamingsK as1 bs1 -> RenamingsK (a ':&&: as1) (b ':&&: bs1)
- RSkip :: forall {k1} {k2} (as1 :: LoT k1) (bs1 :: LoT k1) (k3 :: k2). RenamingsK as1 bs1 -> RenamingsK (k3 ':&&: as1) (k3 ':&&: bs1)
class SinkableK (f :: S -> k) where
- sinkabilityProofK :: forall (as :: LoT (S -> k)) (bs :: LoT (S -> k)) r. RenamingsK as bs -> (f :@@: as) -> (forall (cs :: LoT (S -> k)). RenamingsK as cs -> (f :@@: cs) -> r) -> r
sinkK :: forall {k} (f :: LoT k -> Type) (xs :: LoT (LoT k -> Type)) (as :: LoT (LoT k -> Type)) (bs :: LoT (LoT k -> Type)). GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> (f :@@: as) -> f :@@: bs
sinkabilityProof1 :: forall f (n :: S) (n' :: S). SinkableK f => (Name n -> Name n') -> f n -> f n'
gsinkabilityProof1 :: forall f (n :: S) (n' :: S). GSinkableK f => (Name n -> Name n') -> f (n ':&&: 'LoT0) -> f (n' ':&&: 'LoT0)
gsinkabilityProof2 :: forall f (n :: S) (n' :: S) (l :: S) r. GSinkableK f => (Name n -> Name n') -> f (n ':&&: (l ':&&: 'LoT0)) -> (forall (l' :: S). (Name l -> Name l') -> f (n' ':&&: (l' ':&&: 'LoT0)) -> r) -> r
gsinkabilityProofK' :: forall {k} f (as :: LoT k) (bs :: LoT k). GSinkableK f => RenamingsK as bs -> f as -> f bs
class GSinkableK (p :: LoT k -> Type) where
- gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> p as -> (forall (cs :: LoT k). RenamingsK as cs -> p cs -> r) -> r
gsinkK :: forall {k} f (xs :: LoT k) (as :: LoT k) (bs :: LoT k). GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f as -> f bs
class ExtractRenamingK (i :: TyVar k S) where
- extractRenamingK :: forall (as :: LoT k) (bs :: LoT k). RenamingsK as bs -> Name (Interpret ('Var i) as) -> Name (Interpret ('Var i) bs)
- putBackRenamingK :: forall (c :: S) (as :: LoT k) (bs :: LoT k). (Name (Interpret ('Var i) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT i c bs)
extractTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (as :: LoT k) (bs :: LoT k). (ExtractRenamingK i, ExtractRenamingK j) => RenamingsK as bs -> RenamingsK (Interpret ('Var i) as ':&&: (Interpret ('Var j) as ':&&: 'LoT0)) (Interpret ('Var i) bs ':&&: (Interpret ('Var j) bs ':&&: 'LoT0))
putBackTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (c1 :: S) (c2 :: S) (as :: LoT k) (bs :: LoT k). (ExtractRenamingK i, ExtractRenamingK j) => RenamingsK (Interpret ('Var i) as ':&&: (Interpret ('Var j) as ':&&: 'LoT0)) (c1 ':&&: (c2 ':&&: 'LoT0)) -> RenamingsK as bs -> RenamingsK as (PutBackLoT j c2 (PutBackLoT i c1 bs))
gunsafeWithPatternViaHasNameBinders :: forall pattern f (o :: S) (n :: S) (l :: S) r. (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern)) => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r) -> r
class HasNameBinders (f :: S -> S -> Type) where
- getNameBinders :: forall (n :: S) (l :: S). f n l -> NameBinders n l
- unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). f n l -> NameBinders n l' -> f n l'
- getNameBindersRaw :: forall (n :: S) (l :: S). f n l -> [RawName]
- reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). f n l -> [RawName] -> (f n l', [RawName])
ggetNameBinders :: forall f (n :: S) (l :: S). (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l
gunsafeSetNameBinders :: forall f (n :: S) (l :: S) (l' :: S). (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l'
class GHasNameBinders (f :: k -> Type) where
- ggetNameBindersRaw :: forall (as :: k). f as -> [RawName]
- greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). f as -> [RawName] -> (f bs, [RawName])

Safe types and operations

data S Source #

S is a data kind of scope indices.

Constructors

VoidS

VoidS is the only explicit scope available to the users, representing an empty scope. All other scopes are represented with type variables, bound in rank-2 polymophic functions like withFreshBinder.

Instances

Instances details

(SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) :: LoT k -> Type) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) cs -> r) -> r Source #

(SinkableK f, ExtractRenamingK i) => GSinkableK (Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) :: LoT k -> Type) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) cs -> r) -> r Source #

GSinkableK f => GSinkableK (Exists S f :: LoT k -> Type) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Exists S f as -> (forall (cs :: LoT k). RenamingsK as cs -> Exists S f cs -> r) -> r Source #

HasNameBinders f => GHasNameBinders (Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) :: LoT d -> Type) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

ggetNameBindersRaw :: forall (as :: LoT d). Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> [RawName] Source #

greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> [RawName] -> (Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) bs, [RawName]) Source #

SinkableK NameBinder Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

SinkableK NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

SinkableK NameBinders Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

SinkableK U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

SinkableK V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

GenericK NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK NameBinderList

Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (NameBinderList :@@: x) -> RepK NameBinderList x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK NameBinderList x -> NameBinderList :@@: x #

GenericK U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK U2
Instance details Defined in Control.Monad.Foil.Internal type RepK U2 = ((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (U2 :@@: x) -> RepK U2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK U2 x -> U2 :@@: x #

GenericK V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK V2
Instance details Defined in Control.Monad.Foil.Internal type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (V2 :@@: x) -> RepK V2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK V2 x -> V2 :@@: x #

ExtractRenamingK ('VZ :: TyVar (S -> xs) S) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

extractRenamingK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)). RenamingsK as bs -> Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) as) -> Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) bs) Source #

putBackRenamingK :: forall (c :: S) (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)). (Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT ('VZ :: TyVar (S -> xs) S) c bs) Source #

SinkableK (f a) => GSinkableK (Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) :: LoT (S -> xs) -> Type) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)) r. RenamingsK as bs -> Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) as -> (forall (cs :: LoT (S -> xs)). RenamingsK as cs -> Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) cs -> r) -> r Source #

SinkableK (f a b) => GSinkableK (Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) :: LoT (S -> xs) -> Type) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)) r. RenamingsK as bs -> Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) as -> (forall (cs :: LoT (S -> xs)). RenamingsK as cs -> Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) cs -> r) -> r 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 #

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 #

ExtractRenamingK x2 => ExtractRenamingK ('VS x2 :: TyVar (x1 -> xs) S) Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

extractRenamingK :: forall (as :: LoT (x1 -> xs)) (bs :: LoT (x1 -> xs)). RenamingsK as bs -> Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) as) -> Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) bs) Source #

putBackRenamingK :: forall (c :: S) (as :: LoT (x1 -> xs)) (bs :: LoT (x1 -> xs)). (Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT ('VS x2 :: TyVar (x1 -> xs) S) c bs) Source #

type RepK NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

type RepK U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

type RepK U2 = ((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)

type RepK V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

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

newtype Scope (n :: S) Source #

A safe scope, indexed by a type-level scope index n.

Constructors

UnsafeScope RawScope

Instances

Instances details

NFData (Scope n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods rnf :: Scope n -> () #

newtype Name (n :: S) Source #

A name in a safe scope, indexed by a type-level scope index n.

Constructors

UnsafeName RawName

Instances

Instances details

Sinkable Name Source #	Sinking a `Name` is as simple as applying the renaming.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l Source #
SinkableK Name Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (Name :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (Name :@@: cs) -> r) -> r Source #
RelMonad Name Expr Source #	`Expr` is a monad relative to `Name`.
Instance details Defined in Control.Monad.Foil.Example Methods rreturn :: forall (a :: S). Name a -> Expr a Source # rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> Expr a -> (Name a -> Expr b) -> Expr b 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 (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods showsPrec :: Int -> Name n -> ShowS # show :: Name n -> String # showList :: [Name n] -> ShowS #
NFData (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods rnf :: Name n -> () #
Eq (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods (==) :: Name n -> Name n -> Bool # (/=) :: Name n -> Name n -> Bool #
Ord (Name n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods compare :: Name n -> Name n -> Ordering # (<) :: Name n -> Name n -> Bool # (<=) :: Name n -> Name n -> Bool # (>) :: Name n -> Name n -> Bool # (>=) :: Name n -> Name n -> Bool # max :: Name n -> Name n -> Name n # min :: Name n -> Name n -> Name n #

nameId :: forall (l :: S). Name l -> Id Source #

Convert Name into an identifier. This may be useful for printing and debugging.

newtype NameBinder (n :: S) (l :: S) Source #

A name binder is a name that extends scope n to a (larger) scope l.

Constructors

UnsafeNameBinder (Name l)

Instances

Instances details

CoSinkable NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinder n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinder o o' -> r) -> r Source #
HasNameBinders NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods getNameBinders :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l Source # unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> NameBinders n l' -> NameBinder n l' Source # getNameBindersRaw :: forall (n :: S) (l :: S). NameBinder n l -> [RawName] Source # reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> [RawName] -> (NameBinder n l', [RawName]) Source #
UnifiablePattern NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinder n l -> NameBinder n r -> UnifyNameBinders NameBinder n l r 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 #
Show (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods showsPrec :: Int -> NameBinder n l -> ShowS # show :: NameBinder n l -> String # showList :: [NameBinder n l] -> ShowS #
NFData (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods rnf :: NameBinder n l -> () #
Eq (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods (==) :: NameBinder n l -> NameBinder n l -> Bool # (/=) :: NameBinder n l -> NameBinder n l -> Bool #
Ord (NameBinder n l) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods compare :: NameBinder n l -> NameBinder n l -> Ordering # (<) :: NameBinder n l -> NameBinder n l -> Bool # (<=) :: NameBinder n l -> NameBinder n l -> Bool # (>) :: NameBinder n l -> NameBinder n l -> Bool # (>=) :: NameBinder n l -> NameBinder n l -> Bool # max :: NameBinder n l -> NameBinder n l -> NameBinder n l # min :: NameBinder n l -> NameBinder n l -> NameBinder n l #
SinkableK NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinder :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinder :@@: cs) -> r) -> r Source #

emptyScope :: Scope 'VoidS Source #

An empty scope (without any names).

member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool Source #

A runtime check for potential name capture.

Extending scopes

extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l Source #

$O(\min(n,W))$. Extend a scope with one name (safely). Note that as long as the foil is used as intended, the name binder is guaranteed to introduce a name that does not appear in the initial scope.

extendScopePattern :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Scope n -> Scope l Source #

Extend scope with variables inside a pattern. This is a more flexible version of extendScope.

newtype ExtendScope (n :: S) (l :: S) (o :: S) (o' :: S) Source #

Auxiliary data structure for scope extension. Used in extendScopePattern.

Constructors

ExtendScope (Scope n -> Scope l)

idExtendScope :: forall (n :: S) (o :: S) (o' :: S). ExtendScope n n o o' Source #

Identity scope extension (no extension).

compExtendScope :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). ExtendScope n i o o' -> ExtendScope i l o' o'' -> ExtendScope n l o o'' Source #

Compose scope extensions.

Collecting new names

nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l Source #

Extract name from a name binder.

namesOfPattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> [Name l] Source #

Extract names from a pattern. This is a more flexible version of namesOf.

newtype NamesOf (n :: S) (l :: S) (o :: S) (o' :: S) Source #

Auxiliary structure collecting names in scope l that extend scope n. Used in namesOfPattern.

Constructors

NamesOf [Name l]

idNamesOf :: forall (n :: S) (o :: S) (o' :: S). NamesOf n n o o' Source #

Empty list of names in scope n.

compNamesOf :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o'' Source #

Concatenation of names, resulting in a list of names in l that extend scope n.

Refreshing binders

withFreshBinder :: forall (n :: S) r. Scope n -> (forall (l :: S). NameBinder n l -> r) -> r Source #

Allocate a fresh binder for a given scope.

withFresh :: forall (n :: S) r. Distinct n => Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r Source #

Safely produce a fresh name binder with respect to a given scope.

withFreshPattern Source #

Arguments

:: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
=> Scope o	Ambient scope.
-> pattern n l	Pattern to refresh (if it clashes with the ambient scope).
-> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)	Continuation, accepting the refreshed pattern.
-> r

Rename a given pattern into a fresh version of it to extend a given scope.

This is similar to withRefreshPattern, except here renaming always takes place.

withRefreshed Source #

Arguments

:: forall (o :: S) (i :: S) r. Distinct o
=> Scope o	Ambient scope.
-> Name i	Name to refresh (if it clashes with the ambient scope).
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)	Continuation, accepting the refreshed name.
-> r

Safely rename (if necessary) a given name to extend a given scope. This is similar to withFresh, except if the name does not clash with the scope, it can be used immediately, without renaming.

withRefreshedPattern Source #

Arguments

:: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
=> Scope o	Ambient scope.
-> pattern n l	Pattern to refresh (if it clashes with the ambient scope).
-> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)	Continuation, accepting the refreshed pattern.
-> r

Safely rename (if necessary) a given pattern to extend a given scope. This is similar to withFreshPattern, except if a name in the pattern does not clash with the scope, it can be used immediately, without renaming.

This is a more general version of withRefreshed.

withRefreshedPattern' :: forall pattern (o :: S) e (n :: S) (l :: S) r. (CoSinkable pattern, Distinct o, InjectName e, Sinkable e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r Source #

Refresh (if needed) bound variables introduced in a pattern.

This is a version of withRefreshedPattern that uses functional renamings instead of Substitution.

unsafeAssertFresh :: forall (n :: S) (l :: S) (n' :: S) (l' :: S) r. NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r Source #

Unsafely declare that a given name (binder) is already fresh in any scope n'.

newtype WithRefreshedPattern (e :: S -> Type) (n :: S) (l :: S) (o :: S) (o' :: S) Source #

Auxiliary structure to accumulate substitution extensions produced when refreshing a pattern. Used in withRefreshedPattern and withFreshPattern.

Constructors

WithRefreshedPattern (Substitution e n o -> Substitution e l o')

idWithRefreshedPattern :: forall (e :: S -> Type) (o :: S) (o' :: S) (n :: S). (Sinkable e, DExt o o') => WithRefreshedPattern e n n o o' Source #

Trivial substitution (coercion via sink).

compWithRefreshedPattern :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> Type) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithRefreshedPattern e n i o o' -> WithRefreshedPattern e i l o' o'' -> WithRefreshedPattern e n l o o'' Source #

Composition of substitution extensions.

newtype WithRefreshedPattern' (e :: S -> Type) (n :: S) (l :: S) (o :: S) (o' :: S) Source #

Auxiliary structure to accumulate substitution extensions produced when refreshing a pattern. Similar to WithRefreshedPattern, except here substitutions are represented as functions. Used in withRefreshedPattern'.

Constructors

WithRefreshedPattern' ((Name n -> e o) -> Name l -> e o')

idWithRefreshedPattern' :: forall (e :: S -> Type) (o :: S) (o' :: S) (n :: S). (Sinkable e, DExt o o') => WithRefreshedPattern' e n n o o' Source #

Trivial substitution extension (coercion via sink).

compWithRefreshedPattern' :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> Type) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithRefreshedPattern' e n i o o' -> WithRefreshedPattern' e i l o' o'' -> WithRefreshedPattern' e n l o o'' Source #

Composition of substitution extensions.

Extracting proofs from binders and patterns

data DistinctEvidence (n :: S) where Source #

Evidence that scope n contains distinct names.

Constructors

Distinct :: forall (n :: S). Distinct n => DistinctEvidence n

data ExtEvidence (n :: S) (l :: S) where Source #

Evidence that scope l extends scope n.

Constructors

Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l

assertDistinct :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l Source #

A distinct scope extended with a NameBinder is also distinct.

assertExt :: forall pattern (n :: S) (l :: S). CoSinkable pattern => pattern n l -> ExtEvidence n l Source #

A distinct scope extended with a NameBinder is also distinct.

unsafeDistinct :: forall (n :: S). DistinctEvidence n Source #

Unsafely declare that scope n is distinct. Used in unsafeAssertFresh.

unsafeExt :: forall (n :: S) (l :: S). ExtEvidence n l Source #

Unsafely declare that scope l extends scope n. Used in unsafeAssertFresh.

Unsinking names

unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n) Source #

Try coercing the name back to the (smaller) scope, given a binder that extends that scope.

unsinkNamePattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Name l -> Maybe (Name n) Source #

Check if a name in the extended context is introduced in a pattern or comes from the outer scope n.

This is a generalization of unsinkName.

newtype UnsinkName (n :: S) (l :: S) (o :: S) (o' :: S) Source #

Auxiliary structure for unsinking names. Used in unsinkNamePattern.

Constructors

UnsinkName (Name l -> Maybe (Name n))

idUnsinkName :: forall (n :: S) (o :: S) (o' :: S). UnsinkName n n o o' Source #

Trivial unsinking. If no scope extension took place, any name is free (since it cannot be bound by anything).

compUnsinkName :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S). UnsinkName n i o o' -> UnsinkName i l o' o'' -> UnsinkName n l o o'' Source #

Composition of unsinking for nested binders/patterns.

Unification of binders

data UnifyNameBinders (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S) where Source #

Unification result for two binders, extending some common scope to scopes l and r respectively.

Due to the implementation of the foil, we can often rename binders efficiently, by renaming binders only in one of the two unified terms.

Constructors

SameNameBinders	Binders are the same, proving that type parameters `l` and `r` are in fact equivalent.
Fields :: forall (n :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n l Unordered set of binders in the unified pattern (from any of the original patterns). -> UnifyNameBinders pattern n l l
RenameLeftNameBinder	It is possible to safely rename the left binder to match the right one.
Fields :: forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n r Unordered set of binders in the unified pattern (the binders from the right pattern). -> (NameBinder n l -> NameBinder n r) Binder renaming for the left pattern. -> UnifyNameBinders pattern n l r
RenameRightNameBinder	It is possible to safely rename the right binder to match the left one.
Fields :: forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n l Unordered set of binders in the unified pattern (the binders from the left pattern). -> (NameBinder n r -> NameBinder n l) Binder renaming for the right pattern. -> UnifyNameBinders pattern n l r
RenameBothBinders	It is necessary to rename both binders.
Fields :: forall (n :: S) (lr :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). NameBinders n lr Unordered set of binders in the unified pattern -> (NameBinder n l -> NameBinder n lr) Binder renaming for the left pattern. -> (NameBinder n r -> NameBinder n lr) Binder renaming for the right pattern. -> UnifyNameBinders pattern n l r
NotUnifiable :: forall (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S). UnifyNameBinders pattern n l r	Cannot unify to (sub)patterns.

unifyNameBinders Source #

Arguments

:: forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). Distinct i
=> NameBinder i l	Left pattern.
-> NameBinder i r	Right pattern.
-> UnifyNameBinders pattern i l r

Unify binders either by asserting that they are the same, or by providing a safe renaming function to convert one binder to another.

unsafeMergeUnifyBinders :: forall (pattern :: S -> S -> Type) (a :: S) (a' :: S) (a'' :: S) (a''' :: S) (b' :: S) (b'' :: S). UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b'' Source #

Unsafely merge results of unification for nested binders/patterns. Used in andThenUnifyPatterns.

andThenUnifyPatterns Source #

Arguments

:: forall pattern (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l')
=> UnifyNameBinders pattern n l l'	Unifying action for some outer patterns.
-> (pattern l r, pattern l' r')	Two nested patterns (cannot be unified directly since they extend different scopes).
-> UnifyNameBinders pattern n r r'

Chain unification of nested patterns.

andThenUnifyNameBinders Source #

Arguments

:: forall (pattern :: S -> S -> Type) (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l')
=> UnifyNameBinders pattern n l l'	Unifying action for some outer patterns.
-> (NameBinder l r, NameBinder l' r')	Two nested binders (cannot be unified directly since they extend different scopes).
-> UnifyNameBinders pattern n r r'

Chain unification of nested patterns with NameBinders.

newtype NameBinders (n :: S) (l :: S) Source #

An unordered collection of NameBinders, that together extend scope n to scope l.

For an ordered version see NameBinderList.

Constructors

UnsafeNameBinders IntSet

Instances

Instances details

CoSinkable NameBinders Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinders n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinders n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r) -> r Source #
SinkableK NameBinders Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinders :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinders :@@: cs) -> r) -> r Source #

unsafeMergeNameBinders :: forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S). NameBinders a b -> NameBinders c d -> NameBinders n l Source #

Unsafely merge sets of binders (via set union).

emptyNameBinders :: forall (n :: S). NameBinders n n Source #

An empty set of binders keeps the scope as is.

mergeNameBinders :: forall (n :: S) (i :: S) (l :: S). NameBinders n i -> NameBinders i l -> NameBinders n l Source #

Composition of sets of binders.

nameBindersSingleton :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l Source #

A singleton name binder set.

data NameBinderList (n :: S) (l :: S) where Source #

An ordered collection (list) of NameBinders, that together extend scope n to scope l.

For an unordered version see NameBinders.

Constructors

NameBinderListEmpty :: forall (n :: S). NameBinderList n n	An empty list of binders keeps the scope as is.
NameBinderListCons	A non-empty list of binders.
Fields :: forall (n :: S) (i :: S) (l :: S). NameBinder n i Outermost binder. -> NameBinderList i l Remaining list of binders. -> NameBinderList n l

Instances

Instances details

CoSinkable NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinderList n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r) -> r Source #

withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinderList n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinderList o o' -> r) -> r Source #

HasNameBinders NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

getNameBinders :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l Source #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> NameBinders n l' -> NameBinderList n l' Source #

getNameBindersRaw :: forall (n :: S) (l :: S). NameBinderList n l -> [RawName] Source #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> [RawName] -> (NameBinderList n l', [RawName]) Source #

UnifiablePattern NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinderList n l -> NameBinderList n r -> UnifyNameBinders NameBinderList n l r Source #

SinkableK NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

GenericK NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK NameBinderList

Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (NameBinderList :@@: x) -> RepK NameBinderList x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK NameBinderList x -> NameBinderList :@@: x #

type RepK NameBinderList Source #

Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

nameBindersList :: forall (n :: S) (l :: S). NameBinders n l -> NameBinderList n l Source #

Convert an unordered set of name binders into an ordered list (with some order).

fromNameBindersList :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l Source #

Convert an ordered list of name binders into an unordered set.

Pattern combinators

data V2 (n :: S) (l :: S) Source #

An empty pattern type specifies zero possibilities for patterns.

This type can be used to specify that patterns are not possible.

Instances

Instances details

CoSinkable V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> V2 n l -> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r) -> r Source #

withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> V2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r) -> r Source #

UnifiablePattern V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => V2 n l -> V2 n r -> UnifyNameBinders V2 n l r Source #

SinkableK V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

GenericK V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK V2
Instance details Defined in Control.Monad.Foil.Internal type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (V2 :@@: x) -> RepK V2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK V2 x -> V2 :@@: x #

type RepK V2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

absurd2 :: forall (n :: S) (l :: S) a. V2 n l -> a Source #

Since V2 values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".

data U2 (n :: S) (l :: S) where Source #

A unit pattern type corresponds to a wildcard pattern.

Constructors

U2
Fields :: forall (n :: S). U2 n n Wildcard patten does not modify the scope.

Instances

Instances details

CoSinkable U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> U2 n l -> (forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r) -> r Source #

withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> U2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r) -> r Source #

UnifiablePattern U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => U2 n l -> U2 n r -> UnifyNameBinders U2 n l r Source #

SinkableK U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Methods

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

GenericK U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK U2
Instance details Defined in Control.Monad.Foil.Internal type RepK U2 = ((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (U2 :@@: x) -> RepK U2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK U2 x -> U2 :@@: x #

type RepK U2 Source #

Instance details

Defined in Control.Monad.Foil.Internal

type RepK U2 = ((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)

Unifiable patterns

class CoSinkable pattern => UnifiablePattern (pattern :: S -> S -> Type) where Source #

A pattern type is unifiable if it is possible to match two patterns and decide how to rename binders.

Minimal complete definition

Nothing

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r Source #

Unify two patterns and decide which binders need to be renamed.

default unifyPatterns :: forall (n :: S) (l :: S) (r :: S). (CoSinkable pattern, Distinct n) => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r Source #

Instances

Instances details

UnifiablePattern NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinder n l -> NameBinder n r -> UnifyNameBinders NameBinder n l r Source #
UnifiablePattern NameBinderList Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinderList n l -> NameBinderList n r -> UnifyNameBinders NameBinderList n l r Source #
UnifiablePattern U2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => U2 n l -> U2 n r -> UnifyNameBinders U2 n l r Source #
UnifiablePattern V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => V2 n l -> V2 n r -> UnifyNameBinders V2 n l r Source #

class UnifiableInPattern a where Source #

Unification of values in patterns. By default, Eq instance is used, but it may be useful to ignore some data in pattens (such as location annotations).

Minimal complete definition

Nothing

Methods

unifyInPattern :: a -> a -> Bool Source #

Unify non-binding components of a pattern.

default unifyInPattern :: Eq a => a -> a -> Bool Source #

unsafeEqPattern :: forall pattern (n :: S) (l :: S) (n' :: S) (l' :: S). (UnifiablePattern pattern, Distinct n) => pattern n l -> pattern n' l' -> Bool Source #

The easiest way to compare two patterns is to check if they are the same. This function is labelled unsafe, since we generally are interested in proper α-equivalence instead of direct equality.

Safe sinking

class Sinkable (e :: S -> Type) where Source #

Sinking an expression from scope n into a (usualy extended) scope l, given the renaming (injection from scope n to scope l).

Minimal complete definition

Nothing

Methods

sinkabilityProof Source #

Arguments

:: forall (n :: S) (l :: S). (Name n -> Name l)	Map names from scope `n` to a (possibly larger) scope `l`.
-> e n	Expression with free variables in scope `n`.
-> e l

An implementation of this method that typechecks proves to the compiler that the expression is indeed Sinkable. However, instead of this implementation, sink should be used at all call sites for efficiency.

default sinkabilityProof :: forall (n :: S) (l :: S). (GenericK e, GSinkableK (RepK e)) => (Name n -> Name l) -> e n -> e l Source #

Instances

Instances details

Sinkable Expr Source #	This instance serves as a proof that sinking of `Expr` is safe.
Instance details Defined in Control.Monad.Foil.Example Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l Source #
Sinkable Name Source #	Sinking a `Name` is as simple as applying the renaming.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l Source #
Sinkable e => Sinkable (Substitution e i) Source #	Substitutions are sinkable as long as corresponding expressions are.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l 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 #
(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 #

sink :: forall e (n :: S) (l :: S). (Sinkable e, DExt n l) => e n -> e l Source #

Efficient version of sinkabilityProof. In fact, once sinkabilityProof typechecks, it is safe to sink by coercion. See Section 3.5 in «The Foil: Capture-Avoiding Substitution With No Sharp Edges» for the details.

extendRenaming Source #

Arguments

:: forall pattern (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern
=> (Name n -> Name n')	Map names from scope `n` to a (possibly larger) scope `n'`.
-> pattern n l	A pattern that extends scope `n` to another scope `l`.
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)	A continuation, accepting an extended renaming from `l` to `l'` (which itself extends `n'`) and a (possibly refreshed) pattern that extends `n'` to `l'`.
-> r

Extend renaming when going under a CoSinkable pattern (generalized binder). Note that the scope under pattern is independent of the codomain of the renaming.

This function is used to go under binders when implementing sinkabilityProof and is both a generalization of extendRenamingNameBinder and an efficient implementation of coSinkabilityProof.

extendNameBinderRenaming Source #

Arguments

:: forall pattern (i :: S) (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern
=> (NameBinder i n -> NameBinder i n')	Map names from scope `n` to a (possibly larger) scope `n'`.
-> pattern n l	A pattern that extends scope `n` to another scope `l`.
-> (forall (l' :: S). (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r)	A continuation, accepting an extended renaming from `l` to `l'` (which itself extends `n'`) and a (possibly refreshed) pattern that extends `n'` to `l'`.
-> r

Extend renaming of binders when going under a CoSinkable pattern (generalized binder). Note that the scope under pattern is independent of the codomain of the renaming.

composeNameBinderRenamings Source #

Arguments

:: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S). (NameBinder n i -> NameBinder n i')	Rename binders extending scope `n` from `i` to `i'`.
-> (NameBinder i' l -> NameBinder i' l')	Rename binders extending scope `i'` from `l` to `l'`.
-> NameBinder n l
-> NameBinder n l'

Safely compose renamings of name binders. The underlying implementation is

fromNameBinderRenaming :: forall (n :: S) (l :: S) (l' :: S). (NameBinder n l -> NameBinder n l') -> Name l -> Name l' Source #

Convert renaming of name binders into renaming of names in the inner scopes.

extendRenamingNameBinder Source #

Arguments

:: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n')	Map names from scope `n` to a (possibly larger) scope `n'`.
-> NameBinder n l	A name binder that extends scope `n` to another scope `l`.
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)	A continuation, accepting an extended renaming from `l` to `l'` (which itself extends `n'`) and a (possibly refreshed) binder that extends `n'` to `l'`.
-> r

Extend renaming when going under a NameBinder. Note that the scope under binder is independent of the codomain of the renaming.

Semantically, this function may need to rename the binder (resulting in the new scope l'), to make sure it does not clash with scope n'. However, as it turns out, the foil makes it safe to implement this function as a coercion. See Appendix A in «The Foil: Capture-Avoiding Substitution With No Sharp Edges» for the details.

This function is used to go under binders when implementing sinkabilityProof. A generalization of this function is extendRenaming (which is an efficient version of coSinkabilityProof).

class CoSinkable (pattern :: S -> S -> Type) where Source #

CoSinkable is to patterns (generalized binders) what Sinkable is to expressions.

See Section 2.3 of «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax» for more details.

Minimal complete definition

Nothing

Methods

coSinkabilityProof Source #

Arguments

:: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n')	Map names from scope `n` to a (possibly larger) scope `n'`.
-> pattern n l	A pattern that extends scope `n` to another scope `l`.
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)	A continuation, accepting an extended renaming from `l` to `l'` (which itself extends `n'`) and a (possibly refreshed) pattern that extends `n'` to `l'`.
-> r

An implementation of this method that typechecks proves to the compiler that the pattern is indeed CoSinkable. However, instead of this implementation, extendRenaming should be used at all call sites for efficiency.

default coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (GenericK pattern, GSinkableK (RepK pattern)) => (Name n -> Name n') -> pattern n l -> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) -> r Source #

withPattern Source #

Arguments

:: forall (o :: S) f (n :: S) (l :: S) r. Distinct o
=> (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')	Processing of a single `NameBinder`, this will be applied to each binder in a pattern.
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')	Result in case no binders are present. This can be seen as scope-indexed `mempty`.
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')	Composition of results for nested binders/patterns. This can be seen as scope-indexed `mappend`.
-> Scope o	Ambient scope.
-> pattern n l	Pattern to process.
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)	Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
-> r

Generalized processing of a pattern.

You can see withPattern as a CPS-style traversal over the binders in a pattern.

default withPattern :: forall (o :: S) f (n :: S) (l :: S) r. (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern)) => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r) -> r Source #

Instances

Instances details

CoSinkable NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinder n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinder o o' -> r) -> r Source #
CoSinkable NameBinderList Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinderList n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinderList n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinderList o o' -> r) -> r Source #
CoSinkable NameBinders Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinders n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> NameBinders n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r) -> r Source #
CoSinkable U2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> U2 n l -> (forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> U2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r) -> r Source #
CoSinkable V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> V2 n l -> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> V2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r) -> r Source #

newtype WithNameBinderList (r :: S) (n :: S) (l :: S) (o :: S) (o' :: S) Source #

Auxiliary data structure for collecting name binders. Used in nameBinderListOf.

Constructors

WithNameBinderList (NameBinderList l r -> NameBinderList n r)

idWithNameBinderList :: forall (o :: S) (o' :: S) (r :: S) (n :: S). DExt o o' => WithNameBinderList r n n o o' Source #

Empty list of name binders (identity).

compWithNameBinderList :: forall (o :: S) (o' :: S) (o'' :: S) (r :: S) (n :: S) (i :: S) (l :: S). (DExt o o', DExt o' o'') => WithNameBinderList r n i o o' -> WithNameBinderList r i l o' o'' -> WithNameBinderList r n l o o'' Source #

Concatenating lists of name binders (compose).

nameBinderListOf :: forall binder (n :: S) (l :: S). CoSinkable binder => binder n l -> NameBinderList n l Source #

Collect name binders of a generalized pattern into a name binder list, which can be more easily traversed.

Safe substitions

newtype Substitution (e :: S -> Type) (i :: S) (o :: S) Source #

A substitution is a mapping from names in scope i to expressions e o in scope o.

Constructors

UnsafeSubstitution (IntMap (e o))

Instances

Instances details

Sinkable e => Sinkable (Substitution e i) Source #	Substitutions are sinkable as long as corresponding expressions are.
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l Source #

lookupSubst :: forall e (i :: S) (o :: S). InjectName e => Substitution e i o -> Name i -> e o Source #

Apply substitution to a given name.

identitySubst :: forall (e :: S -> Type) (i :: S). InjectName e => Substitution e i i Source #

Identity substitution maps all names to expresion-variables.

voidSubst :: forall (e :: S -> Type) (n :: S). Substitution e 'VoidS n Source #

An empty substitution from an empty scope.

addSubst :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o Source #

Extend substitution with a particular mapping.

addSubstPattern :: forall binder e (i :: S) (o :: S) (i' :: S). CoSinkable binder => Substitution e i o -> binder i i' -> [e o] -> Substitution e i' o Source #

addSubstList :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinderList i i' -> [e o] -> Substitution e i' o Source #

addRename :: forall (e :: S -> Type) (i :: S) (o :: S) (i' :: S). InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o Source #

Add variable renaming to a substitution. This includes the performance optimization of eliding names mapped to themselves.

`Name` maps

newtype NameMap (n :: S) a Source #

A total map from names in scope n to elements of type a.

Constructors

NameMap
Fields getNameMap :: IntMap a

Instances

Instances details

Foldable (NameMap n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods fold :: Monoid m => NameMap n m -> m # foldMap :: Monoid m => (a -> m) -> NameMap n a -> m # foldMap' :: Monoid m => (a -> m) -> NameMap n a -> m # foldr :: (a -> b -> b) -> b -> NameMap n a -> b # foldr' :: (a -> b -> b) -> b -> NameMap n a -> b # foldl :: (b -> a -> b) -> b -> NameMap n a -> b # foldl' :: (b -> a -> b) -> b -> NameMap n a -> b # foldr1 :: (a -> a -> a) -> NameMap n a -> a # foldl1 :: (a -> a -> a) -> NameMap n a -> a # toList :: NameMap n a -> [a] # null :: NameMap n a -> Bool # length :: NameMap n a -> Int # elem :: Eq a => a -> NameMap n a -> Bool # maximum :: Ord a => NameMap n a -> a # minimum :: Ord a => NameMap n a -> a # sum :: Num a => NameMap n a -> a # product :: Num a => NameMap n a -> a #
Traversable (NameMap n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods traverse :: Applicative f => (a -> f b) -> NameMap n a -> f (NameMap n b) # sequenceA :: Applicative f => NameMap n (f a) -> f (NameMap n a) # mapM :: Monad m => (a -> m b) -> NameMap n a -> m (NameMap n b) # sequence :: Monad m => NameMap n (m a) -> m (NameMap n a) #
Functor (NameMap n) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods fmap :: (a -> b) -> NameMap n a -> NameMap n b # (<$) :: a -> NameMap n b -> NameMap n a #

emptyNameMap :: NameMap 'VoidS a Source #

An empty map belongs in the empty scope.

nameMapToSubstitution :: forall (i :: S) e (o :: S). NameMap i (e o) -> Substitution e i o Source #

Convert a NameMap of expressions into a Substitution.

nameMapToScope :: forall (n :: S) a. NameMap n a -> Scope n Source #

Convert a NameMap of expressions into a Scope.

addNameBinders :: forall binder (n :: S) (l :: S) a. CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a Source #

Extend a map with multiple mappings (by repeatedly applying addNameBinder).

Note that the input list is expected to have at least the same number of elements as there are binders in the input pattern (generalized binder).

addNameBinderList :: forall (n :: S) (l :: S) a. NameBinderList n l -> [a] -> NameMap n a -> NameMap l a Source #

Extend a map with multiple mappings (by repeatedly applying addNameBinder).

Note that the input list is expected to have at least the same number of elements as there are binders in the input name binder list.

See also addNameBinders for a generalized version.

lookupName :: forall (n :: S) a. Name n -> NameMap n a -> a Source #

Looking up a name should always succeed.

Note that since Name is Sinkable, you can lookup a name from scope n in a NameMap for scope l whenever l extends n.

addNameBinder :: forall (n :: S) (l :: S) a. NameBinder n l -> a -> NameMap n a -> NameMap l a Source #

Extending a map with a single mapping.

Note that the scope parameter of the result differs from the initial map.

Raw types and operations

type Id = Int Source #

We will use Int for efficient representation of identifiers.

type RawName = Id Source #

Raw name is simply an identifier.

type RawScope = IntSet Source #

A raw scope is a set of raw names.

rawFreshName :: RawScope -> RawName Source #

$O(\min(n, W))$. Generate a fresh raw name that does not appear in a given raw scope.

rawMember :: RawName -> RawScope -> Bool Source #

Check if a raw name is contained in a raw scope.

Constraints

class ExtEndo (n :: S) Source #

Every scope is a (trivial) extension of itself.

Important: this class exists to assist tracking scope extensions for type variables of kind S. Users of the foil are not supposed to implement any instances of ExtEndo.

class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S) Source #

Some scopes are extensions of other scopes.

Important: this class exists to assist tracking scope extensions for type variables of kind S. Users of the foil are not supposed to implement any instances of Ext.

Instances

Instances details

(ExtEndo n => ExtEndo l) => Ext n l Source #
Instance details Defined in Control.Monad.Foil.Internal

class Distinct (n :: S) Source #

Scopes with distinct names.

Important: this class exists to explicitly mark scopes with distinct names. Users of the foil are not supposed to implement any instances of Distinct.

Instances

Instances details

Distinct 'VoidS Source #
Instance details Defined in Control.Monad.Foil.Internal

type DExt (n :: S) (l :: S) = (Distinct l, Ext n l) Source #

Scope extensions with distinct names.

class InjectName (e :: S -> Type) where Source #

Instances of this typeclass possess the ability to inject names. Usually, this is a variable data constructor.

Methods

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

Inject names into expressions.

Instances

Instances details

InjectName Expr Source #
Instance details Defined in Control.Monad.Foil.Example Methods injectName :: forall (n :: S). Name n -> Expr n Source #
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 #

Kind-polymorphic sinkability

data RenamingsK (as :: LoT k) (bs :: LoT k) where Source #

Constructors

RNil :: RenamingsK 'LoT0 'LoT0
RCons :: forall {k1} (a :: S) (b :: S) (as1 :: LoT k1) (bs1 :: LoT k1). (Name a -> Name b) -> RenamingsK as1 bs1 -> RenamingsK (a ':&&: as1) (b ':&&: bs1)
RSkip :: forall {k1} {k2} (as1 :: LoT k1) (bs1 :: LoT k1) (k3 :: k2). RenamingsK as1 bs1 -> RenamingsK (k3 ':&&: as1) (k3 ':&&: bs1)

class SinkableK (f :: S -> k) where Source #

Minimal complete definition

Nothing

Methods

sinkabilityProofK :: forall (as :: LoT (S -> k)) (bs :: LoT (S -> k)) r. RenamingsK as bs -> (f :@@: as) -> (forall (cs :: LoT (S -> k)). RenamingsK as cs -> (f :@@: cs) -> r) -> r Source #

default sinkabilityProofK :: forall (as :: LoT (S -> k)) (bs :: LoT (S -> k)) r. (GenericK f, GSinkableK (RepK f)) => RenamingsK as bs -> (f :@@: as) -> (forall (cs :: LoT (S -> k)). RenamingsK as cs -> (f :@@: cs) -> r) -> r Source #

Instances

Instances details

SinkableK Name Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (Name :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (Name :@@: cs) -> r) -> r Source #
(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) => 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 #
SinkableK NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinder :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinder :@@: cs) -> r) -> r Source #
SinkableK NameBinderList Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinderList :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinderList :@@: cs) -> r) -> r Source #
SinkableK NameBinders Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinders :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinders :@@: cs) -> r) -> r Source #
SinkableK U2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (U2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (U2 :@@: cs) -> r) -> r Source #
SinkableK V2 Source #
Instance details Defined in Control.Monad.Foil.Internal Methods sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (V2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (V2 :@@: cs) -> r) -> r Source #

sinkK :: forall {k} (f :: LoT k -> Type) (xs :: LoT (LoT k -> Type)) (as :: LoT (LoT k -> Type)) (bs :: LoT (LoT k -> Type)). GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> (f :@@: as) -> f :@@: bs Source #

sinkabilityProof1 :: forall f (n :: S) (n' :: S). SinkableK f => (Name n -> Name n') -> f n -> f n' Source #

gsinkabilityProof1 :: forall f (n :: S) (n' :: S). GSinkableK f => (Name n -> Name n') -> f (n ':&&: 'LoT0) -> f (n' ':&&: 'LoT0) Source #

gsinkabilityProof2 :: forall f (n :: S) (n' :: S) (l :: S) r. GSinkableK f => (Name n -> Name n') -> f (n ':&&: (l ':&&: 'LoT0)) -> (forall (l' :: S). (Name l -> Name l') -> f (n' ':&&: (l' ':&&: 'LoT0)) -> r) -> r Source #

gsinkabilityProofK' :: forall {k} f (as :: LoT k) (bs :: LoT k). GSinkableK f => RenamingsK as bs -> f as -> f bs Source #

class GSinkableK (p :: LoT k -> Type) where Source #

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> p as -> (forall (cs :: LoT k). RenamingsK as cs -> p cs -> r) -> r Source #

Instances

Instances details

GSinkableK (U1 :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> U1 as -> (forall (cs :: LoT k). RenamingsK as cs -> U1 cs -> r) -> r Source #
GSinkableK (V1 :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> V1 as -> (forall (cs :: LoT k). RenamingsK as cs -> V1 cs -> r) -> r Source #
(SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) cs -> r) -> r Source #
(SinkableK f, ExtractRenamingK i) => GSinkableK (Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) cs -> r) -> r Source #
(Bifunctor f, GSinkableK (Field x), GSinkableK (Field y)) => GSinkableK (Field ((('Kon f :: Atom k (Type -> Type -> Type)) ':@: x) ':@: y) :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field ((('Kon f :: Atom k (Type -> Type -> Type)) ':@: x) ':@: y) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field ((('Kon f :: Atom k (Type -> Type -> Type)) ':@: x) ':@: y) cs -> r) -> r Source #
(Functor f, GSinkableK (Field x)) => GSinkableK (Field (('Kon f :: Atom k (Type -> Type)) ':@: x) :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field (('Kon f :: Atom k (Type -> Type)) ':@: x) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field (('Kon f :: Atom k (Type -> Type)) ':@: x) cs -> r) -> r Source #
GSinkableK (Field ('Kon a :: Atom k Type) :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field ('Kon a :: Atom k Type) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field ('Kon a :: Atom k Type) cs -> r) -> r Source #
GSinkableK (Field ('Var a) :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field ('Var a) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field ('Var a) cs -> r) -> r Source #
(GSinkableK f, GSinkableK g) => GSinkableK (f :*: g :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> (f :: g) as -> (forall (cs :: LoT k). RenamingsK as cs -> (f :: g) cs -> r) -> r Source #
(GSinkableK f, GSinkableK g) => GSinkableK (f :+: g :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> (f :+: g) as -> (forall (cs :: LoT k). RenamingsK as cs -> (f :+: g) cs -> r) -> r Source #
GSinkableK f => GSinkableK ((a :~~: b) :=>: f :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> ((a :~~: b) :=>: f) as -> (forall (cs :: LoT k). RenamingsK as cs -> ((a :~~: b) :=>: f) cs -> r) -> r Source #
GSinkableK f => GSinkableK (Exists S f :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Exists S f as -> (forall (cs :: LoT k). RenamingsK as cs -> Exists S f cs -> r) -> r Source #
GSinkableK f => GSinkableK (Exists k2 f :: LoT k1 -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k1) (bs :: LoT k1) r. RenamingsK as bs -> Exists k2 f as -> (forall (cs :: LoT k1). RenamingsK as cs -> Exists k2 f cs -> r) -> r Source #
GSinkableK f => GSinkableK (M1 i c f :: LoT k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> M1 i c f as -> (forall (cs :: LoT k). RenamingsK as cs -> M1 i c f cs -> r) -> r Source #
SinkableK (f a) => GSinkableK (Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) :: LoT (S -> xs) -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)) r. RenamingsK as bs -> Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) as -> (forall (cs :: LoT (S -> xs)). RenamingsK as cs -> Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) cs -> r) -> r Source #
SinkableK (f a b) => GSinkableK (Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) :: LoT (S -> xs) -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods gsinkabilityProofK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)) r. RenamingsK as bs -> Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) as -> (forall (cs :: LoT (S -> xs)). RenamingsK as cs -> Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) cs -> r) -> r Source #

gsinkK :: forall {k} f (xs :: LoT k) (as :: LoT k) (bs :: LoT k). GSinkableK f => RenamingsK xs as -> RenamingsK xs bs -> f as -> f bs Source #

class ExtractRenamingK (i :: TyVar k S) where Source #

Methods

extractRenamingK :: forall (as :: LoT k) (bs :: LoT k). RenamingsK as bs -> Name (Interpret ('Var i) as) -> Name (Interpret ('Var i) bs) Source #

putBackRenamingK :: forall (c :: S) (as :: LoT k) (bs :: LoT k). (Name (Interpret ('Var i) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT i c bs) Source #

Instances

Instances details

ExtractRenamingK ('VZ :: TyVar (S -> xs) S) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods extractRenamingK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)). RenamingsK as bs -> Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) as) -> Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) bs) Source # putBackRenamingK :: forall (c :: S) (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)). (Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT ('VZ :: TyVar (S -> xs) S) c bs) Source #
ExtractRenamingK x2 => ExtractRenamingK ('VS x2 :: TyVar (x1 -> xs) S) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods extractRenamingK :: forall (as :: LoT (x1 -> xs)) (bs :: LoT (x1 -> xs)). RenamingsK as bs -> Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) as) -> Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) bs) Source # putBackRenamingK :: forall (c :: S) (as :: LoT (x1 -> xs)) (bs :: LoT (x1 -> xs)). (Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT ('VS x2 :: TyVar (x1 -> xs) S) c bs) Source #

extractTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (as :: LoT k) (bs :: LoT k). (ExtractRenamingK i, ExtractRenamingK j) => RenamingsK as bs -> RenamingsK (Interpret ('Var i) as ':&&: (Interpret ('Var j) as ':&&: 'LoT0)) (Interpret ('Var i) bs ':&&: (Interpret ('Var j) bs ':&&: 'LoT0)) Source #

putBackTwoRenamingsK :: forall k (i :: TyVar k S) (j :: TyVar k S) (c1 :: S) (c2 :: S) (as :: LoT k) (bs :: LoT k). (ExtractRenamingK i, ExtractRenamingK j) => RenamingsK (Interpret ('Var i) as ':&&: (Interpret ('Var j) as ':&&: 'LoT0)) (c1 ':&&: (c2 ':&&: 'LoT0)) -> RenamingsK as bs -> RenamingsK as (PutBackLoT j c2 (PutBackLoT i c1 bs)) Source #

Kind-polymorphic types with binders

Generic version of `withPattern`

gunsafeWithPatternViaHasNameBinders Source #

Arguments

:: forall pattern f (o :: S) (n :: S) (l :: S) r. (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern))
=> (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')	Processing of a single `NameBinder`, this will be applied to each binder in a pattern.
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')	Result in case no binders are present. This can be seen as scope-indexed `mempty`.
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')	Composition of results for nested binders/patterns. This can be seen as scope-indexed `mappend`.
-> Scope o	Ambient scope.
-> pattern n l	Pattern to process.
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)	Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
-> r

Generic generalized processing of a pattern via GHasNameBinders.

This can be used as a default implementation of withPattern.

Manipulating nested `NameBinder`s

class HasNameBinders (f :: S -> S -> Type) where Source #

If HasNameBinders f, then f n l is expected to act as a binder, introducing into scope n some local variables, extending it to scope l. This class allows to extract and modify the set of binders.

Minimal complete definition

Nothing

Methods

getNameBinders :: forall (n :: S) (l :: S). f n l -> NameBinders n l Source #

Extract a set of binders from a pattern.

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). f n l -> NameBinders n l' -> f n l' Source #

Replace binders in a pattern.

This function is unsafe, because it does not check if the new set of binders has the same size. It can therefore crash at runtime.

You should probably not use this. This is only used for gunsafeWithPatternViaHasNameBinders, which is then safe to use.

getNameBindersRaw :: forall (n :: S) (l :: S). f n l -> [RawName] Source #

Extract RawNames of all binders occurring in a pattern.

default getNameBindersRaw :: forall (n :: S) (l :: S). (GenericK f, GHasNameBinders (RepK f)) => f n l -> [RawName] Source #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). f n l -> [RawName] -> (f n l', [RawName]) Source #

This is a version of unsafeSetNameBinders that takes in a list of RawNames.

It does not check if the given list has enough elements. It does not check if the raw names are fresh in the scope n. It does not check if the raw names given are distinct.

You should never use this. This is only used for generic implementation of HasNameBinders.

default reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> [RawName] -> (f n l', [RawName]) Source #

Instances

Instances details

HasNameBinders NameBinder Source #
Instance details Defined in Control.Monad.Foil.Internal Methods getNameBinders :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l Source # unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> NameBinders n l' -> NameBinder n l' Source # getNameBindersRaw :: forall (n :: S) (l :: S). NameBinder n l -> [RawName] Source # reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> [RawName] -> (NameBinder n l', [RawName]) Source #
HasNameBinders NameBinderList Source #
Instance details Defined in Control.Monad.Foil.Internal Methods getNameBinders :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l Source # unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> NameBinders n l' -> NameBinderList n l' Source # getNameBindersRaw :: forall (n :: S) (l :: S). NameBinderList n l -> [RawName] Source # reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> [RawName] -> (NameBinderList n l', [RawName]) Source #

Generic

ggetNameBinders :: forall f (n :: S) (l :: S). (GenericK f, GHasNameBinders (RepK f)) => f n l -> NameBinders n l Source #

gunsafeSetNameBinders :: forall f (n :: S) (l :: S) (l' :: S). (GenericK f, GValidNameBinders f (RepK f), GHasNameBinders (RepK f)) => f n l -> NameBinders n l' -> f n l' Source #

class GHasNameBinders (f :: k -> Type) where Source #

Methods

ggetNameBindersRaw :: forall (as :: k). f as -> [RawName] Source #

greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). f as -> [RawName] -> (f bs, [RawName]) Source #

Instances

Instances details

GHasNameBinders (U1 :: k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: k). U1 as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). U1 as -> [RawName] -> (U1 bs, [RawName]) Source #
GHasNameBinders (V1 :: k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: k). V1 as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). V1 as -> [RawName] -> (V1 bs, [RawName]) Source #
(GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :*: g :: k -> Type) Source #	FIXME: this is, perhaps, the most "unsafe" place for the user since it does not reject "parallel" binders: data BadPattern n l = BadPattern (NameBinder n l) (NameBinder n l) This instance will treat both binders in the same way as "nested": data GoodPattern n l = forall i. GoodPattern (NameBinder n i) (NameBinder i l) However, Template Haskell code at the moment will never generate "parallel" binders, and the very user is unlikely to misuse this instance, since "parallel" binders require extra effort to support it. Still, it would be better to detect and reject any "parallel" or otherwise improper binders.
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: k). (f :: g) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). (f :: g) as -> [RawName] -> ((f :*: g) bs, [RawName]) Source #
(GHasNameBinders f, GHasNameBinders g) => GHasNameBinders (f :+: g :: k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: k). (f :+: g) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). (f :+: g) as -> [RawName] -> ((f :+: g) bs, [RawName]) Source #
GHasNameBinders f => GHasNameBinders (M1 i c f :: k -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: k). M1 i c f as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: k) (bs :: k). M1 i c f as -> [RawName] -> (M1 i c f bs, [RawName]) Source #
HasNameBinders f => GHasNameBinders (Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) :: LoT d -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: LoT d). Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> [RawName] -> (Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) bs, [RawName]) Source #
GHasNameBinders (Field (('Kon f :: Atom d (k1 -> Type)) ':@: 'Var i) :: LoT d -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: LoT d). Field (('Kon f :: Atom d (k1 -> Type)) ':@: 'Var i) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Field (('Kon f :: Atom d (k1 -> Type)) ':@: 'Var i) as -> [RawName] -> (Field (('Kon f :: Atom d (k1 -> Type)) ':@: 'Var i) bs, [RawName]) Source #
GHasNameBinders (Field ('Kon a :: Atom d Type) :: LoT d -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: LoT d). Field ('Kon a :: Atom d Type) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Field ('Kon a :: Atom d Type) as -> [RawName] -> (Field ('Kon a :: Atom d Type) bs, [RawName]) Source #
GHasNameBinders (Field ('Var x) :: LoT d -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: LoT d). Field ('Var x) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Field ('Var x) as -> [RawName] -> (Field ('Var x) bs, [RawName]) Source #
GHasNameBinders f => GHasNameBinders (('Var i :~~: 'Var j) :=>: f :: LoT d -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: LoT d). (('Var i :~~: 'Var j) :=>: f) as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). (('Var i :~~: 'Var j) :=>: f) as -> [RawName] -> ((('Var i :~~: 'Var j) :=>: f) bs, [RawName]) Source #
GHasNameBinders f => GHasNameBinders (Exists k f :: LoT d -> Type) Source #
Instance details Defined in Control.Monad.Foil.Internal Methods ggetNameBindersRaw :: forall (as :: LoT d). Exists k f as -> [RawName] Source # greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Exists k f as -> [RawName] -> (Exists k f bs, [RawName]) Source #

Safe types and operations

Instances

Instances

Instances

Instances

Extending scopes

Collecting new names

Refreshing binders

Extracting proofs from binders and patterns

Unsinking names

Unification of binders

Instances

Instances

Pattern combinators

Instances

Instances

Unifiable patterns

Instances

Safe sinking

Instances

Instances

Safe substitions

Instances

Name maps

Instances

Raw types and operations

Constraints

Instances

Instances

Instances

Kind-polymorphic sinkability

Instances

Instances

Instances

Kind-polymorphic types with binders

Generic version of withPattern

Manipulating nested NameBinders

Instances

Generic

Instances

`Name` maps

Generic version of `withPattern`

Manipulating nested `NameBinder`s