module UVMHS.Lib.Substitution where

import UVMHS.Core
import UVMHS.Lib.Variables
import UVMHS.Lib.Pretty
import UVMHS.Lib.Parser
import UVMHS.Lib.Rand

--------------------------
-- SUBSTITUTION ELEMENT --
--------------------------

-- ℯ ⩴ s⇈e
data SubstElem s e = SubstElem
  { forall s e. SubstElem s e -> s ⇰ ℕ64
substElemIntro ∷ s ⇰ ℕ64
  , forall s e. SubstElem s e -> () -> 𝑂 e
substElemValue ∷ () → 𝑂 e
  } deriving (SubstElem s e -> SubstElem s e -> Bool
(SubstElem s e -> SubstElem s e -> Bool)
-> (SubstElem s e -> SubstElem s e -> Bool) -> Eq (SubstElem s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e. (Eq s, Eq e) => SubstElem s e -> SubstElem s e -> Bool
$c== :: forall s e. (Eq s, Eq e) => SubstElem s e -> SubstElem s e -> Bool
== :: SubstElem s e -> SubstElem s e -> Bool
$c/= :: forall s e. (Eq s, Eq e) => SubstElem s e -> SubstElem s e -> Bool
/= :: SubstElem s e -> SubstElem s e -> Bool
Eq,Eq (SubstElem s e)
Eq (SubstElem s e) =>
(SubstElem s e -> SubstElem s e -> Ordering)
-> (SubstElem s e -> SubstElem s e -> Bool)
-> (SubstElem s e -> SubstElem s e -> Bool)
-> (SubstElem s e -> SubstElem s e -> Bool)
-> (SubstElem s e -> SubstElem s e -> Bool)
-> (SubstElem s e -> SubstElem s e -> SubstElem s e)
-> (SubstElem s e -> SubstElem s e -> SubstElem s e)
-> Ord (SubstElem s e)
SubstElem s e -> SubstElem s e -> Bool
SubstElem s e -> SubstElem s e -> Ordering
SubstElem s e -> SubstElem s e -> SubstElem s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (SubstElem s e)
forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Bool
forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Ordering
forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> SubstElem s e
$ccompare :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Ordering
compare :: SubstElem s e -> SubstElem s e -> Ordering
$c< :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Bool
< :: SubstElem s e -> SubstElem s e -> Bool
$c<= :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Bool
<= :: SubstElem s e -> SubstElem s e -> Bool
$c> :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Bool
> :: SubstElem s e -> SubstElem s e -> Bool
$c>= :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> Bool
>= :: SubstElem s e -> SubstElem s e -> Bool
$cmax :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> SubstElem s e
max :: SubstElem s e -> SubstElem s e -> SubstElem s e
$cmin :: forall s e.
(Ord s, Ord e) =>
SubstElem s e -> SubstElem s e -> SubstElem s e
min :: SubstElem s e -> SubstElem s e -> SubstElem s e
Ord,Int -> SubstElem s e -> ShowS
[SubstElem s e] -> ShowS
SubstElem s e -> String
(Int -> SubstElem s e -> ShowS)
-> (SubstElem s e -> String)
-> ([SubstElem s e] -> ShowS)
-> Show (SubstElem s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> SubstElem s e -> ShowS
forall s e. (Show s, Show e) => [SubstElem s e] -> ShowS
forall s e. (Show s, Show e) => SubstElem s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> SubstElem s e -> ShowS
showsPrec :: Int -> SubstElem s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => SubstElem s e -> String
show :: SubstElem s e -> String
$cshowList :: forall s e. (Show s, Show e) => [SubstElem s e] -> ShowS
showList :: [SubstElem s e] -> ShowS
Show)
makeLenses ''SubstElem

instance (Pretty s,Pretty e) ⇒ Pretty (SubstElem s e) where
  pretty :: SubstElem s e -> Doc
pretty (SubstElem s ⇰ ℕ64
s () -> 𝑂 e
ueO) = ℕ64 -> Doc -> Doc -> Doc -> Doc
ppInfr ℕ64
pASC (𝕊 -> Doc
ppPun 𝕊
"⇈") ((s ⇰ ℕ64) -> Doc
forall a. Pretty a => a -> Doc
pretty s ⇰ ℕ64
s) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    Doc -> 𝑂 Doc -> Doc
forall a. a -> 𝑂 a -> a
ifNone (𝕊 -> Doc
ppPun 𝕊
"⊥") (𝑂 Doc -> Doc) -> 𝑂 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ e -> Doc
forall a. Pretty a => a -> Doc
pretty (e -> Doc) -> 𝑂 e -> 𝑂 Doc
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ () -> 𝑂 e
ueO ()

instance (Ord s,Fuzzy s,Fuzzy e) ⇒ Fuzzy (SubstElem s e) where
  fuzzy :: FuzzyM (SubstElem s e)
fuzzy = do
    s ⇰ ℕ64
𝑠 ← FuzzyM (s ⇰ ℕ64)
forall a. Fuzzy a => FuzzyM a
fuzzy
    () -> 𝑂 e
ueO ← FuzzyM (() -> 𝑂 e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    SubstElem s e -> FuzzyM (SubstElem s e)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (SubstElem s e -> FuzzyM (SubstElem s e))
-> SubstElem s e -> FuzzyM (SubstElem s e)
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
forall s e. (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
SubstElem s ⇰ ℕ64
𝑠 () -> 𝑂 e
ueO

introSubstElem ∷ (Ord s) ⇒ s ⇰ ℕ64 → SubstElem s e → SubstElem s e
introSubstElem :: forall s e. Ord s => (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e
introSubstElem = (SubstElem s e ⟢ (s ⇰ ℕ64))
-> ((s ⇰ ℕ64) -> s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstElem s e ⟢ (s ⇰ ℕ64)
forall s e. SubstElem s e ⟢ (s ⇰ ℕ64)
substElemIntroL (((s ⇰ ℕ64) -> s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e)
-> ((s ⇰ ℕ64) -> (s ⇰ ℕ64) -> s ⇰ ℕ64)
-> (s ⇰ ℕ64)
-> SubstElem s e
-> SubstElem s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⇰ ℕ64) -> (s ⇰ ℕ64) -> s ⇰ ℕ64
forall a. Plus a => a -> a -> a
(+)

subSubstElem ∷ (s ⇰ ℕ64 → e → 𝑂 e) → SubstElem s e → SubstElem s e
subSubstElem :: forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
subSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE (SubstElem s ⇰ ℕ64
𝑠 () -> 𝑂 e
ueO) = (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
forall s e. (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
SubstElem s ⇰ ℕ64
forall a. Zero a => a
zero ((() -> 𝑂 e) -> SubstElem s e) -> (() -> 𝑂 e) -> SubstElem s e
forall a b. (a -> b) -> a -> b
$ \ () → (s ⇰ ℕ64) -> e -> 𝑂 e
substE s ⇰ ℕ64
𝑠 (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ () -> 𝑂 e
ueO ()

--------------------------------
-- SCOPED SUBSTITUION ELEMENT --
--------------------------------

-- ℯ ⩴ i | s⇈e
data SSubstElem s e = 
    Var_SSE ℕ64
  | Trm_SSE (SubstElem s e)
  deriving (SSubstElem s e -> SSubstElem s e -> Bool
(SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> Eq (SSubstElem s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e.
(Eq s, Eq e) =>
SSubstElem s e -> SSubstElem s e -> Bool
$c== :: forall s e.
(Eq s, Eq e) =>
SSubstElem s e -> SSubstElem s e -> Bool
== :: SSubstElem s e -> SSubstElem s e -> Bool
$c/= :: forall s e.
(Eq s, Eq e) =>
SSubstElem s e -> SSubstElem s e -> Bool
/= :: SSubstElem s e -> SSubstElem s e -> Bool
Eq,Eq (SSubstElem s e)
Eq (SSubstElem s e) =>
(SSubstElem s e -> SSubstElem s e -> Ordering)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> SSubstElem s e)
-> (SSubstElem s e -> SSubstElem s e -> SSubstElem s e)
-> Ord (SSubstElem s e)
SSubstElem s e -> SSubstElem s e -> Bool
SSubstElem s e -> SSubstElem s e -> Ordering
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (SSubstElem s e)
forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Ordering
forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
$ccompare :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Ordering
compare :: SSubstElem s e -> SSubstElem s e -> Ordering
$c< :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
< :: SSubstElem s e -> SSubstElem s e -> Bool
$c<= :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
<= :: SSubstElem s e -> SSubstElem s e -> Bool
$c> :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
> :: SSubstElem s e -> SSubstElem s e -> Bool
$c>= :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
>= :: SSubstElem s e -> SSubstElem s e -> Bool
$cmax :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
max :: SSubstElem s e -> SSubstElem s e -> SSubstElem s e
$cmin :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
min :: SSubstElem s e -> SSubstElem s e -> SSubstElem s e
Ord,Int -> SSubstElem s e -> ShowS
[SSubstElem s e] -> ShowS
SSubstElem s e -> String
(Int -> SSubstElem s e -> ShowS)
-> (SSubstElem s e -> String)
-> ([SSubstElem s e] -> ShowS)
-> Show (SSubstElem s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> SSubstElem s e -> ShowS
forall s e. (Show s, Show e) => [SSubstElem s e] -> ShowS
forall s e. (Show s, Show e) => SSubstElem s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> SSubstElem s e -> ShowS
showsPrec :: Int -> SSubstElem s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => SSubstElem s e -> String
show :: SSubstElem s e -> String
$cshowList :: forall s e. (Show s, Show e) => [SSubstElem s e] -> ShowS
showList :: [SSubstElem s e] -> ShowS
Show)

instance (Pretty s,Pretty e) ⇒ Pretty (SSubstElem s e) where
  pretty :: SSubstElem s e -> Doc
pretty = \case
    Var_SSE ℕ64
i → 𝕐 -> Doc
forall a. Pretty a => a -> Doc
pretty (𝕐 -> Doc) -> 𝕐 -> Doc
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕐
DVar ℕ64
i
    Trm_SSE SubstElem s e
e → SubstElem s e -> Doc
forall a. Pretty a => a -> Doc
pretty SubstElem s e
e

instance (Ord s,Fuzzy s,Fuzzy e) ⇒ Fuzzy (SSubstElem s e) where 
  fuzzy :: FuzzyM (SSubstElem s e)
fuzzy = [() -> FuzzyM (SSubstElem s e)] -> FuzzyM (SSubstElem s e)
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose ([() -> FuzzyM (SSubstElem s e)] -> FuzzyM (SSubstElem s e))
-> [() -> FuzzyM (SSubstElem s e)] -> FuzzyM (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ (FuzzyM (SSubstElem s e) -> () -> FuzzyM (SSubstElem s e))
-> [FuzzyM (SSubstElem s e)] -> [() -> FuzzyM (SSubstElem s e)]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map FuzzyM (SSubstElem s e) -> () -> FuzzyM (SSubstElem s e)
forall a b. a -> b -> a
const
    [ ℕ64 -> SSubstElem s e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE (ℕ64 -> SSubstElem s e) -> FuzzyM ℕ64 -> FuzzyM (SSubstElem s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM ℕ64
forall a. Fuzzy a => FuzzyM a
fuzzy
    , SubstElem s e -> SSubstElem s e
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s e -> SSubstElem s e)
-> FuzzyM (SubstElem s e) -> FuzzyM (SSubstElem s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM (SubstElem s e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]

introSSubstElem ∷ (Ord s) ⇒ s → s ⇰ ℕ64 → SSubstElem s e → SSubstElem s e
introSSubstElem :: forall s e.
Ord s =>
s -> (s ⇰ ℕ64) -> SSubstElem s e -> SSubstElem s e
introSSubstElem s
s s ⇰ ℕ64
𝑠 = \case
  Var_SSE ℕ64
n → ℕ64 -> SSubstElem s e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE (ℕ64 -> SSubstElem s e) -> ℕ64 -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64 -> 𝑂 ℕ64 -> ℕ64
forall a. a -> 𝑂 a -> a
ifNone ℕ64
0 (s ⇰ ℕ64
𝑠 (s ⇰ ℕ64) -> s -> 𝑂 ℕ64
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? s
s)
  Trm_SSE SubstElem s e
e → SubstElem s e -> SSubstElem s e
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s e -> SSubstElem s e)
-> SubstElem s e -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e
forall s e. Ord s => (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e
introSubstElem s ⇰ ℕ64
𝑠 SubstElem s e
e

subSSubstElem ∷ (ℕ64 → SSubstElem s e) → (s ⇰ ℕ64 → e → 𝑂 e) → SSubstElem s e → SSubstElem s e
subSSubstElem :: forall s e.
(ℕ64 -> SSubstElem s e)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e
subSSubstElem ℕ64 -> SSubstElem s e
substV (s ⇰ ℕ64) -> e -> 𝑂 e
substE = \case
  Var_SSE ℕ64
n → ℕ64 -> SSubstElem s e
substV ℕ64
n
  Trm_SSE SubstElem s e
ℯ → SubstElem s e -> SSubstElem s e
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s e -> SSubstElem s e)
-> SubstElem s e -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
subSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
ℯ

----------------------------
-- DE BRUIJN SUBSTITUTION --
----------------------------

-- 𝓈 ⩴ ⟨ρ,es,ι⟩ 
-- INVARIANT: |es| + ι ≥ 0
data DSubst s e = DSubst
  { forall s e. DSubst s e -> ℕ64
dsubstShift ∷ ℕ64
  , forall s e. DSubst s e -> 𝕍 (SSubstElem s e)
dsubstElems ∷ 𝕍 (SSubstElem s e)
  , forall s e. DSubst s e -> ℤ64
dsubstIntro ∷ ℤ64
  } deriving (DSubst s e -> DSubst s e -> Bool
(DSubst s e -> DSubst s e -> Bool)
-> (DSubst s e -> DSubst s e -> Bool) -> Eq (DSubst s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e. (Eq s, Eq e) => DSubst s e -> DSubst s e -> Bool
$c== :: forall s e. (Eq s, Eq e) => DSubst s e -> DSubst s e -> Bool
== :: DSubst s e -> DSubst s e -> Bool
$c/= :: forall s e. (Eq s, Eq e) => DSubst s e -> DSubst s e -> Bool
/= :: DSubst s e -> DSubst s e -> Bool
Eq,Eq (DSubst s e)
Eq (DSubst s e) =>
(DSubst s e -> DSubst s e -> Ordering)
-> (DSubst s e -> DSubst s e -> Bool)
-> (DSubst s e -> DSubst s e -> Bool)
-> (DSubst s e -> DSubst s e -> Bool)
-> (DSubst s e -> DSubst s e -> Bool)
-> (DSubst s e -> DSubst s e -> DSubst s e)
-> (DSubst s e -> DSubst s e -> DSubst s e)
-> Ord (DSubst s e)
DSubst s e -> DSubst s e -> Bool
DSubst s e -> DSubst s e -> Ordering
DSubst s e -> DSubst s e -> DSubst s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (DSubst s e)
forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Bool
forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Ordering
forall s e.
(Ord s, Ord e) =>
DSubst s e -> DSubst s e -> DSubst s e
$ccompare :: forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Ordering
compare :: DSubst s e -> DSubst s e -> Ordering
$c< :: forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Bool
< :: DSubst s e -> DSubst s e -> Bool
$c<= :: forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Bool
<= :: DSubst s e -> DSubst s e -> Bool
$c> :: forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Bool
> :: DSubst s e -> DSubst s e -> Bool
$c>= :: forall s e. (Ord s, Ord e) => DSubst s e -> DSubst s e -> Bool
>= :: DSubst s e -> DSubst s e -> Bool
$cmax :: forall s e.
(Ord s, Ord e) =>
DSubst s e -> DSubst s e -> DSubst s e
max :: DSubst s e -> DSubst s e -> DSubst s e
$cmin :: forall s e.
(Ord s, Ord e) =>
DSubst s e -> DSubst s e -> DSubst s e
min :: DSubst s e -> DSubst s e -> DSubst s e
Ord,Int -> DSubst s e -> ShowS
[DSubst s e] -> ShowS
DSubst s e -> String
(Int -> DSubst s e -> ShowS)
-> (DSubst s e -> String)
-> ([DSubst s e] -> ShowS)
-> Show (DSubst s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> DSubst s e -> ShowS
forall s e. (Show s, Show e) => [DSubst s e] -> ShowS
forall s e. (Show s, Show e) => DSubst s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> DSubst s e -> ShowS
showsPrec :: Int -> DSubst s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => DSubst s e -> String
show :: DSubst s e -> String
$cshowList :: forall s e. (Show s, Show e) => [DSubst s e] -> ShowS
showList :: [DSubst s e] -> ShowS
Show)
makeLenses ''DSubst
makePrettyRecord ''DSubst

instance (Ord s,Fuzzy s,Fuzzy e) ⇒ Fuzzy (DSubst s e) where 
  fuzzy :: FuzzyM (DSubst s e)
fuzzy = do
    ℕ64
ρ ← FuzzyM ℕ64
forall a. Fuzzy a => FuzzyM a
fuzzy
    ℕ64
𝔰 ← FuzzyM ℕ64
forall a. Fuzzy a => FuzzyM a
fuzzy
    𝕍 (SSubstElem s e)
es ← 𝕍 ℕ64
-> (ℕ64 -> FuzzyM (SSubstElem s e)) -> FuzzyM (𝕍 (SSubstElem s e))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn (ℕ64 -> (ℕ64 -> ℕ64) -> 𝕍 ℕ64
forall a. ℕ64 -> (ℕ64 -> a) -> 𝕍 a
vecF ℕ64
𝔰 ℕ64 -> ℕ64
forall a. a -> a
id) ((ℕ64 -> FuzzyM (SSubstElem s e)) -> FuzzyM (𝕍 (SSubstElem s e)))
-> (ℕ64 -> FuzzyM (SSubstElem s e)) -> FuzzyM (𝕍 (SSubstElem s e))
forall a b. (a -> b) -> a -> b
$ FuzzyM (SSubstElem s e) -> ℕ64 -> FuzzyM (SSubstElem s e)
forall a b. a -> b -> a
const (FuzzyM (SSubstElem s e) -> ℕ64 -> FuzzyM (SSubstElem s e))
-> FuzzyM (SSubstElem s e) -> ℕ64 -> FuzzyM (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ FuzzyM (SSubstElem s e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    ℤ64
ι ← ℤ64 -> ℤ64 -> FuzzyM ℤ64
forall a (m :: * -> *). (MonadRand m, RandRange a) => a -> a -> m a
randr (ℤ64 -> ℤ64
forall a. (Zero a, Minus a) => a -> a
neg (ℤ64 -> ℤ64) -> ℤ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
𝔰) (ℤ64 -> FuzzyM ℤ64) -> ℤ64 -> FuzzyM ℤ64
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
𝔰
    DSubst s e -> FuzzyM (DSubst s e)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (DSubst s e -> FuzzyM (DSubst s e))
-> DSubst s e -> FuzzyM (DSubst s e)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
DSubst ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι

isNullDSubst ∷ DSubst s e → 𝔹
isNullDSubst :: forall s e. DSubst s e -> Bool
isNullDSubst (DSubst ℕ64
_ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = 𝕍 (SSubstElem s e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s e)
es ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 Bool -> Bool -> Bool
⩓ ℤ64
ι ℤ64 -> ℤ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℤ64
0

-- 𝓈 ≜ ⟨ρ,es,ι⟩
-- 𝔰 ≜ |es|
-- 𝓈(i) ≜
--   cases (disjoint):
--     |       i < ρ   ⇒ i
--     |   ρ ≤ i < ρ+𝔰 ⇒ es[i-ρ]
--     | ρ+𝔰 ≤ i       ⇒ i+ι
-- 𝓈(i) ≜
--   cases (sequential):
--     | i < ρ   ⇒ i
--     | i < ρ+𝔰 ⇒ es[i-ρ]
--     | ⊤       ⇒ i+ι
-- e.g.,
-- 𝓈 = ⟨2,[e],-1⟩
-- 𝓈 is logically equivalent to the (infinite) substitution vector
-- [ …
-- ,  0 ↦ ⌊ 0⌋    | ≡
-- ,  1 ↦ ⌊ 1⌋    |
-- ----------------
-- ,  2 ↦   e     | [e]
-- ----------------
-- ,  3 ↦ ⌊ 2⌋    | -1
-- ,  4 ↦ ⌊ 3⌋    |
-- , …
-- ]
dsubstVar ∷ DSubst 𝑠 e → ℕ64 → SSubstElem 𝑠 e
dsubstVar :: forall 𝑠 e. DSubst 𝑠 e -> ℕ64 -> SSubstElem 𝑠 e
dsubstVar (DSubst ℕ64
ρ̇ 𝕍 (SSubstElem 𝑠 e)
es ℤ64
ι) ℕ64
ṅ =
  let 𝔰̇ :: ℕ64
𝔰̇  = 𝕍 (SSubstElem 𝑠 e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem 𝑠 e)
es
      n :: ℤ64
n  = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
ṅ
  in 
  if
  | ℕ64
ṅ ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℕ64
ρ̇     → ℕ64 -> SSubstElem 𝑠 e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE ℕ64
ṅ
  | ℕ64
ṅ ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℕ64
𝔰̇ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ℕ64
ρ̇   → 𝕍 (SSubstElem 𝑠 e)
es 𝕍 (SSubstElem 𝑠 e) -> ℕ64 -> SSubstElem 𝑠 e
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! (ℕ64
ṅℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
-ℕ64
ρ̇)
  | Bool
otherwise → ℕ64 -> SSubstElem 𝑠 e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE (ℕ64 -> SSubstElem 𝑠 e) -> ℕ64 -> SSubstElem 𝑠 e
forall a b. (a -> b) -> a -> b
$ ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64 -> ℕ64) -> ℤ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ ℤ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
ι

-------------------------------
-- GENERIC SCOPED SUBSTITUTION --
-------------------------------

data GSubst s₁ s₂ e = GSubst 
  { forall s₁ s₂ e. GSubst s₁ s₂ e -> s₁ ⇰ SubstElem s₂ e
gsubstGVars ∷ s₁ ⇰ SubstElem s₂ e
  , forall s₁ s₂ e. GSubst s₁ s₂ e -> s₁ ⇰ SubstElem s₂ e
gsubstMetas ∷ s₁ ⇰ SubstElem s₂ e
  , forall s₁ s₂ e. GSubst s₁ s₂ e -> s₂ ⇰ DSubst s₂ e
gsubstSubst ∷ s₂ ⇰ DSubst s₂ e 
  } 
  deriving (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
(GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool)
-> Eq (GSubst s₁ s₂ e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s₁ s₂ e.
(Eq s₁, Eq s₂, Eq e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
$c== :: forall s₁ s₂ e.
(Eq s₁, Eq s₂, Eq e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
== :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
$c/= :: forall s₁ s₂ e.
(Eq s₁, Eq s₂, Eq e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
/= :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
Eq,Eq (GSubst s₁ s₂ e)
Eq (GSubst s₁ s₂ e) =>
(GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Ordering)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e)
-> (GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e)
-> Ord (GSubst s₁ s₂ e)
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Ordering
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s₁ s₂ e. (Ord s₁, Ord s₂, Ord e) => Eq (GSubst s₁ s₂ e)
forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Ordering
forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
$ccompare :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Ordering
compare :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Ordering
$c< :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
< :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
$c<= :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
<= :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
$c> :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
> :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
$c>= :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
>= :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool
$cmax :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
max :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
$cmin :: forall s₁ s₂ e.
(Ord s₁, Ord s₂, Ord e) =>
GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
min :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
Ord,Int -> GSubst s₁ s₂ e -> ShowS
[GSubst s₁ s₂ e] -> ShowS
GSubst s₁ s₂ e -> String
(Int -> GSubst s₁ s₂ e -> ShowS)
-> (GSubst s₁ s₂ e -> String)
-> ([GSubst s₁ s₂ e] -> ShowS)
-> Show (GSubst s₁ s₂ e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s₁ s₂ e.
(Show s₁, Show s₂, Show e) =>
Int -> GSubst s₁ s₂ e -> ShowS
forall s₁ s₂ e.
(Show s₁, Show s₂, Show e) =>
[GSubst s₁ s₂ e] -> ShowS
forall s₁ s₂ e.
(Show s₁, Show s₂, Show e) =>
GSubst s₁ s₂ e -> String
$cshowsPrec :: forall s₁ s₂ e.
(Show s₁, Show s₂, Show e) =>
Int -> GSubst s₁ s₂ e -> ShowS
showsPrec :: Int -> GSubst s₁ s₂ e -> ShowS
$cshow :: forall s₁ s₂ e.
(Show s₁, Show s₂, Show e) =>
GSubst s₁ s₂ e -> String
show :: GSubst s₁ s₂ e -> String
$cshowList :: forall s₁ s₂ e.
(Show s₁, Show s₂, Show e) =>
[GSubst s₁ s₂ e] -> ShowS
showList :: [GSubst s₁ s₂ e] -> ShowS
Show)
makeLenses ''GSubst
makePrettyUnion ''GSubst

instance (Ord s₁,Ord s₂,Fuzzy s₁,Fuzzy s₂,Fuzzy e) ⇒ Fuzzy (GSubst s₁ s₂ e) where 
  fuzzy :: FuzzyM (GSubst s₁ s₂ e)
fuzzy = do
    s₁ ⇰ SubstElem s₂ e
esᴳ ← FuzzyM (s₁ ⇰ SubstElem s₂ e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    s₁ ⇰ SubstElem s₂ e
esᴹ ← FuzzyM (s₁ ⇰ SubstElem s₂ e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    s₂ ⇰ DSubst s₂ e
𝓈 ← FuzzyM (s₂ ⇰ DSubst s₂ e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    GSubst s₁ s₂ e -> FuzzyM (GSubst s₁ s₂ e)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (GSubst s₁ s₂ e -> FuzzyM (GSubst s₁ s₂ e))
-> GSubst s₁ s₂ e -> FuzzyM (GSubst s₁ s₂ e)
forall a b. (a -> b) -> a -> b
$ (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst s₁ ⇰ SubstElem s₂ e
esᴳ s₁ ⇰ SubstElem s₂ e
esᴹ s₂ ⇰ DSubst s₂ e
𝓈

𝓈shiftG ∷ (Ord s₂) ⇒ s₂ ⇰ ℕ64 → GSubst s₁ s₂ e → GSubst s₁ s₂ e
𝓈shiftG :: forall s₂ s₁ e.
Ord s₂ =>
(s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
𝓈shiftG s₂ ⇰ ℕ64
𝑠 (GSubst s₁ ⇰ SubstElem s₂ e
esᴳ s₁ ⇰ SubstElem s₂ e
esᴹ s₂ ⇰ DSubst s₂ e
𝓈s) = 
  let esᴳ' :: s₁ ⇰ SubstElem s₂ e
esᴳ' = (SubstElem s₂ e -> SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> s₁ ⇰ SubstElem s₂ e
forall a b. (a -> b) -> (s₁ ⇰ a) -> s₁ ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s₂ ⇰ ℕ64) -> SubstElem s₂ e -> SubstElem s₂ e
forall s e. Ord s => (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e
introSubstElem s₂ ⇰ ℕ64
𝑠) s₁ ⇰ SubstElem s₂ e
esᴳ
      𝓈s' :: s₂ ⇰ DSubst s₂ e
𝓈s' = (s₂ ⇰ DSubst s₂ e)
-> (s₂ -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn s₂ ⇰ DSubst s₂ e
𝓈s ((s₂ -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e)
-> (s₂ -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall a b. (a -> b) -> a -> b
$ \ s₂
s (DSubst ℕ64
ρ 𝕍 (SSubstElem s₂ e)
es ℤ64
ι) →
        let ρ' :: ℕ64
ρ'  = ℕ64
ρ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64 -> 𝑂 ℕ64 -> ℕ64
forall a. a -> 𝑂 a -> a
ifNone ℕ64
0 (s₂ ⇰ ℕ64
𝑠 (s₂ ⇰ ℕ64) -> s₂ -> 𝑂 ℕ64
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? s₂
s)
            es' :: 𝕍 (SSubstElem s₂ e)
es' = 𝕍 (SSubstElem s₂ e)
-> (SSubstElem s₂ e -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 (SSubstElem s₂ e)
es ((SSubstElem s₂ e -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e))
-> (SSubstElem s₂ e -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e)
forall a b. (a -> b) -> a -> b
$ s₂ -> (s₂ ⇰ ℕ64) -> SSubstElem s₂ e -> SSubstElem s₂ e
forall s e.
Ord s =>
s -> (s ⇰ ℕ64) -> SSubstElem s e -> SSubstElem s e
introSSubstElem s₂
s s₂ ⇰ ℕ64
𝑠
        in ℕ64 -> 𝕍 (SSubstElem s₂ e) -> ℤ64 -> DSubst s₂ e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
DSubst ℕ64
ρ' 𝕍 (SSubstElem s₂ e)
es' ℤ64
ι
  in (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst s₁ ⇰ SubstElem s₂ e
esᴳ' s₁ ⇰ SubstElem s₂ e
esᴹ s₂ ⇰ DSubst s₂ e
𝓈s'

𝓈introG ∷ s₂ ⇰ ℕ64 → GSubst s₁ s₂ e
𝓈introG :: forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG s₂ ⇰ ℕ64
𝑠 = (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst s₁ ⇰ SubstElem s₂ e
forall a. Null a => a
null s₁ ⇰ SubstElem s₂ e
forall a. Null a => a
null ((s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e)
-> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall a b. (a -> b) -> a -> b
$ (s₂ ⇰ ℕ64) -> (ℕ64 -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn s₂ ⇰ ℕ64
𝑠 ((ℕ64 -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e)
-> (ℕ64 -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕍 (SSubstElem s₂ e) -> ℤ64 -> DSubst s₂ e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
DSubst ℕ64
0 𝕍 (SSubstElem s₂ e)
forall a. Null a => a
null (ℤ64 -> DSubst s₂ e) -> (ℕ64 -> ℤ64) -> ℕ64 -> DSubst s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64

𝓈sbindsG ∷ s₂ ⇰ 𝕍 e → GSubst s₁ s₂ e
𝓈sbindsG :: forall s₂ e s₁. (s₂ ⇰ 𝕍 e) -> GSubst s₁ s₂ e
𝓈sbindsG s₂ ⇰ 𝕍 e
ess = (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst s₁ ⇰ SubstElem s₂ e
forall a. Null a => a
null s₁ ⇰ SubstElem s₂ e
forall a. Null a => a
null ((s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e)
-> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall a b. (a -> b) -> a -> b
$ (s₂ ⇰ 𝕍 e) -> (𝕍 e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn s₂ ⇰ 𝕍 e
ess ((𝕍 e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e)
-> (𝕍 e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall a b. (a -> b) -> a -> b
$ \ 𝕍 e
es →
  let ℯs :: 𝕍 (SSubstElem s₂ e)
ℯs = (e -> SSubstElem s₂ e) -> 𝕍 e -> 𝕍 (SSubstElem s₂ e)
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (SubstElem s₂ e -> SSubstElem s₂ e
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s₂ e -> SSubstElem s₂ e)
-> ((() -> 𝑂 e) -> SubstElem s₂ e)
-> (() -> 𝑂 e)
-> SSubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s₂ ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s₂ e
forall s e. (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
SubstElem s₂ ⇰ ℕ64
forall a. Null a => a
null ((() -> 𝑂 e) -> SSubstElem s₂ e)
-> (𝑂 e -> () -> 𝑂 e) -> 𝑂 e -> SSubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑂 e -> () -> 𝑂 e
forall a b. a -> b -> a
const (𝑂 e -> SSubstElem s₂ e) -> (e -> 𝑂 e) -> e -> SSubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> 𝑂 e
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return) 𝕍 e
es
      ι :: ℤ64
ι  = ℤ64 -> ℤ64
forall a. (Zero a, Minus a) => a -> a
neg (ℤ64 -> ℤ64) -> ℤ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕍 e -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 e
es
  in ℕ64 -> 𝕍 (SSubstElem s₂ e) -> ℤ64 -> DSubst s₂ e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
DSubst ℕ64
forall a. Zero a => a
zero 𝕍 (SSubstElem s₂ e)
ℯs ℤ64
ι

𝓈sgbindsG ∷ s₁ ⇰ e → GSubst s₁ s₂ e
𝓈sgbindsG :: forall s₁ e s₂. (s₁ ⇰ e) -> GSubst s₁ s₂ e
𝓈sgbindsG s₁ ⇰ e
esᴳ = (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst ((e -> SubstElem s₂ e) -> (s₁ ⇰ e) -> s₁ ⇰ SubstElem s₂ e
forall a b. (a -> b) -> (s₁ ⇰ a) -> s₁ ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s₂ ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s₂ e
forall s e. (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
SubstElem s₂ ⇰ ℕ64
forall a. Null a => a
null ((() -> 𝑂 e) -> SubstElem s₂ e)
-> (𝑂 e -> () -> 𝑂 e) -> 𝑂 e -> SubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑂 e -> () -> 𝑂 e
forall a b. a -> b -> a
const (𝑂 e -> SubstElem s₂ e) -> (e -> 𝑂 e) -> e -> SubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> 𝑂 e
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return) s₁ ⇰ e
esᴳ) s₁ ⇰ SubstElem s₂ e
forall a. Null a => a
null s₂ ⇰ DSubst s₂ e
forall a. Null a => a
null

𝓈smbindsG ∷ s₁ ⇰ e → GSubst s₁ s₂ e
𝓈smbindsG :: forall s₁ e s₂. (s₁ ⇰ e) -> GSubst s₁ s₂ e
𝓈smbindsG s₁ ⇰ e
esᴳ = (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst s₁ ⇰ SubstElem s₂ e
forall a. Null a => a
null ((e -> SubstElem s₂ e) -> (s₁ ⇰ e) -> s₁ ⇰ SubstElem s₂ e
forall a b. (a -> b) -> (s₁ ⇰ a) -> s₁ ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s₂ ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s₂ e
forall s e. (s ⇰ ℕ64) -> (() -> 𝑂 e) -> SubstElem s e
SubstElem s₂ ⇰ ℕ64
forall a. Null a => a
null ((() -> 𝑂 e) -> SubstElem s₂ e)
-> (𝑂 e -> () -> 𝑂 e) -> 𝑂 e -> SubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑂 e -> () -> 𝑂 e
forall a b. a -> b -> a
const (𝑂 e -> SubstElem s₂ e) -> (e -> 𝑂 e) -> e -> SubstElem s₂ e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> 𝑂 e
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return) s₁ ⇰ e
esᴳ) s₂ ⇰ DSubst s₂ e
forall a. Null a => a
null

-- 𝓈₁ ≜ ⟨ρ₁,es₁,ι₁⟩
-- 𝓈₂ ≜ ⟨ρ₂,es₂,ι₂⟩
-- 𝔰₁ = |es₁| 
-- 𝔰₂ = |es₂| 
-- (𝓈₂⧺𝓈₁)(i) 
-- ==
-- 𝓈₂(𝓈₁(i))
-- ==
-- cases (sequential):
--   | i < ρ₁    ⇒ 𝓈₂(i)
--   | i < ρ₁+𝔰₁ ⇒ 𝓈₂(es₁[i-ρ₁])
--   | ⊤         ⇒ 𝓈₂(i+ι₁)
-- ==
-- cases (sequential):
--   | i < ρ₁    ⇒ cases (sequential):
--                    | i < ρ₂    ⇒ i
--                    | i < ρ₂+𝔰₂ ⇒ es₂[i-ρ₂]
--                    | ⊤         ⇒ i+ι₂
--   | i < ρ₁+𝔰₁ ⇒ 𝓈₂(es₁[i-ρ₁])
--   | ⊤         ⇒ cases (sequential):
--                    | i < ρ₂-ι₁    ⇒ i+ι₁
--                    | i < ρ₂+𝔰₂-ι₁ ⇒ es₂[i+ι₁-ρ₂]
--                    | ⊤            ⇒ i+ι₁+ι₂
-- ==
-- cases (sequential):
--   | i < ρ₁⊓ρ₂      ⇒ i
--   ---------------------------------
--   | i < ρ₁⊓(ρ₂+𝔰₂) ⇒ es₂[i-ρ₂]
--   | i < ρ₁         ⇒ i+ι₂
--   | i < ρ₁+𝔰₁      ⇒ 𝓈₂(es₁[i-ρ₁])
--   | i < ρ₂-ι₁      ⇒ i+ι₁
--   | i < ρ₂+𝔰₂-ι₁   ⇒ es₂[i+ι₁-ρ₂]
--   ---------------------------------
--   | ⊤              ⇒ i+ι₁+ι₂
-- == ⟨ρ,es,ι⟩(i)
-- where
--     ρ = ρ₁⊓ρ₂
--     ι = ι₁+ι₂
--     𝔰 ≜ |es|
--   ρ+𝔰 = (ρ₁+𝔰₁)⊔(ρ₂+𝔰₂-ι₁)
--     𝔰 = ((ρ₁+𝔰₁)⊔(ρ₂+𝔰₂-ι₁))-ρ
appendGSubst ∷ 
  (Ord s₁,Ord s₂) 
  ⇒ (GSubst s₁ s₂ e → e → 𝑂 e) 
  → GSubst s₁ s₂ e 
  → GSubst s₁ s₂ e 
  → GSubst s₁ s₂ e
appendGSubst :: forall s₁ s₂ e.
(Ord s₁, Ord s₂) =>
(GSubst s₁ s₂ e -> e -> 𝑂 e)
-> GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
appendGSubst GSubst s₁ s₂ e -> e -> 𝑂 e
esubst GSubst s₁ s₂ e
𝓈̂₂ GSubst s₁ s₂ e
𝓈̂₁ =
  let GSubst s₁ ⇰ SubstElem s₂ e
esᴳ₁ s₁ ⇰ SubstElem s₂ e
esᴹ₁ s₂ ⇰ DSubst s₂ e
𝓈s₁ = GSubst s₁ s₂ e
𝓈̂₁
      GSubst s₁ ⇰ SubstElem s₂ e
esᴳ₂ s₁ ⇰ SubstElem s₂ e
esᴹ₂ s₂ ⇰ DSubst s₂ e
𝓈s₂ = GSubst s₁ s₂ e
𝓈̂₂
      esub :: GSubst s₁ s₂ e -> (s₂ ⇰ ℕ64) -> e -> 𝑂 e
esub GSubst s₁ s₂ e
𝓈 s₂ ⇰ ℕ64
𝑠 = GSubst s₁ s₂ e -> e -> 𝑂 e
esubst (GSubst s₁ s₂ e -> e -> 𝑂 e) -> GSubst s₁ s₂ e -> e -> 𝑂 e
forall a b. (a -> b) -> a -> b
$ (GSubst s₁ s₂ e -> e -> 𝑂 e)
-> GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(Ord s₁, Ord s₂) =>
(GSubst s₁ s₂ e -> e -> 𝑂 e)
-> GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
appendGSubst GSubst s₁ s₂ e -> e -> 𝑂 e
esubst GSubst s₁ s₂ e
𝓈 (GSubst s₁ s₂ e -> GSubst s₁ s₂ e)
-> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
forall a b. (a -> b) -> a -> b
$ (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG s₂ ⇰ ℕ64
𝑠
      ℯsub :: s₂ -> GSubst s₁ s₂ e -> SSubstElem s₂ e -> SSubstElem s₂ e
ℯsub s₂
s GSubst s₁ s₂ e
𝓈 = (ℕ64 -> SSubstElem s₂ e)
-> ((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s₂ e -> SSubstElem s₂ e
forall s e.
(ℕ64 -> SSubstElem s e)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e
subSSubstElem ((() -> ℕ64 -> SSubstElem s₂ e)
-> (DSubst s₂ e -> ℕ64 -> SSubstElem s₂ e)
-> 𝑂 (DSubst s₂ e)
-> ℕ64
-> SSubstElem s₂ e
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 ((ℕ64 -> SSubstElem s₂ e) -> () -> ℕ64 -> SSubstElem s₂ e
forall a b. a -> b -> a
const ℕ64 -> SSubstElem s₂ e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE) DSubst s₂ e -> ℕ64 -> SSubstElem s₂ e
forall 𝑠 e. DSubst 𝑠 e -> ℕ64 -> SSubstElem 𝑠 e
dsubstVar (𝑂 (DSubst s₂ e) -> ℕ64 -> SSubstElem s₂ e)
-> 𝑂 (DSubst s₂ e) -> ℕ64 -> SSubstElem s₂ e
forall a b. (a -> b) -> a -> b
$ GSubst s₁ s₂ e -> s₂ ⇰ DSubst s₂ e
forall s₁ s₂ e. GSubst s₁ s₂ e -> s₂ ⇰ DSubst s₂ e
gsubstSubst GSubst s₁ s₂ e
𝓈 (s₂ ⇰ DSubst s₂ e) -> s₂ -> 𝑂 (DSubst s₂ e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? s₂
s) (((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s₂ e -> SSubstElem s₂ e)
-> ((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s₂ e -> SSubstElem s₂ e
forall a b. (a -> b) -> a -> b
$ GSubst s₁ s₂ e -> (s₂ ⇰ ℕ64) -> e -> 𝑂 e
esub GSubst s₁ s₂ e
𝓈
      esᴳ₁' :: s₁ ⇰ SubstElem s₂ e
esᴳ₁' = (SubstElem s₂ e -> SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> s₁ ⇰ SubstElem s₂ e
forall a b. (a -> b) -> (s₁ ⇰ a) -> s₁ ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s₂ e -> SubstElem s₂ e
forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
subSubstElem (((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s₂ e -> SubstElem s₂ e)
-> ((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s₂ e -> SubstElem s₂ e
forall a b. (a -> b) -> a -> b
$ GSubst s₁ s₂ e -> (s₂ ⇰ ℕ64) -> e -> 𝑂 e
esub GSubst s₁ s₂ e
𝓈̂₂) s₁ ⇰ SubstElem s₂ e
esᴳ₁
      esᴹ₁' :: s₁ ⇰ SubstElem s₂ e
esᴹ₁' = (SubstElem s₂ e -> SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> s₁ ⇰ SubstElem s₂ e
forall a b. (a -> b) -> (s₁ ⇰ a) -> s₁ ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s₂ e -> SubstElem s₂ e
forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
subSubstElem (((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s₂ e -> SubstElem s₂ e)
-> ((s₂ ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s₂ e -> SubstElem s₂ e
forall a b. (a -> b) -> a -> b
$ GSubst s₁ s₂ e -> (s₂ ⇰ ℕ64) -> e -> 𝑂 e
esub GSubst s₁ s₂ e
𝓈̂₂) s₁ ⇰ SubstElem s₂ e
esᴹ₁
      𝓈s₁' :: s₂ ⇰ DSubst s₂ e
𝓈s₁' = (s₂ ⇰ DSubst s₂ e)
-> (s₂ -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn s₂ ⇰ DSubst s₂ e
𝓈s₁ ((s₂ -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e)
-> (s₂ -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall a b. (a -> b) -> a -> b
$ \ s₂
s (DSubst ℕ64
ρ̇₁ 𝕍 (SSubstElem s₂ e)
es₁ ℤ64
ι₁) → ℕ64 -> 𝕍 (SSubstElem s₂ e) -> ℤ64 -> DSubst s₂ e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
DSubst ℕ64
ρ̇₁ (𝕍 (SSubstElem s₂ e)
-> (SSubstElem s₂ e -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 (SSubstElem s₂ e)
es₁ ((SSubstElem s₂ e -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e))
-> (SSubstElem s₂ e -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e)
forall a b. (a -> b) -> a -> b
$ s₂ -> GSubst s₁ s₂ e -> SSubstElem s₂ e -> SSubstElem s₂ e
ℯsub s₂
s GSubst s₁ s₂ e
𝓈̂₂) ℤ64
ι₁
      esᴳ :: s₁ ⇰ SubstElem s₂ e
esᴳ = s₁ ⇰ SubstElem s₂ e
esᴳ₁' (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> s₁ ⇰ SubstElem s₂ e
forall a. (s₁ ⇰ a) -> (s₁ ⇰ a) -> s₁ ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a -> d a -> d a
⩌ s₁ ⇰ SubstElem s₂ e
esᴳ₂ 
      esᴹ :: s₁ ⇰ SubstElem s₂ e
esᴹ = s₁ ⇰ SubstElem s₂ e
esᴹ₁' (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> s₁ ⇰ SubstElem s₂ e
forall a. (s₁ ⇰ a) -> (s₁ ⇰ a) -> s₁ ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a -> d a -> d a
⩌ s₁ ⇰ SubstElem s₂ e
esᴹ₂ 
      𝓈s :: s₂ ⇰ DSubst s₂ e
𝓈s = (s₂ ⇰ DSubst s₂ e)
-> (s₂ ⇰ DSubst s₂ e)
-> (DSubst s₂ e -> DSubst s₂ e -> DSubst s₂ e)
-> s₂ ⇰ DSubst s₂ e
forall k s (d :: * -> *) a.
Dict k s d =>
d a -> d a -> (a -> a -> a) -> d a
dunionByOn s₂ ⇰ DSubst s₂ e
𝓈s₂ s₂ ⇰ DSubst s₂ e
𝓈s₁' ((DSubst s₂ e -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e)
-> (DSubst s₂ e -> DSubst s₂ e -> DSubst s₂ e) -> s₂ ⇰ DSubst s₂ e
forall a b. (a -> b) -> a -> b
$ \ 𝓈₂ :: DSubst s₂ e
𝓈₂@(DSubst ℕ64
ρ̇₂ 𝕍 (SSubstElem s₂ e)
es₂ ℤ64
ι₂) 𝓈₁ :: DSubst s₂ e
𝓈₁@(DSubst ℕ64
ρ̇₁ 𝕍 (SSubstElem s₂ e)
es₁ ℤ64
ι₁) →
        if
        | DSubst s₂ e -> Bool
forall s e. DSubst s e -> Bool
isNullDSubst DSubst s₂ e
𝓈₁ → DSubst s₂ e
𝓈₂
        | DSubst s₂ e -> Bool
forall s e. DSubst s e -> Bool
isNullDSubst DSubst s₂ e
𝓈₂ → DSubst s₂ e
𝓈₁
        | Bool
otherwise →
            let 𝔰₁ :: ℤ64
𝔰₁ = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕍 (SSubstElem s₂ e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s₂ e)
es₁
                𝔰₂ :: ℤ64
𝔰₂ = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕍 (SSubstElem s₂ e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s₂ e)
es₂
                ρ₁ :: ℤ64
ρ₁ = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
ρ̇₁
                ρ₂ :: ℤ64
ρ₂ = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
ρ̇₂
                ρ̇ :: ℕ64
ρ̇  = ℕ64
ρ̇₁ℕ64 -> ℕ64 -> ℕ64
forall a. Meet a => a -> a -> a
⊓ℕ64
ρ̇₂
                ρ :: ℤ64
ρ  = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
ρ̇
                ι :: ℤ64
ι  = ℤ64
ι₁ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
ι₂
                𝔰 :: ℤ64
𝔰  = ((ℤ64
ρ₁ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
𝔰₁)ℤ64 -> ℤ64 -> ℤ64
forall a. Join a => a -> a -> a
⊔(ℤ64
ρ₂ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
𝔰₂ℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ι₁))ℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ρ
                δ :: ℤ64
δ  = ℤ64
ρ
                es :: 𝕍 (SSubstElem s₂ e)
es = ℕ64 -> (ℕ64 -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e)
forall a. ℕ64 -> (ℕ64 -> a) -> 𝕍 a
vecF (ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 ℤ64
𝔰) ((ℕ64 -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e))
-> (ℕ64 -> SSubstElem s₂ e) -> 𝕍 (SSubstElem s₂ e)
forall a b. (a -> b) -> a -> b
$ \ ℕ64
ṅ → 
                  let n :: ℤ64
n = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
ṅ ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ ℤ64
δ in 
                  if
                  | ℤ64
n ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℤ64
ρ₁ℤ64 -> ℤ64 -> ℤ64
forall a. Meet a => a -> a -> a
⊓(ℤ64
ρ₂ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
𝔰₂) → 𝕍 (SSubstElem s₂ e)
es₂ 𝕍 (SSubstElem s₂ e) -> ℕ64 -> SSubstElem s₂ e
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ρ₂)
                  | ℤ64
n ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℤ64
ρ₁         → ℕ64 -> SSubstElem s₂ e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE (ℕ64 -> SSubstElem s₂ e) -> ℕ64 -> SSubstElem s₂ e
forall a b. (a -> b) -> a -> b
$ ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64 -> ℕ64) -> ℤ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ ℤ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
ι₂
                  | ℤ64
n ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℤ64
ρ₁ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
𝔰₁      → 𝕍 (SSubstElem s₂ e)
es₁ 𝕍 (SSubstElem s₂ e) -> ℕ64 -> SSubstElem s₂ e
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ρ₁)
                  | ℤ64
n ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℤ64
ρ₂ℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ι₁      → ℕ64 -> SSubstElem s₂ e
forall s e. ℕ64 -> SSubstElem s e
Var_SSE (ℕ64 -> SSubstElem s₂ e) -> ℕ64 -> SSubstElem s₂ e
forall a b. (a -> b) -> a -> b
$ ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64 -> ℕ64) -> ℤ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ ℤ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
ι₁
                  | ℤ64
n ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℤ64
ρ₂ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
𝔰₂ℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ι₁   → 𝕍 (SSubstElem s₂ e)
es₂ 𝕍 (SSubstElem s₂ e) -> ℕ64 -> SSubstElem s₂ e
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
ι₁ℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
ρ₂)
                  | Bool
otherwise      → 𝕊 -> SSubstElem s₂ e
forall a. STACK => 𝕊 -> a
error 𝕊
"bad"
            in
            ℕ64 -> 𝕍 (SSubstElem s₂ e) -> ℤ64 -> DSubst s₂ e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> DSubst s e
DSubst ℕ64
ρ̇ 𝕍 (SSubstElem s₂ e)
es ℤ64
ι
  in (s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst s₁ ⇰ SubstElem s₂ e
esᴳ s₁ ⇰ SubstElem s₂ e
esᴹ s₂ ⇰ DSubst s₂ e
𝓈s

-------------------------------------------
-- SUBSTY (STANDARD SCOPED SUBSTITUTION) --
-------------------------------------------

newtype Subst s e = Subst { forall s e. Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubst ∷ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e }
  deriving (Subst s e -> Subst s e -> Bool
(Subst s e -> Subst s e -> Bool)
-> (Subst s e -> Subst s e -> Bool) -> Eq (Subst s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e. (Eq s, Eq e) => Subst s e -> Subst s e -> Bool
$c== :: forall s e. (Eq s, Eq e) => Subst s e -> Subst s e -> Bool
== :: Subst s e -> Subst s e -> Bool
$c/= :: forall s e. (Eq s, Eq e) => Subst s e -> Subst s e -> Bool
/= :: Subst s e -> Subst s e -> Bool
Eq,Eq (Subst s e)
Eq (Subst s e) =>
(Subst s e -> Subst s e -> Ordering)
-> (Subst s e -> Subst s e -> Bool)
-> (Subst s e -> Subst s e -> Bool)
-> (Subst s e -> Subst s e -> Bool)
-> (Subst s e -> Subst s e -> Bool)
-> (Subst s e -> Subst s e -> Subst s e)
-> (Subst s e -> Subst s e -> Subst s e)
-> Ord (Subst s e)
Subst s e -> Subst s e -> Bool
Subst s e -> Subst s e -> Ordering
Subst s e -> Subst s e -> Subst s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (Subst s e)
forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Bool
forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Ordering
forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Subst s e
$ccompare :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Ordering
compare :: Subst s e -> Subst s e -> Ordering
$c< :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Bool
< :: Subst s e -> Subst s e -> Bool
$c<= :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Bool
<= :: Subst s e -> Subst s e -> Bool
$c> :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Bool
> :: Subst s e -> Subst s e -> Bool
$c>= :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Bool
>= :: Subst s e -> Subst s e -> Bool
$cmax :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Subst s e
max :: Subst s e -> Subst s e -> Subst s e
$cmin :: forall s e. (Ord s, Ord e) => Subst s e -> Subst s e -> Subst s e
min :: Subst s e -> Subst s e -> Subst s e
Ord,Int -> Subst s e -> ShowS
[Subst s e] -> ShowS
Subst s e -> String
(Int -> Subst s e -> ShowS)
-> (Subst s e -> String)
-> ([Subst s e] -> ShowS)
-> Show (Subst s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> Subst s e -> ShowS
forall s e. (Show s, Show e) => [Subst s e] -> ShowS
forall s e. (Show s, Show e) => Subst s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> Subst s e -> ShowS
showsPrec :: Int -> Subst s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => Subst s e -> String
show :: Subst s e -> String
$cshowList :: forall s e. (Show s, Show e) => [Subst s e] -> ShowS
showList :: [Subst s e] -> ShowS
Show,Subst s e -> Doc
(Subst s e -> Doc) -> Pretty (Subst s e)
forall a. (a -> Doc) -> Pretty a
forall s e. (Pretty s, Pretty e) => Subst s e -> Doc
$cpretty :: forall s e. (Pretty s, Pretty e) => Subst s e -> Doc
pretty :: Subst s e -> Doc
Pretty,FuzzyM (Subst s e)
FuzzyM (Subst s e) -> Fuzzy (Subst s e)
forall a. FuzzyM a -> Fuzzy a
forall s e. (Ord s, Fuzzy s, Fuzzy e) => FuzzyM (Subst s e)
$cfuzzy :: forall s e. (Ord s, Fuzzy s, Fuzzy e) => FuzzyM (Subst s e)
fuzzy :: FuzzyM (Subst s e)
Fuzzy)
makeLenses ''Subst

data FreeVarsAction s = FreeVarsAction
  { forall s. FreeVarsAction s -> s -> 𝕐 -> Bool
freeVarsActionFilter ∷ s → 𝕐 → 𝔹
  , forall s. FreeVarsAction s -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
freeVarsActionScope  ∷ (s ∧ 𝑂 𝕏) ⇰ ℕ64
  }
makeLenses ''FreeVarsAction

data SubstAction s e = SubstAction
  { forall s e. SubstAction s e -> 𝑂 Bool
substActionReBdr ∷ 𝑂 𝔹
  , forall s e. SubstAction s e -> Subst s e
substActionSubst ∷ Subst s e
  }
makeLenses ''SubstAction

data SubstEnv s e = 
    FVsSubstEnv (FreeVarsAction s)
  | SubSubstEnv (SubstAction s e)
makePrisms ''SubstEnv

newtype SubstM s e a = SubstM 
  { forall s e a.
SubstM s e a
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
unSubstM ∷ UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a 
  } deriving
  ( (forall a. a -> SubstM s e a) -> Return (SubstM s e)
forall a. a -> SubstM s e a
forall s e a. a -> SubstM s e a
forall (m :: * -> *). (forall a. a -> m a) -> Return m
$creturn :: forall s e a. a -> SubstM s e a
return :: forall a. a -> SubstM s e a
Return,(forall a b. SubstM s e a -> (a -> SubstM s e b) -> SubstM s e b)
-> Bind (SubstM s e)
forall a b. SubstM s e a -> (a -> SubstM s e b) -> SubstM s e b
forall s e a b. SubstM s e a -> (a -> SubstM s e b) -> SubstM s e b
forall (m :: * -> *).
(forall a b. m a -> (a -> m b) -> m b) -> Bind m
$c≫= :: forall s e a b. SubstM s e a -> (a -> SubstM s e b) -> SubstM s e b
≫= :: forall a b. SubstM s e a -> (a -> SubstM s e b) -> SubstM s e b
Bind,(forall a b. (a -> b) -> SubstM s e a -> SubstM s e b)
-> Functor (SubstM s e)
forall a b. (a -> b) -> SubstM s e a -> SubstM s e b
forall s e a b. (a -> b) -> SubstM s e a -> SubstM s e b
forall (t :: * -> *).
(forall a b. (a -> b) -> t a -> t b) -> Functor t
$cmap :: forall s e a b. (a -> b) -> SubstM s e a -> SubstM s e b
map :: forall a b. (a -> b) -> SubstM s e a -> SubstM s e b
Functor,Bind (SubstM s e)
Return (SubstM s e)
Functor (SubstM s e)
(Functor (SubstM s e), Return (SubstM s e), Bind (SubstM s e)) =>
Monad (SubstM s e)
forall s e. Bind (SubstM s e)
forall s e. Return (SubstM s e)
forall s e. Functor (SubstM s e)
forall (m :: * -> *). (Functor m, Return m, Bind m) => Monad m
Monad
  , (forall a.
 (forall u. (a -> SubstM s e u) -> SubstM s e u) -> SubstM s e a)
-> (forall a u.
    (a -> SubstM s e u) -> SubstM s e a -> SubstM s e u)
-> MonadUCont (SubstM s e)
forall a.
(forall u. (a -> SubstM s e u) -> SubstM s e u) -> SubstM s e a
forall s e a.
Ord s =>
(forall u. (a -> SubstM s e u) -> SubstM s e u) -> SubstM s e a
forall s e a u.
Ord s =>
(a -> SubstM s e u) -> SubstM s e a -> SubstM s e u
forall a u. (a -> SubstM s e u) -> SubstM s e a -> SubstM s e u
forall (m :: * -> *).
(forall a. (forall u. (a -> m u) -> m u) -> m a)
-> (forall a u. (a -> m u) -> m a -> m u) -> MonadUCont m
$cucallCC :: forall s e a.
Ord s =>
(forall u. (a -> SubstM s e u) -> SubstM s e u) -> SubstM s e a
ucallCC :: forall a.
(forall u. (a -> SubstM s e u) -> SubstM s e u) -> SubstM s e a
$cuwithC :: forall s e a u.
Ord s =>
(a -> SubstM s e u) -> SubstM s e a -> SubstM s e u
uwithC :: forall a u. (a -> SubstM s e u) -> SubstM s e a -> SubstM s e u
MonadUCont
  , MonadReader (SubstEnv s e)
  , MonadWriter (s ⇰ 𝑃 𝕐)
  , (forall a. SubstM s e a)
-> (forall a. SubstM s e a -> SubstM s e a -> SubstM s e a)
-> MonadFail (SubstM s e)
forall a. SubstM s e a
forall a. SubstM s e a -> SubstM s e a -> SubstM s e a
forall s e a. Ord s => SubstM s e a
forall s e a. Ord s => SubstM s e a -> SubstM s e a -> SubstM s e a
forall {k} (m :: k -> *).
(forall (a :: k). m a)
-> (forall (a :: k). m a -> m a -> m a) -> MonadFail m
$cabort :: forall s e a. Ord s => SubstM s e a
abort :: forall a. SubstM s e a
$c⎅ :: forall s e a. Ord s => SubstM s e a -> SubstM s e a -> SubstM s e a
⎅ :: forall a. SubstM s e a -> SubstM s e a -> SubstM s e a
MonadFail
  )

mkSubstM ∷ (∀ u. SubstEnv s e → (a → SubstEnv s e → (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) → (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
         → SubstM s e a
mkSubstM :: forall s e a.
(forall u.
 SubstEnv s e
 -> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> SubstM s e a
mkSubstM forall u.
SubstEnv s e
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
f = UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
-> SubstM s e a
forall s e a.
UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
-> SubstM s e a
SubstM (UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
 -> SubstM s e a)
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
-> SubstM s e a
forall a b. (a -> b) -> a -> b
$ (forall u.
 (a -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u)
 -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u)
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
forall {k} (m :: k -> *) a.
(forall (u :: k). (a -> m u) -> m u) -> UContT m a
UContT (\ a -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
𝓀 → (SubstEnv s e -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
forall {k} r (m :: k -> *) (a :: k). (r -> m a) -> ReaderT r m a
ReaderT ((SubstEnv s e -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
 -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u)
-> (SubstEnv s e -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
forall a b. (a -> b) -> a -> b
$ \ SubstEnv s e
γ → WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall (m :: * -> *) a. m (𝑂 a) -> FailT m a
FailT (WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall a b. (a -> b) -> a -> b
$ ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall o (m :: * -> *) a. m (o ∧ a) -> WriterT o m a
WriterT (ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u))
-> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall a b. (a -> b) -> a -> b
$ ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall a. a -> ID a
ID (((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u))
-> ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall a b. (a -> b) -> a -> b
$ SubstEnv s e
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall u.
SubstEnv s e
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
f SubstEnv s e
γ ((a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall a b. (a -> b) -> a -> b
$ \ a
x SubstEnv s e
γ' → 
  ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall a. ID a -> a
unID (ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall a b. (a -> b) -> a -> b
$ WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall o (m :: * -> *) a. WriterT o m a -> m (o ∧ a)
unWriterT (WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u))
-> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall a b. (a -> b) -> a -> b
$ FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall (m :: * -> *) a. FailT m a -> m (𝑂 a)
unFailT (FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u))
-> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall a b. (a -> b) -> a -> b
$ SubstEnv s e
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
-> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall {k} r (m :: k -> *) (a :: k). r -> ReaderT r m a -> m a
runReaderT SubstEnv s e
γ' (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
 -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
-> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall a b. (a -> b) -> a -> b
$ a -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
𝓀 a
x)

runSubstM ∷ 
    SubstEnv s e 
  → (a → SubstEnv s e → (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) 
  → SubstM s e a 
  → (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
runSubstM :: forall s e a u.
SubstEnv s e
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> SubstM s e a
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
runSubstM SubstEnv s e
γ a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
𝓀 = ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall a. ID a -> a
unID (ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> (WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u))
-> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall o (m :: * -> *) a. WriterT o m a -> m (o ∧ a)
unWriterT (WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> (FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u))
-> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall (m :: * -> *) a. FailT m a -> m (𝑂 a)
unFailT (FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
    -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstEnv s e
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
-> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall {k} r (m :: k -> *) (a :: k). r -> ReaderT r m a -> m a
runReaderT SubstEnv s e
γ (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
 -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> (UContT
      (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
    -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u)
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u)
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
forall {k} (u :: k) (m :: k -> *) a.
(a -> m u) -> UContT m a -> m u
runUContT a -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
𝓀' (UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
 -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> (SubstM s e a
    -> UContT
         (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a)
-> SubstM s e a
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstM s e a
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
forall s e a.
SubstM s e a
-> UContT (ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID))) a
unSubstM
  where
    𝓀' :: a -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
𝓀' a
x = (SubstEnv s e -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
forall {k} r (m :: k -> *) (a :: k). (r -> m a) -> ReaderT r m a
ReaderT ((SubstEnv s e -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
 -> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u)
-> (SubstEnv s e -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> ReaderT (SubstEnv s e) (FailT (WriterT (s ⇰ 𝑃 𝕐) ID)) u
forall a b. (a -> b) -> a -> b
$ \ SubstEnv s e
γ' → WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall (m :: * -> *) a. m (𝑂 a) -> FailT m a
FailT (WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u)
-> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u) -> FailT (WriterT (s ⇰ 𝑃 𝕐) ID) u
forall a b. (a -> b) -> a -> b
$ ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall o (m :: * -> *) a. m (o ∧ a) -> WriterT o m a
WriterT (ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u))
-> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> WriterT (s ⇰ 𝑃 𝕐) ID (𝑂 u)
forall a b. (a -> b) -> a -> b
$ ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall a. a -> ID a
ID (((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u))
-> ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> ID ((s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
forall a b. (a -> b) -> a -> b
$ a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
𝓀 a
x SubstEnv s e
γ'

runSubstMHalt ∷ SubstEnv s e → SubstM s e a → (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
runSubstMHalt :: forall s e a. SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
runSubstMHalt SubstEnv s e
γ = SubstEnv s e
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a)
-> SubstM s e a
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
forall s e a u.
SubstEnv s e
-> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u)
-> SubstM s e a
-> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u
runSubstM SubstEnv s e
γ (\ a
x SubstEnv s e
_ → s ⇰ 𝑃 𝕐
forall a. Null a => a
null (s ⇰ 𝑃 𝕐) -> 𝑂 a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
forall a b. a -> b -> a ∧ b
:* a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x)

class Substy s e a | a→s,a→e where
  substy ∷ a → SubstM s e a

subst ∷ (Substy s e a) ⇒ Subst s e → a → 𝑂 a
subst :: forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst Subst s e
𝓈 = ((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> SubstM s e a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
forall s e a. SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
runSubstMHalt (SubstAction s e -> SubstEnv s e
forall s e. SubstAction s e -> SubstEnv s e
SubSubstEnv (SubstAction s e -> SubstEnv s e)
-> SubstAction s e -> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ 𝑂 Bool -> Subst s e -> SubstAction s e
forall s e. 𝑂 Bool -> Subst s e -> SubstAction s e
SubstAction 𝑂 Bool
forall a. 𝑂 a
None Subst s e
𝓈) (SubstM s e a -> 𝑂 a) -> (a -> SubstM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstM s e a
forall s e a. Substy s e a => a -> SubstM s e a
substy

todbr ∷ (Substy s e a) ⇒ a → 𝑂 a
todbr :: forall s e a. Substy s e a => a -> 𝑂 a
todbr = ((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> SubstM s e a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
forall s e a. SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
runSubstMHalt (SubstAction s e -> SubstEnv s e
forall s e. SubstAction s e -> SubstEnv s e
SubSubstEnv (SubstAction s e -> SubstEnv s e)
-> SubstAction s e -> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ 𝑂 Bool -> Subst s e -> SubstAction s e
forall s e. 𝑂 Bool -> Subst s e -> SubstAction s e
SubstAction (Bool -> 𝑂 Bool
forall a. a -> 𝑂 a
Some Bool
True) Subst s e
forall a. Null a => a
null) (SubstM s e a -> 𝑂 a) -> (a -> SubstM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstM s e a
forall s e a. Substy s e a => a -> SubstM s e a
substy

tonmd ∷ (Substy s e a) ⇒ a → 𝑂 a
tonmd :: forall s e a. Substy s e a => a -> 𝑂 a
tonmd = ((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> SubstM s e a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
forall s e a. SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
runSubstMHalt (SubstAction s e -> SubstEnv s e
forall s e. SubstAction s e -> SubstEnv s e
SubSubstEnv (SubstAction s e -> SubstEnv s e)
-> SubstAction s e -> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ 𝑂 Bool -> Subst s e -> SubstAction s e
forall s e. 𝑂 Bool -> Subst s e -> SubstAction s e
SubstAction (Bool -> 𝑂 Bool
forall a. a -> 𝑂 a
Some Bool
False) Subst s e
forall a. Null a => a
null) (SubstM s e a -> 𝑂 a) -> (a -> SubstM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstM s e a
forall s e a. Substy s e a => a -> SubstM s e a
substy

fvsWith ∷ (Substy s e a) ⇒ (FreeVarsAction s → FreeVarsAction s) → a → s ⇰ 𝑃 𝕐
fvsWith :: forall s e a.
Substy s e a =>
(FreeVarsAction s -> FreeVarsAction s) -> a -> s ⇰ 𝑃 𝕐
fvsWith FreeVarsAction s -> FreeVarsAction s
f = ((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> s ⇰ 𝑃 𝕐
forall a b. (a ∧ b) -> a
fst (((s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> s ⇰ 𝑃 𝕐)
-> (SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a) -> SubstM s e a -> s ⇰ 𝑃 𝕐
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
forall s e a. SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a
runSubstMHalt (FreeVarsAction s -> SubstEnv s e
forall s e. FreeVarsAction s -> SubstEnv s e
FVsSubstEnv (FreeVarsAction s -> SubstEnv s e)
-> FreeVarsAction s -> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ FreeVarsAction s -> FreeVarsAction s
f (FreeVarsAction s -> FreeVarsAction s)
-> FreeVarsAction s -> FreeVarsAction s
forall a b. (a -> b) -> a -> b
$ (s -> 𝕐 -> Bool) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> FreeVarsAction s
forall s. (s -> 𝕐 -> Bool) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> FreeVarsAction s
FreeVarsAction ((𝕐 -> Bool) -> s -> 𝕐 -> Bool
forall a b. a -> b -> a
const ((𝕐 -> Bool) -> s -> 𝕐 -> Bool) -> (𝕐 -> Bool) -> s -> 𝕐 -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> 𝕐 -> Bool
forall a b. a -> b -> a
const Bool
True) (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a. Null a => a
null) (SubstM s e a -> s ⇰ 𝑃 𝕐) -> (a -> SubstM s e a) -> a -> s ⇰ 𝑃 𝕐
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstM s e a
forall s e a. Substy s e a => a -> SubstM s e a
substy

fvsSMetas ∷ (Ord s,Substy s e a) ⇒ 𝑃 s → a → s ⇰ 𝑃 𝕏
fvsSMetas :: forall s e a. (Ord s, Substy s e a) => 𝑃 s -> a -> s ⇰ 𝑃 𝕏
fvsSMetas 𝑃 s
ss = 
  (𝑃 𝕐 -> 𝑃 𝕏) -> (s ⇰ 𝑃 𝕐) -> s ⇰ 𝑃 𝕏
forall a b. (a -> b) -> (s ⇰ a) -> s ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝐼 𝕏 -> 𝑃 𝕏
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 𝕏 -> 𝑃 𝕏) -> (𝐼 𝕐 -> 𝐼 𝕏) -> 𝐼 𝕐 -> 𝑃 𝕏
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (𝕐 -> 𝑂 𝕏) -> 𝐼 𝕐 -> 𝐼 𝕏
forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap ((𝕐 ⌲ 𝕏) -> 𝕐 -> 𝑂 𝕏
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝕐 ⌲ 𝕏
mVarL) (𝐼 𝕐 -> 𝑃 𝕏) -> (𝑃 𝕐 -> 𝐼 𝕐) -> 𝑃 𝕐 -> 𝑃 𝕏
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 𝕐 -> 𝐼 𝕐
forall a t. ToIter a t => t -> 𝐼 a
iter) 
  ((s ⇰ 𝑃 𝕐) -> s ⇰ 𝑃 𝕏) -> (a -> s ⇰ 𝑃 𝕐) -> a -> s ⇰ 𝑃 𝕏
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (FreeVarsAction s -> FreeVarsAction s) -> a -> s ⇰ 𝑃 𝕐
forall s e a.
Substy s e a =>
(FreeVarsAction s -> FreeVarsAction s) -> a -> s ⇰ 𝑃 𝕐
fvsWith ((FreeVarsAction s ⟢ (s -> 𝕐 -> Bool))
-> (s -> 𝕐 -> Bool) -> FreeVarsAction s -> FreeVarsAction s
forall (t :: * -> * -> *) a b. Alter t => t a b -> b -> a -> a
update FreeVarsAction s ⟢ (s -> 𝕐 -> Bool)
forall s. FreeVarsAction s ⟢ (s -> 𝕐 -> Bool)
freeVarsActionFilterL ((s -> 𝕐 -> Bool) -> FreeVarsAction s -> FreeVarsAction s)
-> (s -> 𝕐 -> Bool) -> FreeVarsAction s -> FreeVarsAction s
forall a b. (a -> b) -> a -> b
$ \ s
s 𝕐
y → s
s s -> 𝑃 s -> Bool
forall e s. Set e s => e -> s -> Bool
∈ 𝑃 s
ss Bool -> Bool -> Bool
⩓ (𝕐 ⌲ 𝕏) -> 𝕐 -> Bool
forall a b. (a ⌲ b) -> a -> Bool
shape 𝕐 ⌲ 𝕏
mVarL 𝕐
y)

fvsMetas ∷ (Ord s,Substy s e a) ⇒ s → a → 𝑃 𝕏
fvsMetas :: forall s e a. (Ord s, Substy s e a) => s -> a -> 𝑃 𝕏
fvsMetas s
s a
x = 𝑃 𝕏 -> 𝑂 (𝑃 𝕏) -> 𝑃 𝕏
forall a. a -> 𝑂 a -> a
ifNone 𝑃 𝕏
forall e s. Set e s => s
pø (𝑂 (𝑃 𝕏) -> 𝑃 𝕏) -> 𝑂 (𝑃 𝕏) -> 𝑃 𝕏
forall a b. (a -> b) -> a -> b
$ 𝑃 s -> a -> s ⇰ 𝑃 𝕏
forall s e a. (Ord s, Substy s e a) => 𝑃 s -> a -> s ⇰ 𝑃 𝕏
fvsSMetas (s -> 𝑃 s
forall a t. Single a t => a -> t
single s
s) a
x (s ⇰ 𝑃 𝕏) -> s -> 𝑂 (𝑃 𝕏)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? s
s

fvs ∷ (Substy s e a) ⇒ a → s ⇰ 𝑃 𝕐
fvs :: forall s e a. Substy s e a => a -> s ⇰ 𝑃 𝕐
fvs = (FreeVarsAction s -> FreeVarsAction s) -> a -> s ⇰ 𝑃 𝕐
forall s e a.
Substy s e a =>
(FreeVarsAction s -> FreeVarsAction s) -> a -> s ⇰ 𝑃 𝕐
fvsWith FreeVarsAction s -> FreeVarsAction s
forall a. a -> a
id

nullSubst ∷ Subst s e
nullSubst :: forall s e. Subst s e
nullSubst = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₁ s₂ e.
(s₁ ⇰ SubstElem s₂ e)
-> (s₁ ⇰ SubstElem s₂ e) -> (s₂ ⇰ DSubst s₂ e) -> GSubst s₁ s₂ e
GSubst (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
forall a. Null a => a
null (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
forall a. Null a => a
null (s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e
forall a. Null a => a
null

appendSubst ∷ (Ord s,Substy s e e) ⇒ Subst s e → Subst s e → Subst s e
appendSubst :: forall s e.
(Ord s, Substy s e e) =>
Subst s e -> Subst s e -> Subst s e
appendSubst Subst s e
𝓈₂ Subst s e
𝓈₁ = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> e -> 𝑂 e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₁ s₂ e.
(Ord s₁, Ord s₂) =>
(GSubst s₁ s₂ e -> e -> 𝑂 e)
-> GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
appendGSubst (Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (Subst s e -> e -> 𝑂 e)
-> (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
-> e
-> 𝑂 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst) (Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubst Subst s e
𝓈₂) (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubst Subst s e
𝓈₁

instance                        Null   (Subst s e) where null :: Subst s e
null = Subst s e
forall s e. Subst s e
nullSubst
instance (Ord s,Substy s e e) ⇒ Append (Subst s e) where ⧺ :: Subst s e -> Subst s e -> Subst s e
(⧺)  = Subst s e -> Subst s e -> Subst s e
forall s e.
(Ord s, Substy s e e) =>
Subst s e -> Subst s e -> Subst s e
appendSubst
instance (Ord s,Substy s e e) ⇒ Monoid (Subst s e)

𝓈sdshift ∷ (Ord s) ⇒ s ⇰ ℕ64 → Subst s e → Subst s e
𝓈sdshift :: forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e
𝓈sdshift = (Subst s e ⟢ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> Subst s e
-> Subst s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter Subst s e ⟢ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e ⟢ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubstL ((GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
 -> Subst s e -> Subst s e)
-> (((s ∧ 𝑂 𝕏) ⇰ ℕ64)
    -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e.
Ord s₂ =>
(s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
𝓈shiftG (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> Subst s e -> Subst s e)
-> (𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> Subst s e -> Subst s e)
-> (𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64))
-> 𝐼 (s ∧ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64)
-> 𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s -> s ∧ 𝑂 𝕏) -> (s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((s -> s ∧ 𝑂 𝕏) -> (s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64)
-> (s -> s ∧ 𝑂 𝕏) -> (s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64
forall a b. (a -> b) -> a -> b
$ (s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏) -> 𝑂 𝕏 -> s -> s ∧ 𝑂 𝕏
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
(:*) 𝑂 𝕏
forall a. 𝑂 a
None) (𝐼 (s ∧ ℕ64) -> Subst s e -> Subst s e)
-> ((s ⇰ ℕ64) -> 𝐼 (s ∧ ℕ64))
-> (s ⇰ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⇰ ℕ64) -> 𝐼 (s ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter

𝓈snshift ∷ (Ord s) ⇒ s ⇰ 𝕏 ⇰ ℕ64 → Subst s e → Subst s e
𝓈snshift :: forall s e. Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e
𝓈snshift s ⇰ (𝕏 ⇰ ℕ64)
𝑠 = (Subst s e ⟢ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> Subst s e
-> Subst s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter Subst s e ⟢ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e ⟢ GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubstL ((GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
 -> Subst s e -> Subst s e)
-> (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> Subst s e
-> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e.
Ord s₂ =>
(s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e
𝓈shiftG (((s ∧ 𝑂 𝕏) ⇰ ℕ64)
 -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a b. (a -> b) -> a -> b
$ do
  s
s :* 𝕏 ⇰ ℕ64
xns ← (s ⇰ (𝕏 ⇰ ℕ64)) -> 𝐼 (s ∧ (𝕏 ⇰ ℕ64))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (𝕏 ⇰ ℕ64)
𝑠
  𝕏
x :* ℕ64
n ← (𝕏 ⇰ ℕ64) -> 𝐼 (𝕏 ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕏 ⇰ ℕ64
xns
  ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ 𝑂 𝕏) ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64))
-> ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏 -> 𝑂 𝕏
forall a. a -> 𝑂 a
Some 𝕏
x (s ∧ 𝑂 𝕏) -> ℕ64 -> (s ∧ 𝑂 𝕏) ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
n

𝓈sdintro ∷ (Ord s) ⇒ s ⇰ ℕ64 → Subst s e
𝓈sdintro :: forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e
𝓈sdintro = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> Subst s e)
-> (𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> Subst s e)
-> (𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)) -> 𝐼 (s ∧ ℕ64) -> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64)
-> 𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s -> s ∧ 𝑂 𝕏) -> (s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((s -> s ∧ 𝑂 𝕏) -> (s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64)
-> (s -> s ∧ 𝑂 𝕏) -> (s ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ∧ ℕ64
forall a b. (a -> b) -> a -> b
$ (s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏) -> 𝑂 𝕏 -> s -> s ∧ 𝑂 𝕏
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
(:*) 𝑂 𝕏
forall a. 𝑂 a
None) (𝐼 (s ∧ ℕ64) -> Subst s e)
-> ((s ⇰ ℕ64) -> 𝐼 (s ∧ ℕ64)) -> (s ⇰ ℕ64) -> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⇰ ℕ64) -> 𝐼 (s ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter

𝓈snintro ∷ (Ord s) ⇒ s ⇰ 𝕏 ⇰ ℕ64 → Subst s e
𝓈snintro :: forall s e. Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e
𝓈snintro s ⇰ (𝕏 ⇰ ℕ64)
𝑠 = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a b. (a -> b) -> a -> b
$ do
  s
s :* 𝕏 ⇰ ℕ64
xns ← (s ⇰ (𝕏 ⇰ ℕ64)) -> 𝐼 (s ∧ (𝕏 ⇰ ℕ64))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (𝕏 ⇰ ℕ64)
𝑠
  𝕏
x :* ℕ64
n ← (𝕏 ⇰ ℕ64) -> 𝐼 (𝕏 ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕏 ⇰ ℕ64
xns
  ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ 𝑂 𝕏) ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64))
-> ((s ∧ 𝑂 𝕏) ∧ ℕ64) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ ℕ64)
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏 -> 𝑂 𝕏
forall a. a -> 𝑂 a
Some 𝕏
x (s ∧ 𝑂 𝕏) -> ℕ64 -> (s ∧ 𝑂 𝕏) ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
n

𝓈sdbinds ∷ (Ord s) ⇒ s ⇰ 𝕍 e → Subst s e
𝓈sdbinds :: forall s e. Ord s => (s ⇰ 𝕍 e) -> Subst s e
𝓈sdbinds = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> (((s ∧ 𝑂 𝕏) ⇰ 𝕍 e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ 𝕍 e)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ 𝑂 𝕏) ⇰ 𝕍 e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ e s₁. (s₂ ⇰ 𝕍 e) -> GSubst s₁ s₂ e
𝓈sbindsG (((s ∧ 𝑂 𝕏) ⇰ 𝕍 e) -> Subst s e)
-> (𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ⇰ 𝕍 e)
-> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ⇰ 𝕍 e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> Subst s e)
-> (𝐼 (s ∧ 𝕍 e) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e)) -> 𝐼 (s ∧ 𝕍 e) -> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ∧ 𝕍 e)
-> 𝐼 (s ∧ 𝕍 e) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s -> s ∧ 𝑂 𝕏) -> (s ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ∧ 𝕍 e
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((s -> s ∧ 𝑂 𝕏) -> (s ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ∧ 𝕍 e)
-> (s -> s ∧ 𝑂 𝕏) -> (s ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ∧ 𝕍 e
forall a b. (a -> b) -> a -> b
$ (s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏) -> 𝑂 𝕏 -> s -> s ∧ 𝑂 𝕏
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
(:*) 𝑂 𝕏
forall a. 𝑂 a
None) (𝐼 (s ∧ 𝕍 e) -> Subst s e)
-> ((s ⇰ 𝕍 e) -> 𝐼 (s ∧ 𝕍 e)) -> (s ⇰ 𝕍 e) -> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s ⇰ 𝕍 e) -> 𝐼 (s ∧ 𝕍 e)
forall a t. ToIter a t => t -> 𝐼 a
iter

𝓈sdbind ∷ (Ord s) ⇒ s → e → Subst s e
𝓈sdbind :: forall s e. Ord s => s -> e -> Subst s e
𝓈sdbind s
s e
e = (s ⇰ 𝕍 e) -> Subst s e
forall s e. Ord s => (s ⇰ 𝕍 e) -> Subst s e
𝓈sdbinds ((s ⇰ 𝕍 e) -> Subst s e) -> (s ⇰ 𝕍 e) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝕍 e -> s ⇰ 𝕍 e
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e -> 𝕍 e
forall a t. Single a t => a -> t
single e
e

𝓈snbinds ∷ (Ord s) ⇒ s ⇰ 𝕏 ⇰ 𝕍 e → Subst s e
𝓈snbinds :: forall s e. Ord s => (s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e
𝓈snbinds s ⇰ (𝕏 ⇰ 𝕍 e)
𝑠 = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ 𝕍 e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ e s₁. (s₂ ⇰ 𝕍 e) -> GSubst s₁ s₂ e
𝓈sbindsG (((s ∧ 𝑂 𝕏) ⇰ 𝕍 e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝑂 𝕏) ⇰ 𝕍 e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ⇰ 𝕍 e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ⇰ 𝕍 e)
-> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> (s ∧ 𝑂 𝕏) ⇰ 𝕍 e
forall a b. (a -> b) -> a -> b
$ do
  s
s :* 𝕏 ⇰ 𝕍 e
xess ← (s ⇰ (𝕏 ⇰ 𝕍 e)) -> 𝐼 (s ∧ (𝕏 ⇰ 𝕍 e))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (𝕏 ⇰ 𝕍 e)
𝑠
  𝕏
x :* 𝕍 e
es ← (𝕏 ⇰ 𝕍 e) -> 𝐼 (𝕏 ∧ 𝕍 e)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕏 ⇰ 𝕍 e
xess
  ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e))
-> ((s ∧ 𝑂 𝕏) ∧ 𝕍 e) -> 𝐼 ((s ∧ 𝑂 𝕏) ∧ 𝕍 e)
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏 -> 𝑂 𝕏
forall a. a -> 𝑂 a
Some 𝕏
x (s ∧ 𝑂 𝕏) -> 𝕍 e -> (s ∧ 𝑂 𝕏) ∧ 𝕍 e
forall a b. a -> b -> a ∧ b
:* 𝕍 e
es

𝓈snbind ∷ (Ord s) ⇒ s → 𝕏 → e → Subst s e
𝓈snbind :: forall s e. Ord s => s -> 𝕏 -> e -> Subst s e
𝓈snbind s
s 𝕏
x e
e = (s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e
𝓈snbinds ((s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e) -> (s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (𝕏 ⇰ 𝕍 e) -> s ⇰ (𝕏 ⇰ 𝕍 e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕏
x 𝕏 -> 𝕍 e -> 𝕏 ⇰ 𝕍 e
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e -> 𝕍 e
forall a t. Single a t => a -> t
single e
e

𝓈sgbinds ∷ (Ord s) ⇒ s ⇰ 𝕏 ⇰ e → Subst s e
𝓈sgbinds :: forall s e. Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e
𝓈sgbinds s ⇰ (𝕏 ⇰ e)
sxes = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝕏) ⇰ e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₁ e s₂. (s₁ ⇰ e) -> GSubst s₁ s₂ e
𝓈sgbindsG (((s ∧ 𝕏) ⇰ e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝕏) ⇰ e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ 𝕏) ∧ e) -> (s ∧ 𝕏) ⇰ e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝕏) ∧ e) -> (s ∧ 𝕏) ⇰ e) -> 𝐼 ((s ∧ 𝕏) ∧ e) -> (s ∧ 𝕏) ⇰ e
forall a b. (a -> b) -> a -> b
$ do
  s
s :* 𝕏 ⇰ e
xes ← (s ⇰ (𝕏 ⇰ e)) -> 𝐼 (s ∧ (𝕏 ⇰ e))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (𝕏 ⇰ e)
sxes
  𝕏
x :* e
e ← (𝕏 ⇰ e) -> 𝐼 (𝕏 ∧ e)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕏 ⇰ e
xes
  ((s ∧ 𝕏) ∧ e) -> 𝐼 ((s ∧ 𝕏) ∧ e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ 𝕏) ∧ e) -> 𝐼 ((s ∧ 𝕏) ∧ e))
-> ((s ∧ 𝕏) ∧ e) -> 𝐼 ((s ∧ 𝕏) ∧ e)
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝕏 -> s ∧ 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏
x (s ∧ 𝕏) -> e -> (s ∧ 𝕏) ∧ e
forall a b. a -> b -> a ∧ b
:* e
e

𝓈sgbind ∷ (Ord s) ⇒ s → 𝕏 → e → Subst s e
𝓈sgbind :: forall s e. Ord s => s -> 𝕏 -> e -> Subst s e
𝓈sgbind s
s 𝕏
x e
e = (s ⇰ (𝕏 ⇰ e)) -> Subst s e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e
𝓈sgbinds ((s ⇰ (𝕏 ⇰ e)) -> Subst s e) -> (s ⇰ (𝕏 ⇰ e)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (𝕏 ⇰ e) -> s ⇰ (𝕏 ⇰ e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕏
x 𝕏 -> e -> 𝕏 ⇰ e
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e
e

𝓈smbinds ∷ (Ord s) ⇒ s ⇰ 𝕏 ⇰ e → Subst s e
𝓈smbinds :: forall s e. Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e
𝓈smbinds s ⇰ (𝕏 ⇰ e)
sxes = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝕏) ⇰ e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₁ e s₂. (s₁ ⇰ e) -> GSubst s₁ s₂ e
𝓈smbindsG (((s ∧ 𝕏) ⇰ e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> ((s ∧ 𝕏) ⇰ e) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ 𝕏) ∧ e) -> (s ∧ 𝕏) ⇰ e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ 𝕏) ∧ e) -> (s ∧ 𝕏) ⇰ e) -> 𝐼 ((s ∧ 𝕏) ∧ e) -> (s ∧ 𝕏) ⇰ e
forall a b. (a -> b) -> a -> b
$ do
  s
s :* 𝕏 ⇰ e
xes ← (s ⇰ (𝕏 ⇰ e)) -> 𝐼 (s ∧ (𝕏 ⇰ e))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (𝕏 ⇰ e)
sxes
  𝕏
x :* e
e ← (𝕏 ⇰ e) -> 𝐼 (𝕏 ∧ e)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕏 ⇰ e
xes
  ((s ∧ 𝕏) ∧ e) -> 𝐼 ((s ∧ 𝕏) ∧ e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ 𝕏) ∧ e) -> 𝐼 ((s ∧ 𝕏) ∧ e))
-> ((s ∧ 𝕏) ∧ e) -> 𝐼 ((s ∧ 𝕏) ∧ e)
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝕏 -> s ∧ 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏
x (s ∧ 𝕏) -> e -> (s ∧ 𝕏) ∧ e
forall a b. a -> b -> a ∧ b
:* e
e

𝓈smbind ∷ (Ord s) ⇒ s → 𝕏 → e → Subst s e
𝓈smbind :: forall s e. Ord s => s -> 𝕏 -> e -> Subst s e
𝓈smbind s
s 𝕏
x e
e = (s ⇰ (𝕏 ⇰ e)) -> Subst s e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e
𝓈smbinds ((s ⇰ (𝕏 ⇰ e)) -> Subst s e) -> (s ⇰ (𝕏 ⇰ e)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (𝕏 ⇰ e) -> s ⇰ (𝕏 ⇰ e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕏
x 𝕏 -> e -> 𝕏 ⇰ e
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e
e

𝓈dshift ∷ ℕ64 → Subst () e → Subst () e
𝓈dshift :: forall e. ℕ64 -> Subst () e -> Subst () e
𝓈dshift = (() ⇰ ℕ64) -> Subst () e -> Subst () e
forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e
𝓈sdshift ((() ⇰ ℕ64) -> Subst () e -> Subst () e)
-> (ℕ64 -> () ⇰ ℕ64) -> ℕ64 -> Subst () e -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> ℕ64 -> () ⇰ ℕ64
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈nshift ∷ 𝕏 ⇰ ℕ64 → Subst () e → Subst () e
𝓈nshift :: forall e. (𝕏 ⇰ ℕ64) -> Subst () e -> Subst () e
𝓈nshift = (() ⇰ (𝕏 ⇰ ℕ64)) -> Subst () e -> Subst () e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e
𝓈snshift ((() ⇰ (𝕏 ⇰ ℕ64)) -> Subst () e -> Subst () e)
-> ((𝕏 ⇰ ℕ64) -> () ⇰ (𝕏 ⇰ ℕ64))
-> (𝕏 ⇰ ℕ64)
-> Subst () e
-> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> (𝕏 ⇰ ℕ64) -> () ⇰ (𝕏 ⇰ ℕ64)
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈dintro ∷ ℕ64 → Subst () e
𝓈dintro :: forall e. ℕ64 -> Subst () e
𝓈dintro = (() ⇰ ℕ64) -> Subst () e
forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e
𝓈sdintro ((() ⇰ ℕ64) -> Subst () e)
-> (ℕ64 -> () ⇰ ℕ64) -> ℕ64 -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> ℕ64 -> () ⇰ ℕ64
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈nintro ∷ 𝕏 ⇰ ℕ64 → Subst () e
𝓈nintro :: forall e. (𝕏 ⇰ ℕ64) -> Subst () e
𝓈nintro = (() ⇰ (𝕏 ⇰ ℕ64)) -> Subst () e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e
𝓈snintro ((() ⇰ (𝕏 ⇰ ℕ64)) -> Subst () e)
-> ((𝕏 ⇰ ℕ64) -> () ⇰ (𝕏 ⇰ ℕ64)) -> (𝕏 ⇰ ℕ64) -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> (𝕏 ⇰ ℕ64) -> () ⇰ (𝕏 ⇰ ℕ64)
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈dbinds ∷ 𝕍 e → Subst () e
𝓈dbinds :: forall e. 𝕍 e -> Subst () e
𝓈dbinds = (() ⇰ 𝕍 e) -> Subst () e
forall s e. Ord s => (s ⇰ 𝕍 e) -> Subst s e
𝓈sdbinds ((() ⇰ 𝕍 e) -> Subst () e)
-> (𝕍 e -> () ⇰ 𝕍 e) -> 𝕍 e -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> 𝕍 e -> () ⇰ 𝕍 e
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈dbind ∷ e → Subst () e
𝓈dbind :: forall e. e -> Subst () e
𝓈dbind = () -> e -> Subst () e
forall s e. Ord s => s -> e -> Subst s e
𝓈sdbind ()

𝓈nbinds ∷ 𝕏 ⇰ 𝕍 e → Subst () e
𝓈nbinds :: forall e. (𝕏 ⇰ 𝕍 e) -> Subst () e
𝓈nbinds = (() ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst () e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e
𝓈snbinds ((() ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst () e)
-> ((𝕏 ⇰ 𝕍 e) -> () ⇰ (𝕏 ⇰ 𝕍 e)) -> (𝕏 ⇰ 𝕍 e) -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> (𝕏 ⇰ 𝕍 e) -> () ⇰ (𝕏 ⇰ 𝕍 e)
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈nbind ∷ 𝕏 → e → Subst () e
𝓈nbind :: forall e. 𝕏 -> e -> Subst () e
𝓈nbind = () -> 𝕏 -> e -> Subst () e
forall s e. Ord s => s -> 𝕏 -> e -> Subst s e
𝓈snbind ()

𝓈gbinds ∷ 𝕏 ⇰ e → Subst () e
𝓈gbinds :: forall e. (𝕏 ⇰ e) -> Subst () e
𝓈gbinds = (() ⇰ (𝕏 ⇰ e)) -> Subst () e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e
𝓈sgbinds ((() ⇰ (𝕏 ⇰ e)) -> Subst () e)
-> ((𝕏 ⇰ e) -> () ⇰ (𝕏 ⇰ e)) -> (𝕏 ⇰ e) -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> (𝕏 ⇰ e) -> () ⇰ (𝕏 ⇰ e)
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈gbind ∷ 𝕏 → e → Subst () e
𝓈gbind :: forall e. 𝕏 -> e -> Subst () e
𝓈gbind 𝕏
x e
e = (𝕏 ⇰ e) -> Subst () e
forall e. (𝕏 ⇰ e) -> Subst () e
𝓈gbinds ((𝕏 ⇰ e) -> Subst () e) -> (𝕏 ⇰ e) -> Subst () e
forall a b. (a -> b) -> a -> b
$ 𝕏
x 𝕏 -> e -> 𝕏 ⇰ e
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e
e

𝓈mbinds ∷ 𝕏 ⇰ e → Subst () e
𝓈mbinds :: forall e. (𝕏 ⇰ e) -> Subst () e
𝓈mbinds = (() ⇰ (𝕏 ⇰ e)) -> Subst () e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e
𝓈smbinds ((() ⇰ (𝕏 ⇰ e)) -> Subst () e)
-> ((𝕏 ⇰ e) -> () ⇰ (𝕏 ⇰ e)) -> (𝕏 ⇰ e) -> Subst () e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ () -> (𝕏 ⇰ e) -> () ⇰ (𝕏 ⇰ e)
forall a. () -> a -> () ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
(↦) ()

𝓈mbind ∷ 𝕏 → e → Subst () e
𝓈mbind :: forall e. 𝕏 -> e -> Subst () e
𝓈mbind 𝕏
x e
e = (𝕏 ⇰ e) -> Subst () e
forall e. (𝕏 ⇰ e) -> Subst () e
𝓈mbinds ((𝕏 ⇰ e) -> Subst () e) -> (𝕏 ⇰ e) -> Subst () e
forall a b. (a -> b) -> a -> b
$ 𝕏
x 𝕏 -> e -> 𝕏 ⇰ e
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e
e

substyDBdr ∷ (Ord s) ⇒ s → SubstM s e ()
substyDBdr :: forall s e. Ord s => s -> SubstM s e ()
substyDBdr s
s = (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstEnv s e -> SubstEnv s e) -> SubstM s e ())
-> (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ [SubstEnv s e -> SubstEnv s e] -> SubstEnv s e -> SubstEnv s e
forall a t. ToIter (a -> a) t => t -> a -> a
compose
  [ (SubstEnv s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a ⌲ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstEnv s e ⌲ SubstAction s e
forall s e. SubstEnv s e ⌲ SubstAction s e
subSubstEnvL ((SubstAction s e -> SubstAction s e)
 -> SubstEnv s e -> SubstEnv s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> Subst s e -> Subst s e
forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e
𝓈sdshift ((s ⇰ ℕ64) -> Subst s e -> Subst s e)
-> (s ⇰ ℕ64) -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> ℕ64 -> s ⇰ ℕ64
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
  , (SubstEnv s e ⌲ FreeVarsAction s)
-> (FreeVarsAction s -> FreeVarsAction s)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a ⌲ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstEnv s e ⌲ FreeVarsAction s
forall s e. SubstEnv s e ⌲ FreeVarsAction s
fVsSubstEnvL ((FreeVarsAction s -> FreeVarsAction s)
 -> SubstEnv s e -> SubstEnv s e)
-> (FreeVarsAction s -> FreeVarsAction s)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ (FreeVarsAction s ⟢ ((s ∧ 𝑂 𝕏) ⇰ ℕ64))
-> (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> FreeVarsAction s
-> FreeVarsAction s
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter FreeVarsAction s ⟢ ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
forall s. FreeVarsAction s ⟢ ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
freeVarsActionScopeL ((((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
 -> FreeVarsAction s -> FreeVarsAction s)
-> (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> FreeVarsAction s
-> FreeVarsAction s
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a. Append a => a -> a -> a
(⧺) (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a b. (a -> b) -> a -> b
$ (s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝑂 𝕏
forall a. 𝑂 a
None) (s ∧ 𝑂 𝕏) -> ℕ64 -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a. (s ∧ 𝑂 𝕏) -> a -> (s ∧ 𝑂 𝕏) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
  ]

substyNBdr ∷ (Ord s) ⇒ s → 𝕏 → SubstM s e ()
substyNBdr :: forall s e. Ord s => s -> 𝕏 -> SubstM s e ()
substyNBdr s
s 𝕏
x = (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstEnv s e -> SubstEnv s e) -> SubstM s e ())
-> (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ [SubstEnv s e -> SubstEnv s e] -> SubstEnv s e -> SubstEnv s e
forall a t. ToIter (a -> a) t => t -> a -> a
compose
  [ (SubstEnv s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a ⌲ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstEnv s e ⌲ SubstAction s e
forall s e. SubstEnv s e ⌲ SubstAction s e
subSubstEnvL ((SubstAction s e -> SubstAction s e)
 -> SubstEnv s e -> SubstEnv s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e
𝓈snshift ((s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e)
-> (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (𝕏 ⇰ ℕ64) -> s ⇰ (𝕏 ⇰ ℕ64)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕏
x 𝕏 -> ℕ64 -> 𝕏 ⇰ ℕ64
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
  , (SubstEnv s e ⌲ FreeVarsAction s)
-> (FreeVarsAction s -> FreeVarsAction s)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a ⌲ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstEnv s e ⌲ FreeVarsAction s
forall s e. SubstEnv s e ⌲ FreeVarsAction s
fVsSubstEnvL ((FreeVarsAction s -> FreeVarsAction s)
 -> SubstEnv s e -> SubstEnv s e)
-> (FreeVarsAction s -> FreeVarsAction s)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ (FreeVarsAction s ⟢ ((s ∧ 𝑂 𝕏) ⇰ ℕ64))
-> (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> FreeVarsAction s
-> FreeVarsAction s
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter FreeVarsAction s ⟢ ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
forall s. FreeVarsAction s ⟢ ((s ∧ 𝑂 𝕏) ⇰ ℕ64)
freeVarsActionScopeL ((((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
 -> FreeVarsAction s -> FreeVarsAction s)
-> (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> FreeVarsAction s
-> FreeVarsAction s
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a. Append a => a -> a -> a
(⧺) (((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64)
-> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a b. (a -> b) -> a -> b
$ (s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏 -> 𝑂 𝕏
forall a. a -> 𝑂 a
Some 𝕏
x) (s ∧ 𝑂 𝕏) -> ℕ64 -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall a. (s ∧ 𝑂 𝕏) -> a -> (s ∧ 𝑂 𝕏) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
  ]

substyBdr ∷ (Ord s,Substy s e e) ⇒ s → (𝕐 → e) → 𝕏 → SubstM s e ()
substyBdr :: forall s e.
(Ord s, Substy s e e) =>
s -> (𝕐 -> e) -> 𝕏 -> SubstM s e ()
substyBdr s
s 𝕐 -> e
𝓋 𝕏
x = do
  s -> SubstM s e ()
forall s e. Ord s => s -> SubstM s e ()
substyDBdr s
s
  s -> 𝕏 -> SubstM s e ()
forall s e. Ord s => s -> 𝕏 -> SubstM s e ()
substyNBdr s
s 𝕏
x
  𝑂 Bool
bO ← (SubstAction s e ⟢ 𝑂 Bool) -> SubstAction s e -> 𝑂 Bool
forall a b. (a ⟢ b) -> a -> b
access SubstAction s e ⟢ 𝑂 Bool
forall s e. SubstAction s e ⟢ 𝑂 Bool
substActionReBdrL (SubstAction s e -> 𝑂 Bool)
-> (SubstEnv s e -> 𝑂 (SubstAction s e)) -> SubstEnv s e -> 𝑂 Bool
forall (m :: * -> *) b c a.
Bind m =>
(b -> m c) -> (a -> m b) -> a -> m c
*∘ (SubstEnv s e ⌲ SubstAction s e)
-> SubstEnv s e -> 𝑂 (SubstAction s e)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view SubstEnv s e ⌲ SubstAction s e
forall s e. SubstEnv s e ⌲ SubstAction s e
subSubstEnvL (SubstEnv s e -> 𝑂 Bool)
-> SubstM s e (SubstEnv s e) -> SubstM s e (𝑂 Bool)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ SubstM s e (SubstEnv s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case 𝑂 Bool
bO of
    𝑂 Bool
None → SubstM s e ()
forall (m :: * -> *). Return m => m ()
skip
    Some Bool
b → do
      if Bool
b 
      then
        (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstEnv s e -> SubstEnv s e) -> SubstM s e ())
-> (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ (SubstEnv s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a ⌲ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstEnv s e ⌲ SubstAction s e
forall s e. SubstEnv s e ⌲ SubstAction s e
subSubstEnvL ((SubstAction s e -> SubstAction s e)
 -> SubstEnv s e -> SubstEnv s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Subst s e -> Subst s e -> Subst s e
forall a. Append a => a -> a -> a
(⧺) (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ [Subst s e] -> Subst s e
forall a t. (Monoid a, ToIter a t) => t -> a
concat
          [ (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e
forall s e. Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e
𝓈snintro ((s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e) -> (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (𝕏 ⇰ ℕ64) -> s ⇰ (𝕏 ⇰ ℕ64)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕏
x 𝕏 -> ℕ64 -> 𝕏 ⇰ ℕ64
forall a. 𝕏 -> a -> 𝕏 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
          , s -> 𝕏 -> e -> Subst s e
forall s e. Ord s => s -> 𝕏 -> e -> Subst s e
𝓈snbind s
s 𝕏
x (e -> Subst s e) -> e -> Subst s e
forall a b. (a -> b) -> a -> b
$ 𝕐 -> e
𝓋 (𝕐 -> e) -> 𝕐 -> e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕐
DVar ℕ64
0
          ]
      else
        (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstEnv s e -> SubstEnv s e) -> SubstM s e ())
-> (SubstEnv s e -> SubstEnv s e) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ (SubstEnv s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a ⌲ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstEnv s e ⌲ SubstAction s e
forall s e. SubstEnv s e ⌲ SubstAction s e
subSubstEnvL ((SubstAction s e -> SubstAction s e)
 -> SubstEnv s e -> SubstEnv s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstEnv s e
-> SubstEnv s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Subst s e -> Subst s e -> Subst s e
forall a. Append a => a -> a -> a
(⧺) (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ [Subst s e] -> Subst s e
forall a t. (Monoid a, ToIter a t) => t -> a
concat
          [ (s ⇰ ℕ64) -> Subst s e
forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e
𝓈sdintro ((s ⇰ ℕ64) -> Subst s e) -> (s ⇰ ℕ64) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> ℕ64 -> s ⇰ ℕ64
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
          , s -> e -> Subst s e
forall s e. Ord s => s -> e -> Subst s e
𝓈sdbind s
s (e -> Subst s e) -> e -> Subst s e
forall a b. (a -> b) -> a -> b
$ 𝕐 -> e
𝓋 (𝕐 -> e) -> 𝕐 -> e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕏 -> 𝕐
NVar ℕ64
0 𝕏
x
          ]

substyVar ∷ (Ord s,Substy s e e) ⇒ 𝑂 𝕏 → s → (ℕ64 → e) → ℕ64 → SubstM s e e
substyVar :: forall s e.
(Ord s, Substy s e e) =>
𝑂 𝕏 -> s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
substyVar 𝑂 𝕏
xO s
s ℕ64 -> e
𝓋 ℕ64
n = do
  SubstEnv s e
γ ← SubstM s e (SubstEnv s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case SubstEnv s e
γ of
    FVsSubstEnv FreeVarsAction s
𝒶 → do
      let n₀ :: ℕ64
n₀ = ℕ64 -> 𝑂 ℕ64 -> ℕ64
forall a. a -> 𝑂 a -> a
ifNone ℕ64
0 (FreeVarsAction s -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
forall s. FreeVarsAction s -> (s ∧ 𝑂 𝕏) ⇰ ℕ64
freeVarsActionScope FreeVarsAction s
𝒶 ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> (s ∧ 𝑂 𝕏) -> 𝑂 ℕ64
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝑂 𝕏
xO))
      Bool -> (() -> SubstM s e ()) -> SubstM s e ()
forall (m :: * -> *). Return m => Bool -> (() -> m ()) -> m ()
when (ℕ64
n ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
≥ ℕ64
n₀) ((() -> SubstM s e ()) -> SubstM s e ())
-> (() -> SubstM s e ()) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ \ () → do
        let n' :: ℕ64
n' = ℕ64
nℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
-ℕ64
n₀
            y :: 𝕐
y = (() -> ℕ64 -> 𝕐) -> (𝕏 -> ℕ64 -> 𝕐) -> 𝑂 𝕏 -> ℕ64 -> 𝕐
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 ((ℕ64 -> 𝕐) -> () -> ℕ64 -> 𝕐
forall a b. a -> b -> a
const ℕ64 -> 𝕐
DVar) ((ℕ64 -> 𝕏 -> 𝕐) -> 𝕏 -> ℕ64 -> 𝕐
forall a b c. (a -> b -> c) -> b -> a -> c
flip ℕ64 -> 𝕏 -> 𝕐
NVar) 𝑂 𝕏
xO ℕ64
n'
        Bool -> (() -> SubstM s e ()) -> SubstM s e ()
forall (m :: * -> *). Return m => Bool -> (() -> m ()) -> m ()
when (FreeVarsAction s -> s -> 𝕐 -> Bool
forall s. FreeVarsAction s -> s -> 𝕐 -> Bool
freeVarsActionFilter FreeVarsAction s
𝒶 s
s 𝕐
y) ((() -> SubstM s e ()) -> SubstM s e ())
-> (() -> SubstM s e ()) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ \ () → 
          (s ⇰ 𝑃 𝕐) -> SubstM s e ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell ((s ⇰ 𝑃 𝕐) -> SubstM s e ()) -> (s ⇰ 𝑃 𝕐) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑃 𝕐 -> s ⇰ 𝑃 𝕐
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕐 -> 𝑃 𝕐
forall a t. Single a t => a -> t
single 𝕐
y
      e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> e
𝓋 ℕ64
n
    SubSubstEnv SubstAction s e
𝒶 → do
      let 𝓈s :: (s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e
𝓈s = GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e
forall s₁ s₂ e. GSubst s₁ s₂ e -> s₂ ⇰ DSubst s₂ e
gsubstSubst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubst (Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ SubstAction s e -> Subst s e
forall s e. SubstAction s e -> Subst s e
substActionSubst SubstAction s e
𝒶
      case (s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e
𝓈s ((s ∧ 𝑂 𝕏) ⇰ DSubst (s ∧ 𝑂 𝕏) e)
-> (s ∧ 𝑂 𝕏) -> 𝑂 (DSubst (s ∧ 𝑂 𝕏) e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> 𝑂 𝕏 -> s ∧ 𝑂 𝕏
forall a b. a -> b -> a ∧ b
:* 𝑂 𝕏
xO) of
        𝑂 (DSubst (s ∧ 𝑂 𝕏) e)
None → e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> e
𝓋 ℕ64
n
        Some DSubst (s ∧ 𝑂 𝕏) e
𝓈 → case DSubst (s ∧ 𝑂 𝕏) e -> ℕ64 -> SSubstElem (s ∧ 𝑂 𝕏) e
forall 𝑠 e. DSubst 𝑠 e -> ℕ64 -> SSubstElem 𝑠 e
dsubstVar DSubst (s ∧ 𝑂 𝕏) e
𝓈 ℕ64
n of
          Var_SSE ℕ64
n' → e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> e
𝓋 ℕ64
n'
          Trm_SSE (SubstElem (s ∧ 𝑂 𝕏) ⇰ ℕ64
𝑠 () -> 𝑂 e
ueO) → 𝑂 e -> SubstM s e e
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 e -> SubstM s e e) -> 𝑂 e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG (s ∧ 𝑂 𝕏) ⇰ ℕ64
𝑠) (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ () -> 𝑂 e
ueO ()

substyDVar ∷ (Ord s,Substy s e e) ⇒ s → (ℕ64 → e) → ℕ64 → SubstM s e e
substyDVar :: forall s e.
(Ord s, Substy s e e) =>
s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
substyDVar = 𝑂 𝕏 -> s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
forall s e.
(Ord s, Substy s e e) =>
𝑂 𝕏 -> s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
substyVar 𝑂 𝕏
forall a. 𝑂 a
None

substyNVar ∷ (Ord s,Substy s e e) ⇒ s → (ℕ64 → e) → 𝕏 → ℕ64 → SubstM s e e
substyNVar :: forall s e.
(Ord s, Substy s e e) =>
s -> (ℕ64 -> e) -> 𝕏 -> ℕ64 -> SubstM s e e
substyNVar s
s ℕ64 -> e
𝓋 𝕏
x = 𝑂 𝕏 -> s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
forall s e.
(Ord s, Substy s e e) =>
𝑂 𝕏 -> s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
substyVar (𝕏 -> 𝑂 𝕏
forall a. a -> 𝑂 a
Some 𝕏
x) s
s ℕ64 -> e
𝓋

substyGVar ∷ (Ord s,Substy s e e) ⇒ s → (𝕏 → e) → 𝕏 → SubstM s e e
substyGVar :: forall s e.
(Ord s, Substy s e e) =>
s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e
substyGVar s
s 𝕏 -> e
𝓋 𝕏
x = do
  SubstEnv s e
γ ← SubstM s e (SubstEnv s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case SubstEnv s e
γ of
    FVsSubstEnv FreeVarsAction s
𝒶 → do
      let y :: 𝕐
y = 𝕏 -> 𝕐
GVar 𝕏
x
      Bool -> (() -> SubstM s e ()) -> SubstM s e ()
forall (m :: * -> *). Return m => Bool -> (() -> m ()) -> m ()
when (FreeVarsAction s -> s -> 𝕐 -> Bool
forall s. FreeVarsAction s -> s -> 𝕐 -> Bool
freeVarsActionFilter FreeVarsAction s
𝒶 s
s 𝕐
y) ((() -> SubstM s e ()) -> SubstM s e ())
-> (() -> SubstM s e ()) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ \ () → 
        (s ⇰ 𝑃 𝕐) -> SubstM s e ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell ((s ⇰ 𝑃 𝕐) -> SubstM s e ()) -> (s ⇰ 𝑃 𝕐) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑃 𝕐 -> s ⇰ 𝑃 𝕐
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕐 -> 𝑃 𝕐
forall a t. Single a t => a -> t
single 𝕐
y
      e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ 𝕏 -> e
𝓋 𝕏
x
    SubSubstEnv SubstAction s e
𝓈A → do
      let gsᴳ :: (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
gsᴳ =  GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
forall s₁ s₂ e. GSubst s₁ s₂ e -> s₁ ⇰ SubstElem s₂ e
gsubstGVars (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubst (Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ SubstAction s e -> Subst s e
forall s e. SubstAction s e -> Subst s e
substActionSubst SubstAction s e
𝓈A
      case (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
gsᴳ ((s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e)
-> (s ∧ 𝕏) -> 𝑂 (SubstElem (s ∧ 𝑂 𝕏) e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> 𝕏 -> s ∧ 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏
x) of
        𝑂 (SubstElem (s ∧ 𝑂 𝕏) e)
None → e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ 𝕏 -> e
𝓋 𝕏
x
        Some (SubstElem (s ∧ 𝑂 𝕏) ⇰ ℕ64
𝑠 () -> 𝑂 e
ueO) → 𝑂 e -> SubstM s e e
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 e -> SubstM s e e) -> 𝑂 e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG (s ∧ 𝑂 𝕏) ⇰ ℕ64
𝑠) (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ () -> 𝑂 e
ueO ()

substyMVar ∷ (Ord s,Substy s e e) ⇒ s → (𝕏 → e) → 𝕏 → SubstM s e e
substyMVar :: forall s e.
(Ord s, Substy s e e) =>
s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e
substyMVar s
s 𝕏 -> e
𝓋 𝕏
x = do
  SubstEnv s e
γ ← SubstM s e (SubstEnv s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case SubstEnv s e
γ of
    FVsSubstEnv FreeVarsAction s
𝒶 → do
      let y :: 𝕐
y = 𝕏 -> 𝕐
MVar 𝕏
x
      Bool -> (() -> SubstM s e ()) -> SubstM s e ()
forall (m :: * -> *). Return m => Bool -> (() -> m ()) -> m ()
when (FreeVarsAction s -> s -> 𝕐 -> Bool
forall s. FreeVarsAction s -> s -> 𝕐 -> Bool
freeVarsActionFilter FreeVarsAction s
𝒶 s
s 𝕐
y) ((() -> SubstM s e ()) -> SubstM s e ())
-> (() -> SubstM s e ()) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ \ () → 
        (s ⇰ 𝑃 𝕐) -> SubstM s e ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell ((s ⇰ 𝑃 𝕐) -> SubstM s e ()) -> (s ⇰ 𝑃 𝕐) -> SubstM s e ()
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑃 𝕐 -> s ⇰ 𝑃 𝕐
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝕐 -> 𝑃 𝕐
forall a t. Single a t => a -> t
single 𝕐
y
      e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ 𝕏 -> e
𝓋 𝕏
x
    SubSubstEnv SubstAction s e
𝓈A → do
      let gsᴹ :: (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
gsᴹ =  GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
forall s₁ s₂ e. GSubst s₁ s₂ e -> s₁ ⇰ SubstElem s₂ e
gsubstMetas (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s e. Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
unSubst (Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e)
-> Subst s e -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall a b. (a -> b) -> a -> b
$ SubstAction s e -> Subst s e
forall s e. SubstAction s e -> Subst s e
substActionSubst SubstAction s e
𝓈A
      case (s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e
gsᴹ ((s ∧ 𝕏) ⇰ SubstElem (s ∧ 𝑂 𝕏) e)
-> (s ∧ 𝕏) -> 𝑂 (SubstElem (s ∧ 𝑂 𝕏) e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> 𝕏 -> s ∧ 𝕏
forall a b. a -> b -> a ∧ b
:* 𝕏
x) of
        𝑂 (SubstElem (s ∧ 𝑂 𝕏) e)
None → e -> SubstM s e e
forall a. a -> SubstM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstM s e e) -> e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ 𝕏 -> e
𝓋 𝕏
x
        Some (SubstElem (s ∧ 𝑂 𝕏) ⇰ ℕ64
𝑠 () -> 𝑂 e
ueO) → 𝑂 e -> SubstM s e e
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 e -> SubstM s e e) -> 𝑂 e -> SubstM s e e
forall a b. (a -> b) -> a -> b
$ Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall s e. GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
Subst (GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e)
-> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ 𝑂 𝕏) ⇰ ℕ64) -> GSubst (s ∧ 𝕏) (s ∧ 𝑂 𝕏) e
forall s₂ s₁ e. (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e
𝓈introG (s ∧ 𝑂 𝕏) ⇰ ℕ64
𝑠) (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ () -> 𝑂 e
ueO ()

substy𝕐 ∷ (Ord s,Substy s e e) ⇒ s → (𝕐 → e) → 𝕐 → SubstM s e e
substy𝕐 :: forall s e.
(Ord s, Substy s e e) =>
s -> (𝕐 -> e) -> 𝕐 -> SubstM s e e
substy𝕐 s
s 𝕐 -> e
𝓋 = \case
  DVar ℕ64
n   → s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
forall s e.
(Ord s, Substy s e e) =>
s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e
substyDVar s
s (𝕐 -> e
𝓋 (𝕐 -> e) -> (ℕ64 -> 𝕐) -> ℕ64 -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℕ64 -> 𝕐
DVar)          ℕ64
n
  NVar ℕ64
n 𝕏
x → s -> (ℕ64 -> e) -> 𝕏 -> ℕ64 -> SubstM s e e
forall s e.
(Ord s, Substy s e e) =>
s -> (ℕ64 -> e) -> 𝕏 -> ℕ64 -> SubstM s e e
substyNVar s
s (𝕐 -> e
𝓋 (𝕐 -> e) -> (ℕ64 -> 𝕐) -> ℕ64 -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (ℕ64 -> 𝕏 -> 𝕐) -> 𝕏 -> ℕ64 -> 𝕐
forall a b c. (a -> b -> c) -> b -> a -> c
flip ℕ64 -> 𝕏 -> 𝕐
NVar 𝕏
x) 𝕏
x ℕ64
n
  GVar   𝕏
x → s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e
forall s e.
(Ord s, Substy s e e) =>
s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e
substyGVar s
s (𝕐 -> e
𝓋 (𝕐 -> e) -> (𝕏 -> 𝕐) -> 𝕏 -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕏 -> 𝕐
GVar)        𝕏
x
  MVar   𝕏
x → s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e
forall s e.
(Ord s, Substy s e e) =>
s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e
substyMVar s
s (𝕐 -> e
𝓋 (𝕐 -> e) -> (𝕏 -> 𝕐) -> 𝕏 -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕏 -> 𝕐
MVar)        𝕏
x