module UVMHS.Lib.Substitution.SubstScoped where

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

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

-- ============================== --
-- SCOPED (NAMELESS) SUBSTITUTION --
-- ============================== --

--------------------------------------------------------------------------------
-- Scoped (nameless) substitutions are substitutions over nameless
-- variables—i.e., natural numbers, otherwise known as De Bruijn indices—and
-- which are scope aware—i.e., they support operations for reinterpreting the
-- substitution when moving underneath new binders.
--------------------------------------------------------------------------------

-- 𝓈 ⩴ ⟨ρ,es,ι⟩
-- INVARIANT: |es| + ι ≥ 0
data SubstScoped s e = SubstScoped
  { forall s e. SubstScoped s e -> ℕ64
substScopedShift ∷ ℕ64
  -- ^ ρ: De Bruijn indices lower than this number will be untouched by this
  --      substitution. Think of it as a substitution working over all natural
  --      numbers being shifted to the right to ignore this many first indices.
  , forall s e. SubstScoped s e -> 𝕍 (SSubstElem s e)
substScopeElems ∷ 𝕍 (SSubstElem s e)
  -- ^ es: Instantiates as many of the first indices (post-shift by ρ) as the
  --       length of this vector with the values in the vector.
  , forall s e. SubstScoped s e -> ℤ64
substScopeIntro ∷ ℤ64
  -- ^ ι: Starting at the nameless variable index after all the shifts (ρ) and all
  --      the instantiations (es), simulate an introduction of this many new
  --      nameless variables by bumping all subsequent indices by this much.
  } deriving (SubstScoped s e -> SubstScoped s e -> Bool
(SubstScoped s e -> SubstScoped s e -> Bool)
-> (SubstScoped s e -> SubstScoped s e -> Bool)
-> Eq (SubstScoped s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e.
(Eq s, Eq e) =>
SubstScoped s e -> SubstScoped s e -> Bool
$c== :: forall s e.
(Eq s, Eq e) =>
SubstScoped s e -> SubstScoped s e -> Bool
== :: SubstScoped s e -> SubstScoped s e -> Bool
$c/= :: forall s e.
(Eq s, Eq e) =>
SubstScoped s e -> SubstScoped s e -> Bool
/= :: SubstScoped s e -> SubstScoped s e -> Bool
Eq,Eq (SubstScoped s e)
Eq (SubstScoped s e) =>
(SubstScoped s e -> SubstScoped s e -> Ordering)
-> (SubstScoped s e -> SubstScoped s e -> Bool)
-> (SubstScoped s e -> SubstScoped s e -> Bool)
-> (SubstScoped s e -> SubstScoped s e -> Bool)
-> (SubstScoped s e -> SubstScoped s e -> Bool)
-> (SubstScoped s e -> SubstScoped s e -> SubstScoped s e)
-> (SubstScoped s e -> SubstScoped s e -> SubstScoped s e)
-> Ord (SubstScoped s e)
SubstScoped s e -> SubstScoped s e -> Bool
SubstScoped s e -> SubstScoped s e -> Ordering
SubstScoped s e -> SubstScoped s e -> SubstScoped 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 (SubstScoped s e)
forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Bool
forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Ordering
forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> SubstScoped s e
$ccompare :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Ordering
compare :: SubstScoped s e -> SubstScoped s e -> Ordering
$c< :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Bool
< :: SubstScoped s e -> SubstScoped s e -> Bool
$c<= :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Bool
<= :: SubstScoped s e -> SubstScoped s e -> Bool
$c> :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Bool
> :: SubstScoped s e -> SubstScoped s e -> Bool
$c>= :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> Bool
>= :: SubstScoped s e -> SubstScoped s e -> Bool
$cmax :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> SubstScoped s e
max :: SubstScoped s e -> SubstScoped s e -> SubstScoped s e
$cmin :: forall s e.
(Ord s, Ord e) =>
SubstScoped s e -> SubstScoped s e -> SubstScoped s e
min :: SubstScoped s e -> SubstScoped s e -> SubstScoped s e
Ord,Int -> SubstScoped s e -> ShowS
[SubstScoped s e] -> ShowS
SubstScoped s e -> String
(Int -> SubstScoped s e -> ShowS)
-> (SubstScoped s e -> String)
-> ([SubstScoped s e] -> ShowS)
-> Show (SubstScoped s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> SubstScoped s e -> ShowS
forall s e. (Show s, Show e) => [SubstScoped s e] -> ShowS
forall s e. (Show s, Show e) => SubstScoped s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> SubstScoped s e -> ShowS
showsPrec :: Int -> SubstScoped s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => SubstScoped s e -> String
show :: SubstScoped s e -> String
$cshowList :: forall s e. (Show s, Show e) => [SubstScoped s e] -> ShowS
showList :: [SubstScoped s e] -> ShowS
Show)

makeLenses ''SubstScoped

-- 𝓈 ≜ ⟨ρ,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⌋    |
-- , …
-- ]
lookupSubstScoped ∷ SubstScoped s e → DVar → SSubstElem s e
lookupSubstScoped :: forall s e. SubstScoped s e -> DVar -> SSubstElem s e
lookupSubstScoped (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) (DVar ℕ64
n) =
  let 𝔰̇ :: ℕ64
𝔰̇  = 𝕍 (SSubstElem s e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s e)
es
  in
  if | ℕ64
n ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℕ64
ρ     → DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE (DVar -> SSubstElem s e) -> DVar -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar ℕ64
n
     | ℕ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
nℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
-ℕ64
ρ)
     | Bool
otherwise → DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE (DVar -> SSubstElem s e) -> DVar -> SSubstElem s 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 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
nℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
ι

interpSubstScoped ∷ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → SubstScoped s e → DVar → 𝑂 e
interpSubstScoped :: forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstScoped s e -> DVar -> 𝑂 e
interpSubstScoped e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstScoped s e
𝓈 DVar
n = (e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> 𝑂 e
forall e s.
(e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> 𝑂 e
interpSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE (SSubstElem s e -> 𝑂 e) -> SSubstElem s e -> 𝑂 e
forall a b. (a -> b) -> a -> b
$ SubstScoped s e -> DVar -> SSubstElem s e
forall s e. SubstScoped s e -> DVar -> SSubstElem s e
lookupSubstScoped SubstScoped s e
𝓈 DVar
n

wfSubstScoped ∷ SubstScoped s e → 𝔹
wfSubstScoped :: forall s e. SubstScoped s e -> Bool
wfSubstScoped (SubstScoped ℕ64
_ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = ℤ64
ι ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
≥ ℤ64 -> ℤ64
forall a. (Zero a, Minus a) => a -> a
neg (ℕ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)

canonSubstScoped ∷ ∀ s e. (Eq s,Eq e) ⇒ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → (e → e) → SubstScoped s e → SubstScoped s e
canonSubstScoped :: forall s e.
(Eq s, Eq e) =>
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SubstScoped s e
-> SubstScoped s e
canonSubstScoped e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE e -> e
canonE = SubstScoped s e -> SubstScoped s e
collapseNullShift (SubstScoped s e -> SubstScoped s e)
-> (SubstScoped s e -> SubstScoped s e)
-> SubstScoped s e
-> SubstScoped s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstScoped s e -> SubstScoped s e
expandIncs (SubstScoped s e -> SubstScoped s e)
-> (SubstScoped s e -> SubstScoped s e)
-> SubstScoped s e
-> SubstScoped s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstScoped s e -> SubstScoped s e
expandShifts (SubstScoped s e -> SubstScoped s e)
-> (SubstScoped s e -> SubstScoped s e)
-> SubstScoped s e
-> SubstScoped s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstScoped s e -> SubstScoped s e
canonElems
  where
    expandShiftsM ∷ RWS (SubstScoped s e) () ℕ64 ()
    expandShiftsM :: RWS (SubstScoped s e) () ℕ64 ()
expandShiftsM = do
      SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
_ι ← RWST (SubstScoped s e) () ℕ64 ID (SubstScoped s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
      ℕ64
n ← RWST (SubstScoped s e) () ℕ64 ID ℕ64
forall s (m :: * -> *). MonadState s m => m s
get
      if ℕ64
n ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ 𝕍 (SSubstElem s e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s e)
es
      then RWS (SubstScoped s e) () ℕ64 ()
forall (m :: * -> *). Return m => m ()
skip
      else 
        if 𝕍 (SSubstElem s e)
es 𝕍 (SSubstElem s e) -> ℕ64 -> SSubstElem s e
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℕ64
n SSubstElem s e -> SSubstElem s e -> Bool
forall a. Eq a => a -> a -> Bool
≡ DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE (ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> ℕ64 -> DVar
forall a b. (a -> b) -> a -> b
$ ℕ64
ρℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ℕ64
n)
        then do RWS (SubstScoped s e) () ℕ64 ()
forall (m :: * -> *) s.
(Monad m, MonadState s m, Multiplicative s) =>
m ()
bump ; RWS (SubstScoped s e) () ℕ64 ()
expandShiftsM
        else RWS (SubstScoped s e) () ℕ64 ()
forall (m :: * -> *). Return m => m ()
skip
    expandShifts ∷ SubstScoped s e → SubstScoped s e
    expandShifts :: SubstScoped s e -> SubstScoped s e
expandShifts 𝓈 :: SubstScoped s e
𝓈@(SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) =
      let n :: ℕ64
n = (ℕ64 ∧ ()) -> ℕ64
forall a b. (a ∧ b) -> a
fst ((ℕ64 ∧ ()) -> ℕ64) -> (ℕ64 ∧ ()) -> ℕ64
forall a b. (a -> b) -> a -> b
$ ((ℕ64 ∧ ()) ∧ ()) -> ℕ64 ∧ ()
forall a b. (a ∧ b) -> a
fst (((ℕ64 ∧ ()) ∧ ()) -> ℕ64 ∧ ()) -> ((ℕ64 ∧ ()) ∧ ()) -> ℕ64 ∧ ()
forall a b. (a -> b) -> a -> b
$ SubstScoped s e
-> ℕ64 -> RWS (SubstScoped s e) () ℕ64 () -> (ℕ64 ∧ ()) ∧ ()
forall r o s a. r -> s -> RWS r o s a -> (s ∧ o) ∧ a
runRWS SubstScoped s e
𝓈 ℕ64
0 RWS (SubstScoped s e) () ℕ64 ()
expandShiftsM
      in ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped (ℕ64
ρ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
n) (𝐼 (SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a t. ToIter a t => t -> 𝕍 a
vec (𝐼 (SSubstElem s e) -> 𝕍 (SSubstElem s e))
-> 𝐼 (SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a t n.
(ToIter a t, Ord n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
dropN ℕ64
n (𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e))
-> 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ 𝕍 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕍 (SSubstElem s e)
es) ℤ64
ι
    expandIncsM ∷ RWS (SubstScoped s e) () ℕ64 ()
    expandIncsM :: RWS (SubstScoped s e) () ℕ64 ()
expandIncsM = do
      SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι ← RWST (SubstScoped s e) () ℕ64 ID (SubstScoped s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
      ℕ64
n ← RWST (SubstScoped s e) () ℕ64 ID ℕ64
forall s (m :: * -> *). MonadState s m => m s
get
      let 𝔰 :: ℕ64
𝔰 = 𝕍 (SSubstElem s e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s e)
es
      if ℕ64
n ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
𝔰
      then RWS (SubstScoped s e) () ℕ64 ()
forall (m :: * -> *). Return m => m ()
skip
      else
        let i :: ℕ64
i = ℕ64
𝔰 ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
1 ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
n
            i' :: ℤ64
i' = ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
ρ ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
i ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ ℤ64
ι
        in
        if ℤ64
i' ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
≥ ℤ64
0 Bool -> Bool -> Bool
⩓ 𝕍 (SSubstElem s e)
es 𝕍 (SSubstElem s e) -> ℕ64 -> SSubstElem s e
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℕ64
i SSubstElem s e -> SSubstElem s e -> Bool
forall a. Eq a => a -> a -> Bool
≡ DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE (ℕ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
i')
        then do RWS (SubstScoped s e) () ℕ64 ()
forall (m :: * -> *) s.
(Monad m, MonadState s m, Multiplicative s) =>
m ()
bump ; RWS (SubstScoped s e) () ℕ64 ()
expandIncsM
        else RWS (SubstScoped s e) () ℕ64 ()
forall (m :: * -> *). Return m => m ()
skip
    expandIncs ∷ SubstScoped s e → SubstScoped s e
    expandIncs :: SubstScoped s e -> SubstScoped s e
expandIncs 𝓈 :: SubstScoped s e
𝓈@(SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) =
      let n :: ℕ64
n = (ℕ64 ∧ ()) -> ℕ64
forall a b. (a ∧ b) -> a
fst ((ℕ64 ∧ ()) -> ℕ64) -> (ℕ64 ∧ ()) -> ℕ64
forall a b. (a -> b) -> a -> b
$ ((ℕ64 ∧ ()) ∧ ()) -> ℕ64 ∧ ()
forall a b. (a ∧ b) -> a
fst (((ℕ64 ∧ ()) ∧ ()) -> ℕ64 ∧ ()) -> ((ℕ64 ∧ ()) ∧ ()) -> ℕ64 ∧ ()
forall a b. (a -> b) -> a -> b
$ SubstScoped s e
-> ℕ64 -> RWS (SubstScoped s e) () ℕ64 () -> (ℕ64 ∧ ()) ∧ ()
forall r o s a. r -> s -> RWS r o s a -> (s ∧ o) ∧ a
runRWS SubstScoped s e
𝓈 ℕ64
0 RWS (SubstScoped s e) () ℕ64 ()
expandIncsM
      in ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ (𝐼 (SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a t. ToIter a t => t -> 𝕍 a
vec (𝐼 (SSubstElem s e) -> 𝕍 (SSubstElem s e))
-> 𝐼 (SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a t. ToIter a t => t -> 𝐼 a
reverse (𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e))
-> 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a t n.
(ToIter a t, Ord n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
dropN ℕ64
n (𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e))
-> 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a t. ToIter a t => t -> 𝐼 a
reverse (𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e))
-> 𝐼 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ 𝕍 (SSubstElem s e) -> 𝐼 (SSubstElem s e)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕍 (SSubstElem s e)
es) ℤ64
ι
    collapseNullShift ∷ SubstScoped s e → SubstScoped s e
    collapseNullShift :: SubstScoped s e -> SubstScoped s e
collapseNullShift 𝓈 :: SubstScoped s e
𝓈@(SubstScoped ℕ64
_ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) =
      if 𝕍 (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
      then ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
0 𝕍 (SSubstElem s e)
forall a. Null a => a
null ℤ64
0
      else SubstScoped s e
𝓈
    canonElems ∷ SubstScoped s e → SubstScoped s e
    canonElems :: SubstScoped s e -> SubstScoped s e
canonElems (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ ((SSubstElem s e -> SSubstElem s e)
-> 𝕍 (SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SSubstElem s e
-> SSubstElem s e
forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> SSubstElem s e
-> SSubstElem s e
canonSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE e -> e
canonE) 𝕍 (SSubstElem s e)
es) ℤ64
ι
        
isNullSubstScoped ∷ SubstScoped s e → 𝔹
isNullSubstScoped :: forall s e. SubstScoped s e -> Bool
isNullSubstScoped (SubstScoped ℕ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

introSubstScoped ∷ ℕ64 → SubstScoped s e
introSubstScoped :: forall s e. ℕ64 -> SubstScoped s e
introSubstScoped = ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
0 𝕍 (SSubstElem s e)
forall a. Null a => a
null (ℤ64 -> SubstScoped s e) -> (ℕ64 -> ℤ64) -> ℕ64 -> SubstScoped s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64

shiftSubstScoped ∷ (Ord s) ⇒ s ⇰ ℕ64 → s → SubstScoped s e → SubstScoped s e
shiftSubstScoped :: forall s e.
Ord s =>
(s ⇰ ℕ64) -> s -> SubstScoped s e -> SubstScoped s e
shiftSubstScoped s ⇰ ℕ64
ιs s
s (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = 
  let ρ' :: ℕ64
ρ'  = ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
(+) ℕ64
ρ (ℕ64 -> ℕ64) -> ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝑂 ℕ64 -> ℕ64
forall a. a -> 𝑂 a -> a
ifNone ℕ64
0 (𝑂 ℕ64 -> ℕ64) -> 𝑂 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ s ⇰ ℕ64
ιs (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
ιs
  in ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ' 𝕍 (SSubstElem s e)
es' ℤ64
ι

bindSubstScoped ∷ 𝕍 e → SubstScoped s e
bindSubstScoped :: forall e s. 𝕍 e -> SubstScoped s e
bindSubstScoped 𝕍 e
es = 
  let es' :: 𝕍 (SSubstElem s e)
es' = (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. a -> 𝑂 a
Some) 𝕍 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 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
forall a. Null a => a
null 𝕍 (SSubstElem s e)
es' ℤ64
ι

substSubstScoped ∷ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → SubstScoped s e → SubstScoped s e
substSubstScoped :: forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstScoped s e -> SubstScoped s e
substSubstScoped e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = 
  let es' :: 𝕍 (SSubstElem s e)
es' = (SSubstElem s e -> SSubstElem s e)
-> 𝕍 (SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a b. (a -> b) -> 𝕍 a -> 𝕍 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e
forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e
substSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE) 𝕍 (SSubstElem s e)
es
  in ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es' ℤ64
ι

-- -- | If we get a `SubstScoped` where some `dsubstElems` elements are merely emulating what happens under
-- -- a shift, or under an intro, we simplify it to instead use those, making the vector of elements
-- -- shorter.
-- --
-- -- For instance, consider:
-- --   SubstScoped 3 [3, 4, 1, 1, 9, 10] 2
-- -- supposedly, it:
-- --   * keeps the first 3 indices protected (0 ↦ 0, 1 ↦ 1, 2 ↦ 2)
-- --   * then maps indices [3,4,5,6,7,8] to [3,4,1,1,9,10]
-- --   * then maps indices [9,10,11,…] to [11,12,13,‥]
-- -- but this could be better expressed as:
-- --   SubstScoped 5 [1, 1] 2
-- --   * keeps the first 5 indices protected, i.e. [0,1,2,3,4] ↦ [0,1,2,3,4]
-- --   * then [5,6] ↦ [1, 1]
-- --   * then [7,8,9,10,11,…] ↦ [9,10,11,12,13,…]
-- simplifySubstScoped ∷ SubstScoped s e → SubstScoped s e
-- simplifySubstScoped (SubstScoped s es i) =
--   let
--     (shifts :* intermediate) = peelPrefix s (list es)
--     elems = peelReverseSuffix shifts (list $ reverse intermediate) i
--   in SubstScoped shifts elems i
--   where
--     peelPrefix ∷ ℕ64 → 𝐿 (SSubstElem s e) → (ℕ64 ∧ 𝐿 (SSubstElem s e))
--     peelPrefix shifts (Var_SSE h :& t) | h ≡ s = peelPrefix (shifts + 1) t
--     peelPrefix shifts elems = shifts :* elems
-- 
--     -- Note: technically we could pre-add shifts and intros, but this is a bit more readable
--     peelReverseSuffix ∷ ℕ64 → 𝐿 (SSubstElem s e) → ℤ64 → 𝕍 (SSubstElem s e)
--     peelReverseSuffix shifts (Var_SSE h :& t) intros
--       | intΩ64 h ≡ intΩ64 (shifts + count t) + intros
--       = peelReverseSuffix shifts t intros
--     peelReverseSuffix _ revElems _ = vec (reverse revElems)

-- instance (Eq e, Eq s) ⇒ Eq (SubstScoped s e) where
--   ds1 == ds2 =
--     let
--       SubstScoped s1 es1 i1 = simplifySubstScoped ds1
--       SubstScoped s2 es2 i2 = simplifySubstScoped ds2
--       in meets [s1 ≡ s2, es1 ≡ es2, i1 ≡ i2]

-- Note: SubstScoped tend to be quite verbose under makePrettyRecord, so this instance tries to make them
-- print more concisely.
--
-- ⊘ means the identity substitution
--
-- Otherwise the pattern is: `/n{...}↑o` where:
-- - `/n` represents `n` shifts,
-- - `{...}` is the vector of de Bruijn instantiations,
-- - `↑o` represents `o` introductions,
-- Each of these subparts is optional if it's zero/zero-length.

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

ppSubstScopedWith ∷ (Pretty e) ⇒ (s ⇰ ℕ64 → Doc) → (DVarInf → Doc) → SubstScoped s e → 𝐼 (Doc ∧ Doc)
ppSubstScopedWith :: forall e s.
Pretty e =>
((s ⇰ ℕ64) -> Doc)
-> (DVarInf -> Doc) -> SubstScoped s e -> 𝐼 (Doc ∧ Doc)
ppSubstScopedWith (s ⇰ ℕ64) -> Doc
ιD DVarInf -> Doc
xD (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = 
  let kvs :: 𝐼 (Doc ∧ Doc)
kvs = [𝐼 (Doc ∧ Doc)] -> 𝐼 (Doc ∧ Doc)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ if ℕ64
ρ ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 then 𝐼 (Doc ∧ Doc)
forall a. Null 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
$
            let k :: Doc
k = [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [DVarInf -> Doc
xD (DVarInf -> Doc) -> DVarInf -> Doc
forall a b. (a -> b) -> a -> b
$ DVar -> DVarInf
Var_DVI (DVar -> DVarInf) -> DVar -> DVarInf
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar ℕ64
0,𝕊 -> Doc
ppPun 𝕊
"…",DVarInf -> Doc
xD (DVarInf -> Doc) -> DVarInf -> Doc
forall a b. (a -> b) -> a -> b
$ DVar -> DVarInf
Var_DVI (DVar -> DVarInf) -> DVar -> DVarInf
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> ℕ64 -> DVar
forall a b. (a -> b) -> a -> b
$ ℕ64
ρ ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
1] 
                v :: Doc
v = 𝕊 -> Doc
ppLit 𝕊
"[≡]"
            in Doc
k Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* Doc
v
        , 𝐼 (ℕ64 ∧ SSubstElem s e)
-> ((ℕ64 ∧ SSubstElem s e) -> Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> 𝐼 (n ∧ a)
withIndex @ℕ64 𝕍 (SSubstElem s e)
es) (((ℕ64 ∧ SSubstElem s e) -> Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc))
-> ((ℕ64 ∧ SSubstElem s e) -> Doc ∧ Doc) -> 𝐼 (Doc ∧ Doc)
forall a b. (a -> b) -> a -> b
$ \ (ℕ64
n :* SSubstElem s e
e) →
            let k :: Doc
k = [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [DVarInf -> Doc
xD (DVarInf -> Doc) -> DVarInf -> Doc
forall a b. (a -> b) -> a -> b
$ DVar -> DVarInf
Var_DVI (DVar -> DVarInf) -> DVar -> DVarInf
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> ℕ64 -> DVar
forall a b. (a -> b) -> a -> b
$ ℕ64
ρ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
n]
                v :: Doc
v = ((s ⇰ ℕ64) -> Doc) -> (DVarInf -> Doc) -> SSubstElem s e -> Doc
forall e s.
Pretty e =>
((s ⇰ ℕ64) -> Doc) -> (DVarInf -> Doc) -> SSubstElem s e -> Doc
ppSSubstElemNamed (s ⇰ ℕ64) -> Doc
ιD DVarInf -> Doc
xD SSubstElem s e
e
            in Doc
k Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* Doc
v
        , if ℤ64
ι ℤ64 -> ℤ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℤ64
0 then 𝐼 (Doc ∧ Doc)
forall a. Null 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
$ 
            let k :: Doc
k = [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
                  [ DVarInf -> Doc
xD (DVarInf -> Doc) -> DVarInf -> Doc
forall a b. (a -> b) -> a -> b
$ DVar -> DVarInf
Var_DVI (DVar -> DVarInf) -> DVar -> DVarInf
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> ℕ64 -> DVar
forall a b. (a -> b) -> a -> b
$ ℕ64
ρ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ 𝕍 (SSubstElem s e) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 (SSubstElem s e)
es
                  , 𝕊 -> Doc
ppPun 𝕊
"…"
                  , DVarInf -> Doc
xD DVarInf
Inf_DVI
                  ]
                v :: Doc
v = 𝕊 -> Doc
ppLit (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat 
                  [ 𝕊
"["
                  , case ℤ64
ι ℤ64 -> ℤ64 -> Ordering
forall a. Ord a => a -> a -> Ordering
⋚ ℤ64
0 of
                      Ordering
LT → ℤ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℤ64
ι 
                      -- EQ pattern should never happen due to enclosing if condition
                      Ordering
EQ → 𝕊
"≡"    
                      Ordering
GT → [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊
"+",ℤ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℤ64
ι]
                  , 𝕊
"]"
                  ]
            in Doc
k Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* Doc
v
        ]
  in
  𝐼 (Doc ∧ Doc)
kvs

-- ppSubstScopedNamed ∷ (Pretty s,Pretty e) ⇒ (s ⇰ ℕ64 → Doc) → Name → SubstScoped s e → 𝐼 (Doc ∧ Doc)
-- ppSubstScopedNamed ιD x = ppSubstScoped ιD $ \ n → pretty $ NVarInf n x

instance (Pretty e, Pretty s) ⇒ Pretty (SubstScoped s e) where
  pretty :: SubstScoped s e -> Doc
pretty = 𝐼 (Doc ∧ Doc) -> Doc
forall t. ToIter (Doc ∧ Doc) t => t -> Doc
ppDict (𝐼 (Doc ∧ Doc) -> Doc)
-> (SubstScoped s e -> 𝐼 (Doc ∧ Doc)) -> SubstScoped s e -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ⇰ ℕ64) -> Doc)
-> (DVarInf -> Doc) -> SubstScoped s e -> 𝐼 (Doc ∧ Doc)
forall e s.
Pretty e =>
((s ⇰ ℕ64) -> Doc)
-> (DVarInf -> Doc) -> SubstScoped s e -> 𝐼 (Doc ∧ Doc)
ppSubstScopedWith (s ⇰ ℕ64) -> Doc
forall a. Pretty a => a -> Doc
pretty DVarInf -> Doc
forall a. Pretty a => a -> Doc
pretty

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

instance Functor (SubstScoped s) where
  map :: forall a b. (a -> b) -> SubstScoped s a -> SubstScoped s b
map a -> b
f (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s a)
es ℤ64
ι) = ℕ64 -> 𝕍 (SSubstElem s b) -> ℤ64 -> SubstScoped s b
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ ((a -> b) -> 𝕍 (SSubstElem s a) -> 𝕍 (SSubstElem s b)
forall (t :: * -> *) (u :: * -> *) a b.
(Functor t, Functor u) =>
(a -> b) -> t (u a) -> t (u b)
mapp a -> b
f 𝕍 (SSubstElem s a)
es) ℤ64
ι

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

instance (Ord s,Fuzzy s,Fuzzy e) ⇒ Fuzzy (SubstScoped s e) where
  fuzzy :: FuzzyM (SubstScoped s e)
fuzzy = do
    ℕ64
ρ ← FuzzyM ℕ64
forall a. Fuzzy a => FuzzyM a
fuzzy
    ℕ64
𝔰 ← FuzzyM ℕ64
fuzzyDepth
    𝕍 (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
$ \ ℕ64
_ → FuzzyM (SSubstElem s e)
forall a. Fuzzy a => FuzzyM a
fuzzyRec
    ℤ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
𝔰
    SubstScoped s e -> FuzzyM (SubstScoped s e)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (SubstScoped s e -> FuzzyM (SubstScoped s e))
-> SubstScoped s e -> FuzzyM (SubstScoped s e)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι

instance (Ord s,Shrinky e) ⇒ Shrinky (SubstScoped s e) where
  shrink :: SubstScoped s e -> 𝐼 (SubstScoped s e)
shrink (SubstScoped ℕ64
ρ 𝕍 (SSubstElem s e)
es ℤ64
ι) = do
    (ℕ64
ρ',𝕍 (SSubstElem s e)
es',ℤ64
ι') ← (ℕ64, 𝕍 (SSubstElem s e), ℤ64) -> 𝐼 (ℕ64, 𝕍 (SSubstElem s e), ℤ64)
forall a. Shrinky a => a -> 𝐼 a
shrink (ℕ64
ρ,𝕍 (SSubstElem s e)
es,ℤ64
ι)
    Bool -> 𝐼 ()
forall (m :: * -> *). (Monad m, MonadNondet m) => Bool -> m ()
mzeroIfNot (Bool -> 𝐼 ()) -> Bool -> 𝐼 ()
forall a b. (a -> b) -> a -> b
$ ℤ64
ι' ℤ64 -> ℤ64 -> Bool
forall a. Ord a => a -> a -> Bool
≥ ℤ64 -> ℤ64
forall a. (Zero a, Minus a) => a -> a
neg (ℕ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')
    SubstScoped s e -> 𝐼 (SubstScoped s e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (SubstScoped s e -> 𝐼 (SubstScoped s e))
-> SubstScoped s e -> 𝐼 (SubstScoped s e)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
ρ' 𝕍 (SSubstElem s e)
es' ℤ64
ι'