module UVMHS.Lib.Substitution.UVar where

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

import UVMHS.Lib.Substitution.Name
import UVMHS.Lib.Substitution.Subst
import UVMHS.Lib.Substitution.Var

---------------------------------------------------------------------
-- ==== --
-- MVar --
-- ==== --
---------------------------------------------------------------------

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

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

instance Functor (MVar s) where
  map :: forall a b. (a -> b) -> MVar s a -> MVar s b
map a -> b
f (MVar Subst s a
𝓈 Name
x) = Subst s b -> Name -> MVar s b
forall s e. Subst s e -> Name -> MVar s e
MVar ((a -> b) -> Subst s a -> Subst s b
forall a b. (a -> b) -> Subst s a -> Subst s b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f Subst s a
𝓈) Name
x

------------------
-- WELL FOUNDED --
------------------

wfMVar ∷ (Ord s) ⇒ MVar s e → 𝔹
wfMVar :: forall s e. Ord s => MVar s e -> Bool
wfMVar = Subst s e -> Bool
forall s e. Ord s => Subst s e -> Bool
wfSubst (Subst s e -> Bool) -> (MVar s e -> Subst s e) -> MVar s e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ MVar s e -> Subst s e
forall s e. MVar s e -> Subst s e
mvarSubst

-----------
-- FUZZY --
-----------

instance (Ord s,Fuzzy s,Fuzzy e) ⇒ Fuzzy (MVar s e) where
  fuzzy :: FuzzyM (MVar s e)
fuzzy = (Subst s e -> Name -> MVar s e)
-> FuzzyM (Subst s e -> Name -> MVar s e)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return Subst s e -> Name -> MVar s e
forall s e. Subst s e -> Name -> MVar s e
MVar FuzzyM (Subst s e -> Name -> MVar s e)
-> FuzzyM (Subst s e) -> FuzzyM (Name -> MVar s e)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
⊡ FuzzyM (Subst s e)
forall a. Fuzzy a => FuzzyM a
fuzzy FuzzyM (Name -> MVar s e) -> FuzzyM Name -> FuzzyM (MVar s e)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
⊡ FuzzyM Name
forall a. Fuzzy a => FuzzyM a
fuzzy

instance (Ord s,Shrinky e) ⇒ Shrinky (MVar s e) where
  shrink :: MVar s e -> 𝐼 (MVar s e)
shrink (MVar Subst s e
𝓈 Name
x) = do
    (Subst s e
𝓈',Name
x') ← (Subst s e, Name) -> 𝐼 (Subst s e, Name)
forall a. Shrinky a => a -> 𝐼 a
shrink (Subst s e
𝓈,Name
x)
    MVar s e -> 𝐼 (MVar s e)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (MVar s e -> 𝐼 (MVar s e)) -> MVar s e -> 𝐼 (MVar s e)
forall a b. (a -> b) -> a -> b
$ Subst s e -> Name -> MVar s e
forall s e. Subst s e -> Name -> MVar s e
MVar Subst s e
𝓈' Name
x'

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

instance (Ord s,Pretty s,Pretty e) ⇒ Pretty (MVar s e) where
  pretty :: MVar s e -> Doc
pretty (MVar Subst s e
𝓈 Name
x) = [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat 
    [ Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    , 𝕊 -> Doc
ppPun 𝕊
":m"
    , if Subst s e -> Bool
forall s e. Ord s => Subst s e -> Bool
isNullSubst Subst s e
𝓈 then Doc
forall a. Null a => a
null else Doc -> Doc
ppGA (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Subst s e -> Doc
forall a. Pretty a => a -> Doc
pretty Subst s e
𝓈
    ]

---------------------------------------------------------------------
-- ==== --
-- UVar --
-- ==== --
---------------------------------------------------------------------

data UVar s e =
    D_UVar DVar
  | N_UVar NVar
  | G_UVar GVar
  | M_UVar (MVar s e)
  deriving (UVar s e -> UVar s e -> Bool
(UVar s e -> UVar s e -> Bool)
-> (UVar s e -> UVar s e -> Bool) -> Eq (UVar s e)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s e. (Eq s, Eq e) => UVar s e -> UVar s e -> Bool
$c== :: forall s e. (Eq s, Eq e) => UVar s e -> UVar s e -> Bool
== :: UVar s e -> UVar s e -> Bool
$c/= :: forall s e. (Eq s, Eq e) => UVar s e -> UVar s e -> Bool
/= :: UVar s e -> UVar s e -> Bool
Eq,Eq (UVar s e)
Eq (UVar s e) =>
(UVar s e -> UVar s e -> Ordering)
-> (UVar s e -> UVar s e -> Bool)
-> (UVar s e -> UVar s e -> Bool)
-> (UVar s e -> UVar s e -> Bool)
-> (UVar s e -> UVar s e -> Bool)
-> (UVar s e -> UVar s e -> UVar s e)
-> (UVar s e -> UVar s e -> UVar s e)
-> Ord (UVar s e)
UVar s e -> UVar s e -> Bool
UVar s e -> UVar s e -> Ordering
UVar s e -> UVar s e -> UVar s e
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall s e. (Ord s, Ord e) => Eq (UVar s e)
forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Bool
forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Ordering
forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> UVar s e
$ccompare :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Ordering
compare :: UVar s e -> UVar s e -> Ordering
$c< :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Bool
< :: UVar s e -> UVar s e -> Bool
$c<= :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Bool
<= :: UVar s e -> UVar s e -> Bool
$c> :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Bool
> :: UVar s e -> UVar s e -> Bool
$c>= :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> Bool
>= :: UVar s e -> UVar s e -> Bool
$cmax :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> UVar s e
max :: UVar s e -> UVar s e -> UVar s e
$cmin :: forall s e. (Ord s, Ord e) => UVar s e -> UVar s e -> UVar s e
min :: UVar s e -> UVar s e -> UVar s e
Ord,Int -> UVar s e -> ShowS
[UVar s e] -> ShowS
UVar s e -> String
(Int -> UVar s e -> ShowS)
-> (UVar s e -> String) -> ([UVar s e] -> ShowS) -> Show (UVar s e)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s e. (Show s, Show e) => Int -> UVar s e -> ShowS
forall s e. (Show s, Show e) => [UVar s e] -> ShowS
forall s e. (Show s, Show e) => UVar s e -> String
$cshowsPrec :: forall s e. (Show s, Show e) => Int -> UVar s e -> ShowS
showsPrec :: Int -> UVar s e -> ShowS
$cshow :: forall s e. (Show s, Show e) => UVar s e -> String
show :: UVar s e -> String
$cshowList :: forall s e. (Show s, Show e) => [UVar s e] -> ShowS
showList :: [UVar s e] -> ShowS
Show)
makePrisms ''UVar
makePrettyUnion ''UVar

name_UVarL ∷ UVar s e ⌲ Name
name_UVarL :: forall s e. UVar s e ⌲ Name
name_UVarL = NVar ⌲ Name
name_NVarL (NVar ⌲ Name) -> (UVar s e ⌲ NVar) -> UVar s e ⌲ Name
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ UVar s e ⌲ NVar
forall s e. UVar s e ⌲ NVar
n_UVarL

uvar_Name ∷ Name → UVar s e
uvar_Name :: forall s e. Name -> UVar s e
uvar_Name = (UVar s e ⌲ Name) -> Name -> UVar s e
forall a b. (a ⌲ b) -> b -> a
construct UVar s e ⌲ Name
forall s e. UVar s e ⌲ Name
name_UVarL

uvar_SVar ∷ SVar → UVar s e
uvar_SVar :: forall s e. SVar -> UVar s e
uvar_SVar = \case
  D_SVar DVar
x → DVar -> UVar s e
forall s e. DVar -> UVar s e
D_UVar DVar
x
  N_SVar NVar
x → NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar NVar
x

svar_UVarL ∷ UVar s e ⌲ SVar
svar_UVarL :: forall s e. UVar s e ⌲ SVar
svar_UVarL = (SVar -> UVar s e) -> (UVar s e -> 𝑂 SVar) -> UVar s e ⌲ SVar
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism SVar -> UVar s e
forall s e. SVar -> UVar s e
uvar_SVar ((UVar s e -> 𝑂 SVar) -> UVar s e ⌲ SVar)
-> (UVar s e -> 𝑂 SVar) -> UVar s e ⌲ SVar
forall a b. (a -> b) -> a -> b
$ \case
  D_UVar DVar
x → SVar -> 𝑂 SVar
forall a. a -> 𝑂 a
Some (SVar -> 𝑂 SVar) -> SVar -> 𝑂 SVar
forall a b. (a -> b) -> a -> b
$ DVar -> SVar
D_SVar DVar
x
  N_UVar NVar
x → SVar -> 𝑂 SVar
forall a. a -> 𝑂 a
Some (SVar -> 𝑂 SVar) -> SVar -> 𝑂 SVar
forall a b. (a -> b) -> a -> b
$ NVar -> SVar
N_SVar NVar
x
  UVar s e
_        → 𝑂 SVar
forall a. 𝑂 a
None

uvar_Var ∷ Var → UVar s e
uvar_Var :: forall s e. Var -> UVar s e
uvar_Var = \case
  D_Var DVar
x → DVar -> UVar s e
forall s e. DVar -> UVar s e
D_UVar DVar
x
  N_Var NVar
x → NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar NVar
x
  G_Var GVar
x → GVar -> UVar s e
forall s e. GVar -> UVar s e
G_UVar GVar
x

var_UVarL ∷ UVar s e ⌲ Var
var_UVarL :: forall s e. UVar s e ⌲ Var
var_UVarL = (Var -> UVar s e) -> (UVar s e -> 𝑂 Var) -> UVar s e ⌲ Var
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism Var -> UVar s e
forall s e. Var -> UVar s e
uvar_Var ((UVar s e -> 𝑂 Var) -> UVar s e ⌲ Var)
-> (UVar s e -> 𝑂 Var) -> UVar s e ⌲ Var
forall a b. (a -> b) -> a -> b
$ \case
  D_UVar DVar
x → Var -> 𝑂 Var
forall a. a -> 𝑂 a
Some (Var -> 𝑂 Var) -> Var -> 𝑂 Var
forall a b. (a -> b) -> a -> b
$ DVar -> Var
D_Var DVar
x
  N_UVar NVar
x → Var -> 𝑂 Var
forall a. a -> 𝑂 a
Some (Var -> 𝑂 Var) -> Var -> 𝑂 Var
forall a b. (a -> b) -> a -> b
$ NVar -> Var
N_Var NVar
x
  G_UVar GVar
x → Var -> 𝑂 Var
forall a. a -> 𝑂 a
Some (Var -> 𝑂 Var) -> Var -> 𝑂 Var
forall a b. (a -> b) -> a -> b
$ GVar -> Var
G_Var GVar
x
  UVar s e
_        → 𝑂 Var
forall a. 𝑂 a
None
  

gensymUVar ∷ (Monad m,MonadState s m) ⇒ s ⟢ ℕ64 → 𝕊 → m (UVar s e)
gensymUVar :: forall (m :: * -> *) s e.
(Monad m, MonadState s m) =>
(s ⟢ ℕ64) -> 𝕊 -> m (UVar s e)
gensymUVar s ⟢ ℕ64
ℓ 𝕊
s = NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar (NVar -> UVar s e) -> m NVar -> m (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (s ⟢ ℕ64) -> 𝕊 -> m NVar
forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s ⟢ ℕ64) -> 𝕊 -> m NVar
gensymNVar s ⟢ ℕ64
ℓ 𝕊
s

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

instance Functor (UVar s) where
  map :: forall a b. (a -> b) -> UVar s a -> UVar s b
map a -> b
f = \case
    D_UVar DVar
x → DVar -> UVar s b
forall s e. DVar -> UVar s e
D_UVar DVar
x
    N_UVar NVar
x → NVar -> UVar s b
forall s e. NVar -> UVar s e
N_UVar NVar
x
    G_UVar GVar
x → GVar -> UVar s b
forall s e. GVar -> UVar s e
G_UVar GVar
x
    M_UVar MVar s a
x → MVar s b -> UVar s b
forall s e. MVar s e -> UVar s e
M_UVar (MVar s b -> UVar s b) -> MVar s b -> UVar s b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> MVar s a -> MVar s b
forall a b. (a -> b) -> MVar s a -> MVar s b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f MVar s a
x

------------------
-- WELL FOUNDED --
------------------

wfUVar ∷ (Ord s) ⇒ UVar s e → 𝔹
wfUVar :: forall s e. Ord s => UVar s e -> Bool
wfUVar = \case
  D_UVar DVar
_ → Bool
True
  N_UVar NVar
_ → Bool
True
  G_UVar GVar
_ → Bool
True
  M_UVar MVar s e
x → MVar s e -> Bool
forall s e. Ord s => MVar s e -> Bool
wfMVar MVar s e
x

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

-------------------------
-- FUZZY for Variables --
-------------------------

instance (Pretty e,Pretty s,Ord s,Fuzzy s,Fuzzy e) ⇒ Fuzzy (UVar s e) where
  fuzzy :: FuzzyM (UVar s e)
fuzzy = [() -> FuzzyM (UVar s e)] -> FuzzyM (UVar s e)
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose
    [ \ () → DVar -> UVar s e
forall s e. DVar -> UVar s e
D_UVar (DVar -> UVar s e) -> FuzzyM DVar -> FuzzyM (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM DVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → NVar -> UVar s e
forall s e. NVar -> UVar s e
N_UVar (NVar -> UVar s e) -> FuzzyM NVar -> FuzzyM (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM NVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → GVar -> UVar s e
forall s e. GVar -> UVar s e
G_UVar (GVar -> UVar s e) -> FuzzyM GVar -> FuzzyM (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM GVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → MVar s e -> UVar s e
forall s e. MVar s e -> UVar s e
M_UVar (MVar s e -> UVar s e) -> FuzzyM (MVar s e) -> FuzzyM (UVar s e)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM (MVar s e)
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]