Syntax.lean

import FPRDTransfer.FiniteEnum

namespace FPRD

universe uNT uNT' uSym

/-- Ordinary parsing expressions with ordered choice and negative lookahead. -/
inductive Expr (NT : Type uNT) (Sym : Type uSym) where
  | eps
  | fail
  | any
  | term (symbol : Sym)
  | nonterm (name : NT)
  | seq (left right : Expr NT Sym)
  | alt (left right : Expr NT Sym)
  | notP (body : Expr NT Sym)

namespace Expr

/-- Positive lookahead is double negative lookahead and is not primitive. -/
def pos (body : Expr NT Sym) : Expr NT Sym := .notP (.notP body)

/-- A finite sequence; the empty sequence is epsilon. -/
def seqAll : List (Expr NT Sym) → Expr NT Sym :=
  List.foldr .seq .eps

/-- A finite ordered choice; no alternatives means failure, never epsilon. -/
def altAll : List (Expr NT Sym) → Expr NT Sym :=
  List.foldr .alt .fail

/-- Ordered alternatives for the terminals in an executable alphabet list. -/
def termAlt (symbols : List Sym) : Expr NT Sym :=
  altAll (symbols.map .term)

end Expr

/-- A parsing-expression grammar with one start nonterminal. -/
structure Grammar (NT : Type uNT) (Sym : Type uSym) where
  start : NT
  rule : NT → Expr NT Sym

theorem Grammar.ext {G H : Grammar NT Sym}
    (start_eq : G.start = H.start) (rule_eq : G.rule = H.rule) : G = H := by
  cases G
  cases H
  simp_all

/-- A grammar bundled with exhaustive alphabet and nonterminal enumerations. -/
structure FiniteGrammar (Sym : Type uSym) (NT : Type uNT) where
  alphabet : FiniteEnum Sym
  nonterminals : FiniteEnum NT
  grammar : Grammar NT Sym

/-- Rename every nonterminal occurring in an expression. -/
def transportExpr (e : FiniteEquiv NT NT') : Expr NT Sym → Expr NT' Sym
  | .eps => .eps
  | .fail => .fail
  | .any => .any
  | .term symbol => .term symbol
  | .nonterm name => .nonterm (e name)
  | .seq left right => .seq (transportExpr e left) (transportExpr e right)
  | .alt left right => .alt (transportExpr e left) (transportExpr e right)
  | .notP body => .notP (transportExpr e body)

@[simp] theorem transportExpr_symm_apply
    (e : FiniteEquiv NT NT') (expr : Expr NT Sym) :
    transportExpr e.symm (transportExpr e expr) = expr := by
  induction expr <;> simp_all [transportExpr]

@[simp] theorem transportExpr_apply_symm
    (e : FiniteEquiv NT NT') (expr : Expr NT' Sym) :
    transportExpr e (transportExpr e.symm expr) = expr := by
  induction expr <;> simp_all [transportExpr]

/-- Rename a grammar along a proved nonterminal equivalence. -/
def transportGrammar (e : FiniteEquiv NT NT') (G : Grammar NT Sym) :
    Grammar NT' Sym where
  start := e G.start
  rule name := transportExpr e (G.rule (e.symm name))

@[simp] theorem transportGrammar_start
    (e : FiniteEquiv NT NT') (G : Grammar NT Sym) :
    (transportGrammar e G).start = e G.start := rfl

@[simp] theorem transportGrammar_rule_apply
    (e : FiniteEquiv NT NT') (G : Grammar NT Sym) (name : NT) :
    (transportGrammar e G).rule (e name) = transportExpr e (G.rule name) := by
  simp [transportGrammar]

@[simp] theorem transportGrammar_symm_apply
    (e : FiniteEquiv NT NT') (G : Grammar NT Sym) :
    transportGrammar e.symm (transportGrammar e G) = G := by
  cases G with
  | mk start rule =>
      apply Grammar.ext
      · simp [transportGrammar]
      · funext name
        simp [transportGrammar]

@[simp] theorem transportGrammar_apply_symm
    (e : FiniteEquiv NT NT') (G : Grammar NT' Sym) :
    transportGrammar e (transportGrammar e.symm G) = G := by
  cases G with
  | mk start rule =>
      apply Grammar.ext
      · simp [transportGrammar]
      · funext name
        simp [transportGrammar]

/-- Transport both the grammar and its exhaustive nonterminal enumeration. -/
def transportFiniteGrammar (e : FiniteEquiv NT NT')
    (G : FiniteGrammar Sym NT) : FiniteGrammar Sym NT' where
  alphabet := G.alphabet
  nonterminals := FiniteEnum.ofEquiv G.nonterminals e
  grammar := transportGrammar e G.grammar

end FPRD