make deriveEnter and deriveLeave generic for regex and not specific to Hedge

Author: awalterschulze

Validator.lean

@@ -1,6 +1,5 @@
 import Validator.Std
 
-import Validator.Derive
 import Validator.Hedge
 import Validator.Learning
 import Validator.Memoize

Validator/Derive.lean

@@ -18,8 +18,9 @@ import Validator.Hedge.Language
 -- n = the number of non-terminals
 abbrev Ref (n: Nat) := Fin n -- non-terminal
 
-abbrev Rule (n: Nat) (φ: Type) :=
-  Regex (φ × Ref n)
+abbrev Symbol (n: Nat) (φ: Type) := (φ × Ref n)
+
+abbrev Rule (n: Nat) (φ: Type) := Regex (Symbol n φ)
 
 abbrev Rules (n: Nat) (φ: Type) (l: Nat) :=
   Vec (Rule n φ) l

Validator/Derive/Enter.lean

@@ -13,8 +13,8 @@ import Validator.Hedge.IfExpr
 import Validator.Regex.Language
 import Validator.Pred.AnyEq
 
-import Validator.Derive.Enter
-import Validator.Derive.Leave
+import Validator.Regex.Enter
+import Validator.Regex.LeaveSmart
 
 namespace Basic
 
@@ -34,7 +34,7 @@ def derive {α: Type}
       let dchildxs: Rules n φ (Symbol.nums xs) := List.foldl (derive G Φ) childxs children
       let ns: Vec Bool (Symbol.nums xs) := Vec.map dchildxs Rule.null
       -- leaves is the other one of our two new memoizable functions.
-      let lchildxs: Rules n φ l := Leave.deriveLeaves xs ns
+      let lchildxs: Rules n φ l := LeaveSmart.deriveLeaves xs ns
       lchildxs
 
 def derivs {α: Type}

Validator/Derive/Leave.lean

@@ -14,8 +14,8 @@ import Validator.Hedge.Grammar
 import Validator.Hedge.IfExpr
 import Validator.Regex.Regex
 
-import Validator.Derive.Enter
-import Validator.Derive.Leave
+import Validator.Regex.Enter
+import Validator.Regex.LeaveSmart
 
 namespace Compress
 
@@ -36,7 +36,7 @@ def derive [DecidableEq φ]
       let cdchildxs := List.foldl (derive G Φ) cchildxs children
       -- dchildxs = uncompressed derivatives of children.
       let dchildxs := Compress.expand indices cdchildxs
-      Leave.deriveLeaves xs (Vec.map dchildxs Rule.null)
+      LeaveSmart.deriveLeaves xs (Vec.map dchildxs Rule.null)
 
 def derivs [DecidableEq φ]
   (G: Grammar n φ) (Φ : φ → α → Bool)

Validator/Hedge/Grammar.lean

@@ -10,7 +10,7 @@ import Validator.Learning.Parser
 
 namespace Memoize
 
-def validate {m} [DecidableEq φ] [ValidateM m n φ α]
+def validate {m} [DecidableEq φ] [ValidateM m (Symbol n φ) α]
   (G: Grammar n φ) (Φ : φ → α → Bool)
   (x: Rule n φ): m Bool :=
   Parser.validate G Φ x

Validator/Learning/Basic.lean

@@ -14,33 +14,33 @@ import Validator.Parser.Hint
 import Validator.Parser.Parser
 import Validator.Parser.TokenTree
 
-import Validator.Derive.Enter
-import Validator.Derive.Leave
+import Validator.Regex.Enter
+import Validator.Regex.LeaveSmart
 
 import Validator.Validator.ValidateM
 import Validator.Validator.Inst.TreeParserM
 
 namespace Parser
 
-def deriveEnter [DecidableEq φ] [ValidateM m n φ α]
+def deriveEnter [DecidableEq φ] [ValidateM m (Symbol n φ) α]
   (G: Grammar n φ) (Φ: φ -> α -> Bool)
   (xs: Rules n φ l): m (Rules n φ (Symbol.nums xs)) := do
   let enters <- Enter.DeriveEnter.deriveEnter xs
   let token <- Parser.token
   return IfExpr.evals G Φ enters token
 
-def deriveLeaveM [DecidableEq φ] [ValidateM m n φ α] (xs: Rules n φ l) (cs: Rules n φ (Symbol.nums xs)): m (Rules n φ l) :=
-  Leave.DeriveLeaveM.deriveLeaveM xs (Vec.map cs Rule.null)
+def deriveLeaveM [DecidableEq φ] [ValidateM m (Symbol n φ) α] (xs: Rules n φ l) (cs: Rules n φ (Symbol.nums xs)): m (Rules n φ l) :=
+  LeaveSmart.DeriveLeaveM.deriveLeaveM xs (Vec.map cs Rule.null)
 
-def deriveValue [DecidableEq φ] [ValidateM m n φ α]
+def deriveValue [DecidableEq φ] [ValidateM m (Symbol n φ) α]
   (G: Grammar n φ) (Φ: φ -> α -> Bool)
   (xs: Rules n φ l): m (Rules n φ l) := do
   deriveEnter G Φ xs >>= deriveLeaveM (α := α) xs
 
 -- TODO: Is it possible to have a Parser type that can be proved to be of the correct shape, and have not expection throwing
 -- for example: can you prove that your Parser will never return an Hint.leave after returning a Hint.field.
 -- This class can be called the LawfulParser.
-partial def derive [DecidableEq φ] [ValidateM m n φ α]
+partial def derive [DecidableEq φ] [ValidateM m (Symbol n φ) α]
   (G: Grammar n φ) (Φ: φ -> α -> Bool)
   (xs: Rules n φ l): m (Rules n φ l) := do
   if List.all xs.toList Regex.unescapable then
@@ -60,7 +60,7 @@ partial def derive [DecidableEq φ] [ValidateM m n φ α]
   | Hint.leave => return xs -- never happens at the top
   | Hint.eof => return xs -- only happens at the top
 
-def validate {m} [DecidableEq φ] [ValidateM m n φ α]
+def validate {m} [DecidableEq φ] [ValidateM m (Symbol n φ) α]
   (G: Grammar n φ) (Φ: φ -> α -> Bool)
   (x: Rule n φ): m Bool := do
   let dxs <- derive G Φ (Vec.cons x Vec.nil)

Validator/Learning/Compress.lean

@@ -7,7 +7,7 @@ import Validator.Hedge.IfExpr
 import Validator.Regex.Regex
 import Validator.Regex.Symbol
 
-import Validator.Derive.Enter
+import Validator.Regex.Enter
 
 abbrev MemEnter.EnterMap (n: Nat) φ [DecidableEq φ] [Hashable φ] :=
   Std.ExtDHashMap
@@ -62,5 +62,5 @@ def deriveEnter
     Debug.debug "cache hit"
     return value
 
-instance [DecidableEq φ] [Hashable φ] [Monad m] [Debug m] [MemEnter m n φ] : Enter.DeriveEnter m n φ where
+instance [DecidableEq φ] [Hashable φ] [Monad m] [Debug m] [MemEnter m n φ] : Enter.DeriveEnter m (φ × Ref n) where
   deriveEnter {l: Nat} (xs: Rules n φ l): m (IfExprs n φ (Symbol.nums xs)) := deriveEnter xs