module UVMHS.Lib.Substitution.SubstElem where

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

import UVMHS.Lib.Substitution.Var

-- ==================== --
-- SUBSTITUTION ELEMENT --
-- ==================== --

--------------------------------------------------------------------------------
-- A delayed element with a delayed intro renaming. It's nice to delay things
-- like this, because it is often the case that:
-- 1. substitution elements get further shifted, which can be done while
--    maintaining delayed form by just shifting the delayed renaming
-- 2. sometimes you don't need to fully materialize the substitution value
--------------------------------------------------------------------------------

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

-- `substE ιs e`
-- ≡ 
-- first weaken `e` by `ιs`, and then optionally perform some substitution to
-- the result (e.g., just leaving it alone)
interpSubstElem ∷ (s ⇰ ℕ64 → e → 𝑂 e) → SubstElem s e → 𝑂 e
interpSubstElem :: forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE (SubstElem s ⇰ ℕ64
ιs 𝑂 e
eO) = (s ⇰ ℕ64) -> e -> 𝑂 e
substE s ⇰ ℕ64
ιs (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ 𝑂 e
eO

canonSubstElem ∷ (s ⇰ ℕ64 → e → 𝑂 e) → (e → e) → SubstElem s e → SubstElem s e
canonSubstElem :: forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e) -> SubstElem s e -> SubstElem s e
canonSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE e -> e
canonE SubstElem s e
e = (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem s ⇰ ℕ64
forall a. Null a => a
null (𝑂 e -> SubstElem s e) -> 𝑂 e -> SubstElem s e
forall a b. (a -> b) -> a -> b
$ e -> e
canonE (e -> e) -> 𝑂 e -> 𝑂 e
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e

eqSubstElem ∷ (Eq e) ⇒ (s ⇰ ℕ64 → e → 𝑂 e) → SubstElem s e → SubstElem s e → 𝔹
eqSubstElem :: forall e s.
Eq e =>
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e -> Bool
eqSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e₁ SubstElem s e
e₂ = ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e₁ 𝑂 e -> 𝑂 e -> Bool
forall a. Eq a => a -> a -> Bool
≡ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e₂

compareSubstElem ∷ (Ord e) ⇒ (s ⇰ ℕ64 → e → 𝑂 e) → SubstElem s e → SubstElem s e → Ordering
compareSubstElem :: forall e s.
Ord e =>
((s ⇰ ℕ64) -> e -> 𝑂 e)
-> SubstElem s e -> SubstElem s e -> Ordering
compareSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e₁ SubstElem s e
e₂ = ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e₁ 𝑂 e -> 𝑂 e -> Ordering
forall a. Ord a => a -> a -> Ordering
⋚ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e₂

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

substSubstElemE ∷ (s ⇰ ℕ64 → e → 𝑂 e) → SubstElem s e → 𝑂 e
substSubstElemE :: forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
substSubstElemE (s ⇰ ℕ64) -> e -> 𝑂 e
substE (SubstElem s ⇰ ℕ64
ιs 𝑂 e
eO) = (s ⇰ ℕ64) -> e -> 𝑂 e
substE s ⇰ ℕ64
ιs (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ 𝑂 e
eO

substSubstElem ∷ (s ⇰ ℕ64 → e → 𝑂 e) → SubstElem s e → SubstElem s e
substSubstElem :: forall s e.
((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
substSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE = (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem s ⇰ ℕ64
forall a. Null a => a
null (𝑂 e -> SubstElem s e)
-> (SubstElem s e -> 𝑂 e) -> SubstElem s e -> SubstElem s e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
substSubstElemE (s ⇰ ℕ64) -> e -> 𝑂 e
substE

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

instance Functor (SubstElem s) where
  map :: forall a b. (a -> b) -> SubstElem s a -> SubstElem s b
map a -> b
f (SubstElem s ⇰ ℕ64
ιs 𝑂 a
e) = (s ⇰ ℕ64) -> 𝑂 b -> SubstElem s b
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem s ⇰ ℕ64
ιs (𝑂 b -> SubstElem s b) -> 𝑂 b -> SubstElem s b
forall a b. (a -> b) -> a -> b
$ a -> b
f (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝑂 a
e

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

ppSubstElemNamed ∷ (Pretty e) ⇒ (s ⇰ ℕ64 → Doc) → SubstElem s e → Doc
ppSubstElemNamed :: forall e s. Pretty e => ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc
ppSubstElemNamed (s ⇰ ℕ64) -> Doc
ιD (SubstElem s ⇰ ℕ64
ιs 𝑂 e
eO) =
  let eD :: Doc
eD = (() -> Doc) -> (e -> Doc) -> 𝑂 e -> Doc
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (Doc -> () -> Doc
forall a b. a -> b -> a
const (Doc -> () -> Doc) -> Doc -> () -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppCon 𝕊
"⊥") e -> Doc
forall a. Pretty a => a -> Doc
pretty 𝑂 e
eO
  in
  if (s ⇰ ℕ64) -> Bool
forall a t. ToIter a t => t -> Bool
isEmpty s ⇰ ℕ64
ιs
  then Doc
eD
  else ℕ64 -> Doc -> Doc -> Doc -> Doc
ppInf ℕ64
pTOP (𝕊 -> Doc
ppPun 𝕊
"⇈") Doc
eD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> Doc
ιD s ⇰ ℕ64
ιs

instance (Pretty s,Pretty e) ⇒ Pretty (SubstElem s e) where
  pretty :: SubstElem s e -> Doc
pretty = ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc
forall e s. Pretty e => ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc
ppSubstElemNamed (s ⇰ ℕ64) -> Doc
forall a. Pretty a => a -> Doc
pretty

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

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

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

instance (Ord s,Shrinky e) ⇒ Shrinky (SubstElem s e) where
  shrink :: SubstElem s e -> 𝐼 (SubstElem s e)
shrink (SubstElem s ⇰ ℕ64
ιs 𝑂 e
eO) = do
    (s ⇰ ℕ64
ιs',𝑂 e
eO') ← (s ⇰ ℕ64, 𝑂 e) -> 𝐼 (s ⇰ ℕ64, 𝑂 e)
forall a. Shrinky a => a -> 𝐼 a
shrink (s ⇰ ℕ64
ιs,𝑂 e
eO)
    SubstElem s e -> 𝐼 (SubstElem s e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (SubstElem s e -> 𝐼 (SubstElem s e))
-> SubstElem s e -> 𝐼 (SubstElem s e)
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem s ⇰ ℕ64
ιs' 𝑂 e
eO'

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

-- e ⩴ i | ι⇈e
-- ⟦i⟧ = i
-- ⟦ι⇈e⟧ = ⟦ι⟧(e)
-- NOTE: The `Eq` instance is strictly weaker than semantic equality. To
-- compare semantic equality, you should just compare their interpretations.
data SSubstElem s e =
    Var_SSE DVar
  | Trm_SSE (SubstElem s e)
  deriving (SSubstElem s e -> SSubstElem s e -> Bool
(SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> Eq (SSubstElem s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e.
(Eq s, Eq e) =>
SSubstElem s e -> SSubstElem s e -> Bool
$c== :: forall s e.
(Eq s, Eq e) =>
SSubstElem s e -> SSubstElem s e -> Bool
== :: SSubstElem s e -> SSubstElem s e -> Bool
$c/= :: forall s e.
(Eq s, Eq e) =>
SSubstElem s e -> SSubstElem s e -> Bool
/= :: SSubstElem s e -> SSubstElem s e -> Bool
Eq,Eq (SSubstElem s e)
Eq (SSubstElem s e) =>
(SSubstElem s e -> SSubstElem s e -> Ordering)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> Bool)
-> (SSubstElem s e -> SSubstElem s e -> SSubstElem s e)
-> (SSubstElem s e -> SSubstElem s e -> SSubstElem s e)
-> Ord (SSubstElem s e)
SSubstElem s e -> SSubstElem s e -> Bool
SSubstElem s e -> SSubstElem s e -> Ordering
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (SSubstElem s e)
forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Ordering
forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
$ccompare :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Ordering
compare :: SSubstElem s e -> SSubstElem s e -> Ordering
$c< :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
< :: SSubstElem s e -> SSubstElem s e -> Bool
$c<= :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
<= :: SSubstElem s e -> SSubstElem s e -> Bool
$c> :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
> :: SSubstElem s e -> SSubstElem s e -> Bool
$c>= :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> Bool
>= :: SSubstElem s e -> SSubstElem s e -> Bool
$cmax :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
max :: SSubstElem s e -> SSubstElem s e -> SSubstElem s e
$cmin :: forall s e.
(Ord s, Ord e) =>
SSubstElem s e -> SSubstElem s e -> SSubstElem s e
min :: SSubstElem s e -> SSubstElem s e -> SSubstElem s e
Ord,Int -> SSubstElem s e -> ShowS
[SSubstElem s e] -> ShowS
SSubstElem s e -> String
(Int -> SSubstElem s e -> ShowS)
-> (SSubstElem s e -> String)
-> ([SSubstElem s e] -> ShowS)
-> Show (SSubstElem s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> SSubstElem s e -> ShowS
forall s e. (Show s, Show e) => [SSubstElem s e] -> ShowS
forall s e. (Show s, Show e) => SSubstElem s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> SSubstElem s e -> ShowS
showsPrec :: Int -> SSubstElem s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => SSubstElem s e -> String
show :: SSubstElem s e -> String
$cshowList :: forall s e. (Show s, Show e) => [SSubstElem s e] -> ShowS
showList :: [SSubstElem s e] -> ShowS
Show)

mkSSubstElem ∷ e ⌲ DVar → 𝑂 e → SSubstElem s e
mkSSubstElem :: forall e s. (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
mkSSubstElem e ⌲ DVar
ℓvar 𝑂 e
eO = case (𝑂 e ⌲ DVar) -> 𝑂 e -> 𝑂 DVar
forall a b. (a ⌲ b) -> a -> 𝑂 b
view (e ⌲ DVar
ℓvar (e ⌲ DVar) -> (𝑂 e ⌲ e) -> 𝑂 e ⌲ DVar
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ 𝑂 e ⌲ e
forall a. 𝑂 a ⌲ a
someL) 𝑂 e
eO of
  Some DVar
n → DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE DVar
n
  𝑂 DVar
None → SubstElem s e -> SSubstElem s e
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s e -> SSubstElem s e)
-> SubstElem s e -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem s ⇰ ℕ64
forall a. Null a => a
null 𝑂 e
eO

interpSSubstElem ∷ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → SSubstElem s e → 𝑂 e
interpSSubstElem :: forall e s.
(e ⌲ DVar) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> 𝑂 e
interpSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE = \case
  Var_SSE DVar
i → e -> 𝑂 e
forall a. a -> 𝑂 a
Some (e -> 𝑂 e) -> e -> 𝑂 e
forall a b. (a -> b) -> a -> b
$ (e ⌲ DVar) -> DVar -> e
forall a b. (a ⌲ b) -> b -> a
construct e ⌲ DVar
ℓvar DVar
i
  Trm_SSE SubstElem s e
e → ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e

canonSSubstElem ∷ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → (e → e) → SSubstElem s e → SSubstElem s e
canonSSubstElem :: 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 = \case
  Var_SSE DVar
n → DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE DVar
n
  Trm_SSE SubstElem s e
e → (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
forall e s. (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
mkSSubstElem e ⌲ DVar
ℓvar (𝑂 e -> SSubstElem s e) -> 𝑂 e -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ e -> e
canonE (e -> e) -> 𝑂 e -> 𝑂 e
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
interpSubstElem (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e

eqSSubstElem ∷ (Eq e) ⇒ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → SSubstElem s e → SSubstElem s e → 𝔹
eqSSubstElem :: forall e s.
Eq e =>
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e)
-> SSubstElem s e
-> SSubstElem s e
-> Bool
eqSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE SSubstElem s e
e₁ SSubstElem s e
e₂ = (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₁ 𝑂 e -> 𝑂 e -> Bool
forall a. Eq a => a -> a -> Bool
≡ (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₂

compareSSubstElem ∷ (Ord e) ⇒ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → SSubstElem s e → SSubstElem s e → Ordering
compareSSubstElem :: forall e s.
Ord e =>
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e)
-> SSubstElem s e
-> SSubstElem s e
-> Ordering
compareSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE SSubstElem s e
e₁ SSubstElem s e
e₂ = (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₁ 𝑂 e -> 𝑂 e -> Ordering
forall a. Ord a => a -> a -> Ordering
⋚ (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₂

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

substSSubstElem ∷ e ⌲ DVar → (s ⇰ ℕ64 → e → 𝑂 e) → SSubstElem s e → SSubstElem s e
substSSubstElem :: forall e s.
(e ⌲ DVar)
-> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e
substSSubstElem e ⌲ DVar
ℓvar (s ⇰ ℕ64) -> e -> 𝑂 e
substE = \case
  Var_SSE DVar
n → (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
forall e s. (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
mkSSubstElem e ⌲ DVar
ℓvar (𝑂 e -> SSubstElem s e) -> 𝑂 e -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ (s ⇰ ℕ64) -> e -> 𝑂 e
substE s ⇰ ℕ64
forall a. Null a => a
null (e -> 𝑂 e) -> e -> 𝑂 e
forall a b. (a -> b) -> a -> b
$ (e ⌲ DVar) -> DVar -> e
forall a b. (a ⌲ b) -> b -> a
construct e ⌲ DVar
ℓvar DVar
n
  Trm_SSE SubstElem s e
e → (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
forall e s. (e ⌲ DVar) -> 𝑂 e -> SSubstElem s e
mkSSubstElem e ⌲ DVar
ℓvar (𝑂 e -> SSubstElem s e) -> 𝑂 e -> SSubstElem s e
forall a b. (a -> b) -> a -> b
$ ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
forall s e. ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> 𝑂 e
substSubstElemE (s ⇰ ℕ64) -> e -> 𝑂 e
substE SubstElem s e
e

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

instance Functor (SSubstElem s) where
  map :: forall a b. (a -> b) -> SSubstElem s a -> SSubstElem s b
map a -> b
f = \case
    Var_SSE DVar
n → DVar -> SSubstElem s b
forall s e. DVar -> SSubstElem s e
Var_SSE DVar
n
    Trm_SSE SubstElem s a
e → SubstElem s b -> SSubstElem s b
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s b -> SSubstElem s b)
-> SubstElem s b -> SSubstElem s b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> SubstElem s a -> SubstElem s b
forall a b. (a -> b) -> SubstElem s a -> SubstElem s b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f SubstElem s a
e

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

ppSSubstElemNamed ∷ (Pretty e) ⇒ (s ⇰ ℕ64 → Doc) → (DVarInf → Doc) → SSubstElem s e → Doc
ppSSubstElemNamed :: forall e s.
Pretty e =>
((s ⇰ ℕ64) -> Doc) -> (DVarInf -> Doc) -> SSubstElem s e -> Doc
ppSSubstElemNamed (s ⇰ ℕ64) -> Doc
ιD DVarInf -> Doc
xD = \case
  Var_SSE DVar
n → DVarInf -> Doc
xD (DVarInf -> Doc) -> DVarInf -> Doc
forall a b. (a -> b) -> a -> b
$ DVar -> DVarInf
Var_DVI DVar
n
  Trm_SSE SubstElem s e
e → ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc
forall e s. Pretty e => ((s ⇰ ℕ64) -> Doc) -> SubstElem s e -> Doc
ppSubstElemNamed (s ⇰ ℕ64) -> Doc
ιD SubstElem s e
e

instance (Pretty s,Pretty e) ⇒ Pretty (SSubstElem s e) where
  pretty :: SSubstElem s e -> Doc
pretty = ((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
forall a. Pretty a => a -> Doc
pretty DVarInf -> Doc
forall a. Pretty a => a -> Doc
pretty

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

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

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

instance (Ord s,Shrinky e) ⇒ Shrinky (SSubstElem s e) where
  shrink :: SSubstElem s e -> 𝐼 (SSubstElem s e)
shrink = \case
    Var_SSE DVar
i → DVar -> SSubstElem s e
forall s e. DVar -> SSubstElem s e
Var_SSE (DVar -> SSubstElem s e) -> 𝐼 DVar -> 𝐼 (SSubstElem s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ DVar -> 𝐼 DVar
forall a. Shrinky a => a -> 𝐼 a
shrink DVar
i
    Trm_SSE SubstElem s e
e → SubstElem s e -> SSubstElem s e
forall s e. SubstElem s e -> SSubstElem s e
Trm_SSE (SubstElem s e -> SSubstElem s e)
-> 𝐼 (SubstElem s e) -> 𝐼 (SSubstElem s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ SubstElem s e -> 𝐼 (SubstElem s e)
forall a. Shrinky a => a -> 𝐼 a
shrink SubstElem s e
e