module StructurallyRecursiveDescentParsing.Grammar where
open import Data.Bool
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Coinduction
open import Level
open import StructurallyRecursiveDescentParsing.Index
import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified hiding (Parser; module Parser; ⟦_⟧)
infixl 10 _!>>=_ _?>>=_
infixl 5 _∣_
data Parser (NT : NonTerminalType) (Tok : Set) : NonTerminalType where
return : ∀ {R} (x : R) → Parser NT Tok (true ◇ ε) R
fail : ∀ {R} → Parser NT Tok (false ◇ ε) R
token : Parser NT Tok (false ◇ ε) Tok
_∣_ : ∀ {e₁ e₂ c₁ c₂ R}
(p₁ : Parser NT Tok (e₁ ◇ c₁ ) R)
(p₂ : Parser NT Tok ( e₂ ◇ c₂) R) →
Parser NT Tok (e₁ ∨ e₂ ◇ c₁ ∪ c₂) R
_?>>=_ : ∀ {e₂ c₁ c₂ R₁ R₂}
(p₁ : Parser NT Tok (true ◇ c₁ ) R₁)
(p₂ : R₁ → Parser NT Tok (e₂ ◇ c₂) R₂) →
Parser NT Tok (e₂ ◇ c₁ ∪ c₂) R₂
_!>>=_ : ∀ {c₁ R₁ R₂} {i₂ : R₁ → Index}
(p₁ : Parser NT Tok (false ◇ c₁) R₁)
(p₂ : (x : R₁) → ∞ (Parser NT Tok (i₂ x) R₂)) →
Parser NT Tok (false ◇ c₁) R₂
! : ∀ {e c R} (nt : NT (e ◇ c) R) → Parser NT Tok (e ◇ c ∪ ε) R
Grammar : NonTerminalType → Set → Set1
Grammar NT Tok = ∀ {i R} → NT i R → Parser NT Tok i R
EmptyNT : NonTerminalType
EmptyNT _ _ = Lift ⊥
emptyGrammar : ∀ {Tok} → Grammar EmptyNT Tok
emptyGrammar (lift ())
⟦_⟧ : ∀ {Tok NT e c R} →
Parser NT Tok (e ◇ c) R → Grammar NT Tok →
Simplified.Parser Tok e R
⟦ return x ⟧ g = return x
⟦ fail ⟧ g = fail
⟦ token ⟧ g = token
⟦ p₁ ∣ p₂ ⟧ g = ⟦ p₁ ⟧ g ∣ ⟦ p₂ ⟧ g
⟦ p₁ ?>>= p₂ ⟧ g = ⟦ p₁ ⟧ g ?>>= λ x → ⟦ p₂ x ⟧ g
⟦ p₁ !>>= p₂ ⟧ g = ⟦ p₁ ⟧ g !>>= λ x → ♯ ⟦ ♭ (p₂ x) ⟧ g
⟦ ! nt ⟧ g = ⟦ g nt ⟧ g
private
only-plain : Simplified.Parser Bool false Bool
only-plain = return true ?>>= λ x →
if x then token else token ∣ token
mapNT : ∀ {NT₁ NT₂ Tok i R} →
(∀ {i R} → NT₁ i R → NT₂ i R) →
Parser NT₁ Tok i R → Parser NT₂ Tok i R
mapNT f (return x) = return x
mapNT f fail = fail
mapNT f token = token
mapNT f (p₁ ∣ p₂) = mapNT f p₁ ∣ mapNT f p₂
mapNT f (p₁ ?>>= p₂) = mapNT f p₁ ?>>= λ x → mapNT f (p₂ x)
mapNT f (p₁ !>>= p₂) = mapNT f p₁ !>>= λ x → ♯ mapNT f (♭ (p₂ x))
mapNT f (! nt) = ! (f nt)