Parser in agda

FinMap.agda

module FinMap where

open import Agda.Builtin.Equality
open import Relation.Binary.PropositionalEquality using (refl; cong; trans; subst; sym)
open import Data.Nat as ℕ using (ℕ; _<_; _≤_; suc; s≤s; z≤n)
open import Data.Nat.Properties using (≤-refl; +-comm; +-identityˡ; +-identityʳ; +-suc; 1+n≢0)
open import Data.Fin hiding (compare; _<_; _≤_)
open import Data.List
open import Data.Product
open import Data.Sum
open import Data.Maybe
open import Function using (_on_; id; _∘_)
open import Induction.WellFounded
open import Data.Nat.Induction using (<-wellFounded)

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

private
  toℕfromℕ : ∀ n → toℕ (fromℕ n) ≡ n
  toℕfromℕ 0F = refl
  toℕfromℕ (suc n) = cong suc (toℕfromℕ n)

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

  toℕopposite : ∀ {m} {n : Fin m} → toℕ (inject₁ (opposite n)) ≡ toℕ (opposite n)
  toℕopposite {suc m} {0F} = toℕinject (fromℕ m)
  toℕopposite {suc m} {suc n} = toℕinject (inject₁ (opposite n))

lower : ∀ {ub} {n : Fin ub} (i : Fin (toℕ n)) → Fin ub
lower {.(suc _)} {suc n} 0F = zero
lower {.(suc _)} {suc n} (suc i) = suc (lower i)

higher : ∀ {ub} {n : Fin ub} (i : Fin (toℕ (opposite n))) → Fin ub
higher {n = 0F} i = suc (subst Fin (toℕfromℕ _) i)
higher {ub = suc ub} {n = suc n} i = suc (higher {ub} {n} (subst Fin (toℕinject (opposite n)) i))

private
  lemma3 : ∀{ub} (i : Fin ub) → toℕ i ℕ.+ toℕ (opposite i) < ub
  lemma3 {ub} 0F = subst (λ(x) → x < ub) (sym (toℕfromℕ _)) (s≤s ≤-refl)
  lemma3 {ub = suc n} (suc i) rewrite sym (sym (toℕinject (opposite i))) = s≤s (lemma3 i)

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

private
  lemma10 : {z z' : ℕ} {p : z ≡ z'} (x : Fin z') → x ≡ subst Fin p (subst Fin (sym p) x)
  lemma10 {z} {.z} {refl} x = refl

compare : ∀{ub} → (m n : Fin ub) → Comparison ub m n
compare {suc _} 0F 0F = exact refl
compare {suc n} (suc m) 0F = more (subst Fin (sym (toℕfromℕ n)) m) (cong suc (lemma10 {p = toℕfromℕ n} m))
compare {suc _} 0F (suc n) = less 0F refl
compare {suc _} (suc m) (suc n) with compare m n
compare {suc _} (suc m) (suc n) | less x p = less (suc x) (cong suc p)
compare {suc _} (suc m) (suc n) | more x p rewrite p = more (subst Fin (sym (toℕinject (opposite n))) x) (cong suc (cong higher (lemma10 {p = toℕinject (opposite n)} x)))
compare {suc _} (suc m) (suc n) | exact refl = exact refl

private
  rem-lemma1 : ∀ {x l r : ℕ} → (poof : x < l) → (x ℕ.+ r) < l ℕ.+ 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 : x < r) →
             (l ℕ.+ x) < l ℕ.+ r
  rem-lemma2 {x} {0F} {r} poof = poof
  rem-lemma2 {x} {suc l} {r} poof = s≤s (rem-lemma2 poof)

-------------------------------------------------------------------------------
-- Purposefully finite maps
-------------------------------------------------------------------------------

module FinMap (k : Set)
              (size : ℕ)
              (keyfn : k → Fin size)
              (keyfn-inj : ∀{k k'} → keyfn k ≡ keyfn k' → k ≡ k') where

  data FinMap' (ub : ℕ) (m : Fin ub → Fin size) (F : k → Set) : Set where
    blank : FinMap' ub m F
    key : (n : Fin ub) → (x : k) → F x
       → keyfn x ≡ m n
       → FinMap' (toℕ n) (m ∘ lower) F
       → FinMap' (toℕ (opposite n)) (m ∘ higher) F
       → FinMap' ub m F

  FinMap : (k → Set) → Set
  FinMap F = FinMap' size id F

  to-list' : ∀{ub} {F : k → Set} → {m : Fin ub → Fin size} → FinMap' ub m F → List (Σ k F)
  to-list' blank = []
  to-list' (key n x v p s t) = to-list' s ++ ((x , v) ∷ to-list' t)

  to-list : {F : k → Set} → FinMap F → List (Σ k F)
  to-list = to-list'

  remaining : ∀{ub} {F : k → Set} {m : Fin ub → Fin size} → FinMap' ub m F → ℕ
  remaining {ub} blank = ub
  remaining (key _ _ _ _ l r) = remaining l ℕ.+ remaining r

  insert' : ∀{ub} {F : k → Set} {m : Fin ub → Fin size}
    → (n : Fin ub) → (x : k) → (Maybe (F x) → F x) → keyfn x ≡ m n
    → (y : FinMap' ub m F)
    → Σ (FinMap' ub m F) (λ(x) → (remaining y ≡ remaining x) ⊎ (remaining x ℕ.< remaining y))
  insert' n' x' v' p' blank = key n' x' (v' nothing) p' blank blank , inj₂ (lemma3 n')
  insert' n' x' v' p' (key n x v p s t) with compare n' n
  insert' n' x' v' p' (key n x v p s t) | less k p'' rewrite p'' with insert' k x' v' p' s
  insert' n' x' v' p' (key n x v p s t) | less k p'' | s' , inj₁ eq rewrite eq = key n x v p s' t , inj₁ refl
  insert' n' x' v' p' (key n x v p s t) | less k p'' | s' , inj₂ c = key n x v p s' t , inj₂ (rem-lemma1 c)
  insert' n' x' v' p' (key n x v p s t) | more k p'' rewrite p'' with insert' k x' v' p' t
  insert' n' x' v' p' (key n x v p s t) | more k p'' | t' , inj₁ eq rewrite eq = key n x v p s t' , inj₁ refl
  insert' n' x' v' p' (key n x v p s t) | more k p'' | t' , inj₂ c = key n x v p s t' , inj₂ (rem-lemma2 c)
  insert' n' x' v' p' (key n' x v p s t) | exact refl rewrite sym p' with keyfn-inj p
  insert' n' x' v' p' (key n' x' v p s t) | exact refl | refl = key n' x' (v' (just v)) p' s t , inj₁ refl

  insert : ∀{F : k → Set}
    → (x : k) → (Maybe (F x) → F x)
    → (y : FinMap F)
    → Σ (FinMap F) (λ(x) → (remaining y ≡ remaining x) ⊎ (remaining x ℕ.< remaining y))
  insert x' v' = insert' (keyfn x') x' v' refl

  remaining-wellFounded : ∀{a b}{ub} → WellFounded (_<_ on remaining {a}{b} {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))

parser.agda

module parser where

-- It's got problems left to solve

open import Level using (Level; _⊔_)
open import Agda.Builtin.Equality
open import Relation.Nullary using (Dec)
open import Data.Nat as ℕ hiding (compare; _⊔_)
open import Data.Nat.Properties as ℕprop using (suc-injective; n≮n)
open import Data.Fin as Fin hiding (_<_; _≤_; compare)
open import Data.Fin.Properties as 𝔽prop using (suc-injective)
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.Maybe
open import Data.Product
open import Data.Unit hiding (_≤_)
open import Data.Empty
open import Data.List
open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.All.Properties using (all-filter)
open import Relation.Binary.PropositionalEquality using (refl; cong; trans; subst; sym)
open import Data.Nat.Properties using (≤-refl; +-comm; +-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)
open import FinMap
open import Trail as Trail using (Trail; ε; _‣_)

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

data HList : List Set → Set where
  empty : HList []
  cons  : ∀{a : Set}{xs} → a → HList xs → HList (a ∷ xs)

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 → ⊥
        semantic : symbol → Set
        reducer : (i : Fin reductions) → HList (Data.List.map semantic (Vec.toList (rhs i))) → semantic (lhs i)
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 Fin.≟ j
item-eq (item i x) (item i y) | Dec.yes refl with x 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

index-lemma : ∀ {n : ℕ}{a : Set} (i : Fin (suc n)) (j : Fin (suc n)) (x : Vec a n) {v} → index i x ≡ just (v , j) → suc (toℕ i) ≡ toℕ j
index-lemma {.0F} 0F j [] ()
index-lemma {.(suc _)} 0F .1F (x ∷ _) refl = refl
index-lemma {.(suc _)} (suc i) j (_ ∷ k) pf with inspect (index i k)
index-lemma {.(suc _)} (suc i) j (_ ∷ k) pf | just (v , j') with≡ x rewrite x with index-lemma i j' k x
index-lemma {.(suc _)} (suc i) (suc j') (_ ∷ k) refl | just (v , j') with≡ x | lem = cong suc lem
index-lemma {.(suc _)} (suc i) j (_ ∷ k) {v} pf | nothing with≡ x rewrite x = ⊥-elim (bork pf)
    where bork : ∀ {v} → nothing ≡ just v → ⊥
          bork ()

index-lemma2 : ∀ {n : ℕ}{a : Set} (i : Fin (suc n)) (x : Vec a n) → index i x ≡ nothing → toℕ i ≡ n
index-lemma2 0F [] p = refl
index-lemma2 (suc i) (_ ∷ k) p with inspect (index i k)
index-lemma2 (suc i) (_ ∷ k) p | just _ with≡ q rewrite q with p
index-lemma2 (suc i) (_ ∷ k) p | just _ with≡ q | ()
index-lemma2 (suc i) (_ ∷ k) p | nothing with≡ q = cong suc (index-lemma2 i k q)

step-lemma1 : ∀ {g} (i j : Item g) {v : symbol g} → step i ≡ just (v , j) → Item.i i ≡ Item.i j
step-lemma1 {g} (item i x) j p with index x (rhs g i)
step-lemma1 {g} (item i x) .(item i y) refl | just (s , y) = refl

step-lemma2 : ∀ {g} (i j : Item g) {v : symbol g} → step i ≡ just (v , j) → suc (toℕ (Item.x i)) ≡ toℕ (Item.x j)
step-lemma2 {g} (item i x) j p with inspect (index x (rhs g i))
step-lemma2 {g} (item i x) j p | just (fst , snd) with≡ q rewrite q with index-lemma x snd (rhs g i) q
step-lemma2 {g} (item i x) (item i snd) refl | just (fst , snd) with≡ q | lem = lem
step-lemma2 {g} (item i x) j p | nothing with≡ q rewrite q = ⊥-elim (bork p)
    where bork : ∀ {v} → nothing ≡ just v → ⊥
          bork ()

step-lemma3 : ∀ {g} (i : Item g) → step i ≡ nothing → toℕ (Item.x i) ≡ cel g (Item.i i)
step-lemma3 {g} (item i x) p with inspect (index {cel g i} x (rhs g i))
step-lemma3 {g} (item i x) p | just _ with≡ q rewrite q with p
step-lemma3 {g} (item i x) p | just _ with≡ q | ()
step-lemma3 {g} (item i x) p | nothing with≡ q = index-lemma2 x (rhs g i) q

safe-lookup : ∀ {a : Set} (n : ℕ) (list : List a) → n < length list → a
safe-lookup 0F (x ∷ xs) bound = x
safe-lookup (suc n) (x ∷ xs) (s≤s bound) = safe-lookup n xs bound

index-to-safe-lookup : ∀ {a : Set} {n : ℕ} (x y : Fin (suc n)) (xs : Vec a n) {v : a} → index x xs ≡ just (v , y) → toℕ x < n
index-to-safe-lookup {_} {suc _} 0F y (x ∷ xs) p = s≤s z≤n
index-to-safe-lookup {_} {suc _} (suc x) y (_ ∷ xs) p with inspect (index x xs)
index-to-safe-lookup {_} {suc _} (suc x) y (_ ∷ xs) p | just (fst , snd) with≡ q rewrite q with p
index-to-safe-lookup {_} {suc n} (suc x) (suc y) (_ ∷ xs) p | just (v , y) with≡ q | refl = s≤s (index-to-safe-lookup x y xs q)
index-to-safe-lookup {_} {suc _} (suc x) y (_ ∷ xs) p | nothing with≡ q rewrite q with p
index-to-safe-lookup {_} {suc _} (suc x) y (_ ∷ xs) p | nothing with≡ q | ()

vec-length-lemma : ∀ {a : Set} {n : ℕ} (vec : Vec a n) → length (Vec.toList vec) ≡ n
vec-length-lemma {n = 0F} [] = refl
vec-length-lemma {n = suc i} (x ∷ vec) = cong suc (vec-length-lemma vec)

index-to-safe-lookup' : ∀ {a : Set} {n : ℕ} (x y : Fin (suc n)) (xs : Vec a n) {v : a} → (p : index x xs ≡ just (v , y)) → (q : toℕ x < length (Vec.toList xs)) → safe-lookup (toℕ x) (Vec.toList xs) q ≡ v
index-to-safe-lookup' 0F .1F (x ∷ xs) refl q = refl
index-to-safe-lookup' (suc x) y (x₁ ∷ xs) p (s≤s q) with inspect (index x xs)
index-to-safe-lookup' (suc x) y (x₁ ∷ xs) p (s≤s q) | just (v , y') with≡ ö rewrite ö with p
index-to-safe-lookup' (suc x) (suc y) (x₁ ∷ xs) p (s≤s q) | just (v , y) with≡ ö | refl = index-to-safe-lookup' x y xs ö q
index-to-safe-lookup' (suc x) y (x₁ ∷ xs) p (s≤s q) | nothing with≡ ö rewrite ö with p
index-to-safe-lookup' (suc x) y (x₁ ∷ xs) p (s≤s q) | nothing with≡ ö | ()

step-to-safe-lookup : ∀ {g} (i j : Item g) {v : symbol g} → step i ≡ just (v , j) → toℕ (Item.x i) < length (Vec.toList (rhs g (Item.i i)))
step-to-safe-lookup {g} (item i x) j p with inspect (index {cel g i} x (rhs g i))
step-to-safe-lookup {g} (item i x) j p | just (s , y) with≡ q rewrite q with index-to-safe-lookup {n = cel g i} x y (rhs g i) q
step-to-safe-lookup {g} (item i x) j p | just (s , y) with≡ q | cond rewrite vec-length-lemma {n = cel g i} (rhs g i) = cond
step-to-safe-lookup {g} (item i x) j p | nothing with≡ q rewrite q with p
step-to-safe-lookup {g} (item i x) j p | nothing with≡ q | ()

step-to-safe-lookup' : ∀ {g} (i j : Item g) {v : symbol g} → (p : step i ≡ just (v , j))
                                                           → (c : toℕ (Item.x i) < length (Vec.toList (rhs g (Item.i i))))
                                                           → safe-lookup (toℕ (Item.x i)) (Vec.toList (rhs g (Item.i i))) c ≡ v
step-to-safe-lookup' {g} (item i x) j p c with inspect (index {cel g i} x (rhs g i))
step-to-safe-lookup' {g} (item i x) j p c | just (v , y) with≡ q rewrite q with p
step-to-safe-lookup' {g} (item i x) j p c | just (v , y) with≡ q | refl = index-to-safe-lookup' x y (rhs g i) q c
step-to-safe-lookup' {g} (item i x) j p c | nothing with≡ q rewrite q with p
step-to-safe-lookup' {g} (item i x) j p c | nothing with≡ q | ()

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 = tabulate (item i)

-- each i ≡ each j → i ≡ j

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 ∈ tabulate f)
  → (j : f k ∈ 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) (𝔽prop.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 _ = concat (tabulate each)

list-lemma : ∀{a : Set}{x : a}{xs ys : List a} → x ∈ xs → x ∈ (xs ++ 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 ++ 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 (length xs)
contain-to-index (here x) = 0F
contain-to-index (there pos) = suc (contain-to-index pos)

contain-to-index-injective : {a : Set}{k k' : a}(xs : List a)
  → (i : k ∈ xs) → (j : k' ∈ xs)
  → contain-to-index i ≡ contain-to-index j → k ≡ k'
contain-to-index-injective (x ∷ xs) (here refl) (here refl) refl = refl
contain-to-index-injective (x ∷ xs) (here i) (there j) ()
contain-to-index-injective (x ∷ xs) (there i) (here j) ()
contain-to-index-injective (x ∷ xs) (there i) (there j) ij = contain-to-index-injective xs i j (𝔽prop.suc-injective ij)

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

index-to-contain : {a : Set}(xs : List a) → (i : Fin (length xs)) → Σ a (λ(x) → x ∈ xs)
index-to-contain (x ∷ xs) 0F = x , here refl
index-to-contain (x ∷ xs) (suc i) = Data.Product.map₂ there (index-to-contain xs i)

index-thm : {a : Set}(x : a)(xs : List a) (i : x ∈ xs) → index-to-contain xs (contain-to-index i) ≡ (x , i)
index-thm x (y ∷ ys) (here refl) = refl
index-thm x (y ∷ ys) (there i) with index-thm x ys i
index-thm x (y ∷ ys) (there i) | c rewrite c = refl

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 ∈ concat (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 = 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 (all-items g) ix

-- item-theorem0 : (i : Fin (size g)) → item-to-i (i-to-item i) ≡ i
-- item-theorem0 {g} i = {!!}

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

item-to-i-injective : (x y : Item g) → item-to-i x ≡ item-to-i y → x ≡ y
item-to-i-injective {g} x y pf rewrite contain-to-index-injective (all-items g) (all-items-complete g x) (all-items-complete g y) pf = refl


-- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
infixl 5 _↑ˡ_
_↑ˡ_ : ∀ {m} → Fin m → ∀ n → Fin (m ℕ.+ 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 ℕ.+ m)
zero    ↑ʳ i = i
(suc n) ↑ʳ i = suc (n ↑ʳ i)

splitAt' : ∀ m {n} → Fin (m ℕ.+ 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 ℕ.* 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 ℕ.* k)
combine {suc n} {k} zero    y = y ↑ˡ (n ℕ.* k)
combine {suc n} {k} (suc x) y = k ↑ʳ (combine x y)

combine-lemma1 : ∀ {k} n {p q : Fin k} → p ↑ˡ n ≡ q ↑ˡ n → p ≡ q
combine-lemma1 {suc _} n {0F} {0F} refl = refl
combine-lemma1 {suc k} n {suc p} {suc q} pf = cong suc (combine-lemma1 n {p} {q} (𝔽prop.suc-injective pf))

combine-lemma2 : ∀ {k m} (x y : Fin m) → k ↑ʳ x ≡ k ↑ʳ y → x ≡ y
combine-lemma2 {0F} x y pf = pf
combine-lemma2 {suc k} x y pf = combine-lemma2 x y (𝔽prop.suc-injective pf)

sublemma4 : ∀{k n m} → (p : Fin k) → (z : Fin m) → toℕ (p ↑ˡ n) < toℕ (k ↑ʳ z)
sublemma4 {suc k} {n} {m} 0F z = s≤s z≤n
sublemma4 {suc k} {n} {m} (suc p) z = s≤s (sublemma4 p z)

contradiction1 : ∀ {p q : ℕ} → p ≡ q → suc p ≤ q → ⊥
contradiction1 {n} {n} refl p<q = n≮n n p<q

combine-lemma3 : ∀ {n} {k} (i : Fin n) (p q : Fin k)
                   (pf : (p ↑ˡ (n ℕ.* k)) ≡ (k ↑ʳ (combine i q))) → ⊥
combine-lemma3 {n} {k} i p q proof = contradiction1 proof' pum
  where proof' = cong toℕ proof
        pum = sublemma4 {k} {n * k} p (combine i q)

combine-injective : ∀{n k} → (i j : Fin n) (p q : Fin k)
  → combine i p ≡ combine j q → (i ≡ j) × (p ≡ q)
combine-injective {suc n} {k} 0F 0F p q proof = refl , combine-lemma1 (n * k) proof
combine-injective {suc n} {k} 0F (suc j) p q proof = ⊥-elim (combine-lemma3 j p q proof)
combine-injective {suc n} {k} (suc i) 0F p q proof = ⊥-elim (combine-lemma3 i q p (sym proof))
combine-injective {suc n} {k} (suc i) (suc j) p q proof = Data.Product.map₁ (cong suc) poof
  where proof' = combine-lemma2 (combine i p) (combine j q) proof
        poof = combine-injective i j p q proof'

top : ∀{n} → Fin (suc n)
top {0F} = 0F
top {suc n} = suc top



ex6 : Trail ℕ
ex6 = ε ‣ 3 ‣ 2

++-lemma : ∀ m → m ≡ m ℕ.+ 0
++-lemma 0F = refl
++-lemma (suc m) = cong suc (++-lemma m)


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

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

lemma3 : ∀{ub} (i : Fin ub) → toℕ i ℕ.+ toℕ (opposite i) < ub
lemma3 {ub} 0F = subst (λ(x) → x < ub) lemma (s≤s ≤-refl)
lemma3 {ub = suc n} (suc i) rewrite sym (lemma2 (opposite i)) = s≤s (lemma3 i)


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

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

eim-to-i : ∀{n} → EIM 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) → EIM 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) = {!!}

eim-to-i-injective : ∀{n} → {x y : EIM g n} → eim-to-i x ≡ eim-to-i y → x ≡ y
eim-to-i-injective {x = eim og ix} {y = eim og' ix'} p with combine-injective og og' (item-to-i ix) (item-to-i ix') p
eim-to-i-injective {x = eim og ix} {y = eim og ix'} p | refl , p' with item-to-i-injective ix ix' p'
eim-to-i-injective {x = eim og (item i x)} {y = eim og (item i x)} p | refl , p' | refl = refl

-----------------------------------------------------------------
-- Shared packed parse forests
-----------------------------------------------------------------
IsPrefix : {a : Set} → Trail a → Trail a → Set
IsPrefix {a} xs ys = Σ (Trail a) λ(zs) → (xs Trail.++ zs) ≡ ys

data SPPF (g : Grammar) : Trail (symbol g) → Item g → Set where
  leaf : ∀ {i} → Item.x i ≡ 0F → SPPF g ε i
  shift : ∀{xs ys zs i j k} → SPPF g xs i → SPPF g ys j
    → xs Trail.++ ys ≡ zs
    → step j ≡ nothing
    → step i ≡ just (lhs g (Item.i j) , k)
    → SPPF g zs k
  shift' : ∀{xs i j} → SPPF g xs i → (s : symbol g) → semantic g s → step i ≡ just (s , j) → SPPF g (xs ‣ s) j
  branch : ∀{xs i} → SPPF g xs i → SPPF g xs i → SPPF g xs i

-- Otherwise identical structure, but branches are missing.
data SPF (g : Grammar) : Trail (symbol g) → Item g → Set where
  leaf1 : ∀ {i} → Item.x i ≡ 0F → SPF g ε i
  shift1 : ∀{xs ys zs i j k} → SPF g xs i → SPF g ys j
    → xs Trail.++ ys ≡ zs
    → step j ≡ nothing
    → step i ≡ just (lhs g (Item.i j) , k)
    → SPF g zs k
  shift1' : ∀{xs i j} → SPF g xs i → (s : symbol g) → semantic g s → step i ≡ just (s , j) → SPF g (xs ‣ s) j

cartesian : {a b : Set} → List a → List b → List (a × b)
cartesian [] ys = []
cartesian (x ∷ xs) ys = Data.List.map (λ(y) → (x , y)) ys ++ cartesian xs ys

SPPF-to-list : ∀{g}{xs}{i} → SPPF g xs i → List (SPF g xs i)
SPPF-to-list (leaf x) = [ leaf1 x ]
SPPF-to-list (shift sppf sppf' x z w) = Data.List.map (λ(spf , spf') → shift1 spf spf' x z w) (cartesian (SPPF-to-list sppf) (SPPF-to-list sppf'))
SPPF-to-list (shift' sppf s x y) = Data.List.map (λ(spf) → shift1' spf s x y) (SPPF-to-list sppf)
SPPF-to-list (branch sppf sppf') = SPPF-to-list sppf ++ SPPF-to-list sppf'

drop* : ∀ {A : Set} m {n} {p} → Vec A p → p ≡ (m ℕ.+ n) → Vec A n
drop* 0F xs refl = xs
drop* (suc m) (_ ∷ xs) refl = drop* m xs refl

drop-lemma : ∀ {A : Set}{n m} → (a : Vec A n) → (pf : n ≡ m) → Vec.toList (drop* 0 a pf) ≡ Vec.toList a
drop-lemma {n} a refl = refl

vec-lemma : ∀ {A : Set} (a b : Vec A 0) → a ≡ b
vec-lemma [] [] = refl

drop-lemma2 : ∀ {A : Set}{n} → (a : Vec A n) → (pf : n ≡ n ℕ.+ 0) → (drop* n a pf) ≡ []
drop-lemma2 {A} {n} a pf = vec-lemma (drop* n a pf) []

SmallHList : ∀ g → (i : Fin (reductions g)) → (n m : ℕ) → cel g i ≡ n ℕ.+ m → Set
SmallHList g i n m p = HList (Data.List.map (semantic g) (Vec.toList (drop* n (rhs g i) p)))

SPF-init : ∀ {g} (i : Item g)
         (lem : toℕ (Item.x i) ≡ cel g (Item.i i))
         (lem' : toℕ (Item.x i) ℕ.+ 0 ≡ toℕ (Item.x i))
      → SmallHList g (Item.i i) (toℕ (Item.x i)) 0 (trans (sym lem) (sym lem'))
SPF-init {g} i lem lem' rewrite lem | drop-lemma2 (rhs g (Item.i i)) (sym lem') = empty

simplify-problem : ∀ {a : Set} (x n m : ℕ) (xs : Vec a n) (p : n ≡ x ℕ.+ m) → Vec.toList (drop* x xs p) ≡ drop x (Vec.toList xs)
simplify-problem 0F _ n xs refl = refl
simplify-problem (suc x) .(suc x ℕ.+ n) n (_ ∷ xs) refl = simplify-problem x (x ℕ.+ n) n xs refl

drop-lemma3 : ∀ {a : Set} (i : ℕ) (xs : List a) (cmp : i < length xs) → (drop i xs) ≡ safe-lookup i xs cmp ∷ (drop (suc i) xs)
drop-lemma3 0F (x ∷ xs) cmp = refl
drop-lemma3 (suc i) (x ∷ xs) (s≤s cmp) = drop-lemma3 i xs cmp

SPF-lemma1 : ∀ {g} {i : Fin (reductions g)}
               (x1 x2 : Fin (suc (cel g i))) {m}
               {lem3 : toℕ x1 ℕ.+ suc m ≡ suc (toℕ x1 ℕ.+ m)}
               {p : cel g i ≡ suc (toℕ x1) ℕ.+ m}
               (sy : symbol g)
               (w : step (item i x1) ≡ just (sy , item i x2))
           → HList
             (semantic g sy ∷
              Data.List.map (semantic g) (Vec.toList (drop* (suc (toℕ x1)) (rhs g i) p)))
           → HList
             (Data.List.map (semantic g) (Vec.toList (drop* (toℕ x1) (rhs g i) (trans p (sym lem3)))))
SPF-lemma1 {g} {i} x1 x2 {m} {lem3} {p} sy w hlist
  rewrite simplify-problem (toℕ x1) _ _ (rhs g i) (trans p (sym lem3))
  rewrite simplify-problem (suc (toℕ x1)) _ _ (rhs g i) p with step-to-safe-lookup {g} (item i x1) (item i x2) w
SPF-lemma1 {g} {i} x1 x2 {m} {lem3} {p} sy w hlist | safe with step-to-safe-lookup' {g} (item i x1) (item i x2) w safe | drop-lemma3 (toℕ x1) (Vec.toList (rhs g i)) safe
SPF-lemma1 {g} {i} x1 x2 {m} {lem3} {p} sy w hlist | safe | safe' | dr rewrite sym safe' | dr = hlist

mutual
  SPF-to-list : ∀{g}{m}{xs}{i} → SPF g xs i → (p : cel g (Item.i i) ≡ toℕ (Item.x i) ℕ.+ m) → SmallHList g (Item.i i) (toℕ (Item.x i)) m p → SmallHList g (Item.i i) 0 (toℕ (Item.x i) ℕ.+ m) p
  SPF-to-list (leaf1 x) p ac rewrite x = ac
  SPF-to-list {m = m} (shift1 {i = i} {j = j} {k = k} spf rd x z w) p ac with step-lemma1 i k w | step-lemma2 i k w | +-suc (toℕ (Item.x i)) m
  SPF-to-list {g} {m = m} (shift1 {i = item _ x1} {j = j} {k = item _ x2} spf rd x z w) p ac | refl | lem2 | lem3 rewrite sym lem2 with SPF-to-list {m = suc m} spf (trans p (sym lem3)) (SPF-lemma1 x1 x2 (lhs g (Item.i j)) w (cons (SPF-to-semantic z rd) ac))
  SPF-to-list {g} {m = m} (shift1 {i = item q x1} {j = j} {k = item _ x2} spf rd x z w) p ac | refl | lem2 | lem3 | hlist rewrite drop-lemma (rhs g q) p | drop-lemma (rhs g q) (trans p (sym lem3)) = hlist
  SPF-to-list {m = m} (shift1' {i = item q x1} {j = item q' x2} spf s x w) p ac with step-lemma1 (item q x1) (item q' x2) w | step-lemma2 (item q x1) (item q' x2) w | +-suc (toℕ x1) m
  SPF-to-list {m = m} (shift1' {i = item q x1} {j = item q x2} spf s x w) p ac | refl | lem2 | lem3 rewrite sym lem2 with SPF-to-list {m = suc m} spf (trans p (sym lem3)) (SPF-lemma1 x1 x2 s w (cons x ac))
  SPF-to-list {g} {m = m} (shift1' {i = item q x1} {j = item q x2} spf s x w) p ac | refl | lem2 | lem3 | hlist rewrite drop-lemma (rhs g q) p | drop-lemma (rhs g q) (trans p (sym lem3)) = hlist

  SPF-to-hlist : ∀{g}{xs}{i} → step i ≡ nothing → SPF g xs i → HList (Data.List.map (semantic g) (Vec.toList (rhs g (Item.i i))))
  SPF-to-hlist {g} {i = i} p spf with step-lemma3 i p | +-identityʳ (toℕ (Item.x i))
  SPF-to-hlist {g} {i = i} p spf | lem | lem' with SPF-to-list {m = 0} spf (trans (sym lem) (sym lem')) (SPF-init i lem lem') | drop-lemma (rhs g (Item.i i)) (trans (sym lem) (sym lem'))
  SPF-to-hlist {g} p spf | lem | lem' | hlist | lem'' rewrite lem'' = hlist

  SPF-to-semantic : ∀{g}{n}{i} → step i ≡ nothing → SPF g n i → semantic g (lhs g (Item.i i))
  SPF-to-semantic {g} {i = i} p spf = reducer g (Item.i i) (SPF-to-hlist p spf)

-----------------------------------------------------------------
-- Itemsets
-----------------------------------------------------------------
eim-f : ∀{g}{n} (xs : Trail (symbol g)) → EIM g n → Set
eim-f {g} xs ei = SPPF g (Trail.take (toℕ (EIM.og ei)) xs) (EIM.ix ei)

spf-f : ∀{g}{n} (xs : Trail (symbol g)) → EIM g n → Set
spf-f {g} xs ei = SPF g (Trail.take (toℕ (EIM.og ei)) xs) (EIM.ix ei)

module ItemSet {g : Grammar} {n : ℕ} where
  open FinMap.FinMap (EIM g n) (eim-size g n) eim-to-i eim-to-i-injective public
    using (FinMap; remaining; remaining-wellFounded; insert; to-list; blank)

ItemSet : (g : Grammar) → (n : ℕ) → Trail (symbol g) → Set
ItemSet g n xs = ItemSet.FinMap {g} {n} (eim-f xs)

is-first-item : ∀{g}{n} → EIM g n → Set
is-first-item ei = (Item.x (EIM.ix ei) ≡ 0F) × (EIM.og ei ≡ 0F)

first-items : ∀{g}{n} → List (Σ (EIM g n) is-first-item)
first-items = tabulate (λ(x) → eim 0F (first-item x) , refl , refl)

eim-lhs : ∀{g}{n} → Σ (EIM g n) is-first-item  → symbol g
eim-lhs {g} (eim _ (item i _) , _) = lhs g i

LHS : ∀{g}{n} → symbol g → Σ (EIM g n) is-first-item → 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

by-lhs : ∀{g}{n}{xs} → symbol g → List (Σ (EIM g n) (eim-f xs))
by-lhs s = Data.List.map fun (filter (dec-lhs s) first-items)
  where fun : ∀{g}{n}{xs} → Σ (EIM g n) is-first-item → Σ (EIM g n) (eim-f xs)
        fun {g}{n}{xs} (ei , p1 , p2) = ei , subst (λ(x) → SPPF g (Trail.take (toℕ x) xs) (EIM.ix ei)) (sym p2) (leaf p1)

-- These are for recognition phase.
Accepted : ∀ g n → EIM g n → Set
Accepted g n ei = (EIM.og ei ≡ top) × lhs g (Item.i (EIM.ix ei)) ≡ start g × step (EIM.ix ei) ≡ nothing

dec-accepted : ∀{g}{n} → Decidable (Accepted g n)
dec-accepted {g} ei with (EIM.og ei) Fin.≟ top | symbol-eq g (lhs g (Item.i (EIM.ix ei))) (start g) | inspect(step (EIM.ix ei))
dec-accepted {g} (eim og ix) | Dec.yes p | Dec.yes q | nothing with≡ x = Dec.yes ( p , q , x )
dec-accepted {g} (eim og ix) | Dec.yes p | Dec.yes q | just y with≡ x = Dec.no λ( p' , q' , x' ) → ⊥-elim (clash (trans (sym  x) x'))
  where clash : just y ≡ nothing → ⊥
        clash ()
dec-accepted {g} (eim og ix) | Dec.yes p | Dec.no ¬q | y with≡ x = Dec.no λ( p' , q' , x' ) → ⊥-elim (¬q q')
dec-accepted {g} (eim og ix) | Dec.no ¬p | d2 | y with≡ x = Dec.no λ( p' , q' , x' ) → ⊥-elim (¬p p')

new-prediction : ∀{g}{n}{xs} → EIM g n → List (Σ (EIM g n) (eim-f xs))
new-prediction (eim og ix) with step ix
new-prediction {n = n} (eim og ix) | just (sy , _) = by-lhs sy 
new-prediction (eim og ix) | nothing = [] -- we can disregard reduction at prediction because
                                          -- our grammar has no empty rules.

prediction-mutor : ∀{g}{n}{xs} {x} → eim-f {g}{n} xs x → Maybe (eim-f {g}{n} xs x) → eim-f {g}{n} xs x
prediction-mutor x (just y) = y
prediction-mutor x nothing = x

predictions : ∀{g}{n}{xs} → List (Σ (EIM g n) (eim-f xs))
           → (y : ItemSet g n xs) → (ItemSet g n xs)
                                ⊎ (List (Σ (EIM g n) (eim-f xs)) × Σ (ItemSet g n xs) (λ(x) → (_<_ on ItemSet.remaining) x y))
predictions [] eims = inj₁ eims
predictions {g}{n}{xs} ((eim' , sppf) ∷ acu) eims with ItemSet.insert eim' (prediction-mutor {g}{n}{xs}{eim'} sppf) eims
predictions ((eim' , sppf) ∷ acu) eims | new-eims , inj₂ c = inj₂ (new-prediction eim' ++ acu , new-eims , c)
predictions ((eim' , sppf) ∷ acu) eims | new-eims , inj₁ eq rewrite eq = predictions acu new-eims

predict' : ∀{g}{n}{xs} → List (Σ (EIM g n) (eim-f xs))
           → (x : ItemSet g n xs) → Acc (_<_ on ItemSet.remaining) x → ItemSet g n xs
predict' acu eims (acc q) with predictions acu eims
predict' acu eims (acc q) | inj₂ (acu' , eims' , c) = predict' acu' eims' (q eims' c)
predict' acu eims (acc q) | inj₁ eims' = eims'

predict : ∀{g}{n}{xs} → List (Σ (EIM g n) (eim-f xs))
           → (x : ItemSet g n xs) → ItemSet g n xs
predict acu eims = predict' acu eims (ItemSet.remaining-wellFounded eims)

start-items : List (Σ (EIM g 0) (eim-f ε))
start-items {g} = ItemSet.to-list (predict (by-lhs (start g)) ItemSet.blank)

data EarleyTrail (g : Grammar) : (n : ℕ) → Trail (symbol g) → Set where
  empty : List (Σ (EIM g 0) (eim-f ε)) → EarleyTrail g 0 ε
  scanned : ∀{n t} → EarleyTrail g n t
          → {s : symbol g}
          → List (Σ (EIM g (suc n)) (eim-f (t ‣ s))) → EarleyTrail g (suc n) (t ‣ s)

everybody-knows-already : ∀{g n xs} → EarleyTrail g n xs → n ≡ Trail.length xs
everybody-knows-already (empty x) = refl
everybody-knows-already (scanned trail x) = cong suc (everybody-knows-already trail)

latest : ∀{g}{n}{t} → EarleyTrail g n t → List (Σ (EIM g n) (eim-f t))
latest (empty x) = x
latest (scanned _ x) = x

initial : EarleyTrail g 0 ε
initial = empty start-items

move-eim : ∀{g}{n} m → EIM g n → EIM g (m ℕ.+ n)
move-eim {g} {n} m (eim og ix) with m ↑ʳ og
move-eim {g} {n} m (eim og ix) | c = (eim (subst (Fin) (+-suc m n) c) ix)

move-ix-same : ∀{g}{n} m → (x : EIM g n) → EIM.ix (move-eim m x) ≡ (EIM.ix x)
move-ix-same m (eim og ix) = refl

foobar : ∀ {n m} v → (toℕ (subst Fin (+-suc m n) v)) ≡ toℕ v
foobar {n} {m} v rewrite +-suc m n = refl

select-lemma : ∀ {n} (m : ℕ) (og : Fin (suc n)) → (toℕ (m ↑ʳ og)) ≡ (toℕ og) ℕ.+ m
select-lemma {n} 0F og rewrite +-identityʳ (toℕ og) = refl
select-lemma {n} (suc m) og rewrite +-suc (toℕ og) m = cong suc (select-lemma m og)

trail-blank : ∀ {a : Set} n → Trail.take {a} n ε ≡ ε
trail-blank 0F = refl
trail-blank (suc n) = refl

trail-catenation : ∀ {a : Set} n m (zs : Trail a) → Trail.take n (Trail.drop m zs) Trail.++ Trail.take m zs  ≡ Trail.take (n ℕ.+ m) zs
trail-catenation n 0F zs rewrite +-identityʳ n = refl
trail-catenation n (suc m) ε rewrite +-suc n m = trail-blank n
trail-catenation n (suc m) (zs ‣ x) rewrite +-suc n m = cong (λ(xs) → xs ‣ x) (trail-catenation n m zs)

select : ∀ {g}{n m}{zs : Trail (symbol g)}{e} (s : symbol g) → SPPF g (Trail.take m zs) e → (ok1 : step e ≡ nothing)
                                                          → (ok2 : lhs g (Item.i e) ≡ s)
                                                          → List (Σ (EIM g n) (eim-f (Trail.drop m zs)))
                                                          → List (Σ (EIM g (m ℕ.+ n)) (eim-f zs))
select {g} {n} {m} s sp ok1 ok2 [] = []
select {g} {n} {m} s sp ok1 ok2 ((eim og ix , sppf) ∷ xs) with inspect (step ix)
select {g} {n} {m} s sp ok1 ok2 ((eim og ix , sppf) ∷ xs) | just (v , ix') with≡ q with symbol-eq g s v
select {g} {n} {m} s sp ok1 ok2 ((eim og ix , sppf) ∷ xs) | just (v , ix') with≡ q | Dec.yes refl rewrite sym ok2 = (move-eim m (eim og ix') , shift sppf sp (yelp og m) ok1 q) ∷ select s sp ok1 ok2 xs
  where yelp : ∀ {zs} og m → Trail.take (toℕ og) (Trail.drop m zs) Trail.++ Trail.take m zs ≡ Trail.take (toℕ (EIM.og (move-eim m (eim og ix')))) zs
        yelp {zs} og m rewrite trans (foobar (m ↑ʳ og)) (select-lemma m og) = trail-catenation (toℕ og) m zs
select {g} {n} {m} s sp ok1 ok2 ((eim og ix , sppf) ∷ xs) | just (v , ix') with≡ q | Dec.no ¬p = select s sp ok1 ok2 xs
select {g} {n} {m} s sp ok1 ok2 ((eim og ix , sppf) ∷ xs) | nothing with≡ q = select s sp ok1 ok2 xs

select₁ : ∀ {g}{n xs} (s : symbol g) → semantic g s
                                     → List (Σ (EIM g n) (eim-f xs))
                                     → List (Σ (EIM g (suc n)) (eim-f (xs ‣ s)))
select₁ s sem [] = []
select₁ s sem ((eim og ix , sppf) ∷ xs) with inspect (step ix)
select₁ {g} s sem ((eim og ix , sppf) ∷ xs) | just (v , ix') with≡ q with symbol-eq g s v
select₁ {g} s sem ((eim og ix , sppf) ∷ xs) | just (s , ix') with≡ q | Dec.yes refl = (move-eim 1 (eim og ix') , shift' sppf s sem q) ∷ select₁ s sem xs
select₁ {g} s sem ((eim og ix , sppf) ∷ xs) | just (v , ix') with≡ q | Dec.no ¬p = select₁ s sem xs
select₁ s sem ((eim og ix , sppf) ∷ xs) | nothing with≡ q = select₁ s sem xs

scroll : ∀{g} n m {zs} → EarleyTrail g (m ℕ.+ n) zs → List (Σ (EIM g n) (eim-f (Trail.drop m zs)))
scroll n 0F trail = latest trail
scroll n (suc m) (scanned trail _) = scroll n m trail

fin-lemma : ∀ {n} (i : Fin (suc n)) → Σ ℕ (λ(n') → n ≡ toℕ i ℕ.+ n')
fin-lemma {n} 0F = (n , refl)
fin-lemma {suc n} (suc i) = Data.Product.map₂ (cong suc) (fin-lemma i)

scan : ∀{g}{n t}{k}{e} → (i : Fin (suc n)) → (s : symbol g) → SPPF g (Trail.take (suc (toℕ i)) (t ‣ k)) e
           → (ok1 : step e ≡ nothing)
           → (ok2 : lhs g (Item.i e) ≡ s)
           → EarleyTrail g n t
           → List (Σ (EIM g (suc n)) (eim-f (t ‣ k)))
scan {g} {n} {t} {k} {e} i s sp ok1 ok2 tr with fin-lemma i
... | n' , p with select {e = e} s sp ok1 ok2 (scroll n' (toℕ i) (subst (λ(x) → EarleyTrail g x t) p tr))
... | result = subst (λ(x) → List (Σ (EIM g (suc x)) (eim-f (t ‣ k)))) (sym p) result

first-scan : ∀{g}{n}{t} → (s : symbol g) → semantic g s → EarleyTrail g n t → List (Σ (EIM g (suc n)) (eim-f (t ‣ s)))
first-scan s sem tr = select₁ s sem (latest tr)

new-scan : ∀{g}{n}{t}{s} → EarleyTrail g n t → (e : EIM g (suc n)) → SPPF g (Trail.take (toℕ (EIM.og e)) (t ‣ s)) (EIM.ix e) → List (Σ (EIM g (suc n)) (eim-f (t ‣ s)))
new-scan {g} trail (eim og ix) sp with inspect (step ix)
new-scan {g} trail (eim og ix) sp | just (sym , _) with≡ q = [] 
new-scan {g} {n} trail (eim 0F (item i x)) sp | nothing with≡ q = [] -- Empty reduction, invalid in this algorithm.
new-scan {g} {n} trail (eim (suc og) (item i x)) sp | nothing with≡ q = scan og (lhs g i) sp q refl trail

scanning-mutor : ∀{g}{n}{xs} {x} → eim-f {g}{n} xs x → Maybe (eim-f {g}{n} xs x) → eim-f {g}{n} xs x
scanning-mutor x (just y) = branch x y
scanning-mutor x nothing = x

scanning : ∀{g}{n}{t}{s} → EarleyTrail g n t → List (Σ (EIM g (suc n)) (eim-f (t ‣ s)))
                         → (y : ItemSet g (suc n) (t ‣ s))
                         → (ItemSet g (suc n) (t ‣ s))
                         ⊎ (List (Σ (EIM g (suc n)) (eim-f (t ‣ s))) × Σ (ItemSet g (suc n) (t ‣ s)) (λ(x) → (_<_ on ItemSet.remaining) x y))
scanning tr [] eims = inj₁ eims
scanning {g}{n}{t}{s} tr ((eim' , sp) ∷ acu) eims with ItemSet.insert eim' (scanning-mutor {g}{suc n}{t ‣ s}{eim'} sp) eims
scanning tr ((eim' , sp) ∷ acu) eims | new-eims , inj₂ c = inj₂ (new-scan tr eim' sp Data.List.++ acu , new-eims , c)
scanning tr ((eim' , sp) ∷ acu) eims | new-eims , inj₁ eq rewrite eq = scanning tr acu new-eims

full-scan' : ∀{g}{n}{t}{s} → EarleyTrail g n t → List (Σ (EIM g (suc n)) (eim-f (t ‣ s)))
          → (x : ItemSet g (suc n) (t ‣ s)) → Acc (_<_ on ItemSet.remaining) x → ItemSet g (suc n) (t ‣ s)
full-scan' tr acu eims (acc q) with scanning tr acu eims
full-scan' tr acu eims (acc q) | inj₂ (acu' , eims' , c) = full-scan' tr acu' eims' (q eims' c)
full-scan' tr acu eims (acc q) | inj₁ eims' = eims'

full-scan : ∀{g}{n}{t}{s} → EarleyTrail g n t → List (Σ (EIM g (suc n)) (eim-f (t ‣ s)))
          → (x : ItemSet g (suc n) (t ‣ s)) → ItemSet g (suc n) (t ‣ s)
full-scan tr acu eims = full-scan' tr acu eims (ItemSet.remaining-wellFounded eims)

earley-step : ∀{g}{n}{t} → (s : symbol g) → semantic g s → EarleyTrail g n t → EarleyTrail g (suc n) (t ‣ s)
earley-step {_}{n} s sem tr = scanned tr tr''
  where tr' = ItemSet.to-list (full-scan tr (first-scan s sem tr) ItemSet.blank)
        tr'' = ItemSet.to-list (predict tr' ItemSet.blank)

parse : ∀ g (xs : Trail (Σ (symbol g) (semantic g))) → EarleyTrail g (Trail.length xs) (Trail.map proj₁ xs)
parse g ε = initial {g}
parse g (xs ‣ (s , sem)) = earley-step s sem (parse g xs)

flatten : ∀ {a : Set}{F : a → Set} → Σ a (List ∘ F) → List (Σ a F)
flatten (x , xs) = Data.List.map (λ(y) → (x , y)) xs

concat+ : ∀ {a : Set}{F : a → Set} → List (Σ a (List ∘ F)) → List (Σ a F)
concat+ [] = []
concat+ (x ∷ xs) = flatten x ++ concat+ xs

trail-to-spf : ∀ {g}{n}{tr} → List (Σ (EIM g n) (eim-f tr)) → List (Σ (EIM g n) (List ∘ spf-f tr))
trail-to-spf {g}{n}{tr} = Data.List.map (Data.Product.map id SPPF-to-list)

flat-spf : ∀ {g}{n}{tr} → List (Σ (EIM g n) (eim-f tr)) → List (Σ (EIM g n) (spf-f tr))
flat-spf = concat+ ∘ trail-to-spf

filter-accepted : ∀ {g}{n}{F : EIM g n → Set} → List (Σ (EIM g n) F) → List (Σ (EIM g n) (λ(x) → (Accepted g n x) × (F x)))
filter-accepted [] = []
filter-accepted ((ei , a) ∷ xs) with dec-accepted ei
... | Dec.yes p = (ei , (p , a)) ∷ filter-accepted xs
... | Dec.no ¬p = filter-accepted xs

get-semantic : ∀{g}{n}{xs} → List (Σ (EIM g n) (λ(x) → (Accepted g n x) × (spf-f xs x))) → List (semantic g (start g))
get-semantic ys = Data.List.map fub ys
  where fub : ∀{g}{n}{xs} → Σ (EIM g n) (λ(x) → (Accepted g n x) × (spf-f xs x)) → semantic g (start g)
        fub {g} (ei , (f , g' , h) , spf) = subst (λ(x) → semantic g x) g' (SPF-to-semantic h spf) 

accepted : ∀{g}{n}{xs} → EarleyTrail g n xs → List (semantic g (start g))
accepted = get-semantic ∘ filter-accepted ∘ flat-spf ∘ latest

trail-yoga : ∀{a : Set} (xs : Trail a) → Trail.take (Trail.length xs) xs ≡ xs
trail-yoga ε = refl
trail-yoga (xs ‣ x) = cong (λ(xs) → xs ‣ x) (trail-yoga xs)

its-complete : ∀{g} (xs : Trail (Σ (symbol g) (semantic g)))
                    (ei : EIM g (Trail.length xs))
                    (a : Accepted g (Trail.length xs) ei)
                    (spf : SPF g (Trail.take (toℕ (EIM.og ei)) (Trail.map proj₁ xs)) (EIM.ix ei))
                    → (ei , spf) ∈ flat-spf (latest (parse g xs))
its-complete ε ei (p , q , r) spf = {!!}
its-complete (xs ‣ x) ei (p , q , r) spf = {!!}

-------------------------------------------------------------------------------
-- 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 ()
semantic sample1 S = ℕ
semantic sample1 A = ⊤
semantic sample1 hello = ⊤
semantic sample1 something = ⊤
reducer sample1 0F (cons tt (cons tt empty)) = 15
reducer sample1 1F (cons tt empty) = tt
reducer sample1 2F (cons tt (cons x empty)) = tt

ex3 : EarleyTrail sample1 0 ε
ex3 = initial

ex4 : EarleyTrail sample1 1 (ε ‣ hello)
ex4 = earley-step hello tt ex3

ex5 : EarleyTrail sample1 2 (ε ‣ hello ‣ something)
ex5 = earley-step something tt ex4

ex7 : List (semantic sample1 (start sample1))
ex7 = accepted ex5

Trail.agda

module Trail where

open import Data.List using (List; _∷_; [])
open import Data.Nat using (ℕ; zero; suc)

infixl 4 _‣_
data Trail (a : Set) : Set where
  ε : Trail a
  _‣_ : Trail a → a → Trail a

variable
  a : Set
  b : Set

to-list' : Trail a → List a → List a
to-list' ε ys = ys
to-list' (xs ‣ x) ys = to-list' xs (x ∷ ys)

to-list : Trail a → List a
to-list xs = to-list' xs []

infixl 20 _++_
_++_ : Trail a → Trail a → Trail a
_++_ xs ε = xs
_++_ xs (ys ‣ x) = (xs ++ ys) ‣ x

length : Trail a → ℕ
length ε = zero
length (xs ‣ _) = suc (length xs)

map : (a → b) → Trail a → Trail b
map f ε = ε
map f (xs ‣ x) = map f xs ‣ f x

take : ℕ → Trail a → Trail a
take zero _ = ε
take (suc n) ε = ε
take (suc n) (xs ‣ x) = take n xs ‣ x

drop : ℕ → Trail a → Trail a
drop zero xs = xs
drop (suc n) ε = ε
drop (suc n) (xs ‣ x) = drop n xs