lean: simplify main

fix running with cli args

fix step8 macro

Author: loredanacirstea

impls/lean/LeanMal/core.lean

@@ -236,12 +236,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) (_: Env) : 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 -- Dict.empty
       | Except.error e => throw (IO.userError e)
       | Except.ok res => return res
     | x => throw (IO.userError s!"unexpected symbol: {x.toString true}, expected: string")

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
@@ -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
@@ -121,7 +121,7 @@ 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
@@ -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
@@ -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
@@ -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

impls/lean/LeanMal/step4_if_fn_do.lean

@@ -194,13 +194,13 @@ mutual
 end
 
 def READ (input : String): Except String Types :=
-  read_str.{u} input
+  read_str input
 
 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
@@ -212,7 +212,7 @@ def rep (env: Env) (input : String): IO (Env × String) := do
 def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
   fndefs.foldlM (fun (res : Env × String) fndef => do
     let (ref, msg) := res
-    let (newref, newmsg) ← rep.{u} ref fndef
+    let (newref, newmsg) ← rep ref fndef
     return (newref, s!"{msg}¬{newmsg}")
   ) (env, "")
 
@@ -226,7 +226,7 @@ def repAndPrint (env: Env) (output : String): IO Env := do
   return env
 
 def main : IO Unit := do
-  let (env0, _) ← loadMalFns.{u} (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
   let mut env := env0
   let mut donext := true
   while donext do
@@ -240,5 +240,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

impls/lean/LeanMal/step5_tco.lean

@@ -193,13 +193,13 @@ mutual
 end
 
 def READ (input : String): Except String Types :=
-  read_str.{u} input
+  read_str input
 
 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
@@ -211,7 +211,7 @@ def rep (env: Env) (input : String): IO (Env × String) := do
 def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
   fndefs.foldlM (fun (res : Env × String) fndef => do
     let (ref, msg) := res
-    let (newref, newmsg) ← rep.{u} ref fndef
+    let (newref, newmsg) ← rep ref fndef
     return (newref, s!"{msg}¬{newmsg}")
   ) (env, "")
 
@@ -225,7 +225,7 @@ def repAndPrint (env: Env) (output : String): IO Env := do
   return env
 
 def main : IO Unit := do
-  let (env0, _) ← loadMalFns.{u} (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
   let mut env := env0
   let mut donext := true
   while donext do
@@ -239,5 +239,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

impls/lean/LeanMal/step6_file.lean

@@ -238,13 +238,13 @@ mutual
 end
 
 def READ (input : String): Except String Types :=
-  read_str.{u} input
+  read_str input
 
 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
@@ -256,7 +256,7 @@ def rep (env: Env) (input : String): IO (Env × String) := do
 def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
   fndefs.foldlM (fun (res : Env × String) fndef => do
     let (ref, msg) := res
-    let (newref, newmsg) ← rep.{u} ref fndef
+    let (newref, newmsg) ← rep ref fndef
     return (newref, s!"{msg}¬{newmsg}")
   ) (env, "")
 
@@ -270,16 +270,10 @@ def repAndPrint (env: Env) (output : String): IO Env := do
   else IO.println output
   return env
 
-def main (args : List String) : IO Unit := do
-  let (env0, _) ← loadMalFns.{u} (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
-  let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
-  let mut env := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
-  if args.length > 0 then
-    let (_, val) ← rep.{u} env s!"(load-file \"{args[0]!}\")"
-    IO.println val
-  else
-
-  let mut donext := true
+def reploop (inienv: Env) : IO Unit := do
+  let mut donext := false
+  let mut env := inienv
+  donext := true
   while donext do
     IO.print "user> "
     let stdin ← IO.getStdin
@@ -291,5 +285,16 @@ def main (args : List String) : 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
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env

impls/lean/LeanMal/step7_quote.lean

@@ -278,13 +278,13 @@ mutual
 end
 
 def READ (input : String): Except String Types :=
-  read_str.{u} input
+  read_str input
 
 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
@@ -296,7 +296,7 @@ def rep (env: Env) (input : String): IO (Env × String) := do
 def loadMalFns (env: Env) (fndefs: List String): IO (Env × String) := do
   fndefs.foldlM (fun (res : Env × String) fndef => do
     let (ref, msg) := res
-    let (newref, newmsg) ← rep.{u} ref fndef
+    let (newref, newmsg) ← rep ref fndef
     return (newref, s!"{msg}¬{newmsg}")
   ) (env, "")
 
@@ -310,17 +310,10 @@ def repAndPrint (env: Env) (output : String): IO Env := do
   else IO.println output
   return env
 
-def main (args : List String) : IO Unit := do
-  let (env0, _) ← loadMalFns.{u} (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
-  let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
-  let mut env := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
-
-  if args.length > 0 then
-    let (_, val) ← rep.{u} env s!"(load-file \"{args[0]!}\")"
-    IO.println val
-  else
-
-  let mut donext := true
+def reploop (inienv: Env) : IO Unit := do
+  let mut donext := false
+  let mut env := inienv
+  donext := true
   while donext do
     IO.print "user> "
     let stdin ← IO.getStdin
@@ -332,5 +325,16 @@ def main (args : List String) : 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
+
+def main (args : List String) : IO Unit := do
+  let (env0, _) ← loadMalFns (loadFnNativeAll (Env.data 0 Dict.empty)) fnDefs
+  let env := setSymbol env0 "*ARGV*" (Types.listVal [])
+
+  if args.length > 0 then do
+    let astArgs := ((args.drop 1).map (fun arg => Types.strVal arg))
+    let newenv := setSymbol env0 "*ARGV*" (Types.listVal astArgs)
+    let (_, _) ← rep newenv s!"(load-file \"{args[0]!}\")"
+    IO.Process.exit 0
+  else reploop env