module UVMHS.Lib.Substitution.Name where

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

---------------------------------------------------------------------
-- ==== --
-- Name --
-- ==== --
---------------------------------------------------------------------

data Name = Name
  { Name -> 𝑂 ℕ64
nameMark ∷ 𝑂 ℕ64
  , Name -> 𝕊
nameName ∷ 𝕊
  } deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
/= :: Name -> Name -> Bool
Eq,Eq Name
Eq Name =>
(Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
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
$ccompare :: Name -> Name -> Ordering
compare :: Name -> Name -> Ordering
$c< :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
>= :: Name -> Name -> Bool
$cmax :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
min :: Name -> Name -> Name
Ord,Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Name -> ShowS
showsPrec :: Int -> Name -> ShowS
$cshow :: Name -> String
show :: Name -> String
$cshowList :: [Name] -> ShowS
showList :: [Name] -> ShowS
Show)
makeLenses ''Name

mkName ∷ 𝕊 → Name
mkName :: 𝕊 -> Name
mkName = 𝑂 ℕ64 -> 𝕊 -> Name
Name 𝑂 ℕ64
forall a. 𝑂 a
None

gensymName ∷ (Monad m,MonadState s m) ⇒ s ⟢ ℕ64 → 𝕊 → m Name
gensymName :: forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s ⟢ ℕ64) -> 𝕊 -> m Name
gensymName s ⟢ ℕ64
ℓ 𝕊
s = do
  ℕ64
n ← (s ⟢ ℕ64) -> m ℕ64
forall (m :: * -> *) s a.
(Monad m, MonadState s m, Multiplicative a) =>
(s ⟢ a) -> m a
nextL s ⟢ ℕ64
ℓ
  Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (Name -> m Name) -> Name -> m Name
forall a b. (a -> b) -> a -> b
$ 𝑂 ℕ64 -> 𝕊 -> Name
Name (ℕ64 -> 𝑂 ℕ64
forall a. a -> 𝑂 a
Some ℕ64
n) 𝕊
s

instance Fuzzy Name where
  fuzzy :: FuzzyM Name
fuzzy = do 
    𝑂 ℕ64
nO ← FuzzyM (𝑂 ℕ64)
forall a. Fuzzy a => FuzzyM a
fuzzy 
    Name -> FuzzyM Name
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (Name -> FuzzyM Name) -> Name -> FuzzyM Name
forall a b. (a -> b) -> a -> b
$ 𝑂 ℕ64 -> 𝕊 -> Name
Name 𝑂 ℕ64
nO 𝕊
"x"

instance Shrinky Name where
  shrink :: Name -> 𝐼 Name
shrink = 𝐼 Name -> Name -> 𝐼 Name
forall a b. a -> b -> a
const 𝐼 Name
forall a. Null a => a
null

instance Pretty Name where
  pretty :: Name -> Doc
pretty (Name 𝑂 ℕ64
nO 𝕊
x) = [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ 𝕊 -> Doc
ppString 𝕊
x
    , case 𝑂 ℕ64
nO of
        𝑂 ℕ64
None → Doc
forall a. Null a => a
null
        Some ℕ64
n → 𝕊 -> Doc
ppPun (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊
"#",ℕ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℕ64
n]
    ]

syntaxName ∷ LexerBasicSyntax
syntaxName :: LexerBasicSyntax
syntaxName = LexerBasicSyntax
forall a. Null a => a
null { lexerBasicSyntaxPuns = pow ["#"] }

pName ∷ CParser TokenBasic Name
pName :: CParser TokenBasic Name
pName = do
  𝕊
x ← (TokenBasic -> 𝑂 𝕊) -> CParser TokenBasic 𝕊
forall t a. (t -> 𝑂 a) -> CParser t a
cpShaped ((TokenBasic -> 𝑂 𝕊) -> CParser TokenBasic 𝕊)
-> (TokenBasic -> 𝑂 𝕊) -> CParser TokenBasic 𝕊
forall a b. (a -> b) -> a -> b
$ (TokenBasic ⌲ 𝕊) -> TokenBasic -> 𝑂 𝕊
forall a b. (a ⌲ b) -> a -> 𝑂 b
view TokenBasic ⌲ 𝕊
nameTBasicL
  𝑂 ℕ64
nO ← CParser TokenBasic ℕ64 -> CParser TokenBasic (𝑂 ℕ64)
forall t a. Ord t => CParser t a -> CParser t (𝑂 a)
cpOptional (CParser TokenBasic ℕ64 -> CParser TokenBasic (𝑂 ℕ64))
-> CParser TokenBasic ℕ64 -> CParser TokenBasic (𝑂 ℕ64)
forall a b. (a -> b) -> a -> b
$ 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
cpSyntax 𝕊
"#"
    CParser TokenBasic ℕ64
cpNat64
  Name -> CParser TokenBasic Name
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (Name -> CParser TokenBasic Name)
-> Name -> CParser TokenBasic Name
forall a b. (a -> b) -> a -> b
$ 𝑂 ℕ64 -> 𝕊 -> Name
Name 𝑂 ℕ64
nO 𝕊
x

pNameWS ∷ CParser TokenWSBasic Name
pNameWS :: CParser TokenWSBasic Name
pNameWS = do
  𝕊
x ← (TokenWSBasic -> 𝑂 𝕊) -> CParser TokenWSBasic 𝕊
forall t a. (t -> 𝑂 a) -> CParser t a
cpShaped ((TokenWSBasic -> 𝑂 𝕊) -> CParser TokenWSBasic 𝕊)
-> (TokenWSBasic -> 𝑂 𝕊) -> CParser TokenWSBasic 𝕊
forall a b. (a -> b) -> a -> b
$ (TokenWSBasic ⌲ 𝕊) -> TokenWSBasic -> 𝑂 𝕊
forall a b. (a ⌲ b) -> a -> 𝑂 b
view TokenWSBasic ⌲ 𝕊
nameTWSBasicL
  𝑂 ℕ64
nO ← CParser TokenWSBasic ℕ64 -> CParser TokenWSBasic (𝑂 ℕ64)
forall t a. Ord t => CParser t a -> CParser t (𝑂 a)
cpOptional (CParser TokenWSBasic ℕ64 -> CParser TokenWSBasic (𝑂 ℕ64))
-> CParser TokenWSBasic ℕ64 -> CParser TokenWSBasic (𝑂 ℕ64)
forall a b. (a -> b) -> a -> b
$ do
    CParser TokenWSBasic TokenWSBasic -> CParser TokenWSBasic ()
forall (m :: * -> *) a. Functor m => m a -> m ()
void (CParser TokenWSBasic TokenWSBasic -> CParser TokenWSBasic ())
-> CParser TokenWSBasic TokenWSBasic -> CParser TokenWSBasic ()
forall a b. (a -> b) -> a -> b
$ 𝕊 -> CParser TokenWSBasic TokenWSBasic
cpSyntaxWS 𝕊
"#"
    𝑂 ℕ64 -> CParser TokenWSBasic ℕ64
forall (m :: * -> *) a. (Monad m, MonadFail m) => 𝑂 a -> m a
failEff (𝑂 ℕ64 -> CParser TokenWSBasic ℕ64)
-> (ℤ -> 𝑂 ℕ64) -> ℤ -> CParser TokenWSBasic ℕ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ℤ -> 𝑂 ℕ64
forall a. ToNatO64 a => a -> 𝑂 ℕ64
natO64 (ℤ -> CParser TokenWSBasic ℕ64)
-> CParser TokenWSBasic ℤ -> CParser TokenWSBasic ℕ64
forall (m :: * -> *) a b. Bind m => (a -> m b) -> m a -> m b
*$ CParser TokenWSBasic ℤ
cpIntegerWS
  Name -> CParser TokenWSBasic Name
forall a. a -> CParser TokenWSBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (Name -> CParser TokenWSBasic Name)
-> Name -> CParser TokenWSBasic Name
forall a b. (a -> b) -> a -> b
$ 𝑂 ℕ64 -> 𝕊 -> Name
Name 𝑂 ℕ64
nO 𝕊
x

---------------------------------------------------------------------
-- ===== --
-- SName --
-- ===== --
---------------------------------------------------------------------

data SName =
    D_SName       -- De Bruijn Scope
  | N_SName Name  -- Named Scope
  deriving (SName -> SName -> Bool
(SName -> SName -> Bool) -> (SName -> SName -> Bool) -> Eq SName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SName -> SName -> Bool
== :: SName -> SName -> Bool
$c/= :: SName -> SName -> Bool
/= :: SName -> SName -> Bool
Eq,Eq SName
Eq SName =>
(SName -> SName -> Ordering)
-> (SName -> SName -> Bool)
-> (SName -> SName -> Bool)
-> (SName -> SName -> Bool)
-> (SName -> SName -> Bool)
-> (SName -> SName -> SName)
-> (SName -> SName -> SName)
-> Ord SName
SName -> SName -> Bool
SName -> SName -> Ordering
SName -> SName -> SName
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
$ccompare :: SName -> SName -> Ordering
compare :: SName -> SName -> Ordering
$c< :: SName -> SName -> Bool
< :: SName -> SName -> Bool
$c<= :: SName -> SName -> Bool
<= :: SName -> SName -> Bool
$c> :: SName -> SName -> Bool
> :: SName -> SName -> Bool
$c>= :: SName -> SName -> Bool
>= :: SName -> SName -> Bool
$cmax :: SName -> SName -> SName
max :: SName -> SName -> SName
$cmin :: SName -> SName -> SName
min :: SName -> SName -> SName
Ord,Int -> SName -> ShowS
[SName] -> ShowS
SName -> String
(Int -> SName -> ShowS)
-> (SName -> String) -> ([SName] -> ShowS) -> Show SName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SName -> ShowS
showsPrec :: Int -> SName -> ShowS
$cshow :: SName -> String
show :: SName -> String
$cshowList :: [SName] -> ShowS
showList :: [SName] -> ShowS
Show)

instance Fuzzy SName where 
  fuzzy :: FuzzyM SName
fuzzy = [() -> FuzzyM SName] -> FuzzyM SName
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose
    [ \ () → SName -> FuzzyM SName
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return SName
D_SName
    , \ () → Name -> SName
N_SName (Name -> SName) -> FuzzyM Name -> FuzzyM SName
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM Name
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]
instance Shrinky SName where 
  shrink :: SName -> 𝐼 SName
shrink = \case
    SName
D_SName → 𝐼 SName
forall a. Null a => a
null
    N_SName Name
x → Name -> SName
N_SName (Name -> SName) -> 𝐼 Name -> 𝐼 SName
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> 𝐼 Name
forall a. Shrinky a => a -> 𝐼 a
shrink Name
x

instance Pretty SName where
  pretty :: SName -> Doc
pretty = \case
    SName
D_SName   → 𝕊 -> Doc
ppPun 𝕊
"•"
    N_SName Name
x → Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x

---------------------------------------------------------------------
-- ====== --
-- SGName --
-- ====== --
---------------------------------------------------------------------

data SGName =
    D_SGName       -- De Bruijn Scope
  | N_SGName Name  -- Named Scope
  | G_SGName Name  -- Global Scope
  deriving (SGName -> SGName -> Bool
(SGName -> SGName -> Bool)
-> (SGName -> SGName -> Bool) -> Eq SGName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SGName -> SGName -> Bool
== :: SGName -> SGName -> Bool
$c/= :: SGName -> SGName -> Bool
/= :: SGName -> SGName -> Bool
Eq,Eq SGName
Eq SGName =>
(SGName -> SGName -> Ordering)
-> (SGName -> SGName -> Bool)
-> (SGName -> SGName -> Bool)
-> (SGName -> SGName -> Bool)
-> (SGName -> SGName -> Bool)
-> (SGName -> SGName -> SGName)
-> (SGName -> SGName -> SGName)
-> Ord SGName
SGName -> SGName -> Bool
SGName -> SGName -> Ordering
SGName -> SGName -> SGName
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
$ccompare :: SGName -> SGName -> Ordering
compare :: SGName -> SGName -> Ordering
$c< :: SGName -> SGName -> Bool
< :: SGName -> SGName -> Bool
$c<= :: SGName -> SGName -> Bool
<= :: SGName -> SGName -> Bool
$c> :: SGName -> SGName -> Bool
> :: SGName -> SGName -> Bool
$c>= :: SGName -> SGName -> Bool
>= :: SGName -> SGName -> Bool
$cmax :: SGName -> SGName -> SGName
max :: SGName -> SGName -> SGName
$cmin :: SGName -> SGName -> SGName
min :: SGName -> SGName -> SGName
Ord,Int -> SGName -> ShowS
[SGName] -> ShowS
SGName -> String
(Int -> SGName -> ShowS)
-> (SGName -> String) -> ([SGName] -> ShowS) -> Show SGName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SGName -> ShowS
showsPrec :: Int -> SGName -> ShowS
$cshow :: SGName -> String
show :: SGName -> String
$cshowList :: [SGName] -> ShowS
showList :: [SGName] -> ShowS
Show)

instance Fuzzy SGName where 
  fuzzy :: FuzzyM SGName
fuzzy = [() -> FuzzyM SGName] -> FuzzyM SGName
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose
    [ \ () → SGName -> FuzzyM SGName
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return SGName
D_SGName
    , \ () → Name -> SGName
N_SGName (Name -> SGName) -> FuzzyM Name -> FuzzyM SGName
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM Name
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → Name -> SGName
G_SGName (Name -> SGName) -> FuzzyM Name -> FuzzyM SGName
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM Name
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]

instance Shrinky SGName where 
  shrink :: SGName -> 𝐼 SGName
shrink = \case
    SGName
D_SGName → 𝐼 SGName
forall a. Null a => a
null
    N_SGName Name
x → Name -> SGName
N_SGName (Name -> SGName) -> 𝐼 Name -> 𝐼 SGName
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> 𝐼 Name
forall a. Shrinky a => a -> 𝐼 a
shrink Name
x
    G_SGName Name
x → Name -> SGName
G_SGName (Name -> SGName) -> 𝐼 Name -> 𝐼 SGName
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> 𝐼 Name
forall a. Shrinky a => a -> 𝐼 a
shrink Name
x

instance Pretty SGName where
  pretty :: SGName -> Doc
pretty = \case
    SGName
D_SGName   → 𝕊 -> Doc
ppPun 𝕊
"•"
    N_SGName Name
x → Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x
    G_SGName Name
x → Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x