TableEvalExamples.lean

import FPRDTransfer.PEG.TableEval

namespace FPRD
namespace TableEvalExamples

def anyStarGrammar : Grammar (Fin 1) Bool where
  start := 0
  rule _ := .alt (.seq .any (.nonterm 0)) .eps

def singletonGrammar : Grammar (Fin 1) Bool where
  start := 0
  rule _ := .term true

def starSchedule : RankSchedule anyStarGrammar where
  order := [0]
  nodup := by simp
  complete name := by
    have hval : name.val = 0 := by omega
    have hname : name = 0 := by apply Fin.ext; exact hval
    subst name
    simp
  earlier := by
    intro before after caller callee horder hcall
    simp [anyStarGrammar, Expr.samePositionCalls, Expr.guaranteedConsumes] at hcall

def singletonSchedule : RankSchedule singletonGrammar where
  order := [0]
  nodup := by simp
  complete name := by
    have hval : name.val = 0 := by omega
    have hname : name = 0 := by apply Fin.ext; exact hval
    subst name
    simp
  earlier := by
    intro before after caller callee horder hcall
    simp [singletonGrammar, Expr.samePositionCalls] at hcall

example (word : List Bool) :
    evalTable anyStarGrammar starSchedule word = .ok [] := by
  apply evalTable_eq_of_eval
  exact anyStar_ok anyStarGrammar 0 rfl word

example :
    evalTable singletonGrammar singletonSchedule [true, false] = .ok [false] := by
  apply evalTable_eq_of_eval
  exact .nonterm .termOk

example : evalTable singletonGrammar singletonSchedule [false] = .err := by
  apply evalTable_eq_of_eval
  exact .nonterm (.termNe (by decide))

def lowerRankGrammar : Grammar (Fin 2) Bool where
  start := 1
  rule
    | 0 => .eps
    | 1 => .nonterm 0

def lowerRankSchedule : RankSchedule lowerRankGrammar where
  order := [0, 1]
  nodup := by decide
  complete name := by
    have hval : name.val = 0 ∨ name.val = 1 := by omega
    rcases hval with h | h
    · have : name = 0 := by apply Fin.ext; simpa using h
      subst name
      simp
    · have : name = 1 := by apply Fin.ext; simpa using h
      subst name
      simp
  earlier := by
    intro before after caller callee horder hcall
    have hcaller : caller = 0 ∨ caller = 1 := by
      have hval : caller.val = 0 ∨ caller.val = 1 := by omega
      rcases hval with h | h
      · left; apply Fin.ext; simpa using h
      · right; apply Fin.ext; simpa using h
    rcases hcaller with rfl | rfl
    · simp [lowerRankGrammar, Expr.samePositionCalls] at hcall
    · have hcallee : callee = 0 := by
        simpa [lowerRankGrammar, Expr.samePositionCalls] using hcall
      subst callee
      cases before with
      | nil => simp at horder
      | cons head tail =>
          have hhead : head = 0 := by injection horder with h; exact h.symm
          subst head
          simp

example (word : List Bool) :
    evalTable lowerRankGrammar lowerRankSchedule word = .ok word := by
  apply evalTable_eq_of_eval
  exact .nonterm (.nonterm .eps)

def malformedGrammar : Grammar (Fin 1) Bool where
  start := 0
  rule _ := .nonterm 0

example : RankSchedule malformedGrammar → False := by
  exact no_self_schedule malformedGrammar 0 rfl

example (word : List Bool) :
    Eval anyStarGrammar (.nonterm anyStarGrammar.start) word
      (evalTable anyStarGrammar starSchedule word) :=
  evalTable_sound anyStarGrammar starSchedule word

example : evalTable anyStarGrammar starSchedule [true, false, true] = .ok [] :=
  by decide

example : evalTable singletonGrammar singletonSchedule [true, false] =
    .ok [false] := by decide

example : evalTable singletonGrammar singletonSchedule [false] = .err :=
  by decide

end TableEvalExamples
end FPRD