remove generic Pred parameter from Grammar

Author: awalterschulze

Validator/Derive/Enter.lean

@@ -7,7 +7,7 @@ import Validator.Expr.Symbol
 
 namespace Enter
 
-def deriveEnter (xs: Rules n α Pred l): IfExprs n α (Symbol.nums xs) :=
+def deriveEnter (xs: Rules n (Pred α) l): IfExprs n α (Symbol.nums xs) :=
   List.Vector.map
     (fun (pred, ref) => IfExpr.mk pred ref)
     (Symbol.Symbols.cast
@@ -16,7 +16,7 @@ def deriveEnter (xs: Rules n α Pred l): IfExprs n α (Symbol.nums xs) :=
     )
 
 class DeriveEnter (m: Type -> Type u) (n: Nat) (α: outParam Type) where
-  deriveEnter {l: Nat} (xs: Rules n α Pred l): m (IfExprs n α (Symbol.nums xs))
+  deriveEnter {l: Nat} (xs: Rules n (Pred α) l): m (IfExprs n α (Symbol.nums xs))
 
-def deriveEnter_list (xs: List (Rule n α Pred)): List (IfExpr n α) :=
+def deriveEnter_list (xs: List (Rule n (Pred α))): List (IfExpr n α) :=
   List.map (fun (pred, ref) => IfExpr.mk pred ref) (Symbol.extracts_list xs []).2

Validator/Derive/Leave.lean

@@ -5,7 +5,7 @@ import Validator.Derive.Enter
 
 namespace Leave
 
-def leave (x: Regex (Fin l)) (es: Symbol.Symbols (Pred α × Ref n) l) (ns: List.Vector Bool l): (Rule n α Pred) :=
+def leave (x: Regex (Fin l)) (es: Symbol.Symbols (Pred α × Ref n) l) (ns: List.Vector Bool l): (Rule n (Pred α)) :=
   match x with
   | Regex.emptyset => Regex.emptyset
   | Regex.emptystr => Regex.emptyset
@@ -31,7 +31,7 @@ def deriveLeave
   (xs: List.Vector (Regex (Fin l1)) l2)
   (es: Symbol.Symbols (Pred α × Ref n) l1)
   (ns: List.Vector Bool l1)
-  : (Rules n α Pred l2) :=
+  : (Rules n (Pred α) l2) :=
   match xs with
   | ⟨[], h⟩ => ⟨[], h⟩
   | ⟨x::xs, h⟩ =>
@@ -46,14 +46,14 @@ def deriveLeave
       )
 
 def deriveLeaves
-  (xs: Rules n α Pred l)
+  (xs: Rules n (Pred α) l)
   (ns: List.Vector Bool (Symbol.nums xs))
-  : (Rules n α Pred l) :=
+  : (Rules n (Pred α) l) :=
   let (regexes, symbols) := Symbol.extracts xs List.Vector.nil
   deriveLeave regexes symbols (Symbol.Symbols.cast ns (by simp only [zero_add]))
 
-def deriveLeaveM [Monad m] {n: Nat} {l: Nat} (xs: Rules n α Pred l) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules n α Pred l) := do
+def deriveLeaveM [Monad m] {n: Nat} {l: Nat} (xs: Rules n (Pred α) l) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules n (Pred α) l) := do
   return deriveLeaves xs ns
 
 class DeriveLeaveM (m: Type -> Type u) (n: Nat) (α: outParam Type) where
-  deriveLeaveM {l: Nat} (xs: Rules n α Pred l) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules n α Pred l)
+  deriveLeaveM {l: Nat} (xs: Rules n (Pred α) l) (ns: List.Vector Bool (Symbol.nums xs)): m (Rules n (Pred α) l)

Validator/Expr/Compress.lean

@@ -133,16 +133,16 @@ def vector_cast (h: n = m) (xs: List.Vector α n): List.Vector α m := by
   subst h
   exact xs
 
-def compress [DecidableEq α] (xs: Rules n α Pred l1): Σ l2, ((Rules n α Pred l2) × (Indices l2 l1)) :=
-  let xs_list: List (Rule n α Pred) := xs.toList
+def compress [DecidableEq α] (xs: Rules n (Pred α) l1): Σ l2, ((Rules n (Pred α) l2) × (Indices l2 l1)) :=
+  let xs_list: List (Rule n (Pred α)) := xs.toList
   have hn : xs_list.length = l1 := by
     simp_all only [List.Vector.toList_length, xs_list]
 
   -- sort to increase chance of cache hit
   -- TODO: let sxs := List.mergeSort xs
 
   -- remove duplicates
-  let xs_noreps: { ys: List (Rule n α Pred) // ∀ x ∈ xs_list, x ∈ ys } := eraseReps_sub xs_list
+  let xs_noreps: { ys: List (Rule n (Pred α)) // ∀ x ∈ xs_list, x ∈ ys } := eraseReps_sub xs_list
 
   -- get indices
   let xs_idxs: List.Vector (Fin (xs_noreps.val).length) (List.length xs_list) := indices xs_noreps
@@ -228,10 +228,10 @@ def indexOf [DecidableEq α] (xs: List.Vector (Regex α) l) (y: Regex α) (h: y
   then Index.emptyset
   else Index.val (indexOf' xs y (memVector_emptyset h hy))
 
-def ofIndex' (xs: Rules n α Pred l) (index: Fin l): Rule n α Pred :=
+def ofIndex' (xs: Rules n (Pred α) l) (index: Fin l): Rule n (Pred α) :=
   xs.get index
 
-def ofIndex (xs: Rules n α Pred l) (index: Index l): Rule n α Pred :=
+def ofIndex (xs: Rules n (Pred α) l) (index: Index l): Rule n (Pred α) :=
   match index with
   | Index.emptyset => Regex.emptyset
   | Index.val n => ofIndex' xs n
@@ -436,12 +436,12 @@ def smallest [DecidableEq α] [LT α] [DecidableLT α] (xs: List.Vector α l) (y
 --       | Option.some dup => sorry
 --     | Option.some i => sorry
 
-def compressM [DecidableEq α] [Monad m] (xs: Rules n α Pred l1): m (Σ l2, (Rules n α Pred l2) × Indices l2 l1) := do
+def compressM [DecidableEq α] [Monad m] (xs: Rules n (Pred α) l1): m (Σ l2, (Rules n (Pred α) l2) × Indices l2 l1) := do
   return compress xs
 
 -- expand expands a list of expressions.
-def expand (indices: Indices l1 l2) (xs: Rules n α Pred l1): (Rules n α Pred l2) :=
+def expand (indices: Indices l1 l2) (xs: Rules n (Pred α) l1): (Rules n (Pred α) l2) :=
   List.Vector.map (ofIndex xs) indices
 
-def expandM [Monad m] (indices: Indices l1 l2) (xs: Rules n α Pred l1): m (Rules n α Pred l2) :=
+def expandM [Monad m] (indices: Indices l1 l2) (xs: Rules n (Pred α) l1): m (Rules n (Pred α) l2) :=
   return (expand indices xs)

Validator/Expr/Grammar.lean

@@ -16,42 +16,42 @@ import Validator.Expr.Language
 -- n = the number of non-terminals
 abbrev Ref (n: Nat) := Fin n -- non-terminal
 
-abbrev Rule (n: Nat) (α: Type) (Φ: (α: Type) -> Type) :=
-  Regex (Φ α × Ref n)
+abbrev Rule (n: Nat) (Φ: Type) :=
+  Regex (Φ × Ref n)
 
-abbrev Rules (n: Nat) (α: Type) (Φ: (α: Type) -> Type) (l: Nat) :=
-  List.Vector (Rule n α Φ) l
+abbrev Rules (n: Nat) (Φ: Type) (l: Nat) :=
+  List.Vector (Rule n Φ) l
 
 def hashVector [Hashable α] (xs: List.Vector α n): UInt64 :=
   hash xs.toList
 
 instance (α: Type) (n: Nat) [Hashable α] : Hashable (List.Vector α n) where
   hash := hashVector
 
-def hashRules {n: Nat} {α: Type} {Φ: (α: Type) -> Type} {l: Nat} [Hashable α] [Hashable (Φ α)] (xs: Rules n α Φ l): UInt64 :=
+def hashRules {n: Nat} {Φ: Type} {l: Nat} [Hashable Φ] (xs: Rules n Φ l): UInt64 :=
   hash xs.toList
 
-instance (n: Nat) (α: Type) (Φ: (α: Type) -> Type) (l: Nat) [Hashable α] [Hashable (Φ α)] : Hashable (Rules n α Φ l) where
+instance (n: Nat) (Φ: Type) (l: Nat) [Hashable Φ] : Hashable (Rules n Φ l) where
   hash := hashRules
 
-structure Grammar (n: Nat) (α: Type) (Φ: (α: Type) -> Type) where
-  start: Rule n α Φ
-  prods: Vector (Rule n α Φ) n
+structure Grammar (n: Nat) (Φ: Type) where
+  start: Rule n Φ
+  prods: Vector (Rule n Φ) n
 
-def Grammar.lookup {n: Nat} {α: Type} {Φ: (α: Type) -> Type}
-  (g: Grammar n α Φ) (ref: Fin n): Rule n α Φ :=
+def Grammar.lookup {n: Nat} {Φ: Type}
+  (g: Grammar n Φ) (ref: Fin n): Rule n Φ :=
   Vector.get g.prods ref
 
-def Grammar.singleton (x: Rule 0 α Φ): Grammar 0 α Φ  :=
+def Grammar.singleton (x: Rule 0 Φ): Grammar 0 Φ  :=
   Grammar.mk x #v[]
 
-def Grammar.emptyset: Grammar 0 α Φ :=
+def Grammar.emptyset: Grammar 0 Φ :=
   Grammar.mk Regex.emptyset #v[]
 
-def Grammar.emptystr: Grammar 0 α Φ :=
+def Grammar.emptystr: Grammar 0 Φ :=
   Grammar.mk Regex.emptystr #v[]
 
-example : Grammar 5 String Pred := Grammar.mk
+example : Grammar 5 (Pred String) := Grammar.mk
   -- start := ("html", Html)
   (start := Regex.symbol (Pred.eq "html", 0))
   -- production rules
@@ -72,7 +72,7 @@ example : Grammar 5 String Pred := Grammar.mk
     , Regex.emptystr
   ])
 
-def example_grammar: Grammar 1 Char Pred :=
+def example_grammar: Grammar 1 (Pred Char) :=
   Grammar.mk
     (Regex.or Regex.emptystr (Regex.symbol (Pred.eq 'a', 0)))
     #v[Regex.emptystr]
@@ -91,7 +91,7 @@ theorem Rule.denote_decreasing {x: Hedge.Node α} {xs: Hedge α} (h: List.IsInfi
   simp +arith only at h
   omega
 
-def Rule.denote {α: Type} [BEq α] (g: Grammar n α Pred) (r: Rule n α Pred) (xs: Hedge α): Prop :=
+def Rule.denote {α: Type} [BEq α] (g: Grammar n (Pred α)) (r: Rule n (Pred α)) (xs: Hedge α): Prop :=
   Regex.denote_infix r xs (fun (pred, ref) xs' =>
     match xs' with
     | Subtype.mk [x] _hx =>
@@ -102,10 +102,10 @@ def Rule.denote {α: Type} [BEq α] (g: Grammar n α Pred) (r: Rule n α Pred) (
   termination_by xs
   decreasing_by exact (Rule.denote_decreasing _hx)
 
-def Grammar.denote {α: Type} [BEq α] (g: Grammar n α Pred) (xs: Hedge α): Prop :=
+def Grammar.denote {α: Type} [BEq α] (g: Grammar n (Pred α)) (xs: Hedge α): Prop :=
   Rule.denote g g.start xs
 
-theorem simp_denote_rule' {α: Type} [BEq α] (g: Grammar n α Pred) (r: Rule n α Pred) (xs: Hedge α):
+theorem simp_denote_rule' {α: Type} [BEq α] (g: Grammar n (Pred α)) (r: Rule n (Pred α)) (xs: Hedge α):
   (Regex.denote_infix r xs (fun (pred, ref) xs' =>
     match xs' with
     | Subtype.mk [x] _hx =>
@@ -133,7 +133,7 @@ theorem simp_denote_rule' {α: Type} [BEq α] (g: Grammar n α Pred) (r: Rule n
     | nil =>
       simp
 
-theorem simp_denote_rule {α: Type} [BEq α] (g: Grammar n α Pred) (r: Rule n α Pred) (xs: Hedge α):
+theorem simp_denote_rule {α: Type} [BEq α] (g: Grammar n (Pred α)) (r: Rule n (Pred α)) (xs: Hedge α):
   Rule.denote g r xs =
   Regex.denote_infix r xs (fun (pred, ref) xs' =>
     ∃ label children, xs'.val = [Hedge.Node.mk label children] /\ Pred.eval pred label /\ Rule.denote g (g.lookup ref) children
@@ -156,22 +156,22 @@ theorem simp_denote_rule {α: Type} [BEq α] (g: Grammar n α Pred) (r: Rule n 
     obtain ⟨label, children, hxs, h⟩ := h
     exists Hedge.Node.mk label children
 
-theorem Rule.denote_emptyset {α: Type} [BEq α] {g: Grammar n α Pred}:
+theorem Rule.denote_emptyset {α: Type} [BEq α] {g: Grammar n (Pred α)}:
   Rule.denote g Regex.emptyset = Language.emptyset := by
   unfold Language.emptyset
   funext xs
   unfold Rule.denote
   simp [Regex.denote_infix_emptyset]
 
-theorem Rule.denote_emptystr {α: Type} [BEq α] {g: Grammar n α Pred}:
+theorem Rule.denote_emptystr {α: Type} [BEq α] {g: Grammar n (Pred α)}:
   Rule.denote g Regex.emptystr = Language.emptystr := by
   unfold Language.emptystr
   funext xs
   unfold Rule.denote
   simp [Regex.denote_infix_emptystr]
 
 theorem denote_rule_symbol' {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {pred: Pred α} {ref: Ref n} {xs: Hedge α}:
+  {g: Grammar n (Pred α)} {pred: Pred α} {ref: Ref n} {xs: Hedge α}:
   Rule.denote g (Regex.symbol (pred, ref)) xs
   <-> Language.tree (Pred.eval pred) (Rule.denote g (g.lookup ref)) xs := by
   cases xs with
@@ -218,14 +218,14 @@ theorem denote_rule_symbol' {n: Nat} {α: Type} [BEq α]
         apply And.intro hp hg
 
 theorem Rule.denote_symbol {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {pred: Pred α} {ref: Ref n}:
+  {g: Grammar n (Pred α)} {pred: Pred α} {ref: Ref n}:
   Rule.denote g (Regex.symbol (pred, ref))
   = Language.tree (Pred.eval pred) (Rule.denote g (g.lookup ref)) := by
   funext xs
   rw [denote_rule_symbol']
 
 theorem Rule.denote_or {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {p q: Rule n α Pred}:
+  {g: Grammar n (Pred α)} {p q: Rule n (Pred α)}:
   Rule.denote g (Regex.or p q)
   = Language.or (Rule.denote g p) (Rule.denote g q) := by
   funext xs
@@ -234,7 +234,7 @@ theorem Rule.denote_or {n: Nat} {α: Type} [BEq α]
   simp [Regex.denote_infix_or]
 
 theorem Rule.denote_concat_n {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {p q: Rule n α Pred}:
+  {g: Grammar n (Pred α)} {p q: Rule n (Pred α)}:
   Rule.denote g (Regex.concat p q)
   = Language.concat_n (Rule.denote g p) (Rule.denote g q) := by
   funext xs
@@ -279,15 +279,15 @@ theorem Rule.denote_concat_n {n: Nat} {α: Type} [BEq α]
         simp
 
 theorem Rule.denote_concat {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {p q: Rule n α Pred}:
+  {g: Grammar n (Pred α)} {p q: Rule n (Pred α)}:
   Rule.denote g (Regex.concat p q)
   = Language.concat (Rule.denote g p) (Rule.denote g q) := by
   rw [Rule.denote_concat_n]
   funext xs
   rw [Language.concat_is_concat_n]
 
 theorem denote_rule_star_n' {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {r: Rule n α Pred} (xs: Hedge α):
+  {g: Grammar n (Pred α)} {r: Rule n (Pred α)} (xs: Hedge α):
   Rule.denote g (Regex.star r) xs
   <->
   Language.star_n (Rule.denote g r) xs := by
@@ -349,23 +349,23 @@ theorem denote_rule_star_n' {n: Nat} {α: Type} [BEq α]
     apply List.list_length_drop_lt_cons
 
 theorem Rule.denote_star_n {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {r: Rule n α Pred}:
+  {g: Grammar n (Pred α)} {r: Rule n (Pred α)}:
   Rule.denote g (Regex.star r)
   =
   Language.star_n (Rule.denote g r) := by
   funext xs
   rw [denote_rule_star_n']
 
 theorem Rule.denote_star {n: Nat} {α: Type} [BEq α]
-  {g: Grammar n α Pred} {r: Rule n α Pred}:
+  {g: Grammar n (Pred α)} {r: Rule n (Pred α)}:
   Rule.denote g (Regex.star r)
   =
   Language.star (Rule.denote g r) := by
   funext xs
   rw [denote_rule_star_n']
   rw [Language.star_is_star_n]
 
-def Rule.denote_onlyif {α: Type} [BEq α] (condition: Prop) [dcond: Decidable condition] (g: Grammar n α Pred) (x: Rule n α Pred):
+def Rule.denote_onlyif {α: Type} [BEq α] (condition: Prop) [dcond: Decidable condition] (g: Grammar n (Pred α)) (x: Rule n (Pred α)):
   denote g (Regex.onlyif condition x) = Language.onlyif condition (denote g x) := by
   unfold Language.onlyif
   unfold Regex.onlyif
@@ -382,13 +382,13 @@ def Rule.denote_onlyif {α: Type} [BEq α] (condition: Prop) [dcond: Decidable c
     intro hc'
     contradiction
 
-def Rule.nullable (r: Rule n α Φ): Bool :=
+def Rule.nullable (r: Rule n Φ): Bool :=
   Regex.nullable r
 
-def Grammar.nullable (g: Grammar n α Φ): Bool :=
+def Grammar.nullable (g: Grammar n Φ): Bool :=
   Rule.nullable g.start
 
-theorem Rule.null_commutes {α: Type} [BEq α] (g: Grammar n α Pred) (x: Rule n α Pred):
+theorem Rule.null_commutes {α: Type} [BEq α] (g: Grammar n (Pred α)) (x: Rule n (Pred α)):
   ((Rule.nullable x) = true) = Language.null (denote g x) := by
   induction x with
   | emptyset =>

Validator/Expr/IfExpr.lean

@@ -12,17 +12,17 @@ abbrev IfExprs n α l := List.Vector (IfExpr n α) l
 
 namespace IfExpr
 
-def eval {α: Type} [DecidableEq α] (g: Grammar n α Pred) (ifExpr: IfExpr n α) (t: α): Rule n α Pred :=
+def eval {α: Type} [DecidableEq α] (g: Grammar n (Pred α)) (ifExpr: IfExpr n α) (t: α): Rule n (Pred α) :=
   match ifExpr with
   | IfExpr.mk cnd thn =>
     if Pred.eval cnd t
     then g.lookup thn
     else Regex.emptyset
 
-def evals {α: Type} {n: Nat} [DecidableEq α] (g: Grammar n α Pred) (ifExprs: IfExprs n α l) (t: α): Rules n α Pred l :=
+def evals {α: Type} {n: Nat} [DecidableEq α] (g: Grammar n (Pred α)) (ifExprs: IfExprs n α l) (t: α): Rules n (Pred α) l :=
   List.Vector.map (fun x => eval g x t) ifExprs
 
-theorem evals_nil_is_nil {α: Type} {n: Nat} [DecidableEq α] (g: Grammar n α Pred) (a: α):
+theorem evals_nil_is_nil {α: Type} {n: Nat} [DecidableEq α] (g: Grammar n (Pred α)) (a: α):
   evals g (n := n) List.Vector.nil a = List.Vector.nil := by
   unfold evals
   simp

Validator/Learning/Basic.lean

@@ -16,7 +16,7 @@ import Validator.Derive.Leave
 
 namespace Basic
 
-def derive {α: Type} [DecidableEq α] (g: Grammar μ α Pred) (xs: Rules μ α Pred ν) (t: Hedge.Node α): Rules μ α Pred ν :=
+def derive {α: Type} [DecidableEq α] (g: Grammar μ (Pred α)) (xs: Rules μ (Pred α) ν) (t: Hedge.Node α): Rules μ (Pred α) ν :=
   if List.all xs.toList Regex.unescapable
   then xs
   else
@@ -25,21 +25,21 @@ def derive {α: Type} [DecidableEq α] (g: Grammar μ α Pred) (xs: Rules μ α
       -- enters is one of our two new memoizable functions.
       let ifExprs: IfExprs μ α (Symbol.nums xs) := Enter.deriveEnter xs
       -- childxs = expressions to evaluate on children.
-      let childxs: Rules μ α Pred (Symbol.nums xs) := IfExpr.evals g ifExprs label
+      let childxs: Rules μ (Pred α) (Symbol.nums xs) := IfExpr.evals g ifExprs label
       -- dchildxs = derivatives of children.
       let dchildxs := List.foldl (derive g) childxs children
       -- leaves is the other one of our two new memoizable functions.
       Leave.deriveLeaves xs (List.Vector.map Rule.nullable dchildxs)
 
-def derivs {α: Type} [DecidableEq α] (g: Grammar μ α Pred) (x: Rule μ α Pred) (hedge: Hedge α): Rule μ α Pred :=
+def derivs {α: Type} [DecidableEq α] (g: Grammar μ (Pred α)) (x: Rule μ (Pred α)) (hedge: Hedge α): Rule μ (Pred α) :=
   let dxs := List.foldl (derive g) (List.Vector.cons x List.Vector.nil) hedge
   dxs.head
 
-def validate {α: Type} [DecidableEq α] (g: Grammar μ α Pred) (x: Rule μ α Pred) (hedge: Hedge α): Bool :=
+def validate {α: Type} [DecidableEq α] (g: Grammar μ (Pred α)) (x: Rule μ (Pred α)) (hedge: Hedge α): Bool :=
   let dx := derivs g x hedge
   Rule.nullable dx
 
-def run {α: Type} [DecidableEq α] (g: Grammar μ α Pred) (t: Hedge.Node α): Bool :=
+def run {α: Type} [DecidableEq α] (g: Grammar μ (Pred α)) (t: Hedge.Node α): Bool :=
   validate g g.start [t]
 
 -- Tests