module UVMHS.Lib.Substitution.SubstSpaced where

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

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

-- =================================================================== --
-- (NAME)SPACED SUBSTITUTION (NAMED AND NAMELESS, SCOPED AND UNSCOPED) --
-- =================================================================== --

--------------------------------------------------------------------------------
-- `SubstSpaced` builds on `SubstScoped` and adds support for:
-- - namespaced scoped   nameless variables
-- - scoped   named variables
-- - unscoped named variables
--
-- The namespace parameters can be instantiated to easily recover named
-- variables. Conceptually a nameless substitution is a map `ℕ ⇰ Expr`. A well
-- behaved named substitution will also track a notion of nameless indices (see
-- example below), and so a named substitution is a map from `𝕎 ∧ ℕ ⇰ Expr`.
-- This can be restructued as `ℕ ⇰ 𝕎 ⇰ Expr`, and because `SubstSpaced` has a
-- generic structure `ℕ ⇰ s ⇰ Expr` for any `s`, we can just instantiate `s` to
-- be `𝕎` to recover named substitutions.
--
-- [aside]
-- The reason to want nameless indices for named substitutions is so you can do
-- substitutions of the form:
-- 
--     λx.λy.[x↦y](λy.x) ≡ λx.λy.λy.y↑1
--
-- where the final `y↑1` is the name `y` paired with the nameless index `1` to
-- indicate that it points to the outer `y` binding, not the inner `y` binding.
-- This structure allows you to do capture avoiding substitution very cleanly
-- without the need to gensym unique variable names, or rename/rebind lambdas
-- during substitution. □
--
-- Say you have two scope namespaces: one for expressions and one for types,
-- and we have a simple enum type `data Scope = Exp | Type`.
-- Then, you could instantiate `SubstSpaced sG sS e` with:
-- - `sG = Scope ∧ 𝕎`  
--   - i.e., an unscoped substitution for each (global) raw variable name and
--   `Scope`
-- - `sS = Scope ∧ 𝑂 𝕏` 
--   - i.e., a scoped for each for each: (non-global) raw variable name, and
--    `Scope`, plus one additional for nameless variables
--  In this way, the generic `SubstSpaced` type is instantiated to recover
--  three conceptual substitution maps:
--  - unscoped substitutions for global named expression variables and global
--    named type variables
--  - scoped substitutions for named expression variables and named type
--    variables
--  - scoped substitutions for nameless expression variables and nameless type
--    variables
--------------------------------------------------------------------------------

-- 𝓈 = ⟨𝓈G,𝓈S⟩
data SubstSpaced sG sS e = SubstSpaced
  { forall sG sS e. SubstSpaced sG sS e -> sG ⇰ SubstElem sS e
substSpacedUnscoped ∷ sG ⇰ SubstElem sS e
  , forall sG sS e. SubstSpaced sG sS e -> sS ⇰ SubstScoped sS e
substSpacedScoped   ∷ sS ⇰ SubstScoped sS e
  }
  deriving (SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
(SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool)
-> (SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool)
-> Eq (SubstSpaced sG sS e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall sG sS e.
(Eq sG, Eq sS, Eq e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
$c== :: forall sG sS e.
(Eq sG, Eq sS, Eq e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
== :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
$c/= :: forall sG sS e.
(Eq sG, Eq sS, Eq e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
/= :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
Eq,Eq (SubstSpaced sG sS e)
Eq (SubstSpaced sG sS e) =>
(SubstSpaced sG sS e -> SubstSpaced sG sS e -> Ordering)
-> (SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool)
-> (SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool)
-> (SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool)
-> (SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool)
-> (SubstSpaced sG sS e
    -> SubstSpaced sG sS e -> SubstSpaced sG sS e)
-> (SubstSpaced sG sS e
    -> SubstSpaced sG sS e -> SubstSpaced sG sS e)
-> Ord (SubstSpaced sG sS e)
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Ordering
SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS 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 sG sS e. (Ord sG, Ord sS, Ord e) => Eq (SubstSpaced sG sS e)
forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Ordering
forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS e
$ccompare :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Ordering
compare :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Ordering
$c< :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
< :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
$c<= :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
<= :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
$c> :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
> :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
$c>= :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
>= :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> Bool
$cmax :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS e
max :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS e
$cmin :: forall sG sS e.
(Ord sG, Ord sS, Ord e) =>
SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS e
min :: SubstSpaced sG sS e -> SubstSpaced sG sS e -> SubstSpaced sG sS e
Ord,Int -> SubstSpaced sG sS e -> ShowS
[SubstSpaced sG sS e] -> ShowS
SubstSpaced sG sS e -> String
(Int -> SubstSpaced sG sS e -> ShowS)
-> (SubstSpaced sG sS e -> String)
-> ([SubstSpaced sG sS e] -> ShowS)
-> Show (SubstSpaced sG sS e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall sG sS e.
(Show sG, Show sS, Show e) =>
Int -> SubstSpaced sG sS e -> ShowS
forall sG sS e.
(Show sG, Show sS, Show e) =>
[SubstSpaced sG sS e] -> ShowS
forall sG sS e.
(Show sG, Show sS, Show e) =>
SubstSpaced sG sS e -> String
$cshowsPrec :: forall sG sS e.
(Show sG, Show sS, Show e) =>
Int -> SubstSpaced sG sS e -> ShowS
showsPrec :: Int -> SubstSpaced sG sS e -> ShowS
$cshow :: forall sG sS e.
(Show sG, Show sS, Show e) =>
SubstSpaced sG sS e -> String
show :: SubstSpaced sG sS e -> String
$cshowList :: forall sG sS e.
(Show sG, Show sS, Show e) =>
[SubstSpaced sG sS e] -> ShowS
showList :: [SubstSpaced sG sS e] -> ShowS
Show)
makeLenses ''SubstSpaced

isNullSubstSpaced ∷ (Ord sS) ⇒ SubstSpaced sG sS e → 𝔹
isNullSubstSpaced :: forall sS sG e. Ord sS => SubstSpaced sG sS e -> Bool
isNullSubstSpaced (SubstSpaced sG ⇰ SubstElem sS e
𝓈G sS ⇰ SubstScoped sS e
𝓈S) = [Bool] -> Bool
forall t. ToIter Bool t => t -> Bool
and
  [ (sG ⇰ SubstElem sS e) -> Bool
forall a t. ToIter a t => t -> Bool
isEmpty sG ⇰ SubstElem sS e
𝓈G
  , 𝐼 Bool -> Bool
forall t. ToIter Bool t => t -> Bool
and (𝐼 Bool -> Bool) -> 𝐼 Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (SubstScoped sS e -> Bool) -> 𝐼 (SubstScoped sS e) -> 𝐼 Bool
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map SubstScoped sS e -> Bool
forall s e. SubstScoped s e -> Bool
isNullSubstScoped (𝐼 (SubstScoped sS e) -> 𝐼 Bool) -> 𝐼 (SubstScoped sS e) -> 𝐼 Bool
forall a b. (a -> b) -> a -> b
$ (sS ⇰ SubstScoped sS e) -> 𝐼 (SubstScoped sS e)
forall a. (sS ⇰ a) -> 𝐼 a
forall k s (d :: * -> *) a. Dict k s d => d a -> 𝐼 a
dvals sS ⇰ SubstScoped sS e
𝓈S
  ]

wfSubstSpaced ∷ (Ord sS) ⇒ SubstSpaced sG sS e → 𝔹
wfSubstSpaced :: forall sS sG e. Ord sS => SubstSpaced sG sS e -> Bool
wfSubstSpaced (SubstSpaced sG ⇰ SubstElem sS e
_𝓈G sS ⇰ SubstScoped sS e
𝓈S) = 𝐼 Bool -> Bool
forall t. ToIter Bool t => t -> Bool
and (𝐼 Bool -> Bool) -> 𝐼 Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (SubstScoped sS e -> Bool) -> 𝐼 (SubstScoped sS e) -> 𝐼 Bool
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map SubstScoped sS e -> Bool
forall s e. SubstScoped s e -> Bool
wfSubstScoped (𝐼 (SubstScoped sS e) -> 𝐼 Bool) -> 𝐼 (SubstScoped sS e) -> 𝐼 Bool
forall a b. (a -> b) -> a -> b
$ (sS ⇰ SubstScoped sS e) -> 𝐼 (SubstScoped sS e)
forall a. (sS ⇰ a) -> 𝐼 a
forall k s (d :: * -> *) a. Dict k s d => d a -> 𝐼 a
dvals sS ⇰ SubstScoped sS e
𝓈S

canonSubstSpaced ∷ (Ord sS,Eq e) ⇒ (sS → e ⌲ DVar) → (sS ⇰ ℕ64 → e → 𝑂 e) → (e → e) → SubstSpaced sG sS e → SubstSpaced sG sS e
canonSubstSpaced :: 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 sS -> e ⌲ DVar
ℓvar (sS ⇰ ℕ64) -> e -> 𝑂 e
substE e -> e
canonE (SubstSpaced sG ⇰ SubstElem sS e
𝓈G sS ⇰ SubstScoped sS e
𝓈S) = 
  let 𝓈G' :: sG ⇰ SubstElem sS e
𝓈G' = (SubstElem sS e -> SubstElem sS e)
-> (sG ⇰ SubstElem sS e) -> sG ⇰ SubstElem sS e
forall a b. (a -> b) -> (sG ⇰ a) -> sG ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (((sS ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e) -> SubstElem sS e -> SubstElem sS e
forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e) -> SubstElem s e -> SubstElem s e
canonSubstElem (sS ⇰ ℕ64) -> e -> 𝑂 e
substE e -> e
canonE) sG ⇰ SubstElem sS e
𝓈G
      𝓈S' :: sS ⇰ SubstScoped sS e
𝓈S' = (sS ⇰ SubstScoped sS e)
-> (sS -> SubstScoped sS e -> 𝑂 (SubstScoped sS e))
-> sS ⇰ SubstScoped sS e
forall k (t :: * -> *) a b.
OKFunctor k t =>
t a -> (k -> a -> 𝑂 b) -> t b
okmapOn sS ⇰ SubstScoped sS e
𝓈S ((sS -> SubstScoped sS e -> 𝑂 (SubstScoped sS e))
 -> sS ⇰ SubstScoped sS e)
-> (sS -> SubstScoped sS e -> 𝑂 (SubstScoped sS e))
-> sS ⇰ SubstScoped sS e
forall a b. (a -> b) -> a -> b
$ \ sS
s SubstScoped sS e
𝓈 → 
        let 𝓈' :: SubstScoped sS e
𝓈' = (e ⌲ DVar)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SubstScoped sS e
-> SubstScoped sS e
forall s e.
(Eq s, Eq e) =>
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SubstScoped s e
-> SubstScoped s e
canonSubstScoped (sS -> e ⌲ DVar
ℓvar sS
s) (sS ⇰ ℕ64) -> e -> 𝑂 e
substE e -> e
canonE SubstScoped sS e
𝓈
        in
        if SubstScoped sS e -> Bool
forall s e. SubstScoped s e -> Bool
isNullSubstScoped SubstScoped sS e
𝓈'
        then 𝑂 (SubstScoped sS e)
forall a. 𝑂 a
None
        else SubstScoped sS e -> 𝑂 (SubstScoped sS e)
forall a. a -> 𝑂 a
Some SubstScoped sS e
𝓈'
  in (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced sG ⇰ SubstElem sS e
𝓈G' sS ⇰ SubstScoped sS e
𝓈S'

-- Alter a substitution to "protect" the first n nameless indices. This
-- commonly occurs when moving a substitution underneath a binder.
-- E.g.,
--
--     shift 1
--     [ 0 ↦ 1
--     , 1 ↦ 2
--     , 2 ↦ 3
--     ]
--     ≡
--     [ 0 ↦ 0
--     , 1 ↦ 2
--     , 2 ↦ 3
--     , 3 ↦ 4
--     ]
shiftSubstSpaced ∷ (Ord sS) ⇒ sS ⇰ ℕ64 → SubstSpaced sG sS e → SubstSpaced sG sS e
shiftSubstSpaced :: forall sS sG e.
Ord sS =>
(sS ⇰ ℕ64) -> SubstSpaced sG sS e -> SubstSpaced sG sS e
shiftSubstSpaced sS ⇰ ℕ64
ιs (SubstSpaced sG ⇰ SubstElem sS e
𝓈G sS ⇰ SubstScoped sS e
𝓈S) =
  let 𝓈G' :: sG ⇰ SubstElem sS e
𝓈G' = (SubstElem sS e -> SubstElem sS e)
-> (sG ⇰ SubstElem sS e) -> sG ⇰ SubstElem sS e
forall a b. (a -> b) -> (sG ⇰ a) -> sG ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((sS ⇰ ℕ64) -> SubstElem sS e -> SubstElem sS e
forall s e. Ord s => (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e
introSubstElem sS ⇰ ℕ64
ιs) sG ⇰ SubstElem sS e
𝓈G
      𝓈S' :: sS ⇰ SubstScoped sS e
𝓈S' = (sS -> SubstScoped sS e -> SubstScoped sS e)
-> (sS ⇰ SubstScoped sS e) -> sS ⇰ SubstScoped sS e
forall a b. (sS -> a -> b) -> (sS ⇰ a) -> sS ⇰ b
forall k (t :: * -> *) a b.
KFunctor k t =>
(k -> a -> b) -> t a -> t b
kmap ((sS ⇰ ℕ64) -> sS -> SubstScoped sS e -> SubstScoped sS e
forall s e.
Ord s =>
(s ⇰ ℕ64) -> s -> SubstScoped s e -> SubstScoped s e
shiftSubstScoped sS ⇰ ℕ64
ιs) sS ⇰ SubstScoped sS e
𝓈S
  in (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced sG ⇰ SubstElem sS e
𝓈G' sS ⇰ SubstScoped sS e
𝓈S'

-- The substitution that introduces de bruijn variable 0, and shifts everything
-- else up by one.
-- E.g.,
--
--     intro 1
--     ≡
--     [ 0 ↦ 1
--     , 1 ↦ 2
--     , 2 ↦ 3 
--     , …
--     ]
introSubstSpaced ∷ sS ⇰ ℕ64 → SubstSpaced sG sS e
introSubstSpaced :: forall sS sG e. (sS ⇰ ℕ64) -> SubstSpaced sG sS e
introSubstSpaced = (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced sG ⇰ SubstElem sS e
forall a. Null a => a
null ((sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
-> ((sS ⇰ ℕ64) -> sS ⇰ SubstScoped sS e)
-> (sS ⇰ ℕ64)
-> SubstSpaced sG sS e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (ℕ64 -> SubstScoped sS e) -> (sS ⇰ ℕ64) -> sS ⇰ SubstScoped sS e
forall a b. (a -> b) -> (sS ⇰ a) -> sS ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ℕ64 -> SubstScoped sS e
forall s e. ℕ64 -> SubstScoped s e
introSubstScoped

sbindsSubstSpaced ∷ sS ⇰ 𝕍 e → SubstSpaced sG sS e
sbindsSubstSpaced :: forall sS e sG. (sS ⇰ 𝕍 e) -> SubstSpaced sG sS e
sbindsSubstSpaced sS ⇰ 𝕍 e
ess = (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced sG ⇰ SubstElem sS e
forall a. Null a => a
null ((sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall a b. (a -> b) -> a -> b
$ (sS ⇰ 𝕍 e) -> (𝕍 e -> SubstScoped sS e) -> sS ⇰ SubstScoped sS e
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn sS ⇰ 𝕍 e
ess 𝕍 e -> SubstScoped sS e
forall e s. 𝕍 e -> SubstScoped s e
bindSubstScoped

ubindsSubstSpaced ∷ sG ⇰ e → SubstSpaced sG sS e
ubindsSubstSpaced :: forall sG e sS. (sG ⇰ e) -> SubstSpaced sG sS e
ubindsSubstSpaced sG ⇰ e
es = (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced ((e -> SubstElem sS e) -> (sG ⇰ e) -> sG ⇰ SubstElem sS e
forall a b. (a -> b) -> (sG ⇰ a) -> sG ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((sS ⇰ ℕ64) -> 𝑂 e -> SubstElem sS e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem sS ⇰ ℕ64
forall a. Null a => a
null (𝑂 e -> SubstElem sS e) -> (e -> 𝑂 e) -> e -> SubstElem sS e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ e -> 𝑂 e
forall a. a -> 𝑂 a
Some) sG ⇰ e
es) sS ⇰ SubstScoped sS e
forall a. Null a => a
null

-- 𝓈smbindsG ∷ sG ⇰ e → SubstSpaced sG sS e
-- 𝓈smbindsG esᴳ = SubstSpaced null (map (SubstElem null ∘ const ∘ return) esᴳ) 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|
--   ρ+𝔰 = (ρ₁+𝔰₁)⊔(ρ₂+𝔰₂-ι₁)
--     𝔰 = ((ρ₁+𝔰₁)⊔(ρ₂+𝔰₂-ι₁))-ρ


-- substSpacedExtended _ _ 𝓈 ιs e ≈ 𝓈(e⇈ιs)
substSpacedExtended ∷ (Ord sG,Ord sS) ⇒ (sS → e ⌲ DVar) → (SubstSpaced sG sS e → e → 𝑂 e) → SubstSpaced sG sS e → sS ⇰ ℕ64 → e → 𝑂 e
substSpacedExtended :: forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
substSpacedExtended sS -> e ⌲ DVar
ℓvar SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P sS ⇰ ℕ64
ιs = SubstSpaced sG sS e -> e -> 𝑂 e
substE (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e -> e -> 𝑂 e
forall a b. (a -> b) -> a -> b
$ (sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
appendSubstSpaced sS -> e ⌲ DVar
ℓvar SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P (SubstSpaced sG sS e -> SubstSpaced sG sS e)
-> SubstSpaced sG sS e -> SubstSpaced sG sS e
forall a b. (a -> b) -> a -> b
$ (sS ⇰ ℕ64) -> SubstSpaced sG sS e
forall sS sG e. (sS ⇰ ℕ64) -> SubstSpaced sG sS e
introSubstSpaced sS ⇰ ℕ64
ιs

-- CURRENTLY NOT USED
substSubstElemSpacedE ∷ (Ord sG,Ord sS) ⇒ (sS → e ⌲ DVar) → (SubstSpaced sG sS e → e → 𝑂 e) → SubstSpaced sG sS e → SubstElem sS e → 𝑂 e
substSubstElemSpacedE :: forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstElem sS e
-> 𝑂 e
substSubstElemSpacedE sS -> e ⌲ DVar
ℓvar SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P = ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem sS e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
substSubstElemE (((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem sS e -> 𝑂 e)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem sS e -> 𝑂 e
forall a b. (a -> b) -> a -> b
$ (sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
substSpacedExtended sS -> e ⌲ DVar
ℓvar SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P

substSubstElemSpaced ∷ (Ord sG,Ord sS) ⇒ (sS → e ⌲ DVar) → (SubstSpaced sG sS e → e → 𝑂 e) → SubstSpaced sG sS e → SubstElem sS e → SubstElem sS e
substSubstElemSpaced :: forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstElem sS e
-> SubstElem sS e
substSubstElemSpaced sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P = ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem sS e -> SubstElem sS e
forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
substSubstElem (((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem sS e -> SubstElem sS e)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem sS e -> SubstElem sS e
forall a b. (a -> b) -> a -> b
$ (sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
substSpacedExtended sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P

-- CURRENTLY NOT USED
substSSubstElemSpaced ∷ (Ord sG,Ord sS) ⇒ (sS → e ⌲ DVar) → (SubstSpaced sG sS e → e → 𝑂 e) → SubstSpaced sG sS e → sS → SSubstElem sS e → SSubstElem sS e
substSSubstElemSpaced :: forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> sS
-> SSubstElem sS e
-> SSubstElem sS e
substSSubstElemSpaced sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P sS
s = (e ⌲ DVar)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem sS e -> SSubstElem sS e
forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e
substSSubstElem (sS -> e ⌲ DVar
ℓvars sS
s) (((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem sS e -> SSubstElem sS e)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem sS e -> SSubstElem sS e
forall a b. (a -> b) -> a -> b
$ (sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
substSpacedExtended sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P

appendSubstSpaced ∷
  ∀ sG sS e. (Ord sG,Ord sS)
  ⇒ (sS → e ⌲ DVar)
  → (SubstSpaced sG sS e → e → 𝑂 e)
  → SubstSpaced sG sS e
  → SubstSpaced sG sS e
  → SubstSpaced sG sS e
appendSubstSpaced :: forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
-> SubstSpaced sG sS e
appendSubstSpaced sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P₂ SubstSpaced sG sS e
𝓈P₁ =
  let SubstSpaced sG ⇰ SubstElem sS e
𝓈G₁ sS ⇰ SubstScoped sS e
𝓈S₁ = SubstSpaced sG sS e
𝓈P₁
      SubstSpaced sG ⇰ SubstElem sS e
𝓈G₂ sS ⇰ SubstScoped sS e
𝓈S₂ = SubstSpaced sG sS e
𝓈P₂
      𝓈Gᵣ :: sG ⇰ SubstElem sS e
𝓈Gᵣ = (SubstElem sS e -> SubstElem sS e)
-> (sG ⇰ SubstElem sS e) -> sG ⇰ SubstElem sS e
forall a b. (a -> b) -> (sG ⇰ a) -> sG ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstElem sS e
-> SubstElem sS e
forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> SubstElem sS e
-> SubstElem sS e
substSubstElemSpaced sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P₂) sG ⇰ SubstElem sS e
𝓈G₁ (sG ⇰ SubstElem sS e)
-> (sG ⇰ SubstElem sS e) -> sG ⇰ SubstElem sS e
forall a. (sG ⇰ a) -> (sG ⇰ a) -> sG ⇰ a
forall k s (d :: * -> *) a. Dict k s d => d a -> d a -> d a
⩌ sG ⇰ SubstElem sS e
𝓈G₂
      𝓈S₁' :: sS ⇰ SubstScoped sS e
𝓈S₁' = (sS ⇰ SubstScoped sS e)
-> (sS -> SubstScoped sS e -> SubstScoped sS e)
-> sS ⇰ SubstScoped sS e
forall k (t :: * -> *) a b.
KFunctor k t =>
t a -> (k -> a -> b) -> t b
kmapOn sS ⇰ SubstScoped sS e
𝓈S₁ ((sS -> SubstScoped sS e -> SubstScoped sS e)
 -> sS ⇰ SubstScoped sS e)
-> (sS -> SubstScoped sS e -> SubstScoped sS e)
-> sS ⇰ SubstScoped sS e
forall a b. (a -> b) -> a -> b
$ \ sS
s SubstScoped sS e
𝓈 → 
        (e ⌲ DVar)
-> ((sS ⇰ ℕ64) -> e -> 𝑂 e) -> SubstScoped sS e -> SubstScoped sS e
forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstScoped s e -> SubstScoped s e
substSubstScoped (sS -> e ⌲ DVar
ℓvars sS
s) ((sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
forall sG sS e.
(Ord sG, Ord sS) =>
(sS -> e ⌲ DVar)
-> (SubstSpaced sG sS e -> e -> 𝑂 e)
-> SubstSpaced sG sS e
-> (sS ⇰ ℕ64)
-> e
-> 𝑂 e
substSpacedExtended sS -> e ⌲ DVar
ℓvars SubstSpaced sG sS e -> e -> 𝑂 e
substE SubstSpaced sG sS e
𝓈P₂) SubstScoped sS e
𝓈
      𝓈Sᵣ :: sS ⇰ SubstScoped sS e
𝓈Sᵣ= (sS ⇰ SubstScoped sS e)
-> (sS ⇰ SubstScoped sS e)
-> (SubstScoped sS e -> SubstScoped sS e -> SubstScoped sS e)
-> sS ⇰ SubstScoped sS e
forall k s (d :: * -> *) a.
Dict k s d =>
d a -> d a -> (a -> a -> a) -> d a
dunionByOn sS ⇰ SubstScoped sS e
𝓈S₁' sS ⇰ SubstScoped sS e
𝓈S₂ ((SubstScoped sS e -> SubstScoped sS e -> SubstScoped sS e)
 -> sS ⇰ SubstScoped sS e)
-> (SubstScoped sS e -> SubstScoped sS e -> SubstScoped sS e)
-> sS ⇰ SubstScoped sS e
forall a b. (a -> b) -> a -> b
$ \ SubstScoped sS e
𝓈₁ SubstScoped sS e
𝓈₂ →
        if
        | SubstScoped sS e -> Bool
forall s e. SubstScoped s e -> Bool
isNullSubstScoped SubstScoped sS e
𝓈₁ → SubstScoped sS e
𝓈₂
        | SubstScoped sS e -> Bool
forall s e. SubstScoped s e -> Bool
isNullSubstScoped SubstScoped sS e
𝓈₂ → SubstScoped sS e
𝓈₁
        | Bool
otherwise →
            let SubstScoped ℕ64
ρ̇₁ 𝕍 (SSubstElem sS e)
es₁ ℤ64
ι₁ = SubstScoped sS e
𝓈₁
                SubstScoped ℕ64
ρ̇₂ 𝕍 (SSubstElem sS e)
es₂ ℤ64
ι₂ = SubstScoped sS e
𝓈₂
                𝔰₁ :: ℤ64
𝔰₁ = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕍 (SSubstElem sS e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem sS 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 sS e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem sS 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 sS e)
es = ℕ64 -> (ℕ64 -> SSubstElem sS e) -> 𝕍 (SSubstElem sS e)
forall a. ℕ64 -> (ℕ64 -> a) -> 𝕍 a
vecF (ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 ℤ64
𝔰) ((ℕ64 -> SSubstElem sS e) -> 𝕍 (SSubstElem sS e))
-> (ℕ64 -> SSubstElem sS e) -> 𝕍 (SSubstElem sS 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 sS e)
es₂ 𝕍 (SSubstElem sS e) -> ℕ64 -> SSubstElem sS 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
ρ₁         → DVar -> SSubstElem sS e
forall s e. DVar -> SSubstElem s e
Var_SSE (DVar -> SSubstElem sS e) -> DVar -> SSubstElem sS e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> ℕ64 -> DVar
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 sS e)
es₁ 𝕍 (SSubstElem sS e) -> ℕ64 -> SSubstElem sS 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
ι₁      → DVar -> SSubstElem sS e
forall s e. DVar -> SSubstElem s e
Var_SSE (DVar -> SSubstElem sS e) -> DVar -> SSubstElem sS e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> ℕ64 -> DVar
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 sS e)
es₂ 𝕍 (SSubstElem sS e) -> ℕ64 -> SSubstElem sS 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 sS e
forall a. STACK => 𝕊 -> a
error 𝕊
"bad"
            in
            ℕ64 -> 𝕍 (SSubstElem sS e) -> ℤ64 -> SubstScoped sS e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ̇ 𝕍 (SSubstElem sS e)
es ℤ64
ι
  in (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced sG ⇰ SubstElem sS e
𝓈Gᵣ sS ⇰ SubstScoped sS e
𝓈Sᵣ

-------------
-- FUNCTOR --
-------------

instance Functor (SubstSpaced sG sS) where
  map :: forall a b. (a -> b) -> SubstSpaced sG sS a -> SubstSpaced sG sS b
map a -> b
f (SubstSpaced sG ⇰ SubstElem sS a
𝓈G sS ⇰ SubstScoped sS a
𝓈S) = (sG ⇰ SubstElem sS b)
-> (sS ⇰ SubstScoped sS b) -> SubstSpaced sG sS b
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced ((a -> b) -> (sG ⇰ SubstElem sS a) -> sG ⇰ SubstElem sS b
forall (t :: * -> *) (u :: * -> *) a b.
(Functor t, Functor u) =>
(a -> b) -> t (u a) -> t (u b)
mapp a -> b
f sG ⇰ SubstElem sS a
𝓈G) ((sS ⇰ SubstScoped sS b) -> SubstSpaced sG sS b)
-> (sS ⇰ SubstScoped sS b) -> SubstSpaced sG sS b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (sS ⇰ SubstScoped sS a) -> sS ⇰ SubstScoped sS b
forall (t :: * -> *) (u :: * -> *) a b.
(Functor t, Functor u) =>
(a -> b) -> t (u a) -> t (u b)
mapp a -> b
f sS ⇰ SubstScoped sS a
𝓈S

---------------------
-- PRETTY PRINTING --
---------------------

instance (Pretty s₁,Pretty s₂,Pretty e) ⇒ Pretty (SubstSpaced s₁ s₂ e) where
  pretty :: SubstSpaced s₁ s₂ e -> Doc
pretty (SubstSpaced s₁ ⇰ SubstElem s₂ e
𝓈G s₂ ⇰ SubstScoped s₂ e
𝓈S) = 𝐼 (Doc ∧ Doc) -> Doc
forall t. ToIter (Doc ∧ Doc) t => t -> Doc
ppDict (𝐼 (Doc ∧ Doc) -> Doc) -> 𝐼 (Doc ∧ Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ [𝐼 (Doc ∧ Doc)] -> 𝐼 (Doc ∧ Doc)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ if (s₁ ⇰ SubstElem s₂ e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize s₁ ⇰ SubstElem s₂ e
𝓈G ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 then 𝐼 (Doc ∧ Doc)
forall a. 𝐼 a
null𝐼 else (Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a t. Single a t => a -> t
single ((Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)) -> (Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppCon 𝕊
"𝐔" Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* (s₁ ⇰ SubstElem s₂ e) -> Doc
forall a. Pretty a => a -> Doc
pretty s₁ ⇰ SubstElem s₂ e
𝓈G
    , if (s₂ ⇰ SubstScoped s₂ e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize s₂ ⇰ SubstScoped s₂ e
𝓈S ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 then 𝐼 (Doc ∧ Doc)
forall a. 𝐼 a
null𝐼 else (Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a t. Single a t => a -> t
single ((Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)) -> (Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppCon 𝕊
"𝐒" Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* (s₂ ⇰ SubstScoped s₂ e) -> Doc
forall a. Pretty a => a -> Doc
pretty s₂ ⇰ SubstScoped s₂ e
𝓈S
    ]

-------------
-- FUZZING --
-------------

-- generates random substitutions for property based testing
instance (Ord sG,Ord sS,Fuzzy sG,Fuzzy sS,Fuzzy e) ⇒ Fuzzy (SubstSpaced sG sS e) where
  fuzzy :: FuzzyM (SubstSpaced sG sS e)
fuzzy = ((sG ⇰ SubstElem sS e)
 -> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
-> FuzzyM
     ((sG ⇰ SubstElem sS e)
      -> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced FuzzyM
  ((sG ⇰ SubstElem sS e)
   -> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
-> FuzzyM (sG ⇰ SubstElem sS e)
-> FuzzyM ((sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
⊡ FuzzyM (sG ⇰ SubstElem sS e)
forall a. Fuzzy a => FuzzyM a
fuzzy FuzzyM ((sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e)
-> FuzzyM (sS ⇰ SubstScoped sS e) -> FuzzyM (SubstSpaced sG sS e)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
⊡ FuzzyM (sS ⇰ SubstScoped sS e)
forall a. Fuzzy a => FuzzyM a
fuzzy

---------------
-- SHRINKING --
---------------

instance (Ord sG,Ord sS,Shrinky e) ⇒ Shrinky (SubstSpaced sG sS e) where
  shrink :: SubstSpaced sG sS e -> 𝐼 (SubstSpaced sG sS e)
shrink (SubstSpaced sG ⇰ SubstElem sS e
𝓈G sS ⇰ SubstScoped sS e
𝓈S) = do
    (sG ⇰ SubstElem sS e
𝓈G',sS ⇰ SubstScoped sS e
𝓈S') ← (sG ⇰ SubstElem sS e, sS ⇰ SubstScoped sS e)
-> 𝐼 (sG ⇰ SubstElem sS e, sS ⇰ SubstScoped sS e)
forall a. Shrinky a => a -> 𝐼 a
shrink (sG ⇰ SubstElem sS e
𝓈G,sS ⇰ SubstScoped sS e
𝓈S)
    SubstSpaced sG sS e -> 𝐼 (SubstSpaced sG sS e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (SubstSpaced sG sS e -> 𝐼 (SubstSpaced sG sS e))
-> SubstSpaced sG sS e -> 𝐼 (SubstSpaced sG sS e)
forall a b. (a -> b) -> a -> b
$ (sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced sG ⇰ SubstElem sS e
𝓈G' sS ⇰ SubstScoped sS e
𝓈S'