From 646f2bdefe65bd09816cb9a8aa0fa26ec4d805a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2020 16:32:05 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/CMakeLists.txt | 8 + stage0/src/Init/Data/Char/Basic.lean | 2 +- stage0/src/Init/Data/UInt.lean | 4 +- stage0/src/Init/Fix.lean | 12 +- stage0/src/Init/Prelude.lean | 75 ++++--- stage0/src/Lean/Compiler/IR/EmitC.lean | 2 +- stage0/src/Lean/Data/Json/Parser.lean | 4 +- stage0/src/Std/Data/PersistentArray.lean | 2 +- stage0/src/bin/leanc.in | 4 +- stage0/stdlib/Init/Prelude.c | 240 ++++++++++++--------- stage0/stdlib/Lean/Compiler/ConstFolding.c | 8 +- stage0/stdlib/Lean/Compiler/IR/EmitC.c | 4 +- stage0/stdlib/Lean/Data/Json/Parser.c | 10 +- stage0/stdlib/Lean/Expr.c | 88 ++++++-- stage0/stdlib/Lean/Level.c | 27 ++- stage0/stdlib/Std/Data/PersistentArray.c | 4 +- 16 files changed, 303 insertions(+), 191 deletions(-) diff --git a/stage0/src/CMakeLists.txt b/stage0/src/CMakeLists.txt index e9dba6ac24..6a26bafba7 100644 --- a/stage0/src/CMakeLists.txt +++ b/stage0/src/CMakeLists.txt @@ -311,6 +311,14 @@ find_package(PythonInterp) include_directories(${CMAKE_BINARY_DIR}/include) +# libleancpp and the stdlib libraries are cyclically dependent. This works by default on macOS, which also doesn't like +# the linker flags necessary on other platforms. +if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + set(LEANC_STATIC_LINKER_FLAGS "-lleancpp -lInit -lStd -lLean") +else() + set(LEANC_STATIC_LINKER_FLAGS "-Wl,--start-group -lleancpp -lInit -lStd -lLean -Wl,--end-group") +endif() + if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") set(LEANC_SHARED_LINKER_FLAGS "${LEANC_SHARED_LINKER_FLAGS} -fPIC") endif() diff --git a/stage0/src/Init/Data/Char/Basic.lean b/stage0/src/Init/Data/Char/Basic.lean index 1806d82c0b..0712b64c26 100644 --- a/stage0/src/Init/Data/Char/Basic.lean +++ b/stage0/src/Init/Data/Char/Basic.lean @@ -30,7 +30,7 @@ instance (a b : Char) : Decidable (a ≤ b) := abbrev isValidCharNat (n : Nat) : Prop := n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000) -theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < uint32Sz := by +theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by match h with | Or.inl h => apply Nat.ltTrans h diff --git a/stage0/src/Init/Data/UInt.lean b/stage0/src/Init/Data/UInt.lean index 0cecf19817..77f4e0fbff 100644 --- a/stage0/src/Init/Data/UInt.lean +++ b/stage0/src/Init/Data/UInt.lean @@ -111,7 +111,7 @@ instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b @[extern "lean_uint32_of_nat"] def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩ @[extern "lean_uint32_of_nat"] -def UInt32.ofNat' (n : Nat) (h : n < uint32Sz) : UInt32 := ⟨⟨n, h⟩⟩ +def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩ abbrev Nat.toUInt32 := UInt32.ofNat @[extern c inline "#1 + #2"] def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩ @@ -215,7 +215,7 @@ def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) := instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b -theorem usizeSzGt0 : usizeSz > 0 := +theorem usizeSzGt0 : USize.size > 0 := Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _) @[extern "lean_usize_of_nat"] diff --git a/stage0/src/Init/Fix.lean b/stage0/src/Init/Fix.lean index a01a955208..c626917df3 100644 --- a/stage0/src/Init/Fix.lean +++ b/stage0/src/Init/Fix.lean @@ -13,7 +13,7 @@ def bfix1 {α β : Type u} (base : α → β) (rec : (α → β) → α → β) @[extern c inline "lean_fixpoint(#4, #5)"] def fixCore1 {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β := - bfix1 base rec usizeSz + bfix1 base rec USize.size @[inline] def fixCore {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β := fixCore1 base rec @@ -30,7 +30,7 @@ def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α @[extern c inline "lean_fixpoint2(#5, #6, #7)"] def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β := - bfix2 base rec usizeSz + bfix2 base rec USize.size @[inline] def fix2 {α₁ α₂ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β := fixCore2 (fun _ _ => arbitrary β) rec @@ -41,7 +41,7 @@ def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → @[extern c inline "lean_fixpoint3(#6, #7, #8, #9)"] def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β := - bfix3 base rec usizeSz + bfix3 base rec USize.size @[inline] def fix3 {α₁ α₂ α₃ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β := fixCore3 (fun _ _ _ => arbitrary β) rec @@ -52,7 +52,7 @@ def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α @[extern c inline "lean_fixpoint4(#7, #8, #9, #10, #11)"] def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β := - bfix4 base rec usizeSz + bfix4 base rec USize.size @[inline] def fix4 {α₁ α₂ α₃ α₄ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β := fixCore4 (fun _ _ _ _ => arbitrary β) rec @@ -63,7 +63,7 @@ def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ @[extern c inline "lean_fixpoint5(#8, #9, #10, #11, #12, #13)"] def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β := - bfix5 base rec usizeSz + bfix5 base rec USize.size @[inline] def fix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β := fixCore5 (fun _ _ _ _ _ => arbitrary β) rec @@ -74,7 +74,7 @@ def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α @[extern c inline "lean_fixpoint6(#9, #10, #11, #12, #13, #14, #15)"] def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β := - bfix6 base rec usizeSz + bfix6 base rec USize.size @[inline] def fix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} [Inhabited β] (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β := fixCore6 (fun _ _ _ _ _ _ => arbitrary β) rec diff --git a/stage0/src/Init/Prelude.lean b/stage0/src/Init/Prelude.lean index 7716792a95..ce6c0a536f 100644 --- a/stage0/src/Init/Prelude.lean +++ b/stage0/src/Init/Prelude.lean @@ -596,9 +596,14 @@ instance {n} : HasLessEq (Fin n) := ⟨Fin.le⟩ instance Fin.decLt {n} (a b : Fin n) : Decidable (Less a b) := Nat.decLt .. instance Fin.decLe {n} (a b : Fin n) : Decidable (LessEq a b) := Nat.decLe .. -def uint8Sz : Nat := 256 +def UInt8.size : Nat := 256 structure UInt8 := - (val : Fin uint8Sz) + (val : Fin UInt8.size) + +@[extern "lean_uint8_of_nat"] +def UInt8.ofNatCore (n : @& Nat) (h : Less n UInt8.size) : UInt8 := { + val := { val := n, isLt := h } +} set_option bootstrap.gen_matcher_code false in @[extern c inline "#1 == #2"] @@ -610,12 +615,17 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) := instance : DecidableEq UInt8 := UInt8.decEq instance : Inhabited UInt8 := { - default := { val := { val := 0, isLt := decide! } } + default := UInt8.ofNatCore 0 decide! } -def uint16Sz : Nat := 65536 +def UInt16.size : Nat := 65536 structure UInt16 := - (val : Fin uint16Sz) + (val : Fin UInt16.size) + +@[extern "lean_uint16_of_nat"] +def UInt16.ofNatCore (n : @& Nat) (h : Less n UInt16.size) : UInt16 := { + val := { val := n, isLt := h } +} set_option bootstrap.gen_matcher_code false in @[extern c inline "#1 == #2"] @@ -627,12 +637,17 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) := instance : DecidableEq UInt16 := UInt16.decEq instance : Inhabited UInt16 := { - default := { val := { val := 0, isLt := decide! } } + default := UInt16.ofNatCore 0 decide! } -def uint32Sz : Nat := 4294967296 +def UInt32.size : Nat := 4294967296 structure UInt32 := - (val : Fin uint32Sz) + (val : Fin UInt32.size) + +@[extern "lean_uint32_of_nat"] +def UInt32.ofNatCore (n : @& Nat) (h : Less n UInt32.size) : UInt32 := { + val := { val := n, isLt := h } +} @[extern "lean_uint32_to_nat"] def UInt32.toNat (n : UInt32) : Nat := n.val.val @@ -647,7 +662,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) := instance : DecidableEq UInt32 := UInt32.decEq instance : Inhabited UInt32 := { - default := { val := { val := 0, isLt := decide! } } + default := UInt32.ofNatCore 0 decide! } def UInt32.lt (a b : UInt32) : Prop := Less a.val b.val @@ -671,15 +686,15 @@ def UInt32.decLe (a b : UInt32) : Decidable (LessEq a b) := instance (a b : UInt32) : Decidable (Less a b) := UInt32.decLt a b instance (a b : UInt32) : Decidable (LessEq a b) := UInt32.decLe a b -@[extern "lean_uint32_of_nat"] -def UInt32.ofNatCore (n : @& Nat) (h : Less n uint32Sz) : UInt32 := { +def UInt64.size : Nat := 18446744073709551616 +structure UInt64 := + (val : Fin UInt64.size) + +@[extern "lean_uint64_of_nat"] +def UInt64.ofNatCore (n : @& Nat) (h : Less n UInt64.size) : UInt64 := { val := { val := n, isLt := h } } -def uint64Sz : Nat := 18446744073709551616 -structure UInt64 := - (val : Fin uint64Sz) - set_option bootstrap.gen_matcher_code false in @[extern c inline "#1 == #2"] def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) := @@ -690,19 +705,24 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) := instance : DecidableEq UInt64 := UInt64.decEq instance : Inhabited UInt64 := { - default := { val := { val := 0, isLt := decide! } } + default := UInt64.ofNatCore 0 decide! } -def usizeSz : Nat := pow 2 System.Platform.numBits +def USize.size : Nat := pow 2 System.Platform.numBits -theorem usizeSzEq : Or (Eq usizeSz 4294967296) (Eq usizeSz 18446744073709551616) := +theorem usizeSzEq : Or (Eq USize.size 4294967296) (Eq USize.size 18446744073709551616) := show Or (Eq (pow 2 System.Platform.numBits) 4294967296) (Eq (pow 2 System.Platform.numBits) 18446744073709551616) from match System.Platform.numBits, System.Platform.numBitsEq with | _, Or.inl rfl => Or.inl (decide! : (Eq (pow 2 32) (4294967296:Nat))) | _, Or.inr rfl => Or.inr (decide! : (Eq (pow 2 64) (18446744073709551616:Nat))) structure USize := - (val : Fin usizeSz) + (val : Fin USize.size) + +@[extern "lean_usize_of_nat"] +def USize.ofNatCore (n : @& Nat) (h : Less n USize.size) : USize := { + val := { val := n, isLt := h } +} set_option bootstrap.gen_matcher_code false in @[extern c inline "#1 == #2"] @@ -714,24 +734,19 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) := instance : DecidableEq USize := USize.decEq instance : Inhabited USize := { - default := { val := { val := 0, isLt := match usizeSz, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide! } } + default := USize.ofNatCore 0 (match USize.size, usizeSzEq with | _, Or.inl rfl => decide! | _, Or.inr rfl => decide!) } @[extern "lean_usize_of_nat"] def USize.ofNat32 (n : @& Nat) (h : Less n 4294967296) : USize := { val := { val := n, - isLt := match usizeSz, usizeSzEq with + isLt := match USize.size, usizeSzEq with | _, Or.inl rfl => h | _, Or.inr rfl => Nat.ltTrans h (decide! : Less 4294967296 18446744073709551616) } } -@[extern "lean_usize_of_nat"] -def USize.ofNatCore (n : @& Nat) (h : Less n usizeSz) : USize := { - val := { val := n, isLt := h } -} - abbrev Nat.isValidChar (n : Nat) : Prop := Or (Less n 0xd800) (And (Less 0xdfff n) (Less n 0x110000)) @@ -744,10 +759,10 @@ structure Char := (val : UInt32) (valid : val.isValidChar) -private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n uint32Sz := +private theorem validCharIsUInt32 {n : Nat} (h : n.isValidChar) : Less n UInt32.size := match h with - | Or.inl h => Nat.ltTrans h (decide! : Less 55296 uint32Sz) - | Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 uint32Sz) + | Or.inl h => Nat.ltTrans h (decide! : Less 55296 UInt32.size) + | Or.inr ⟨_, h⟩ => Nat.ltTrans h (decide! : Less 1114112 UInt32.size) @[extern "lean_uint32_of_nat"] private def Char.ofNatAux (n : Nat) (h : n.isValidChar) : Char := @@ -1366,7 +1381,7 @@ def mkStr (p : Name) (s : String) : Name := @[export lean_name_mk_numeral] def mkNum (p : Name) (v : Nat) : Name := - Name.num p v (mixHash (hash p) (dite (Less v usizeSz) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 decide!))) + Name.num p v (mixHash (hash p) (dite (Less v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 decide!))) def mkSimple (s : String) : Name := mkStr Name.anonymous s diff --git a/stage0/src/Lean/Compiler/IR/EmitC.lean b/stage0/src/Lean/Compiler/IR/EmitC.lean index 4ede1d8a0f..78a87f0f61 100644 --- a/stage0/src/Lean/Compiler/IR/EmitC.lean +++ b/stage0/src/Lean/Compiler/IR/EmitC.lean @@ -474,7 +474,7 @@ def quoteString (s : String) : String := def emitNumLit (t : IRType) (v : Nat) : M Unit := do if t.isObj then - if v < uint32Sz then + if v < UInt32.size then emit "lean_unsigned_to_nat("; emit v; emit "u)" else emit "lean_cstr_to_nat(\""; emit v; emit "\")" diff --git a/stage0/src/Lean/Data/Json/Parser.lean b/stage0/src/Lean/Data/Json/Parser.lean index af895eef2d..eef92ed91d 100644 --- a/stage0/src/Lean/Data/Json/Parser.lean +++ b/stage0/src/Lean/Data/Json/Parser.lean @@ -203,7 +203,7 @@ def num : Quickparse JsonNumber := do if c? = some '.' then skip let (n, d) ← natNumDigits - if d > usizeSz then fail "too many decimals" + if d > USize.size then fail "too many decimals" let mantissa' := res.mantissa * (10^d : Nat) + n let exponent' := res.exponent + d pure $ JsonNumber.mk mantissa' exponent' @@ -220,7 +220,7 @@ def num : Quickparse JsonNumber := do else do if c = '+' then skip let n ← natMaybeZero - if n > usizeSz then fail "exp too large" + if n > USize.size then fail "exp too large" pure (res.shiftl n) else pure res diff --git a/stage0/src/Std/Data/PersistentArray.lean b/stage0/src/Std/Data/PersistentArray.lean index 17a6b3c770..6634da3be3 100644 --- a/stage0/src/Std/Data/PersistentArray.lean +++ b/stage0/src/Std/Data/PersistentArray.lean @@ -129,7 +129,7 @@ def mkNewTail (t : PersistentArray α) : PersistentArray α := shift := t.shift + initShift, tailOff := t.size } -def tooBig : Nat := usizeSz / 8 +def tooBig : Nat := USize.size / 8 def push (t : PersistentArray α) (a : α) : PersistentArray α := let r := { t with tail := t.tail.push a, size := t.size + 1 } diff --git a/stage0/src/bin/leanc.in b/stage0/src/bin/leanc.in index ee65efdd85..def749ac5f 100755 --- a/stage0/src/bin/leanc.in +++ b/stage0/src/bin/leanc.in @@ -16,9 +16,7 @@ bindir=$(dirname $0) cflags=("-I$bindir/../include") ldflags=("-L$bindir/../lib/lean" "-lgmp" @LEANC_EXTRA_FLAGS@) -# static linker flags -# NOTE: libleancpp and libInit are cyclically dependent -ldflags_ext=("-lleancpp" "-lInit" "-lStd" "-lLean" "-lleancpp" "-lInit" "-lStd" "-lLean" "-lStd") +ldflags_ext=(@LEANC_STATIC_LINKER_FLAGS@) for arg in "$@"; do # passed -shared ~> switch to shared linker flags [[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) diff --git a/stage0/stdlib/Init/Prelude.c b/stage0/stdlib/Init/Prelude.c index 2815bd1d6d..facdd5dd02 100644 --- a/stage0/stdlib/Init/Prelude.c +++ b/stage0/stdlib/Init/Prelude.c @@ -34,7 +34,7 @@ lean_object* l_EStateM_tryCatch(lean_object*, lean_object*, lean_object*); lean_object* l_UInt32_decLe___boxed(lean_object*, lean_object*); lean_object* l___private_Init_Prelude_0__String_utf8ByteSizeAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_erase_macro_scopes(lean_object*); -lean_object* l_Init_Prelude___instance__32; +uint64_t l_Init_Prelude___instance__32; lean_object* l_withTheReader(lean_object*, lean_object*); lean_object* l_Nat_sub___boxed(lean_object*, lean_object*); lean_object* l_Functor_mapConst___default(lean_object*); @@ -74,6 +74,7 @@ lean_object* l_String_mk___boxed(lean_object*); lean_object* l_Nat_decEq_match__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_read___at_Lean_Macro_Init_Prelude___instance__79___spec__1(lean_object*, lean_object*); lean_object* l_getModify___rarg___lambda__1(lean_object*, lean_object*); +uint64_t lean_uint64_of_nat(lean_object*); lean_object* l_EStateM_Init_Prelude___instance__63___closed__6; lean_object* l_String_utf8ByteSize_match__1(lean_object*); lean_object* l_Lean_Name_Init_Prelude___instance__70; @@ -90,7 +91,8 @@ lean_object* l_Lean_Macro_Init_Prelude___instance__80___lambda__1___boxed(lean_o lean_object* l_Lean_Syntax_getKind_match__1(lean_object*); lean_object* l_ReaderT_Init_Prelude___instance__49___closed__1; lean_object* l_Init_Prelude___instance__6(lean_object*, lean_object*); -lean_object* l_Init_Prelude___instance__32___closed__1; +lean_object* l_UInt64_size___closed__1; +uint64_t l_Init_Prelude___instance__32___closed__1; lean_object* l_ReaderT_map___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_withRef___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -108,6 +110,7 @@ lean_object* l_Lean_Macro_Init_Prelude___instance__79___closed__4; lean_object* l_Lean_Macro_Init_Prelude___instance__80___closed__1; lean_object* l_List_foldl___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_run(lean_object*, lean_object*, lean_object*); +lean_object* l_UInt8_size; lean_object* l_EStateM_Init_Prelude___instance__63___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_getKind_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__44___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -155,6 +158,7 @@ lean_object* l_Lean_addMacroScope_match__2___rarg___boxed(lean_object*, lean_obj lean_object* l_Lean_Init_Prelude___instance__72; lean_object* l_Init_Prelude___instance__8(lean_object*); lean_object* l_Lean_Macro_withFreshMacroScope(lean_object*); +lean_object* l_USize_size___closed__1; lean_object* l_Init_Prelude___instance__16; lean_object* l_ReaderT_lift___rarg___boxed(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__54___rarg(lean_object*, lean_object*); @@ -185,7 +189,6 @@ lean_object* l_Applicative_seqRight___default___rarg___closed__1; lean_object* l_cond_match__1___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_readThe___rarg___boxed(lean_object*); lean_object* l_Lean_Macro_Context_currRecDepth___default; -lean_object* l_uint64Sz___closed__1; lean_object* l_Applicative_seqRight___default(lean_object*); lean_object* l_Init_Prelude___instance__38(lean_object*); lean_object* l_EStateM_adaptExcept(lean_object*, lean_object*, lean_object*, lean_object*); @@ -193,15 +196,15 @@ lean_object* lean_string_utf8_byte_size(lean_object*); lean_object* l_cond___rarg(uint8_t, lean_object*, lean_object*); lean_object* l_List_hasDecEq_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_adapt___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_UInt8_ofNatCore___boxed(lean_object*, lean_object*); lean_object* l_False_elim(lean_object*, uint8_t); lean_object* l_Init_Prelude___instance__43___rarg___boxed(lean_object*); lean_object* l_cond_match__1(lean_object*, lean_object*); -lean_object* l_Init_Prelude___instance__34; +size_t l_Init_Prelude___instance__34; lean_object* l_EStateM_dummySave___boxed(lean_object*, lean_object*); lean_object* l_Lean_nameLitKind; lean_object* l_cond(lean_object*); lean_object* l_EStateM_dummyRestore(lean_object*); -lean_object* l_uint64Sz; lean_object* l_Applicative_map___default___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Init_Prelude___instance__74; uint8_t l_Init_Prelude___instance__33(size_t, size_t); @@ -245,7 +248,7 @@ lean_object* l_Lean_addMacroScope_match__1(lean_object*); lean_object* l_EStateM_Init_Prelude___instance__65(lean_object*, lean_object*); lean_object* l_getThe___rarg(lean_object*); lean_object* l___private_Init_Prelude_0__Lean_extractMacroScopesAux(lean_object*, lean_object*); -lean_object* l_Init_Prelude___instance__24; +uint16_t l_Init_Prelude___instance__24; uint8_t l_Lean_Name_hasMacroScopes(lean_object*); lean_object* l_Init_Prelude___instance__48___rarg___boxed(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__59___rarg___lambda__1(lean_object*, lean_object*, lean_object*); @@ -319,7 +322,6 @@ lean_object* l_Init_Prelude___instance__18_match__1___boxed(lean_object*, lean_o uint32_t l_Char_utf8Size___closed__2; lean_object* l_Lean_replaceRef_match__1(lean_object*); lean_object* l_EStateM_Init_Prelude___instance__63___closed__3; -lean_object* l_uint16Sz; lean_object* l_Init_Prelude___instance__12___closed__1; lean_object* l_modify(lean_object*, lean_object*); lean_object* l_Lean_Init_Prelude___instance__69___closed__1; @@ -333,7 +335,7 @@ lean_object* l_Init_Prelude___instance__45___rarg(lean_object*); lean_object* l_Lean_firstFrontendMacroScope___closed__1; lean_object* l_Lean_replaceRef(lean_object*, lean_object*); lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); -lean_object* l_Init_Prelude___instance__24___closed__1; +uint16_t l_Init_Prelude___instance__24___closed__1; uint8_t l_UInt32_decLt(uint32_t, uint32_t); lean_object* l_Lean_numLitKind___closed__1; lean_object* l_List_hasDecEq_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*); @@ -377,7 +379,7 @@ lean_object* l_ReaderT_bind(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__35___boxed(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__11; lean_object* l_EStateM_modifyGet(lean_object*, lean_object*, lean_object*); -lean_object* l_Init_Prelude___instance__22___closed__1; +uint8_t l_Init_Prelude___instance__22___closed__1; lean_object* l_Array_mkEmpty___boxed(lean_object*, lean_object*); lean_object* l_EStateM_nonBacktrackable___closed__1; lean_object* l_Lean_choiceKind; @@ -391,7 +393,7 @@ lean_object* l_Init_Prelude___instance__2(lean_object*, lean_object*); lean_object* l_Lean_Macro_Init_Prelude___instance__80___closed__4; lean_object* l_Init_Prelude___instance__11___closed__1; size_t lean_usize_of_nat(lean_object*); -lean_object* l_Init_Prelude___instance__26___closed__1; +uint32_t l_Init_Prelude___instance__26___closed__1; lean_object* l_ReaderT_Init_Prelude___instance__50___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_read___rarg(lean_object*, lean_object*); lean_object* l_inferInstance___rarg___boxed(lean_object*); @@ -413,6 +415,7 @@ lean_object* l_EStateM_nonBacktrackable___closed__2; lean_object* l_Lean_Macro_withIncRecDepth_match__1___rarg(uint8_t, lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__13; lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_UInt16_size; lean_object* l_Lean_Syntax_getHeadInfo_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_UInt32_ofNatCore___boxed(lean_object*, lean_object*); lean_object* l_decEq(lean_object*); @@ -454,6 +457,7 @@ uint8_t l_or(uint8_t, uint8_t); lean_object* l_Monad_map___default(lean_object*); lean_object* l_ReaderT_bind___at_Lean_Macro_Init_Prelude___instance__79___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_add___boxed(lean_object*, lean_object*); +lean_object* l_UInt64_ofNatCore___boxed(lean_object*, lean_object*); lean_object* l_Lean_nullKind___closed__1; lean_object* l_Lean_SourceInfo_pos___default; lean_object* l_Init_Prelude___instance__57___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -470,7 +474,6 @@ lean_object* l_ReaderT_Init_Prelude___instance__49(lean_object*, lean_object*); lean_object* l_Nat_decEq_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_getArgs_match__1(lean_object*); lean_object* l_Lean_SourceInfo_leading___default; -lean_object* l_uint8Sz; lean_object* l_UInt16_decEq___boxed(lean_object*, lean_object*); lean_object* l_typedExpr___rarg(lean_object*); lean_object* l_Init_Prelude___instance__15; @@ -486,7 +489,7 @@ lean_object* l_Init_Prelude___instance__55___rarg(lean_object*); lean_object* l_Lean_replaceRef___boxed(lean_object*, lean_object*); lean_object* l_Lean_extractMacroScopes_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_read(lean_object*, lean_object*); -lean_object* l_Init_Prelude___instance__34___closed__1; +size_t l_Init_Prelude___instance__34___closed__1; lean_object* l_Lean_Syntax_getHeadInfo_loop(lean_object*, lean_object*); lean_object* l_Eq_ndrec___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_and___boxed(lean_object*, lean_object*); @@ -509,7 +512,7 @@ uint8_t l_UInt32_decEq(uint32_t, uint32_t); lean_object* l___private_Init_Prelude_0__Lean_extractMainModule_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_nonBacktrackable___closed__3; lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux(lean_object*); -lean_object* l_Init_Prelude___instance__26; +uint32_t l_Init_Prelude___instance__26; lean_object* l_Init_Prelude___instance__27; lean_object* l_Lean_Syntax_setKind_match__1(lean_object*); lean_object* l_Init_Prelude___instance__12; @@ -531,7 +534,7 @@ lean_object* l_Init_Prelude___instance__7(lean_object*, lean_object*); lean_object* l_Monad_seqRight___default___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_mk(lean_object*, lean_object*); lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux_match__2(lean_object*); -lean_object* l_Init_Prelude___instance__22; +uint8_t l_Init_Prelude___instance__22; lean_object* l_tryCatchThe(lean_object*, lean_object*); lean_object* l_String_bsize(lean_object*); lean_object* l_Init_Prelude___instance__39___boxed(lean_object*, lean_object*); @@ -546,7 +549,6 @@ lean_object* l_Lean_Macro_withIncRecDepth(lean_object*); lean_object* l_Lean_Name_append_match__1(lean_object*); lean_object* l_and_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Macro_withIncRecDepth_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); -lean_object* l_usizeSz___closed__1; lean_object* l_ReaderT_Init_Prelude___instance__50___rarg(lean_object*); lean_object* l___private_Init_Prelude_0__Char_ofNatAux___boxed(lean_object*, lean_object*); lean_object* l_EStateM_adaptExcept___rarg(lean_object*, lean_object*, lean_object*); @@ -607,7 +609,6 @@ lean_object* l_Init_Prelude___instance__35_match__1___boxed(lean_object*, lean_o lean_object* lean_nat_mul(lean_object*, lean_object*); lean_object* l_Lean_Syntax_getPos(lean_object*); lean_object* l_throwThe___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_uint32Sz; lean_object* l_UInt32_decEq___boxed(lean_object*, lean_object*); lean_object* l_Lean_Name_append_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_cast(lean_object*, lean_object*, lean_object*); @@ -618,12 +619,14 @@ lean_object* l_EStateM_set___rarg(lean_object*, lean_object*); lean_object* l_List_foldl___at_Lean_MacroScopesView_review___spec__1(lean_object*, lean_object*); lean_object* l_ReaderT_pure___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Decidable_decide___rarg___boxed(lean_object*); +lean_object* l_USize_size; lean_object* l_Lean_Name_hasMacroScopes_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_orElse(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_cond___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Macro_Init_Prelude___instance__80___lambda__2(lean_object*, lean_object*); lean_object* l_getModify___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* lean_name_mk_numeral(lean_object*, lean_object*); +lean_object* l_Char_ofNat___closed__1; lean_object* l_Function_const(lean_object*, lean_object*); lean_object* l_Lean_Init_Prelude___instance__74___closed__2; lean_object* l_ReaderT_map(lean_object*, lean_object*); @@ -636,6 +639,7 @@ lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__6(lean_objec lean_object* l_EStateM_Init_Prelude___instance__63___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_List_hasDecEq_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Array_getOp___rarg(lean_object*, lean_object*, lean_object*); +uint8_t lean_uint8_of_nat(lean_object*); lean_object* l_Fin_decLe___rarg___boxed(lean_object*, lean_object*); lean_object* l_modifyGetThe(lean_object*, lean_object*, lean_object*); lean_object* l_cond_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -643,12 +647,14 @@ lean_object* l_List_hasDecEq_match__3(lean_object*, lean_object*); lean_object* l_Lean_Init_Prelude___instance__73; lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux___boxed(lean_object*); lean_object* l_Init_Prelude___instance__55(lean_object*, lean_object*); +lean_object* l_UInt16_ofNatCore___boxed(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__6_match__1(lean_object*, lean_object*); lean_object* l_Lean_Macro_Init_Prelude___instance__79___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* lean_array_data(lean_object*, lean_object*); uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__29___boxed(lean_object*, lean_object*); size_t lean_usize_mix_hash(size_t, size_t); +lean_object* l_UInt32_size; lean_object* l_List_hasDecEq_match__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_USize_ofNatCore___boxed(lean_object*, lean_object*); lean_object* l_MonadExcept_orelse(lean_object*, lean_object*); @@ -675,7 +681,6 @@ lean_object* l_Init_Prelude___instance__8_match__1(lean_object*, lean_object*); lean_object* l_or_match__1(lean_object*); lean_object* l_id(lean_object*); lean_object* l_Init_Prelude___instance__41(lean_object*, lean_object*); -lean_object* l_usizeSz; lean_object* l___private_Init_Prelude_0__Lean_assembleParts___closed__1; lean_object* l_Lean_Syntax_getOp___boxed(lean_object*, lean_object*); lean_object* l_Init_Prelude___instance__59(lean_object*, lean_object*); @@ -708,6 +713,7 @@ lean_object* l___private_Init_Prelude_0__Lean_eraseMacroScopesAux_match__1___rar lean_object* l_ReaderT_Init_Prelude___instance__51___rarg___lambda__7(lean_object*, lean_object*, lean_object*); lean_object* l_ReaderT_pure(lean_object*, lean_object*); lean_object* l_Lean_Syntax_getHeadInfo_loop___boxed(lean_object*, lean_object*); +uint16_t lean_uint16_of_nat(lean_object*); lean_object* l_Array_sz___boxed(lean_object*, lean_object*); lean_object* l_ReaderT_lift___rarg(lean_object*, lean_object*); lean_object* l_ReaderT_Init_Prelude___instance__51(lean_object*, lean_object*); @@ -722,6 +728,7 @@ lean_object* l_Monad_seq___default___rarg___lambda__1(lean_object*, lean_object* lean_object* l_Init_Prelude___instance__42___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Name_Init_Prelude___instance__71___closed__1; lean_object* l_Array_mkEmpty_match__1___rarg(lean_object*, lean_object*); +lean_object* l_UInt64_size; lean_object* l_EStateM_Init_Prelude___instance__65___closed__2; lean_object* l_EStateM_Init_Prelude___instance__66___rarg(lean_object*); lean_object* l_Init_Prelude___instance__37(lean_object*); @@ -2412,7 +2419,7 @@ lean_dec(x_1); return x_2; } } -static lean_object* _init_l_uint8Sz() { +static lean_object* _init_l_UInt8_size() { _start: { lean_object* x_1; @@ -2420,6 +2427,16 @@ x_1 = lean_unsigned_to_nat(256u); return x_1; } } +lean_object* l_UInt8_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint8_t x_3; lean_object* x_4; +x_3 = lean_uint8_of_nat(x_1); +lean_dec(x_1); +x_4 = lean_box(x_3); +return x_4; +} +} lean_object* l_UInt8_decEq___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -2454,25 +2471,24 @@ x_6 = lean_box(x_5); return x_6; } } -static lean_object* _init_l_Init_Prelude___instance__22___closed__1() { +static uint8_t _init_l_Init_Prelude___instance__22___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; +lean_object* x_1; uint8_t x_2; x_1 = lean_unsigned_to_nat(0u); -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); +x_2 = lean_uint8_of_nat(x_1); return x_2; } } -static lean_object* _init_l_Init_Prelude___instance__22() { +static uint8_t _init_l_Init_Prelude___instance__22() { _start: { -lean_object* x_1; +uint8_t x_1; x_1 = l_Init_Prelude___instance__22___closed__1; return x_1; } } -static lean_object* _init_l_uint16Sz() { +static lean_object* _init_l_UInt16_size() { _start: { lean_object* x_1; @@ -2480,6 +2496,16 @@ x_1 = lean_unsigned_to_nat(65536u); return x_1; } } +lean_object* l_UInt16_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint16_t x_3; lean_object* x_4; +x_3 = lean_uint16_of_nat(x_1); +lean_dec(x_1); +x_4 = lean_box(x_3); +return x_4; +} +} lean_object* l_UInt16_decEq___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -2514,25 +2540,24 @@ x_6 = lean_box(x_5); return x_6; } } -static lean_object* _init_l_Init_Prelude___instance__24___closed__1() { +static uint16_t _init_l_Init_Prelude___instance__24___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; +lean_object* x_1; uint16_t x_2; x_1 = lean_unsigned_to_nat(0u); -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); +x_2 = lean_uint16_of_nat(x_1); return x_2; } } -static lean_object* _init_l_Init_Prelude___instance__24() { +static uint16_t _init_l_Init_Prelude___instance__24() { _start: { -lean_object* x_1; +uint16_t x_1; x_1 = l_Init_Prelude___instance__24___closed__1; return x_1; } } -static lean_object* _init_l_uint32Sz() { +static lean_object* _init_l_UInt32_size() { _start: { lean_object* x_1; @@ -2540,6 +2565,16 @@ x_1 = lean_cstr_to_nat("4294967296"); return x_1; } } +lean_object* l_UInt32_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint32_t x_3; lean_object* x_4; +x_3 = lean_uint32_of_nat(x_1); +lean_dec(x_1); +x_4 = lean_box_uint32(x_3); +return x_4; +} +} lean_object* l_UInt32_toNat___boxed(lean_object* x_1) { _start: { @@ -2584,20 +2619,19 @@ x_6 = lean_box(x_5); return x_6; } } -static lean_object* _init_l_Init_Prelude___instance__26___closed__1() { +static uint32_t _init_l_Init_Prelude___instance__26___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; +lean_object* x_1; uint32_t x_2; x_1 = lean_unsigned_to_nat(0u); -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); +x_2 = lean_uint32_of_nat(x_1); return x_2; } } -static lean_object* _init_l_Init_Prelude___instance__26() { +static uint32_t _init_l_Init_Prelude___instance__26() { _start: { -lean_object* x_1; +uint32_t x_1; x_1 = l_Init_Prelude___instance__26___closed__1; return x_1; } @@ -2686,17 +2720,7 @@ x_6 = lean_box(x_5); return x_6; } } -lean_object* l_UInt32_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { -_start: -{ -uint32_t x_3; lean_object* x_4; -x_3 = lean_uint32_of_nat(x_1); -lean_dec(x_1); -x_4 = lean_box_uint32(x_3); -return x_4; -} -} -static lean_object* _init_l_uint64Sz___closed__1() { +static lean_object* _init_l_UInt64_size___closed__1() { _start: { lean_object* x_1; @@ -2704,14 +2728,24 @@ x_1 = lean_cstr_to_nat("18446744073709551616"); return x_1; } } -static lean_object* _init_l_uint64Sz() { +static lean_object* _init_l_UInt64_size() { _start: { lean_object* x_1; -x_1 = l_uint64Sz___closed__1; +x_1 = l_UInt64_size___closed__1; return x_1; } } +lean_object* l_UInt64_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +uint64_t x_3; lean_object* x_4; +x_3 = lean_uint64_of_nat(x_1); +lean_dec(x_1); +x_4 = lean_box_uint64(x_3); +return x_4; +} +} lean_object* l_UInt64_decEq___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -2746,25 +2780,24 @@ x_6 = lean_box(x_5); return x_6; } } -static lean_object* _init_l_Init_Prelude___instance__32___closed__1() { +static uint64_t _init_l_Init_Prelude___instance__32___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; +lean_object* x_1; uint64_t x_2; x_1 = lean_unsigned_to_nat(0u); -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); +x_2 = lean_uint64_of_nat(x_1); return x_2; } } -static lean_object* _init_l_Init_Prelude___instance__32() { +static uint64_t _init_l_Init_Prelude___instance__32() { _start: { -lean_object* x_1; +uint64_t x_1; x_1 = l_Init_Prelude___instance__32___closed__1; return x_1; } } -static lean_object* _init_l_usizeSz___closed__1() { +static lean_object* _init_l_USize_size___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -2774,14 +2807,24 @@ x_3 = lean_nat_pow(x_1, x_2); return x_3; } } -static lean_object* _init_l_usizeSz() { +static lean_object* _init_l_USize_size() { _start: { lean_object* x_1; -x_1 = l_usizeSz___closed__1; +x_1 = l_USize_size___closed__1; return x_1; } } +lean_object* l_USize_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { +_start: +{ +size_t x_3; lean_object* x_4; +x_3 = lean_usize_of_nat(x_1); +lean_dec(x_1); +x_4 = lean_box_usize(x_3); +return x_4; +} +} lean_object* l_USize_decEq___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -2816,20 +2859,19 @@ x_6 = lean_box(x_5); return x_6; } } -static lean_object* _init_l_Init_Prelude___instance__34___closed__1() { +static size_t _init_l_Init_Prelude___instance__34___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; +lean_object* x_1; size_t x_2; x_1 = lean_unsigned_to_nat(0u); -x_2 = lean_alloc_ctor(0, 1, 0); -lean_ctor_set(x_2, 0, x_1); +x_2 = lean_usize_of_nat(x_1); return x_2; } } -static lean_object* _init_l_Init_Prelude___instance__34() { +static size_t _init_l_Init_Prelude___instance__34() { _start: { -lean_object* x_1; +size_t x_1; x_1 = l_Init_Prelude___instance__34___closed__1; return x_1; } @@ -2844,16 +2886,6 @@ x_4 = lean_box_usize(x_3); return x_4; } } -lean_object* l_USize_ofNatCore___boxed(lean_object* x_1, lean_object* x_2) { -_start: -{ -size_t x_3; lean_object* x_4; -x_3 = lean_usize_of_nat(x_1); -lean_dec(x_1); -x_4 = lean_box_usize(x_3); -return x_4; -} -} lean_object* l___private_Init_Prelude_0__Char_ofNatAux___boxed(lean_object* x_1, lean_object* x_2) { _start: { @@ -2863,6 +2895,16 @@ x_4 = lean_box_uint32(x_3); return x_4; } } +static lean_object* _init_l_Char_ofNat___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(0u); +x_2 = lean_alloc_ctor(0, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} lean_object* l_Char_ofNat(lean_object* x_1) { _start: { @@ -2878,7 +2920,7 @@ if (x_5 == 0) { lean_object* x_6; lean_dec(x_1); -x_6 = l_Init_Prelude___instance__26___closed__1; +x_6 = l_Char_ofNat___closed__1; return x_6; } else @@ -2890,7 +2932,7 @@ if (x_8 == 0) { lean_object* x_9; lean_dec(x_1); -x_9 = l_Init_Prelude___instance__26___closed__1; +x_9 = l_Char_ofNat___closed__1; return x_9; } else @@ -6690,7 +6732,7 @@ _start: { size_t x_3; lean_object* x_4; uint8_t x_5; x_3 = l_Lean_Name_hash(x_1); -x_4 = l_usizeSz; +x_4 = l_USize_size; x_5 = lean_nat_dec_lt(x_2, x_4); if (x_5 == 0) { @@ -10446,44 +10488,36 @@ l_System_Platform_numBits___closed__1 = _init_l_System_Platform_numBits___closed lean_mark_persistent(l_System_Platform_numBits___closed__1); l_System_Platform_numBits = _init_l_System_Platform_numBits(); lean_mark_persistent(l_System_Platform_numBits); -l_uint8Sz = _init_l_uint8Sz(); -lean_mark_persistent(l_uint8Sz); +l_UInt8_size = _init_l_UInt8_size(); +lean_mark_persistent(l_UInt8_size); l_Init_Prelude___instance__22___closed__1 = _init_l_Init_Prelude___instance__22___closed__1(); -lean_mark_persistent(l_Init_Prelude___instance__22___closed__1); l_Init_Prelude___instance__22 = _init_l_Init_Prelude___instance__22(); -lean_mark_persistent(l_Init_Prelude___instance__22); -l_uint16Sz = _init_l_uint16Sz(); -lean_mark_persistent(l_uint16Sz); +l_UInt16_size = _init_l_UInt16_size(); +lean_mark_persistent(l_UInt16_size); l_Init_Prelude___instance__24___closed__1 = _init_l_Init_Prelude___instance__24___closed__1(); -lean_mark_persistent(l_Init_Prelude___instance__24___closed__1); l_Init_Prelude___instance__24 = _init_l_Init_Prelude___instance__24(); -lean_mark_persistent(l_Init_Prelude___instance__24); -l_uint32Sz = _init_l_uint32Sz(); -lean_mark_persistent(l_uint32Sz); +l_UInt32_size = _init_l_UInt32_size(); +lean_mark_persistent(l_UInt32_size); l_Init_Prelude___instance__26___closed__1 = _init_l_Init_Prelude___instance__26___closed__1(); -lean_mark_persistent(l_Init_Prelude___instance__26___closed__1); l_Init_Prelude___instance__26 = _init_l_Init_Prelude___instance__26(); -lean_mark_persistent(l_Init_Prelude___instance__26); l_Init_Prelude___instance__27 = _init_l_Init_Prelude___instance__27(); lean_mark_persistent(l_Init_Prelude___instance__27); l_Init_Prelude___instance__28 = _init_l_Init_Prelude___instance__28(); lean_mark_persistent(l_Init_Prelude___instance__28); -l_uint64Sz___closed__1 = _init_l_uint64Sz___closed__1(); -lean_mark_persistent(l_uint64Sz___closed__1); -l_uint64Sz = _init_l_uint64Sz(); -lean_mark_persistent(l_uint64Sz); +l_UInt64_size___closed__1 = _init_l_UInt64_size___closed__1(); +lean_mark_persistent(l_UInt64_size___closed__1); +l_UInt64_size = _init_l_UInt64_size(); +lean_mark_persistent(l_UInt64_size); l_Init_Prelude___instance__32___closed__1 = _init_l_Init_Prelude___instance__32___closed__1(); -lean_mark_persistent(l_Init_Prelude___instance__32___closed__1); l_Init_Prelude___instance__32 = _init_l_Init_Prelude___instance__32(); -lean_mark_persistent(l_Init_Prelude___instance__32); -l_usizeSz___closed__1 = _init_l_usizeSz___closed__1(); -lean_mark_persistent(l_usizeSz___closed__1); -l_usizeSz = _init_l_usizeSz(); -lean_mark_persistent(l_usizeSz); +l_USize_size___closed__1 = _init_l_USize_size___closed__1(); +lean_mark_persistent(l_USize_size___closed__1); +l_USize_size = _init_l_USize_size(); +lean_mark_persistent(l_USize_size); l_Init_Prelude___instance__34___closed__1 = _init_l_Init_Prelude___instance__34___closed__1(); -lean_mark_persistent(l_Init_Prelude___instance__34___closed__1); l_Init_Prelude___instance__34 = _init_l_Init_Prelude___instance__34(); -lean_mark_persistent(l_Init_Prelude___instance__34); +l_Char_ofNat___closed__1 = _init_l_Char_ofNat___closed__1(); +lean_mark_persistent(l_Char_ofNat___closed__1); l_Char_utf8Size___closed__1 = _init_l_Char_utf8Size___closed__1(); l_Char_utf8Size___closed__2 = _init_l_Char_utf8Size___closed__2(); l_Char_utf8Size___closed__3 = _init_l_Char_utf8Size___closed__3(); diff --git a/stage0/stdlib/Lean/Compiler/ConstFolding.c b/stage0/stdlib/Lean/Compiler/ConstFolding.c index ff43c9326a..37ea41f44d 100644 --- a/stage0/stdlib/Lean/Compiler/ConstFolding.c +++ b/stage0/stdlib/Lean/Compiler/ConstFolding.c @@ -42,6 +42,7 @@ lean_object* l_Lean_Compiler_NumScalarTypeInfo_size___default___boxed(lean_objec lean_object* l_Lean_Compiler_foldCharOfNat___closed__1; lean_object* l_Lean_Compiler_foldUIntSub___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Compiler_natFoldFns___closed__15; +extern lean_object* l_UInt64_size___closed__1; lean_object* l_Lean_Compiler_foldCharOfNat___closed__2; extern lean_object* l_myMacro____x40_Init_Notation___hyg_874____closed__6; lean_object* l_Lean_Compiler_NumScalarTypeInfo_ofNatFn___default(lean_object*); @@ -70,6 +71,7 @@ lean_object* l_Lean_Compiler_natFoldFns___closed__19; lean_object* l_Lean_Compiler_foldNatDecLe___closed__2; lean_object* l_Lean_Compiler_preUIntBinFoldFns___closed__9; lean_object* l_Lean_Compiler_foldUIntSub___boxed(lean_object*, lean_object*, lean_object*); +extern lean_object* l_USize_size___closed__1; lean_object* l_Lean_Compiler_NumScalarTypeInfo_size___default(lean_object*); lean_object* l_Lean_Compiler_foldUIntSub___closed__1; extern lean_object* l_myMacro____x40_Init_Notation___hyg_1547____closed__7; @@ -89,7 +91,6 @@ lean_object* l_Lean_Compiler_foldUIntAdd___lambda__1___boxed(lean_object*, lean_ lean_object* l_Lean_Compiler_numScalarTypes___closed__1; lean_object* l_Lean_Compiler_natFoldFns___closed__31; lean_object* l_Lean_Compiler_foldNatMul___boxed(lean_object*); -extern lean_object* l_uint64Sz___closed__1; lean_object* l_Lean_Compiler_binFoldFns___closed__2; lean_object* l_Lean_Compiler_NumScalarTypeInfo_toNatFn___default___closed__1; lean_object* l_Lean_Compiler_uintFoldToNatFns; @@ -258,7 +259,6 @@ lean_object* l_Lean_Compiler_mkNatLt(lean_object*, lean_object*); lean_object* l_Lean_mkApp(lean_object*, lean_object*); lean_object* l_Lean_Compiler_mkUIntLit(lean_object*, lean_object*); lean_object* l_List_map___at_Lean_Compiler_uintBinFoldFns___spec__1___boxed(lean_object*, lean_object*); -extern lean_object* l_usizeSz___closed__1; lean_object* l_Lean_Compiler_foldBinUInt___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Name_append(lean_object*, lean_object*); lean_object* l_Lean_Compiler_mkNatLe___closed__1; @@ -598,7 +598,7 @@ x_1 = lean_unsigned_to_nat(64u); x_2 = l_Lean_Compiler_numScalarTypes___closed__13; x_3 = l_Lean_Compiler_numScalarTypes___closed__14; x_4 = l_Lean_Compiler_numScalarTypes___closed__15; -x_5 = l_uint64Sz___closed__1; +x_5 = l_UInt64_size___closed__1; x_6 = lean_alloc_ctor(0, 5, 0); lean_ctor_set(x_6, 0, x_1); lean_ctor_set(x_6, 1, x_2); @@ -654,7 +654,7 @@ x_1 = l_System_Platform_numBits; x_2 = l_Lean_Compiler_numScalarTypes___closed__18; x_3 = l_Lean_Compiler_numScalarTypes___closed__19; x_4 = l_Lean_Compiler_numScalarTypes___closed__20; -x_5 = l_usizeSz___closed__1; +x_5 = l_USize_size___closed__1; x_6 = lean_alloc_ctor(0, 5, 0); lean_ctor_set(x_6, 0, x_1); lean_ctor_set(x_6, 1, x_2); diff --git a/stage0/stdlib/Lean/Compiler/IR/EmitC.c b/stage0/stdlib/Lean/Compiler/IR/EmitC.c index 9ff2a79ef5..794d4f9be1 100644 --- a/stage0/stdlib/Lean/Compiler/IR/EmitC.c +++ b/stage0/stdlib/Lean/Compiler/IR/EmitC.c @@ -498,7 +498,6 @@ lean_object* l_Lean_IR_EmitC_emitApp(lean_object*, lean_object*, lean_object*, l lean_object* l_List_forM___at_Lean_IR_EmitC_emitFnDecls___spec__3___closed__2; lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitArgs___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_uint32Sz; lean_object* l_Nat_foldM_loop___at_Lean_IR_EmitC_emitSimpleExternalCall___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); lean_object* l_Lean_IR_EmitC_emitTag(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_EmitC_emitDecl(lean_object*, lean_object*, lean_object*); @@ -542,6 +541,7 @@ lean_object* l_Lean_IR_EmitC_emitSProj_match__1(lean_object*); lean_object* l_Lean_IR_EmitC_emitFullApp_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__12; extern lean_object* l___kind_term____x40_Init_Notation___hyg_2679____closed__2; +extern lean_object* l_UInt32_size; lean_object* l_Nat_forM_loop___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_EmitC_getJPParams___closed__1; lean_object* lean_ir_find_env_decl(lean_object*, lean_object*); @@ -9462,7 +9462,7 @@ return x_9; else { lean_object* x_10; uint8_t x_11; -x_10 = l_uint32Sz; +x_10 = l_UInt32_size; x_11 = lean_nat_dec_lt(x_2, x_10); if (x_11 == 0) { diff --git a/stage0/stdlib/Lean/Data/Json/Parser.c b/stage0/stdlib/Lean/Data/Json/Parser.c index a876c132b7..b46fc0fc3d 100644 --- a/stage0/stdlib/Lean/Data/Json/Parser.c +++ b/stage0/stdlib/Lean/Data/Json/Parser.c @@ -130,6 +130,7 @@ lean_object* lean_nat_mul(lean_object*, lean_object*); lean_object* l_Lean_Lean_Data_Json_Parser___instance__1(lean_object*); lean_object* l_Lean_Json_Parser_escapedChar___boxed__const__8; lean_object* l_UInt32_decEq___boxed(lean_object*, lean_object*); +extern lean_object* l_USize_size; lean_object* l_Lean_Quickparse_Lean_Data_Json_Parser___instance__2___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Quickparse_bind(lean_object*, lean_object*); lean_object* l_Lean_Quickparse_Lean_Data_Json_Parser___instance__2___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*); @@ -149,7 +150,6 @@ lean_object* l_Lean_Json_Parser_num___lambda__3___closed__3; extern lean_object* l_stdNext___closed__7; lean_object* l_Lean_Json_Parser_num___lambda__6___boxed(lean_object*, lean_object*); lean_object* lean_int_add(lean_object*, lean_object*); -extern lean_object* l_usizeSz; lean_object* l_Lean_Json_Parser_natCore(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Quickparse_peek_x21(lean_object*); lean_object* l_Lean_Json_parse_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -2974,7 +2974,7 @@ x_20 = lean_ctor_get(x_17, 0); x_21 = lean_ctor_get(x_19, 0); lean_inc(x_21); lean_dec(x_19); -x_22 = l_usizeSz; +x_22 = l_USize_size; x_23 = lean_nat_dec_lt(x_22, x_21); if (x_23 == 0) { @@ -3007,7 +3007,7 @@ lean_dec(x_17); x_29 = lean_ctor_get(x_27, 0); lean_inc(x_29); lean_dec(x_27); -x_30 = l_usizeSz; +x_30 = l_USize_size; x_31 = lean_nat_dec_lt(x_30, x_29); if (x_31 == 0) { @@ -3461,7 +3461,7 @@ lean_inc(x_33); x_34 = lean_ctor_get(x_31, 1); lean_inc(x_34); lean_dec(x_31); -x_35 = l_usizeSz; +x_35 = l_USize_size; x_36 = lean_nat_dec_lt(x_35, x_34); if (x_36 == 0) { @@ -3498,7 +3498,7 @@ lean_inc(x_42); x_43 = lean_ctor_get(x_40, 1); lean_inc(x_43); lean_dec(x_40); -x_44 = l_usizeSz; +x_44 = l_USize_size; x_45 = lean_nat_dec_lt(x_44, x_43); if (x_45 == 0) { diff --git a/stage0/stdlib/Lean/Expr.c b/stage0/stdlib/Lean/Expr.c index 9c74978063..da74ded01a 100644 --- a/stage0/stdlib/Lean/Expr.c +++ b/stage0/stdlib/Lean/Expr.c @@ -35,7 +35,7 @@ lean_object* l_Lean_Expr_bindingDomain_x21___boxed(lean_object*); uint8_t l_Lean_Expr_isCharLit(lean_object*); lean_object* l_Lean_Expr_letName_x21(lean_object*); uint8_t l_Lean_Expr_isNatLit(lean_object*); -extern lean_object* l_Init_Prelude___instance__32; +extern uint64_t l_Init_Prelude___instance__32; lean_object* l_Lean_mkFreshMVarId___rarg(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateFn_match__1(lean_object*); lean_object* l_Lean_BinderInfo_isAuxDecl_match__1___rarg(uint8_t, lean_object*, lean_object*); @@ -80,7 +80,7 @@ lean_object* l_Lean_Expr_isLit___boxed(lean_object*); lean_object* l_Lean_Expr_replaceFVars___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_updateLambda_x21___closed__3; lean_object* l_Lean_Expr_getAppFn_match__1___rarg(lean_object*, lean_object*, lean_object*); -extern lean_object* l_Init_Prelude___instance__32___closed__1; +extern uint64_t l_Init_Prelude___instance__32___closed__1; uint64_t l_UInt64_add(uint64_t, uint64_t); lean_object* l_Lean_Expr_constName_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_isStringLit_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -451,6 +451,7 @@ lean_object* l_Lean_mkFVar(lean_object*); lean_object* l_Lean_Expr_getAutoParamTactic_x3f___closed__1; uint8_t l_Lean_Expr_Data_binderInfo(uint64_t); lean_object* l_Lean_ExprStructEq_Lean_Expr___instance__20___boxed(lean_object*); +lean_object* l_Lean_Expr_mkData___boxed__const__1; lean_object* l_Lean_MData_empty; size_t lean_usize_of_nat(lean_object*); lean_object* l_Lean_mkSimpleThunkType(lean_object*); @@ -471,7 +472,7 @@ lean_object* l_Lean_Lean_Expr___instance__1; lean_object* lean_expr_update_proj(lean_object*, lean_object*); lean_object* l_Lean_Level_instantiateParams___at_Lean_Expr_instantiateLevelParamsArray___spec__3(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_looseBVarRange(lean_object*); -lean_object* l_Lean_Lean_Expr___instance__9; +uint64_t l_Lean_Lean_Expr___instance__9; lean_object* l_Lean_Lean_Expr___instance__1___closed__1; lean_object* l_Lean_Expr_bvarIdx_x21(lean_object*); lean_object* l_Lean_Expr_updateProj_x21___closed__2; @@ -487,6 +488,7 @@ lean_object* l_Lean_Expr_updateLambda_x21___closed__1; lean_object* l_Lean_mkAppN___boxed(lean_object*, lean_object*); lean_object* l_Lean_Expr_bindingInfo_x21_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Expr_mvarId_x21_match__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Expr_mkDataForLet___boxed__const__1; lean_object* l_Lean_Expr_updateProj_x21___closed__1; lean_object* l_Lean_Lean_Expr___instance__8___closed__1; lean_object* lean_level_update_imax(lean_object*, lean_object*, lean_object*); @@ -528,6 +530,7 @@ lean_object* l_Lean_Expr_hasMVar___boxed(lean_object*); lean_object* l_Lean_mkForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_le(lean_object*, lean_object*); lean_object* l_Lean_Expr_constLevels_x21___closed__2; +lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1; lean_object* l_Lean_mkApp(lean_object*, lean_object*); lean_object* l_Lean_Expr_getAppNumArgsAux___boxed(lean_object*, lean_object*); size_t l_Lean_Literal_hash(lean_object*); @@ -547,6 +550,7 @@ lean_object* l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1; lean_object* l_Lean_Expr_Data_looseBVarRange___boxed(lean_object*); lean_object* l_Lean_mkAppRev(lean_object*, lean_object*); lean_object* l_Lean_Expr_updateConst_x21_match__1(lean_object*); +lean_object* l_Lean_Expr_mkDataForBinder___boxed__const__1; lean_object* l_Lean_Expr_bvarIdx_x21___closed__1; lean_object* lean_panic_fn(lean_object*, lean_object*); uint32_t l_USize_toUInt32(size_t); @@ -1832,10 +1836,10 @@ x_1 = lean_box(0); return x_1; } } -static lean_object* _init_l_Lean_Lean_Expr___instance__9() { +static uint64_t _init_l_Lean_Lean_Expr___instance__9() { _start: { -lean_object* x_1; +uint64_t x_1; x_1 = l_Init_Prelude___instance__32; return x_1; } @@ -2156,6 +2160,15 @@ x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); return x_6; } } +static lean_object* _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_Lean_Expr___instance__9; +x_2 = lean_box_uint64(x_1); +return x_2; +} +} uint64_t l___private_Lean_Expr_0__Lean_Expr_mkDataCore(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6, uint8_t x_7, uint8_t x_8) { _start: { @@ -2200,9 +2213,9 @@ return x_40; else { lean_object* x_41; lean_object* x_42; lean_object* x_43; uint64_t x_44; -x_41 = l_Lean_Lean_Expr___instance__9; -x_42 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; -x_43 = lean_panic_fn(x_41, x_42); +x_41 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; +x_42 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1; +x_43 = lean_panic_fn(x_42, x_41); x_44 = lean_unbox_uint64(x_43); lean_dec(x_43); return x_44; @@ -2271,6 +2284,15 @@ x_3 = x_2 << x_1; return x_3; } } +static lean_object* _init_l_Lean_Expr_mkData___boxed__const__1() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_Lean_Expr___instance__9; +x_2 = lean_box_uint64(x_1); +return x_2; +} +} uint64_t l_Lean_Expr_mkData(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6) { _start: { @@ -2311,9 +2333,9 @@ return x_34; else { lean_object* x_35; lean_object* x_36; lean_object* x_37; uint64_t x_38; -x_35 = l_Lean_Lean_Expr___instance__9; -x_36 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; -x_37 = lean_panic_fn(x_35, x_36); +x_35 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; +x_36 = l_Lean_Expr_mkData___boxed__const__1; +x_37 = lean_panic_fn(x_36, x_35); x_38 = lean_unbox_uint64(x_37); lean_dec(x_37); return x_38; @@ -2340,6 +2362,15 @@ x_13 = lean_box_uint64(x_12); return x_13; } } +static lean_object* _init_l_Lean_Expr_mkDataForBinder___boxed__const__1() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_Lean_Expr___instance__9; +x_2 = lean_box_uint64(x_1); +return x_2; +} +} uint64_t l_Lean_Expr_mkDataForBinder(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6, uint8_t x_7) { _start: { @@ -2382,9 +2413,9 @@ return x_37; else { lean_object* x_38; lean_object* x_39; lean_object* x_40; uint64_t x_41; -x_38 = l_Lean_Lean_Expr___instance__9; -x_39 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; -x_40 = lean_panic_fn(x_38, x_39); +x_38 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; +x_39 = l_Lean_Expr_mkDataForBinder___boxed__const__1; +x_40 = lean_panic_fn(x_39, x_38); x_41 = lean_unbox_uint64(x_40); lean_dec(x_40); return x_41; @@ -2413,6 +2444,15 @@ x_15 = lean_box_uint64(x_14); return x_15; } } +static lean_object* _init_l_Lean_Expr_mkDataForLet___boxed__const__1() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_Lean_Expr___instance__9; +x_2 = lean_box_uint64(x_1); +return x_2; +} +} uint64_t l_Lean_Expr_mkDataForLet(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, uint8_t x_5, uint8_t x_6, uint8_t x_7) { _start: { @@ -2455,9 +2495,9 @@ return x_37; else { lean_object* x_38; lean_object* x_39; lean_object* x_40; uint64_t x_41; -x_38 = l_Lean_Lean_Expr___instance__9; -x_39 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; -x_40 = lean_panic_fn(x_38, x_39); +x_38 = l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4; +x_39 = l_Lean_Expr_mkDataForLet___boxed__const__1; +x_40 = lean_panic_fn(x_39, x_38); x_41 = lean_unbox_uint64(x_40); lean_dec(x_40); return x_41; @@ -2489,13 +2529,12 @@ return x_15; static lean_object* _init_l_Lean_Expr_Lean_Expr___instance__11___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; uint64_t x_4; +lean_object* x_1; uint64_t x_2; lean_object* x_3; x_1 = l_Lean_levelZero; x_2 = l_Init_Prelude___instance__32___closed__1; x_3 = lean_alloc_ctor(3, 1, 8); lean_ctor_set(x_3, 0, x_1); -x_4 = lean_unbox_uint64(x_2); -lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_4); +lean_ctor_set_uint64(x_3, sizeof(void*)*1, x_2); return x_3; } } @@ -15706,7 +15745,6 @@ lean_mark_persistent(l_Lean_Lean_Expr___instance__8); l_Lean_MData_empty = _init_l_Lean_MData_empty(); lean_mark_persistent(l_Lean_MData_empty); l_Lean_Lean_Expr___instance__9 = _init_l_Lean_Lean_Expr___instance__9(); -lean_mark_persistent(l_Lean_Lean_Expr___instance__9); l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1(); lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__1); l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__2(); @@ -15715,10 +15753,18 @@ l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__3 = _init_l___private_Le lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__3); l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4(); lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___closed__4); +l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1 = _init_l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1(); +lean_mark_persistent(l___private_Lean_Expr_0__Lean_Expr_mkDataCore___boxed__const__1); l_Lean_Expr_mkData___closed__1 = _init_l_Lean_Expr_mkData___closed__1(); l_Lean_Expr_mkData___closed__2 = _init_l_Lean_Expr_mkData___closed__2(); l_Lean_Expr_mkData___closed__3 = _init_l_Lean_Expr_mkData___closed__3(); l_Lean_Expr_mkData___closed__4 = _init_l_Lean_Expr_mkData___closed__4(); +l_Lean_Expr_mkData___boxed__const__1 = _init_l_Lean_Expr_mkData___boxed__const__1(); +lean_mark_persistent(l_Lean_Expr_mkData___boxed__const__1); +l_Lean_Expr_mkDataForBinder___boxed__const__1 = _init_l_Lean_Expr_mkDataForBinder___boxed__const__1(); +lean_mark_persistent(l_Lean_Expr_mkDataForBinder___boxed__const__1); +l_Lean_Expr_mkDataForLet___boxed__const__1 = _init_l_Lean_Expr_mkDataForLet___boxed__const__1(); +lean_mark_persistent(l_Lean_Expr_mkDataForLet___boxed__const__1); l_Lean_Expr_Lean_Expr___instance__11___closed__1 = _init_l_Lean_Expr_Lean_Expr___instance__11___closed__1(); lean_mark_persistent(l_Lean_Expr_Lean_Expr___instance__11___closed__1); l_Lean_Expr_Lean_Expr___instance__11 = _init_l_Lean_Expr_Lean_Expr___instance__11(); diff --git a/stage0/stdlib/Lean/Level.c b/stage0/stdlib/Lean/Level.c index 9caca7ef35..9540cb7329 100644 --- a/stage0/stdlib/Lean/Level.c +++ b/stage0/stdlib/Lean/Level.c @@ -26,7 +26,7 @@ lean_object* l_Array_qsort_sort___at_Lean_Level_normalize___spec__2___boxed(lean lean_object* l_Lean_Level_isMax___boxed(lean_object*); lean_object* l_Lean_Level_isSucc_match__1(lean_object*); extern lean_object* l_Lean_Syntax_strLitToAtom___closed__3; -extern lean_object* l_Init_Prelude___instance__32; +extern uint64_t l_Init_Prelude___instance__32; lean_object* l_Lean_Level_mvarId_x21___closed__2; lean_object* l_Lean_Level_dec_match__1(lean_object*); lean_object* l_Lean_Level_LevelToFormat_Result_format___closed__5; @@ -238,6 +238,7 @@ lean_object* l_Lean_Level_normalize(lean_object*); uint64_t l_UInt64_shiftLeft(uint64_t, uint64_t); lean_object* l_Lean_Level_mkNaryMax_match__1(lean_object*); extern lean_object* l_Lean_Format_paren___closed__2; +lean_object* l_Lean_Level_mkData___boxed__const__1; lean_object* l_Lean_Level_dec_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Level_updateSucc_x21___closed__2; lean_object* l_Lean_Level_normLtAux_match__1(lean_object*); @@ -254,7 +255,7 @@ lean_object* l_Nat_imax(lean_object*, lean_object*); lean_object* l_Lean_Level_depthEx___boxed(lean_object*); lean_object* lean_level_update_succ(lean_object*, lean_object*); lean_object* l_Lean_Level_getLevelOffset(lean_object*); -lean_object* l_Lean_Lean_Level___instance__1; +uint64_t l_Lean_Lean_Level___instance__1; lean_object* l_Lean_Level_updateIMax_x21_match__1(lean_object*); lean_object* l_Lean_fmt___at_Lean_Level_LevelToFormat_toResult___spec__1(lean_object*); lean_object* l_Lean_Level_dec___boxed(lean_object*); @@ -351,10 +352,10 @@ lean_dec(x_1); return x_3; } } -static lean_object* _init_l_Lean_Lean_Level___instance__1() { +static uint64_t _init_l_Lean_Lean_Level___instance__1() { _start: { -lean_object* x_1; +uint64_t x_1; x_1 = l_Init_Prelude___instance__32; return x_1; } @@ -514,6 +515,15 @@ x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); return x_6; } } +static lean_object* _init_l_Lean_Level_mkData___boxed__const__1() { +_start: +{ +uint64_t x_1; lean_object* x_2; +x_1 = l_Lean_Lean_Level___instance__1; +x_2 = lean_box_uint64(x_1); +return x_2; +} +} uint64_t l_Lean_Level_mkData(size_t x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4) { _start: { @@ -542,9 +552,9 @@ return x_20; else { lean_object* x_21; lean_object* x_22; lean_object* x_23; uint64_t x_24; -x_21 = l_Lean_Lean_Level___instance__1; -x_22 = l_Lean_Level_mkData___closed__5; -x_23 = lean_panic_fn(x_21, x_22); +x_21 = l_Lean_Level_mkData___closed__5; +x_22 = l_Lean_Level_mkData___boxed__const__1; +x_23 = lean_panic_fn(x_22, x_21); x_24 = lean_unbox_uint64(x_23); lean_dec(x_23); return x_24; @@ -6583,7 +6593,6 @@ res = initialize_Lean_Data_Format(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Lean_Level___instance__1 = _init_l_Lean_Lean_Level___instance__1(); -lean_mark_persistent(l_Lean_Lean_Level___instance__1); l_Lean_Level_mkData___closed__1 = _init_l_Lean_Level_mkData___closed__1(); lean_mark_persistent(l_Lean_Level_mkData___closed__1); l_Lean_Level_mkData___closed__2 = _init_l_Lean_Level_mkData___closed__2(); @@ -6594,6 +6603,8 @@ l_Lean_Level_mkData___closed__4 = _init_l_Lean_Level_mkData___closed__4(); lean_mark_persistent(l_Lean_Level_mkData___closed__4); l_Lean_Level_mkData___closed__5 = _init_l_Lean_Level_mkData___closed__5(); lean_mark_persistent(l_Lean_Level_mkData___closed__5); +l_Lean_Level_mkData___boxed__const__1 = _init_l_Lean_Level_mkData___boxed__const__1(); +lean_mark_persistent(l_Lean_Level_mkData___boxed__const__1); l_Lean_Level_Lean_Level___instance__3___closed__1 = _init_l_Lean_Level_Lean_Level___instance__3___closed__1(); lean_mark_persistent(l_Lean_Level_Lean_Level___instance__3___closed__1); l_Lean_Level_Lean_Level___instance__3 = _init_l_Lean_Level_Lean_Level___instance__3(); diff --git a/stage0/stdlib/Std/Data/PersistentArray.c b/stage0/stdlib/Std/Data/PersistentArray.c index bea5b12eb1..23ca275fff 100644 --- a/stage0/stdlib/Std/Data/PersistentArray.c +++ b/stage0/stdlib/Std/Data/PersistentArray.c @@ -479,6 +479,7 @@ lean_object* l_Std_PersistentArray_stats___rarg(lean_object*); lean_object* l_Array_foldlMUnsafe_fold___at_Array_toPersistentArray___spec__1___rarg(lean_object*, size_t, size_t, lean_object*); lean_object* l_Std_PersistentArray_forMAux_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Std_PersistentArray_toList___spec__3(lean_object*); +extern lean_object* l_USize_size; lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlMAux___at_Std_PersistentArray_filter___spec__10(lean_object*); lean_object* l_Array_findSomeRevM_x3f_find___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_anyMAux___rarg(lean_object*, lean_object*, lean_object*); @@ -536,7 +537,6 @@ lean_object* l_Std_PersistentArray_push(lean_object*); lean_object* l_Std_PersistentArray_findSomeM_x3f___at_Std_PersistentArray_findSome_x3f___spec__1(lean_object*, lean_object*); lean_object* l___private_Std_Data_PersistentArray_0__Std_PersistentArray_foldlFromMAux_match__1(lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_findSomeMAux___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -extern lean_object* l_usizeSz; lean_object* l_Array_foldlMUnsafe_fold___at_Std_PersistentArray_foldl___spec__8___rarg(lean_object*, lean_object*, size_t, size_t, lean_object*); lean_object* l_Std_PersistentArray_foldlM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Std_PersistentArray_modifyAux_match__1(lean_object*, lean_object*); @@ -2090,7 +2090,7 @@ static lean_object* _init_l_Std_PersistentArray_tooBig___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_usizeSz; +x_1 = l_USize_size; x_2 = lean_unsigned_to_nat(8u); x_3 = lean_nat_div(x_1, x_2); return x_3;