module StructurallyRecursiveDescentParsing.Grammar where
open import Data.Bool
open import Data.Empty1
open import Data.Product1 renaming (proj₀₁₂ to proj₂)
open import Relation.Binary.PropositionalEquality
open import Coinduction
open import StructurallyRecursiveDescentParsing.Index
import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified hiding (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 _ _ = ⊥₁
emptyGrammar : ∀ {Tok} → Grammar EmptyNT Tok
emptyGrammar ()
⟦_⟧ : ∀ {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)