move parser and memoize implementations into Learning folder and create one Validate algorithm in Deriv

Author: awalterschulze

Validator.lean

@@ -24,10 +24,7 @@ import Validator.Deriv.Leave
 import Validator.Deriv.Mem
 import Validator.Deriv.MemEnter
 import Validator.Deriv.MemLeave
-import Validator.Deriv.ParserConcise
-import Validator.Deriv.ParserConciseMem
-import Validator.Deriv.ParserConciseMemTest
-import Validator.Deriv.ParserConciseCompress
-import Validator.Deriv.ParserConciseCompressMem
+import Validator.Deriv.Validate
+import Validator.Deriv.TestMemoize
 
 import Validator.Learning.Learning

Validator/Deriv/ParserConciseCompressMem.lean

@@ -3,16 +3,18 @@ import Validator.Parser.ParseTree
 import Validator.Deriv.Env
 import Validator.Deriv.EnvTreeParserStateWithMem
 import Validator.Deriv.EnvTreeParserStateWithMemTest
-import Validator.Deriv.ParserConcise
+import Validator.Deriv.Validate
 
-namespace ParserConciseMemTest
+namespace TestMemoize
 
 def validate {m} [Env m] (x: Expr): m Bool :=
-  ParserConcise.validate x
+  Validate.validate x
 
 def run (x: Expr) (t: ParseTree): Except String Bool :=
   EnvTreeParserStateWithMem.run (validate x) t
 
+-- Tests
+
 def testCacheIsHitOnSecondRun (x: Expr) (t: ParseTree): Except String Bool :=
   match EnvTreeParserStateWithMem.run' (validate x) t with
   | EStateM.Result.error err _ => Except.error err

Validator/Deriv/ParserConciseMemTest.lean Validator/Deriv/TestMemoize.leanValidator/Deriv/ParserConciseMemTest.lean renamed to Validator/Deriv/TestMemoize.lean

@@ -9,14 +9,14 @@ import Validator.Expr.IfExpr
 
 import Validator.Deriv.Enter
 import Validator.Deriv.Env
-import Validator.Deriv.EnvTreeParserState
+import Validator.Deriv.EnvTreeParserStateWithMem
 import Validator.Deriv.Leave
 
 import Validator.Parser.ParseTree
 import Validator.Parser.Parser
 import Validator.Parser.Hint
 
-namespace ParserConciseCompress
+namespace Validate
 
 def deriveEnter [Env m] (xs: List Expr): m (List Expr) := do
   let token <- Parser.token
@@ -61,7 +61,9 @@ def validate {m} [Env m] (x: Expr): m Bool := do
   | _ => throw "expected one expression"
 
 def run (x: Expr) (t: ParseTree): Except String Bool :=
-  EnvTreeParserState.run (validate x) t
+  EnvTreeParserStateWithMem.run (validate x) t
+
+-- Tests
 
 open ParseTree (node)
 

…lidator/Deriv/ParserConciseCompress.lean Validator/Deriv/Validate.leanValidator/Deriv/ParserConciseCompress.lean renamed to Validator/Deriv/Validate.lean Validator/Deriv/ParserConciseCompress.lean renamed to Validator/Deriv/Validate.lean

@@ -3,4 +3,6 @@ import Validator.Learning.Compress
 import Validator.Learning.ImperativeBasic
 import Validator.Learning.ImperativeCompress
 import Validator.Learning.ImperativeLeave
+import Validator.Learning.Memoize
 import Validator.Learning.Original
+import Validator.Learning.Parser

Validator/Learning/Learning.lean

@@ -2,16 +2,19 @@ import Validator.Parser.ParseTree
 
 import Validator.Deriv.Env
 import Validator.Deriv.EnvTreeParserStateWithMem
-import Validator.Deriv.ParserConcise
 
-namespace ParserConciseMem
+import Validator.Learning.Parser
+
+namespace Memoize
 
 def validate {m} [Env m] (x: Expr): m Bool :=
-  ParserConcise.validate x
+  Parser.validate x
 
 def run (x: Expr) (t: ParseTree): Except String Bool :=
   EnvTreeParserStateWithMem.run (validate x) t
 
+-- Tests
+
 open ParseTree (node)
 
 #guard run

Validator/Deriv/ParserConciseMem.lean Validator/Learning/Memoize.leanValidator/Deriv/ParserConciseMem.lean renamed to Validator/Learning/Memoize.lean

@@ -1,4 +1,4 @@
--- ParserConcise is a memoizable version of the validation algorithm.
+-- Parser is a memoizable version of the validation algorithm.
 -- This version of the algorithm uses a Parser instead of a ParseTree.
 -- It is intended to be used for explanation purposes. This means that it gives up speed for readability. Thus it has no memoization implemented.
 
@@ -15,7 +15,7 @@ import Validator.Parser.Hint
 import Validator.Parser.Parser
 import Validator.Parser.ParseTree
 
-namespace ParserConcise
+namespace Parser
 
 def deriveEnter [Env m] (xs: List Expr): m (List Expr) := do
   let token <- Parser.token
@@ -55,6 +55,8 @@ def validate {m} [Env m] (x: Expr): m Bool := do
 def run (x: Expr) (t: ParseTree): Except String Bool :=
   EnvTreeParserState.run (validate x) t
 
+-- Tests
+
 open ParseTree (node)
 
 #guard run

Validator/Deriv/ParserConcise.lean Validator/Learning/Parser.leanValidator/Deriv/ParserConcise.lean renamed to Validator/Learning/Parser.lean

@@ -8,4 +8,6 @@ We assume a background in Lean and an understanding of derivatives for regular e
  * [ImperativeBasic](./ImperativeBasic.lean) is the simplest version of the memoizable algorithm, which using [enter](../Deriv/Enter.lean) and [leave](../ImperativeLeave.lean). NO compression, NO monads, NO parser. NO memoization.
  * [ImperativeCompress](./ImperativeCompress.lean) adds compression to [ImperativeBasic](./ImperativeBasic.lean) for a little extra efficiency. NO monads, NO parser, NO memoization.
  * [Basic](./Basic.lean) is the simplest version of the memoizable algorithm, which using [enter](../Deriv/Enter.lean) and [leave](../Deriv/Leave.lean). It uses monads to make the code more concise. NO compression, NO parser, NO memoization.
- * [Compress](./Compress.lean) adds compression to [Basic](./Basic.lean) for a little extra efficiency. NO parser, NO memoization.
+ * [Compress](./Compress.lean) adds compression to [Basic](./Basic.lean) for a little extra efficiency. NO parser, NO memoization.
+ * [Parser](./Parser.lean) adds the use of a pull-based Parser which makes it possible to only parse what is truly necessary to parse. NO memoization. NO compression.
+ * [Memoize](./Memoize.lean) adds memoization, by simply swapping out the implementation of Env. NO compression.