open import Data.List
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product

module Earley where

data Terminality : Set where
  T : Terminality
  NT : Terminality

module Grammar
  (Symbol : (Terminality → Set))
  where

  Terminal = Symbol

  infixr 5 _~∷_
  infixr 5 _|∷_

  -- infix 5 _~_
  -- infix 5 _ǁ_

  infix 4 _∷=_

  infix 5 _∷⟨×⟩_
  infix 6 _∷|+|_

  -- a parse forest is a grammar where each nonterminal is a forest.

  data SymbolicString : Set where
    ε : SymbolicString
    _~∷_ : {t : Terminality} (a : Symbol t) → (b : SymbolicString) → SymbolicString
    _|∷_ : {t : Terminality} (a : Symbol t) → (b : SymbolicString) → SymbolicString

  -- _~_ : (x : SymbolicString) → (y : SymbolicString) → SymbolicString
  -- _|_ : (x : SymbolicString) → (y : SymbolicString) → SymbolicString

  data Rule : Set where
    _∷=_ : (α : Symbol NT) → (β : SymbolicString) → Rule

  Grammar = List Rule

  data ParseTree : Set where
    ∅ : ParseTree
    λ' : ParseTree
    Leaf : Symbol T → ParseTree
    _⟨×⟩_ : (left right : ParseTree) → ParseTree

  data Level : Set where
    sum-level : Level
    product-level : Level

  data ParseForest : Level → Set

  data ParseForest where
    ∅ : ParseForest sum-level
    λ' : ParseForest product-level
    Leaf : {l : Level} → (Symbol T) → ParseForest l
    _∷⟨×⟩_ : (x : ParseForest product-level) → (xs : ParseForest sum-level) → ParseForest product-level
    _∷|+|_ : (x : ParseForest sum-level) → (xs : ParseForest product-level) → ParseForest sum-level

  flip-level : Level → Level
  flip-level sum-level = product-level
  flip-level product-level = sum-level

  -- flip-level : {l : Level} (forest : ParseForest l) → ParseForest (flip l)
  -- flip-level {sum-level} s = λ' ∷⟨×⟩ s
  -- flip-level {product-level} p = ∅ ∷|+| p

  -- Leaf' : Symbol T → ParseForest product-level
  -- Leaf' l = flip-level (Leaf l)

data MySymbol : Terminality → Set

data MySymbol where
  MyT : ℕ → MySymbol T
  MyNT : ℕ → MySymbol NT

open Grammar MySymbol

The = MyT 0
A = MyT 1
Man = MyT 2
Dog = MyT 3
Bites = MyT 4
Pets = MyT 5

sentence = MyNT 0
subject = MyNT 1
predicate = MyNT 2
article = MyNT 3
noun = MyNT 4
verb = MyNT 5
direct_object = MyNT 6

forest = (λ' ∷⟨×⟩ Leaf The) ∷⟨×⟩ Leaf Man

grammar = (sentence ∷= subject ~∷ predicate ~∷ ε) ∷
          (subject ∷= article ~∷ noun ~∷ ε) ∷
          (predicate ∷= verb ~∷ direct_object ~∷ ε) ∷
          (direct_object ∷= article ~∷ noun ~∷ ε) ∷
          (article ∷= The |∷ A ~∷ ε) ∷
          (noun ∷= Man |∷ Dog ~∷ ε) ∷
          (verb ∷= Bites |∷ Pets ~∷ ε) ∷
          []

  -- rule ∷=