lean: support multilevels for scope variables

fixing mal process output
lean: remove SLOW tag

Author: loredanacirstea

IMPLS.yml

@@ -49,7 +49,7 @@ IMPL:
   - {IMPL: julia}
   - {IMPL: kotlin}
   - {IMPL: latex3, NO_PERF: 1, NO_SELF_HOST: 1, SLOW: 1}
-  - {IMPL: lean, SLOW: 1}
+  - {IMPL: lean}
   - {IMPL: livescript}
   - {IMPL: logo}
   - {IMPL: lua}

impls/lean/LeanMal/core.lean

@@ -100,10 +100,6 @@ mutual
       if !(eqInternal a b strict) then false
       else eqList nrest vrest strict
 
-  -- partial def eqDictKeys (k1: List KeyType) (k2: List KeyType) : Bool :=
-  --   match k1, k2 with
-  --   | KeyType.strKey x,
-
   partial def eqDict (n: Dict) (v: Dict) (strict: Bool) : Bool :=
     match n, v with
     | Dict.empty, Dict.empty => true
@@ -114,7 +110,7 @@ mutual
       else
         keys1.all (fun k =>
           match (d1.get k, d2.get k) with
-          | (some (_, v1), some (_, v2)) => eqInternal v1 v2 strict
+          | (some v1, some v2) => eqInternal v1 v2 strict
           | _ => false)
 
   partial def eqInternal (first: Types) (second: Types) (strict: Bool) : Bool :=
@@ -136,7 +132,7 @@ mutual
       let v := toList vvec
       if n.length != v.length then false
       else eqList n v strict
-    | Types.dictVal n, Types.dictVal v => eqDict n v strict
+    | Types.dictVal n, Types.dictVal v => eqDict n v strict -- mal hash-maps are Dict level 0
     | Types.listVal n, Types.vecVal vvec => if strict then false else
       let v := toList vvec
       if n.length != v.length then false
@@ -181,7 +177,7 @@ def resetAtom (env : Env) (lst: List Types) (args: List Types) : IO (Env × Type
     let atomSymbol := args[0]!
     match atomSymbol with
     | Types.symbolVal sym =>
-      match env.get (KeyType.strKey sym) with
+      match env.getRecursive (KeyType.strKey sym) with
       | none => throw (IO.userError s!"{sym} not found")
       | some (level, _) => match first with
         | Types.atomVal x => match x with
@@ -201,8 +197,8 @@ def prStrInternal (lst: List Types) (printReadably: Bool) (sep: String) : String
 def KEY_DEBUG_EVAL := "DEBUG-EVAL"
 
 def getDebugEval (env : Env): Bool :=
-  match env.get (KeyType.strKey KEY_DEBUG_EVAL) with
-    | some (_, v) => match v with
+  match env.get (KeyType.strKey KEY_DEBUG_EVAL) 0 with
+    | some v => match v with
       | Types.boolVal v => v
       | Types.Nil => false
       | _ => false
@@ -236,12 +232,12 @@ def countFunc(env : Env) (lst: List Types) : IO (Env × Types) := do
       | Types.Nil => return (env, Types.intVal 0)
       | _ => throw (IO.userError "count called on non-sequence")
 
-def readString (lst: List Types) (envir: Env) : IO Types := do
+def readString (lst: List Types) : IO Types := do
   if lst.length < 1 then throw (IO.userError "read-string: 1 arguments required")
   else
     let first := lst[0]!
     match first with
-    | Types.strVal v => match read_types_with_env v envir.getDict with -- Dict.empty
+    | Types.strVal v => match read_types_with_env v with
       | Except.error e => throw (IO.userError e)
       | Except.ok res => return res
     | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: string")
@@ -344,10 +340,10 @@ def makeDictInternal (initialDict : Dict) (lst: List Types) : IO (Dict) := do
     | [] => return (acc, acckeys)
     | (Types.strVal k) :: v :: rest =>
       if acckeys.contains k then return (acc, acckeys)
-      else loop rest (acckeys ++ [k]) (Dict.insert (KeyType.strKey k) 0 v acc)
+      else loop rest (acckeys ++ [k]) (Dict.insert (KeyType.strKey k) v acc)
     | (Types.keywordVal k) :: v :: rest =>
       if acckeys.contains k then return (acc, acckeys)
-      else loop rest (acckeys ++ [k]) (Dict.insert (KeyType.keywordKey k) 0 v acc)
+      else loop rest (acckeys ++ [k]) (Dict.insert (KeyType.keywordKey k) v acc)
     | _ => throw (IO.userError "Invalid list format: Expected alternating string/keyword and value")
   let (v, _) ← loop lst [] initialDict
   return v
@@ -406,11 +402,11 @@ def getDict (env : Env) (lst: List Types) : IO (Env × Types) := do
         match (rest[0]!) with
         | Types.strVal k =>
           match v.get (KeyType.strKey k) with
-          | some (_, val) => return (env, val)
+          | some val => return (env, val)
           | none => return (env, Types.Nil)
         | Types.keywordVal k =>
           match v.get (KeyType.keywordKey k) with
-          | some (_, val) => return (env, val)
+          | some val => return (env, val)
           | none => return (env, Types.Nil)
         | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: keyword or string")
     | Types.Nil => return (env, Types.Nil)
@@ -610,12 +606,8 @@ def setSymbol (env : Env) (name: String) (value: Types): Env :=
 -- used to forward mutated atoms and variables defined by `eval` in the root scope
 def forwardOuterScopeDefs (envSource: Env) (envOuter: Env): Env :=
   envSource.getDict.fold envOuter (fun key l v acc =>
+    -- do not propagate vars defined in current scope (higher level index)
     if l > acc.getLevel then acc
-    else if l < acc.getLevel then acc.add key l v
-    else
-      match acc.get key with
-        | none => acc.add key l v
-        | some (lOuter, _) =>
-          if l != lOuter then acc
-          else acc.add key l v
+    -- propagate vars defined in outer scopes - with <= level index (e.g. defined by eval, mutated atoms)
+    else acc.add key l v
   )

impls/lean/LeanMal/reader.lean

@@ -163,13 +163,13 @@ def read_comment : Parsec Unit := do
     pure ()
 
 mutual
-  partial def read_list (envir: Dict := Dict.empty) : Parsec Types := do
+  partial def read_list : Parsec Types := do
     -- ws
     let _ ← optional  wspace_or_comma_strict
     let _ ← pstring "("
     let _ ← optional  wspace_or_comma_strict
     let els ← many (do
-      let e ← read_types envir
+      let e ← read_types
       let _ ← optional  wspace_or_comma_strict
       -- let _ ← optional (pchar ',')
       return e)
@@ -179,12 +179,12 @@ mutual
     let _ ← optional  wspace_or_comma_strict
     return Types.listVal (els.toList)
 
-    partial def read_vector (envir: Dict := Dict.empty) : Parsec Types := do
+    partial def read_vector : Parsec Types := do
     let _ ← optional  wspace_or_comma_strict
     let _ ← pchar '['
     let _ ← optional  wspace_or_comma_strict
     let els ← many (do
-      let e ← read_types envir
+      let e ← read_types
       let _ ← optional  wspace_or_comma_strict
       -- let _ ← optional (pchar ',')
       return e)
@@ -195,7 +195,7 @@ mutual
     let vec  := listToVec vecLst
     return Types.vecVal vec
 
-  partial def read_hash_map (_: Dict := Dict.empty) : Parsec Types := do
+  partial def read_hash_map : Parsec Types := do
     let _ ← optional  wspace_or_comma_strict
     let _ ← pchar '{'
     let _ ← optional  wspace_or_comma_strict
@@ -205,7 +205,7 @@ mutual
     let _ ← optional  wspace_or_comma_strict
     let dict := Array.foldl (fun m (k, v) =>
 
-      m.insert k 0 v
+      m.insert k v
     ) (Dict.empty) els
     return Types.dictVal dict
 
@@ -222,21 +222,21 @@ mutual
       | Types.strVal v => return (KeyType.strKey v, value)
       | _ => default
 
-  partial def read_symbol (chars: String) (name: String) (envir: Dict := Dict.empty) : Parsec Types := do
+  partial def read_symbol (chars: String) (name: String) : Parsec Types := do
     let _ ← optional  wspace_or_comma_strict
     let _ ← pstring chars
-    let elem ← read_types envir
+    let elem ← read_types
     let _ ← optional  wspace_or_comma_strict
 
     let vecLst := [(Types.symbolVal name), elem]
     return Types.listVal vecLst
 
-  partial def read_with_meta (envir: Dict := Dict.empty) : Parsec Types := do
+  partial def read_with_meta : Parsec Types := do
     ws
     let _ ← pstring "^"
 
     let els ← many (do
-      let e ← read_types envir
+      let e ← read_types
       ws
       let _ ← optional (pchar ',')
       return e)
@@ -245,22 +245,22 @@ mutual
     let vecLst := (Types.symbolVal "with-meta") :: elsVec
     return Types.listVal (List.append vecLst elsVec)
 
-  partial def read_atom (_: Dict := Dict.empty) : Parsec Types :=
+  partial def read_atom : Parsec Types :=
     read_operator_or_number <|> read_float_or_int <|> read_str_val <|> read_keyword <|> read_nil_val <|> read_bool_val <|> read_symbol_val
 
-  partial def read_types (envir: Dict := Dict.empty) : Parsec Types := do
+  partial def read_types : Parsec Types := do
       let _ ← optional  wspace
       let _ ← optional (many read_comment)
       match ← peek? with
       | none => fail "endofinput"
       | some _ =>
-        read_list envir <|> read_vector envir <|> read_hash_map envir  <|> read_symbol "'" "quote" envir <|> read_symbol "`" "quasiquote" envir <|> read_symbol "~@" "splice-unquote" envir <|> read_symbol "~" "unquote" envir <|> read_symbol "@" "deref" envir <|> read_with_meta envir <|> read_atom envir
+        read_list <|> read_vector <|> read_hash_map  <|> read_symbol "'" "quote" <|> read_symbol "`" "quasiquote" <|> read_symbol "~@" "splice-unquote" <|> read_symbol "~" "unquote" <|> read_symbol "@" "deref" <|> read_with_meta <|> read_atom
 end
 
-def read_types_with_env (input : String) (envir: Dict := Dict.empty)  : Except String Types :=
-  match read_types envir input.trim.iter with
+def read_types_with_env (input : String)  : Except String Types :=
+  match read_types input.trim.iter with
   | Lean.Parsec.ParseResult.success _ res => Except.ok res
   | Lean.Parsec.ParseResult.error _ err => Except.error err
 
 def read_str (input : String)  : Except String Types :=
-  read_types_with_env input (Dict.empty : Dict.{u})
+  read_types_with_env input

impls/lean/LeanMal/step1_read_print.lean

@@ -4,15 +4,15 @@ import LeanMal.printer
 universe u
 
 def READ (input : String) :=
-  read_str.{u} input
+  read_str input
 
 def EVAL (ast : Types) (_: String) := ast
 
 def PRINT (ast : Types): String :=
   pr_str true ast
 
 def rep (input : String): String :=
-  match READ.{u} input with
+  match READ input with
   | Except.ok result =>
     PRINT (EVAL result "")
   | Except.error err =>
@@ -31,4 +31,4 @@ def main : IO Unit := do
     if value.isEmpty then
       donext := false
     else
-      IO.println (rep.{u} value)
+      IO.println (rep value)

impls/lean/LeanMal/step2_eval.lean

@@ -4,7 +4,7 @@ import LeanMal.printer
 universe u
 
 def READ (input : String): Except String Types :=
-  read_str.{u} input
+  read_str input
 
 def sum (env : Env) (lst: List Types) : IO (Env × Types) := do
   match lst with
@@ -54,7 +54,7 @@ mutual
 
   partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
     match ast with
-    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+    | Types.symbolVal v   => match env.getRecursive (KeyType.strKey v) with
       | some (_, vi) => return (env, vi)
       | none    => return (env, Types.symbolVal v )
     | Types.listVal el    => (evalList env el)
@@ -77,8 +77,8 @@ mutual
           let keys: List String := match params with
             | Types.listVal v => v.map fun x => x.toString false
             | _               => []
-          let argsDict := (buildDict 0 keys results)
-          let merged := (newEnv.merge fenv).mergeDict (fenv.getLevel + 1) argsDict
+          let argsEnv := (buildEnv (fenv.getLevel + 1) keys results)
+          let merged := (newEnv.merge fenv).merge argsEnv
           evalTypes merged body
         | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
       | _ => throw (IO.userError s!"`unexpected token, expected: function`")
@@ -103,10 +103,10 @@ mutual
   partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
     match lst with
       | Dict.empty => return (env, lst)
-      | Dict.insert k _ v restDict =>
+      | Dict.insert k v restDict =>
         let (newEnv, newVal) ← evalTypes env v
         let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
-        let newDict := Dict.insert k 0 newVal updatedDict
+        let newDict := Dict.insert k newVal updatedDict
         return (updatedEnv, newDict)
 
   partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) := do
@@ -121,10 +121,10 @@ def PRINT (ast : Types): String :=
   pr_str true ast
 
 def rep (input : String): IO String := do
-  match READ.{u} input with
+  match READ input with
   | Except.ok result =>
     try
-      let (_, res) ← evalTypes (Env.data 0 Dict.empty) result
+      let (_, res) ← evalTypes (Env.data 0 LevelDict.empty KLDict.empty) result
       return PRINT res
     catch
       | e => return s!"Error: {e}"
@@ -144,5 +144,5 @@ def main : IO Unit := do
     if value.isEmpty then
       donext := false
     else
-      let output ← rep.{u} value
+      let output ← rep value
       IO.println output

impls/lean/LeanMal/step3_env.lean

@@ -5,7 +5,7 @@ import LeanMal.types
 universe u
 
 def READ (input : String): Except String Types :=
-  read_str.{u} input
+  read_str input
 
 def sum (env : Env) (lst: List Types) : IO (Env × Types) := do
   match lst with
@@ -55,7 +55,7 @@ mutual
 
   partial def evalTypes (env : Env) (ast : Types) : IO (Env × Types) := do
     match ast with
-    | Types.symbolVal v   => match env.get (KeyType.strKey v) with
+    | Types.symbolVal v   => match env.getRecursive (KeyType.strKey v) with
       | some (_, vi) => return (env, vi)
       | none => throw (IO.userError s!"'{v}' not found")
     | Types.listVal el    => (evalList env el)
@@ -78,8 +78,8 @@ mutual
             | Types.listVal v => v.map fun x => x.toString false
             | _               => []
           let argsLevel := fenv.getLevel + 1
-          let argsDict := (buildDict argsLevel keys results)
-          let merged := (newEnv.merge fenv).mergeDict argsLevel argsDict
+          let argsEnv := (buildEnv argsLevel keys results)
+          let merged := (newEnv.merge fenv).merge argsEnv
           evalTypes merged body
         | Fun.macroFn _ _ _ => throw (IO.userError "macro not implemented")
       | _ => throw (IO.userError s!"`unexpected token, expected: function`")
@@ -106,10 +106,10 @@ mutual
   partial def evalDictInner (env: Env) (lst : Dict) : IO (Env × Dict) := do
     match lst with
       | Dict.empty => return (env, lst)
-      | Dict.insert k _ v restDict =>
+      | Dict.insert k v restDict =>
         let (newEnv, newVal) ← evalTypes env v
         let (updatedEnv, updatedDict) ← evalDictInner newEnv restDict
-        let newDict := Dict.insert k 0 newVal updatedDict
+        let newDict := Dict.insert k newVal updatedDict
         return (updatedEnv, newDict)
 
   partial def evalFuncArgs (env: Env) (args: List Types) : IO (Env × List Types) := do
@@ -173,7 +173,7 @@ def PRINT (ast : Types): String :=
   pr_str true ast
 
 def rep (env: Env) (input : String): IO (Env × String) := do
-  match READ.{u} input with
+  match READ input with
   | Except.ok result =>
     try
       let (newenv, res) ← evalTypes env result
@@ -188,7 +188,7 @@ def repAndPrint (env: Env) (output : String): IO Env := do
   return env
 
 def main : IO Unit := do
-  let mut env := loadFnNativeAll (Env.data 0 Dict.empty)
+  let mut env := loadFnNativeAll (Env.data 0 LevelDict.empty KLDict.empty)
   let mut donext := true
   while donext do
     IO.print "user> "
@@ -201,5 +201,5 @@ def main : IO Unit := do
     if value.isEmpty then
       donext := false
     else
-      let (newenv, value) ← rep.{u} env value
+      let (newenv, value) ← rep env value
       env ← repAndPrint newenv value