parsergen4.agda

module parsergen4 where

-- for troubleshooting, not a complete parser generator/parsing engine.

open import Agda.Builtin.Equality
open import Relation.Nullary using (Dec)
open import Data.Nat
open import Data.Fin hiding (_<_)
open import Data.Fin.Properties using (suc-injective)
open import Data.Vec hiding (_>>=_)
open import Data.Maybe
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Data.List
open import Relation.Binary.PropositionalEquality using (refl; cong; subst; sym)
open import Data.Nat.Properties using (≤-refl; +-identityˡ; +-identityʳ; +-suc; 1+n≢0)
open import Data.Nat.Induction using (<-wellFounded)
open import Induction.WellFounded
open import Function using (_on_; id; _∘_)
open import Data.Sum
open import Relation.Unary using (Decidable)

data Singleton {a} {A : Set a} (x : A) : Set a where
  _with≡_ : (y : A) → x ≡ y → Singleton x

inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
inspect x = x with≡ refl

record Grammar : Set₁ where
  constructor grammar
  field symbol : Set
        symbol-eq : (x y : symbol) → Dec (x ≡ y)
        start : symbol
        reductions : ℕ
        lhs : Fin reductions → symbol
        cel : Fin reductions → ℕ
        rhs : (i : Fin reductions) → Vec symbol (cel i)
        nhs : (i : Fin reductions) → cel i ≡ zero → ⊥
open Grammar

variable
  g : Grammar

record Item (g : Grammar) : Set where
  constructor item
  field i : Fin (reductions g)
        x : Fin (suc (cel g i))

item-lemma : ∀{i j : Fin (reductions g)}{x}{y} → item {g} i x ≡ item j y → i ≡ j
item-lemma refl = refl

item-lemma2 : ∀{i : Fin (reductions g)}{x y} → item {g} i x ≡ item i y → x ≡ y
item-lemma2 refl = refl

item-eq : (x y : Item g) → Dec (x ≡ y)
item-eq (item i x) (item j y) with i Data.Fin.≟ j
item-eq (item i x) (item i y) | Dec.yes refl with x Data.Fin.≟ y
item-eq (item i x) (item i x) | Dec.yes refl | Dec.yes refl = Dec.yes refl
item-eq (item i x) (item i y) | Dec.yes refl | Dec.no ¬p = Dec.no λ(a) → ¬p (item-lemma2 a)
item-eq (item i x) (item j y) | Dec.no ¬p = Dec.no λ(a) → ¬p (item-lemma a) 

first-item : Fin (reductions g) → Item g
first-item i = item i 0F

index : {n : ℕ}{a : Set} → Fin (suc n) → Vec a n → Maybe (a × Fin (suc n))
index 0F [] = nothing
index 0F (x ∷ _) = just (x , 1F)
index (suc i) (_ ∷ k) with index i k
... | just (s , j) = just (s , suc j)
... | nothing = nothing

step : Item g → Maybe (symbol g × Item g)
step {g} (item i x) with index x (rhs g i)
step {g} (item i x) | just (s , y) = just (s , item i y)
step {g} (item i x) | nothing = nothing

data Any {A : Set} (P : A → Set) : List A → Set where
  here  : ∀ {x : A} {xs : List A} → P x → Any P (x ∷ xs)
  there : ∀ {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)

infix 4 _∈_

_∈_ : ∀ {A : Set} (x : A) (xs : List A) → Set
x ∈ xs = Any (x ≡_) xs

each : Fin (reductions g) → List (Item g)
each i = Data.List.tabulate (item i)

tabulate-lemma : ∀ {A : Set}{n} (f : Fin n → A) → (x : Fin n)
  → f x ∈ Data.List.tabulate f
tabulate-lemma f 0F = here refl
tabulate-lemma f (suc x) = there (tabulate-lemma (f ∘ suc) x)

tabulate-lemma2 : ∀ {A : Set}{n m} (f : Fin (suc n) → A) → (g : Fin m → Fin n)
  → (∀{a b} → f a ≡ f b → a ≡ b)
  → f 0F ∈ Data.List.tabulate (f ∘ suc ∘ g) → ⊥
tabulate-lemma2 {m = suc n} f g f' (here x) = ⊥-elim (1+n≢0 (sym (cong toℕ (f' x))))
tabulate-lemma2 {m = suc n} f g f' (there tab) = tabulate-lemma2 f (g ∘ suc) (f') tab

tabulate-unique : ∀ {A : Set}{n} (f : Fin n → A) → (∀{a b} → f a ≡ f b → a ≡ b)
  → (k : Fin n)
  → (i : f k ∈ Data.List.tabulate f)
  → (j : f k ∈ Data.List.tabulate f)
  → i ≡ j
tabulate-unique f f' 0F (here refl) (here refl) = refl
tabulate-unique f f' 0F x (there j) = ⊥-elim (tabulate-lemma2 f id f' j)
tabulate-unique f f' 0F (there i) x = ⊥-elim (tabulate-lemma2 f id f' i)
tabulate-unique f f' (suc k) (here x) j = ⊥-elim (1+n≢0 (cong toℕ (f' x)))
tabulate-unique f f' (suc k) (there i) (here x) = ⊥-elim (1+n≢0 (cong toℕ (f' x)))
tabulate-unique f f' (suc k) (there i) (there j) = cong there
  (tabulate-unique (f ∘ suc) (suc-injective ∘ f') k i j)

each-complete : (i : Fin (reductions g)) → (x : Fin (suc (cel g i))) → (item {g} i x ∈ each i)
each-complete {g} i x = tabulate-lemma (item {g} i) x

all-items : (g : Grammar) → List (Item g)
all-items _ = Data.List.concat (Data.List.tabulate each)

list-lemma : ∀{a : Set}{x : a}{xs ys : List a} → x ∈ xs → x ∈ (xs Data.List.++ ys)
list-lemma (here x) = here x
list-lemma (there im) = there (list-lemma im)

list-lemma2 : ∀{a : Set}{x : a}{xs ys : List a} → x ∈ ys → x ∈ (xs Data.List.++ ys)
list-lemma2 {xs = []} pos = pos
list-lemma2 {xs = x ∷ xs} pos = there (list-lemma2 pos)

contain-to-index : {a : Set}{x : a}{xs : List a} → x ∈ xs → Fin (Data.List.length xs)
contain-to-index (here x) = 0F
contain-to-index (there pos) = suc (contain-to-index pos)

index-lookup : {a : Set}{xs : List a} → Fin (length xs) → a
index-lookup {xs = x ∷ xs} 0F = x
index-lookup {xs = x ∷ xs} (suc i) = index-lookup {xs = xs} i

all-ix-complete : ∀{m} → (f : Fin m → Fin (reductions g)) → (k : Fin m)
                → (x : Fin (suc (cel g (f k))))
                → item {g} (f k) x ∈ Data.List.concat (Data.List.tabulate (each ∘ f))
all-ix-complete f 0F x = list-lemma (each-complete (f 0F) x)
all-ix-complete f (suc k) x = list-lemma2 (all-ix-complete (f ∘ suc) k x)

all-items-complete : (g : Grammar) → (i : Item g) → (i ∈ all-items g)
all-items-complete g (item i x) = all-ix-complete id i x

size : (g : Grammar) → ℕ
size g = Data.List.length (all-items g)

item-to-i : Item g → Fin (size g)
item-to-i {g} ix = contain-to-index (all-items-complete g ix)

i-to-item : Fin (size g) → Item g
i-to-item {g} ix = index-lookup {xs = all-items g} ix

-- item-theorem1 : (i : Item g) → i-to-item (item-to-i i) ≡ i
-- item-theorem1 (item i x) = {!!}

-- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
infixl 5 _↑ˡ_
_↑ˡ_ : ∀ {m} → Fin m → ∀ n → Fin (m Data.Nat.+ n)
zero    ↑ˡ n = zero
(suc i) ↑ˡ n = suc (i ↑ˡ n)

-- injection on the right: n ↑ʳ "i" = "n + i" in Fin (n + m)
infixr 5 _↑ʳ_
_↑ʳ_ : ∀ {m} n → Fin m → Fin (n Data.Nat.+ m)
zero    ↑ʳ i = i
(suc n) ↑ʳ i = suc (n ↑ʳ i)

splitAt' : ∀ m {n} → Fin (m Data.Nat.+ n) → Fin m ⊎ Fin n
splitAt' zero    i       = inj₂ i
splitAt' (suc m) zero    = inj₁ zero
splitAt' (suc m) (suc i) = Data.Sum.map suc id (splitAt' m i)

remQuot : ∀ {n} k → Fin (n Data.Nat.* k) → Fin n × Fin k
remQuot {suc n} k i with splitAt' k i
... | inj₁ j = zero , j
... | inj₂ j = Data.Product.map₁ suc (remQuot {n} k j)

-- inverse of remQuot
combine : ∀ {n k} → Fin n → Fin k → Fin (n Data.Nat.* k)
combine {suc n} {k} zero    y = y ↑ˡ (n Data.Nat.* k)
combine {suc n} {k} (suc x) y = k ↑ʳ (combine x y)

opposite : ∀ {n} → Fin n → Fin n
opposite {suc n} zero    = fromℕ n
opposite {suc n} (suc i) = inject₁ (opposite i)


data FinSet (ub : ℕ) (k : Set) : Set where
  blank : FinSet ub k
  key : (n : Fin ub) → k
     → FinSet (toℕ n) k
     → FinSet (toℕ (opposite n)) k
     → FinSet ub k

to-list : ∀{a}{ub} → FinSet ub a → List a
to-list blank = []
to-list (key n x s t) = to-list s Data.List.++ (x Data.List.∷ to-list t)

ex1 : Fin 10
ex1 = opposite 3F

ex2 : FinSet 10 ⊤
ex2 = key 1F tt
  (key 0F tt blank blank)
  (key 6F tt (key 2F tt (key 0F tt blank blank) blank) (key 0F tt blank blank))

data Comparison (ub : ℕ) (m n : Fin ub) : Set where
  less : Fin (toℕ n) → Comparison ub m n
  more : Fin (toℕ (opposite n)) → Comparison ub m n
  exact : Comparison ub m n

compare-lemma : ∀{n} → n ≡ toℕ (fromℕ n)
compare-lemma {0F} = refl
compare-lemma {suc n} = cong suc compare-lemma

compare-lemma2 : ∀{m} (n : Fin m) → toℕ n ≡ toℕ (inject₁ n)
compare-lemma2 0F = refl
compare-lemma2 (suc n) = cong suc (compare-lemma2 n)

compare' : ∀{ub} → (m n : Fin ub) → Comparison ub m n
compare' {suc _} 0F 0F = exact
compare' {suc _} (suc m) 0F = more (subst Fin compare-lemma m)
compare' {suc _} 0F (suc n) = less 0F
compare' {suc _} (suc m) (suc n) with compare' m n
compare' {suc _} (suc m) (suc n) | less x = less (suc x)
compare' {suc _} (suc m) (suc n) | more x = more (subst Fin (compare-lemma2 ((opposite n))) x)
compare' {suc _} (suc m) (suc n) | exact = exact

-- Only return something if it was changed.
-- On later design this comes against us, but lets hold on it for a moment.
insert' : ∀{a}{ub} → Fin ub → a → FinSet ub a → Maybe (FinSet ub a)
insert' i x blank = just (key i x blank blank)
insert' i x (key n _ l r) with compare' i n
insert' i x (key n y l r) | less p = do
  nl ← insert' p x l
  just (key n y nl r)
insert' i x (key n y l r) | more p = do
  nr ← insert' p x r
  just (key n y l nr)
insert' i x (key n y l r) | exact = nothing

remaining : ∀{a}{ub} → FinSet ub a → ℕ
remaining {a} {ub} blank = ub
remaining {a} (key n x l r) = remaining l Data.Nat.+ remaining r

insertion-lemma : ∀ {a : Set} {ub} {i : Fin ub} →
                  toℕ i Data.Nat.+ toℕ (opposite i) Data.Nat.< ub
insertion-lemma {a} {1F} {0F} = s≤s z≤n
insertion-lemma {a} {suc (suc n)} {0F} rewrite sym (compare-lemma {n}) = ≤-refl 
insertion-lemma {a} {suc (suc n)} {suc i} rewrite sym (compare-lemma2 (opposite i)) = s≤s (insertion-lemma {a} {suc n} {i})

just-lemma : ∀{a : Set}{x y : a} → just x ≡ just y → x ≡ y
just-lemma refl = refl

smoothie : ∀ {a b : Set} {v : b} → nothing ≡ just v → a
smoothie ()

rem-lemma1 : ∀ {x l r : ℕ} →
           (poof : suc x Data.Nat.≤ l) →
         suc (x Data.Nat.+ r) Data.Nat.≤ l Data.Nat.+ r
rem-lemma1 {x} {l} {0F} poof rewrite +-identityʳ x | +-identityʳ l = poof
rem-lemma1 {x} {l} {suc r} poof rewrite +-suc x r | +-suc l r = s≤s (rem-lemma1 poof)

rem-lemma2 : ∀ {x l r : ℕ} →
           (poof : suc x Data.Nat.≤ r) →
         suc (l Data.Nat.+ x) Data.Nat.≤ l Data.Nat.+ r
rem-lemma2 {x} {0F} {r} poof = poof
rem-lemma2 {x} {suc l} {r} poof = s≤s (rem-lemma2 poof)

remaining-thm : ∀{a}{ub} → (i : Fin ub) → (x : a) → (s v : FinSet ub a)
  → insert' i x s ≡ just v
  → remaining v Data.Nat.< remaining s
remaining-thm {a} {ub} i x blank (key i x blank blank) refl = insertion-lemma {a} {ub} {i}
remaining-thm i x (key n y l r) v pf with compare' i n
remaining-thm i x (key n y l r) v pf | less z with inspect (insert' z x l)
remaining-thm i x (key n y l r) v pf | less z | just x1 with≡ pf2 rewrite pf2 with remaining-thm z x l x1 pf2
remaining-thm i x (key n y l r) v pf | less z | just x1 with≡ pf2 | poof with just-lemma pf
remaining-thm i x (key n y l r) v pf | less z | just x1 with≡ pf2 | poof | paf rewrite sym paf = rem-lemma1 poof
remaining-thm i x (key n y l r) v pf | less z | nothing with≡ pf2 rewrite pf2 = smoothie pf
remaining-thm i x (key n y l r) v pf | more z with inspect (insert' z x r)
remaining-thm i x (key n y l r) v pf | more z | just x1 with≡ pf2 rewrite pf2 with remaining-thm z x r x1 pf2
remaining-thm i x (key n y l r) v pf | more z | just x1 with≡ pf2 | poof with just-lemma pf
remaining-thm i x (key n y l r) v pf | more z | just x1 with≡ pf2 | poof | paf rewrite sym paf = rem-lemma2 poof
remaining-thm i x (key n y l r) v pf | more z | nothing with≡ pf2 rewrite pf2 = smoothie pf

remaining-wellFounded : ∀{a}{ub} → WellFounded (_<_ on remaining {a} {ub})
remaining-wellFounded = λ x → accessible (<-wellFounded (remaining x))
  where accessible : ∀ {x} → Acc _<_ (remaining x) → Acc (_<_ on remaining) x
        accessible (acc rs) = acc (λ y fy<fx → accessible (rs (remaining y) fy<fx))

record EarleyItem (g : Grammar) (n : ℕ) : Set where
  constructor eim
  field og : Fin (suc n)
        ix : Item g

eim-size : Grammar → ℕ → ℕ
eim-size g n = suc n Data.Nat.* size g 

eim-to-i : ∀{n} → EarleyItem g n → Fin (eim-size g n)
eim-to-i (eim og ix) = combine og (item-to-i ix)

i-to-eim : ∀{n} → Fin (eim-size g n) → EarleyItem g n
i-to-eim {g} {n} i with remQuot {suc n} (size g) i
i-to-eim {g} {n} i | og , j = eim og (i-to-item j)

--eim-theorem1 : ∀{n} → (i : EarleyItem g n) → i-to-eim (eim-to-i i) ≡ i
--eim-theorem1 (eim og ix) = {!!}

ItemSet : Grammar → ℕ → Set
ItemSet g n = FinSet (eim-size g n) (EarleyItem g n)


first-items : ∀{g}{n} → List (EarleyItem g n)
first-items = Data.List.tabulate (λ(x) → eim 0F (first-item x))

eim-lhs : ∀{g}{n} → EarleyItem g n → symbol g
eim-lhs {g} (eim _ (item i _)) = lhs g i

LHS : ∀{g}{n} → symbol g → EarleyItem g n → Set
LHS {g} sym ei = (eim-lhs ei ≡ sym)

dec-lhs : ∀{g}{n} → (s : symbol g) → Decidable (LHS {g} {n} s)
dec-lhs {g} sym ei = symbol-eq g (eim-lhs ei) sym

new-prediction : ∀{g}{n} → EarleyItem g n → List (EarleyItem g n)
new-prediction (eim og ix) with step ix
new-prediction (eim og ix) | just (sym , _) = Data.List.filter (dec-lhs sym) first-items
new-prediction (eim og ix) | nothing = [] -- we can disregard reduction at prediction because
                                          -- our grammar has no empty rules.

prediction : ∀{g}{n} → List (EarleyItem g n)
           → (y : ItemSet g n) → Maybe (List (EarleyItem g n) × Σ (ItemSet g n) (λ(x) → (_<_ on remaining) x y))
prediction [] eims = nothing
prediction (eim' ∷ acu) eims with inspect (insert' (eim-to-i eim') eim' eims)
prediction (eim' ∷ acu) eims | just eims' with≡ pf with remaining-thm (eim-to-i eim') eim' eims eims' pf
prediction (eim' ∷ acu) eims | just eims' with≡ pf | c = just (new-prediction eim' Data.List.++ acu , eims' , c)
prediction (eim' ∷ acu) eims | nothing with≡ _ = prediction acu eims

predict' : ∀{g}{n} → List (EarleyItem g n)
           → (x : ItemSet g n) → Acc (_<_ on remaining) x → ItemSet g n
predict' acu eims (acc q) with prediction acu eims
predict' acu eims (acc q) | just (acu' , eims' , c) = predict' acu' eims' (q eims' c)
predict' acu eims (acc q) | nothing = eims

full-predict : ∀{g}{n} → List (EarleyItem g n)
           → (x : ItemSet g n) → ItemSet g n
full-predict acu eims = predict' acu eims (remaining-wellFounded eims)

start-items : List (EarleyItem g 0)
start-items {g} = to-list (full-predict (Data.List.filter (dec-lhs (start g)) first-items) blank)

data EarleyTrail (g : Grammar) : ℕ → Set where
  empty : List (EarleyItem g 0) → EarleyTrail g 0
  scanned : ∀{n} → EarleyTrail g n → List (EarleyItem g (suc n)) → EarleyTrail g (suc n)

initial : EarleyTrail g 0
initial = empty start-items

move-eim : ∀{g}{n} m → EarleyItem g n → EarleyItem g (m Data.Nat.+ n)
move-eim {g} {n} m (eim og ix) with m ↑ʳ og
move-eim {g} {n} m (eim og ix) | c rewrite +-suc m n = eim c ix

select : ∀ {g}{n} (s : symbol g) → List (EarleyItem g n) → List (EarleyItem g n)
select {g} s [] = []
select {g} s (eim og ix ∷ xs) with step ix
select {g} s (eim og ix ∷ xs) | just (v , ix') with symbol-eq g s v
select {g} s (eim og ix ∷ xs) | just (v , ix') | Dec.yes p = eim og ix' ∷ select s xs
select {g} s (eim og ix ∷ xs) | just (v , ix') | Dec.no ¬p = select s xs
select {g} s (eim og ix ∷ xs) | nothing = select s xs

scan' : ∀{g}{n} → Fin (suc n) → symbol g → EarleyTrail g n → List (EarleyItem g n)
scan' 0F s (empty x) = select s x
scan' 0F s (scanned _ x) = select s x
scan' (suc i) s (scanned trail x) with scan' i s trail
scan' (suc i) s (scanned trail x) | xs = Data.List.map (move-eim 1) xs

new-scan : ∀{g}{n} → EarleyTrail g n → EarleyItem g n → List (EarleyItem g n)
new-scan {g} trail (eim og ix) with step ix
new-scan {g} trail (eim og ix) | just (sym , _) = [] 
new-scan {g} trail (eim og (item i x)) | nothing = scan' og (lhs g i) trail

scanning : ∀{g}{n} → EarleyTrail g n → List (EarleyItem g n)
           → (y : ItemSet g n) → Maybe (List (EarleyItem g n) × Σ (ItemSet g n) (λ(x) → (_<_ on remaining) x y))
scanning tr [] eims = nothing
scanning tr (eim' ∷ acu) eims with inspect (insert' (eim-to-i eim') eim' eims)
scanning tr (eim' ∷ acu) eims | just eims' with≡ pf with remaining-thm (eim-to-i eim') eim' eims eims' pf
scanning tr (eim' ∷ acu) eims | just eims' with≡ pf | c = just (new-scan tr eim' Data.List.++ acu , eims' , c)
scanning tr (eim' ∷ acu) eims | nothing with≡ _ = scanning tr acu eims

scanning' : ∀{g}{n} → EarleyTrail g n → List (EarleyItem g n)
           → (x : ItemSet g n) → Acc (_<_ on remaining) x → ItemSet g n
scanning' tr acu eims (acc q) with scanning tr acu eims
scanning' tr acu eims (acc q) | just (acu' , eims' , c) = scanning' tr acu' eims' (q eims' c)
scanning' tr acu eims (acc q) | nothing = eims

full-scan : ∀{g}{n} → EarleyTrail g n → List (EarleyItem g n)
           → (x : ItemSet g n) → ItemSet g n
full-scan tr acu eims = scanning' tr acu eims (remaining-wellFounded eims)

earley-step : ∀{g}{n} → symbol g → EarleyTrail g n → EarleyTrail g (suc n)
earley-step s tr = scanned tr post-predict
  where post-scan = to-list (full-scan tr (scan' 0F s tr) blank)
        post-predict = to-list (full-predict (Data.List.map (move-eim 1) post-scan) blank)

-------------------------------------------------------------------------------
-- Sample grammar
-------------------------------------------------------------------------------
data sample1symbol : Set where
  S A hello something : sample1symbol

sample1symbol-eq : (x y : sample1symbol) → Dec (x ≡ y)
sample1symbol-eq S S = Dec.yes refl
sample1symbol-eq S A = Dec.no (λ ())
sample1symbol-eq S hello = Dec.no (λ ())
sample1symbol-eq S something = Dec.no (λ ())
sample1symbol-eq A S = Dec.no (λ ())
sample1symbol-eq A A = Dec.yes refl
sample1symbol-eq A hello = Dec.no (λ ())
sample1symbol-eq A something = Dec.no (λ ())
sample1symbol-eq hello S = Dec.no (λ ())
sample1symbol-eq hello A = Dec.no (λ ())
sample1symbol-eq hello hello = Dec.yes refl
sample1symbol-eq hello something = Dec.no (λ ())
sample1symbol-eq something S = Dec.no (λ ())
sample1symbol-eq something A = Dec.no (λ ())
sample1symbol-eq something hello = Dec.no (λ ())
sample1symbol-eq something something = Dec.yes refl

sample1 : Grammar
symbol sample1 = sample1symbol
symbol-eq sample1 = sample1symbol-eq
start sample1 = S
reductions sample1 = 3
lhs sample1 0F = S
lhs sample1 1F = A
lhs sample1 2F = A
cel sample1 0F = 2
cel sample1 1F = 1
cel sample1 2F = 2
rhs sample1 0F = A ∷ something ∷ []
rhs sample1 1F = hello ∷ []
rhs sample1 2F = A ∷ hello ∷ []
nhs sample1 0F ()
nhs sample1 1F ()
nhs sample1 2F ()

ex3 = initial {sample1}
ex4 = earley-step hello ex3