rename EnvM to Env

Author: awalterschulze

Validator/Env.lean

@@ -1,4 +1,4 @@
-import Validator.Env.EnvM
+import Validator.Env.Env
 import Validator.Env.EnvTreeParserIO
 import Validator.Env.EnvTreeParserState
 import Validator.Env.EnvTreeParserStateWithMem

Validator/Env/EnvM.lean Validator/Env/Env.leanValidator/Env/EnvM.lean renamed to Validator/Env/Env.lean

@@ -1,24 +1,23 @@
 import Validator.Std.Debug
 
 import Validator.Parser.Parser
-import Validator.Parser.ParseTree
 
 import Validator.Derive.Enter
 import Validator.Derive.Leave
 
--- EnvM is the derivative validator environment monad.
+-- Env is the derivative validator environment monad.
 -- Executing the derivative algorithm requires:
 --   a pull based Parser
 --   a deriveEnter and deriveLeave function that could optionally be memoized.
 --   the possibility of returning an error.
 --   a debug line printer (implementations should print nothing when not debugging).
 -- Tagless final class inspired by https://jproyo.github.io/posts/2019-03-17-tagless-final-haskell/
-class EnvM (m: Type -> Type u) extends
+class Env (m: Type -> Type u) extends
   Monad m,
   Debug m,
   MonadExcept String m,
   Parser m,
   Enter.DeriveEnter m,
   Leave.DeriveLeave m
 
-namespace EnvM
+namespace Env

Validator/Env/EnvTreeParserIO.lean

@@ -3,7 +3,7 @@ import Validator.Std.Debug
 import Validator.Parser.ParseTree
 import Validator.Parser.TreeParser
 
-import Validator.Env.EnvM
+import Validator.Env.Env
 import Validator.Memoize.MemEnter
 import Validator.Memoize.MemLeave
 
@@ -76,7 +76,7 @@ instance : MemLeave.MemLeave TreeParserIO where
 instance : Leave.DeriveLeave TreeParserIO where
   deriveLeave (xs: List Expr) (ns: List Bool): TreeParserIO (List Expr) := MemLeave.deriveLeave xs ns
 
-instance : EnvM TreeParserIO where
+instance : Env TreeParserIO where
   -- all instances have been created, so no implementations are required here
 
 def run (f: TreeParserIO α) (t: ParseTree): EIO String α :=

Validator/Env/EnvTreeParserState.lean

@@ -1,6 +1,6 @@
 import Validator.Parser.TreeParser
 
-import Validator.Env.EnvM
+import Validator.Env.Env
 
 namespace EnvTreeParserState
 
@@ -25,7 +25,7 @@ instance : Enter.DeriveEnter TreeParserState where
 instance : Leave.DeriveLeave TreeParserState where
   deriveLeave xs ns := Leave.deriveLeave xs ns
 
-instance : EnvM TreeParserState where
+instance : Env TreeParserState where
   -- all instances have been created, so no implementations are required here
 
 def run (x: TreeParserState α) (t: ParseTree): Except String α :=

Validator/Env/EnvTreeParserStateWithMem.lean

@@ -3,7 +3,7 @@ import Validator.Std.Debug
 import Validator.Parser.ParseTree
 import Validator.Parser.TreeParser
 
-import Validator.Env.EnvM
+import Validator.Env.Env
 import Validator.Memoize.MemEnter
 import Validator.Memoize.MemLeave
 
@@ -73,7 +73,7 @@ instance : MemLeave.MemLeave TreeParserStateWithMem where
 instance : Leave.DeriveLeave TreeParserStateWithMem where
   deriveLeave (xs: List Expr) (ns: List Bool): TreeParserStateWithMem (List Expr) := MemLeave.deriveLeave xs ns
 
-instance : EnvM TreeParserStateWithMem where
+instance : Env TreeParserStateWithMem where
   -- all instances have been created, so no implementations are required here
 
 def run (f: TreeParserStateWithMem α) (t: ParseTree): Except String α :=

Validator/Env/TestEnvTreeParserStateWithMem.lean

@@ -4,7 +4,7 @@ import Validator.Memoize.MemEnter
 import Validator.Memoize.MemLeave
 
 import Validator.Env.EnvTreeParserStateWithMem
-import Validator.Env.EnvM
+import Validator.Env.Env
 
 namespace TestEnvTreeParserStateWithMem
 
@@ -86,7 +86,7 @@ instance : Leave.DeriveLeave TreeParserStateWithMemTest where
       Debug.debug "test cache hit"
       return value
 
-instance : EnvM TreeParserStateWithMemTest where
+instance : Env TreeParserStateWithMemTest where
   -- all instances have been created, so no implementations are required here
 
 def run (f: TreeParserStateWithMemTest α) (t: ParseTree): Except String α :=

Validator/Learning/Memoize.lean

@@ -1,13 +1,13 @@
 import Validator.Parser.ParseTree
 
-import Validator.Env.EnvM
+import Validator.Env.Env
 import Validator.Env.EnvTreeParserStateWithMem
 
 import Validator.Learning.Parser
 
 namespace Memoize
 
-def validate {m} [EnvM m] (x: Expr): m Bool :=
+def validate {m} [Env m] (x: Expr): m Bool :=
   Parser.validate x
 
 def run (x: Expr) (t: ParseTree): Except String Bool :=

Validator/Learning/Parser.lean

@@ -9,7 +9,7 @@ import Validator.Expr.IfExpr
 import Validator.Derive.Enter
 import Validator.Derive.Leave
 
-import Validator.Env.EnvM
+import Validator.Env.Env
 import Validator.Env.EnvTreeParserState
 
 import Validator.Parser.Hint
@@ -18,18 +18,18 @@ import Validator.Parser.ParseTree
 
 namespace Parser
 
-def deriveEnter [EnvM m] (xs: List Expr): m (List Expr) := do
+def deriveEnter [Env m] (xs: List Expr): m (List Expr) := do
   let token <- Parser.token
   let enters <- Enter.DeriveEnter.deriveEnter xs
   return IfExpr.evals enters token
 
-def deriveLeave [EnvM m] (xs: List Expr) (cs: List Expr): m (List Expr) :=
+def deriveLeave [Env m] (xs: List Expr) (cs: List Expr): m (List Expr) :=
   Leave.DeriveLeave.deriveLeave xs (List.map Expr.nullable cs)
 
-def deriveValue [EnvM m] (xs: List Expr): m (List Expr) := do
+def deriveValue [Env m] (xs: List Expr): m (List Expr) := do
   deriveLeave xs (<- deriveEnter xs)
 
-partial def derive [EnvM m] (xs: List Expr): m (List Expr) := do
+partial def derive [Env m] (xs: List Expr): m (List Expr) := do
   if List.all xs Expr.unescapable then
     Parser.skip; return xs
   match <- Parser.next with
@@ -47,7 +47,7 @@ partial def derive [EnvM m] (xs: List Expr): m (List Expr) := do
   | Hint.leave => return xs -- never happens at the top
   | Hint.eof => return xs -- only happens at the top
 
-def validate {m} [EnvM m] (x: Expr): m Bool := do
+def validate {m} [Env m] (x: Expr): m Bool := do
   let dxs <- derive [x]
   match dxs with
   | [dx] => return Expr.nullable dx

Validator/Validator/TestDebug.lean

@@ -3,11 +3,11 @@ import Validator.Parser.ParseTree
 import Validator.Validator.Validate
 
 import Validator.Env.EnvTreeParserIO
-import Validator.Env.EnvM
+import Validator.Env.Env
 
 namespace TestDebug
 
-def validate {m} [EnvM m] (x: Expr): m Bool :=
+def validate {m} [Env m] (x: Expr): m Bool :=
   Validate.validate x
 
 unsafe def run (x: Expr) (t: ParseTree): Except String Bool :=

Validator/Validator/TestMemoize.lean

@@ -2,13 +2,13 @@ import Validator.Parser.ParseTree
 
 import Validator.Validator.Validate
 
-import Validator.Env.EnvM
+import Validator.Env.Env
 import Validator.Env.EnvTreeParserStateWithMem
 import Validator.Env.TestEnvTreeParserStateWithMem
 
 namespace TestMemoize
 
-def validate {m} [EnvM m] (x: Expr): m Bool :=
+def validate {m} [Env m] (x: Expr): m Bool :=
   Validate.validate x
 
 def run (x: Expr) (t: ParseTree): Except String Bool :=