module TotalParserCombinators.Recogniser where
open import Codata.Musical.Notation
open import Data.Bool
open import Data.List as List
import Data.List.Effectful
open import Data.Maybe
open import Data.Unit
open import Effect.Monad
open import Level
open RawMonadPlus {f = zero} Data.List.Effectful.monadPlus
using () renaming (_⊛_ to _⊛′_)
open import TotalParserCombinators.Parser as Parser
using (Parser; flatten); open Parser.Parser
import TotalParserCombinators.Lib as Lib
infixl 4 _·′_
_·′_ : (mb₁ mb₂ : Maybe (List ⊤)) → List ⊤
mb₁ ·′ nothing = []
mb₁ ·′ just b₂ = List.map _ (flatten mb₁) ⊛′ b₂
infixl 50 _·_
infixl 5 _∣_
mutual
data P (Tok : Set) : List ⊤ → Set₁ where
lift : ∀ {R n} (p : Parser Tok R n) → P Tok (List.map _ n)
_∣_ : ∀ {n₁ n₂}
(p₁ : P Tok n₁) (p₂ : P Tok n₂) → P Tok (n₁ ++ n₂)
_·_ : ∀ {n₁ n₂}
(p₁ : ∞⟨ n₂ ⟩P Tok (flatten n₁))
(p₂ : ∞⟨ n₁ ⟩P Tok (flatten n₂)) →
P Tok (n₁ ·′ n₂)
∞⟨_⟩P : Maybe (List ⊤) → Set → List ⊤ → Set₁
∞⟨ nothing ⟩P Tok n = ∞ (P Tok n)
∞⟨ just _ ⟩P Tok n = P Tok n
forced? : ∀ {Tok m n} → ∞⟨ m ⟩P Tok n → Maybe (List ⊤)
forced? {m = m} _ = m
⟦_⟧ : ∀ {Tok n} (p : P Tok n) → Parser Tok ⊤ n
⟦ lift p ⟧ = _ <$> p
⟦ p₁ ∣ p₂ ⟧ = ⟦ p₁ ⟧ ∣ ⟦ p₂ ⟧
⟦ p₁ · p₂ ⟧ with forced? p₁ | forced? p₂
... | just xs | nothing = _ <$> ⟦ p₁ ⟧ ⊛ ♯ ⟦ ♭ p₂ ⟧
... | just xs | just ys = _ <$> ⟦ p₁ ⟧ ⊛ ⟦ p₂ ⟧
... | nothing | nothing = ♯ (_ <$> ⟦ ♭ p₁ ⟧) ⊛ ♯ ⟦ ♭ p₂ ⟧
... | nothing | just ys = ♯ (_ <$> ⟦ ♭ p₁ ⟧) ⊛ ⟦ p₂ ⟧