Grammar.agda

module Grammar where
  open import Category.Applicative
  open import Data.Char using (Char)
  open import Data.List using (List)
  open import Data.List.NonEmpty using (List⁺; map; foldl₁; fromList)
  open import Data.Maybe using (from-just)
  open import Data.Nat using (ℕ; _+_; _*_)
  open import Data.String using (String; toList)
  open import Data.Unit
  open import Function
  open import Level

  private
    variable
      ℓ : Level
      P : Set ℓ → Set ℓ

      i : Level
      I : Set i

  record ProductionRule (P : Set ℓ → Set ℓ) : Set (suc ℓ) where
    field
      alternative : RawAlternative P
      end : P (Lift _ ⊤)
    open RawAlternative alternative public
  open ProductionRule {{...}} public

  record RecProductionRule (P : Set ℓ → Set ℓ) {i} {I : Set i} (R : I → Set ℓ) : Set (suc ℓ ⊔ i) where
    field
      {{productionRule}} : ProductionRule P
      ⟨_⟩ : (ix : I) → P (R ix)
  open RecProductionRule {{...}} public

  record LoopProductionRule (P : Set ℓ → Set ℓ) {i} {I : Set i} (R : I → Set ℓ) : Set (suc ℓ ⊔ i) where
    field
      {{recProductionRule}} : RecProductionRule P R
      ⟨_⟩* : (ix : I) → P (List (R ix))
      ⟨_⟩+ : (ix : I) → P (List⁺ (R ix))
  open LoopProductionRule {{...}} public

  record TokenProductionRule (P : Set ℓ → Set ℓ) (T : Set ℓ) : Set (suc ℓ) where
    field
      token : T → P T
  open TokenProductionRule {{...}} public

  tokenRange : ∀ {T} → {{_ : ProductionRule P}} → {{_ : TokenProductionRule P T}} → List⁺ T → P T
  tokenRange = foldl₁ _∣_ ∘ map token

  PatternFunctor : ∀ ℓ → Set i → Set (suc ℓ ⊔ i)
  PatternFunctor ℓ I = (I → Set ℓ) → I → Set ℓ

  ExtendedContextFreeGrammar : ∀ {i} {I : Set i} → PatternFunctor ℓ I → Set ℓ → Set (suc ℓ ⊔ i)
  ExtendedContextFreeGrammar {I = I} pf T = ∀ {P R}
    → {{_ : LoopProductionRule P R}}
    → {{_ : TokenProductionRule P T}}
    → (ix : I) → P (pf R ix)

  Processor : ∀ {i} {I : Set i} → PatternFunctor ℓ I → (I → Set ℓ) → Set (ℓ ⊔ i)
  Processor {I = I} pf R = {ix : I} → pf R ix → R ix

  module Example where

    data ϕ : Set where
      Line Expr Term Factor Digit : ϕ

    data Calc (R : ϕ → Set ℓ) : ϕ → Set ℓ where
      line    : R Expr            → Calc R Line
      term    : R Term            → Calc R Expr
      sum     : R Expr → R Term   → Calc R Expr
      factor  : R Factor          → Calc R Term
      product : R Term → R Factor → Calc R Term
      paren   : R Expr            → Calc R Factor
      number  : List⁺ (R Digit)   → Calc R Factor
      digit   : Char              → Calc R Digit

    allDigits : List⁺ Char
    allDigits = from-just (fromList (toList "0123456789"))

    grammar : ExtendedContextFreeGrammar Calc Char
    grammar Line   = line    <$> ⟨ Expr ⟩ <⊛ end
    grammar Expr   = term    <$> ⟨ Term ⟩
                   ∣ sum     <$> ⟨ Expr ⟩ <⊛ token '+' ⊛ ⟨ Term ⟩
    grammar Term   = factor  <$> ⟨ Factor ⟩
                   ∣ product <$> ⟨ Term ⟩ <⊛ token '*' ⊛ ⟨ Factor ⟩
    grammar Factor = paren   <$  token '(' ⊛ ⟨ Expr ⟩ <⊛ token ')'
                   ∣ number  <$> ⟨ Digit ⟩+
    grammar Digit  = digit   <$> tokenRange allDigits

    Eval : ϕ → Set
    Eval Line   = ℕ
    Eval Expr   = ℕ
    Eval Term   = ℕ
    Eval Factor = ℕ
    Eval Digit  = Char

    data ⟦⟧ : ϕ → Set where
      ⟦_⟧ : {ix : ϕ} → Eval ix → ⟦⟧ ix

    calc : Processor Calc ⟦⟧
    calc (line ⟦ x ⟧)          = ⟦ x ⟧
    calc (term ⟦ x ⟧)          = ⟦ x ⟧
    calc (sum ⟦ a ⟧ ⟦ b ⟧)     = ⟦ a + b ⟧
    calc (factor ⟦ x ⟧)        = ⟦ x ⟧
    calc (product ⟦ a ⟧ ⟦ b ⟧) = ⟦ a * b ⟧
    calc (paren ⟦ x ⟧)         = ⟦ x ⟧
    calc (number x)            = {!!}
    calc (digit x)             = {!!}