module UVMHS.Lib.Parser.Mixfix where

import UVMHS.Core

import UVMHS.Lib.Annotated

import UVMHS.Lib.Parser.ParserContext
import UVMHS.Lib.Parser.CParser

-------------------
-- STATIC LEVELS --
-------------------

pDEF ∷ ℕ64
pLET,pSEP,pASC,pARR,pOR,pAND,pCMP,pCONS ∷ ℕ64
pBWAND,pBWOR,pBSHFT ∷ ℕ64
pPLUS,pTIMES,pNEG,pPOW,pFAC,pAPP,pREF,pIDX ∷ ℕ64
pTOP ∷ ℕ64

pDEF :: ℕ64
pDEF    = ℕ64
001  --  x = e

pLET :: ℕ64
pLET    = ℕ64
005  --  let fun
pSEP :: ℕ64
pSEP    = ℕ64
006  --  , ;
pASC :: ℕ64
pASC    = ℕ64
007  --  e : τ
pARR :: ℕ64
pARR    = ℕ64
010  --  →
pOR :: ℕ64
pOR     = ℕ64
020  --  ∨
pAND :: ℕ64
pAND    = ℕ64
030  --  ∧
pCMP :: ℕ64
pCMP    = ℕ64
040  --  ==
pCONS :: ℕ64
pCONS   = ℕ64
041  --  ∷

pBWAND :: ℕ64
pBWAND  = ℕ64
045  -- ⊻ ⩔
pBWOR :: ℕ64
pBWOR   = ℕ64
046  -- ⩓
pBSHFT :: ℕ64
pBSHFT  = ℕ64
047  -- ⋙ ⋘

pPLUS :: ℕ64
pPLUS   = ℕ64
050  --  + - ⩔ ⊻
pTIMES :: ℕ64
pTIMES  = ℕ64
060  --  * / ⩓
pNEG :: ℕ64
pNEG    = ℕ64
065  --  - (negation)
pPOW :: ℕ64
pPOW    = ℕ64
070  --  ^ ⋙ ⋘
pFAC :: ℕ64
pFAC    = ℕ64
090  --  !

pAPP :: ℕ64
pAPP    = ℕ64
200  --  ␣

pREF :: ℕ64
pREF    = ℕ64
250  --  *x &x
pIDX :: ℕ64
pIDX    = ℕ64
300  --  x.y x@y


pTOP :: ℕ64
pTOP    = ℕ64
999

-----------------------------------
-- Fully Functor/Comonad general --
-----------------------------------

data MixesF t f a = MixesF
  { forall t (f :: * -> *) a. MixesF t f a -> CParser t (f a -> a)
mixesFPrefix  ∷ CParser t (f a → a)
  , forall t (f :: * -> *) a. MixesF t f a -> CParser t (f a -> a)
mixesFPostfix ∷ CParser t (f a → a)
  , forall t (f :: * -> *) a.
MixesF t f a -> CParser t (f a -> f a -> a)
mixesFInfix  ∷ CParser t (f a → f a → a)
  , forall t (f :: * -> *) a.
MixesF t f a -> CParser t (f a -> f a -> a)
mixesFInfixL ∷ CParser t (f a → f a → a)
  , forall t (f :: * -> *) a.
MixesF t f a -> CParser t (f a -> f a -> a)
mixesFInfixR ∷ CParser t (f a → f a → a)
  }

instance Null (MixesF t f a) where null :: MixesF t f a
null = CParser t (f a -> a)
-> CParser t (f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> MixesF t f a
forall t (f :: * -> *) a.
CParser t (f a -> a)
-> CParser t (f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> MixesF t f a
MixesF CParser t (f a -> a)
forall a. Null a => a
null CParser t (f a -> a)
forall a. Null a => a
null CParser t (f a -> f a -> a)
forall a. Null a => a
null CParser t (f a -> f a -> a)
forall a. Null a => a
null CParser t (f a -> f a -> a)
forall a. Null a => a
null
instance (Ord t) ⇒ Append (MixesF t f a) where
  MixesF CParser t (f a -> a)
pre₁ CParser t (f a -> a)
post₁ CParser t (f a -> f a -> a)
inf₁ CParser t (f a -> f a -> a)
infl₁ CParser t (f a -> f a -> a)
infr₁ ⧺ :: MixesF t f a -> MixesF t f a -> MixesF t f a
⧺ MixesF CParser t (f a -> a)
pre₂ CParser t (f a -> a)
post₂ CParser t (f a -> f a -> a)
inf₂ CParser t (f a -> f a -> a)
infl₂ CParser t (f a -> f a -> a)
infr₂ = 
    CParser t (f a -> a)
-> CParser t (f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> MixesF t f a
forall t (f :: * -> *) a.
CParser t (f a -> a)
-> CParser t (f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> MixesF t f a
MixesF (CParser t (f a -> a)
pre₁ CParser t (f a -> a)
-> CParser t (f a -> a) -> CParser t (f a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (f a -> a)
pre₂) (CParser t (f a -> a)
post₁ CParser t (f a -> a)
-> CParser t (f a -> a) -> CParser t (f a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (f a -> a)
post₂) (CParser t (f a -> f a -> a)
inf₁ CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a) -> CParser t (f a -> f a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (f a -> f a -> a)
inf₂) (CParser t (f a -> f a -> a)
infl₁ CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a) -> CParser t (f a -> f a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (f a -> f a -> a)
infl₂) (CParser t (f a -> f a -> a) -> MixesF t f a)
-> CParser t (f a -> f a -> a) -> MixesF t f a
forall a b. (a -> b) -> a -> b
$ CParser t (f a -> f a -> a)
infr₁ CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a) -> CParser t (f a -> f a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (f a -> f a -> a)
infr₂
instance (Ord t) ⇒ Monoid (MixesF t f a)

data MixfixF t f a = MixfixF
  { forall t (f :: * -> *) a. MixfixF t f a -> CParser t a
mixfixFTerminals ∷ CParser t a
  , forall t (f :: * -> *) a. MixfixF t f a -> ℕ64 ⇰ MixesF t f a
mixfixFLevels ∷ ℕ64 ⇰ MixesF t f a
  }
instance Null (MixfixF t f a) where null :: MixfixF t f a
null = CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
forall t (f :: * -> *) a.
CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
MixfixF CParser t a
forall a. Null a => a
null ℕ64 ⇰ MixesF t f a
forall a. Null a => a
null
instance (Ord t) ⇒ Append (MixfixF t f a) where MixfixF CParser t a
ts₁ ℕ64 ⇰ MixesF t f a
ls₁ ⧺ :: MixfixF t f a -> MixfixF t f a -> MixfixF t f a
⧺ MixfixF CParser t a
ts₂ ℕ64 ⇰ MixesF t f a
ls₂ = CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
forall t (f :: * -> *) a.
CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
MixfixF (CParser t a
ts₁ CParser t a -> CParser t a -> CParser t a
forall a. Append a => a -> a -> a
⧺ CParser t a
ts₂) (ℕ64 ⇰ MixesF t f a
ls₁ (ℕ64 ⇰ MixesF t f a) -> (ℕ64 ⇰ MixesF t f a) -> ℕ64 ⇰ MixesF t f a
forall a. Append a => a -> a -> a
⧺ ℕ64 ⇰ MixesF t f a
ls₂)
instance (Ord t) ⇒ Monoid (MixfixF t f a)

onlyTerminalsF ∷ MixfixF t f a → MixfixF t f a
onlyTerminalsF :: forall t (f :: * -> *) a. MixfixF t f a -> MixfixF t f a
onlyTerminalsF MixfixF t f a
m = CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
forall t (f :: * -> *) a.
CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
MixfixF (MixfixF t f a -> CParser t a
forall t (f :: * -> *) a. MixfixF t f a -> CParser t a
mixfixFTerminals MixfixF t f a
m) ℕ64 ⇰ MixesF t f a
forall a. Null a => a
null

fmixPrefix ∷ ℕ64 → CParser t (f a → a) → MixfixF t f a
fmixPrefix :: forall t (f :: * -> *) a.
ℕ64 -> CParser t (f a -> a) -> MixfixF t f a
fmixPrefix ℕ64
l CParser t (f a -> a)
p = MixfixF t Any a
forall a. Null a => a
null { mixfixFLevels = dict [ l ↦♭ null {mixesFPrefix = p} ] }

fmixPostfix ∷ ℕ64 → CParser t (f a → a) → MixfixF t f a
fmixPostfix :: forall t (f :: * -> *) a.
ℕ64 -> CParser t (f a -> a) -> MixfixF t f a
fmixPostfix ℕ64
l CParser t (f a -> a)
p = MixfixF t Any a
forall a. Null a => a
null { mixfixFLevels = dict [ l ↦♭ null {mixesFPostfix = p} ] }

fmixInfix ∷ ℕ64 → CParser t (f a → f a → a) → MixfixF t f a
fmixInfix :: forall t (f :: * -> *) a.
ℕ64 -> CParser t (f a -> f a -> a) -> MixfixF t f a
fmixInfix ℕ64
l CParser t (f a -> f a -> a)
p = MixfixF t Any a
forall a. Null a => a
null { mixfixFLevels = dict [ l ↦♭ null {mixesFInfix = p} ] }

fmixInfixL ∷ ℕ64 → CParser t (f a → f a → a) → MixfixF t f a
fmixInfixL :: forall t (f :: * -> *) a.
ℕ64 -> CParser t (f a -> f a -> a) -> MixfixF t f a
fmixInfixL ℕ64
l CParser t (f a -> f a -> a)
p = MixfixF t Any a
forall a. Null a => a
null { mixfixFLevels = dict [ l ↦♭ null {mixesFInfixL = p} ] }

fmixInfixR ∷ ℕ64 → CParser t (f a → f a → a) → MixfixF t f a
fmixInfixR :: forall t (f :: * -> *) a.
ℕ64 -> CParser t (f a -> f a -> a) -> MixfixF t f a
fmixInfixR ℕ64
l CParser t (f a -> f a -> a)
p = MixfixF t Any a
forall a. Null a => a
null { mixfixFLevels = dict [ l ↦♭ null {mixesFInfixR = p} ] }

fmixTerminal ∷ CParser t a → MixfixF t f a
fmixTerminal :: forall t a (f :: * -> *). CParser t a -> MixfixF t f a
fmixTerminal CParser t a
p = MixfixF t f a
forall a. Null a => a
null { mixfixFTerminals = p}

-- PRE PRE x INFR PRE PRE y
-- ≈
-- PRE (PRE (x INFR (PRE (PRE y))))
-- 
-- x POST POST INFL y POST POST
-- ≈
-- ((((x POST) POST) INFL y) POST) POST

fmixfix ∷ 
  ∀ t f a. (Ord t,Comonad f)
  ⇒ (CParser t (f a) → CParser t (f a)) 
  → (CParser t (f a) → CParser t (f a)) 
  → (CParser t a → CParser t (f a)) 
  → MixfixF t f a 
  → CParser t (f a)
fmixfix :: forall t (f :: * -> *) a.
(Ord t, Comonad f) =>
(CParser t (f a) -> CParser t (f a))
-> (CParser t (f a) -> CParser t (f a))
-> (CParser t a -> CParser t (f a))
-> MixfixF t f a
-> CParser t (f a)
fmixfix CParser t (f a) -> CParser t (f a)
new CParser t (f a) -> CParser t (f a)
bracket CParser t a -> CParser t (f a)
cxt (MixfixF CParser t a
terms ℕ64 ⇰ MixesF t f a
levels₀) = (ℕ64 ⇰ MixesF t f a) -> CParser t (f a)
loop ℕ64 ⇰ MixesF t f a
levels₀
  where
    loop ∷ ℕ64 ⇰ MixesF t f a → CParser t (f a)
    loop :: (ℕ64 ⇰ MixesF t f a) -> CParser t (f a)
loop ℕ64 ⇰ MixesF t f a
levels = case (ℕ64 ⇰ MixesF t f a)
-> 𝑂 ((ℕ64 ∧ MixesF t f a) ∧ (ℕ64 ⇰ MixesF t f a))
forall a. (ℕ64 ⇰ a) -> 𝑂 ((ℕ64 ∧ a) ∧ (ℕ64 ⇰ a))
forall k s (d :: * -> *) a. Dict k s d => d a -> 𝑂 ((k ∧ a) ∧ d a)
dminView ℕ64 ⇰ MixesF t f a
levels of
      𝑂 ((ℕ64 ∧ MixesF t f a) ∧ (ℕ64 ⇰ MixesF t f a))
None → CParser t (f a) -> CParser t (f a)
new (CParser t (f a) -> CParser t (f a))
-> CParser t (f a) -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ CParser t a -> CParser t (f a)
cxt CParser t a
terms
      Some ((ℕ64
i :* MixesF t f a
mixes) :* ℕ64 ⇰ MixesF t f a
levels') →
        let msg :: 𝕊
msg = 𝕊
"lvl " 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ ℂ -> ℕ -> 𝕊 -> 𝕊
alignRightFill ℂ
'0' ℕ
3 (ℕ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℕ64
i)
        in 
        CParser t (f a) -> CParser t (f a)
new (CParser t (f a) -> CParser t (f a))
-> CParser t (f a) -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ CParser t a -> CParser t (f a)
cxt (CParser t a -> CParser t (f a)) -> CParser t a -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ 𝕊 -> MixesF t f a -> CParser t (f a) -> CParser t a
buildLevelDirected 𝕊
msg MixesF t f a
mixes (CParser t (f a) -> CParser t a) -> CParser t (f a) -> CParser t a
forall a b. (a -> b) -> a -> b
$ 
        CParser t (f a) -> CParser t (f a)
new (CParser t (f a) -> CParser t (f a))
-> CParser t (f a) -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ CParser t a -> CParser t (f a)
cxt (CParser t a -> CParser t (f a)) -> CParser t a -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ 𝕊 -> MixesF t f a -> CParser t (f a) -> CParser t a
buildLevelNondirected 𝕊
msg MixesF t f a
mixes (CParser t (f a) -> CParser t a) -> CParser t (f a) -> CParser t a
forall a b. (a -> b) -> a -> b
$ 
        (ℕ64 ⇰ MixesF t f a) -> CParser t (f a)
loop ℕ64 ⇰ MixesF t f a
levels'
    buildLevelNondirected ∷ 𝕊 → MixesF t f a → CParser t (f a) → CParser t a
    buildLevelNondirected :: 𝕊 -> MixesF t f a -> CParser t (f a) -> CParser t a
buildLevelNondirected 𝕊
msg MixesF t f a
mixes CParser t (f a)
nextLevel = do
      f a
x ← CParser t (f a)
nextLevel
      [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ 𝕊 -> CParser t a -> CParser t a
forall t a. Ord t => 𝕊 -> CParser t a -> CParser t a
cpErr (𝕊
msg 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
" infix") (CParser t a -> CParser t a) -> CParser t a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInfAfterOne f a
x MixesF t f a
mixes CParser t (f a)
nextLevel
        , a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> a
forall a. f a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract f a
x
        ]
    buildLevelDirected ∷ 𝕊 → MixesF t f a → CParser t (f a) → CParser t a
    buildLevelDirected :: 𝕊 -> MixesF t f a -> CParser t (f a) -> CParser t a
buildLevelDirected 𝕊
msg MixesF t f a
mixes CParser t (f a)
nextLevel = [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ do
          f a
x ← CParser t (f a)
nextLevel
          [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
            [ 𝕊 -> CParser t a -> CParser t a
forall t a. Ord t => 𝕊 -> CParser t a -> CParser t a
cpErr (𝕊
msg 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
" infixl") (CParser t a -> CParser t a) -> CParser t a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInflAfterOne f a
x MixesF t f a
mixes CParser t (f a)
nextLevel
            , 𝕊 -> CParser t a -> CParser t a
forall t a. Ord t => 𝕊 -> CParser t a -> CParser t a
cpErr (𝕊
msg 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
" infixr") (CParser t a -> CParser t a) -> CParser t a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInfrAfterOne f a
x MixesF t f a
mixes CParser t (f a)
nextLevel
            , a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> a
forall a. f a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract f a
x
            ]
      , 𝕊 -> CParser t a -> CParser t a
forall t a. Ord t => 𝕊 -> CParser t a -> CParser t a
cpErr (𝕊
msg 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
" infixr") (CParser t a -> CParser t a) -> CParser t a -> CParser t a
forall a b. (a -> b) -> a -> b
$ MixesF t f a -> CParser t (f a) -> CParser t a
levelInfrNotAfterOne MixesF t f a
mixes CParser t (f a)
nextLevel
      ]
    levelInfAfterOne ∷ f a → MixesF t f a → CParser t (f a) → CParser t a
    levelInfAfterOne :: f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInfAfterOne f a
x₁ MixesF t f a
mixes CParser t (f a)
nextLevel = do
      f a -> f a -> a
f ← MixesF t f a -> CParser t (f a -> f a -> a)
forall t (f :: * -> *) a.
MixesF t f a -> CParser t (f a -> f a -> a)
mixesFInfix MixesF t f a
mixes
      f a
x₂ ← CParser t (f a)
nextLevel
      a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> f a -> a
f f a
x₁ f a
x₂
    levelInflAfterOne ∷ f a → MixesF t f a → CParser t (f a) → CParser t a
    levelInflAfterOne :: f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInflAfterOne f a
x₁ MixesF t f a
mixes CParser t (f a)
nextLevel = do
      f a
x₁' ← CParser t a -> CParser t (f a)
cxt (CParser t a -> CParser t (f a)) -> CParser t a -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ do f a -> f a -> a
f ← MixesF t f a -> CParser t (f a -> f a -> a)
forall t (f :: * -> *) a.
MixesF t f a -> CParser t (f a -> f a -> a)
mixesFInfixL MixesF t f a
mixes
             f a
x₂ ← CParser t (f a)
nextLevel
             a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> f a -> a
f f a
x₁ f a
x₂
        , do f a -> a
f ← MixesF t f a -> CParser t (f a -> a)
forall t (f :: * -> *) a. MixesF t f a -> CParser t (f a -> a)
mixesFPostfix MixesF t f a
mixes
             a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> a
f f a
x₁
        ]
      [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInflAfterOne f a
x₁' MixesF t f a
mixes CParser t (f a)
nextLevel
        , a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> a
forall a. f a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract f a
x₁'
        ]
    levelInfrAfterOne ∷ f a → MixesF t f a → CParser t (f a) → CParser t a
    levelInfrAfterOne :: f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInfrAfterOne f a
x₁ MixesF t f a
mixes CParser t (f a)
nextLevel = do
      f a -> f a -> a
f ← MixesF t f a -> CParser t (f a -> f a -> a)
forall t (f :: * -> *) a.
MixesF t f a -> CParser t (f a -> f a -> a)
mixesFInfixR MixesF t f a
mixes
      f a
x₂ ← CParser t (f a) -> CParser t (f a)
bracket (CParser t (f a) -> CParser t (f a))
-> CParser t (f a) -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ CParser t a -> CParser t (f a)
cxt (CParser t a -> CParser t (f a)) -> CParser t a -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ MixesF t f a -> CParser t (f a) -> CParser t a
levelInfr MixesF t f a
mixes CParser t (f a)
nextLevel
      a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> f a -> a
f f a
x₁ f a
x₂
    levelInfr ∷ MixesF t f a → CParser t (f a) → CParser t a
    levelInfr :: MixesF t f a -> CParser t (f a) -> CParser t a
levelInfr MixesF t f a
mixes CParser t (f a)
nextLevel = [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ do f a
x₁ ← CParser t (f a)
nextLevel
           [CParser t a] -> CParser t a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
             [ f a -> MixesF t f a -> CParser t (f a) -> CParser t a
levelInfrAfterOne f a
x₁ MixesF t f a
mixes CParser t (f a)
nextLevel
             , a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> a
forall a. f a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract f a
x₁
             ]
      , MixesF t f a -> CParser t (f a) -> CParser t a
levelInfrNotAfterOne MixesF t f a
mixes CParser t (f a)
nextLevel
      ]
    levelInfrNotAfterOne ∷ MixesF t f a → CParser t (f a) → CParser t a
    levelInfrNotAfterOne :: MixesF t f a -> CParser t (f a) -> CParser t a
levelInfrNotAfterOne MixesF t f a
mixes CParser t (f a)
nextLevel = do
      f a -> a
f ← MixesF t f a -> CParser t (f a -> a)
forall t (f :: * -> *) a. MixesF t f a -> CParser t (f a -> a)
mixesFPrefix MixesF t f a
mixes
      f a
x ← CParser t (f a) -> CParser t (f a)
bracket (CParser t (f a) -> CParser t (f a))
-> CParser t (f a) -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ CParser t a -> CParser t (f a)
cxt (CParser t a -> CParser t (f a)) -> CParser t a -> CParser t (f a)
forall a b. (a -> b) -> a -> b
$ MixesF t f a -> CParser t (f a) -> CParser t a
levelInfr MixesF t f a
mixes CParser t (f a)
nextLevel
      a -> CParser t a
forall a. a -> CParser t a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> CParser t a) -> a -> CParser t a
forall a b. (a -> b) -> a -> b
$ f a -> a
f f a
x

fmixfixWithContext ∷ ∀ t a. (Ord t) ⇒ 𝕊 → MixfixF t (𝐴 SrcCxt) a → CParser t (𝐴 SrcCxt a)
fmixfixWithContext :: forall t a.
Ord t =>
𝕊 -> MixfixF t (𝐴 SrcCxt) a -> CParser t (𝐴 SrcCxt a)
fmixfixWithContext 𝕊
s = (CParser t (𝐴 SrcCxt a) -> CParser t (𝐴 SrcCxt a))
-> (CParser t (𝐴 SrcCxt a) -> CParser t (𝐴 SrcCxt a))
-> (CParser t a -> CParser t (𝐴 SrcCxt a))
-> MixfixF t (𝐴 SrcCxt) a
-> CParser t (𝐴 SrcCxt a)
forall t (f :: * -> *) a.
(Ord t, Comonad f) =>
(CParser t (f a) -> CParser t (f a))
-> (CParser t (f a) -> CParser t (f a))
-> (CParser t a -> CParser t (f a))
-> MixfixF t f a
-> CParser t (f a)
fmixfix (𝕊 -> CParser t (𝐴 SrcCxt a) -> CParser t (𝐴 SrcCxt a)
forall t a. Ord t => 𝕊 -> CParser t a -> CParser t a
cpNewContext 𝕊
s) CParser t (𝐴 SrcCxt a) -> CParser t (𝐴 SrcCxt a)
forall t a. Ord t => CParser t a -> CParser t a
cpNewExpressionContext CParser t a -> CParser t (𝐴 SrcCxt a)
forall t a. Ord t => CParser t a -> CParser t (𝐴 SrcCxt a)
cpWithContextRendered

---------------
-- Non-fancy --
---------------

data Mixes t a = Mixes
  { forall t a. Mixes t a -> CParser t (a -> a)
mixesPrefix  ∷ CParser t (a → a)
  , forall t a. Mixes t a -> CParser t (a -> a)
mixesPostfix ∷ CParser t (a → a)
  , forall t a. Mixes t a -> CParser t (a -> a -> a)
mixesInfix  ∷ CParser t (a → a → a)
  , forall t a. Mixes t a -> CParser t (a -> a -> a)
mixesInfixL ∷ CParser t (a → a → a)
  , forall t a. Mixes t a -> CParser t (a -> a -> a)
mixesInfixR ∷ CParser t (a → a → a)
  }

instance Null (Mixes t a) where null :: Mixes t a
null = CParser t (a -> a)
-> CParser t (a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> Mixes t a
forall t a.
CParser t (a -> a)
-> CParser t (a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> Mixes t a
Mixes CParser t (a -> a)
forall a. Null a => a
null CParser t (a -> a)
forall a. Null a => a
null CParser t (a -> a -> a)
forall a. Null a => a
null CParser t (a -> a -> a)
forall a. Null a => a
null CParser t (a -> a -> a)
forall a. Null a => a
null
instance (Ord t) ⇒ Append (Mixes t a) where 
  Mixes CParser t (a -> a)
pre₁ CParser t (a -> a)
post₁ CParser t (a -> a -> a)
inf₁ CParser t (a -> a -> a)
infl₁ CParser t (a -> a -> a)
infr₁ ⧺ :: Mixes t a -> Mixes t a -> Mixes t a
⧺ Mixes CParser t (a -> a)
pre₂ CParser t (a -> a)
post₂ CParser t (a -> a -> a)
inf₂ CParser t (a -> a -> a)
infl₂ CParser t (a -> a -> a)
infr₂ = 
    CParser t (a -> a)
-> CParser t (a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> Mixes t a
forall t a.
CParser t (a -> a)
-> CParser t (a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> CParser t (a -> a -> a)
-> Mixes t a
Mixes (CParser t (a -> a)
pre₁ CParser t (a -> a) -> CParser t (a -> a) -> CParser t (a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (a -> a)
pre₂) (CParser t (a -> a)
post₁ CParser t (a -> a) -> CParser t (a -> a) -> CParser t (a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (a -> a)
post₂) (CParser t (a -> a -> a)
inf₁ CParser t (a -> a -> a)
-> CParser t (a -> a -> a) -> CParser t (a -> a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (a -> a -> a)
inf₂) (CParser t (a -> a -> a)
infl₁ CParser t (a -> a -> a)
-> CParser t (a -> a -> a) -> CParser t (a -> a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (a -> a -> a)
infl₂) (CParser t (a -> a -> a)
infr₁ CParser t (a -> a -> a)
-> CParser t (a -> a -> a) -> CParser t (a -> a -> a)
forall a. Append a => a -> a -> a
⧺ CParser t (a -> a -> a)
infr₂)
instance (Ord t) ⇒ Monoid (Mixes t a)

data Mixfix t a = Mixfix 
  { forall t a. Mixfix t a -> CParser t a
mixfixTerminals ∷ CParser t a
  , forall t a. Mixfix t a -> ℕ64 ⇰ Mixes t a
mixfixLevels ∷ ℕ64 ⇰ Mixes t a
  }

instance Null (Mixfix t a) where null :: Mixfix t a
null = CParser t a -> (ℕ64 ⇰ Mixes t a) -> Mixfix t a
forall t a. CParser t a -> (ℕ64 ⇰ Mixes t a) -> Mixfix t a
Mixfix CParser t a
forall a. Null a => a
null ℕ64 ⇰ Mixes t a
forall a. Bot a => a
bot
instance (Ord t) ⇒ Append (Mixfix t a) where Mixfix CParser t a
ts₁ ℕ64 ⇰ Mixes t a
ls₁ ⧺ :: Mixfix t a -> Mixfix t a -> Mixfix t a
⧺ Mixfix CParser t a
ts₂ ℕ64 ⇰ Mixes t a
ls₂ = CParser t a -> (ℕ64 ⇰ Mixes t a) -> Mixfix t a
forall t a. CParser t a -> (ℕ64 ⇰ Mixes t a) -> Mixfix t a
Mixfix (CParser t a
ts₁ CParser t a -> CParser t a -> CParser t a
forall a. Append a => a -> a -> a
⧺ CParser t a
ts₂) (ℕ64 ⇰ Mixes t a
ls₁ (ℕ64 ⇰ Mixes t a) -> (ℕ64 ⇰ Mixes t a) -> ℕ64 ⇰ Mixes t a
forall a. Append a => a -> a -> a
⧺ ℕ64 ⇰ Mixes t a
ls₂)
instance (Ord t) ⇒ Monoid (Mixfix t a)

mixPrefix ∷ ℕ64 → CParser t (a → a) → Mixfix t a
mixPrefix :: forall t a. ℕ64 -> CParser t (a -> a) -> Mixfix t a
mixPrefix ℕ64
l CParser t (a -> a)
p = Mixfix t a
forall a. Null a => a
null { mixfixLevels = dict [ l ↦♭ null {mixesPrefix = p} ] }

mixPostfix ∷ ℕ64 → CParser t (a → a) → Mixfix t a
mixPostfix :: forall t a. ℕ64 -> CParser t (a -> a) -> Mixfix t a
mixPostfix ℕ64
l CParser t (a -> a)
p = Mixfix t a
forall a. Null a => a
null { mixfixLevels = dict [ l ↦♭ null {mixesPostfix = p} ] }

mixInfix ∷ ℕ64 → CParser t (a → a → a) → Mixfix t a
mixInfix :: forall t a. ℕ64 -> CParser t (a -> a -> a) -> Mixfix t a
mixInfix ℕ64
l CParser t (a -> a -> a)
p = Mixfix t a
forall a. Null a => a
null { mixfixLevels = dict [ l ↦♭ null {mixesInfix = p} ] }

mixInfixL ∷ ℕ64 → CParser t (a → a → a) → Mixfix t a
mixInfixL :: forall t a. ℕ64 -> CParser t (a -> a -> a) -> Mixfix t a
mixInfixL ℕ64
l CParser t (a -> a -> a)
p = Mixfix t a
forall a. Null a => a
null { mixfixLevels = dict [ l ↦♭ null {mixesInfixL = p} ] }

mixInfixR ∷ ℕ64 → CParser t (a → a → a) → Mixfix t a
mixInfixR :: forall t a. ℕ64 -> CParser t (a -> a -> a) -> Mixfix t a
mixInfixR ℕ64
l CParser t (a -> a -> a)
p = Mixfix t a
forall a. Null a => a
null { mixfixLevels = dict [ l ↦♭ null {mixesInfixR = p} ] }

mixTerminal ∷ CParser t a → Mixfix t a
mixTerminal :: forall t a. CParser t a -> Mixfix t a
mixTerminal CParser t a
p = Mixfix t a
forall a. Null a => a
null { mixfixTerminals = p}

mixesPure ∷ (Ord t) ⇒ Mixes t a → MixesF t ID a
mixesPure :: forall t a. Ord t => Mixes t a -> MixesF t ID a
mixesPure (Mixes CParser t (a -> a)
pre CParser t (a -> a)
post CParser t (a -> a -> a)
inf CParser t (a -> a -> a)
infl CParser t (a -> a -> a)
infr) =
  CParser t (ID a -> a)
-> CParser t (ID a -> a)
-> CParser t (ID a -> ID a -> a)
-> CParser t (ID a -> ID a -> a)
-> CParser t (ID a -> ID a -> a)
-> MixesF t ID a
forall t (f :: * -> *) a.
CParser t (f a -> a)
-> CParser t (f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> CParser t (f a -> f a -> a)
-> MixesF t f a
MixesF
  (((a -> a) -> ID a -> a)
-> CParser t (a -> a) -> CParser t (ID a -> a)
forall a b. (a -> b) -> CParser t a -> CParser t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a) -> ID a -> a
forall (w :: * -> *) a b. Extract w => (a -> b) -> w a -> b
kextract CParser t (a -> a)
pre)
  (((a -> a) -> ID a -> a)
-> CParser t (a -> a) -> CParser t (ID a -> a)
forall a b. (a -> b) -> CParser t a -> CParser t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a) -> ID a -> a
forall (w :: * -> *) a b. Extract w => (a -> b) -> w a -> b
kextract CParser t (a -> a)
post)
  (((a -> a -> a) -> ID a -> ID a -> a)
-> CParser t (a -> a -> a) -> CParser t (ID a -> ID a -> a)
forall a b. (a -> b) -> CParser t a -> CParser t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a -> a) -> ID a -> ID a -> a
forall (w :: * -> *) a b c.
Extract w =>
(a -> b -> c) -> w a -> w b -> c
kextract2 CParser t (a -> a -> a)
inf)
  (((a -> a -> a) -> ID a -> ID a -> a)
-> CParser t (a -> a -> a) -> CParser t (ID a -> ID a -> a)
forall a b. (a -> b) -> CParser t a -> CParser t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a -> a) -> ID a -> ID a -> a
forall (w :: * -> *) a b c.
Extract w =>
(a -> b -> c) -> w a -> w b -> c
kextract2 CParser t (a -> a -> a)
infl)
  (((a -> a -> a) -> ID a -> ID a -> a)
-> CParser t (a -> a -> a) -> CParser t (ID a -> ID a -> a)
forall a b. (a -> b) -> CParser t a -> CParser t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a -> a) -> ID a -> ID a -> a
forall (w :: * -> *) a b c.
Extract w =>
(a -> b -> c) -> w a -> w b -> c
kextract2 CParser t (a -> a -> a)
infr)

mixfixPure ∷ (Ord t) ⇒ Mixfix t a → MixfixF t ID a
mixfixPure :: forall t a. Ord t => Mixfix t a -> MixfixF t ID a
mixfixPure (Mixfix CParser t a
terminals ℕ64 ⇰ Mixes t a
levels) = CParser t a -> (ℕ64 ⇰ MixesF t ID a) -> MixfixF t ID a
forall t (f :: * -> *) a.
CParser t a -> (ℕ64 ⇰ MixesF t f a) -> MixfixF t f a
MixfixF CParser t a
terminals ((ℕ64 ⇰ MixesF t ID a) -> MixfixF t ID a)
-> (ℕ64 ⇰ MixesF t ID a) -> MixfixF t ID a
forall a b. (a -> b) -> a -> b
$ (Mixes t a -> MixesF t ID a)
-> (ℕ64 ⇰ Mixes t a) -> ℕ64 ⇰ MixesF t ID a
forall a b. (a -> b) -> (ℕ64 ⇰ a) -> ℕ64 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Mixes t a -> MixesF t ID a
forall t a. Ord t => Mixes t a -> MixesF t ID a
mixesPure ℕ64 ⇰ Mixes t a
levels

mixfix ∷ (Ord t) ⇒ Mixfix t a → CParser t a
mixfix :: forall t a. Ord t => Mixfix t a -> CParser t a
mixfix Mixfix t a
mix = ID a -> a
forall a. ID a -> a
unID (ID a -> a) -> CParser t (ID a) -> CParser t a
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (CParser t (ID a) -> CParser t (ID a))
-> (CParser t (ID a) -> CParser t (ID a))
-> (CParser t a -> CParser t (ID a))
-> MixfixF t ID a
-> CParser t (ID a)
forall t (f :: * -> *) a.
(Ord t, Comonad f) =>
(CParser t (f a) -> CParser t (f a))
-> (CParser t (f a) -> CParser t (f a))
-> (CParser t a -> CParser t (f a))
-> MixfixF t f a
-> CParser t (f a)
fmixfix CParser t (ID a) -> CParser t (ID a)
forall a. a -> a
id CParser t (ID a) -> CParser t (ID a)
forall a. a -> a
id ((a -> ID a) -> CParser t a -> CParser t (ID a)
forall a b. (a -> b) -> CParser t a -> CParser t b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> ID a
forall a. a -> ID a
ID) (Mixfix t a -> MixfixF t ID a
forall t a. Ord t => Mixfix t a -> MixfixF t ID a
mixfixPure Mixfix t a
mix) 

mixfixWithContext ∷ (Ord t) ⇒ 𝕊 → Mixfix t a → CParser t (𝐴 SrcCxt a)
mixfixWithContext :: forall t a. Ord t => 𝕊 -> Mixfix t a -> CParser t (𝐴 SrcCxt a)
mixfixWithContext 𝕊
s = 𝕊 -> CParser t (𝐴 SrcCxt a) -> CParser t (𝐴 SrcCxt a)
forall t a. Ord t => 𝕊 -> CParser t a -> CParser t a
cpNewContext 𝕊
s (CParser t (𝐴 SrcCxt a) -> CParser t (𝐴 SrcCxt a))
-> (CParser t a -> CParser t (𝐴 SrcCxt a))
-> CParser t a
-> CParser t (𝐴 SrcCxt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ CParser t a -> CParser t (𝐴 SrcCxt a)
forall t a. Ord t => CParser t a -> CParser t (𝐴 SrcCxt a)
cpWithContextRendered (CParser t a -> CParser t (𝐴 SrcCxt a))
-> (Mixfix t a -> CParser t a)
-> Mixfix t a
-> CParser t (𝐴 SrcCxt a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Mixfix t a -> CParser t a
forall t a. Ord t => Mixfix t a -> CParser t a
mixfix