Examples.lean

import FPRDTransfer.PEG.Syntax
import FPRDTransfer.PEG.Semantics

namespace FPRD
namespace PEGExamples

def rejecting : Grammar Bool Bool where
  start := false
  rule _ := .fail

example : Eval rejecting (.term true) [true, false] (.ok [false]) := by
  exact .termOk

example : Eval rejecting (.term true) [false] .err := by
  exact .termNe (by decide)

example : Eval rejecting (.alt .eps (.term true)) [true] (.ok [true]) := by
  exact .altOk .eps

example : Eval rejecting (.notP (.term true)) [false] (.ok [false]) := by
  exact .notErr (.termNe (by decide))

example : Eval rejecting (.pos (.term true)) [true, false] (.ok [true, false]) := by
  exact .notErr (.notOk .termOk)

example : Eval rejecting (.pos (.term true)) [false] .err := by
  exact .notOk (.notErr (.termNe (by decide)))

example : Eval rejecting (.notP .any) [] (.ok []) := by
  exact (notAny_iff_nil rejecting [] []).mpr ⟨rfl, rfl⟩

inductive StarNT where
  | star
  deriving DecidableEq

def starGrammar : Grammar StarNT Bool where
  start := .star
  rule _ := .alt (.seq .any (.nonterm .star)) .eps

theorem star_rule :
    starGrammar.rule .star = .alt (.seq .any (.nonterm .star)) .eps := rfl

example (word : List Bool) :
    Eval starGrammar (.nonterm .star) word (.ok []) := by
  exact anyStar_ok starGrammar .star star_rule word

example (word rest : List Bool) :
    Eval starGrammar (.nonterm .star) word (.ok rest) ↔ rest = [] := by
  exact anyStar_ok_iff starGrammar .star star_rule word rest

def singletonTrue : Grammar Bool Bool where
  start := false
  rule
    | false => .term true
    | true => .fail

theorem singletonTrue_recognizes :
    Recognizes singletonTrue (fun word => word = [true]) := by
  intro word
  rw [eval_nonterm_iff]
  simp only [singletonTrue]
  exact (term_ok_nil_iff singletonTrue true word).symm

def boolEquivFin := FiniteEnum.equivFin Bool

example (expr : Expr Bool Bool) (word : List Bool) (result : Result Bool) :
    Eval (transportGrammar boolEquivFin singletonTrue)
        (transportExpr boolEquivFin expr) word result ↔
      Eval singletonTrue expr word result := by
  exact eval_transport_iff boolEquivFin singletonTrue expr word result

example : FiniteGrammar Bool Bool where
  alphabet := inferInstance
  nonterminals := inferInstance
  grammar := singletonTrue

end PEGExamples
end FPRD