module UVMHS.Lib.Variables where

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

-- ========= --
-- VARIABLES --
-- ========= --

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

-- fancy variables
data 𝕐 = 
    DVar ℕ64
  | NVar ℕ64 𝕏
  | GVar 𝕏
  | MVar 𝕏
  deriving (𝕐 -> 𝕐 -> Bool
(𝕐 -> 𝕐 -> Bool) -> (𝕐 -> 𝕐 -> Bool) -> Eq 𝕐
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: 𝕐 -> 𝕐 -> Bool
== :: 𝕐 -> 𝕐 -> Bool
$c/= :: 𝕐 -> 𝕐 -> Bool
/= :: 𝕐 -> 𝕐 -> Bool
Eq,Eq 𝕐
Eq 𝕐 =>
(𝕐 -> 𝕐 -> Ordering)
-> (𝕐 -> 𝕐 -> Bool)
-> (𝕐 -> 𝕐 -> Bool)
-> (𝕐 -> 𝕐 -> Bool)
-> (𝕐 -> 𝕐 -> Bool)
-> (𝕐 -> 𝕐 -> 𝕐)
-> (𝕐 -> 𝕐 -> 𝕐)
-> Ord 𝕐
𝕐 -> 𝕐 -> Bool
𝕐 -> 𝕐 -> Ordering
𝕐 -> 𝕐 -> 𝕐
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 :: 𝕐 -> 𝕐 -> Ordering
compare :: 𝕐 -> 𝕐 -> Ordering
$c< :: 𝕐 -> 𝕐 -> Bool
< :: 𝕐 -> 𝕐 -> Bool
$c<= :: 𝕐 -> 𝕐 -> Bool
<= :: 𝕐 -> 𝕐 -> Bool
$c> :: 𝕐 -> 𝕐 -> Bool
> :: 𝕐 -> 𝕐 -> Bool
$c>= :: 𝕐 -> 𝕐 -> Bool
>= :: 𝕐 -> 𝕐 -> Bool
$cmax :: 𝕐 -> 𝕐 -> 𝕐
max :: 𝕐 -> 𝕐 -> 𝕐
$cmin :: 𝕐 -> 𝕐 -> 𝕐
min :: 𝕐 -> 𝕐 -> 𝕐
Ord,Int -> 𝕐 -> ShowS
[𝕐] -> ShowS
𝕐 -> String
(Int -> 𝕐 -> ShowS) -> (𝕐 -> String) -> ([𝕐] -> ShowS) -> Show 𝕐
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> 𝕐 -> ShowS
showsPrec :: Int -> 𝕐 -> ShowS
$cshow :: 𝕐 -> String
show :: 𝕐 -> String
$cshowList :: [𝕐] -> ShowS
showList :: [𝕐] -> ShowS
Show)
makePrisms ''𝕐

var ∷ 𝕊 → 𝕏
var :: 𝕊 -> 𝕏
var = 𝑂 ℕ64 -> 𝕊 -> 𝕏
𝕏 𝑂 ℕ64
forall a. 𝑂 a
None

nvar ∷ 𝕏 → 𝕐
nvar :: 𝕏 -> 𝕐
nvar = ℕ64 -> 𝕏 -> 𝕐
NVar ℕ64
0

nvarL ∷ 𝕐 ⌲ 𝕏
nvarL :: 𝕐 ⌲ 𝕏
nvarL = (𝕏 -> 𝕐) -> (𝕐 -> 𝑂 𝕏) -> 𝕐 ⌲ 𝕏
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism 𝕏 -> 𝕐
nvar ((𝕐 -> 𝑂 𝕏) -> 𝕐 ⌲ 𝕏) -> (𝕐 -> 𝑂 𝕏) -> 𝕐 ⌲ 𝕏
forall a b. (a -> b) -> a -> b
$ \case
  NVar ℕ64
n 𝕏
x | ℕ64
nℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ℕ64
0 → 𝕏 -> 𝑂 𝕏
forall a. a -> 𝑂 a
Some 𝕏
x
  𝕐
_ → 𝑂 𝕏
forall a. 𝑂 a
None

gensymVar ∷ (Monad m,MonadState s m) ⇒ s ⟢ ℕ64 → 𝕊 → m 𝕏
gensymVar :: forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s ⟢ ℕ64) -> 𝕊 -> m 𝕏
gensymVar 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
ℓ
  𝕏 -> m 𝕏
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝕏 -> m 𝕏) -> 𝕏 -> m 𝕏
forall a b. (a -> b) -> a -> b
$ 𝑂 ℕ64 -> 𝕊 -> 𝕏
𝕏 (ℕ64 -> 𝑂 ℕ64
forall a. a -> 𝑂 a
Some ℕ64
n) 𝕊
s

instance Pretty 𝕏 where
  pretty :: 𝕏 -> Doc
pretty (𝕏 𝑂 ℕ64
nO 𝕊
x) = [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ 𝕊 -> Doc
ppString 𝕊
x
    , (() -> Doc) -> (ℕ64 -> Doc) -> 𝑂 ℕ64 -> Doc
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 () -> Doc
forall a. Null a => a
null (\ ℕ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]) 𝑂 ℕ64
nO
    ]

instance Pretty 𝕐 where
  pretty :: 𝕐 -> Doc
pretty = \case
    NVar ℕ64
n 𝕏
x → [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕏 -> Doc
forall a. Pretty a => a -> Doc
pretty 𝕏
x,if ℕ64
n ℕ64 -> ℕ64 -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64
0 then Doc
forall a. Null a => a
null else 𝕊 -> 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]]
    DVar ℕ64
n → [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊 -> Doc
ppPun 𝕊
"⌊",ℕ64 -> Doc
forall a. Pretty a => a -> Doc
pretty ℕ64
n,𝕊 -> Doc
ppPun 𝕊
"⌋"]
    GVar 𝕏
x → [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕏 -> Doc
forall a. Pretty a => a -> Doc
pretty 𝕏
x]
    MVar 𝕏
x → [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕏 -> Doc
forall a. Pretty a => a -> Doc
pretty 𝕏
x,𝕊 -> Doc
ppPun 𝕊
"†"]

cpVar ∷ CParser TokenBasic 𝕏
cpVar :: CParser TokenBasic 𝕏
cpVar = 𝕊 -> 𝕏
var (𝕊 -> 𝕏) -> CParser TokenBasic 𝕊 -> CParser TokenBasic 𝕏
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (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

cpNVar ∷ CParser TokenBasic 𝕐
cpNVar :: CParser TokenBasic 𝕐
cpNVar = 𝕏 -> 𝕐
nvar (𝕏 -> 𝕐) -> (𝕊 -> 𝕏) -> 𝕊 -> 𝕐
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> 𝕏
var (𝕊 -> 𝕐) -> CParser TokenBasic 𝕊 -> CParser TokenBasic 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (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

cpGVar ∷ CParser TokenBasic 𝕐
cpGVar :: CParser TokenBasic 𝕐
cpGVar = 𝕏 -> 𝕐
GVar (𝕏 -> 𝕐) -> (𝕊 -> 𝕏) -> 𝕊 -> 𝕐
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> 𝕏
var (𝕊 -> 𝕐) -> CParser TokenBasic 𝕊 -> CParser TokenBasic 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (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

cpVarWS ∷ CParser TokenWSBasic 𝕏
cpVarWS :: CParser TokenWSBasic 𝕏
cpVarWS = 𝕊 -> 𝕏
var (𝕊 -> 𝕏) -> CParser TokenWSBasic 𝕊 -> CParser TokenWSBasic 𝕏
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (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

cpNVarWS ∷ CParser TokenWSBasic 𝕐
cpNVarWS :: CParser TokenWSBasic 𝕐
cpNVarWS = 𝕏 -> 𝕐
nvar (𝕏 -> 𝕐) -> (𝕊 -> 𝕏) -> 𝕊 -> 𝕐
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> 𝕏
var (𝕊 -> 𝕐) -> CParser TokenWSBasic 𝕊 -> CParser TokenWSBasic 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (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

cpGVarWS ∷ CParser TokenWSBasic 𝕐
cpGVarWS :: CParser TokenWSBasic 𝕐
cpGVarWS = 𝕏 -> 𝕐
GVar (𝕏 -> 𝕐) -> (𝕊 -> 𝕏) -> 𝕊 -> 𝕐
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> 𝕏
var (𝕊 -> 𝕐) -> CParser TokenWSBasic 𝕊 -> CParser TokenWSBasic 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (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

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

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

instance Fuzzy 𝕐 where
  fuzzy :: FuzzyM 𝕐
fuzzy = [() -> FuzzyM 𝕐] -> FuzzyM 𝕐
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose ([() -> FuzzyM 𝕐] -> FuzzyM 𝕐) -> [() -> FuzzyM 𝕐] -> FuzzyM 𝕐
forall a b. (a -> b) -> a -> b
$ (FuzzyM 𝕐 -> () -> FuzzyM 𝕐) -> [FuzzyM 𝕐] -> [() -> FuzzyM 𝕐]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map FuzzyM 𝕐 -> () -> FuzzyM 𝕐
forall a b. a -> b -> a
const
    [ ℕ64 -> 𝕐
DVar (ℕ64 -> 𝕐) -> FuzzyM ℕ64 -> FuzzyM 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM ℕ64
forall a. Fuzzy a => FuzzyM a
fuzzy
    , do ℕ64
n ← FuzzyM ℕ64
forall a. Fuzzy a => FuzzyM a
fuzzy
         𝕏
x ← FuzzyM 𝕏
forall a. Fuzzy a => FuzzyM a
fuzzy
         𝕐 -> FuzzyM 𝕐
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return (𝕐 -> FuzzyM 𝕐) -> 𝕐 -> FuzzyM 𝕐
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕏 -> 𝕐
NVar ℕ64
n 𝕏
x
    , 𝕏 -> 𝕐
GVar (𝕏 -> 𝕐) -> FuzzyM 𝕏 -> FuzzyM 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM 𝕏
forall a. Fuzzy a => FuzzyM a
fuzzy
    , 𝕏 -> 𝕐
MVar (𝕏 -> 𝕐) -> FuzzyM 𝕏 -> FuzzyM 𝕐
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM 𝕏
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]