From f115c3919bce9b56b25491dfbfcbf62160d644c9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Jan 2021 10:36:38 -0800
Subject: [PATCH] chore: update stage0

---
 stage0/src/Init/Data/Float.lean |   8 +++
 stage0/src/runtime/object.cpp   |   5 +-
 stage0/stdlib/Init/Data/Float.c | 100 ++++++++++++++++++++++++++++++++
 stage0/stdlib/Init/Prelude.c    |  12 ++++
 4 files changed, 122 insertions(+), 3 deletions(-)

diff --git a/stage0/src/Init/Data/Float.lean b/stage0/src/Init/Data/Float.lean
index d8762c87a8..ac99122aa6 100644
--- a/stage0/src/Init/Data/Float.lean
+++ b/stage0/src/Init/Data/Float.lean
@@ -35,6 +35,7 @@ instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
 @[extern c inline "#1 - #2"]  constant Float.sub : Float → Float → Float
 @[extern c inline "#1 * #2"]  constant Float.mul : Float → Float → Float
 @[extern c inline "#1 / #2"]  constant Float.div : Float → Float → Float
+@[extern c inline "(- #1)"]   constant Float.neg : Float → Float
 
 set_option bootstrap.gen_matcher_code false
 def Float.lt  : Float → Float → Prop := fun a b =>
@@ -49,6 +50,7 @@ instance : Add Float       := ⟨Float.add⟩
 instance : Sub Float       := ⟨Float.sub⟩
 instance : Mul Float       := ⟨Float.mul⟩
 instance : Div Float       := ⟨Float.div⟩
+instance : Neg Float       := ⟨Float.neg⟩
 instance : HasLess Float   := ⟨Float.lt⟩
 instance : HasLessEq Float := ⟨Float.le⟩
 
@@ -69,6 +71,12 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 
 @[extern "lean_float_to_string"] constant Float.toString : Float → String
 
+@[extern c inline "(uint8_t)#1"] constant Float.toUInt8 : Float → UInt8
+@[extern c inline "(uint16_t)#1"] constant Float.toUInt16 : Float → UInt16
+@[extern c inline "(uint32_t)#1"] constant Float.toUInt32 : Float → UInt32
+@[extern c inline "(uint64_t)#1"] constant Float.toUInt64 : Float → UInt64
+@[extern c inline "(size_t)#1"] constant Float.toUSize : Float → USize
+
 instance : ToString Float where
   toString := Float.toString
 
diff --git a/stage0/src/runtime/object.cpp b/stage0/src/runtime/object.cpp
index c921c4bd1e..b36e3b0660 100644
--- a/stage0/src/runtime/object.cpp
+++ b/stage0/src/runtime/object.cpp
@@ -25,8 +25,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 extern "C" void lean_panic(char const * msg) {
-    std::cerr << msg << "\n";
-    lean_unreachable();
+    std::cerr << "INTERNAL PANIC: " << msg << "\n";
     std::exit(1);
 }
 
@@ -59,7 +58,7 @@ extern "C" object * lean_panic_fn(object * default_val, object * msg) {
 }
 
 extern "C" object * lean_sorry(uint8) {
-    lean_panic("executing sorry");
+    lean_panic("executed 'sorry'");
 }
 
 extern "C" size_t lean_object_byte_size(lean_object * o) {
diff --git a/stage0/stdlib/Init/Data/Float.c b/stage0/stdlib/Init/Data/Float.c
index 382886f030..840c765576 100644
--- a/stage0/stdlib/Init/Data/Float.c
+++ b/stage0/stdlib/Init/Data/Float.c
@@ -34,10 +34,12 @@ extern uint8_t l_instDecidableTrue;
 lean_object* l_instReprFloat___boxed(lean_object*, lean_object*);
 double l_instOfNatFloat(lean_object*);
 uint8_t l_Float_beq(double, double);
+size_t l_Float_toUSize(double);
 double sqrt(double);
 lean_object* l_Float_log10___boxed(lean_object*);
 lean_object* l_Float_div___boxed(lean_object*, lean_object*);
 lean_object* l_Float_pow___boxed(lean_object*, lean_object*);
+lean_object* l_Float_toUInt64___boxed(lean_object*);
 lean_object* l_instHasLessFloat;
 lean_object* l_Float_cbrt___boxed(lean_object*);
 lean_object* l_Float_atanh___boxed(lean_object*);
@@ -45,11 +47,14 @@ lean_object* l_instReprAtomFloat;
 double atanh(double);
 lean_object* l_floatSpec___closed__1;
 uint8_t l_Float_decLe(double, double);
+lean_object* l_instNegFloat;
 double sinh(double);
 lean_object* l_floatSpec___closed__2;
+lean_object* l_Float_toUInt16___boxed(lean_object*);
 lean_object* l_Float_asin___boxed(lean_object*);
 lean_object* l_instInhabitedFloat;
 uint8_t l_Float_decLt(double, double);
+lean_object* l_Float_toUInt32___boxed(lean_object*);
 lean_object* l_Float_tan___boxed(lean_object*);
 lean_object* l_Float_sinh___boxed(lean_object*);
 lean_object* l_instAddFloat;
@@ -63,16 +68,19 @@ lean_object* l_Float_ofScientific___boxed(lean_object*, lean_object*, lean_objec
 lean_object* l_instToStringFloat;
 lean_object* l_Float_decLt___boxed(lean_object*, lean_object*);
 double cosh(double);
+uint16_t l_Float_toUInt16(double);
 double l_Float_sub(double, double);
 lean_object* l_floatSpec___elambda__1___boxed(lean_object*, lean_object*);
 double l_Float_add(double, double);
 double log(double);
+lean_object* l_Float_neg___boxed(lean_object*);
 lean_object* l_Float_log___boxed(lean_object*);
 lean_object* l_instPowFloat___closed__1;
 lean_object* l_instDivFloat;
 double log10(double);
 lean_object* l_Float_atan___boxed(lean_object*);
 lean_object* l_instInhabitedFloat___closed__1;
+lean_object* l_Float_toUSize___boxed(lean_object*);
 double atan(double);
 double atan2(double, double);
 double exp(double);
@@ -89,6 +97,7 @@ double acosh(double);
 lean_object* l_Float_atan2___boxed(lean_object*, lean_object*);
 double acos(double);
 lean_object* l_Float_sub___boxed(lean_object*, lean_object*);
+double l_Float_neg(double);
 lean_object* l_instMulFloat___closed__1;
 double cbrt(double);
 lean_object* l_Float_sqrt___boxed(lean_object*);
@@ -100,14 +109,19 @@ lean_object* l_Float_toString___boxed(lean_object*);
 double exp2(double);
 lean_object* l_instMulFloat;
 lean_object* l_Float_beq___boxed(lean_object*, lean_object*);
+lean_object* l_instNegFloat___closed__1;
 lean_object* l_instHasLessEqFloat;
 lean_object* l_instBEqFloat___closed__1;
 lean_object* l_Float_exp___boxed(lean_object*);
 lean_object* l_Float_add___boxed(lean_object*, lean_object*);
+uint64_t l_Float_toUInt64(double);
 lean_object* l_instPowFloat;
+uint32_t l_Float_toUInt32(double);
 lean_object* l_floatDecLt___boxed(lean_object*, lean_object*);
+uint8_t l_Float_toUInt8(double);
 lean_object* l_Float_log2___boxed(lean_object*);
 lean_object* l_Float_asinh___boxed(lean_object*);
+lean_object* l_Float_toUInt8___boxed(lean_object*);
 double l_Float_mul(double, double);
 lean_object* l_Float_acosh___boxed(lean_object*);
 uint8_t l_floatSpec___elambda__1(lean_object* x_1, lean_object* x_2) {
@@ -238,6 +252,17 @@ x_6 = lean_box_float(x_5);
 return x_6;
 }
 }
+lean_object* l_Float_neg___boxed(lean_object* x_1) {
+_start:
+{
+double x_2; double x_3; lean_object* x_4; 
+x_2 = lean_unbox_float(x_1);
+lean_dec(x_1);
+x_3 = (- x_2);
+x_4 = lean_box_float(x_3);
+return x_4;
+}
+}
 double l_instOfNatFloat(lean_object* x_1) {
 _start:
 {
@@ -320,6 +345,22 @@ x_1 = l_instDivFloat___closed__1;
 return x_1;
 }
 }
+static lean_object* _init_l_instNegFloat___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = lean_alloc_closure((void*)(l_Float_neg___boxed), 1, 0);
+return x_1;
+}
+}
+static lean_object* _init_l_instNegFloat() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_instNegFloat___closed__1;
+return x_1;
+}
+}
 static lean_object* _init_l_instHasLessFloat() {
 _start:
 {
@@ -443,6 +484,61 @@ x_3 = lean_float_to_string(x_2);
 return x_3;
 }
 }
+lean_object* l_Float_toUInt8___boxed(lean_object* x_1) {
+_start:
+{
+double x_2; uint8_t x_3; lean_object* x_4; 
+x_2 = lean_unbox_float(x_1);
+lean_dec(x_1);
+x_3 = (uint8_t)x_2;
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* l_Float_toUInt16___boxed(lean_object* x_1) {
+_start:
+{
+double x_2; uint16_t x_3; lean_object* x_4; 
+x_2 = lean_unbox_float(x_1);
+lean_dec(x_1);
+x_3 = (uint16_t)x_2;
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* l_Float_toUInt32___boxed(lean_object* x_1) {
+_start:
+{
+double x_2; uint32_t x_3; lean_object* x_4; 
+x_2 = lean_unbox_float(x_1);
+lean_dec(x_1);
+x_3 = (uint32_t)x_2;
+x_4 = lean_box_uint32(x_3);
+return x_4;
+}
+}
+lean_object* l_Float_toUInt64___boxed(lean_object* x_1) {
+_start:
+{
+double x_2; uint64_t x_3; lean_object* x_4; 
+x_2 = lean_unbox_float(x_1);
+lean_dec(x_1);
+x_3 = (uint64_t)x_2;
+x_4 = lean_box_uint64(x_3);
+return x_4;
+}
+}
+lean_object* l_Float_toUSize___boxed(lean_object* x_1) {
+_start:
+{
+double x_2; size_t x_3; lean_object* x_4; 
+x_2 = lean_unbox_float(x_1);
+lean_dec(x_1);
+x_3 = (size_t)x_2;
+x_4 = lean_box_usize(x_3);
+return x_4;
+}
+}
 static lean_object* _init_l_instToStringFloat___closed__1() {
 _start:
 {
@@ -807,6 +903,10 @@ l_instDivFloat___closed__1 = _init_l_instDivFloat___closed__1();
 lean_mark_persistent(l_instDivFloat___closed__1);
 l_instDivFloat = _init_l_instDivFloat();
 lean_mark_persistent(l_instDivFloat);
+l_instNegFloat___closed__1 = _init_l_instNegFloat___closed__1();
+lean_mark_persistent(l_instNegFloat___closed__1);
+l_instNegFloat = _init_l_instNegFloat();
+lean_mark_persistent(l_instNegFloat);
 l_instHasLessFloat = _init_l_instHasLessFloat();
 lean_mark_persistent(l_instHasLessFloat);
 l_instHasLessEqFloat = _init_l_instHasLessEqFloat();
diff --git a/stage0/stdlib/Init/Prelude.c b/stage0/stdlib/Init/Prelude.c
index e0bbb27256..5b08c1c233 100644
--- a/stage0/stdlib/Init/Prelude.c
+++ b/stage0/stdlib/Init/Prelude.c
@@ -332,6 +332,7 @@ lean_object* l___private_Init_Prelude_0__Lean_extractImported_match__1___rarg___
 lean_object* l_instMonadWithReaderOfReaderT___rarg(lean_object*, lean_object*, lean_object*);
 uint32_t l_Char_utf8Size___closed__2;
 lean_object* l_Lean_replaceRef_match__1(lean_object*);
+lean_object* l_sorryAx___boxed(lean_object*, lean_object*);
 lean_object* l_modify(lean_object*, lean_object*);
 lean_object* l_UInt8_val___boxed(lean_object*);
 lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*, lean_object*);
@@ -690,6 +691,7 @@ lean_object* l_instDecidableOr_match__3(lean_object*, lean_object*);
 lean_object* l_cast(lean_object*, lean_object*, lean_object*);
 lean_object* l_instHDiv___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Macro_instMonadQuotationMacroM___closed__1;
+lean_object* lean_sorry(uint8_t);
 lean_object* l_liftM___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_instMonadExceptOfReaderT___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@@ -1230,6 +1232,16 @@ lean_dec(x_2);
 return x_3;
 }
 }
+lean_object* l_sorryAx___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = lean_unbox(x_2);
+lean_dec(x_2);
+x_4 = lean_sorry(x_3);
+return x_4;
+}
+}
 lean_object* l_arbitrary___rarg(lean_object* x_1) {
 _start:
 {