Semantics.lean

import FPRDTransfer.PEG.Syntax

namespace FPRD

universe uNT uNT' uSym

/-- A PEG either rejects or succeeds with one exact unconsumed suffix. -/
inductive Result (Sym : Type uSym) where
  | ok (rest : List Sym)
  | err
  deriving DecidableEq

/-- The theorem-bearing relational semantics of ordinary ordered-choice PEGs. -/
inductive Eval (G : Grammar NT Sym) :
    Expr NT Sym → List Sym → Result Sym → Prop where
  | eps : Eval G .eps input (.ok input)
  | fail : Eval G .fail input .err
  | anyOk : Eval G .any (symbol :: rest) (.ok rest)
  | anyNil : Eval G .any [] .err
  | termOk : Eval G (.term symbol) (symbol :: rest) (.ok rest)
  | termNe : left ≠ right → Eval G (.term left) (right :: rest) .err
  | termNil : Eval G (.term symbol) [] .err
  | nonterm : Eval G (G.rule name) input result →
      Eval G (.nonterm name) input result
  | seqOk : Eval G left input (.ok middle) → Eval G right middle result →
      Eval G (.seq left right) input result
  | seqErr : Eval G left input .err → Eval G (.seq left right) input .err
  | altOk : Eval G left input (.ok rest) →
      Eval G (.alt left right) input (.ok rest)
  | altErr : Eval G left input .err → Eval G right input result →
      Eval G (.alt left right) input result
  | notOk : Eval G body input (.ok rest) → Eval G (.notP body) input .err
  | notErr : Eval G body input .err → Eval G (.notP body) input (.ok input)

/-- Relational evaluation, including recursive nonterminals, has one result. -/
theorem eval_deterministic {G : Grammar NT Sym} {expr : Expr NT Sym}
    {input : List Sym} {left right : Result Sym}
    (hleft : Eval G expr input left) (hright : Eval G expr input right) :
    left = right := by
  induction hleft generalizing right with
  | eps => cases hright; rfl
  | fail => cases hright; rfl
  | anyOk => cases hright; rfl
  | anyNil => cases hright; rfl
  | termOk =>
      cases hright with
      | termOk => rfl
      | termNe hne => exact (hne rfl).elim
  | termNe hne =>
      cases hright with
      | termOk => exact (hne rfl).elim
      | termNe _ => rfl
  | termNil => cases hright; rfl
  | nonterm _ ih =>
      cases hright with
      | nonterm hright => exact ih hright
  | seqOk _ _ ihLeft ihRight =>
      cases hright with
      | seqOk hLeft hRight =>
          have middle_eq := ihLeft hLeft
          cases middle_eq
          exact ihRight hRight
      | seqErr hLeft =>
          have impossible := ihLeft hLeft
          cases impossible
  | seqErr _ ihLeft =>
      cases hright with
      | seqOk hLeft _ =>
          have impossible := ihLeft hLeft
          cases impossible
      | seqErr _ => rfl
  | altOk _ ihLeft =>
      cases hright with
      | altOk hLeft => exact ihLeft hLeft
      | altErr hLeft _ =>
          have impossible := ihLeft hLeft
          cases impossible
  | altErr _ _ ihLeft ihRight =>
      cases hright with
      | altOk hLeft =>
          have impossible := ihLeft hLeft
          cases impossible
      | altErr _ hRight => exact ihRight hRight
  | notOk _ ihBody =>
      cases hright with
      | notOk _ => rfl
      | notErr hBody =>
          have impossible := ihBody hBody
          cases impossible
  | notErr _ ihBody =>
      cases hright with
      | notOk hBody =>
          have impossible := ihBody hBody
          cases impossible
      | notErr _ => rfl

theorem eval_nonterm_iff (G : Grammar NT Sym) (name : NT)
    (input : List Sym) (result : Result Sym) :
    Eval G (.nonterm name) input result ↔ Eval G (G.rule name) input result := by
  constructor
  · intro h
    cases h with
    | nonterm h => exact h
  · exact Eval.nonterm

theorem term_ok_iff (G : Grammar NT Sym) (symbol : Sym)
    (input rest : List Sym) :
    Eval G (.term symbol) input (.ok rest) ↔ input = symbol :: rest := by
  constructor
  · intro h
    cases h
    rfl
  · intro h
    subst input
    exact .termOk

theorem term_ok_nil_iff (G : Grammar NT Sym) (symbol : Sym)
    (input : List Sym) :
    Eval G (.term symbol) input (.ok []) ↔ input = [symbol] :=
  term_ok_iff G symbol input []

/-- Every expression and input has a relational result.  This is a property of
a grammar, not an assumption built into `Eval`. -/
def Total (G : Grammar NT Sym) : Prop :=
  ∀ expr input, ∃ result, Eval G expr input result

/-- Complete-match recognition requires the start rule to consume all input. -/
def Recognizes (G : Grammar NT Sym) (language : List Sym → Prop) : Prop :=
  ∀ input, language input ↔ Eval G (.nonterm G.start) input (.ok [])

/-- Membership in PEG uses a literal finite `Fin n` nonterminal carrier. -/
def InPEG [DecidableEq Sym] (language : List Sym → Prop) : Prop :=
  ∃ (n : Nat) (G : FiniteGrammar Sym (Fin n)),
    Total G.grammar ∧ Recognizes G.grammar language

/-- Rename an evaluation derivation along a nonterminal equivalence. -/
theorem eval_transport (e : FiniteEquiv NT NT') (G : Grammar NT Sym)
    {expr : Expr NT Sym} {input : List Sym} {result : Result Sym}
    (h : Eval G expr input result) :
    Eval (transportGrammar e G) (transportExpr e expr) input result := by
  induction h with
  | eps => exact .eps
  | fail => exact .fail
  | anyOk => exact .anyOk
  | anyNil => exact .anyNil
  | termOk => exact .termOk
  | termNe hne => exact .termNe hne
  | termNil => exact .termNil
  | nonterm _ ih =>
      apply Eval.nonterm
      simpa using ih
  | seqOk _ _ ihLeft ihRight => exact .seqOk ihLeft ihRight
  | seqErr _ ih => exact .seqErr ih
  | altOk _ ih => exact .altOk ih
  | altErr _ _ ihLeft ihRight => exact .altErr ihLeft ihRight
  | notOk _ ih => exact .notOk ih
  | notErr _ ih => exact .notErr ih

theorem eval_transport_iff (e : FiniteEquiv NT NT') (G : Grammar NT Sym)
    (expr : Expr NT Sym) (input : List Sym) (result : Result Sym) :
    Eval (transportGrammar e G) (transportExpr e expr) input result ↔
      Eval G expr input result := by
  constructor
  · intro h
    simpa using eval_transport e.symm (transportGrammar e G) h
  · exact eval_transport e G

theorem total_transport_iff (e : FiniteEquiv NT NT') (G : Grammar NT Sym) :
    Total (transportGrammar e G) ↔ Total G := by
  constructor
  · intro h expr input
    obtain ⟨result, hresult⟩ := h (transportExpr e expr) input
    exact ⟨result, (eval_transport_iff e G expr input result).mp hresult⟩
  · intro h expr input
    obtain ⟨result, hresult⟩ := h (transportExpr e.symm expr) input
    refine ⟨result, ?_⟩
    simpa using eval_transport e G hresult

theorem recognizes_transport_iff (e : FiniteEquiv NT NT')
    (G : Grammar NT Sym) (language : List Sym → Prop) :
    Recognizes (transportGrammar e G) language ↔ Recognizes G language := by
  constructor
  · intro h input
    exact (h input).trans
      (eval_transport_iff e G (.nonterm G.start) input (.ok []))
  · intro h input
    exact (h input).trans
      (eval_transport_iff e G (.nonterm G.start) input (.ok [])).symm

/-- Two expressions with the same canonical result accept exactly the same
result at that input, by determinism. -/
theorem eval_iff_of_shared_result {G : Grammar NT Sym}
    {left right : Expr NT Sym} {input : List Sym} {canonical result : Result Sym}
    (hleft : Eval G left input canonical) (hright : Eval G right input canonical) :
    Eval G left input result ↔ Eval G right input result := by
  constructor
  · intro h
    have result_eq := eval_deterministic h hleft
    cases result_eq
    exact hright
  · intro h
    have result_eq := eval_deterministic h hright
    cases result_eq
    exact hleft

/-- Negative lookahead for `any` succeeds exactly at end of input. -/
theorem notAny_iff_nil (G : Grammar NT Sym) (input rest : List Sym) :
    Eval G (.notP .any) input (.ok rest) ↔ input = [] ∧ rest = [] := by
  constructor
  · intro h
    cases input with
    | nil =>
        cases h with
        | notErr _ => exact ⟨rfl, rfl⟩
    | cons symbol tail =>
        cases h with
        | notErr hAny => cases hAny
  · rintro ⟨rfl, rfl⟩
    exact .notErr .anyNil

theorem termAlt_ok_of_mem (G : Grammar NT Sym) {symbol : Sym}
    {symbols : List Sym} {rest : List Sym} (hmem : symbol ∈ symbols) :
    Eval G (Expr.termAlt symbols) (symbol :: rest) (.ok rest) := by
  induction symbols with
  | nil => simp at hmem
  | cons head tail ih =>
      change Eval G (.alt (.term head) (Expr.termAlt tail))
        (symbol :: rest) (.ok rest)
      by_cases hhead : head = symbol
      · subst head
        exact .altOk .termOk
      · have htail : symbol ∈ tail :=
          (List.mem_cons.mp hmem).resolve_left (Ne.symm hhead)
        exact .altErr (.termNe hhead) (ih htail)

theorem termAlt_nil_err (G : Grammar NT Sym) (symbols : List Sym) :
    Eval G (Expr.termAlt symbols) [] .err := by
  induction symbols with
  | nil => exact .fail
  | cons head tail ih =>
      exact .altErr .termNil ih

/-- For an exhaustive symbol list, looking past every terminal is exactly the
ordinary end-of-input predicate `!any`. -/
theorem notAlt_enum_iff_notAny (G : Grammar NT Sym) (symbols : List Sym)
    (complete : ∀ symbol, symbol ∈ symbols) (input : List Sym)
    (result : Result Sym) :
    Eval G (.notP (Expr.termAlt symbols)) input result ↔
      Eval G (.notP .any) input result := by
  cases input with
  | nil =>
      exact eval_iff_of_shared_result
        (.notErr (termAlt_nil_err G symbols)) (.notErr .anyNil)
  | cons symbol rest =>
      exact eval_iff_of_shared_result
        (.notOk (termAlt_ok_of_mem G (complete symbol))) (.notOk .anyOk)

/-- The guarded rule `any A / eps` consumes every finite input. -/
theorem anyStar_ok (G : Grammar NT Sym) (name : NT)
    (rule_eq : G.rule name = .alt (.seq .any (.nonterm name)) .eps)
    (input : List Sym) : Eval G (.nonterm name) input (.ok []) := by
  induction input with
  | nil =>
      apply Eval.nonterm
      rw [rule_eq]
      exact .altErr (.seqErr .anyNil) .eps
  | cons symbol rest ih =>
      apply Eval.nonterm
      rw [rule_eq]
      exact .altOk (.seqOk .anyOk ih)

theorem anyStar_ok_iff (G : Grammar NT Sym) (name : NT)
    (rule_eq : G.rule name = .alt (.seq .any (.nonterm name)) .eps)
    (input rest : List Sym) :
    Eval G (.nonterm name) input (.ok rest) ↔ rest = [] := by
  constructor
  · intro h
    have result_eq := eval_deterministic h (anyStar_ok G name rule_eq input)
    cases result_eq
    rfl
  · intro h
    subst rest
    exact anyStar_ok G name rule_eq input

end FPRD