module UVMHS.Lib.Substitution.Subst where

import UVMHS.Core
import UVMHS.Lib.Pretty
import UVMHS.Lib.Fuzzy
import UVMHS.Lib.Shrinky

import UVMHS.Lib.Substitution.Name
import UVMHS.Lib.Substitution.SubstElem
import UVMHS.Lib.Substitution.SubstScoped
import UVMHS.Lib.Substitution.SubstSpaced
import UVMHS.Lib.Substitution.Var

-- ===== --
-- SUBST --
-- ===== --

--------------------------------------------------------------------------------
-- Instances for `Null`, `Append` and `Monoid` are defined in the `Substy`
-- module.
--
-- If semantically you want to achieve "apply substitution 𝓈₁ to substitution
-- 𝓈₂", this can be done using those instances, simply by `𝓈₁ ⧺ 𝓈₂`, which is
-- also semantically equivalent to `subst 𝓈₁ ∘ subst 𝓈₂`.
--
-- See documentation for `SubstSpaced` for notes about how it is instantiated
-- in this context.
--------------------------------------------------------------------------------

newtype Subst s e = Subst { forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst ∷ SubstSpaced (s ∧ Name) (s ∧ SName) 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,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,(forall a b. (a -> b) -> Subst s a -> Subst s b)
-> Functor (Subst s)
forall a b. (a -> b) -> Subst s a -> Subst s b
forall s a b. (a -> b) -> Subst s a -> Subst s b
forall (t :: * -> *).
(forall a b. (a -> b) -> t a -> t b) -> Functor t
$cmap :: forall s a b. (a -> b) -> Subst s a -> Subst s b
map :: forall a b. (a -> b) -> Subst s a -> Subst s b
Functor,Subst s e -> 𝐼 (Subst s e)
(Subst s e -> 𝐼 (Subst s e)) -> Shrinky (Subst s e)
forall a. (a -> 𝐼 a) -> Shrinky a
forall s e. (Ord s, Shrinky e) => Subst s e -> 𝐼 (Subst s e)
$cshrink :: forall s e. (Ord s, Shrinky e) => Subst s e -> 𝐼 (Subst s e)
shrink :: Subst s e -> 𝐼 (Subst s e)
Shrinky)
makeLenses ''Subst

isNullSubst ∷ (Ord s) ⇒ Subst s e → 𝔹
isNullSubst :: forall s e. Ord s => Subst s e -> Bool
isNullSubst = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Bool
forall sS sG e. Ord sS => SubstSpaced sG sS e -> Bool
isNullSubstSpaced (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Bool)
-> (Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> Subst s e
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst

wfSubst ∷ (Ord s) ⇒ Subst s e → 𝔹
wfSubst :: forall s e. Ord s => Subst s e -> Bool
wfSubst = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Bool
forall sS sG e. Ord sS => SubstSpaced sG sS e -> Bool
wfSubstSpaced (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Bool)
-> (Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> Subst s e
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst

canonSubstWith ∷ (Ord s,Eq e) ⇒ (s ∧ SName → e ⌲ DVar) → (s ∧ SName ⇰ ℕ64 → e → 𝑂 e) → (e → e) → Subst s e → Subst s e
canonSubstWith :: forall s e.
(Ord s, Eq e) =>
((s ∧ SName) -> e ⌲ DVar)
-> (((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> Subst s e
-> Subst s e
canonSubstWith (s ∧ SName) -> e ⌲ DVar
ℓvar ((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e
intro e -> e
canonE (Subst SubstSpaced (s ∧ Name) (s ∧ SName) e
𝓈) = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) -> e ⌲ DVar)
-> (((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS e sG.
(Ord sS, Eq e) =>
(sS -> e ⌲ DVar)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
canonSubstSpaced (s ∧ SName) -> e ⌲ DVar
ℓvar ((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e
intro e -> e
canonE SubstSpaced (s ∧ Name) (s ∧ SName) e
𝓈

---------------------
-- SHIFT DE BRUIJN --
---------------------

dshiftsSubst ∷ (Ord s) ⇒ s ⇰ ℕ64 → Subst s e → Subst s e
dshiftsSubst :: forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e
dshiftsSubst = (Subst s e ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> (SubstSpaced (s ∧ Name) (s ∧ SName) e
    -> SubstSpaced (s ∧ Name) (s ∧ SName) 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 ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubstL ((SubstSpaced (s ∧ Name) (s ∧ SName) e
  -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
 -> Subst s e -> Subst s e)
-> (((s ∧ SName) ⇰ ℕ64)
    -> SubstSpaced (s ∧ Name) (s ∧ SName) e
    -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ SName) ⇰ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ SName) ⇰ ℕ64)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS sG e.
Ord sS =>
(sS ⇰ ℕ64) -> SubstSpaced sG sS e -> SubstSpaced sG sS e
shiftSubstSpaced (((s ∧ SName) ⇰ ℕ64) -> Subst s e -> Subst s e)
-> (𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> 𝐼 ((s ∧ SName) ∧ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ SName) ∧ ℕ64) -> Subst s e -> Subst s e)
-> (𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64))
-> 𝐼 (s ∧ ℕ64)
-> Subst s e
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64)
-> 𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s -> s ∧ SName) -> (s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((s -> s ∧ SName) -> (s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64)
-> (s -> s ∧ SName) -> (s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64
forall a b. (a -> b) -> a -> b
$ (s -> SName -> s ∧ SName) -> SName -> s -> s ∧ SName
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
(:*) SName
D_SName) (𝐼 (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

dshiftSubst ∷ (Ord s) ⇒ s → ℕ64 → Subst s e → Subst s e
dshiftSubst :: forall s e. Ord s => s -> ℕ64 -> Subst s e -> Subst s e
dshiftSubst s
x ℕ64
ρ = (s ⇰ ℕ64) -> Subst s e -> Subst s e
forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e
dshiftsSubst ((s ⇰ ℕ64) -> Subst s e -> Subst s e)
-> (s ⇰ ℕ64) -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
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
ρ

--------------------
-- INTRO DE BRUIJN --
--------------------

dintrosSubst ∷ (Ord s) ⇒ s ⇰ ℕ64 → Subst s e
dintrosSubst :: forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e
dintrosSubst = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> (((s ∧ SName) ⇰ ℕ64) -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ SName) ⇰ ℕ64)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ SName) ⇰ ℕ64) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS sG e. (sS ⇰ ℕ64) -> SubstSpaced sG sS e
introSubstSpaced (((s ∧ SName) ⇰ ℕ64) -> Subst s e)
-> (𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> 𝐼 ((s ∧ SName) ∧ ℕ64)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ SName) ∧ ℕ64) -> Subst s e)
-> (𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64))
-> 𝐼 (s ∧ ℕ64)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64)
-> 𝐼 (s ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s -> s ∧ SName) -> (s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((s -> s ∧ SName) -> (s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64)
-> (s -> s ∧ SName) -> (s ∧ ℕ64) -> (s ∧ SName) ∧ ℕ64
forall a b. (a -> b) -> a -> b
$ (s -> SName -> s ∧ SName) -> SName -> s -> s ∧ SName
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
(:*) SName
D_SName) (𝐼 (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

dintroSubst ∷ (Ord s) ⇒ s → ℕ64 → Subst s e
dintroSubst :: forall s e. Ord s => s -> ℕ64 -> Subst s e
dintroSubst s
s ℕ64
ι = (s ⇰ ℕ64) -> Subst s e
forall s e. Ord s => (s ⇰ ℕ64) -> Subst s e
dintrosSubst ((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
ι

--------------------
-- BIND DE BRUIJN --
--------------------

dbindsSubst ∷ (Ord s) ⇒ s ⇰ 𝕍 e → Subst s e
dbindsSubst :: forall s e. Ord s => (s ⇰ 𝕍 e) -> Subst s e
dbindsSubst = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> (((s ∧ SName) ⇰ 𝕍 e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ SName) ⇰ 𝕍 e)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ SName) ⇰ 𝕍 e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS e sG. (sS ⇰ 𝕍 e) -> SubstSpaced sG sS e
sbindsSubstSpaced (((s ∧ SName) ⇰ 𝕍 e) -> Subst s e)
-> (𝐼 ((s ∧ SName) ∧ 𝕍 e) -> (s ∧ SName) ⇰ 𝕍 e)
-> 𝐼 ((s ∧ SName) ∧ 𝕍 e)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 ((s ∧ SName) ∧ 𝕍 e) -> (s ∧ SName) ⇰ 𝕍 e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ SName) ∧ 𝕍 e) -> Subst s e)
-> (𝐼 (s ∧ 𝕍 e) -> 𝐼 ((s ∧ SName) ∧ 𝕍 e))
-> 𝐼 (s ∧ 𝕍 e)
-> Subst s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ∧ 𝕍 e) -> (s ∧ SName) ∧ 𝕍 e)
-> 𝐼 (s ∧ 𝕍 e) -> 𝐼 ((s ∧ SName) ∧ 𝕍 e)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((s -> s ∧ SName) -> (s ∧ 𝕍 e) -> (s ∧ SName) ∧ 𝕍 e
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((s -> s ∧ SName) -> (s ∧ 𝕍 e) -> (s ∧ SName) ∧ 𝕍 e)
-> (s -> s ∧ SName) -> (s ∧ 𝕍 e) -> (s ∧ SName) ∧ 𝕍 e
forall a b. (a -> b) -> a -> b
$ (s -> SName -> s ∧ SName) -> SName -> s -> s ∧ SName
forall a b c. (a -> b -> c) -> b -> a -> c
flip s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
(:*) SName
D_SName) (𝐼 (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

dbindSubst ∷ (Ord s) ⇒ s → e → Subst s e
dbindSubst :: forall s e. Ord s => s -> e -> Subst s e
dbindSubst s
s e
e = (s ⇰ 𝕍 e) -> Subst s e
forall s e. Ord s => (s ⇰ 𝕍 e) -> Subst s e
dbindsSubst ((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

-----------------
-- SHIFT NAMED --
-----------------

nshiftsSubst ∷ (Ord s) ⇒ s ⇰ Name ⇰ ℕ64 → Subst s e → Subst s e
nshiftsSubst :: forall s e. Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e
nshiftsSubst s ⇰ (Name ⇰ ℕ64)
ρ = (Subst s e ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> (SubstSpaced (s ∧ Name) (s ∧ SName) e
    -> SubstSpaced (s ∧ Name) (s ∧ SName) 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 ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e ⟢ SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubstL ((SubstSpaced (s ∧ Name) (s ∧ SName) e
  -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
 -> Subst s e -> Subst s e)
-> (SubstSpaced (s ∧ Name) (s ∧ SName) e
    -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> Subst s e
-> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) ⇰ ℕ64)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS sG e.
Ord sS =>
(sS ⇰ ℕ64) -> SubstSpaced sG sS e -> SubstSpaced sG sS e
shiftSubstSpaced (((s ∧ SName) ⇰ ℕ64)
 -> SubstSpaced (s ∧ Name) (s ∧ SName) e
 -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ SName) ⇰ ℕ64)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> 𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall a b. (a -> b) -> a -> b
$ do
  s
s :* Name ⇰ ℕ64
xns ← (s ⇰ (Name ⇰ ℕ64)) -> 𝐼 (s ∧ (Name ⇰ ℕ64))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (Name ⇰ ℕ64)
ρ
  Name
x :* ℕ64
n ← (Name ⇰ ℕ64) -> 𝐼 (Name ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter Name ⇰ ℕ64
xns
  ((s ∧ SName) ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ SName) ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64))
-> ((s ∧ SName) ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a b. (a -> b) -> a -> b
$ s
s s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
:* Name -> SName
N_SName Name
x (s ∧ SName) -> ℕ64 -> (s ∧ SName) ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
n

nshiftSubst ∷ (Ord s) ⇒ s → Name → ℕ64 → Subst s e → Subst s e
nshiftSubst :: forall s e. Ord s => s -> Name -> ℕ64 -> Subst s e -> Subst s e
nshiftSubst s
s Name
x ℕ64
ρ = (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e
forall s e. Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e
nshiftsSubst ((s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e)
-> (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (Name ⇰ ℕ64) -> s ⇰ (Name ⇰ ℕ64)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ Name
x Name -> ℕ64 -> Name ⇰ ℕ64
forall a. Name -> a -> Name ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
ρ

-----------------
-- INTRO NAMED --
-----------------

nintrosSubst ∷ (Ord s) ⇒ s ⇰ Name ⇰ ℕ64 → Subst s e
nintrosSubst :: forall s e. Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e
nintrosSubst s ⇰ (Name ⇰ ℕ64)
ι = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) ⇰ ℕ64) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS sG e. (sS ⇰ ℕ64) -> SubstSpaced sG sS e
introSubstSpaced (((s ∧ SName) ⇰ ℕ64) -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ SName) ⇰ ℕ64) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> 𝐼 ((s ∧ SName) ∧ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall a b. (a -> b) -> a -> b
$ do
  s
s :* Name ⇰ ℕ64
xns ← (s ⇰ (Name ⇰ ℕ64)) -> 𝐼 (s ∧ (Name ⇰ ℕ64))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (Name ⇰ ℕ64)
ι
  Name
x :* ℕ64
n ← (Name ⇰ ℕ64) -> 𝐼 (Name ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter Name ⇰ ℕ64
xns
  ((s ∧ SName) ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ SName) ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64))
-> ((s ∧ SName) ∧ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a b. (a -> b) -> a -> b
$ s
s s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
:* Name -> SName
N_SName Name
x (s ∧ SName) -> ℕ64 -> (s ∧ SName) ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
n

nintroSubst ∷ (Ord s) ⇒ s → Name → ℕ64 → Subst s e
nintroSubst :: forall s e. Ord s => s -> Name -> ℕ64 -> Subst s e
nintroSubst s
s Name
x ℕ64
ι = (s ⇰ (Name ⇰ ℕ64)) -> Subst s e
forall s e. Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e
nintrosSubst ((s ⇰ (Name ⇰ ℕ64)) -> Subst s e)
-> (s ⇰ (Name ⇰ ℕ64)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (Name ⇰ ℕ64) -> s ⇰ (Name ⇰ ℕ64)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ Name
x Name -> ℕ64 -> Name ⇰ ℕ64
forall a. Name -> a -> Name ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
ι

-------------------
----------------
-- BIND NAMED --
----------------

nbindsSubst ∷ (Ord s) ⇒ s ⇰ Name ⇰ 𝕍 e → Subst s e
nbindsSubst :: forall s e. Ord s => (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e
nbindsSubst s ⇰ (Name ⇰ 𝕍 e)
swes = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) ⇰ 𝕍 e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS e sG. (sS ⇰ 𝕍 e) -> SubstSpaced sG sS e
sbindsSubstSpaced (((s ∧ SName) ⇰ 𝕍 e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ SName) ⇰ 𝕍 e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ SName) ∧ 𝕍 e) -> (s ∧ SName) ⇰ 𝕍 e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ SName) ∧ 𝕍 e) -> (s ∧ SName) ⇰ 𝕍 e)
-> 𝐼 ((s ∧ SName) ∧ 𝕍 e) -> (s ∧ SName) ⇰ 𝕍 e
forall a b. (a -> b) -> a -> b
$ do
  s
s :* Name ⇰ 𝕍 e
xess ← (s ⇰ (Name ⇰ 𝕍 e)) -> 𝐼 (s ∧ (Name ⇰ 𝕍 e))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (Name ⇰ 𝕍 e)
swes
  Name
x :* 𝕍 e
es ← (Name ⇰ 𝕍 e) -> 𝐼 (Name ∧ 𝕍 e)
forall a t. ToIter a t => t -> 𝐼 a
iter Name ⇰ 𝕍 e
xess
  ((s ∧ SName) ∧ 𝕍 e) -> 𝐼 ((s ∧ SName) ∧ 𝕍 e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ SName) ∧ 𝕍 e) -> 𝐼 ((s ∧ SName) ∧ 𝕍 e))
-> ((s ∧ SName) ∧ 𝕍 e) -> 𝐼 ((s ∧ SName) ∧ 𝕍 e)
forall a b. (a -> b) -> a -> b
$ s
s s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
:* Name -> SName
N_SName Name
x (s ∧ SName) -> 𝕍 e -> (s ∧ SName) ∧ 𝕍 e
forall a b. a -> b -> a ∧ b
:* 𝕍 e
es

nbindSubst ∷ (Ord s) ⇒ s → Name → e → Subst s e
nbindSubst :: forall s e. Ord s => s -> Name -> e -> Subst s e
nbindSubst s
s Name
x e
e = (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e
forall s e. Ord s => (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e
nbindsSubst ((s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e)
-> (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (Name ⇰ 𝕍 e) -> s ⇰ (Name ⇰ 𝕍 e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ Name
x Name -> 𝕍 e -> Name ⇰ 𝕍 e
forall a. Name -> a -> Name ⇰ 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

-----------------
-- BIND GLOBAL --
-----------------

gbindsSubst ∷ (Ord s) ⇒ s ⇰ Name ⇰ e → Subst s e
gbindsSubst :: forall s e. Ord s => (s ⇰ (Name ⇰ e)) -> Subst s e
gbindsSubst s ⇰ (Name ⇰ e)
sxes = SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ Name) ⇰ e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sG e sS. (sG ⇰ e) -> SubstSpaced sG sS e
ubindsSubstSpaced (((s ∧ Name) ⇰ e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> ((s ∧ Name) ⇰ e) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ Name) ∧ e) -> (s ∧ Name) ⇰ e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ Name) ∧ e) -> (s ∧ Name) ⇰ e)
-> 𝐼 ((s ∧ Name) ∧ e) -> (s ∧ Name) ⇰ e
forall a b. (a -> b) -> a -> b
$ do
  s
s :* Name ⇰ e
xes ← (s ⇰ (Name ⇰ e)) -> 𝐼 (s ∧ (Name ⇰ e))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (Name ⇰ e)
sxes
  Name
x :* e
e ← (Name ⇰ e) -> 𝐼 (Name ∧ e)
forall a t. ToIter a t => t -> 𝐼 a
iter Name ⇰ e
xes
  ((s ∧ Name) ∧ e) -> 𝐼 ((s ∧ Name) ∧ e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ Name) ∧ e) -> 𝐼 ((s ∧ Name) ∧ e))
-> ((s ∧ Name) ∧ e) -> 𝐼 ((s ∧ Name) ∧ e)
forall a b. (a -> b) -> a -> b
$ s
s s -> Name -> s ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
x (s ∧ Name) -> e -> (s ∧ Name) ∧ e
forall a b. a -> b -> a ∧ b
:* e
e

gbindSubst ∷ (Ord s) ⇒ s → Name → e → Subst s e
gbindSubst :: forall s e. Ord s => s -> Name -> e -> Subst s e
gbindSubst s
s Name
x e
e = (s ⇰ (Name ⇰ e)) -> Subst s e
forall s e. Ord s => (s ⇰ (Name ⇰ e)) -> Subst s e
gbindsSubst ((s ⇰ (Name ⇰ e)) -> Subst s e) -> (s ⇰ (Name ⇰ e)) -> Subst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (Name ⇰ e) -> s ⇰ (Name ⇰ e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ Name
x Name -> e -> Name ⇰ e
forall a. Name -> a -> Name ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e
e

------------
-- PRETTY --
------------

instance ∀ s e. (Ord s,Pretty s,Pretty e) ⇒ Pretty (Subst s e) where
  pretty ∷ Subst s e → Doc
  pretty :: Subst s e -> Doc
pretty (Subst (SubstSpaced (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈G (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
𝓈S)) = 
    let sD ∷ s ∧ SName ⇰ ℕ64 → Doc
        sD :: ((s ∧ SName) ⇰ ℕ64) -> Doc
sD (s ∧ SName) ⇰ ℕ64
sιs = (s ⇰ Doc) -> Doc
forall a. Pretty a => a -> Doc
pretty ((s ⇰ Doc) -> Doc) -> (s ⇰ Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (𝐼 Doc -> Doc) -> (s ⇰ 𝐼 Doc) -> s ⇰ Doc
forall a b. (a -> b) -> (s ⇰ a) -> s ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppSet ((s ⇰ 𝐼 Doc) -> s ⇰ Doc) -> (s ⇰ 𝐼 Doc) -> s ⇰ Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 (s ⇰ 𝐼 Doc) -> s ⇰ 𝐼 Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (s ⇰ 𝐼 Doc) -> s ⇰ 𝐼 Doc) -> 𝐼 (s ⇰ 𝐼 Doc) -> s ⇰ 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ SName) ∧ ℕ64)
-> (((s ∧ SName) ∧ ℕ64) -> s ⇰ 𝐼 Doc) -> 𝐼 (s ⇰ 𝐼 Doc)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (((s ∧ SName) ⇰ ℕ64) -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter (s ∧ SName) ⇰ ℕ64
sιs) ((((s ∧ SName) ∧ ℕ64) -> s ⇰ 𝐼 Doc) -> 𝐼 (s ⇰ 𝐼 Doc))
-> (((s ∧ SName) ∧ ℕ64) -> s ⇰ 𝐼 Doc) -> 𝐼 (s ⇰ 𝐼 Doc)
forall a b. (a -> b) -> a -> b
$ \ (s
s :* SName
xO :* ℕ64
n) → 
          s -> 𝐼 Doc -> s ⇰ 𝐼 Doc
forall k a. k -> a -> k ⇰ a
(↦♭) s
s (𝐼 Doc -> s ⇰ 𝐼 Doc) -> 𝐼 Doc -> s ⇰ 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝐼 Doc
forall a. a -> 𝐼 a
single𝐼 (Doc -> 𝐼 Doc) -> Doc -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ 
            case SName
xO of
            SName
D_SName → [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊 -> Doc
ppPun 𝕊
"⇈",ℕ64 -> Doc
forall a. Pretty a => a -> Doc
pretty ℕ64
n]
            N_SName Name
x → [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊 -> Doc
ppBdr (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> 𝕊
forall a. Pretty a => a -> 𝕊
ppshow Name
x,𝕊 -> Doc
ppPun 𝕊
"⇈",ℕ64 -> Doc
forall a. Pretty a => a -> Doc
pretty ℕ64
n]
        xD ∷ SName → DVarInf → Doc
        xD :: SName -> DVarInf -> Doc
xD SName
xO DVarInf
n = case SName
xO of
          SName
D_SName → DVarInf -> Doc
forall a. Pretty a => a -> Doc
pretty DVarInf
n
          N_SName Name
x → NVarInf -> Doc
forall a. Pretty a => a -> Doc
pretty (NVarInf -> Doc) -> NVarInf -> Doc
forall a b. (a -> b) -> a -> b
$ DVarInf -> Name -> NVarInf
NVarInf DVarInf
n Name
x
    in 
    (s ⇰ Doc) -> Doc
forall a. Pretty a => a -> Doc
pretty ((s ⇰ Doc) -> Doc) -> (s ⇰ Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ (𝐼 (Doc ∧ Doc) -> Doc) -> (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ Doc
forall a b. (a -> b) -> (s ⇰ a) -> s ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝐼 (Doc ∧ Doc) -> Doc
forall t. ToIter (Doc ∧ Doc) t => t -> Doc
ppDict ((s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ Doc) -> (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ Doc
forall a b. (a -> b) -> a -> b
$ [s ⇰ 𝐼 (Doc ∧ Doc)] -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ if ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈G ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 then s ⇰ 𝐼 (Doc ∧ Doc)
forall a. Null a => a
null else 
          𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
-> (((s ∧ Name) ∧ SubstElem (s ∧ SName) e) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (((s ∧ Name) ⇰ SubstElem (s ∧ SName) e)
-> 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
forall a t. ToIter a t => t -> 𝐼 a
iter (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈G) ((((s ∧ Name) ∧ SubstElem (s ∧ SName) e) -> s ⇰ 𝐼 (Doc ∧ Doc))
 -> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)))
-> (((s ∧ Name) ∧ SubstElem (s ∧ SName) e) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc))
forall a b. (a -> b) -> a -> b
$ \ ((s
s :* Name
x) :* SubstElem (s ∧ SName) e
e) →
            s -> 𝐼 (Doc ∧ Doc) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall k a. k -> a -> k ⇰ a
(↦♭) s
s (𝐼 (Doc ∧ Doc) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (Doc ∧ Doc) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ (Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a. a -> 𝐼 a
single𝐼 ((Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)) -> (Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ 
              ([Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊 -> Doc
ppBdr (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ Name -> 𝕊
forall a. Pretty a => a -> 𝕊
ppshow Name
x,𝕊 -> Doc
ppPun 𝕊
":",𝕊 -> Doc
ppPun 𝕊
"g"]) 
              Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* 
              ((((s ∧ SName) ⇰ ℕ64) -> Doc) -> SubstElem (s ∧ SName) e -> Doc
forall e s. Pretty e => ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc
ppSubstElemNamed ((s ∧ SName) ⇰ ℕ64) -> Doc
sD SubstElem (s ∧ SName) e
e)
      , if ((s ∧ SName) ⇰ SubstScoped (s ∧ SName) e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
𝓈S ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 then s ⇰ 𝐼 (Doc ∧ Doc)
forall a. Null a => a
null else 
          𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ SName) ∧ SubstScoped (s ∧ SName) e)
-> (((s ∧ SName) ∧ SubstScoped (s ∧ SName) e) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc))
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (((s ∧ SName) ⇰ SubstScoped (s ∧ SName) e)
-> 𝐼 ((s ∧ SName) ∧ SubstScoped (s ∧ SName) e)
forall a t. ToIter a t => t -> 𝐼 a
iter (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
𝓈S) ((((s ∧ SName) ∧ SubstScoped (s ∧ SName) e) -> s ⇰ 𝐼 (Doc ∧ Doc))
 -> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc)))
-> (((s ∧ SName) ∧ SubstScoped (s ∧ SName) e) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (s ⇰ 𝐼 (Doc ∧ Doc))
forall a b. (a -> b) -> a -> b
$ \ (s
s :* SName
xO :* SubstScoped (s ∧ SName) e
𝓈) →
            s -> 𝐼 (Doc ∧ Doc) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall k a. k -> a -> k ⇰ a
(↦♭) s
s (𝐼 (Doc ∧ Doc) -> s ⇰ 𝐼 (Doc ∧ Doc))
-> 𝐼 (Doc ∧ Doc) -> s ⇰ 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ (((s ∧ SName) ⇰ ℕ64) -> Doc)
-> (DVarInf -> Doc) -> SubstScoped (s ∧ SName) e -> 𝐼 (Doc ∧ Doc)
forall e s.
Pretty e =>
((s ⇰ ℕ64) -> Doc)
-> (DVarInf -> Doc) -> SubstScoped s e -> 𝐼 (Doc ∧ Doc)
ppSubstScopedWith ((s ∧ SName) ⇰ ℕ64) -> Doc
sD (SName -> DVarInf -> Doc
xD SName
xO) SubstScoped (s ∧ SName) e
𝓈
      ]

-- ========== --
-- META SUBST --
-- ========== --

newtype MetaSubst s e = MetaSubst { forall s e. MetaSubst s e -> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
unMetaSubst ∷ (s ∧ Name) ⇰ SubstElem (s ∧ SName) e }
  deriving (MetaSubst s e -> MetaSubst s e -> Bool
(MetaSubst s e -> MetaSubst s e -> Bool)
-> (MetaSubst s e -> MetaSubst s e -> Bool) -> Eq (MetaSubst s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e. (Eq s, Eq e) => MetaSubst s e -> MetaSubst s e -> Bool
$c== :: forall s e. (Eq s, Eq e) => MetaSubst s e -> MetaSubst s e -> Bool
== :: MetaSubst s e -> MetaSubst s e -> Bool
$c/= :: forall s e. (Eq s, Eq e) => MetaSubst s e -> MetaSubst s e -> Bool
/= :: MetaSubst s e -> MetaSubst s e -> Bool
Eq,Eq (MetaSubst s e)
Eq (MetaSubst s e) =>
(MetaSubst s e -> MetaSubst s e -> Ordering)
-> (MetaSubst s e -> MetaSubst s e -> Bool)
-> (MetaSubst s e -> MetaSubst s e -> Bool)
-> (MetaSubst s e -> MetaSubst s e -> Bool)
-> (MetaSubst s e -> MetaSubst s e -> Bool)
-> (MetaSubst s e -> MetaSubst s e -> MetaSubst s e)
-> (MetaSubst s e -> MetaSubst s e -> MetaSubst s e)
-> Ord (MetaSubst s e)
MetaSubst s e -> MetaSubst s e -> Bool
MetaSubst s e -> MetaSubst s e -> Ordering
MetaSubst s e -> MetaSubst s e -> MetaSubst 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 (MetaSubst s e)
forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Bool
forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Ordering
forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> MetaSubst s e
$ccompare :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Ordering
compare :: MetaSubst s e -> MetaSubst s e -> Ordering
$c< :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Bool
< :: MetaSubst s e -> MetaSubst s e -> Bool
$c<= :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Bool
<= :: MetaSubst s e -> MetaSubst s e -> Bool
$c> :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Bool
> :: MetaSubst s e -> MetaSubst s e -> Bool
$c>= :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> Bool
>= :: MetaSubst s e -> MetaSubst s e -> Bool
$cmax :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> MetaSubst s e
max :: MetaSubst s e -> MetaSubst s e -> MetaSubst s e
$cmin :: forall s e.
(Ord s, Ord e) =>
MetaSubst s e -> MetaSubst s e -> MetaSubst s e
min :: MetaSubst s e -> MetaSubst s e -> MetaSubst s e
Ord,Int -> MetaSubst s e -> ShowS
[MetaSubst s e] -> ShowS
MetaSubst s e -> String
(Int -> MetaSubst s e -> ShowS)
-> (MetaSubst s e -> String)
-> ([MetaSubst s e] -> ShowS)
-> Show (MetaSubst s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> MetaSubst s e -> ShowS
forall s e. (Show s, Show e) => [MetaSubst s e] -> ShowS
forall s e. (Show s, Show e) => MetaSubst s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> MetaSubst s e -> ShowS
showsPrec :: Int -> MetaSubst s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => MetaSubst s e -> String
show :: MetaSubst s e -> String
$cshowList :: forall s e. (Show s, Show e) => [MetaSubst s e] -> ShowS
showList :: [MetaSubst s e] -> ShowS
Show,MetaSubst s e -> Doc
(MetaSubst s e -> Doc) -> Pretty (MetaSubst s e)
forall a. (a -> Doc) -> Pretty a
forall s e. (Pretty s, Pretty e) => MetaSubst s e -> Doc
$cpretty :: forall s e. (Pretty s, Pretty e) => MetaSubst s e -> Doc
pretty :: MetaSubst s e -> Doc
Pretty,FuzzyM (MetaSubst s e)
FuzzyM (MetaSubst s e) -> Fuzzy (MetaSubst s e)
forall a. FuzzyM a -> Fuzzy a
forall s e. (Ord s, Fuzzy s, Fuzzy e) => FuzzyM (MetaSubst s e)
$cfuzzy :: forall s e. (Ord s, Fuzzy s, Fuzzy e) => FuzzyM (MetaSubst s e)
fuzzy :: FuzzyM (MetaSubst s e)
Fuzzy,MetaSubst s e -> 𝐼 (MetaSubst s e)
(MetaSubst s e -> 𝐼 (MetaSubst s e)) -> Shrinky (MetaSubst s e)
forall a. (a -> 𝐼 a) -> Shrinky a
forall s e.
(Ord s, Shrinky e) =>
MetaSubst s e -> 𝐼 (MetaSubst s e)
$cshrink :: forall s e.
(Ord s, Shrinky e) =>
MetaSubst s e -> 𝐼 (MetaSubst s e)
shrink :: MetaSubst s e -> 𝐼 (MetaSubst s e)
Shrinky)
makeLenses ''MetaSubst

----------
-- BIND --
----------

mbindsSubst ∷ (Ord s) ⇒ s ⇰ Name ⇰ e → MetaSubst s e
mbindsSubst :: forall s e. Ord s => (s ⇰ (Name ⇰ e)) -> MetaSubst s e
mbindsSubst s ⇰ (Name ⇰ e)
sxes = ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e) -> MetaSubst s e
forall s e. ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e) -> MetaSubst s e
MetaSubst (((s ∧ Name) ⇰ SubstElem (s ∧ SName) e) -> MetaSubst s e)
-> ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e) -> MetaSubst s e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
-> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
 -> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e)
-> 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
-> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ do
  s
s :* Name ⇰ e
xes ← (s ⇰ (Name ⇰ e)) -> 𝐼 (s ∧ (Name ⇰ e))
forall a t. ToIter a t => t -> 𝐼 a
iter s ⇰ (Name ⇰ e)
sxes
  Name
x :* e
e ← (Name ⇰ e) -> 𝐼 (Name ∧ e)
forall a t. ToIter a t => t -> 𝐼 a
iter Name ⇰ e
xes
  ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
-> 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
 -> 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e))
-> ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
-> 𝐼 ((s ∧ Name) ∧ SubstElem (s ∧ SName) e)
forall a b. (a -> b) -> a -> b
$ (s ∧ Name)
-> SubstElem (s ∧ SName) e -> (s ∧ Name) ∧ SubstElem (s ∧ SName) e
forall a b. a -> b -> a ∧ b
(:*) (s
s s -> Name -> s ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
x) (SubstElem (s ∧ SName) e -> (s ∧ Name) ∧ SubstElem (s ∧ SName) e)
-> SubstElem (s ∧ SName) e -> (s ∧ Name) ∧ SubstElem (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) ⇰ ℕ64) -> 𝑂 e -> SubstElem (s ∧ SName) e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem (s ∧ SName) ⇰ ℕ64
forall a. Null a => a
null (𝑂 e -> SubstElem (s ∧ SName) e) -> 𝑂 e -> SubstElem (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ e -> 𝑂 e
forall a. a -> 𝑂 a
Some e
e

mbindSubst ∷ (Ord s) ⇒ s → Name → e → MetaSubst s e
mbindSubst :: forall s e. Ord s => s -> Name -> e -> MetaSubst s e
mbindSubst s
s Name
x e
e = (s ⇰ (Name ⇰ e)) -> MetaSubst s e
forall s e. Ord s => (s ⇰ (Name ⇰ e)) -> MetaSubst s e
mbindsSubst ((s ⇰ (Name ⇰ e)) -> MetaSubst s e)
-> (s ⇰ (Name ⇰ e)) -> MetaSubst s e
forall a b. (a -> b) -> a -> b
$ s
s s -> (Name ⇰ e) -> s ⇰ (Name ⇰ e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ Name
x Name -> e -> Name ⇰ e
forall a. Name -> a -> Name ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ e
e