From 16f6da6a626da61fa3f4617c57740fb53b8dd37e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 Feb 2019 15:28:15 -0800
Subject: [PATCH] chore(boot): update

---
 src/boot/init/core.cpp        | 111 --------------
 src/boot/init/lean/format.cpp | 213 +++++++++++++-------------
 src/boot/init/lean/trace.cpp  | 278 +++++++++++++++++-----------------
 src/boot/init/version.cpp     |   2 +-
 4 files changed, 251 insertions(+), 353 deletions(-)

diff --git a/src/boot/init/core.cpp b/src/boot/init/core.cpp
index 25f9d676a4..790d56d684 100644
--- a/src/boot/init/core.cpp
+++ b/src/boot/init/core.cpp
@@ -13,7 +13,6 @@ typedef lean::object obj;
 obj* l_psum_sizeof(obj*, obj*);
 obj* l_sigma_sizeof___main___rarg(obj*, obj*, obj*);
 obj* l_eq_ndrec__on___rarg(obj*);
-obj* l_thunk_map(obj*, obj*);
 obj* l_bool_has__sizeof;
 obj* l_quot_rec__on__subsingleton___rarg(obj*, obj*);
 obj* l_total;
@@ -21,13 +20,11 @@ obj* l_implies_decidable___rarg(obj*, obj*);
 obj* l_psigma_has__sizeof(obj*, obj*);
 obj* l_nat_add___main(obj*, obj*);
 obj* l_quotient_rec__on__subsingleton_u_2082___at_quotient_decidable__eq___spec__1___rarg(obj*, obj*, obj*);
-obj* l_thunk_bind___rarg(obj*, obj*, unsigned char);
 obj* l_eq_ndrec(obj*, obj*, obj*);
 obj* l_prod_inhabited___rarg(obj*, obj*);
 obj* l_prod_sizeof___main(obj*, obj*);
 obj* l_subtype_inhabited___rarg(obj*, obj*);
 obj* l_decidable_to__bool(obj*);
-obj* l_thunk_pure___rarg___boxed(obj*, obj*);
 obj* l_sum_sizeof___main(obj*, obj*);
 obj* l_punit_sizeof(unsigned char);
 obj* l_inline(obj*);
@@ -57,7 +54,6 @@ obj* l_prod_sizeof(obj*, obj*);
 unsigned char l_bxor___main(unsigned char, unsigned char);
 unsigned char l_unit_star;
 obj* l_exists_intro;
-obj* l_thunk_map___rarg(obj*, obj*, unsigned char);
 obj* l___private_2312050019__extfun__app(obj*, obj*);
 obj* l_or_intro__right;
 obj* l_bit1(obj*);
@@ -107,7 +103,6 @@ obj* l_false_elim___boxed(obj*, obj*);
 unsigned char l_band(unsigned char, unsigned char);
 obj* l_false_elim(obj*, unsigned char);
 obj* l_std_priority_max;
-obj* l_thunk_pure(obj*);
 obj* l_punit_sizeof___main(unsigned char);
 unsigned char l_bor(unsigned char, unsigned char);
 obj* l_option_sizeof___main(obj*);
@@ -124,7 +119,6 @@ obj* l_psum_sizeof___main___rarg(obj*, obj*, obj*);
 obj* l_subrelation;
 obj* l_quot_rec__on___rarg(obj*, obj*, obj*);
 obj* l_bor___boxed(obj*, obj*);
-obj* l_thunk_bind(obj*, obj*);
 obj* l_ite(obj*);
 obj* l_eq_ndrec___rarg(obj*, obj*, obj*);
 obj* l_or_by__cases___rarg(obj*, obj*, obj*, obj*, obj*, obj*);
@@ -140,7 +134,6 @@ obj* l_sum_sizeof(obj*, obj*);
 obj* l_type__eq__of__heq;
 obj* l_inv__image;
 obj* l_punit_subsingleton;
-obj* l_thunk_get___rarg(obj*);
 obj* l_bool_inhabited___boxed;
 obj* l_list_sizeof___main(obj*);
 obj* l_xor;
@@ -197,7 +190,6 @@ obj* l_iff_decidable___rarg(obj*, obj*);
 obj* l_std_prec_max__plus;
 obj* l_bit0(obj*);
 obj* l_exists__prop__decidable___rarg(obj*, obj*);
-obj* l_thunk_bind___rarg___boxed(obj*, obj*, obj*);
 obj* l_prod_has__sizeof(obj*, obj*);
 obj* l_decidable_rec__on__true___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_decidable_to__bool___rarg___boxed(obj*);
@@ -247,7 +239,6 @@ obj* l_sigma_has__sizeof___rarg(obj*, obj*);
 obj* l_true_inhabited;
 obj* l_pi_subsingleton;
 obj* l_forall__prop__decidable___rarg(obj*, obj*);
-obj* l_thunk_get(obj*);
 obj* l_ne_decidable___rarg(obj*, obj*, obj*);
 obj* l_and__implies;
 obj* l_anti__symmetric;
@@ -286,7 +277,6 @@ obj* l_psigma_sizeof___main___at_psigma_has__sizeof___spec__2(obj*, obj*);
 obj* l_quotient_mk(obj*, obj*);
 obj* l_typed__expr(obj*);
 obj* l_not_decidable(obj*);
-obj* l_thunk_pure___rarg(obj*, unsigned char);
 obj* l_sum_decidable__eq___rarg(obj*, obj*, obj*, obj*);
 obj* l_cast(obj*, obj*, obj*);
 obj* l_quotient_decidable__eq(obj*);
@@ -354,7 +344,6 @@ obj* l_prod_map___rarg(obj*, obj*, obj*);
 obj* l_subsingleton_helim;
 obj* l_id__rhs___rarg(obj*);
 unsigned char l_bnot(unsigned char);
-obj* l_thunk_map___rarg___boxed(obj*, obj*, obj*);
 obj* l_decidable_by__cases___rarg(obj*, obj*, obj*);
 obj* l_decidable__of__decidable__of__iff(obj*, obj*);
 obj* l_right__commutative;
@@ -519,106 +508,6 @@ x_1 = lean::box(x_0);
 return x_1;
 }
 }
-obj* l_thunk_pure___rarg(obj* x_0, unsigned char x_1) {
-_start:
-{
-return x_0;
-}
-}
-obj* l_thunk_pure(obj* x_0) {
-_start:
-{
-obj* x_2; 
-lean::dec(x_0);
-x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_pure___rarg___boxed), 2, 0);
-return x_2;
-}
-}
-obj* l_thunk_pure___rarg___boxed(obj* x_0, obj* x_1) {
-_start:
-{
-unsigned char x_2; obj* x_3; 
-x_2 = lean::unbox(x_1);
-x_3 = l_thunk_pure___rarg(x_0, x_2);
-return x_3;
-}
-}
-obj* l_thunk_get___rarg(obj* x_0) {
-_start:
-{
-unsigned char x_1; obj* x_2; obj* x_3; 
-x_1 = 0;
-x_2 = lean::box(x_1);
-x_3 = lean::apply_1(x_0, x_2);
-return x_3;
-}
-}
-obj* l_thunk_get(obj* x_0) {
-_start:
-{
-obj* x_2; 
-lean::dec(x_0);
-x_2 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_get___rarg), 1, 0);
-return x_2;
-}
-}
-obj* l_thunk_map___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
-_start:
-{
-obj* x_3; obj* x_4; 
-x_3 = l_thunk_get___rarg(x_1);
-x_4 = lean::apply_1(x_0, x_3);
-return x_4;
-}
-}
-obj* l_thunk_map(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_4; 
-lean::dec(x_1);
-lean::dec(x_0);
-x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_map___rarg___boxed), 3, 0);
-return x_4;
-}
-}
-obj* l_thunk_map___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-unsigned char x_3; obj* x_4; 
-x_3 = lean::unbox(x_2);
-x_4 = l_thunk_map___rarg(x_0, x_1, x_3);
-return x_4;
-}
-}
-obj* l_thunk_bind___rarg(obj* x_0, obj* x_1, unsigned char x_2) {
-_start:
-{
-obj* x_3; obj* x_4; obj* x_5; 
-x_3 = l_thunk_get___rarg(x_0);
-x_4 = lean::apply_1(x_1, x_3);
-x_5 = l_thunk_get___rarg(x_4);
-return x_5;
-}
-}
-obj* l_thunk_bind(obj* x_0, obj* x_1) {
-_start:
-{
-obj* x_4; 
-lean::dec(x_1);
-lean::dec(x_0);
-x_4 = lean::alloc_closure(reinterpret_cast<void*>(l_thunk_bind___rarg___boxed), 3, 0);
-return x_4;
-}
-}
-obj* l_thunk_bind___rarg___boxed(obj* x_0, obj* x_1, obj* x_2) {
-_start:
-{
-unsigned char x_3; obj* x_4; 
-x_3 = lean::unbox(x_2);
-x_4 = l_thunk_bind___rarg(x_0, x_1, x_3);
-return x_4;
-}
-}
 obj* l_task_pure___rarg(obj* x_0, unsigned char x_1) {
 _start:
 {
diff --git a/src/boot/init/lean/format.cpp b/src/boot/init/lean/format.cpp
index 447a4c3364..18cf079797 100644
--- a/src/boot/init/lean/format.cpp
+++ b/src/boot/init/lean/format.cpp
@@ -54,7 +54,6 @@ obj* l_lean_format_sbracket___closed__1;
 obj* l_lean_format_repr___main___closed__6;
 obj* l_lean_format_sbracket(obj*);
 obj* l_lean_prod__has__to__format(obj*, obj*);
-obj* l_thunk_get___rarg(obj*);
 obj* l_lean_format_space__upto__line_x_27___main___lambda__1(obj*, obj*, unsigned char);
 obj* l_lean_nat__has__to__format(obj*);
 obj* l_lean_string__has__to__format(obj*);
@@ -375,53 +374,54 @@ return x_1;
 }
 lbl_4:
 {
-obj* x_13; unsigned char x_14; 
-x_13 = l_thunk_get___rarg(x_2);
-x_14 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1 + 1);
-if (x_14 == 0)
-{
-unsigned char x_15; 
-x_15 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1);
+obj* x_13; unsigned char x_15; 
+x_13 = lean::thunk_get(x_2);
+lean::dec(x_2);
+x_15 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1 + 1);
 if (x_15 == 0)
 {
-obj* x_16; obj* x_19; obj* x_22; obj* x_25; 
-x_16 = lean::cnstr_get(x_1, 0);
-lean::inc(x_16);
-lean::dec(x_1);
-x_19 = lean::cnstr_get(x_13, 0);
-lean::inc(x_19);
-lean::dec(x_13);
-x_22 = lean::nat_add(x_16, x_19);
-lean::dec(x_19);
-lean::dec(x_16);
-x_25 = lean::nat_dec_lt(x_0, x_22);
-lean::dec(x_0);
-if (lean::obj_tag(x_25) == 0)
+unsigned char x_16; 
+x_16 = lean::cnstr_get_scalar<unsigned char>(x_13, sizeof(void*)*1);
+if (x_16 == 0)
 {
-unsigned char x_28; obj* x_29; obj* x_30; obj* x_31; 
-lean::dec(x_25);
-x_28 = 0;
-x_29 = lean::alloc_cnstr(0, 1, 2);
-lean::cnstr_set(x_29, 0, x_22);
-lean::cnstr_set_scalar(x_29, sizeof(void*)*1, x_28);
-x_30 = x_29;
-lean::cnstr_set_scalar(x_30, sizeof(void*)*1 + 1, x_28);
+obj* x_17; obj* x_20; obj* x_23; obj* x_26; 
+x_17 = lean::cnstr_get(x_1, 0);
+lean::inc(x_17);
+lean::dec(x_1);
+x_20 = lean::cnstr_get(x_13, 0);
+lean::inc(x_20);
+lean::dec(x_13);
+x_23 = lean::nat_add(x_17, x_20);
+lean::dec(x_20);
+lean::dec(x_17);
+x_26 = lean::nat_dec_lt(x_0, x_23);
+lean::dec(x_0);
+if (lean::obj_tag(x_26) == 0)
+{
+unsigned char x_29; obj* x_30; obj* x_31; obj* x_32; 
+lean::dec(x_26);
+x_29 = 0;
+x_30 = lean::alloc_cnstr(0, 1, 2);
+lean::cnstr_set(x_30, 0, x_23);
+lean::cnstr_set_scalar(x_30, sizeof(void*)*1, x_29);
 x_31 = x_30;
-return x_31;
+lean::cnstr_set_scalar(x_31, sizeof(void*)*1 + 1, x_29);
+x_32 = x_31;
+return x_32;
 }
 else
 {
-unsigned char x_33; unsigned char x_34; obj* x_35; obj* x_36; obj* x_37; 
-lean::dec(x_25);
-x_33 = 0;
-x_34 = 1;
-x_35 = lean::alloc_cnstr(0, 1, 2);
-lean::cnstr_set(x_35, 0, x_22);
-lean::cnstr_set_scalar(x_35, sizeof(void*)*1, x_33);
-x_36 = x_35;
-lean::cnstr_set_scalar(x_36, sizeof(void*)*1 + 1, x_34);
+unsigned char x_34; unsigned char x_35; obj* x_36; obj* x_37; obj* x_38; 
+lean::dec(x_26);
+x_34 = 0;
+x_35 = 1;
+x_36 = lean::alloc_cnstr(0, 1, 2);
+lean::cnstr_set(x_36, 0, x_23);
+lean::cnstr_set_scalar(x_36, sizeof(void*)*1, x_34);
 x_37 = x_36;
-return x_37;
+lean::cnstr_set_scalar(x_37, sizeof(void*)*1 + 1, x_35);
+x_38 = x_37;
+return x_38;
 }
 }
 else
@@ -433,46 +433,46 @@ return x_13;
 }
 else
 {
-if (x_14 == 0)
+if (x_15 == 0)
 {
-obj* x_40; obj* x_43; obj* x_46; obj* x_49; 
-x_40 = lean::cnstr_get(x_1, 0);
-lean::inc(x_40);
+obj* x_41; obj* x_44; obj* x_47; obj* x_50; 
+x_41 = lean::cnstr_get(x_1, 0);
+lean::inc(x_41);
 lean::dec(x_1);
-x_43 = lean::cnstr_get(x_13, 0);
-lean::inc(x_43);
+x_44 = lean::cnstr_get(x_13, 0);
+lean::inc(x_44);
 lean::dec(x_13);
-x_46 = lean::nat_add(x_40, x_43);
-lean::dec(x_43);
-lean::dec(x_40);
-x_49 = lean::nat_dec_lt(x_0, x_46);
+x_47 = lean::nat_add(x_41, x_44);
+lean::dec(x_44);
+lean::dec(x_41);
+x_50 = lean::nat_dec_lt(x_0, x_47);
 lean::dec(x_0);
-if (lean::obj_tag(x_49) == 0)
+if (lean::obj_tag(x_50) == 0)
 {
-unsigned char x_52; obj* x_53; obj* x_54; obj* x_55; 
-lean::dec(x_49);
-x_52 = 0;
-x_53 = lean::alloc_cnstr(0, 1, 2);
-lean::cnstr_set(x_53, 0, x_46);
-lean::cnstr_set_scalar(x_53, sizeof(void*)*1, x_52);
-x_54 = x_53;
-lean::cnstr_set_scalar(x_54, sizeof(void*)*1 + 1, x_52);
+unsigned char x_53; obj* x_54; obj* x_55; obj* x_56; 
+lean::dec(x_50);
+x_53 = 0;
+x_54 = lean::alloc_cnstr(0, 1, 2);
+lean::cnstr_set(x_54, 0, x_47);
+lean::cnstr_set_scalar(x_54, sizeof(void*)*1, x_53);
 x_55 = x_54;
-return x_55;
+lean::cnstr_set_scalar(x_55, sizeof(void*)*1 + 1, x_53);
+x_56 = x_55;
+return x_56;
 }
 else
 {
-unsigned char x_57; unsigned char x_58; obj* x_59; obj* x_60; obj* x_61; 
-lean::dec(x_49);
-x_57 = 0;
-x_58 = 1;
-x_59 = lean::alloc_cnstr(0, 1, 2);
-lean::cnstr_set(x_59, 0, x_46);
-lean::cnstr_set_scalar(x_59, sizeof(void*)*1, x_57);
-x_60 = x_59;
-lean::cnstr_set_scalar(x_60, sizeof(void*)*1 + 1, x_58);
+unsigned char x_58; unsigned char x_59; obj* x_60; obj* x_61; obj* x_62; 
+lean::dec(x_50);
+x_58 = 0;
+x_59 = 1;
+x_60 = lean::alloc_cnstr(0, 1, 2);
+lean::cnstr_set(x_60, 0, x_47);
+lean::cnstr_set_scalar(x_60, sizeof(void*)*1, x_58);
 x_61 = x_60;
-return x_61;
+lean::cnstr_set_scalar(x_61, sizeof(void*)*1 + 1, x_59);
+x_62 = x_61;
+return x_62;
 }
 }
 else
@@ -556,7 +556,7 @@ goto _start;
 }
 case 4:
 {
-obj* x_32; obj* x_34; obj* x_38; obj* x_40; obj* x_41; 
+obj* x_32; obj* x_34; obj* x_38; obj* x_40; obj* x_41; obj* x_42; 
 x_32 = lean::cnstr_get(x_0, 0);
 lean::inc(x_32);
 x_34 = lean::cnstr_get(x_0, 1);
@@ -568,16 +568,17 @@ lean::inc(x_1);
 x_40 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_format_space__upto__line___main___lambda__1___boxed), 3, 2);
 lean::closure_set(x_40, 0, x_34);
 lean::closure_set(x_40, 1, x_1);
-x_41 = l___private_3682637481__merge(x_1, x_38, x_40);
-return x_41;
+x_41 = lean::mk_thunk(x_40);
+x_42 = l___private_3682637481__merge(x_1, x_38, x_41);
+return x_42;
 }
 default:
 {
-obj* x_42; 
-x_42 = lean::cnstr_get(x_0, 1);
-lean::inc(x_42);
+obj* x_43; 
+x_43 = lean::cnstr_get(x_0, 1);
+lean::inc(x_43);
 lean::dec(x_0);
-x_0 = x_42;
+x_0 = x_43;
 goto _start;
 }
 }
@@ -653,7 +654,7 @@ return x_4;
 }
 else
 {
-obj* x_6; obj* x_8; obj* x_11; obj* x_15; obj* x_17; obj* x_18; 
+obj* x_6; obj* x_8; obj* x_11; obj* x_15; obj* x_17; obj* x_18; obj* x_19; 
 x_6 = lean::cnstr_get(x_0, 0);
 lean::inc(x_6);
 x_8 = lean::cnstr_get(x_0, 1);
@@ -668,8 +669,9 @@ lean::inc(x_1);
 x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_format_space__upto__line_x_27___main___lambda__1___boxed), 3, 2);
 lean::closure_set(x_17, 0, x_8);
 lean::closure_set(x_17, 1, x_1);
-x_18 = l___private_3682637481__merge(x_1, x_15, x_17);
-return x_18;
+x_18 = lean::mk_thunk(x_17);
+x_19 = l___private_3682637481__merge(x_1, x_15, x_18);
+return x_19;
 }
 }
 }
@@ -913,7 +915,7 @@ goto _start;
 }
 default:
 {
-obj* x_103; obj* x_105; obj* x_110; obj* x_113; obj* x_115; unsigned char x_116; 
+obj* x_103; obj* x_105; obj* x_110; obj* x_113; obj* x_114; obj* x_116; unsigned char x_117; 
 x_103 = lean::cnstr_get(x_14, 0);
 lean::inc(x_103);
 x_105 = lean::cnstr_get(x_14, 1);
@@ -927,50 +929,51 @@ lean::inc(x_9);
 x_113 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_format_space__upto__line_x_27___main___lambda__1___boxed), 3, 2);
 lean::closure_set(x_113, 0, x_9);
 lean::closure_set(x_113, 1, x_0);
+x_114 = lean::mk_thunk(x_113);
 lean::inc(x_0);
-x_115 = l___private_3682637481__merge(x_0, x_110, x_113);
-x_116 = lean::cnstr_get_scalar<unsigned char>(x_115, sizeof(void*)*1 + 1);
-lean::dec(x_115);
-if (x_116 == 0)
+x_116 = l___private_3682637481__merge(x_0, x_110, x_114);
+x_117 = lean::cnstr_get_scalar<unsigned char>(x_116, sizeof(void*)*1 + 1);
+lean::dec(x_116);
+if (x_117 == 0)
 {
-obj* x_119; obj* x_120; 
+obj* x_120; obj* x_121; 
 lean::dec(x_105);
 if (lean::is_scalar(x_16)) {
- x_119 = lean::alloc_cnstr(0, 2, 0);
+ x_120 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_119 = x_16;
+ x_120 = x_16;
 }
-lean::cnstr_set(x_119, 0, x_12);
-lean::cnstr_set(x_119, 1, x_103);
+lean::cnstr_set(x_120, 0, x_12);
+lean::cnstr_set(x_120, 1, x_103);
 if (lean::is_scalar(x_11)) {
- x_120 = lean::alloc_cnstr(1, 2, 0);
+ x_121 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_120 = x_11;
+ x_121 = x_11;
 }
-lean::cnstr_set(x_120, 0, x_119);
-lean::cnstr_set(x_120, 1, x_9);
-x_3 = x_120;
+lean::cnstr_set(x_121, 0, x_120);
+lean::cnstr_set(x_121, 1, x_9);
+x_3 = x_121;
 goto _start;
 }
 else
 {
-obj* x_123; obj* x_124; 
+obj* x_124; obj* x_125; 
 lean::dec(x_103);
 if (lean::is_scalar(x_16)) {
- x_123 = lean::alloc_cnstr(0, 2, 0);
+ x_124 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_123 = x_16;
+ x_124 = x_16;
 }
-lean::cnstr_set(x_123, 0, x_12);
-lean::cnstr_set(x_123, 1, x_105);
+lean::cnstr_set(x_124, 0, x_12);
+lean::cnstr_set(x_124, 1, x_105);
 if (lean::is_scalar(x_11)) {
- x_124 = lean::alloc_cnstr(1, 2, 0);
+ x_125 = lean::alloc_cnstr(1, 2, 0);
 } else {
- x_124 = x_11;
+ x_125 = x_11;
 }
-lean::cnstr_set(x_124, 0, x_123);
-lean::cnstr_set(x_124, 1, x_9);
-x_3 = x_124;
+lean::cnstr_set(x_125, 0, x_124);
+lean::cnstr_set(x_125, 1, x_9);
+x_3 = x_125;
 goto _start;
 }
 }
diff --git a/src/boot/init/lean/trace.cpp b/src/boot/init/lean/trace.cpp
index cbe30a44ea..42f103deeb 100644
--- a/src/boot/init/lean/trace.cpp
+++ b/src/boot/init/lean/trace.cpp
@@ -36,7 +36,6 @@ obj* l_lean_trace_trace__map;
 obj* l_lean_trace_lean_trace_monad__tracer(obj*);
 extern obj* l_lean_format_join___closed__1;
 obj* l_rbnode_insert___at_lean_trace_lean_trace_monad__tracer___spec__2(obj*, obj*, obj*);
-obj* l_thunk_get___rarg(obj*);
 obj* l_lean_position_decidable__lt___main(obj*, obj*);
 obj* l_state__t_monad___rarg(obj*);
 obj* l_lean_trace_trace__t_run___rarg(obj*, obj*, obj*);
@@ -181,14 +180,15 @@ return x_2;
 obj* l_lean_trace_trace___rarg(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
-obj* x_4; obj* x_7; obj* x_8; 
+obj* x_4; obj* x_7; obj* x_8; obj* x_9; 
 x_4 = lean::cnstr_get(x_1, 1);
 lean::inc(x_4);
 lean::dec(x_1);
 x_7 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_trace___rarg___lambda__1___boxed), 2, 1);
 lean::closure_set(x_7, 0, x_0);
-x_8 = lean::apply_4(x_4, lean::box(0), x_2, x_3, x_7);
-return x_8;
+x_8 = lean::mk_thunk(x_7);
+x_9 = lean::apply_4(x_4, lean::box(0), x_2, x_3, x_8);
+return x_9;
 }
 }
 obj* l_lean_trace_trace___rarg___lambda__1(obj* x_0, unsigned char x_1) {
@@ -321,20 +321,21 @@ return x_29;
 obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5) {
 _start:
 {
-obj* x_6; obj* x_9; obj* x_10; obj* x_12; obj* x_13; 
+obj* x_6; obj* x_9; obj* x_11; obj* x_13; obj* x_14; 
 x_6 = lean::cnstr_get(x_5, 1);
 lean::inc(x_6);
 lean::dec(x_5);
-x_9 = l_thunk_get___rarg(x_0);
-x_10 = lean::apply_1(x_9, x_6);
+x_9 = lean::thunk_get(x_0);
+lean::dec(x_0);
+x_11 = lean::apply_1(x_9, x_6);
 lean::inc(x_4);
-x_12 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__2), 5, 4);
-lean::closure_set(x_12, 0, x_1);
-lean::closure_set(x_12, 1, x_2);
-lean::closure_set(x_12, 2, x_3);
-lean::closure_set(x_12, 3, x_4);
-x_13 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_10, x_12);
-return x_13;
+x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__2), 5, 4);
+lean::closure_set(x_13, 0, x_1);
+lean::closure_set(x_13, 1, x_2);
+lean::closure_set(x_13, 2, x_3);
+lean::closure_set(x_13, 3, x_4);
+x_14 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_11, x_13);
+return x_14;
 }
 }
 obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__4(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
@@ -359,83 +360,85 @@ lean::dec(x_7);
 x_17 = l_lean_kvmap_get__bool(x_14, x_5);
 if (lean::obj_tag(x_17) == 0)
 {
-obj* x_24; obj* x_25; 
+obj* x_24; obj* x_26; 
 lean::dec(x_11);
 lean::dec(x_4);
 lean::dec(x_0);
 lean::dec(x_1);
 lean::dec(x_3);
 lean::dec(x_17);
-x_24 = l_thunk_get___rarg(x_2);
-x_25 = lean::apply_1(x_24, x_9);
-return x_25;
+x_24 = lean::thunk_get(x_2);
+lean::dec(x_2);
+x_26 = lean::apply_1(x_24, x_9);
+return x_26;
 }
 else
 {
-obj* x_26; unsigned char x_29; 
-x_26 = lean::cnstr_get(x_17, 0);
-lean::inc(x_26);
+obj* x_27; unsigned char x_30; 
+x_27 = lean::cnstr_get(x_17, 0);
+lean::inc(x_27);
 lean::dec(x_17);
-x_29 = lean::unbox(x_26);
-lean::dec(x_26);
-if (x_29 == 0)
+x_30 = lean::unbox(x_27);
+lean::dec(x_27);
+if (x_30 == 0)
 {
-obj* x_36; obj* x_37; 
+obj* x_37; obj* x_39; 
 lean::dec(x_11);
 lean::dec(x_4);
 lean::dec(x_0);
 lean::dec(x_1);
 lean::dec(x_3);
-x_36 = l_thunk_get___rarg(x_2);
-x_37 = lean::apply_1(x_36, x_9);
-return x_37;
+x_37 = lean::thunk_get(x_2);
+lean::dec(x_2);
+x_39 = lean::apply_1(x_37, x_9);
+return x_39;
 }
 else
 {
-unsigned char x_38; 
-x_38 = 0;
-x_12 = x_38;
+unsigned char x_40; 
+x_40 = 0;
+x_12 = x_40;
 goto lbl_13;
 }
 }
 lbl_13:
 {
-obj* x_39; obj* x_41; obj* x_45; obj* x_46; obj* x_47; unsigned char x_48; obj* x_49; obj* x_50; obj* x_52; obj* x_54; obj* x_55; 
-x_39 = lean::cnstr_get(x_9, 0);
-lean::inc(x_39);
-x_41 = lean::cnstr_get(x_9, 1);
+obj* x_41; obj* x_43; obj* x_47; obj* x_48; obj* x_49; unsigned char x_50; obj* x_51; obj* x_52; obj* x_54; obj* x_56; obj* x_57; 
+x_41 = lean::cnstr_get(x_9, 0);
 lean::inc(x_41);
+x_43 = lean::cnstr_get(x_9, 1);
+lean::inc(x_43);
 lean::dec(x_9);
 lean::inc(x_0);
-x_45 = lean::alloc_cnstr(1, 1, 0);
-lean::cnstr_set(x_45, 0, x_0);
-x_46 = lean::alloc_cnstr(0, 0, 0);
+x_47 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_47, 0, x_0);
+x_48 = lean::alloc_cnstr(0, 0, 0);
 ;
-x_47 = lean::alloc_cnstr(0, 4, 0);
-lean::cnstr_set(x_47, 0, x_39);
-lean::cnstr_set(x_47, 1, x_41);
-lean::cnstr_set(x_47, 2, x_45);
-lean::cnstr_set(x_47, 3, x_46);
-x_48 = 0;
-x_49 = lean::box(x_48);
+x_49 = lean::alloc_cnstr(0, 4, 0);
+lean::cnstr_set(x_49, 0, x_41);
+lean::cnstr_set(x_49, 1, x_43);
+lean::cnstr_set(x_49, 2, x_47);
+lean::cnstr_set(x_49, 3, x_48);
+x_50 = 0;
+x_51 = lean::box(x_50);
 if (lean::is_scalar(x_11)) {
- x_50 = lean::alloc_cnstr(0, 2, 0);
+ x_52 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_50 = x_11;
+ x_52 = x_11;
 }
-lean::cnstr_set(x_50, 0, x_49);
-lean::cnstr_set(x_50, 1, x_47);
+lean::cnstr_set(x_52, 0, x_51);
+lean::cnstr_set(x_52, 1, x_49);
 lean::inc(x_1);
-x_52 = lean::apply_2(x_1, lean::box(0), x_50);
+x_54 = lean::apply_2(x_1, lean::box(0), x_52);
 lean::inc(x_4);
-x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3), 6, 5);
-lean::closure_set(x_54, 0, x_2);
-lean::closure_set(x_54, 1, x_3);
-lean::closure_set(x_54, 2, x_0);
-lean::closure_set(x_54, 3, x_1);
-lean::closure_set(x_54, 4, x_4);
-x_55 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_52, x_54);
-return x_55;
+x_56 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__3), 6, 5);
+lean::closure_set(x_56, 0, x_2);
+lean::closure_set(x_56, 1, x_3);
+lean::closure_set(x_56, 2, x_0);
+lean::closure_set(x_56, 3, x_1);
+lean::closure_set(x_56, 4, x_4);
+x_57 = lean::apply_4(x_4, lean::box(0), lean::box(0), x_54, x_56);
+return x_57;
 }
 }
 }
@@ -570,21 +573,22 @@ return x_33;
 obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
 _start:
 {
-obj* x_7; obj* x_10; obj* x_11; obj* x_13; obj* x_14; 
+obj* x_7; obj* x_10; obj* x_12; obj* x_14; obj* x_15; 
 x_7 = lean::cnstr_get(x_6, 1);
 lean::inc(x_7);
 lean::dec(x_6);
-x_10 = l_thunk_get___rarg(x_0);
-x_11 = lean::apply_1(x_10, x_7);
+x_10 = lean::thunk_get(x_0);
+lean::dec(x_0);
+x_12 = lean::apply_1(x_10, x_7);
 lean::inc(x_5);
-x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__8), 6, 5);
-lean::closure_set(x_13, 0, x_1);
-lean::closure_set(x_13, 1, x_2);
-lean::closure_set(x_13, 2, x_3);
-lean::closure_set(x_13, 3, x_4);
-lean::closure_set(x_13, 4, x_5);
-x_14 = lean::apply_4(x_5, lean::box(0), lean::box(0), x_11, x_13);
-return x_14;
+x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__8), 6, 5);
+lean::closure_set(x_14, 0, x_1);
+lean::closure_set(x_14, 1, x_2);
+lean::closure_set(x_14, 2, x_3);
+lean::closure_set(x_14, 3, x_4);
+lean::closure_set(x_14, 4, x_5);
+x_15 = lean::apply_4(x_5, lean::box(0), lean::box(0), x_12, x_14);
+return x_15;
 }
 }
 obj* l_lean_trace_lean_trace_monad__tracer___rarg___lambda__10(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7, obj* x_8) {
@@ -605,7 +609,7 @@ if (lean::is_shared(x_8)) {
 }
 if (lean::obj_tag(x_9) == 0)
 {
-obj* x_23; obj* x_24; 
+obj* x_23; obj* x_25; 
 lean::dec(x_9);
 lean::dec(x_13);
 lean::dec(x_4);
@@ -615,105 +619,107 @@ lean::dec(x_7);
 lean::dec(x_1);
 lean::dec(x_2);
 lean::dec(x_3);
-x_23 = l_thunk_get___rarg(x_0);
-x_24 = lean::apply_1(x_23, x_11);
-return x_24;
+x_23 = lean::thunk_get(x_0);
+lean::dec(x_0);
+x_25 = lean::apply_1(x_23, x_11);
+return x_25;
 }
 else
 {
-obj* x_26; unsigned char x_28; unsigned char x_30; obj* x_33; 
+obj* x_27; unsigned char x_29; unsigned char x_31; obj* x_34; 
 lean::dec(x_9);
-x_26 = lean::cnstr_get(x_1, 0);
-lean::inc(x_26);
-lean::inc(x_26);
-x_33 = l_lean_kvmap_get__bool(x_26, x_7);
-if (lean::obj_tag(x_33) == 0)
+x_27 = lean::cnstr_get(x_1, 0);
+lean::inc(x_27);
+lean::inc(x_27);
+x_34 = l_lean_kvmap_get__bool(x_27, x_7);
+if (lean::obj_tag(x_34) == 0)
 {
-unsigned char x_39; 
+unsigned char x_40; 
 lean::dec(x_13);
 lean::dec(x_4);
 lean::dec(x_5);
 lean::dec(x_6);
-lean::dec(x_33);
-x_39 = 0;
-x_28 = x_39;
-goto lbl_29;
+lean::dec(x_34);
+x_40 = 0;
+x_29 = x_40;
+goto lbl_30;
 }
 else
 {
-obj* x_40; unsigned char x_43; 
-x_40 = lean::cnstr_get(x_33, 0);
-lean::inc(x_40);
-lean::dec(x_33);
-x_43 = lean::unbox(x_40);
-lean::dec(x_40);
-if (x_43 == 0)
+obj* x_41; unsigned char x_44; 
+x_41 = lean::cnstr_get(x_34, 0);
+lean::inc(x_41);
+lean::dec(x_34);
+x_44 = lean::unbox(x_41);
+lean::dec(x_41);
+if (x_44 == 0)
 {
-unsigned char x_49; 
+unsigned char x_50; 
 lean::dec(x_13);
 lean::dec(x_4);
 lean::dec(x_5);
 lean::dec(x_6);
-x_49 = 0;
-x_28 = x_49;
-goto lbl_29;
+x_50 = 0;
+x_29 = x_50;
+goto lbl_30;
 }
 else
 {
-unsigned char x_52; 
+unsigned char x_53; 
 lean::dec(x_11);
 lean::dec(x_3);
-x_52 = 0;
-x_30 = x_52;
-goto lbl_31;
+x_53 = 0;
+x_31 = x_53;
+goto lbl_32;
 }
 }
-lbl_29:
+lbl_30:
 {
-obj* x_53; obj* x_54; obj* x_55; obj* x_56; 
-x_53 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__6), 3, 2);
-lean::closure_set(x_53, 0, x_1);
-lean::closure_set(x_53, 1, x_26);
-x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__7), 2, 1);
-lean::closure_set(x_54, 0, x_2);
-x_55 = l_thunk_get___rarg(x_0);
-x_56 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_3, lean::box(0), x_53, x_54, x_55, x_11);
-return x_56;
+obj* x_54; obj* x_55; obj* x_56; obj* x_58; 
+x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__6), 3, 2);
+lean::closure_set(x_54, 0, x_1);
+lean::closure_set(x_54, 1, x_27);
+x_55 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__7), 2, 1);
+lean::closure_set(x_55, 0, x_2);
+x_56 = lean::thunk_get(x_0);
+lean::dec(x_0);
+x_58 = l_monad__state__adapter_adapt__state_x_27___at_lean_trace_lean_trace_monad__tracer___spec__4___rarg(x_3, lean::box(0), x_54, x_55, x_56, x_11);
+return x_58;
 }
-lbl_31:
+lbl_32:
 {
-obj* x_57; obj* x_59; obj* x_61; unsigned char x_62; obj* x_63; obj* x_64; obj* x_66; obj* x_68; obj* x_69; 
-x_57 = lean::cnstr_get(x_1, 1);
-lean::inc(x_57);
-x_59 = lean::alloc_cnstr(0, 0, 0);
-;
+obj* x_59; obj* x_61; obj* x_63; unsigned char x_64; obj* x_65; obj* x_66; obj* x_68; obj* x_70; obj* x_71; 
+x_59 = lean::cnstr_get(x_1, 1);
 lean::inc(x_59);
-x_61 = lean::alloc_cnstr(0, 4, 0);
-lean::cnstr_set(x_61, 0, x_26);
-lean::cnstr_set(x_61, 1, x_57);
-lean::cnstr_set(x_61, 2, x_2);
-lean::cnstr_set(x_61, 3, x_59);
-x_62 = 0;
-x_63 = lean::box(x_62);
+x_61 = lean::alloc_cnstr(0, 0, 0);
+;
+lean::inc(x_61);
+x_63 = lean::alloc_cnstr(0, 4, 0);
+lean::cnstr_set(x_63, 0, x_27);
+lean::cnstr_set(x_63, 1, x_59);
+lean::cnstr_set(x_63, 2, x_2);
+lean::cnstr_set(x_63, 3, x_61);
+x_64 = 0;
+x_65 = lean::box(x_64);
 if (lean::is_scalar(x_13)) {
- x_64 = lean::alloc_cnstr(0, 2, 0);
+ x_66 = lean::alloc_cnstr(0, 2, 0);
 } else {
- x_64 = x_13;
+ x_66 = x_13;
 }
-lean::cnstr_set(x_64, 0, x_63);
-lean::cnstr_set(x_64, 1, x_61);
+lean::cnstr_set(x_66, 0, x_65);
+lean::cnstr_set(x_66, 1, x_63);
 lean::inc(x_4);
-x_66 = lean::apply_2(x_4, lean::box(0), x_64);
+x_68 = lean::apply_2(x_4, lean::box(0), x_66);
 lean::inc(x_6);
-x_68 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9), 7, 6);
-lean::closure_set(x_68, 0, x_0);
-lean::closure_set(x_68, 1, x_1);
-lean::closure_set(x_68, 2, x_5);
-lean::closure_set(x_68, 3, x_59);
-lean::closure_set(x_68, 4, x_4);
-lean::closure_set(x_68, 5, x_6);
-x_69 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_66, x_68);
-return x_69;
+x_70 = lean::alloc_closure(reinterpret_cast<void*>(l_lean_trace_lean_trace_monad__tracer___rarg___lambda__9), 7, 6);
+lean::closure_set(x_70, 0, x_0);
+lean::closure_set(x_70, 1, x_1);
+lean::closure_set(x_70, 2, x_5);
+lean::closure_set(x_70, 3, x_61);
+lean::closure_set(x_70, 4, x_4);
+lean::closure_set(x_70, 5, x_6);
+x_71 = lean::apply_4(x_6, lean::box(0), lean::box(0), x_68, x_70);
+return x_71;
 }
 }
 }
diff --git a/src/boot/init/version.cpp b/src/boot/init/version.cpp
index c8300b17f6..943628c5ae 100644
--- a/src/boot/init/version.cpp
+++ b/src/boot/init/version.cpp
@@ -35,7 +35,7 @@ obj* _init_l_lean_githash() {
 _start:
 {
 obj* x_0; 
-x_0 = lean::mk_string("4d668362551df18e7f1949f65c281a7d865dc97a");
+x_0 = lean::mk_string("7c355d3ba60e86b89fc9da89ee7ea2cfd24c3cf3");
 return x_0;
 }
 }