module UVMHS.Lib.Substitution.Var where

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

import UVMHS.Lib.Substitution.Name

---------------------------------------------------------------------
-- ==== --
-- DVar --
-- ==== --
---------------------------------------------------------------------

-- De Bruijn Index
newtype DVar = DVar { DVar -> ℕ64
unDVar ∷ ℕ64 }
  deriving (DVar -> DVar -> Bool
(DVar -> DVar -> Bool) -> (DVar -> DVar -> Bool) -> Eq DVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DVar -> DVar -> Bool
== :: DVar -> DVar -> Bool
$c/= :: DVar -> DVar -> Bool
/= :: DVar -> DVar -> Bool
Eq,Eq DVar
Eq DVar =>
(DVar -> DVar -> Ordering)
-> (DVar -> DVar -> Bool)
-> (DVar -> DVar -> Bool)
-> (DVar -> DVar -> Bool)
-> (DVar -> DVar -> Bool)
-> (DVar -> DVar -> DVar)
-> (DVar -> DVar -> DVar)
-> Ord DVar
DVar -> DVar -> Bool
DVar -> DVar -> Ordering
DVar -> DVar -> DVar
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 :: DVar -> DVar -> Ordering
compare :: DVar -> DVar -> Ordering
$c< :: DVar -> DVar -> Bool
< :: DVar -> DVar -> Bool
$c<= :: DVar -> DVar -> Bool
<= :: DVar -> DVar -> Bool
$c> :: DVar -> DVar -> Bool
> :: DVar -> DVar -> Bool
$c>= :: DVar -> DVar -> Bool
>= :: DVar -> DVar -> Bool
$cmax :: DVar -> DVar -> DVar
max :: DVar -> DVar -> DVar
$cmin :: DVar -> DVar -> DVar
min :: DVar -> DVar -> DVar
Ord,Int -> DVar -> ShowS
[DVar] -> ShowS
DVar -> String
(Int -> DVar -> ShowS)
-> (DVar -> String) -> ([DVar] -> ShowS) -> Show DVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DVar -> ShowS
showsPrec :: Int -> DVar -> ShowS
$cshow :: DVar -> String
show :: DVar -> String
$cshowList :: [DVar] -> ShowS
showList :: [DVar] -> ShowS
Show,FuzzyM DVar
FuzzyM DVar -> Fuzzy DVar
forall a. FuzzyM a -> Fuzzy a
$cfuzzy :: FuzzyM DVar
fuzzy :: FuzzyM DVar
Fuzzy,DVar -> 𝐼 DVar
(DVar -> 𝐼 DVar) -> Shrinky DVar
forall a. (a -> 𝐼 a) -> Shrinky a
$cshrink :: DVar -> 𝐼 DVar
shrink :: DVar -> 𝐼 DVar
Shrinky)
makeLenses ''DVar

instance Pretty DVar where
  pretty :: DVar -> Doc
pretty (DVar ℕ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]

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

pDVarTail ∷ CParser TokenBasic DVar
pDVarTail :: CParser TokenBasic DVar
pDVarTail = ℕ64 -> DVar
DVar (ℕ64 -> DVar) -> CParser TokenBasic ℕ64 -> CParser TokenBasic DVar
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic ℕ64
cpNat64

pDVar ∷ CParser TokenBasic DVar
pDVar :: CParser TokenBasic DVar
pDVar = 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 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 DVar
pDVarTail

---------------------------------------------------------------------
-- ==== --
-- NVar --
-- ==== --
---------------------------------------------------------------------

-- Named variables with a De Bruijn index
-- λ x. λ x. x:0
--        └───┘
-- λ x. λ x. x:1
--   └────────┘
data NVar = NVar
  { NVar -> DVar
nvarIndex ∷ DVar
  , NVar -> Name
nvarName  ∷ Name
  } deriving (NVar -> NVar -> Bool
(NVar -> NVar -> Bool) -> (NVar -> NVar -> Bool) -> Eq NVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NVar -> NVar -> Bool
== :: NVar -> NVar -> Bool
$c/= :: NVar -> NVar -> Bool
/= :: NVar -> NVar -> Bool
Eq,Eq NVar
Eq NVar =>
(NVar -> NVar -> Ordering)
-> (NVar -> NVar -> Bool)
-> (NVar -> NVar -> Bool)
-> (NVar -> NVar -> Bool)
-> (NVar -> NVar -> Bool)
-> (NVar -> NVar -> NVar)
-> (NVar -> NVar -> NVar)
-> Ord NVar
NVar -> NVar -> Bool
NVar -> NVar -> Ordering
NVar -> NVar -> NVar
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 :: NVar -> NVar -> Ordering
compare :: NVar -> NVar -> Ordering
$c< :: NVar -> NVar -> Bool
< :: NVar -> NVar -> Bool
$c<= :: NVar -> NVar -> Bool
<= :: NVar -> NVar -> Bool
$c> :: NVar -> NVar -> Bool
> :: NVar -> NVar -> Bool
$c>= :: NVar -> NVar -> Bool
>= :: NVar -> NVar -> Bool
$cmax :: NVar -> NVar -> NVar
max :: NVar -> NVar -> NVar
$cmin :: NVar -> NVar -> NVar
min :: NVar -> NVar -> NVar
Ord,Int -> NVar -> ShowS
[NVar] -> ShowS
NVar -> String
(Int -> NVar -> ShowS)
-> (NVar -> String) -> ([NVar] -> ShowS) -> Show NVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NVar -> ShowS
showsPrec :: Int -> NVar -> ShowS
$cshow :: NVar -> String
show :: NVar -> String
$cshowList :: [NVar] -> ShowS
showList :: [NVar] -> ShowS
Show)
makeLenses ''NVar

nvar_Name ∷ Name → NVar
nvar_Name :: Name -> NVar
nvar_Name = DVar -> Name -> NVar
NVar (DVar -> Name -> NVar) -> DVar -> Name -> NVar
forall a b. (a -> b) -> a -> b
$ ℕ64 -> DVar
DVar ℕ64
0

name_NVarL ∷ NVar ⌲ Name
name_NVarL :: NVar ⌲ Name
name_NVarL = (Name -> NVar) -> (NVar -> 𝑂 Name) -> NVar ⌲ Name
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism Name -> NVar
nvar_Name ((NVar -> 𝑂 Name) -> NVar ⌲ Name)
-> (NVar -> 𝑂 Name) -> NVar ⌲ Name
forall a b. (a -> b) -> a -> b
$ \ (NVar DVar
n Name
x) → if DVar
n DVar -> DVar -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64 -> DVar
DVar ℕ64
0 then Name -> 𝑂 Name
forall a. a -> 𝑂 a
Some Name
x else 𝑂 Name
forall a. 𝑂 a
None

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

instance Fuzzy NVar where 
  fuzzy :: FuzzyM NVar
fuzzy = (DVar -> Name -> NVar) -> FuzzyM (DVar -> Name -> NVar)
forall a. a -> FuzzyM a
forall (m :: * -> *) a. Return m => a -> m a
return DVar -> Name -> NVar
NVar FuzzyM (DVar -> Name -> NVar)
-> FuzzyM DVar -> FuzzyM (Name -> NVar)
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
⊡ FuzzyM DVar
forall a. Fuzzy a => FuzzyM a
fuzzy FuzzyM (Name -> NVar) -> FuzzyM Name -> FuzzyM NVar
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
⊡ FuzzyM Name
forall a. Fuzzy a => FuzzyM a
fuzzy

instance Shrinky NVar where 
  shrink :: NVar -> 𝐼 NVar
shrink (NVar DVar
n Name
x) = do
    (DVar
n',Name
x') ← (DVar, Name) -> 𝐼 (DVar, Name)
forall a. Shrinky a => a -> 𝐼 a
shrink (DVar
n,Name
x)
    NVar -> 𝐼 NVar
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (NVar -> 𝐼 NVar) -> NVar -> 𝐼 NVar
forall a b. (a -> b) -> a -> b
$ DVar -> Name -> NVar
NVar DVar
n' Name
x'

instance Pretty NVar where
  pretty :: NVar -> Doc
pretty (NVar DVar
n 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
    , if DVar
n DVar -> DVar -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ64 -> DVar
DVar ℕ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 -> 𝕊) -> ℕ64 -> 𝕊
forall a b. (a -> b) -> a -> b
$ DVar -> ℕ64
unDVar DVar
n]
    ]

syntaxNVar ∷ LexerBasicSyntax
syntaxNVar :: LexerBasicSyntax
syntaxNVar = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxName
  , LexerBasicSyntax
syntaxDVar
  ]

pNVarTail ∷ Name → CParser TokenBasic NVar
pNVarTail :: Name -> CParser TokenBasic NVar
pNVarTail Name
x = do
  DVar
n ← DVar -> 𝑂 DVar -> DVar
forall a. a -> 𝑂 a -> a
ifNone (ℕ64 -> DVar
DVar ℕ64
0) (𝑂 DVar -> DVar)
-> CParser TokenBasic (𝑂 DVar) -> CParser TokenBasic DVar
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic DVar -> CParser TokenBasic (𝑂 DVar)
forall t a. Ord t => CParser t a -> CParser t (𝑂 a)
cpOptional (CParser TokenBasic DVar -> CParser TokenBasic (𝑂 DVar))
-> CParser TokenBasic DVar -> CParser TokenBasic (𝑂 DVar)
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 DVar
pDVarTail
  NVar -> CParser TokenBasic NVar
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (NVar -> CParser TokenBasic NVar)
-> NVar -> CParser TokenBasic NVar
forall a b. (a -> b) -> a -> b
$ DVar -> Name -> NVar
NVar DVar
n Name
x

pNVar ∷ CParser TokenBasic NVar
pNVar :: CParser TokenBasic NVar
pNVar = do
  Name
x ← CParser TokenBasic Name
pName
  Name -> CParser TokenBasic NVar
pNVarTail Name
x

---------------------------------------------------------------------
-- ==== --
-- GVar --
-- ==== --
---------------------------------------------------------------------

-- Global Variables
newtype GVar = GVar { GVar -> Name
unGVar ∷ Name }
  deriving (GVar -> GVar -> Bool
(GVar -> GVar -> Bool) -> (GVar -> GVar -> Bool) -> Eq GVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GVar -> GVar -> Bool
== :: GVar -> GVar -> Bool
$c/= :: GVar -> GVar -> Bool
/= :: GVar -> GVar -> Bool
Eq,Eq GVar
Eq GVar =>
(GVar -> GVar -> Ordering)
-> (GVar -> GVar -> Bool)
-> (GVar -> GVar -> Bool)
-> (GVar -> GVar -> Bool)
-> (GVar -> GVar -> Bool)
-> (GVar -> GVar -> GVar)
-> (GVar -> GVar -> GVar)
-> Ord GVar
GVar -> GVar -> Bool
GVar -> GVar -> Ordering
GVar -> GVar -> GVar
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 :: GVar -> GVar -> Ordering
compare :: GVar -> GVar -> Ordering
$c< :: GVar -> GVar -> Bool
< :: GVar -> GVar -> Bool
$c<= :: GVar -> GVar -> Bool
<= :: GVar -> GVar -> Bool
$c> :: GVar -> GVar -> Bool
> :: GVar -> GVar -> Bool
$c>= :: GVar -> GVar -> Bool
>= :: GVar -> GVar -> Bool
$cmax :: GVar -> GVar -> GVar
max :: GVar -> GVar -> GVar
$cmin :: GVar -> GVar -> GVar
min :: GVar -> GVar -> GVar
Ord,Int -> GVar -> ShowS
[GVar] -> ShowS
GVar -> String
(Int -> GVar -> ShowS)
-> (GVar -> String) -> ([GVar] -> ShowS) -> Show GVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> GVar -> ShowS
showsPrec :: Int -> GVar -> ShowS
$cshow :: GVar -> String
show :: GVar -> String
$cshowList :: [GVar] -> ShowS
showList :: [GVar] -> ShowS
Show,FuzzyM GVar
FuzzyM GVar -> Fuzzy GVar
forall a. FuzzyM a -> Fuzzy a
$cfuzzy :: FuzzyM GVar
fuzzy :: FuzzyM GVar
Fuzzy,GVar -> 𝐼 GVar
(GVar -> 𝐼 GVar) -> Shrinky GVar
forall a. (a -> 𝐼 a) -> Shrinky a
$cshrink :: GVar -> 𝐼 GVar
shrink :: GVar -> 𝐼 GVar
Shrinky)
makeLenses ''GVar

instance Pretty GVar where
  pretty :: GVar -> Doc
pretty (GVar 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 𝕊
":g"]

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

pGVarTail ∷ Name → CParser TokenBasic GVar
pGVarTail :: Name -> CParser TokenBasic GVar
pGVarTail 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
$ 𝕊 -> CParser TokenBasic TokenBasic
cpSyntax 𝕊
":g"
  GVar -> CParser TokenBasic GVar
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (GVar -> CParser TokenBasic GVar)
-> GVar -> CParser TokenBasic GVar
forall a b. (a -> b) -> a -> b
$ Name -> GVar
GVar Name
x

pGVar ∷ CParser TokenBasic GVar
pGVar :: CParser TokenBasic GVar
pGVar = do
  Name
x ← CParser TokenBasic Name
pName
  Name -> CParser TokenBasic GVar
pGVarTail Name
x

---------------------------------------------------------------------
-- ==== --
-- SVar --
-- ==== --
---------------------------------------------------------------------

-- Scoped Variables: either De Bruijn scoped or Named scoped
data SVar =
    D_SVar DVar
  | N_SVar NVar
  deriving (SVar -> SVar -> Bool
(SVar -> SVar -> Bool) -> (SVar -> SVar -> Bool) -> Eq SVar
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SVar -> SVar -> Bool
== :: SVar -> SVar -> Bool
$c/= :: SVar -> SVar -> Bool
/= :: SVar -> SVar -> Bool
Eq,Eq SVar
Eq SVar =>
(SVar -> SVar -> Ordering)
-> (SVar -> SVar -> Bool)
-> (SVar -> SVar -> Bool)
-> (SVar -> SVar -> Bool)
-> (SVar -> SVar -> Bool)
-> (SVar -> SVar -> SVar)
-> (SVar -> SVar -> SVar)
-> Ord SVar
SVar -> SVar -> Bool
SVar -> SVar -> Ordering
SVar -> SVar -> SVar
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 :: SVar -> SVar -> Ordering
compare :: SVar -> SVar -> Ordering
$c< :: SVar -> SVar -> Bool
< :: SVar -> SVar -> Bool
$c<= :: SVar -> SVar -> Bool
<= :: SVar -> SVar -> Bool
$c> :: SVar -> SVar -> Bool
> :: SVar -> SVar -> Bool
$c>= :: SVar -> SVar -> Bool
>= :: SVar -> SVar -> Bool
$cmax :: SVar -> SVar -> SVar
max :: SVar -> SVar -> SVar
$cmin :: SVar -> SVar -> SVar
min :: SVar -> SVar -> SVar
Ord,Int -> SVar -> ShowS
[SVar] -> ShowS
SVar -> String
(Int -> SVar -> ShowS)
-> (SVar -> String) -> ([SVar] -> ShowS) -> Show SVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SVar -> ShowS
showsPrec :: Int -> SVar -> ShowS
$cshow :: SVar -> String
show :: SVar -> String
$cshowList :: [SVar] -> ShowS
showList :: [SVar] -> ShowS
Show)
makePrisms ''SVar
makePrettyUnion ''SVar

mkSVar ∷ SName → DVar → SVar
mkSVar :: SName -> DVar -> SVar
mkSVar SName
xO DVar
n = case SName
xO of
  SName
D_SName → DVar -> SVar
D_SVar DVar
n
  N_SName Name
x → NVar -> SVar
N_SVar (NVar -> SVar) -> NVar -> SVar
forall a b. (a -> b) -> a -> b
$ DVar -> Name -> NVar
NVar DVar
n Name
x

svar_Name ∷ Name → SVar
svar_Name :: Name -> SVar
svar_Name = NVar -> SVar
N_SVar (NVar -> SVar) -> (Name -> NVar) -> Name -> SVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Name -> NVar
nvar_Name

svarName ∷ SVar → SName
svarName :: SVar -> SName
svarName = \case
  D_SVar DVar
_          → SName
D_SName
  N_SVar (NVar DVar
_ Name
x) → Name -> SName
N_SName Name
x

svarLevel ∷ SVar → DVar
svarLevel :: SVar -> DVar
svarLevel = \case
  D_SVar DVar
n → DVar
n
  N_SVar (NVar DVar
n Name
_x) → DVar
n

instance Fuzzy SVar where 
  fuzzy :: FuzzyM SVar
fuzzy = [() -> FuzzyM SVar] -> FuzzyM SVar
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose
    [ \ () → DVar -> SVar
D_SVar (DVar -> SVar) -> FuzzyM DVar -> FuzzyM SVar
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM DVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → NVar -> SVar
N_SVar (NVar -> SVar) -> FuzzyM NVar -> FuzzyM SVar
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM NVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]

instance Shrinky SVar where 
  shrink :: SVar -> 𝐼 SVar
shrink = \case
    D_SVar DVar
x → DVar -> SVar
D_SVar (DVar -> SVar) -> 𝐼 DVar -> 𝐼 SVar
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ DVar -> 𝐼 DVar
forall a. Shrinky a => a -> 𝐼 a
shrink DVar
x
    N_SVar NVar
x → NVar -> SVar
N_SVar (NVar -> SVar) -> 𝐼 NVar -> 𝐼 SVar
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ NVar -> 𝐼 NVar
forall a. Shrinky a => a -> 𝐼 a
shrink NVar
x

---------------------------------------------------------------------
-- === --
-- Var --
-- === --
---------------------------------------------------------------------

-- Variables: either De Bruijn, Named or Global
data Var =
    D_Var DVar
  | N_Var NVar
  | G_Var GVar
  deriving (Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
/= :: Var -> Var -> Bool
Eq,Eq Var
Eq Var =>
(Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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 :: Var -> Var -> Ordering
compare :: Var -> Var -> Ordering
$c< :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
>= :: Var -> Var -> Bool
$cmax :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
min :: Var -> Var -> Var
Ord,Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Var -> ShowS
showsPrec :: Int -> Var -> ShowS
$cshow :: Var -> String
show :: Var -> String
$cshowList :: [Var] -> ShowS
showList :: [Var] -> ShowS
Show)
makePrisms ''Var
makePrettyUnion ''Var

var_Name ∷ Name → Var
var_Name :: Name -> Var
var_Name = NVar -> Var
N_Var (NVar -> Var) -> (Name -> NVar) -> Name -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Name -> NVar
nvar_Name

var_SVar ∷ SVar → Var
var_SVar :: SVar -> Var
var_SVar = \case
  D_SVar DVar
x → DVar -> Var
D_Var DVar
x
  N_SVar NVar
x → NVar -> Var
N_Var NVar
x

name_VarL ∷ Var ⌲ Name
name_VarL :: Var ⌲ Name
name_VarL = NVar ⌲ Name
name_NVarL (NVar ⌲ Name) -> (Var ⌲ NVar) -> Var ⌲ 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
⊚ Var ⌲ NVar
n_VarL

gensymVar ∷ (Monad m,MonadState s m) ⇒ s ⟢ ℕ64 → 𝕊 → m Var
gensymVar :: forall (m :: * -> *) s.
(Monad m, MonadState s m) =>
(s ⟢ ℕ64) -> 𝕊 -> m Var
gensymVar s ⟢ ℕ64
ℓ 𝕊
s = NVar -> Var
N_Var (NVar -> Var) -> m NVar -> m Var
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

instance Fuzzy Var where
  fuzzy :: FuzzyM Var
fuzzy = [() -> FuzzyM Var] -> FuzzyM Var
forall (m :: * -> *) a t.
(Monad m, MonadRand m, ToIter (() -> m a) t) =>
t -> m a
rchoose
    [ \ () → DVar -> Var
D_Var (DVar -> Var) -> FuzzyM DVar -> FuzzyM Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM DVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → NVar -> Var
N_Var (NVar -> Var) -> FuzzyM NVar -> FuzzyM Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM NVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    , \ () → GVar -> Var
G_Var (GVar -> Var) -> FuzzyM GVar -> FuzzyM Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ FuzzyM GVar
forall a. Fuzzy a => FuzzyM a
fuzzy
    ]

instance Shrinky Var where
  shrink :: Var -> 𝐼 Var
shrink = \case
    D_Var DVar
x → DVar -> Var
D_Var (DVar -> Var) -> 𝐼 DVar -> 𝐼 Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ DVar -> 𝐼 DVar
forall a. Shrinky a => a -> 𝐼 a
shrink DVar
x
    N_Var NVar
x → NVar -> Var
N_Var (NVar -> Var) -> 𝐼 NVar -> 𝐼 Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ NVar -> 𝐼 NVar
forall a. Shrinky a => a -> 𝐼 a
shrink NVar
x
    G_Var GVar
x → GVar -> Var
G_Var (GVar -> Var) -> 𝐼 GVar -> 𝐼 Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ GVar -> 𝐼 GVar
forall a. Shrinky a => a -> 𝐼 a
shrink GVar
x

syntaxVar ∷ LexerBasicSyntax
syntaxVar :: LexerBasicSyntax
syntaxVar = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxName
  , LexerBasicSyntax
syntaxDVar
  , LexerBasicSyntax
syntaxNVar
  , LexerBasicSyntax
syntaxGVar
  ]

pVar ∷ CParser TokenBasic Var
pVar :: CParser TokenBasic Var
pVar = [CParser TokenBasic Var] -> CParser TokenBasic Var
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ DVar -> Var
D_Var (DVar -> Var) -> CParser TokenBasic DVar -> CParser TokenBasic Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic DVar
pDVar
  , do Name
x ← CParser TokenBasic Name
pName
       [CParser TokenBasic Var] -> CParser TokenBasic Var
forall a t. (Monoid a, ToIter a t) => t -> a
concat 
         [ NVar -> Var
N_Var (NVar -> Var) -> CParser TokenBasic NVar -> CParser TokenBasic Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> CParser TokenBasic NVar
pNVarTail Name
x
         , GVar -> Var
G_Var (GVar -> Var) -> CParser TokenBasic GVar -> CParser TokenBasic Var
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> CParser TokenBasic GVar
pGVarTail Name
x
         ]
  ]

---------------------------------------------------------------------
-- ======= --
-- DVarInf --
-- ======= --
---------------------------------------------------------------------

-- De Bruijn Variables with an extra "∞" element
data DVarInf =
    Var_DVI DVar
  | Inf_DVI
  deriving (DVarInf -> DVarInf -> Bool
(DVarInf -> DVarInf -> Bool)
-> (DVarInf -> DVarInf -> Bool) -> Eq DVarInf
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DVarInf -> DVarInf -> Bool
== :: DVarInf -> DVarInf -> Bool
$c/= :: DVarInf -> DVarInf -> Bool
/= :: DVarInf -> DVarInf -> Bool
Eq,Eq DVarInf
Eq DVarInf =>
(DVarInf -> DVarInf -> Ordering)
-> (DVarInf -> DVarInf -> Bool)
-> (DVarInf -> DVarInf -> Bool)
-> (DVarInf -> DVarInf -> Bool)
-> (DVarInf -> DVarInf -> Bool)
-> (DVarInf -> DVarInf -> DVarInf)
-> (DVarInf -> DVarInf -> DVarInf)
-> Ord DVarInf
DVarInf -> DVarInf -> Bool
DVarInf -> DVarInf -> Ordering
DVarInf -> DVarInf -> DVarInf
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 :: DVarInf -> DVarInf -> Ordering
compare :: DVarInf -> DVarInf -> Ordering
$c< :: DVarInf -> DVarInf -> Bool
< :: DVarInf -> DVarInf -> Bool
$c<= :: DVarInf -> DVarInf -> Bool
<= :: DVarInf -> DVarInf -> Bool
$c> :: DVarInf -> DVarInf -> Bool
> :: DVarInf -> DVarInf -> Bool
$c>= :: DVarInf -> DVarInf -> Bool
>= :: DVarInf -> DVarInf -> Bool
$cmax :: DVarInf -> DVarInf -> DVarInf
max :: DVarInf -> DVarInf -> DVarInf
$cmin :: DVarInf -> DVarInf -> DVarInf
min :: DVarInf -> DVarInf -> DVarInf
Ord,Int -> DVarInf -> ShowS
[DVarInf] -> ShowS
DVarInf -> String
(Int -> DVarInf -> ShowS)
-> (DVarInf -> String) -> ([DVarInf] -> ShowS) -> Show DVarInf
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DVarInf -> ShowS
showsPrec :: Int -> DVarInf -> ShowS
$cshow :: DVarInf -> String
show :: DVarInf -> String
$cshowList :: [DVarInf] -> ShowS
showList :: [DVarInf] -> ShowS
Show)
makePrisms ''DVarInf

instance Pretty DVarInf where
  pretty :: DVarInf -> Doc
pretty = \case
    Var_DVI DVar
x → DVar -> Doc
forall a. Pretty a => a -> Doc
pretty DVar
x
    DVarInf
Inf_DVI   → 𝕊 -> Doc
ppPun 𝕊
"•:∞"

syntaxDVarInf ∷ LexerBasicSyntax
syntaxDVarInf :: LexerBasicSyntax
syntaxDVarInf = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxDVar
  , LexerBasicSyntax
forall a. Null a => a
null { lexerBasicSyntaxPuns = pow ["INF","∞"] }
  ]

pDVarInfTail ∷ CParser  TokenBasic DVarInf
pDVarInfTail :: CParser TokenBasic DVarInf
pDVarInfTail = [CParser TokenBasic DVarInf] -> CParser TokenBasic DVarInf
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ DVar -> DVarInf
Var_DVI (DVar -> DVarInf)
-> CParser TokenBasic DVar -> CParser TokenBasic DVarInf
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic DVar
pDVarTail
  , 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
$ (𝕊 -> CParser TokenBasic TokenBasic)
-> [𝕊] -> [CParser TokenBasic TokenBasic]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝕊 -> CParser TokenBasic TokenBasic
cpSyntax [𝕊
"INF",𝕊
"∞"]
       DVarInf -> CParser TokenBasic DVarInf
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return DVarInf
Inf_DVI
  ]

pDVarInf ∷ CParser TokenBasic DVarInf
pDVarInf :: CParser TokenBasic DVarInf
pDVarInf = 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 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 DVarInf
pDVarInfTail

---------------------------------------------------------------------
-- ======= --
-- NVarInf --
-- ======= --
---------------------------------------------------------------------

-- Named Variables where indices have an extra ∞ element
data NVarInf = NVarInf
  { NVarInf -> DVarInf
nvarInfIndex ∷ DVarInf
  , NVarInf -> Name
nvarInfName  ∷ Name
  } deriving (NVarInf -> NVarInf -> Bool
(NVarInf -> NVarInf -> Bool)
-> (NVarInf -> NVarInf -> Bool) -> Eq NVarInf
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NVarInf -> NVarInf -> Bool
== :: NVarInf -> NVarInf -> Bool
$c/= :: NVarInf -> NVarInf -> Bool
/= :: NVarInf -> NVarInf -> Bool
Eq,Eq NVarInf
Eq NVarInf =>
(NVarInf -> NVarInf -> Ordering)
-> (NVarInf -> NVarInf -> Bool)
-> (NVarInf -> NVarInf -> Bool)
-> (NVarInf -> NVarInf -> Bool)
-> (NVarInf -> NVarInf -> Bool)
-> (NVarInf -> NVarInf -> NVarInf)
-> (NVarInf -> NVarInf -> NVarInf)
-> Ord NVarInf
NVarInf -> NVarInf -> Bool
NVarInf -> NVarInf -> Ordering
NVarInf -> NVarInf -> NVarInf
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 :: NVarInf -> NVarInf -> Ordering
compare :: NVarInf -> NVarInf -> Ordering
$c< :: NVarInf -> NVarInf -> Bool
< :: NVarInf -> NVarInf -> Bool
$c<= :: NVarInf -> NVarInf -> Bool
<= :: NVarInf -> NVarInf -> Bool
$c> :: NVarInf -> NVarInf -> Bool
> :: NVarInf -> NVarInf -> Bool
$c>= :: NVarInf -> NVarInf -> Bool
>= :: NVarInf -> NVarInf -> Bool
$cmax :: NVarInf -> NVarInf -> NVarInf
max :: NVarInf -> NVarInf -> NVarInf
$cmin :: NVarInf -> NVarInf -> NVarInf
min :: NVarInf -> NVarInf -> NVarInf
Ord,Int -> NVarInf -> ShowS
[NVarInf] -> ShowS
NVarInf -> String
(Int -> NVarInf -> ShowS)
-> (NVarInf -> String) -> ([NVarInf] -> ShowS) -> Show NVarInf
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NVarInf -> ShowS
showsPrec :: Int -> NVarInf -> ShowS
$cshow :: NVarInf -> String
show :: NVarInf -> String
$cshowList :: [NVarInf] -> ShowS
showList :: [NVarInf] -> ShowS
Show)
makeLenses ''NVarInf

instance Pretty NVarInf where
  pretty :: NVarInf -> Doc
pretty (NVarInf DVarInf
n 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
    , case DVarInf
n of
        Var_DVI DVar
n' | DVar
n' DVar -> DVar -> Bool
forall a. Eq a => a -> a -> Bool
≢ ℕ64 -> DVar
DVar ℕ64
0 → 𝕊 -> Doc
ppBdr (𝕊 -> 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 -> 𝕊) -> ℕ64 -> 𝕊
forall a b. (a -> b) -> a -> b
$ DVar -> ℕ64
unDVar DVar
n']
        DVarInf
_ → Doc
forall a. Null a => a
null
    ]

syntaxNVarInf ∷ LexerBasicSyntax
syntaxNVarInf :: LexerBasicSyntax
syntaxNVarInf = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxName
  , LexerBasicSyntax
syntaxDVarInf
  ]

pNVarInfTail ∷ Name → CParser TokenBasic NVarInf
pNVarInfTail :: Name -> CParser TokenBasic NVarInf
pNVarInfTail 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
$ 𝕊 -> CParser TokenBasic TokenBasic
cpSyntax 𝕊
":"
  DVarInf
n ← CParser TokenBasic DVarInf
pDVarInfTail
  NVarInf -> CParser TokenBasic NVarInf
forall a. a -> CParser TokenBasic a
forall (m :: * -> *) a. Return m => a -> m a
return (NVarInf -> CParser TokenBasic NVarInf)
-> NVarInf -> CParser TokenBasic NVarInf
forall a b. (a -> b) -> a -> b
$ DVarInf -> Name -> NVarInf
NVarInf DVarInf
n Name
x

pNVarInf ∷ CParser TokenBasic NVarInf
pNVarInf :: CParser TokenBasic NVarInf
pNVarInf = do
  Name
x ← CParser TokenBasic Name
pName
  Name -> CParser TokenBasic NVarInf
pNVarInfTail Name
x

---------------------------------------------------------------------
-- ====== --
-- VarInf --
-- ====== --
---------------------------------------------------------------------

data VarInf =
    D_VarInf DVarInf
  | N_VarInf NVarInf
  | G_VarInf GVar
  deriving (VarInf -> VarInf -> Bool
(VarInf -> VarInf -> Bool)
-> (VarInf -> VarInf -> Bool) -> Eq VarInf
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VarInf -> VarInf -> Bool
== :: VarInf -> VarInf -> Bool
$c/= :: VarInf -> VarInf -> Bool
/= :: VarInf -> VarInf -> Bool
Eq,Eq VarInf
Eq VarInf =>
(VarInf -> VarInf -> Ordering)
-> (VarInf -> VarInf -> Bool)
-> (VarInf -> VarInf -> Bool)
-> (VarInf -> VarInf -> Bool)
-> (VarInf -> VarInf -> Bool)
-> (VarInf -> VarInf -> VarInf)
-> (VarInf -> VarInf -> VarInf)
-> Ord VarInf
VarInf -> VarInf -> Bool
VarInf -> VarInf -> Ordering
VarInf -> VarInf -> VarInf
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 :: VarInf -> VarInf -> Ordering
compare :: VarInf -> VarInf -> Ordering
$c< :: VarInf -> VarInf -> Bool
< :: VarInf -> VarInf -> Bool
$c<= :: VarInf -> VarInf -> Bool
<= :: VarInf -> VarInf -> Bool
$c> :: VarInf -> VarInf -> Bool
> :: VarInf -> VarInf -> Bool
$c>= :: VarInf -> VarInf -> Bool
>= :: VarInf -> VarInf -> Bool
$cmax :: VarInf -> VarInf -> VarInf
max :: VarInf -> VarInf -> VarInf
$cmin :: VarInf -> VarInf -> VarInf
min :: VarInf -> VarInf -> VarInf
Ord,Int -> VarInf -> ShowS
[VarInf] -> ShowS
VarInf -> String
(Int -> VarInf -> ShowS)
-> (VarInf -> String) -> ([VarInf] -> ShowS) -> Show VarInf
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> VarInf -> ShowS
showsPrec :: Int -> VarInf -> ShowS
$cshow :: VarInf -> String
show :: VarInf -> String
$cshowList :: [VarInf] -> ShowS
showList :: [VarInf] -> ShowS
Show)
makePrisms ''VarInf
makePrettyUnion ''VarInf

syntaxVarInf ∷ LexerBasicSyntax
syntaxVarInf :: LexerBasicSyntax
syntaxVarInf = [LexerBasicSyntax] -> LexerBasicSyntax
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ LexerBasicSyntax
syntaxDVarInf
  , LexerBasicSyntax
syntaxNVarInf
  , LexerBasicSyntax
syntaxGVar
  ]

pVarInf ∷ CParser TokenBasic VarInf
pVarInf :: CParser TokenBasic VarInf
pVarInf = [CParser TokenBasic VarInf] -> CParser TokenBasic VarInf
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ DVarInf -> VarInf
D_VarInf (DVarInf -> VarInf)
-> CParser TokenBasic DVarInf -> CParser TokenBasic VarInf
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ CParser TokenBasic DVarInf
pDVarInf
  , do Name
x ← CParser TokenBasic Name
pName
       [CParser TokenBasic VarInf] -> CParser TokenBasic VarInf
forall a t. (Monoid a, ToIter a t) => t -> a
concat
         [ NVarInf -> VarInf
N_VarInf (NVarInf -> VarInf)
-> CParser TokenBasic NVarInf -> CParser TokenBasic VarInf
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> CParser TokenBasic NVarInf
pNVarInfTail Name
x
         , GVar -> VarInf
G_VarInf (GVar -> VarInf)
-> CParser TokenBasic GVar -> CParser TokenBasic VarInf
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> CParser TokenBasic GVar
pGVarTail Name
x
         ]
  ]

---------------------------------------------------------------------
-- ======== --
-- SVarView --
-- ======== --
---------------------------------------------------------------------

class SVarView s e | e→s where
  svarL ∷ s → e ⌲ SVar

svarScopeL ∷ ∀ s e. (SVarView s e) ⇒ s → SName → e ⌲ DVar
svarScopeL :: forall s e. SVarView s e => s -> SName -> e ⌲ DVar
svarScopeL s
s SName
xO = 
  let ctor ∷ DVar → e
      ctor :: DVar -> e
ctor = case SName
xO of
        SName
D_SName → \ DVar
n → (e ⌲ SVar) -> SVar -> e
forall a b. (a ⌲ b) -> b -> a
construct (s -> e ⌲ SVar
forall s e. SVarView s e => s -> e ⌲ SVar
svarL s
s) (SVar -> e) -> SVar -> e
forall a b. (a -> b) -> a -> b
$ DVar -> SVar
D_SVar DVar
n
        N_SName Name
x → \ DVar
n → (e ⌲ SVar) -> SVar -> e
forall a b. (a ⌲ b) -> b -> a
construct (s -> e ⌲ SVar
forall s e. SVarView s e => s -> e ⌲ SVar
svarL s
s) (SVar -> e) -> SVar -> e
forall a b. (a -> b) -> a -> b
$ NVar -> SVar
N_SVar (NVar -> SVar) -> NVar -> SVar
forall a b. (a -> b) -> a -> b
$ DVar -> Name -> NVar
NVar DVar
n Name
x
      dtor ∷ e → 𝑂 DVar
      dtor :: e -> 𝑂 DVar
dtor = case SName
xO of
        SName
D_SName → \ e
e → (e ⌲ DVar) -> e -> 𝑂 DVar
forall a b. (a ⌲ b) -> a -> 𝑂 b
view (SVar ⌲ DVar
d_SVarL (SVar ⌲ DVar) -> (e ⌲ SVar) -> e ⌲ DVar
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ s -> e ⌲ SVar
forall s e. SVarView s e => s -> e ⌲ SVar
svarL s
s) e
e
        N_SName Name
x → \ e
e → do
          NVar DVar
n Name
x' ← (e ⌲ NVar) -> e -> 𝑂 NVar
forall a b. (a ⌲ b) -> a -> 𝑂 b
view (SVar ⌲ NVar
n_SVarL (SVar ⌲ NVar) -> (e ⌲ SVar) -> e ⌲ NVar
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
⊚ s -> e ⌲ SVar
forall s e. SVarView s e => s -> e ⌲ SVar
svarL s
s) e
e
          Bool -> 𝑂 ()
forall (m :: * -> *). (Monad m, MonadFail m) => Bool -> m ()
guard (Bool -> 𝑂 ()) -> Bool -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
≡ Name
x'
          DVar -> 𝑂 DVar
forall a. a -> 𝑂 a
forall (m :: * -> *) a. Return m => a -> m a
return DVar
n
  in (DVar -> e) -> (e -> 𝑂 DVar) -> e ⌲ DVar
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism DVar -> e
ctor e -> 𝑂 DVar
dtor