gesund

Author: hargoniX

src/library/ir_interpreter.cpp

@@ -1083,7 +1083,9 @@ class interpreter {
         } else { // IO _
             lean_assert(params.size() == 1);
         }
-        object* w = call_boxed("main", call_args.size(), &call_args[0]);
+        object * w = io_mk_world();
+        call_args.push_back(w);
+        w = call_boxed("main", call_args.size(), &call_args[0]);
         if (io_result_is_ok(w)) {
             int ret = 0;
             lean::expr ret_ty = m_env.get("main").get_type();

tests/lake/examples/reverse-ffi/main.c

@@ -7,7 +7,7 @@ extern uint64_t my_length(lean_obj_arg);
 extern void lean_initialize_runtime_module();
 extern void lean_initialize();
 extern void lean_io_mark_end_initialization();
-extern lean_object * initialize_RFFI(uint8_t builtin, lean_object *);
+extern lean_object * initialize_RFFI(uint8_t builtin);
 
 int main() {
   lean_initialize_runtime_module();

tests/lean/baseIO.lean.expected.out

@@ -1,7 +1,7 @@
 [Compiler.saveBase] size: 9
-    def test _y.1 : ST.Out lcAny UInt32 :=
+    def test a.1 : ST.Out lcAny UInt32 :=
       let _x.2 := 42;
-      let _x.3 := @ST.Prim.mkRef _ _ _x.2 _y.1;
+      let _x.3 := @ST.Prim.mkRef _ _ _x.2 a.1;
       cases _x.3 : ST.Out lcAny UInt32
       | ST.Out.mk val.4 state.5 =>
         let _x.6 := 10;

tests/lean/jpClosureIssue.lean.expected.out

@@ -1,11 +1,11 @@
 [Compiler.saveMono] size: 7
-    def foo b _y.1 : EST.Out IO.Error lcAny PUnit :=
+    def foo b a.1 : EST.Out IO.Error lcAny PUnit :=
       cases b : EST.Out IO.Error lcAny PUnit
       | Bool.false =>
         let _x.2 := 1;
-        let _x.3 := print _x.2 _y.1;
+        let _x.3 := print _x.2 a.1;
         return _x.3
       | Bool.true =>
         let _x.4 := 0;
-        let _x.5 := print _x.4 _y.1;
+        let _x.5 := print _x.4 a.1;
         return _x.5

tests/lean/run/emptyLcnf.lean

@@ -41,15 +41,15 @@ trace: [Compiler.result] size: 5
       let _x.3 := Array.push ◾ _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 8
-    def _eval a.1 a.2 _y.3 : EST.Out Lean.Exception lcAny PUnit :=
+    def _eval a.1 a.2 a.3 : EST.Out Lean.Exception lcAny PUnit :=
       let _x.4 := _eval._closed_0;
       let _x.5 := _eval._closed_1;
       let _x.6 := 1;
       let _x.7 := _eval._closed_2;
       let _x.8 := _eval._closed_3;
       let _x.9 := PUnit.unit;
       let _f.10 := _eval._lam_0 _x.8 _x.9;
-      let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 _y.3;
+      let _x.11 := Lean.Elab.Command.liftTermElabM._redArg _f.10 a.1 a.2 a.3;
       return _x.11
 -/
 #guard_msgs in

tests/lean/run/erased.lean

@@ -62,7 +62,7 @@ trace: [Compiler.result] size: 5
       let _x.3 : Array Lean.Name := Array.push ◾ _x.2 _x.1;
       return _x.3
 [Compiler.result] size: 9
-    def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (_y.3 : lcVoid) : EST.Out Lean.Exception lcAny PUnit :=
+    def _eval (a.1 : Lean.Elab.Command.Context) (a.2 : lcAny) (a.3 : lcVoid) : EST.Out Lean.Exception lcAny PUnit :=
       let _x.4 : String := _eval._closed_0;
       let _x.5 : String := _eval._closed_1;
       let _x.6 : Lean.Name := _eval._closed_2;
@@ -74,7 +74,7 @@ trace: [Compiler.result] size: 5
         lcAny →
           Lean.Meta.Context →
             lcAny → Lean.Core.Context → lcAny → lcVoid → EST.Out Lean.Exception lcAny PUnit := _eval._lam_0 _x.9 _x.10;
-      let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 _y.3;
+      let _x.12 : EST.Out Lean.Exception lcAny PUnit := Lean.Elab.Command.liftTermElabM._redArg _f.11 a.1 a.2 a.3;
       return _x.12
 -/
 #guard_msgs in

tests/lean/seqToCodeIssue.lean.expected.out

@@ -1,5 +1,5 @@
 [Compiler.saveMono] size: 12
-    def f b _y.1 : EST.Out IO.Error lcAny PUnit :=
+    def f b a.1 : EST.Out IO.Error lcAny PUnit :=
       jp _jp.2 a _y.3 : EST.Out IO.Error lcAny PUnit :=
         let _x.4 := print a _y.3;
         cases _x.4 : EST.Out IO.Error lcAny PUnit
@@ -11,7 +11,7 @@
       cases b : EST.Out IO.Error lcAny PUnit
       | Bool.false =>
         let _x.10 := 1;
-        goto _jp.2 _x.10 _y.1
+        goto _jp.2 _x.10 a.1
       | Bool.true =>
         let _x.11 := 0;
-        goto _jp.2 _x.11 _y.1
+        goto _jp.2 _x.11 a.1

tests/lean/unboxStruct.lean.expected.out

@@ -1,6 +1,6 @@
 [Compiler.IR] [result]
     def test2 (x_1 : u32) (x_2 : void) : obj :=
-      let x_3 : obj := foo x_1 x_2;
+      let x_3 : obj := foo x_1 ◾;
       ret x_3
     def test2._boxed (x_1 : tobj) (x_2 : tagged) : obj :=
       let x_3 : u32 := unbox x_1;