module UVMHS.Lib.Substitution.Substy where

import UVMHS.Core
import UVMHS.Lib.Pretty
import UVMHS.Lib.Parser
import UVMHS.Lib.Shrinky

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

-- ====== --
-- SUBSTY --
-- ====== --

-- When computing free variables, modify the standard way you would do it
-- using:
-- - `freeVarsActionFilter` (typically a global parameter) to filter out free
--    variables you don't want (e.g., by discriminating on scope `s`)
-- - `freeVarsActionScope` (local internal information) to indicate what
--   binders are in scope, e.g., free variables are those which are not bound,
--   so `⌊1⌋` is free but not `⌊0⌋` in the (nameless) lambda `λ. ⌊0⌋ ⌊1⌋`.
data FreeVarsAction s e = FreeVarsAction
  { forall s e. FreeVarsAction s e -> s -> UVar s e -> 𝔹
freeVarsActionFilter ∷ s → UVar s e → 𝔹
  , forall s e. FreeVarsAction s e -> (s ∧ SName) ⇰ ℕ64
freeVarsActionScope  ∷ s ∧ SName ⇰ ℕ64
  }
makeLenses ''FreeVarsAction

data RebindAction = ID_RA | AllNameless_RA | AllNamed_RA
  deriving (RebindAction -> RebindAction -> 𝔹
(RebindAction -> RebindAction -> 𝔹)
-> (RebindAction -> RebindAction -> 𝔹) -> Eq RebindAction
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: RebindAction -> RebindAction -> 𝔹
== :: RebindAction -> RebindAction -> 𝔹
$c/= :: RebindAction -> RebindAction -> 𝔹
/= :: RebindAction -> RebindAction -> 𝔹
Eq,Eq RebindAction
Eq RebindAction =>
(RebindAction -> RebindAction -> Ordering)
-> (RebindAction -> RebindAction -> 𝔹)
-> (RebindAction -> RebindAction -> 𝔹)
-> (RebindAction -> RebindAction -> 𝔹)
-> (RebindAction -> RebindAction -> 𝔹)
-> (RebindAction -> RebindAction -> RebindAction)
-> (RebindAction -> RebindAction -> RebindAction)
-> Ord RebindAction
RebindAction -> RebindAction -> 𝔹
RebindAction -> RebindAction -> Ordering
RebindAction -> RebindAction -> RebindAction
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: RebindAction -> RebindAction -> Ordering
compare :: RebindAction -> RebindAction -> Ordering
$c< :: RebindAction -> RebindAction -> 𝔹
< :: RebindAction -> RebindAction -> 𝔹
$c<= :: RebindAction -> RebindAction -> 𝔹
<= :: RebindAction -> RebindAction -> 𝔹
$c> :: RebindAction -> RebindAction -> 𝔹
> :: RebindAction -> RebindAction -> 𝔹
$c>= :: RebindAction -> RebindAction -> 𝔹
>= :: RebindAction -> RebindAction -> 𝔹
$cmax :: RebindAction -> RebindAction -> RebindAction
max :: RebindAction -> RebindAction -> RebindAction
$cmin :: RebindAction -> RebindAction -> RebindAction
min :: RebindAction -> RebindAction -> RebindAction
Ord,Int -> RebindAction -> ShowS
[RebindAction] -> ShowS
RebindAction -> String
(Int -> RebindAction -> ShowS)
-> (RebindAction -> String)
-> ([RebindAction] -> ShowS)
-> Show RebindAction
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RebindAction -> ShowS
showsPrec :: Int -> RebindAction -> ShowS
$cshow :: RebindAction -> String
show :: RebindAction -> String
$cshowList :: [RebindAction] -> ShowS
showList :: [RebindAction] -> ShowS
Show)

data SubstAction s e = SubstAction
  { forall s e. SubstAction s e -> RebindAction
substActionRebind ∷ RebindAction
  , forall s e. SubstAction s e -> Subst s e
substActionSubst ∷ Subst s e
  } deriving (SubstAction s e -> SubstAction s e -> 𝔹
(SubstAction s e -> SubstAction s e -> 𝔹)
-> (SubstAction s e -> SubstAction s e -> 𝔹)
-> Eq (SubstAction s e)
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
forall s e. (Eq s, Eq e) => SubstAction s e -> SubstAction s e -> 𝔹
$c== :: forall s e. (Eq s, Eq e) => SubstAction s e -> SubstAction s e -> 𝔹
== :: SubstAction s e -> SubstAction s e -> 𝔹
$c/= :: forall s e. (Eq s, Eq e) => SubstAction s e -> SubstAction s e -> 𝔹
/= :: SubstAction s e -> SubstAction s e -> 𝔹
Eq,Eq (SubstAction s e)
Eq (SubstAction s e) =>
(SubstAction s e -> SubstAction s e -> Ordering)
-> (SubstAction s e -> SubstAction s e -> 𝔹)
-> (SubstAction s e -> SubstAction s e -> 𝔹)
-> (SubstAction s e -> SubstAction s e -> 𝔹)
-> (SubstAction s e -> SubstAction s e -> 𝔹)
-> (SubstAction s e -> SubstAction s e -> SubstAction s e)
-> (SubstAction s e -> SubstAction s e -> SubstAction s e)
-> Ord (SubstAction s e)
SubstAction s e -> SubstAction s e -> 𝔹
SubstAction s e -> SubstAction s e -> Ordering
SubstAction s e -> SubstAction s e -> SubstAction s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (SubstAction s e)
forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> 𝔹
forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> Ordering
forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> SubstAction s e
$ccompare :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> Ordering
compare :: SubstAction s e -> SubstAction s e -> Ordering
$c< :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> 𝔹
< :: SubstAction s e -> SubstAction s e -> 𝔹
$c<= :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> 𝔹
<= :: SubstAction s e -> SubstAction s e -> 𝔹
$c> :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> 𝔹
> :: SubstAction s e -> SubstAction s e -> 𝔹
$c>= :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> 𝔹
>= :: SubstAction s e -> SubstAction s e -> 𝔹
$cmax :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> SubstAction s e
max :: SubstAction s e -> SubstAction s e -> SubstAction s e
$cmin :: forall s e.
(Ord s, Ord e) =>
SubstAction s e -> SubstAction s e -> SubstAction s e
min :: SubstAction s e -> SubstAction s e -> SubstAction s e
Ord,Int -> SubstAction s e -> ShowS
[SubstAction s e] -> ShowS
SubstAction s e -> String
(Int -> SubstAction s e -> ShowS)
-> (SubstAction s e -> String)
-> ([SubstAction s e] -> ShowS)
-> Show (SubstAction s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> SubstAction s e -> ShowS
forall s e. (Show s, Show e) => [SubstAction s e] -> ShowS
forall s e. (Show s, Show e) => SubstAction s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> SubstAction s e -> ShowS
showsPrec :: Int -> SubstAction s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => SubstAction s e -> String
show :: SubstAction s e -> String
$cshowList :: forall s e. (Show s, Show e) => [SubstAction s e] -> ShowS
showList :: [SubstAction s e] -> ShowS
Show)
makeLenses ''SubstAction

-- Substy things are things that support having an action in the SubstyM monad.
-- This "action" can either be a "compute free variables" action or a
-- "substition" action. This action is encoded as a parameter in the monadic
-- environment.
data SubstyAction s e =
    FreeVars_SA (FreeVarsAction s e)
  | Subst_SA (SubstAction s e)
  | MetaSubst_SA (MetaSubst s e)
makePrisms ''SubstyAction

-- instance (Pretty e, Pretty s) ⇒ Pretty (SubstAction s e) where
--   pretty (FreeVars_SA{}) = ppString "FreeVars_SA (cannot be prettified)"
--   pretty (Subst_SA sa) = pretty sa
--   pretty (MetaSubst_SA s) = pretty s

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

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

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

evalSubstM
  ∷ SubstyAction s e
  → SubstyM s e a
  → (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM :: forall s e a.
SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM SubstyAction s e
γ = ID ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall a. ID a -> a
unID (ID ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> (WriterT (s ⇰ 𝑃 (UVar s e)) ID (𝑂 a)
    -> ID ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a))
-> WriterT (s ⇰ 𝑃 (UVar s e)) ID (𝑂 a)
-> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ WriterT (s ⇰ 𝑃 (UVar s e)) ID (𝑂 a)
-> ID ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
forall o (m :: * -> *) a. WriterT o m a -> m (o ∧ a)
unWriterT (WriterT (s ⇰ 𝑃 (UVar s e)) ID (𝑂 a) -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID) a
    -> WriterT (s ⇰ 𝑃 (UVar s e)) ID (𝑂 a))
-> FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID) a
-> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID) a
-> WriterT (s ⇰ 𝑃 (UVar s e)) ID (𝑂 a)
forall (m :: * -> *) a. FailT m a -> m (𝑂 a)
unFailT (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID) a
 -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> (ReaderT
      (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)) a
    -> FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID) a)
-> ReaderT
     (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)) a
-> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyAction s e
-> ReaderT
     (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)) a
-> FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID) a
forall {k} r (m :: k -> *) (a :: k). r -> ReaderT r m a -> m a
runReaderT SubstyAction s e
γ (ReaderT
   (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)) a
 -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> (UContT
      (ReaderT
         (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
      a
    -> ReaderT
         (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)) a)
-> UContT
     (ReaderT
        (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
     a
-> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ UContT
  (ReaderT
     (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
  a
-> ReaderT
     (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)) a
forall (m :: * -> *) a. Return m => UContT m a -> m a
evalUContT (UContT
   (ReaderT
      (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
   a
 -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> (SubstyM s e a
    -> UContT
         (ReaderT
            (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
         a)
-> SubstyM s e a
-> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyM s e a
-> UContT
     (ReaderT
        (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
     a
forall s e a.
SubstyM s e a
-> UContT
     (ReaderT
        (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID)))
     a
unSubstyM

------------
-- Substy --
------------

class (SVarView s e) ⇒ Substy s e a | a→e,e→s where
  substy ∷ a → SubstyM s e a

fvssWith ∷ (Substy s e a) ⇒ (s → UVar s e → 𝔹) → a → s ⇰ 𝑃 (UVar s e)
fvssWith :: forall s e a.
Substy s e a =>
(s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
fvssWith s -> UVar s e -> 𝔹
f = ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> s ⇰ 𝑃 (UVar s e)
forall a b. (a ∧ b) -> a
fst (((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> s ⇰ 𝑃 (UVar s e))
-> (SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> SubstyM s e a
-> s ⇰ 𝑃 (UVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall s e a.
SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM (FreeVarsAction s e -> SubstyAction s e
forall s e. FreeVarsAction s e -> SubstyAction s e
FreeVars_SA (FreeVarsAction s e -> SubstyAction s e)
-> FreeVarsAction s e -> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (s -> UVar s e -> 𝔹) -> ((s ∧ SName) ⇰ ℕ64) -> FreeVarsAction s e
forall s e.
(s -> UVar s e -> 𝔹) -> ((s ∧ SName) ⇰ ℕ64) -> FreeVarsAction s e
FreeVarsAction s -> UVar s e -> 𝔹
f (s ∧ SName) ⇰ ℕ64
forall a. Null a => a
null) (SubstyM s e a -> s ⇰ 𝑃 (UVar s e))
-> (a -> SubstyM s e a) -> a -> s ⇰ 𝑃 (UVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstyM s e a
forall s e a. Substy s e a => a -> SubstyM s e a
substy

fvsWith ∷ (Ord s,Substy s e a) ⇒ s → (UVar s e → 𝔹) → a → 𝑃 (UVar s e)
fvsWith :: forall s e a.
(Ord s, Substy s e a) =>
s -> (UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e)
fvsWith s
s UVar s e -> 𝔹
f = 𝑃 (UVar s e) -> 𝑂 (𝑃 (UVar s e)) -> 𝑃 (UVar s e)
forall a. a -> 𝑂 a -> a
ifNone 𝑃 (UVar s e)
forall a. Null a => a
null (𝑂 (𝑃 (UVar s e)) -> 𝑃 (UVar s e))
-> ((s ⇰ 𝑃 (UVar s e)) -> 𝑂 (𝑃 (UVar s e)))
-> (s ⇰ 𝑃 (UVar s e))
-> 𝑃 (UVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ s -> (s ⇰ 𝑃 (UVar s e)) -> 𝑂 (𝑃 (UVar s e))
forall k v t. Lookup k v t => k -> t -> 𝑂 v
lup s
s ((s ⇰ 𝑃 (UVar s e)) -> 𝑃 (UVar s e))
-> (a -> s ⇰ 𝑃 (UVar s e)) -> a -> 𝑃 (UVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
forall s e a.
Substy s e a =>
(s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
fvssWith (\ s
s' UVar s e
x → s
s s -> s -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ s
s' 𝔹 -> 𝔹 -> 𝔹
⩓ UVar s e -> 𝔹
f UVar s e
x)

fvss ∷ (Substy s e a) ⇒ a → s ⇰ 𝑃 (UVar s e)
fvss :: forall s e a. Substy s e a => a -> s ⇰ 𝑃 (UVar s e)
fvss = (s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
forall s e a.
Substy s e a =>
(s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
fvssWith ((s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e))
-> (s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
forall a b. (a -> b) -> a -> b
$ (UVar s e -> 𝔹) -> s -> UVar s e -> 𝔹
forall a b. a -> b -> a
const ((UVar s e -> 𝔹) -> s -> UVar s e -> 𝔹)
-> (UVar s e -> 𝔹) -> s -> UVar s e -> 𝔹
forall a b. (a -> b) -> a -> b
$ 𝔹 -> UVar s e -> 𝔹
forall a b. a -> b -> a
const 𝔹
True

fvs ∷ (Ord s,Substy s e a) ⇒ s → a → 𝑃 (UVar s e)
fvs :: forall s e a. (Ord s, Substy s e a) => s -> a -> 𝑃 (UVar s e)
fvs s
s = s -> (UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e)
forall s e a.
(Ord s, Substy s e a) =>
s -> (UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e)
fvsWith s
s ((UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e))
-> (UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e)
forall a b. (a -> b) -> a -> b
$ 𝔹 -> UVar s e -> 𝔹
forall a b. a -> b -> a
const 𝔹
True

fvssMetas ∷ (Ord s,Ord e,Substy s e a) ⇒ a → s ⇰ 𝑃 (MVar s e)
fvssMetas :: forall s e a. (Ord s, Ord e, Substy s e a) => a -> s ⇰ 𝑃 (MVar s e)
fvssMetas = (𝑃 (UVar s e) -> 𝑃 (MVar s e))
-> (s ⇰ 𝑃 (UVar s e)) -> s ⇰ 𝑃 (MVar s e)
forall a b. (a -> b) -> (s ⇰ a) -> s ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝐼 (MVar s e) -> 𝑃 (MVar s e)
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 (MVar s e) -> 𝑃 (MVar s e))
-> (𝐼 (UVar s e) -> 𝐼 (MVar s e)) -> 𝐼 (UVar s e) -> 𝑃 (MVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (UVar s e -> 𝑂 (MVar s e)) -> 𝐼 (UVar s e) -> 𝐼 (MVar s e)
forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap ((UVar s e ⌲ MVar s e) -> UVar s e -> 𝑂 (MVar s e)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view UVar s e ⌲ MVar s e
forall s e. UVar s e ⌲ MVar s e
m_UVarL) (𝐼 (UVar s e) -> 𝑃 (MVar s e))
-> (𝑃 (UVar s e) -> 𝐼 (UVar s e)) -> 𝑃 (UVar s e) -> 𝑃 (MVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 (UVar s e) -> 𝐼 (UVar s e)
forall a t. ToIter a t => t -> 𝐼 a
iter) ((s ⇰ 𝑃 (UVar s e)) -> s ⇰ 𝑃 (MVar s e))
-> (a -> s ⇰ 𝑃 (UVar s e)) -> a -> s ⇰ 𝑃 (MVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
forall s e a.
Substy s e a =>
(s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
fvssWith (\ s
_s UVar s e
y → (UVar s e ⌲ MVar s e) -> UVar s e -> 𝔹
forall a b. (a ⌲ b) -> a -> 𝔹
shape UVar s e ⌲ MVar s e
forall s e. UVar s e ⌲ MVar s e
m_UVarL UVar s e
y)

fvsMetas ∷ (Ord s,Ord e,Substy s e a) ⇒ s → a → 𝑃 (MVar s e)
fvsMetas :: forall s e a.
(Ord s, Ord e, Substy s e a) =>
s -> a -> 𝑃 (MVar s e)
fvsMetas s
s = 𝑃 (MVar s e) -> 𝑂 (𝑃 (MVar s e)) -> 𝑃 (MVar s e)
forall a. a -> 𝑂 a -> a
ifNone 𝑃 (MVar s e)
forall e s. Set e s => s
pø (𝑂 (𝑃 (MVar s e)) -> 𝑃 (MVar s e))
-> ((s ⇰ 𝑃 (MVar s e)) -> 𝑂 (𝑃 (MVar s e)))
-> (s ⇰ 𝑃 (MVar s e))
-> 𝑃 (MVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ s -> (s ⇰ 𝑃 (MVar s e)) -> 𝑂 (𝑃 (MVar s e))
forall k v t. Lookup k v t => k -> t -> 𝑂 v
lup s
s ((s ⇰ 𝑃 (MVar s e)) -> 𝑃 (MVar s e))
-> (a -> s ⇰ 𝑃 (MVar s e)) -> a -> 𝑃 (MVar s e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> s ⇰ 𝑃 (MVar s e)
forall s e a. (Ord s, Ord e, Substy s e a) => a -> s ⇰ 𝑃 (MVar s e)
fvssMetas

todbr ∷ (Substy s e a) ⇒ a → 𝑂 a
todbr :: forall s e a. Substy s e a => a -> 𝑂 a
todbr = ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> SubstyM s e a
-> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall s e a.
SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM (SubstAction s e -> SubstyAction s e
forall s e. SubstAction s e -> SubstyAction s e
Subst_SA (SubstAction s e -> SubstyAction s e)
-> SubstAction s e -> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ RebindAction -> Subst s e -> SubstAction s e
forall s e. RebindAction -> Subst s e -> SubstAction s e
SubstAction RebindAction
AllNameless_RA Subst s e
forall a. Null a => a
null) (SubstyM s e a -> 𝑂 a) -> (a -> SubstyM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstyM s e a
forall s e a. Substy s e a => a -> SubstyM s e a
substy

tonmd ∷ (Substy s e a) ⇒ a → 𝑂 a
tonmd :: forall s e a. Substy s e a => a -> 𝑂 a
tonmd = ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> SubstyM s e a
-> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall s e a.
SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM (SubstAction s e -> SubstyAction s e
forall s e. SubstAction s e -> SubstyAction s e
Subst_SA (SubstAction s e -> SubstyAction s e)
-> SubstAction s e -> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ RebindAction -> Subst s e -> SubstAction s e
forall s e. RebindAction -> Subst s e -> SubstAction s e
SubstAction RebindAction
AllNamed_RA Subst s e
forall a. Null a => a
null) (SubstyM s e a -> 𝑂 a) -> (a -> SubstyM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstyM s e a
forall s e a. Substy s e a => a -> SubstyM s e a
substy

subst ∷ (Substy s e a) ⇒ Subst s e → a → 𝑂 a
subst :: forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst Subst s e
𝓈 = ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> SubstyM s e a
-> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall s e a.
SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM (SubstAction s e -> SubstyAction s e
forall s e. SubstAction s e -> SubstyAction s e
Subst_SA (SubstAction s e -> SubstyAction s e)
-> SubstAction s e -> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ RebindAction -> Subst s e -> SubstAction s e
forall s e. RebindAction -> Subst s e -> SubstAction s e
SubstAction RebindAction
ID_RA Subst s e
𝓈) (SubstyM s e a -> 𝑂 a) -> (a -> SubstyM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstyM s e a
forall s e a. Substy s e a => a -> SubstyM s e a
substy

msubst  ∷ (Substy s e a) ⇒ MetaSubst s e → a → 𝑂 a
msubst :: forall s e a. Substy s e a => MetaSubst s e -> a -> 𝑂 a
msubst MetaSubst s e
𝓈 = ((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a
forall a b. (a ∧ b) -> b
snd (((s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a) -> 𝑂 a)
-> (SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a)
-> SubstyM s e a
-> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
forall s e a.
SubstyAction s e -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 a
evalSubstM (MetaSubst s e -> SubstyAction s e
forall s e. MetaSubst s e -> SubstyAction s e
MetaSubst_SA MetaSubst s e
𝓈) (SubstyM s e a -> 𝑂 a) -> (a -> SubstyM s e a) -> a -> 𝑂 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> SubstyM s e a
forall s e a. Substy s e a => a -> SubstyM s e a
substy

------------------
-- SUBST MONOID --
------------------

canonSubst ∷ (Ord s,Eq e,Substy s e e) ⇒ (e → e) → Subst s e → Subst s e
canonSubst :: forall s e.
(Ord s, Eq e, Substy s e e) =>
(e -> e) -> Subst s e -> Subst s e
canonSubst e -> e
canonE Subst s e
𝓈 = 
  let introE :: p -> a -> 𝑂 a
introE p
ιs = Subst s e -> a -> 𝑂 a
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (Subst s e -> a -> 𝑂 a) -> Subst s e -> a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ 𝐼 (Subst s e) -> Subst s e
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (Subst s e) -> Subst s e) -> 𝐼 (Subst s e) -> Subst s e
forall a b. (a -> b) -> a -> b
$ 𝐼 ((s ∧ SName) ∧ ℕ64)
-> (((s ∧ SName) ∧ ℕ64) -> Subst s e) -> 𝐼 (Subst s e)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (p -> 𝐼 ((s ∧ SName) ∧ ℕ64)
forall a t. ToIter a t => t -> 𝐼 a
iter p
ιs) ((((s ∧ SName) ∧ ℕ64) -> Subst s e) -> 𝐼 (Subst s e))
-> (((s ∧ SName) ∧ ℕ64) -> Subst s e) -> 𝐼 (Subst s e)
forall a b. (a -> b) -> a -> b
$ \ (s
s :* SName
xO :* ℕ64
n) → case SName
xO of
        SName
D_SName → s -> ℕ64 -> Subst s e
forall s e. Ord s => s -> ℕ64 -> Subst s e
dintroSubst s
s ℕ64
n
        N_SName Name
x → s -> Name -> ℕ64 -> Subst s e
forall s e. Ord s => s -> Name -> ℕ64 -> Subst s e
nintroSubst s
s Name
x ℕ64
n
  in ((s ∧ SName) -> e ⌲ DVar)
-> (((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e)
-> (e -> e)
-> Subst s e
-> Subst s e
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) -> (s ∧ SName) -> e ⌲ DVar
forall a b c. (a -> b -> c) -> (a ∧ b) -> c
uncurry s -> SName -> e ⌲ DVar
forall s e. SVarView s e => s -> SName -> e ⌲ DVar
svarScopeL) ((s ∧ SName) ⇰ ℕ64) -> e -> 𝑂 e
forall {s} {e} {a} {p}.
(Substy s e e, Substy s e a, Ord s,
 ToIter ((s ∧ SName) ∧ ℕ64) p) =>
p -> a -> 𝑂 a
introE e -> e
canonE Subst s e
𝓈

canonMVar ∷ (Ord s,Eq e,Substy s e e) ⇒ (e → e) → MVar s e → MVar s e
canonMVar :: forall s e.
(Ord s, Eq e, Substy s e e) =>
(e -> e) -> MVar s e -> MVar s e
canonMVar e -> e
canonE (MVar Subst s e
𝓈 Name
x) = Subst s e -> Name -> MVar s e
forall s e. Subst s e -> Name -> MVar s e
MVar ((e -> e) -> Subst s e -> Subst s e
forall s e.
(Ord s, Eq e, Substy s e e) =>
(e -> e) -> Subst s e -> Subst s e
canonSubst e -> e
canonE Subst s e
𝓈) Name
x

substMVar ∷ (Ord s,Substy s e e) ⇒ Subst s e → MVar s e → MVar s e
substMVar :: forall s e.
(Ord s, Substy s e e) =>
Subst s e -> MVar s e -> MVar s e
substMVar Subst s e
𝓈 (MVar Subst s e
𝓈ₓ Name
x) = Subst s e -> Name -> MVar s e
forall s e. Subst s e -> Name -> MVar s e
MVar (Subst s e
𝓈 Subst s e -> Subst s e -> Subst s e
forall a. Append a => a -> a -> a
⧺ Subst s e
𝓈ₓ) Name
x

canonUVar ∷ (Ord s,Eq e,Substy s e e) ⇒ (e → e) → UVar s e → UVar s e
canonUVar :: forall s e.
(Ord s, Eq e, Substy s e e) =>
(e -> e) -> UVar s e -> UVar s e
canonUVar e -> e
canonE = \case
  D_UVar DVar
x → DVar -> UVar s e
forall s e. DVar -> UVar s e
D_UVar DVar
x
  N_UVar NVar
x → NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar NVar
x
  G_UVar GVar
x → GVar -> UVar s e
forall s e. GVar -> UVar s e
G_UVar GVar
x
  M_UVar MVar s e
x → MVar s e -> UVar s e
forall s e. MVar s e -> UVar s e
M_UVar (MVar s e -> UVar s e) -> MVar s e -> UVar s e
forall a b. (a -> b) -> a -> b
$ (e -> e) -> MVar s e -> MVar s e
forall s e.
(Ord s, Eq e, Substy s e e) =>
(e -> e) -> MVar s e -> MVar s e
canonMVar e -> e
canonE MVar s e
x

nullSubst ∷ Subst s e
nullSubst :: forall s e. Subst s e
nullSubst = 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) ⇰ SubstElem (s ∧ SName) e)
-> ((s ∧ SName) ⇰ SubstScoped (s ∧ SName) e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
forall a. Null a => a
null (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
forall a. Null a => a
null

appendSubst ∷ (Ord s,Substy s e e) ⇒ Subst s e → Subst s e → Subst s e
appendSubst :: forall s e.
(Ord s, Substy s e e) =>
Subst s e -> Subst s e -> Subst s e
appendSubst Subst s e
𝓈₂ Subst s e
𝓈₁ = 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)
-> (SubstSpaced (s ∧ Name) (s ∧ SName) e -> e -> 𝑂 e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) 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 ((s -> SName -> e ⌲ DVar) -> (s ∧ SName) -> e ⌲ DVar
forall a b c. (a -> b -> c) -> (a ∧ b) -> c
uncurry s -> SName -> e ⌲ DVar
forall s e. SVarView s e => s -> SName -> e ⌲ DVar
svarScopeL) (Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (Subst s e -> e -> 𝑂 e)
-> (SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> e
-> 𝑂 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst) (Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst Subst s e
𝓈₂) (SubstSpaced (s ∧ Name) (s ∧ SName) e
 -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst Subst s e
𝓈₁

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

--------------------------------------------------
-- CONCRETE IMPLEMENTATIONS OF SUBSTY INSTANCES --
--------------------------------------------------

substyDBdr ∷ (Ord s,Ord e) ⇒ s → SubstyM s e ()
substyDBdr :: forall s e. (Ord s, Ord e) => s -> SubstyM s e ()
substyDBdr s
s = (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstyAction s e -> SubstyAction s e) -> SubstyM s e ())
-> (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ [SubstyAction s e -> SubstyAction s e]
-> SubstyAction s e -> SubstyAction s e
forall a t. ToIter (a -> a) t => t -> a -> a
compose
  [ (SubstyAction s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction 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 SubstyAction s e ⌲ SubstAction s e
forall s e. SubstyAction s e ⌲ SubstAction s e
subst_SAL ((SubstAction s e -> SubstAction s e)
 -> SubstyAction s e -> SubstyAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ s -> ℕ64 -> Subst s e -> Subst s e
forall s e. Ord s => s -> ℕ64 -> Subst s e -> Subst s e
dshiftSubst s
s ℕ64
1
  , (SubstyAction s e ⌲ FreeVarsAction s e)
-> (FreeVarsAction s e -> FreeVarsAction s e)
-> SubstyAction s e
-> SubstyAction 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 SubstyAction s e ⌲ FreeVarsAction s e
forall s e. SubstyAction s e ⌲ FreeVarsAction s e
freeVars_SAL ((FreeVarsAction s e -> FreeVarsAction s e)
 -> SubstyAction s e -> SubstyAction s e)
-> (FreeVarsAction s e -> FreeVarsAction s e)
-> SubstyAction s e
-> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64))
-> (((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> FreeVarsAction s e
-> FreeVarsAction 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 FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64)
forall s e. FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64)
freeVarsActionScopeL ((((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
 -> FreeVarsAction s e -> FreeVarsAction s e)
-> (((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> FreeVarsAction s e
-> FreeVarsAction s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) ⇰ ℕ64) -> ((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall a. Append a => a -> a -> a
(⧺) (((s ∧ SName) ⇰ ℕ64) -> ((s ∧ SName) ⇰ ℕ64) -> (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
:* SName
D_SName) (s ∧ SName) -> ℕ64 -> (s ∧ SName) ⇰ ℕ64
forall a. (s ∧ SName) -> a -> (s ∧ SName) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
  ]

substyNBdr ∷ (Ord s,Ord e) ⇒ s → Name → SubstyM s e ()
substyNBdr :: forall s e. (Ord s, Ord e) => s -> Name -> SubstyM s e ()
substyNBdr s
s Name
x = (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstyAction s e -> SubstyAction s e) -> SubstyM s e ())
-> (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ [SubstyAction s e -> SubstyAction s e]
-> SubstyAction s e -> SubstyAction s e
forall a t. ToIter (a -> a) t => t -> a -> a
compose
  [ (SubstyAction s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction 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 SubstyAction s e ⌲ SubstAction s e
forall s e. SubstyAction s e ⌲ SubstAction s e
subst_SAL ((SubstAction s e -> SubstAction s e)
 -> SubstyAction s e -> SubstyAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ s -> Name -> ℕ64 -> Subst s e -> Subst s e
forall s e. Ord s => s -> Name -> ℕ64 -> Subst s e -> Subst s e
nshiftSubst s
s Name
x ℕ64
1
  , (SubstyAction s e ⌲ FreeVarsAction s e)
-> (FreeVarsAction s e -> FreeVarsAction s e)
-> SubstyAction s e
-> SubstyAction 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 SubstyAction s e ⌲ FreeVarsAction s e
forall s e. SubstyAction s e ⌲ FreeVarsAction s e
freeVars_SAL ((FreeVarsAction s e -> FreeVarsAction s e)
 -> SubstyAction s e -> SubstyAction s e)
-> (FreeVarsAction s e -> FreeVarsAction s e)
-> SubstyAction s e
-> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64))
-> (((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> FreeVarsAction s e
-> FreeVarsAction 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 FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64)
forall s e. FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64)
freeVarsActionScopeL ((((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
 -> FreeVarsAction s e -> FreeVarsAction s e)
-> (((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64)
-> FreeVarsAction s e
-> FreeVarsAction s e
forall a b. (a -> b) -> a -> b
$ ((s ∧ SName) ⇰ ℕ64) -> ((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) ⇰ ℕ64
forall a. Append a => a -> a -> a
(⧺) (((s ∧ SName) ⇰ ℕ64) -> ((s ∧ SName) ⇰ ℕ64) -> (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. (s ∧ SName) -> a -> (s ∧ SName) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
1
  ]

substyBdr ∷ (Ord s,Ord e,Substy s e e) ⇒ s → (SVar → e) → Name → SubstyM s e ()
substyBdr :: forall s e.
(Ord s, Ord e, Substy s e e) =>
s -> (SVar -> e) -> Name -> SubstyM s e ()
substyBdr s
s SVar -> e
mkVar Name
x = do
  s -> SubstyM s e ()
forall s e. (Ord s, Ord e) => s -> SubstyM s e ()
substyDBdr s
s
  s -> Name -> SubstyM s e ()
forall s e. (Ord s, Ord e) => s -> Name -> SubstyM s e ()
substyNBdr s
s Name
x
  𝑂 RebindAction
aO ← (SubstAction s e ⟢ RebindAction) -> SubstAction s e -> RebindAction
forall a b. (a ⟢ b) -> a -> b
access SubstAction s e ⟢ RebindAction
forall s e. SubstAction s e ⟢ RebindAction
substActionRebindL (SubstAction s e -> RebindAction)
-> (SubstyAction s e -> 𝑂 (SubstAction s e))
-> SubstyAction s e
-> 𝑂 RebindAction
forall (t :: * -> *) b c a.
Functor t =>
(b -> c) -> (a -> t b) -> a -> t c
^∘ (SubstyAction s e ⌲ SubstAction s e)
-> SubstyAction s e -> 𝑂 (SubstAction s e)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view SubstyAction s e ⌲ SubstAction s e
forall s e. SubstyAction s e ⌲ SubstAction s e
subst_SAL (SubstyAction s e -> 𝑂 RebindAction)
-> SubstyM s e (SubstyAction s e) -> SubstyM s e (𝑂 RebindAction)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ SubstyM s e (SubstyAction s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case 𝑂 RebindAction
aO of
    𝑂 RebindAction
None → SubstyM s e ()
forall (m :: * -> *). Return m => m ()
skip
    Some RebindAction
ID_RA → SubstyM s e ()
forall (m :: * -> *). Return m => m ()
skip
    Some RebindAction
AllNameless_RA → 
      (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstyAction s e -> SubstyAction s e) -> SubstyM s e ())
-> (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ (SubstyAction s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction 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 SubstyAction s e ⌲ SubstAction s e
forall s e. SubstyAction s e ⌲ SubstAction s e
subst_SAL ((SubstAction s e -> SubstAction s e)
 -> SubstyAction s e -> SubstyAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Subst s e -> Subst s e -> Subst s e
forall a. Append a => a -> a -> a
(⧺) (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ [Subst s e] -> Subst s e
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ s -> Name -> ℕ64 -> Subst s e
forall s e. Ord s => s -> Name -> ℕ64 -> Subst s e
nintroSubst s
s Name
x ℕ64
1
        , s -> Name -> e -> Subst s e
forall s e. Ord s => s -> Name -> e -> Subst s e
nbindSubst s
s Name
x (e -> Subst s e) -> e -> Subst s e
forall a b. (a -> b) -> a -> b
$ SVar -> e
mkVar (SVar -> e) -> SVar -> e
forall a b. (a -> b) -> a -> b
$ DVar -> SVar
D_SVar (DVar -> SVar) -> DVar -> SVar
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar ℕ64
0
        ]
    Some RebindAction
AllNamed_RA → 
      (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall (m :: * -> *) r.
(Monad m, MonadReader r m, MonadUCont m) =>
(r -> r) -> m ()
umodifyEnv ((SubstyAction s e -> SubstyAction s e) -> SubstyM s e ())
-> (SubstyAction s e -> SubstyAction s e) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ (SubstyAction s e ⌲ SubstAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction 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 SubstyAction s e ⌲ SubstAction s e
forall s e. SubstyAction s e ⌲ SubstAction s e
subst_SAL ((SubstAction s e -> SubstAction s e)
 -> SubstyAction s e -> SubstyAction s e)
-> (SubstAction s e -> SubstAction s e)
-> SubstyAction s e
-> SubstyAction s e
forall a b. (a -> b) -> a -> b
$ (SubstAction s e ⟢ Subst s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a ⟢ b) -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter SubstAction s e ⟢ Subst s e
forall s e. SubstAction s e ⟢ Subst s e
substActionSubstL ((Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e)
-> (Subst s e -> Subst s e) -> SubstAction s e -> SubstAction s e
forall a b. (a -> b) -> a -> b
$ (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Subst s e -> Subst s e -> Subst s e
forall a. Append a => a -> a -> a
(⧺) (Subst s e -> Subst s e -> Subst s e)
-> Subst s e -> Subst s e -> Subst s e
forall a b. (a -> b) -> a -> b
$ [Subst s e] -> Subst s e
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ s -> ℕ64 -> Subst s e
forall s e. Ord s => s -> ℕ64 -> Subst s e
dintroSubst s
s ℕ64
1
        , s -> e -> Subst s e
forall s e. Ord s => s -> e -> Subst s e
dbindSubst s
s (e -> Subst s e) -> e -> Subst s e
forall a b. (a -> b) -> a -> b
$ SVar -> e
mkVar (SVar -> e) -> SVar -> e
forall a b. (a -> b) -> a -> b
$ Name -> SVar
svar_Name Name
x
        ]

-- TRICKY: 
-- it should always be the case that `(mkVar n $ svarLevel x) ≈ x`
-- i.e., if `x` is an `NVar`, then `mkVar` should create named variables with
-- the same name as `x`, just with a new level.
substySVarG ∷ ∀ s e. (Ord s,Ord e,Substy s e e) ⇒ (DVar → e) → s → SVar → SubstyM s e e
substySVarG :: forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> SVar -> SubstyM s e e
substySVarG DVar -> e
mkVar s
s SVar
x = do
  let xName :: SName
xName = SVar -> SName
svarName SVar
x
      xLevel :: DVar
xLevel = SVar -> DVar
svarLevel SVar
x
  SubstyAction s e
γ ← SubstyM s e (SubstyAction s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case SubstyAction s e
γ of
    FreeVars_SA FreeVarsAction s e
a → do
      let -- `m` is the number of binders we are underneath
          m ∷ ℕ64
          m :: ℕ64
m = ℕ64 -> 𝑂 ℕ64 -> ℕ64
forall a. a -> 𝑂 a -> a
ifNone ℕ64
0 (𝑂 ℕ64 -> ℕ64) -> 𝑂 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ FreeVarsAction s e -> (s ∧ SName) ⇰ ℕ64
forall s e. FreeVarsAction s e -> (s ∧ SName) ⇰ ℕ64
freeVarsActionScope FreeVarsAction s e
a ((s ∧ SName) ⇰ ℕ64) -> (s ∧ SName) -> 𝑂 ℕ64
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
:* SName
xName)
      -- when `xLevel ≥ m` it is a free variable
      𝔹 -> (() -> SubstyM s e ()) -> SubstyM s e ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when (DVar -> ℕ64
unDVar DVar
xLevel ℕ64 -> ℕ64 -> 𝔹
forall a. Ord a => a -> a -> 𝔹
≥ ℕ64
m) ((() -> SubstyM s e ()) -> SubstyM s e ())
-> (() -> SubstyM s e ()) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ \ () → do
        let -- create the free variable to accumulate, whose variable level
            -- must be recalculated to be the found variable's level minus `m`
            y :: UVar s e
y = SVar -> UVar s e
forall s e. SVar -> UVar s e
uvar_SVar (SVar -> UVar s e) -> SVar -> UVar s e
forall a b. (a -> b) -> a -> b
$ SName -> DVar -> SVar
mkSVar SName
xName (DVar -> SVar) -> DVar -> SVar
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
xLevel ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- ℕ64
m
        -- only accumulate the free variable when it passes the filter
        𝔹 -> (() -> SubstyM s e ()) -> SubstyM s e ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when (FreeVarsAction s e -> s -> UVar s e -> 𝔹
forall s e. FreeVarsAction s e -> s -> UVar s e -> 𝔹
freeVarsActionFilter FreeVarsAction s e
a s
s UVar s e
y) ((() -> SubstyM s e ()) -> SubstyM s e ())
-> (() -> SubstyM s e ()) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ \ () →
          (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell ((s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ())
-> (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑃 (UVar s e) -> s ⇰ 𝑃 (UVar s e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ UVar s e -> 𝑃 (UVar s e)
forall a t. Single a t => a -> t
single UVar s e
y
      -- return the variable we found unchanged
      e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ DVar -> e
mkVar DVar
xLevel
    Subst_SA SubstAction s e
a → do
      let 𝓈Ss ∷ (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
          𝓈Ss :: (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
𝓈Ss = SubstSpaced (s ∧ Name) (s ∧ SName) e
-> (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
forall sG sS e. SubstSpaced sG sS e -> sS ⇰ SubstScoped sS e
substSpacedScoped (SubstSpaced (s ∧ Name) (s ∧ SName) e
 -> (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst (Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ SubstAction s e -> Subst s e
forall s e. SubstAction s e -> Subst s e
substActionSubst SubstAction s e
a
      case (s ∧ SName) ⇰ SubstScoped (s ∧ SName) e
𝓈Ss ((s ∧ SName) ⇰ SubstScoped (s ∧ SName) e)
-> (s ∧ SName) -> 𝑂 (SubstScoped (s ∧ SName) e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> SName -> s ∧ SName
forall a b. a -> b -> a ∧ b
:* SName
xName) of
        𝑂 (SubstScoped (s ∧ SName) e)
None → 
          -- there is no substitution for this scope and name
          -- return the variable we found unchanged
          e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ DVar -> e
mkVar DVar
xLevel
        Some SubstScoped (s ∧ SName) e
𝓈 → case SubstScoped (s ∧ SName) e -> DVar -> SSubstElem (s ∧ SName) e
forall s e. SubstScoped s e -> DVar -> SSubstElem s e
lookupSubstScoped SubstScoped (s ∧ SName) e
𝓈 DVar
xLevel of
          Var_SSE DVar
xLevel' → 
            -- rename the found variable to same name but new level
            e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ DVar -> e
mkVar DVar
xLevel'
          Trm_SSE (SubstElem (s ∧ SName) ⇰ ℕ64
ιs 𝑂 e
eO) → 
            -- substitute the found variable for expression `eO` with delayed
            -- increment `ιs`
            𝑂 e -> SubstyM s e e
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 e -> SubstyM s e e) -> 𝑂 e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (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
ιs) (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ 𝑂 e
eO
    MetaSubst_SA MetaSubst s e
_ → 
      -- the substitution is only looking for meta-variables, so return the
      -- found variable unchanged
      e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ DVar -> e
mkVar DVar
xLevel

substyDVar ∷ (Ord s,Ord e,Substy s e e) ⇒ (DVar → e) → s → DVar → SubstyM s e e
substyDVar :: forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> DVar -> SubstyM s e e
substyDVar DVar -> e
mkVar s
s = (DVar -> e) -> s -> SVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> SVar -> SubstyM s e e
substySVarG DVar -> e
mkVar s
s (SVar -> SubstyM s e e) -> (DVar -> SVar) -> DVar -> SubstyM s e e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ DVar -> SVar
D_SVar

substyNVar ∷ (Ord s,Ord e,Substy s e e) ⇒ (NVar → e) → s → NVar → SubstyM s e e
substyNVar :: forall s e.
(Ord s, Ord e, Substy s e e) =>
(NVar -> e) -> s -> NVar -> SubstyM s e e
substyNVar NVar -> e
mkVar s
s NVar
x = (DVar -> e) -> s -> SVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> SVar -> SubstyM s e e
substySVarG (\ DVar
n → NVar -> e
mkVar (NVar -> e) -> NVar -> e
forall a b. (a -> b) -> a -> b
$ DVar -> Name -> NVar
NVar DVar
n (Name -> NVar) -> Name -> NVar
forall a b. (a -> b) -> a -> b
$ NVar -> Name
nvarName NVar
x) s
s (SVar -> SubstyM s e e) -> SVar -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ NVar -> SVar
N_SVar NVar
x

substyGVar ∷ ∀ s e. (Ord s,Ord e,Substy s e e) ⇒ (GVar → e) → s → GVar → SubstyM s e e
substyGVar :: forall s e.
(Ord s, Ord e, Substy s e e) =>
(GVar -> e) -> s -> GVar -> SubstyM s e e
substyGVar GVar -> e
mkVar s
s GVar
x = do
  SubstyAction s e
γ ← SubstyM s e (SubstyAction s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case SubstyAction s e
γ of
    FreeVars_SA FreeVarsAction s e
a → do
      -- global variables are always free...
      -- create the free variable to accumulate
      let y :: UVar s e
y = GVar -> UVar s e
forall s e. GVar -> UVar s e
G_UVar  GVar
x
      -- only accumulate the free variable when it passes the filter
      𝔹 -> (() -> SubstyM s e ()) -> SubstyM s e ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when (FreeVarsAction s e -> s -> UVar s e -> 𝔹
forall s e. FreeVarsAction s e -> s -> UVar s e -> 𝔹
freeVarsActionFilter FreeVarsAction s e
a s
s UVar s e
y) ((() -> SubstyM s e ()) -> SubstyM s e ())
-> (() -> SubstyM s e ()) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ \ () →
        (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell ((s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ())
-> (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑃 (UVar s e) -> s ⇰ 𝑃 (UVar s e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ UVar s e -> 𝑃 (UVar s e)
forall a t. Single a t => a -> t
single UVar s e
y
      e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ GVar -> e
mkVar GVar
x
    Subst_SA SubstAction s e
𝓈A → do
      let 𝓈Gs ∷ (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
          𝓈Gs :: (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈Gs =  SubstSpaced (s ∧ Name) (s ∧ SName) e
-> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
forall sG sS e. SubstSpaced sG sS e -> sG ⇰ SubstElem sS e
substSpacedUnscoped (SubstSpaced (s ∧ Name) (s ∧ SName) e
 -> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e)
-> SubstSpaced (s ∧ Name) (s ∧ SName) e
-> (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall s e. Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
unSubst (Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e)
-> Subst s e -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall a b. (a -> b) -> a -> b
$ SubstAction s e -> Subst s e
forall s e. SubstAction s e -> Subst s e
substActionSubst SubstAction s e
𝓈A
      case (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈Gs ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e)
-> (s ∧ Name) -> 𝑂 (SubstElem (s ∧ SName) e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> Name -> s ∧ Name
forall a b. a -> b -> a ∧ b
:* GVar -> Name
unGVar GVar
x) of
        𝑂 (SubstElem (s ∧ SName) e)
None → e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ GVar -> e
mkVar GVar
x
        Some (SubstElem (s ∧ SName) ⇰ ℕ64
ιs 𝑂 e
eO) → 𝑂 e -> SubstyM s e e
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 e -> SubstyM s e e) -> 𝑂 e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (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
ιs) (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ 𝑂 e
eO
    MetaSubst_SA MetaSubst s e
_ → e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ GVar -> e
mkVar GVar
x

substySVar ∷ (Ord s,Ord e,Substy s e e) ⇒ (SVar → e) → s → SVar → SubstyM s e e
substySVar :: forall s e.
(Ord s, Ord e, Substy s e e) =>
(SVar -> e) -> s -> SVar -> SubstyM s e e
substySVar SVar -> e
mkVar s
s SVar
x = (DVar -> e) -> s -> SVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> SVar -> SubstyM s e e
substySVarG (SVar -> e
mkVar (SVar -> e) -> (DVar -> SVar) -> DVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ SName -> DVar -> SVar
mkSVar (SVar -> SName
svarName SVar
x)) s
s SVar
x

substyVar ∷ (Ord s,Ord e,Pretty e,Pretty s,Substy s e e) ⇒ (Var → e) → s → Var → SubstyM s e e
substyVar :: forall s e.
(Ord s, Ord e, Pretty e, Pretty s, Substy s e e) =>
(Var -> e) -> s -> Var -> SubstyM s e e
substyVar Var -> e
mkVar s
s = \case
  D_Var DVar
x → (DVar -> e) -> s -> DVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> DVar -> SubstyM s e e
substyDVar (Var -> e
mkVar (Var -> e) -> (DVar -> Var) -> DVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ DVar -> Var
D_Var) s
s DVar
x
  N_Var NVar
x → (NVar -> e) -> s -> NVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(NVar -> e) -> s -> NVar -> SubstyM s e e
substyNVar (Var -> e
mkVar (Var -> e) -> (NVar -> Var) -> NVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ NVar -> Var
N_Var) s
s NVar
x
  G_Var GVar
x → (GVar -> e) -> s -> GVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(GVar -> e) -> s -> GVar -> SubstyM s e e
substyGVar (Var -> e
mkVar (Var -> e) -> (GVar -> Var) -> GVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ GVar -> Var
G_Var) s
s GVar
x

substyMVar ∷ ∀ s e. (Ord s,Ord e,Pretty e,Pretty s,Substy s e e) ⇒ (MVar s e → e) → s → MVar s e → SubstyM s e e
substyMVar :: forall s e.
(Ord s, Ord e, Pretty e, Pretty s, Substy s e e) =>
(MVar s e -> e) -> s -> MVar s e -> SubstyM s e e
substyMVar MVar s e -> e
mkVar s
s MVar s e
x = do
  SubstyAction s e
γ ← SubstyM s e (SubstyAction s e)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
  case SubstyAction s e
γ of
    FreeVars_SA FreeVarsAction s e
a → do
      -- meta variables are always free...
      -- create the free variable to accumulate
      let y :: UVar s e
y = MVar s e -> UVar s e
forall s e. MVar s e -> UVar s e
M_UVar MVar s e
x
      -- only accumulate the free variable when it passes the filter
      𝔹 -> (() -> SubstyM s e ()) -> SubstyM s e ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when (FreeVarsAction s e -> s -> UVar s e -> 𝔹
forall s e. FreeVarsAction s e -> s -> UVar s e -> 𝔹
freeVarsActionFilter FreeVarsAction s e
a s
s UVar s e
y) ((() -> SubstyM s e ()) -> SubstyM s e ())
-> (() -> SubstyM s e ()) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ \ () →
        (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell ((s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ())
-> (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e ()
forall a b. (a -> b) -> a -> b
$ s
s s -> 𝑃 (UVar s e) -> s ⇰ 𝑃 (UVar s e)
forall a. s -> a -> s ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ UVar s e -> 𝑃 (UVar s e)
forall a t. Single a t => a -> t
single UVar s e
y
      e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ MVar s e -> e
mkVar MVar s e
x
    Subst_SA SubstAction s e
𝓈A → do
      let 𝓈 ∷ Subst s e
          𝓈 :: Subst s e
𝓈 = SubstAction s e -> Subst s e
forall s e. SubstAction s e -> Subst s e
substActionSubst SubstAction s e
𝓈A
      e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ MVar s e -> e
mkVar (MVar s e -> e) -> MVar s e -> e
forall a b. (a -> b) -> a -> b
$ Subst s e -> MVar s e -> MVar s e
forall s e.
(Ord s, Substy s e e) =>
Subst s e -> MVar s e -> MVar s e
substMVar Subst s e
𝓈 MVar s e
x
    MetaSubst_SA (MetaSubst (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈M) →
      case (s ∧ Name) ⇰ SubstElem (s ∧ SName) e
𝓈M ((s ∧ Name) ⇰ SubstElem (s ∧ SName) e)
-> (s ∧ Name) -> 𝑂 (SubstElem (s ∧ SName) e)
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? (s
s s -> Name -> s ∧ Name
forall a b. a -> b -> a ∧ b
:* MVar s e -> Name
forall s e. MVar s e -> Name
mvarName MVar s e
x) of
        𝑂 (SubstElem (s ∧ SName) e)
None → e -> SubstyM s e e
forall a. a -> SubstyM s e a
forall (m :: * -> *) a. Return m => a -> m a
return (e -> SubstyM s e e) -> e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ MVar s e -> e
mkVar MVar s e
x
        Some (SubstElem (s ∧ SName) ⇰ ℕ64
ιs 𝑂 e
eO) →
          𝑂 e -> SubstyM s e e
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 e -> SubstyM s e e) -> 𝑂 e -> SubstyM s e e
forall a b. (a -> b) -> a -> b
$ Subst s e -> e -> 𝑂 e
forall s e a. Substy s e a => Subst s e -> a -> 𝑂 a
subst (MVar s e -> Subst s e
forall s e. MVar s e -> Subst s e
mvarSubst MVar s e
x Subst s e -> Subst s e -> Subst s e
forall a. Append a => a -> a -> a
⧺ SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (((s ∧ SName) ⇰ ℕ64) -> SubstSpaced (s ∧ Name) (s ∧ SName) e
forall sS sG e. (sS ⇰ ℕ64) -> SubstSpaced sG sS e
introSubstSpaced (s ∧ SName) ⇰ ℕ64
ιs)) (e -> 𝑂 e) -> 𝑂 e -> 𝑂 e
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ 𝑂 e
eO

substyUVar ∷ (Ord s,Ord e,Pretty e,Pretty s,Substy s e e) ⇒ (UVar s e → e) → s → UVar s e → SubstyM s e e
substyUVar :: forall s e.
(Ord s, Ord e, Pretty e, Pretty s, Substy s e e) =>
(UVar s e -> e) -> s -> UVar s e -> SubstyM s e e
substyUVar UVar s e -> e
mkVar s
s = \case
  D_UVar DVar
x → (DVar -> e) -> s -> DVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(DVar -> e) -> s -> DVar -> SubstyM s e e
substyDVar (UVar s e -> e
mkVar (UVar s e -> e) -> (DVar -> UVar s e) -> DVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ DVar -> UVar s e
forall s e. DVar -> UVar s e
D_UVar) s
s DVar
x
  N_UVar NVar
x → (NVar -> e) -> s -> NVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(NVar -> e) -> s -> NVar -> SubstyM s e e
substyNVar (UVar s e -> e
mkVar (UVar s e -> e) -> (NVar -> UVar s e) -> NVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar) s
s NVar
x
  G_UVar GVar
x → (GVar -> e) -> s -> GVar -> SubstyM s e e
forall s e.
(Ord s, Ord e, Substy s e e) =>
(GVar -> e) -> s -> GVar -> SubstyM s e e
substyGVar (UVar s e -> e
mkVar (UVar s e -> e) -> (GVar -> UVar s e) -> GVar -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ GVar -> UVar s e
forall s e. GVar -> UVar s e
G_UVar) s
s GVar
x
  M_UVar MVar s e
x → (MVar s e -> e) -> s -> MVar s e -> SubstyM s e e
forall s e.
(Ord s, Ord e, Pretty e, Pretty s, Substy s e e) =>
(MVar s e -> e) -> s -> MVar s e -> SubstyM s e e
substyMVar (UVar s e -> e
mkVar (UVar s e -> e) -> (MVar s e -> UVar s e) -> MVar s e -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ MVar s e -> UVar s e
forall s e. MVar s e -> UVar s e
M_UVar) s
s MVar s e
x

-------------
-- PARSING --
-------------

syntaxSubst ∷ LexerBasicSyntax
syntaxSubst :: LexerBasicSyntax
syntaxSubst = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxVarInf
  , LexerBasicSyntax
forall a. Null a => a
null { lexerBasicSyntaxPuns = pow 
             [ ",","...","…"
             , "{","}","[","]"
             , "|->","↦"
             , "==","≡","+"
             ] }
  ]

syntaxMVar ∷ LexerBasicSyntax
syntaxMVar :: LexerBasicSyntax
syntaxMVar = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxSubst
  , LexerBasicSyntax
forall a. Null a => a
null { lexerBasicSyntaxPuns = pow 
             [ ":m"
             ] }
  ]

syntaxUVar ∷ LexerBasicSyntax
syntaxUVar :: LexerBasicSyntax
syntaxUVar = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxVar
  , LexerBasicSyntax
syntaxMVar
  ]

data ParseSubstAction e = ParseSubstAction
  { forall e. ParseSubstAction e -> 𝐼 ℕ64
parseSubstActionShfts ∷ 𝐼 ℕ64          -- x:0…x:n ↦ [≡]
  , forall e. ParseSubstAction e -> 𝑂 DVar ⇰ 𝐼 e
parseSubstActionElems ∷ 𝑂 DVar ⇰ 𝐼 e   -- x:n     ↦ e
  , forall e. ParseSubstAction e -> 𝐼 (ℕ64 ∧ ℤ64)
parseSubstActionIncrs ∷ 𝐼 (ℕ64 ∧ ℤ64)  -- x:n…x:∞ ↦ i
  } deriving (ParseSubstAction e -> ParseSubstAction e -> 𝔹
(ParseSubstAction e -> ParseSubstAction e -> 𝔹)
-> (ParseSubstAction e -> ParseSubstAction e -> 𝔹)
-> Eq (ParseSubstAction e)
forall e. Eq e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
forall a. (a -> a -> 𝔹) -> (a -> a -> 𝔹) -> Eq a
$c== :: forall e. Eq e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
== :: ParseSubstAction e -> ParseSubstAction e -> 𝔹
$c/= :: forall e. Eq e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
/= :: ParseSubstAction e -> ParseSubstAction e -> 𝔹
Eq,Eq (ParseSubstAction e)
Eq (ParseSubstAction e) =>
(ParseSubstAction e -> ParseSubstAction e -> Ordering)
-> (ParseSubstAction e -> ParseSubstAction e -> 𝔹)
-> (ParseSubstAction e -> ParseSubstAction e -> 𝔹)
-> (ParseSubstAction e -> ParseSubstAction e -> 𝔹)
-> (ParseSubstAction e -> ParseSubstAction e -> 𝔹)
-> (ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e)
-> (ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e)
-> Ord (ParseSubstAction e)
ParseSubstAction e -> ParseSubstAction e -> 𝔹
ParseSubstAction e -> ParseSubstAction e -> Ordering
ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> 𝔹)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall e. Ord e => Eq (ParseSubstAction e)
forall e. Ord e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
forall e.
Ord e =>
ParseSubstAction e -> ParseSubstAction e -> Ordering
forall e.
Ord e =>
ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
$ccompare :: forall e.
Ord e =>
ParseSubstAction e -> ParseSubstAction e -> Ordering
compare :: ParseSubstAction e -> ParseSubstAction e -> Ordering
$c< :: forall e. Ord e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
< :: ParseSubstAction e -> ParseSubstAction e -> 𝔹
$c<= :: forall e. Ord e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
<= :: ParseSubstAction e -> ParseSubstAction e -> 𝔹
$c> :: forall e. Ord e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
> :: ParseSubstAction e -> ParseSubstAction e -> 𝔹
$c>= :: forall e. Ord e => ParseSubstAction e -> ParseSubstAction e -> 𝔹
>= :: ParseSubstAction e -> ParseSubstAction e -> 𝔹
$cmax :: forall e.
Ord e =>
ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
max :: ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
$cmin :: forall e.
Ord e =>
ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
min :: ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
Ord,Int -> ParseSubstAction e -> ShowS
[ParseSubstAction e] -> ShowS
ParseSubstAction e -> String
(Int -> ParseSubstAction e -> ShowS)
-> (ParseSubstAction e -> String)
-> ([ParseSubstAction e] -> ShowS)
-> Show (ParseSubstAction e)
forall e. Show e => Int -> ParseSubstAction e -> ShowS
forall e. Show e => [ParseSubstAction e] -> ShowS
forall e. Show e => ParseSubstAction e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall e. Show e => Int -> ParseSubstAction e -> ShowS
showsPrec :: Int -> ParseSubstAction e -> ShowS
$cshow :: forall e. Show e => ParseSubstAction e -> String
show :: ParseSubstAction e -> String
$cshowList :: forall e. Show e => [ParseSubstAction e] -> ShowS
showList :: [ParseSubstAction e] -> ShowS
Show)
makeLenses ''ParseSubstAction

parseSubstActionShft ∷ ℕ64 → ParseSubstAction e
parseSubstActionShft :: forall e. ℕ64 -> ParseSubstAction e
parseSubstActionShft ℕ64
n = ParseSubstAction e
forall a. Null a => a
null { parseSubstActionShfts = single n }

parseSubstActionElem ∷ 𝑂 DVar → e → ParseSubstAction e
parseSubstActionElem :: forall e. 𝑂 DVar -> e -> ParseSubstAction e
parseSubstActionElem 𝑂 DVar
nO e
e = ParseSubstAction Any
forall a. Null a => a
null { parseSubstActionElems = nO ↦ single e }

parseSubstActionIncr ∷ ℕ64 → ℤ64 → ParseSubstAction e
parseSubstActionIncr :: forall e. ℕ64 -> ℤ64 -> ParseSubstAction e
parseSubstActionIncr ℕ64
n ℤ64
i = ParseSubstAction e
forall a. Null a => a
null { parseSubstActionIncrs = single $ n :* i }

instance Null (ParseSubstAction e) where
  null :: ParseSubstAction e
null = 𝐼 ℕ64 -> (𝑂 DVar ⇰ 𝐼 e) -> 𝐼 (ℕ64 ∧ ℤ64) -> ParseSubstAction e
forall e.
𝐼 ℕ64 -> (𝑂 DVar ⇰ 𝐼 e) -> 𝐼 (ℕ64 ∧ ℤ64) -> ParseSubstAction e
ParseSubstAction 𝐼 ℕ64
forall a. Null a => a
null 𝑂 DVar ⇰ 𝐼 e
forall a. Null a => a
null 𝐼 (ℕ64 ∧ ℤ64)
forall a. Null a => a
null
instance Append (ParseSubstAction e) where
  ParseSubstAction 𝐼 ℕ64
shfts₁ 𝑂 DVar ⇰ 𝐼 e
elems₁ 𝐼 (ℕ64 ∧ ℤ64)
incrs₁ ⧺ :: ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e
⧺ ParseSubstAction 𝐼 ℕ64
shfts₂ 𝑂 DVar ⇰ 𝐼 e
elems₂ 𝐼 (ℕ64 ∧ ℤ64)
incrs₂ =
    𝐼 ℕ64 -> (𝑂 DVar ⇰ 𝐼 e) -> 𝐼 (ℕ64 ∧ ℤ64) -> ParseSubstAction e
forall e.
𝐼 ℕ64 -> (𝑂 DVar ⇰ 𝐼 e) -> 𝐼 (ℕ64 ∧ ℤ64) -> ParseSubstAction e
ParseSubstAction (𝐼 ℕ64
shfts₁ 𝐼 ℕ64 -> 𝐼 ℕ64 -> 𝐼 ℕ64
forall a. Append a => a -> a -> a
⧺ 𝐼 ℕ64
shfts₂) (𝑂 DVar ⇰ 𝐼 e
elems₁ (𝑂 DVar ⇰ 𝐼 e) -> (𝑂 DVar ⇰ 𝐼 e) -> 𝑂 DVar ⇰ 𝐼 e
forall a. Append a => a -> a -> a
⧺ 𝑂 DVar ⇰ 𝐼 e
elems₂) (𝐼 (ℕ64 ∧ ℤ64) -> ParseSubstAction e)
-> 𝐼 (ℕ64 ∧ ℤ64) -> ParseSubstAction e
forall a b. (a -> b) -> a -> b
$ 𝐼 (ℕ64 ∧ ℤ64)
incrs₁ 𝐼 (ℕ64 ∧ ℤ64) -> 𝐼 (ℕ64 ∧ ℤ64) -> 𝐼 (ℕ64 ∧ ℤ64)
forall a. Append a => a -> a -> a
⧺ 𝐼 (ℕ64 ∧ ℤ64)
incrs₂
instance Monoid (ParseSubstAction e)

type ParseSubstActions e = SGName ⇰ ParseSubstAction e

pSubst ∷ ∀ e. (Eq e,Substy () e e) ⇒ (() → CParser TokenBasic e) → CParser TokenBasic (Subst () e)
pSubst :: forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e) -> CParser TokenBasic (Subst () e)
pSubst () -> CParser TokenBasic e
pE = Text
-> CParser TokenBasic (Subst () e)
-> CParser TokenBasic (Subst () e)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpNewContext Text
"subst" (CParser TokenBasic (Subst () e)
 -> CParser TokenBasic (Subst () e))
-> CParser TokenBasic (Subst () e)
-> CParser TokenBasic (Subst () e)
forall a b. (a -> b) -> a -> b
$ do
  let pSubstIncr ∷ Var → CParser TokenBasic (ParseSubstActions e)
      pSubstIncr :: Var -> CParser TokenBasic (ParseSubstActions e)
pSubstIncr Var
x₁ = do
        CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic)
-> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a b. (a -> b) -> a -> b
$ (Text -> CParser TokenBasic TokenBasic)
-> [Text] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Text -> CParser TokenBasic TokenBasic
cpSyntax [Text
"...",Text
"…"]
        VarInf
x₂ ← Text -> CParser TokenBasic VarInf -> CParser TokenBasic VarInf
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"parsing varinf" CParser TokenBasic VarInf
pVarInf
        CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic)
-> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a b. (a -> b) -> a -> b
$ (Text -> CParser TokenBasic TokenBasic)
-> [Text] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Text -> CParser TokenBasic TokenBasic
cpSyntax [Text
"|->",Text
"↦"]
        CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic)
-> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a b. (a -> b) -> a -> b
$ (Text -> CParser TokenBasic TokenBasic)
-> [Text] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Text -> CParser TokenBasic TokenBasic
cpSyntax [Text
"["]
        ℤ64
i ← Text -> CParser TokenBasic ℤ64 -> CParser TokenBasic ℤ64
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"valid subst shift/incr update" (CParser TokenBasic ℤ64 -> CParser TokenBasic ℤ64)
-> CParser TokenBasic ℤ64 -> CParser TokenBasic ℤ64
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic ℤ64] -> CParser TokenBasic ℤ64
forall a t. (Monoid a, ToIter a t) => t -> a
concat
          [ do CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic)
-> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a b. (a -> b) -> a -> b
$ (Text -> CParser TokenBasic TokenBasic)
-> [Text] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Text -> CParser TokenBasic TokenBasic
cpSyntax [Text
"==",Text
"≡"]
               ℤ64 -> CParser TokenBasic ℤ64
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return ℤ64
0
          , do ℤ64
i ← CParser TokenBasic ℤ64
cpInt64
               𝔹 -> CParser TokenBasic ()
forall t. 𝔹 -> CParser t ()
cpGuard (𝔹 -> CParser TokenBasic ()) -> 𝔹 -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ ℤ64
i ℤ64 -> ℤ64 -> 𝔹
forall a. Ord a => a -> a -> 𝔹
< ℤ64
0
               ℤ64 -> CParser TokenBasic ℤ64
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return ℤ64
i
          , do CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ Text -> CParser TokenBasic TokenBasic
cpSyntax Text
"+"
               ℤ64
i ← CParser TokenBasic ℤ64
cpInt64
               𝔹 -> CParser TokenBasic ()
forall t. 𝔹 -> CParser t ()
cpGuard (𝔹 -> CParser TokenBasic ()) -> 𝔹 -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ ℤ64
i ℤ64 -> ℤ64 -> 𝔹
forall a. Ord a => a -> a -> 𝔹
> ℤ64
0
               ℤ64 -> CParser TokenBasic ℤ64
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return ℤ64
i
          ]
        ParseSubstActions e
a ← Text
-> CParser TokenBasic (ParseSubstActions e)
-> CParser TokenBasic (ParseSubstActions e)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"valid subst shift/incr range" (CParser TokenBasic (ParseSubstActions e)
 -> CParser TokenBasic (ParseSubstActions e))
-> CParser TokenBasic (ParseSubstActions e)
-> CParser TokenBasic (ParseSubstActions e)
forall a b. (a -> b) -> a -> b
$ case (Var
x₁,VarInf
x₂) of
          (D_Var(DVar ℕ64
n)         ,D_VarInf(Var_DVI(DVar ℕ64
n'))             ) | ℕ64
nℕ64 -> ℕ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ℕ64
0,ℤ64
iℤ64 -> ℤ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ℤ64
0      → ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e))
-> ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a b. (a -> b) -> a -> b
$ SGName
D_SGName    SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64 -> ParseSubstAction e
forall e. ℕ64 -> ParseSubstAction e
parseSubstActionShft (ℕ64
n' ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
1)
          (N_Var(NVar (DVar ℕ64
n) Name
x),N_VarInf(NVarInf(Var_DVI (DVar ℕ64
n')) Name
x')) | ℕ64
nℕ64 -> ℕ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ℕ64
0,ℤ64
iℤ64 -> ℤ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ℤ64
0,Name
xName -> Name -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡Name
x' → ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e))
-> ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a b. (a -> b) -> a -> b
$ Name -> SGName
N_SGName Name
x' SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64 -> ParseSubstAction e
forall e. ℕ64 -> ParseSubstAction e
parseSubstActionShft (ℕ64
n' ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
1)
          (D_Var(DVar ℕ64
n)         ,D_VarInf DVarInf
Inf_DVI                       )                → ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e))
-> ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a b. (a -> b) -> a -> b
$ SGName
D_SGName    SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64 -> ℤ64 -> ParseSubstAction e
forall e. ℕ64 -> ℤ64 -> ParseSubstAction e
parseSubstActionIncr ℕ64
n ℤ64
i
          (N_Var(NVar (DVar ℕ64
n) Name
x),N_VarInf(NVarInf DVarInf
Inf_DVI Name
x')           ) |         Name
xName -> Name -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡Name
x' → ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e))
-> ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a b. (a -> b) -> a -> b
$ Name -> SGName
N_SGName Name
x' SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64 -> ℤ64 -> ParseSubstAction e
forall e. ℕ64 -> ℤ64 -> ParseSubstAction e
parseSubstActionIncr ℕ64
n ℤ64
i
          (Var, VarInf)
_ → CParser TokenBasic (ParseSubstActions e)
forall t a. CParser t a
cpDie
        CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic)
-> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a b. (a -> b) -> a -> b
$ (Text -> CParser TokenBasic TokenBasic)
-> [Text] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Text -> CParser TokenBasic TokenBasic
cpSyntax [Text
"]"]
        ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return ParseSubstActions e
a
      pSubstElem ∷ Var → CParser TokenBasic (ParseSubstActions e)
      pSubstElem :: Var -> CParser TokenBasic (ParseSubstActions e)
pSubstElem Var
x₀ = do
        CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic)
-> [CParser TokenBasic TokenBasic] -> CParser TokenBasic TokenBasic
forall a b. (a -> b) -> a -> b
$ (Text -> CParser TokenBasic TokenBasic)
-> [Text] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Text -> CParser TokenBasic TokenBasic
cpSyntax [Text
"|->",Text
"↦"]
        e
e ← () -> CParser TokenBasic e
pE ()
        ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e))
-> ParseSubstActions e -> CParser TokenBasic (ParseSubstActions e)
forall a b. (a -> b) -> a -> b
$ case Var
x₀ of
          D_Var DVar
n          → SGName
D_SGName   SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝑂 DVar -> e -> ParseSubstAction e
forall e. 𝑂 DVar -> e -> ParseSubstAction e
parseSubstActionElem (DVar -> 𝑂 DVar
forall a. a -> 𝑂 a
Some DVar
n) e
e
          N_Var (NVar DVar
n Name
x) → Name -> SGName
N_SGName Name
x SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝑂 DVar -> e -> ParseSubstAction e
forall e. 𝑂 DVar -> e -> ParseSubstAction e
parseSubstActionElem (DVar -> 𝑂 DVar
forall a. a -> 𝑂 a
Some DVar
n) e
e
          G_Var (GVar Name
x)   → Name -> SGName
G_SGName Name
x SGName -> ParseSubstAction e -> ParseSubstActions e
forall a. SGName -> a -> SGName ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ 𝑂 DVar -> e -> ParseSubstAction e
forall e. 𝑂 DVar -> e -> ParseSubstAction e
parseSubstActionElem 𝑂 DVar
forall a. 𝑂 a
None     e
e
  CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ Text -> CParser TokenBasic TokenBasic
cpSyntax Text
"{"
  ParseSubstActions e
xas ← 𝐿 (ParseSubstActions e) -> ParseSubstActions e
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐿 (ParseSubstActions e) -> ParseSubstActions e)
-> CParser TokenBasic (𝐿 (ParseSubstActions e))
-> CParser TokenBasic (ParseSubstActions e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic ()
-> CParser TokenBasic (ParseSubstActions e)
-> CParser TokenBasic (𝐿 (ParseSubstActions e))
forall t a. Ord t => CParser t () -> CParser t a -> CParser t (𝐿 a)
cpManySepBy (CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ Text -> CParser TokenBasic TokenBasic
cpSyntax Text
",") (CParser TokenBasic (ParseSubstActions e)
 -> CParser TokenBasic (𝐿 (ParseSubstActions e)))
-> CParser TokenBasic (ParseSubstActions e)
-> CParser TokenBasic (𝐿 (ParseSubstActions e))
forall a b. (a -> b) -> a -> b
$ do
    Var
x ← CParser TokenBasic Var
pVar
    [CParser TokenBasic (ParseSubstActions e)]
-> CParser TokenBasic (ParseSubstActions e)
forall a t. (Monoid a, ToIter a t) => t -> a
concat 
      [ Var -> CParser TokenBasic (ParseSubstActions e)
pSubstIncr Var
x
      , Var -> CParser TokenBasic (ParseSubstActions e)
pSubstElem Var
x
      ]
  Subst () e
𝓈 ← Text
-> CParser TokenBasic (Subst () e)
-> CParser TokenBasic (Subst () e)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"all subst actions valid" (CParser TokenBasic (Subst () e)
 -> CParser TokenBasic (Subst () e))
-> CParser TokenBasic (Subst () e)
-> CParser TokenBasic (Subst () e)
forall a b. (a -> b) -> a -> b
$
   𝐼 (Subst () e) -> Subst () e
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (Subst () e) -> Subst () e)
-> CParser TokenBasic (𝐼 (Subst () e))
-> CParser TokenBasic (Subst () e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝐼 (SGName ∧ ParseSubstAction e)
-> ((SGName ∧ ParseSubstAction e)
    -> CParser TokenBasic (Subst () e))
-> CParser TokenBasic (𝐼 (Subst () e))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn (ParseSubstActions e -> 𝐼 (SGName ∧ ParseSubstAction e)
forall a t. ToIter a t => t -> 𝐼 a
iter ParseSubstActions e
xas) (((SGName ∧ ParseSubstAction e) -> CParser TokenBasic (Subst () e))
 -> CParser TokenBasic (𝐼 (Subst () e)))
-> ((SGName ∧ ParseSubstAction e)
    -> CParser TokenBasic (Subst () e))
-> CParser TokenBasic (𝐼 (Subst () e))
forall a b. (a -> b) -> a -> b
$ \ (SGName
wbO :* ParseSubstAction 𝐼 ℕ64
shfts 𝑂 DVar ⇰ 𝐼 e
elemss 𝐼 (ℕ64 ∧ ℤ64)
incrs) → do
    let doScoped :: CParser TokenBasic ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
doScoped = do 
          -- should only have zero or one shift
          ℕ64
nShft ∷ ℕ64  
                ← Text -> CParser TokenBasic ℕ64 -> CParser TokenBasic ℕ64
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"zero or one shift actions" (CParser TokenBasic ℕ64 -> CParser TokenBasic ℕ64)
-> CParser TokenBasic ℕ64 -> CParser TokenBasic ℕ64
forall a b. (a -> b) -> a -> b
$ 𝑂 ℕ64 -> CParser TokenBasic ℕ64
forall a t. 𝑂 a -> CParser t a
cpFailEff (𝑂 ℕ64 -> CParser TokenBasic ℕ64)
-> 𝑂 ℕ64 -> CParser TokenBasic ℕ64
forall a b. (a -> b) -> a -> b
$ [𝑂 ℕ64] -> 𝑂 ℕ64
forall (m :: * -> *) a t.
(Monad m, MonadFail m, ToIter (m a) t) =>
t -> m a
tries
            [ do (𝐼 ℕ64 ⌲ ()) -> 𝐼 ℕ64 -> 𝑂 ()
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐼 ℕ64 ⌲ ()
forall a. 𝐼 a ⌲ ()
empty𝐼L 𝐼 ℕ64
shfts ; ℕ64 -> 𝑂 ℕ64
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return ℕ64
0
            , (𝐼 ℕ64 ⌲ ℕ64) -> 𝐼 ℕ64 -> 𝑂 ℕ64
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐼 ℕ64 ⌲ ℕ64
forall a. 𝐼 a ⌲ a
single𝐼L 𝐼 ℕ64
shfts
            ]
          -- elems should map names to only one element
          𝑂 DVar ⇰ e
elems ∷ 𝑂 DVar ⇰ e
                ← Text
-> CParser TokenBasic (𝑂 DVar ⇰ e)
-> CParser TokenBasic (𝑂 DVar ⇰ e)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"one bind per name (scoped)" (CParser TokenBasic (𝑂 DVar ⇰ e)
 -> CParser TokenBasic (𝑂 DVar ⇰ e))
-> CParser TokenBasic (𝑂 DVar ⇰ e)
-> CParser TokenBasic (𝑂 DVar ⇰ e)
forall a b. (a -> b) -> a -> b
$ 𝑂 (𝑂 DVar ⇰ e) -> CParser TokenBasic (𝑂 DVar ⇰ e)
forall a t. 𝑂 a -> CParser t a
cpFailEff (𝑂 (𝑂 DVar ⇰ e) -> CParser TokenBasic (𝑂 DVar ⇰ e))
-> 𝑂 (𝑂 DVar ⇰ e) -> CParser TokenBasic (𝑂 DVar ⇰ e)
forall a b. (a -> b) -> a -> b
$ (𝑂 DVar ⇰ 𝐼 e) -> (𝐼 e -> 𝑂 e) -> 𝑂 (𝑂 DVar ⇰ e)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝑂 DVar ⇰ 𝐼 e
elemss ((𝐼 e -> 𝑂 e) -> 𝑂 (𝑂 DVar ⇰ e)) -> (𝐼 e -> 𝑂 e) -> 𝑂 (𝑂 DVar ⇰ e)
forall a b. (a -> b) -> a -> b
$ (𝐼 e ⌲ e) -> 𝐼 e -> 𝑂 e
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐼 e ⌲ e
forall a. 𝐼 a ⌲ a
single𝐼L
          -- all names of element bindings should have an index
          𝐼 DVar
elemsKeys ∷ 𝐼 DVar
                    ← Text -> CParser TokenBasic (𝐼 DVar) -> CParser TokenBasic (𝐼 DVar)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"all variables must have index" (CParser TokenBasic (𝐼 DVar) -> CParser TokenBasic (𝐼 DVar))
-> CParser TokenBasic (𝐼 DVar) -> CParser TokenBasic (𝐼 DVar)
forall a b. (a -> b) -> a -> b
$ 𝑂 (𝐼 DVar) -> CParser TokenBasic (𝐼 DVar)
forall a t. 𝑂 a -> CParser t a
cpFailEff (𝑂 (𝐼 DVar) -> CParser TokenBasic (𝐼 DVar))
-> 𝑂 (𝐼 DVar) -> CParser TokenBasic (𝐼 DVar)
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝑂 DVar) -> 𝑂 (𝐼 DVar)
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange (𝐼 (𝑂 DVar) -> 𝑂 (𝐼 DVar)) -> 𝐼 (𝑂 DVar) -> 𝑂 (𝐼 DVar)
forall a b. (a -> b) -> a -> b
$ 𝑃 (𝑂 DVar) -> 𝐼 (𝑂 DVar)
forall a t. ToIter a t => t -> 𝐼 a
iter (𝑃 (𝑂 DVar) -> 𝐼 (𝑂 DVar)) -> 𝑃 (𝑂 DVar) -> 𝐼 (𝑂 DVar)
forall a b. (a -> b) -> a -> b
$ (𝑂 DVar ⇰ e) -> 𝑃 (𝑂 DVar)
forall a. (𝑂 DVar ⇰ a) -> 𝑃 (𝑂 DVar)
forall k s (d :: * -> *) a. Dict k s d => d a -> s
dkeys 𝑂 DVar ⇰ e
elems
          let elemsVals ∷ 𝕍 e
              elemsVals :: 𝕍 e
elemsVals = 𝐼 e -> 𝕍 e
forall a t. ToIter a t => t -> 𝕍 a
vec (𝐼 e -> 𝕍 e) -> 𝐼 e -> 𝕍 e
forall a b. (a -> b) -> a -> b
$ (𝑂 DVar ⇰ e) -> 𝐼 e
forall a. (𝑂 DVar ⇰ a) -> 𝐼 a
forall k s (d :: * -> *) a. Dict k s d => d a -> 𝐼 a
dvals 𝑂 DVar ⇰ e
elems
          -- should only have zero or one increment
          ℕ64
nIncr :* ℤ64
iIncr ∷ ℕ64 ∧ ℤ64
                         ← Text
-> CParser TokenBasic (ℕ64 ∧ ℤ64) -> CParser TokenBasic (ℕ64 ∧ ℤ64)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"zero or one incr actions" (CParser TokenBasic (ℕ64 ∧ ℤ64) -> CParser TokenBasic (ℕ64 ∧ ℤ64))
-> CParser TokenBasic (ℕ64 ∧ ℤ64) -> CParser TokenBasic (ℕ64 ∧ ℤ64)
forall a b. (a -> b) -> a -> b
$ 𝑂 (ℕ64 ∧ ℤ64) -> CParser TokenBasic (ℕ64 ∧ ℤ64)
forall a t. 𝑂 a -> CParser t a
cpFailEff (𝑂 (ℕ64 ∧ ℤ64) -> CParser TokenBasic (ℕ64 ∧ ℤ64))
-> 𝑂 (ℕ64 ∧ ℤ64) -> CParser TokenBasic (ℕ64 ∧ ℤ64)
forall a b. (a -> b) -> a -> b
$ [𝑂 (ℕ64 ∧ ℤ64)] -> 𝑂 (ℕ64 ∧ ℤ64)
forall (m :: * -> *) a t.
(Monad m, MonadFail m, ToIter (m a) t) =>
t -> m a
tries
            [ do (𝐼 (ℕ64 ∧ ℤ64) ⌲ ()) -> 𝐼 (ℕ64 ∧ ℤ64) -> 𝑂 ()
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐼 (ℕ64 ∧ ℤ64) ⌲ ()
forall a. 𝐼 a ⌲ ()
empty𝐼L 𝐼 (ℕ64 ∧ ℤ64)
incrs ; (ℕ64 ∧ ℤ64) -> 𝑂 (ℕ64 ∧ ℤ64)
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return ((ℕ64 ∧ ℤ64) -> 𝑂 (ℕ64 ∧ ℤ64)) -> (ℕ64 ∧ ℤ64) -> 𝑂 (ℕ64 ∧ ℤ64)
forall a b. (a -> b) -> a -> b
$ (ℕ64
nShft ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ 𝕍 e -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 e
elemsVals) ℕ64 -> ℤ64 -> ℕ64 ∧ ℤ64
forall a b. a -> b -> a ∧ b
:* ℤ64
0
            , (𝐼 (ℕ64 ∧ ℤ64) ⌲ (ℕ64 ∧ ℤ64)) -> 𝐼 (ℕ64 ∧ ℤ64) -> 𝑂 (ℕ64 ∧ ℤ64)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐼 (ℕ64 ∧ ℤ64) ⌲ (ℕ64 ∧ ℤ64)
forall a. 𝐼 a ⌲ a
single𝐼L 𝐼 (ℕ64 ∧ ℤ64)
incrs
            ]
          -- element bindings should fill gap between shift and incr
          Text -> CParser TokenBasic () -> CParser TokenBasic ()
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"elements should fill gap" (CParser TokenBasic () -> CParser TokenBasic ())
-> CParser TokenBasic () -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ 𝔹 -> CParser TokenBasic ()
forall t. 𝔹 -> CParser t ()
cpGuard (𝔹 -> CParser TokenBasic ()) -> 𝔹 -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ (DVar -> ℕ64) -> 𝐼 DVar -> 𝐼 ℕ64
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map DVar -> ℕ64
unDVar 𝐼 DVar
elemsKeys 𝐼 ℕ64 -> 𝐼 ℕ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ64 -> ℕ64 -> 𝐼 ℕ64
forall n. (Eq n, Additive n, One n, Minus n) => n -> n -> 𝐼 n
range ℕ64
nShft ℕ64
nIncr
          -- biding N elements creates a -N incr
          -- target incr I = -N + E for extra incr E
          -- so E = I+N
          -- target incr I shouldn't be less than -N
          -- so E should be nonnegative
          -- let numElems = nIncr - nShft
          𝔹 -> (() -> CParser TokenBasic ()) -> CParser TokenBasic ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when (ℤ64
iIncr ℤ64 -> ℤ64 -> 𝔹
forall a. Ord a => a -> a -> 𝔹
< ℤ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
$ 𝕍 e -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝕍 e
elemsVals)) ((() -> CParser TokenBasic ()) -> CParser TokenBasic ())
-> (() -> CParser TokenBasic ()) -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ \ () →
            Text -> CParser TokenBasic () -> CParser TokenBasic ()
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"incr cannot be less than number of substitution elems" CParser TokenBasic ()
forall t a. CParser t a
cpDie
          let elemsVals' ∷ 𝕍 (SSubstElem s e)
              elemsVals' :: forall s. 𝕍 (SSubstElem s e)
elemsVals' = 𝕍 e -> (e -> SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝕍 e
elemsVals ((e -> SSubstElem s e) -> 𝕍 (SSubstElem s e))
-> (e -> SSubstElem s e) -> 𝕍 (SSubstElem s e)
forall a b. (a -> b) -> a -> b
$ 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
          ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
-> CParser TokenBasic ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
 -> CParser
      TokenBasic ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64))
-> ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
-> CParser TokenBasic ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
forall a b. (a -> b) -> a -> b
$ ℕ64
nShft ℕ64
-> 𝕍 (SSubstElem (() ∧ SName) e)
-> ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)
forall a b. a -> b -> a ∧ b
:* 𝕍 (SSubstElem (() ∧ SName) e)
forall s. 𝕍 (SSubstElem s e)
elemsVals' (ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e))
-> ℤ64 -> (ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64
forall a b. a -> b -> a ∧ b
:* ℤ64
iIncr
    case SGName
wbO of
      -- nameless
      SGName
D_SGName → do
        ℕ64
nShft :* 𝕍 (SSubstElem (() ∧ SName) e)
elemsVals :* ℤ64
incr  ← CParser TokenBasic ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
doScoped
        Subst () e -> CParser TokenBasic (Subst () e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (Subst () e -> CParser TokenBasic (Subst () e))
-> Subst () e -> CParser TokenBasic (Subst () e)
forall a b. (a -> b) -> a -> b
$ SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e
forall a b. (a -> b) -> a -> b
$ ((() ∧ Name) ⇰ SubstElem (() ∧ SName) e)
-> ((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced (() ∧ Name) ⇰ SubstElem (() ∧ SName) e
forall a. Null a => a
null (((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
 -> SubstSpaced (() ∧ Name) (() ∧ SName) e)
-> ((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e
forall a b. (a -> b) -> a -> b
$ (() () -> SName -> () ∧ SName
forall a b. a -> b -> a ∧ b
:* SName
D_SName) (() ∧ SName)
-> SubstScoped (() ∧ SName) e
-> (() ∧ SName) ⇰ SubstScoped (() ∧ SName) e
forall a. (() ∧ SName) -> a -> (() ∧ SName) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
-> 𝕍 (SSubstElem (() ∧ SName) e)
-> ℤ64
-> SubstScoped (() ∧ SName) e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
nShft 𝕍 (SSubstElem (() ∧ SName) e)
elemsVals ℤ64
incr
      -- named
      N_SGName Name
x → do
        ℕ64
nShft :* 𝕍 (SSubstElem (() ∧ SName) e)
elemsVals :* ℤ64
incr ← CParser TokenBasic ((ℕ64 ∧ 𝕍 (SSubstElem (() ∧ SName) e)) ∧ ℤ64)
doScoped
        Subst () e -> CParser TokenBasic (Subst () e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (Subst () e -> CParser TokenBasic (Subst () e))
-> Subst () e -> CParser TokenBasic (Subst () e)
forall a b. (a -> b) -> a -> b
$ SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e
forall a b. (a -> b) -> a -> b
$ ((() ∧ Name) ⇰ SubstElem (() ∧ SName) e)
-> ((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced (() ∧ Name) ⇰ SubstElem (() ∧ SName) e
forall a. Null a => a
null (((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
 -> SubstSpaced (() ∧ Name) (() ∧ SName) e)
-> ((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e
forall a b. (a -> b) -> a -> b
$ (() () -> SName -> () ∧ SName
forall a b. a -> b -> a ∧ b
:* Name -> SName
N_SName Name
x) (() ∧ SName)
-> SubstScoped (() ∧ SName) e
-> (() ∧ SName) ⇰ SubstScoped (() ∧ SName) e
forall a. (() ∧ SName) -> a -> (() ∧ SName) ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ℕ64
-> 𝕍 (SSubstElem (() ∧ SName) e)
-> ℤ64
-> SubstScoped (() ∧ SName) e
forall s e. ℕ64 -> 𝕍 (SSubstElem s e) -> ℤ64 -> SubstScoped s e
SubstScoped ℕ64
nShft 𝕍 (SSubstElem (() ∧ SName) e)
elemsVals ℤ64
incr
      -- global
      G_SGName Name
x → do
        -- global can't have shifts
        Text -> CParser TokenBasic () -> CParser TokenBasic ()
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"global vars can't have shifts" (CParser TokenBasic () -> CParser TokenBasic ())
-> CParser TokenBasic () -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ 𝔹 -> CParser TokenBasic ()
forall t. 𝔹 -> CParser t ()
cpGuard (𝔹 -> CParser TokenBasic ()) -> 𝔹 -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ 𝐼 ℕ64 -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝐼 ℕ64
shfts
        -- global can't have incrs
        Text -> CParser TokenBasic () -> CParser TokenBasic ()
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"global vars can't have incrs" (CParser TokenBasic () -> CParser TokenBasic ())
-> CParser TokenBasic () -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ 𝔹 -> CParser TokenBasic ()
forall t. 𝔹 -> CParser t ()
cpGuard (𝔹 -> CParser TokenBasic ()) -> 𝔹 -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ 𝐼 (ℕ64 ∧ ℤ64) -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝐼 (ℕ64 ∧ ℤ64)
incrs
        -- should only map each name to one element
        𝑂 DVar ⇰ e
elems ← Text
-> CParser TokenBasic (𝑂 DVar ⇰ e)
-> CParser TokenBasic (𝑂 DVar ⇰ e)
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"one bind per name (scoped)" (CParser TokenBasic (𝑂 DVar ⇰ e)
 -> CParser TokenBasic (𝑂 DVar ⇰ e))
-> CParser TokenBasic (𝑂 DVar ⇰ e)
-> CParser TokenBasic (𝑂 DVar ⇰ e)
forall a b. (a -> b) -> a -> b
$ 𝑂 (𝑂 DVar ⇰ e) -> CParser TokenBasic (𝑂 DVar ⇰ e)
forall a t. 𝑂 a -> CParser t a
cpFailEff (𝑂 (𝑂 DVar ⇰ e) -> CParser TokenBasic (𝑂 DVar ⇰ e))
-> 𝑂 (𝑂 DVar ⇰ e) -> CParser TokenBasic (𝑂 DVar ⇰ e)
forall a b. (a -> b) -> a -> b
$ (𝑂 DVar ⇰ 𝐼 e) -> (𝐼 e -> 𝑂 e) -> 𝑂 (𝑂 DVar ⇰ e)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn 𝑂 DVar ⇰ 𝐼 e
elemss ((𝐼 e -> 𝑂 e) -> 𝑂 (𝑂 DVar ⇰ e)) -> (𝐼 e -> 𝑂 e) -> 𝑂 (𝑂 DVar ⇰ e)
forall a b. (a -> b) -> a -> b
$ (𝐼 e ⌲ e) -> 𝐼 e -> 𝑂 e
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝐼 e ⌲ e
forall a. 𝐼 a ⌲ a
single𝐼L
        (() ∧ Name) ⇰ SubstElem (() ∧ SName) e
wes ← 𝐼 ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
-> (() ∧ Name) ⇰ SubstElem (() ∧ SName) e
forall k a t. (Ord k, ToIter (k ∧ a) t) => t -> k ⇰ a
assoc𝐷 (𝐼 ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
 -> (() ∧ Name) ⇰ SubstElem (() ∧ SName) e)
-> CParser TokenBasic (𝐼 ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
-> CParser TokenBasic ((() ∧ Name) ⇰ SubstElem (() ∧ SName) e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝐼 (𝑂 DVar ∧ e)
-> ((𝑂 DVar ∧ e)
    -> CParser TokenBasic ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
-> CParser TokenBasic (𝐼 ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
t a -> (a -> m b) -> m (t b)
mapMOn ((𝑂 DVar ⇰ e) -> 𝐼 (𝑂 DVar ∧ e)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑂 DVar ⇰ e
elems) (((𝑂 DVar ∧ e)
  -> CParser TokenBasic ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
 -> CParser TokenBasic (𝐼 ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)))
-> ((𝑂 DVar ∧ e)
    -> CParser TokenBasic ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
-> CParser TokenBasic (𝐼 ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
forall a b. (a -> b) -> a -> b
$ \ (𝑂 DVar
nO :* e
e) → do
          -- having an index for the name doesn't make sense
          Text -> CParser TokenBasic () -> CParser TokenBasic ()
forall t a. Ord t => Text -> CParser t a -> CParser t a
cpErr Text
"global vars can't have index" (CParser TokenBasic () -> CParser TokenBasic ())
-> CParser TokenBasic () -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ 𝔹 -> CParser TokenBasic ()
forall t. 𝔹 -> CParser t ()
cpGuard (𝔹 -> CParser TokenBasic ()) -> 𝔹 -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ (𝑂 DVar ⌲ ()) -> 𝑂 DVar -> 𝔹
forall a b. (a ⌲ b) -> a -> 𝔹
shape 𝑂 DVar ⌲ ()
forall a. 𝑂 a ⌲ ()
noneL 𝑂 DVar
nO
          ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
-> CParser TokenBasic ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
 -> CParser TokenBasic ((() ∧ Name) ∧ SubstElem (() ∧ SName) e))
-> ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
-> CParser TokenBasic ((() ∧ Name) ∧ SubstElem (() ∧ SName) e)
forall a b. (a -> b) -> a -> b
$ (() ∧ Name)
-> SubstElem (() ∧ SName) e
-> (() ∧ Name) ∧ SubstElem (() ∧ SName) e
forall a b. a -> b -> a ∧ b
(:*) (() () -> Name -> () ∧ Name
forall a b. a -> b -> a ∧ b
:* Name
x) (SubstElem (() ∧ SName) e
 -> (() ∧ Name) ∧ SubstElem (() ∧ SName) e)
-> SubstElem (() ∧ SName) e
-> (() ∧ Name) ∧ SubstElem (() ∧ SName) e
forall a b. (a -> b) -> a -> b
$ ((() ∧ SName) ⇰ ℕ64) -> 𝑂 e -> SubstElem (() ∧ SName) e
forall s e. (s ⇰ ℕ64) -> 𝑂 e -> SubstElem s e
SubstElem (() ∧ SName) ⇰ ℕ64
forall a. Null a => a
null (𝑂 e -> SubstElem (() ∧ SName) e)
-> 𝑂 e -> SubstElem (() ∧ SName) e
forall a b. (a -> b) -> a -> b
$ e -> 𝑂 e
forall a. a -> 𝑂 a
Some e
e
        Subst () e -> CParser TokenBasic (Subst () e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (Subst () e -> CParser TokenBasic (Subst () e))
-> Subst () e -> CParser TokenBasic (Subst () e)
forall a b. (a -> b) -> a -> b
$ SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e
forall s e. SubstSpaced (s ∧ Name) (s ∧ SName) e -> Subst s e
Subst (SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e -> Subst () e
forall a b. (a -> b) -> a -> b
$ ((() ∧ Name) ⇰ SubstElem (() ∧ SName) e)
-> ((() ∧ SName) ⇰ SubstScoped (() ∧ SName) e)
-> SubstSpaced (() ∧ Name) (() ∧ SName) e
forall sG sS e.
(sG ⇰ SubstElem sS e)
-> (sS ⇰ SubstScoped sS e) -> SubstSpaced sG sS e
SubstSpaced (() ∧ Name) ⇰ SubstElem (() ∧ SName) e
wes (() ∧ SName) ⇰ SubstScoped (() ∧ SName) e
forall a. Null a => a
null
  CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ Text -> CParser TokenBasic TokenBasic
cpSyntax Text
"}"
  Subst () e -> CParser TokenBasic (Subst () e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return Subst () e
𝓈

pMVarTail ∷ (Eq e,Substy () e e) ⇒ (() → CParser TokenBasic e) → Name → CParser TokenBasic (MVar () e)
pMVarTail :: forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e)
-> Name -> CParser TokenBasic (MVar () e)
pMVarTail () -> CParser TokenBasic e
pE Name
x = do
  CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenBasic TokenBasic -> CParser TokenBasic ())
-> CParser TokenBasic TokenBasic -> CParser TokenBasic ()
forall a b. (a -> b) -> a -> b
$ Text -> CParser TokenBasic TokenBasic
cpSyntax Text
":m"
  Subst () e
𝓈 ← Subst () e -> 𝑂 (Subst () e) -> Subst () e
forall a. a -> 𝑂 a -> a
ifNone Subst () e
forall a. Null a => a
null (𝑂 (Subst () e) -> Subst () e)
-> CParser TokenBasic (𝑂 (Subst () e))
-> CParser TokenBasic (Subst () e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic (Subst () e)
-> CParser TokenBasic (𝑂 (Subst () e))
forall t a. Ord t => CParser t a -> CParser t (𝑂 a)
cpOptional (CParser TokenBasic (Subst () e)
 -> CParser TokenBasic (𝑂 (Subst () e)))
-> CParser TokenBasic (Subst () e)
-> CParser TokenBasic (𝑂 (Subst () e))
forall a b. (a -> b) -> a -> b
$ (() -> CParser TokenBasic e) -> CParser TokenBasic (Subst () e)
forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e) -> CParser TokenBasic (Subst () e)
pSubst () -> CParser TokenBasic e
pE
  MVar () e -> CParser TokenBasic (MVar () e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (MVar () e -> CParser TokenBasic (MVar () e))
-> MVar () e -> CParser TokenBasic (MVar () e)
forall a b. (a -> b) -> a -> b
$ Subst () e -> Name -> MVar () e
forall s e. Subst s e -> Name -> MVar s e
MVar Subst () e
𝓈 Name
x

pMVar ∷ (Eq e,Substy () e e) ⇒ (() → CParser TokenBasic e) → CParser TokenBasic (MVar () e)
pMVar :: forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e) -> CParser TokenBasic (MVar () e)
pMVar () -> CParser TokenBasic e
pE = do
  Name
x ← CParser TokenBasic Name
pName
  (() -> CParser TokenBasic e)
-> Name -> CParser TokenBasic (MVar () e)
forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e)
-> Name -> CParser TokenBasic (MVar () e)
pMVarTail () -> CParser TokenBasic e
pE Name
x

pUVar ∷ (Eq e,Substy () e e) ⇒ (() → CParser TokenBasic e) → CParser TokenBasic (UVar () e)
pUVar :: forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e) -> CParser TokenBasic (UVar () e)
pUVar () -> CParser TokenBasic e
pE = [CParser TokenBasic (UVar () e)] -> CParser TokenBasic (UVar () e)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ do DVar
x ← CParser TokenBasic DVar
pDVar
       UVar () e -> CParser TokenBasic (UVar () e)
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (UVar () e -> CParser TokenBasic (UVar () e))
-> UVar () e -> CParser TokenBasic (UVar () e)
forall a b. (a -> b) -> a -> b
$ DVar -> UVar () e
forall s e. DVar -> UVar s e
D_UVar DVar
x
  , do Name
x ← CParser TokenBasic Name
pName
       [CParser TokenBasic (UVar () e)] -> CParser TokenBasic (UVar () e)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
         [ NVar -> UVar () e
forall s e. NVar -> UVar s e
N_UVar (NVar -> UVar () e)
-> CParser TokenBasic NVar -> CParser TokenBasic (UVar () e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> CParser TokenBasic NVar
pNVarTail Name
x
         , GVar -> UVar () e
forall s e. GVar -> UVar s e
G_UVar (GVar -> UVar () e)
-> CParser TokenBasic GVar -> CParser TokenBasic (UVar () e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> CParser TokenBasic GVar
pGVarTail Name
x
         , MVar () e -> UVar () e
forall s e. MVar s e -> UVar s e
M_UVar (MVar () e -> UVar () e)
-> CParser TokenBasic (MVar () e) -> CParser TokenBasic (UVar () e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (() -> CParser TokenBasic e)
-> Name -> CParser TokenBasic (MVar () e)
forall e.
(Eq e, Substy () e e) =>
(() -> CParser TokenBasic e)
-> Name -> CParser TokenBasic (MVar () e)
pMVarTail () -> CParser TokenBasic e
pE Name
x
         ]
  ]

instance (Ord s,Shrinky e) ⇒ Shrinky (UVar s e) where
  shrink :: UVar s e -> 𝐼 (UVar s e)
shrink = \case
    D_UVar DVar
x → DVar -> UVar s e
forall s e. DVar -> UVar s e
D_UVar (DVar -> UVar s e) -> 𝐼 DVar -> 𝐼 (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ DVar -> 𝐼 DVar
forall a. Shrinky a => a -> 𝐼 a
shrink DVar
x
    N_UVar NVar
x → NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar (NVar -> UVar s e) -> 𝐼 NVar -> 𝐼 (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ NVar -> 𝐼 NVar
forall a. Shrinky a => a -> 𝐼 a
shrink NVar
x
    G_UVar GVar
x → GVar -> UVar s e
forall s e. GVar -> UVar s e
G_UVar (GVar -> UVar s e) -> 𝐼 GVar -> 𝐼 (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ GVar -> 𝐼 GVar
forall a. Shrinky a => a -> 𝐼 a
shrink GVar
x
    M_UVar MVar s e
x → MVar s e -> UVar s e
forall s e. MVar s e -> UVar s e
M_UVar (MVar s e -> UVar s e) -> 𝐼 (MVar s e) -> 𝐼 (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ MVar s e -> 𝐼 (MVar s e)
forall a. Shrinky a => a -> 𝐼 a
shrink MVar s e
x