max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Kim Morrison 2024-09-10 17:59:00 +10:00
parent c209d0d745
commit 6c97c4ce37
11 changed files with 1976 additions and 1556 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
stage0/stdlib/Init/Data.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Bool Init.Data.BitVec Init.Data.Cast Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.Array.Subarray.Split Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Ord Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream Init.Data.Prod Init.Data.AC Init.Data.Queue Init.Data.Channel Init.Data.Cast Init.Data.Sum Init.Data.BEq Init.Data.Subtype Init.Data.ULift Init.Data.PLift
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Bool Init.Data.BitVec Init.Data.Cast Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.Array.Subarray.Split Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Ord Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream Init.Data.Prod Init.Data.AC Init.Data.Queue Init.Data.Channel Init.Data.Cast Init.Data.Sum Init.Data.BEq Init.Data.Subtype Init.Data.ULift Init.Data.PLift Init.Data.Zero Init.Data.NeZero
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -48,6 +48,8 @@ lean_object* initialize_Init_Data_BEq(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Subtype(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_ULift(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_PLift(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Zero(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_NeZero(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -158,6 +160,12 @@ lean_dec_ref(res);
res = initialize_Init_Data_PLift(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Zero(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_NeZero(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

33
stage0/stdlib/Init/Data/Fin/Basic.c generated
View file

@ -46,7 +46,7 @@ LEAN_EXPORT lean_object* l_Fin_ofNat_x27___boxed(lean_object*, lean_object*, lea
LEAN_EXPORT lean_object* l_Fin_instDiv___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Fin_castLT___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_instDiv(lean_object*);
LEAN_EXPORT lean_object* l_Fin_instOfNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_instOfNat(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_ofNat___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_instMod___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Fin_castSucc___rarg___boxed(lean_object*);
@ -86,7 +86,7 @@ LEAN_EXPORT lean_object* l_Fin_subNat___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Fin_subNat(lean_object*);
LEAN_EXPORT lean_object* l_Fin_castLT___boxed(lean_object*, lean_object*);
lean_object* lean_nat_lxor(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_instOfNat___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_instOfNat___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_cast___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Fin_modn___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Fin_shiftRight(lean_object*, lean_object*, lean_object*);
@ -645,31 +645,34 @@ lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Fin_instOfNat(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Fin_instOfNat(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3;
x_3 = l_Fin_ofNat(x_1, x_2);
return x_3;
lean_object* x_4;
x_4 = lean_nat_mod(x_3, x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Fin_instOfNat___boxed(lean_object* x_1, lean_object* x_2) {
LEAN_EXPORT lean_object* l_Fin_instOfNat___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3;
x_3 = l_Fin_instOfNat(x_1, x_2);
lean_dec(x_2);
lean_object* x_4;
x_4 = l_Fin_instOfNat(x_1, x_2, x_3);
lean_dec(x_3);
lean_dec(x_1);
return x_3;
return x_4;
}
}
LEAN_EXPORT lean_object* l_Fin_instInhabitedHAddNatOfNat(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Fin_ofNat(x_1, x_2);
return x_3;
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = lean_unsigned_to_nat(1u);
x_3 = lean_nat_add(x_1, x_2);
x_4 = lean_unsigned_to_nat(0u);
x_5 = lean_nat_mod(x_4, x_3);
lean_dec(x_3);
return x_5;
}
}
LEAN_EXPORT lean_object* l_Fin_instInhabitedHAddNatOfNat___boxed(lean_object* x_1) {

6
stage0/stdlib/Init/Data/Nat/Basic.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Nat.Basic
// Imports: Init.SimpLemmas
// Imports: Init.SimpLemmas Init.Data.NeZero
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -1020,6 +1020,7 @@ return x_4;
}
}
lean_object* initialize_Init_SimpLemmas(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_NeZero(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Nat_Basic(uint8_t builtin, lean_object* w) {
lean_object * res;
@ -1028,6 +1029,9 @@ _G_initialized = true;
res = initialize_Init_SimpLemmas(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_NeZero(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Nat_instTransLt = _init_l_Nat_instTransLt();
l_Nat_instTransLe = _init_l_Nat_instTransLe();
l_Nat_instTransLtLe = _init_l_Nat_instTransLtLe();

29
stage0/stdlib/Init/Data/NeZero.c generated Normal file
View file

@ -0,0 +1,29 @@
// Lean compiler output
// Module: Init.Data.NeZero
// Imports: Init.Data.Zero
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* initialize_Init_Data_Zero(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_NeZero(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Data_Zero(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

83
stage0/stdlib/Init/Data/Zero.c generated Normal file
View file

@ -0,0 +1,83 @@
// Lean compiler output
// Module: Init.Data.Zero
// Imports: Init.Core
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
LEAN_EXPORT lean_object* l_Zero_ofOfNat0___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Zero_ofOfNat0(lean_object*);
LEAN_EXPORT lean_object* l_Zero_toOfNat0___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Zero_toOfNat0___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Zero_toOfNat0(lean_object*);
LEAN_EXPORT lean_object* l_Zero_ofOfNat0___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Zero_toOfNat0___rarg(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Zero_toOfNat0(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Zero_toOfNat0___rarg___boxed), 1, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Zero_toOfNat0___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Zero_toOfNat0___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Zero_ofOfNat0___rarg(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
LEAN_EXPORT lean_object* l_Zero_ofOfNat0(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Zero_ofOfNat0___rarg___boxed), 1, 0);
return x_2;
}
}
LEAN_EXPORT lean_object* l_Zero_ofOfNat0___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Zero_ofOfNat0___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* initialize_Init_Core(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
LEAN_EXPORT lean_object* initialize_Init_Data_Zero(uint8_t builtin, lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Core(builtin, lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

129
stage0/stdlib/Lean/Meta/LitValues.c generated
View file

@ -60,10 +60,12 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getCharValue_x3f___lambda__1___boxed(lean_o
LEAN_EXPORT lean_object* l_Lean_Meta_normLitValue___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_getBitVecValue_x3f___closed__2;
static lean_object* l_Lean_Loop_forIn_loop___at_Lean_Meta_getListLitOf_x3f___spec__1___rarg___closed__1;
static lean_object* l_Lean_Meta_normLitValue___lambda__9___closed__5;
static lean_object* l_Lean_Meta_normLitValue___lambda__2___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_getUInt32Value_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_litToCtor___lambda__2___closed__1;
LEAN_EXPORT lean_object* l_Lean_Meta_normLitValue(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_normLitValue___lambda__9___closed__6;
static lean_object* l_Lean_Meta_litToCtor___lambda__1___closed__25;
static lean_object* l_Lean_Meta_normLitValue___lambda__2___closed__6;
static lean_object* l_Lean_Meta_litToCtor___lambda__1___closed__9;
@ -186,6 +188,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_getIntValue_x3f___lambda__1___boxed(lean_ob
static lean_object* l_Lean_Meta_normLitValue___lambda__9___closed__3;
LEAN_EXPORT lean_object* l_Lean_Loop_forIn_loop___at_Lean_Meta_getListLitOf_x3f___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_isLitValue___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_normLitValue___lambda__9___closed__4;
static lean_object* l_Lean_Meta_litToCtor___lambda__1___closed__17;
lean_object* l_Lean_Expr_app___override(lean_object*, lean_object*);
static lean_object* l_Lean_Meta_normLitValue___lambda__9___closed__1;
@ -4439,6 +4442,34 @@ x_3 = l_Lean_Expr_const___override(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_normLitValue___lambda__9___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("instNeZeroSucc", 14, 14);
return x_1;
}
}
static lean_object* _init_l_Lean_Meta_normLitValue___lambda__9___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_getNatValue_x3f___lambda__1___closed__1;
x_2 = l_Lean_Meta_normLitValue___lambda__9___closed__4;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Meta_normLitValue___lambda__9___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_normLitValue___lambda__9___closed__5;
x_3 = l_Lean_Expr_const___override(x_2, x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_Meta_normLitValue___lambda__9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
@ -4478,7 +4509,7 @@ lean_dec(x_9);
x_14 = !lean_is_exclusive(x_8);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28;
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_15 = lean_ctor_get(x_8, 0);
lean_dec(x_15);
x_16 = lean_ctor_get(x_13, 0);
@ -4490,76 +4521,82 @@ x_18 = l_Lean_mkRawNatLit(x_17);
lean_inc(x_16);
x_19 = l_Lean_mkNatLit(x_16);
x_20 = l_Lean_Meta_normLitValue___lambda__9___closed__1;
lean_inc(x_19);
x_21 = l_Lean_Expr_app___override(x_20, x_19);
x_22 = lean_unsigned_to_nat(1u);
x_23 = lean_nat_sub(x_16, x_22);
lean_dec(x_16);
x_24 = l_Lean_mkNatLit(x_23);
x_25 = l_Lean_Meta_normLitValue___lambda__9___closed__3;
x_25 = l_Lean_Meta_normLitValue___lambda__9___closed__6;
x_26 = l_Lean_Expr_app___override(x_25, x_24);
x_27 = l_Lean_Meta_normLitValue___lambda__9___closed__3;
lean_inc(x_18);
x_26 = l_Lean_mkAppB(x_25, x_24, x_18);
x_27 = l_Lean_Meta_normLitValue___lambda__2___closed__3;
x_28 = l_Lean_mkApp3(x_27, x_21, x_18, x_26);
lean_ctor_set(x_8, 0, x_28);
x_28 = l_Lean_mkApp3(x_27, x_19, x_26, x_18);
x_29 = l_Lean_Meta_normLitValue___lambda__2___closed__3;
x_30 = l_Lean_mkApp3(x_29, x_21, x_18, x_28);
lean_ctor_set(x_8, 0, x_30);
return x_8;
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_29 = lean_ctor_get(x_8, 1);
lean_inc(x_29);
lean_dec(x_8);
x_30 = lean_ctor_get(x_13, 0);
lean_inc(x_30);
x_31 = lean_ctor_get(x_13, 1);
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_31 = lean_ctor_get(x_8, 1);
lean_inc(x_31);
lean_dec(x_13);
x_32 = l_Lean_mkRawNatLit(x_31);
lean_inc(x_30);
x_33 = l_Lean_mkNatLit(x_30);
x_34 = l_Lean_Meta_normLitValue___lambda__9___closed__1;
x_35 = l_Lean_Expr_app___override(x_34, x_33);
x_36 = lean_unsigned_to_nat(1u);
x_37 = lean_nat_sub(x_30, x_36);
lean_dec(x_30);
x_38 = l_Lean_mkNatLit(x_37);
x_39 = l_Lean_Meta_normLitValue___lambda__9___closed__3;
lean_dec(x_8);
x_32 = lean_ctor_get(x_13, 0);
lean_inc(x_32);
x_40 = l_Lean_mkAppB(x_39, x_38, x_32);
x_41 = l_Lean_Meta_normLitValue___lambda__2___closed__3;
x_42 = l_Lean_mkApp3(x_41, x_35, x_32, x_40);
x_43 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_29);
return x_43;
x_33 = lean_ctor_get(x_13, 1);
lean_inc(x_33);
lean_dec(x_13);
x_34 = l_Lean_mkRawNatLit(x_33);
lean_inc(x_32);
x_35 = l_Lean_mkNatLit(x_32);
x_36 = l_Lean_Meta_normLitValue___lambda__9___closed__1;
lean_inc(x_35);
x_37 = l_Lean_Expr_app___override(x_36, x_35);
x_38 = lean_unsigned_to_nat(1u);
x_39 = lean_nat_sub(x_32, x_38);
lean_dec(x_32);
x_40 = l_Lean_mkNatLit(x_39);
x_41 = l_Lean_Meta_normLitValue___lambda__9___closed__6;
x_42 = l_Lean_Expr_app___override(x_41, x_40);
x_43 = l_Lean_Meta_normLitValue___lambda__9___closed__3;
lean_inc(x_34);
x_44 = l_Lean_mkApp3(x_43, x_35, x_42, x_34);
x_45 = l_Lean_Meta_normLitValue___lambda__2___closed__3;
x_46 = l_Lean_mkApp3(x_45, x_37, x_34, x_44);
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_31);
return x_47;
}
}
}
else
{
uint8_t x_44;
uint8_t x_48;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_44 = !lean_is_exclusive(x_8);
if (x_44 == 0)
x_48 = !lean_is_exclusive(x_8);
if (x_48 == 0)
{
return x_8;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_8, 0);
x_46 = lean_ctor_get(x_8, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_8, 0);
x_50 = lean_ctor_get(x_8, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_8);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
}
@ -7943,6 +7980,12 @@ l_Lean_Meta_normLitValue___lambda__9___closed__2 = _init_l_Lean_Meta_normLitValu
lean_mark_persistent(l_Lean_Meta_normLitValue___lambda__9___closed__2);
l_Lean_Meta_normLitValue___lambda__9___closed__3 = _init_l_Lean_Meta_normLitValue___lambda__9___closed__3();
lean_mark_persistent(l_Lean_Meta_normLitValue___lambda__9___closed__3);
l_Lean_Meta_normLitValue___lambda__9___closed__4 = _init_l_Lean_Meta_normLitValue___lambda__9___closed__4();
lean_mark_persistent(l_Lean_Meta_normLitValue___lambda__9___closed__4);
l_Lean_Meta_normLitValue___lambda__9___closed__5 = _init_l_Lean_Meta_normLitValue___lambda__9___closed__5();
lean_mark_persistent(l_Lean_Meta_normLitValue___lambda__9___closed__5);
l_Lean_Meta_normLitValue___lambda__9___closed__6 = _init_l_Lean_Meta_normLitValue___lambda__9___closed__6();
lean_mark_persistent(l_Lean_Meta_normLitValue___lambda__9___closed__6);
l_Lean_Meta_normLitValue___lambda__10___closed__1 = _init_l_Lean_Meta_normLitValue___lambda__10___closed__1();
lean_mark_persistent(l_Lean_Meta_normLitValue___lambda__10___closed__1);
l_Lean_Meta_normLitValue___lambda__10___closed__2 = _init_l_Lean_Meta_normLitValue___lambda__10___closed__2();

1040
stage0/stdlib/Lean/Meta/Match/Match.c generated
View file

File diff suppressed because it is too large Load diff

225
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.c generated
View file

@ -478,6 +478,7 @@ static lean_object* l___regBuiltin_BitVec_reduceReplicate_declare__1____x40_Lean
static lean_object* l_BitVec_reduceHShiftRight___closed__3;
LEAN_EXPORT lean_object* l___regBuiltin_BitVec_reduceULT_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_4241_(lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_BitVec_reduceSShiftRight_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_2215_(lean_object*);
static lean_object* l_BitVec_reduceBitVecToFin___lambda__1___closed__11;
LEAN_EXPORT lean_object* l___regBuiltin_BitVec_reduceGT_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_4177_(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_reduceUShiftRight___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_reduceBin(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -612,6 +613,7 @@ static lean_object* l_BitVec_reduceGE___closed__2;
LEAN_EXPORT lean_object* l_BitVec_reduceUShiftRight(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appFnCleanup(lean_object*, lean_object*);
static lean_object* l___regBuiltin_BitVec_reduceMul_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1791____closed__12;
static lean_object* l_BitVec_reduceBitVecToFin___lambda__1___closed__13;
static lean_object* l___regBuiltin_BitVec_reduceCast_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_3065____closed__6;
lean_object* l_BitVec_srem(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___regBuiltin_BitVec_reduceSDiv_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_2077_(lean_object*);
@ -790,6 +792,7 @@ LEAN_EXPORT lean_object* l_BitVec_reduceBitVecToFin___lambda__1(lean_object*, le
LEAN_EXPORT lean_object* l___regBuiltin_BitVec_reduceSRem_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_2050_(lean_object*);
static lean_object* l___regBuiltin_BitVec_reduceNeg_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1532____closed__12;
static lean_object* l___regBuiltin_BitVec_reduceAdd_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1751____closed__8;
static lean_object* l_BitVec_reduceBitVecToFin___lambda__1___closed__10;
static lean_object* l___regBuiltin_BitVec_reduceULT_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_4237____closed__7;
static lean_object* l___regBuiltin_BitVec_reduceZeroExtend_x27_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_4632____closed__2;
static lean_object* l___regBuiltin_BitVec_reduceNe_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_4050____closed__6;
@ -829,6 +832,7 @@ static lean_object* l___regBuiltin_BitVec_reduceSMTUDiv_declare__1____x40_Lean_M
static lean_object* l___regBuiltin_BitVec_reduceXOr_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1711____closed__3;
static lean_object* l___regBuiltin_BitVec_reduceNeg_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1532____closed__1;
static lean_object* l___regBuiltin_BitVec_reduceMul_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1791____closed__7;
static lean_object* l_BitVec_reduceBitVecToFin___lambda__1___closed__12;
LEAN_EXPORT lean_object* l_BitVec_reduceBitVecToFin(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_reduceOfNat___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_BitVec_reduceUMod_declare__1____x40_Lean_Meta_Tactic_Simp_BuiltinSimprocs_BitVec___hyg_1940____closed__1;
@ -28076,6 +28080,42 @@ x_3 = l_Lean_Expr_const___override(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__10() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("Nat", 3, 3);
return x_1;
}
}
static lean_object* _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("instNeZeroSucc", 14, 14);
return x_1;
}
}
static lean_object* _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__12() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_BitVec_reduceBitVecToFin___lambda__1___closed__10;
x_2 = l_BitVec_reduceBitVecToFin___lambda__1___closed__11;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__13() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_BitVec_reduceBitVecToFin___lambda__1___closed__12;
x_3 = l_Lean_Expr_const___override(x_2, x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_BitVec_reduceBitVecToFin___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
@ -28122,7 +28162,7 @@ uint8_t x_19;
x_19 = !lean_is_exclusive(x_10);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_20 = lean_ctor_get(x_11, 0);
x_21 = lean_ctor_get(x_10, 0);
lean_dec(x_21);
@ -28138,128 +28178,137 @@ x_26 = l_Lean_mkRawNatLit(x_23);
lean_inc(x_25);
x_27 = l_Lean_mkNatLit(x_25);
x_28 = l_BitVec_reduceBitVecToFin___lambda__1___closed__6;
lean_inc(x_27);
x_29 = l_Lean_Expr_app___override(x_28, x_27);
x_30 = lean_unsigned_to_nat(1u);
x_31 = lean_nat_sub(x_25, x_30);
lean_dec(x_25);
x_32 = l_Lean_mkNatLit(x_31);
x_33 = l_BitVec_reduceBitVecToFin___lambda__1___closed__9;
x_33 = l_BitVec_reduceBitVecToFin___lambda__1___closed__13;
x_34 = l_Lean_Expr_app___override(x_33, x_32);
x_35 = l_BitVec_reduceBitVecToFin___lambda__1___closed__9;
lean_inc(x_26);
x_34 = l_Lean_mkAppB(x_33, x_32, x_26);
x_35 = l_BitVec_reduceBitVecToFin___lambda__1___closed__3;
x_36 = l_Lean_mkApp3(x_35, x_29, x_26, x_34);
x_36 = l_Lean_mkApp3(x_35, x_27, x_34, x_26);
x_37 = l_BitVec_reduceBitVecToFin___lambda__1___closed__3;
x_38 = l_Lean_mkApp3(x_37, x_29, x_26, x_36);
lean_ctor_set_tag(x_11, 0);
lean_ctor_set(x_11, 0, x_36);
lean_ctor_set(x_11, 0, x_38);
return x_10;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_37 = lean_ctor_get(x_11, 0);
x_38 = lean_ctor_get(x_10, 1);
lean_inc(x_38);
lean_dec(x_10);
x_39 = lean_ctor_get(x_37, 0);
lean_inc(x_39);
x_40 = lean_ctor_get(x_37, 1);
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_39 = lean_ctor_get(x_11, 0);
x_40 = lean_ctor_get(x_10, 1);
lean_inc(x_40);
lean_dec(x_37);
x_41 = lean_unsigned_to_nat(2u);
x_42 = lean_nat_pow(x_41, x_39);
lean_dec(x_39);
x_43 = l_Lean_mkRawNatLit(x_40);
lean_dec(x_10);
x_41 = lean_ctor_get(x_39, 0);
lean_inc(x_41);
x_42 = lean_ctor_get(x_39, 1);
lean_inc(x_42);
x_44 = l_Lean_mkNatLit(x_42);
x_45 = l_BitVec_reduceBitVecToFin___lambda__1___closed__6;
x_46 = l_Lean_Expr_app___override(x_45, x_44);
x_47 = lean_unsigned_to_nat(1u);
x_48 = lean_nat_sub(x_42, x_47);
lean_dec(x_42);
x_49 = l_Lean_mkNatLit(x_48);
x_50 = l_BitVec_reduceBitVecToFin___lambda__1___closed__9;
lean_inc(x_43);
x_51 = l_Lean_mkAppB(x_50, x_49, x_43);
x_52 = l_BitVec_reduceBitVecToFin___lambda__1___closed__3;
x_53 = l_Lean_mkApp3(x_52, x_46, x_43, x_51);
lean_dec(x_39);
x_43 = lean_unsigned_to_nat(2u);
x_44 = lean_nat_pow(x_43, x_41);
lean_dec(x_41);
x_45 = l_Lean_mkRawNatLit(x_42);
lean_inc(x_44);
x_46 = l_Lean_mkNatLit(x_44);
x_47 = l_BitVec_reduceBitVecToFin___lambda__1___closed__6;
lean_inc(x_46);
x_48 = l_Lean_Expr_app___override(x_47, x_46);
x_49 = lean_unsigned_to_nat(1u);
x_50 = lean_nat_sub(x_44, x_49);
lean_dec(x_44);
x_51 = l_Lean_mkNatLit(x_50);
x_52 = l_BitVec_reduceBitVecToFin___lambda__1___closed__13;
x_53 = l_Lean_Expr_app___override(x_52, x_51);
x_54 = l_BitVec_reduceBitVecToFin___lambda__1___closed__9;
lean_inc(x_45);
x_55 = l_Lean_mkApp3(x_54, x_46, x_53, x_45);
x_56 = l_BitVec_reduceBitVecToFin___lambda__1___closed__3;
x_57 = l_Lean_mkApp3(x_56, x_48, x_45, x_55);
lean_ctor_set_tag(x_11, 0);
lean_ctor_set(x_11, 0, x_53);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_11);
lean_ctor_set(x_54, 1, x_38);
return x_54;
lean_ctor_set(x_11, 0, x_57);
x_58 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_58, 0, x_11);
lean_ctor_set(x_58, 1, x_40);
return x_58;
}
}
else
{
lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
x_55 = lean_ctor_get(x_11, 0);
lean_inc(x_55);
lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80;
x_59 = lean_ctor_get(x_11, 0);
lean_inc(x_59);
lean_dec(x_11);
x_56 = lean_ctor_get(x_10, 1);
lean_inc(x_56);
x_60 = lean_ctor_get(x_10, 1);
lean_inc(x_60);
if (lean_is_exclusive(x_10)) {
lean_ctor_release(x_10, 0);
lean_ctor_release(x_10, 1);
x_57 = x_10;
x_61 = x_10;
} else {
lean_dec_ref(x_10);
x_57 = lean_box(0);
x_61 = lean_box(0);
}
x_58 = lean_ctor_get(x_55, 0);
lean_inc(x_58);
x_59 = lean_ctor_get(x_55, 1);
lean_inc(x_59);
lean_dec(x_55);
x_60 = lean_unsigned_to_nat(2u);
x_61 = lean_nat_pow(x_60, x_58);
lean_dec(x_58);
x_62 = l_Lean_mkRawNatLit(x_59);
lean_inc(x_61);
x_63 = l_Lean_mkNatLit(x_61);
x_64 = l_BitVec_reduceBitVecToFin___lambda__1___closed__6;
x_65 = l_Lean_Expr_app___override(x_64, x_63);
x_66 = lean_unsigned_to_nat(1u);
x_67 = lean_nat_sub(x_61, x_66);
lean_dec(x_61);
x_68 = l_Lean_mkNatLit(x_67);
x_69 = l_BitVec_reduceBitVecToFin___lambda__1___closed__9;
x_62 = lean_ctor_get(x_59, 0);
lean_inc(x_62);
x_70 = l_Lean_mkAppB(x_69, x_68, x_62);
x_71 = l_BitVec_reduceBitVecToFin___lambda__1___closed__3;
x_72 = l_Lean_mkApp3(x_71, x_65, x_62, x_70);
x_73 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_73, 0, x_72);
if (lean_is_scalar(x_57)) {
x_74 = lean_alloc_ctor(0, 2, 0);
x_63 = lean_ctor_get(x_59, 1);
lean_inc(x_63);
lean_dec(x_59);
x_64 = lean_unsigned_to_nat(2u);
x_65 = lean_nat_pow(x_64, x_62);
lean_dec(x_62);
x_66 = l_Lean_mkRawNatLit(x_63);
lean_inc(x_65);
x_67 = l_Lean_mkNatLit(x_65);
x_68 = l_BitVec_reduceBitVecToFin___lambda__1___closed__6;
lean_inc(x_67);
x_69 = l_Lean_Expr_app___override(x_68, x_67);
x_70 = lean_unsigned_to_nat(1u);
x_71 = lean_nat_sub(x_65, x_70);
lean_dec(x_65);
x_72 = l_Lean_mkNatLit(x_71);
x_73 = l_BitVec_reduceBitVecToFin___lambda__1___closed__13;
x_74 = l_Lean_Expr_app___override(x_73, x_72);
x_75 = l_BitVec_reduceBitVecToFin___lambda__1___closed__9;
lean_inc(x_66);
x_76 = l_Lean_mkApp3(x_75, x_67, x_74, x_66);
x_77 = l_BitVec_reduceBitVecToFin___lambda__1___closed__3;
x_78 = l_Lean_mkApp3(x_77, x_69, x_66, x_76);
x_79 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_79, 0, x_78);
if (lean_is_scalar(x_61)) {
x_80 = lean_alloc_ctor(0, 2, 0);
} else {
x_74 = x_57;
x_80 = x_61;
}
lean_ctor_set(x_74, 0, x_73);
lean_ctor_set(x_74, 1, x_56);
return x_74;
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_60);
return x_80;
}
}
}
else
{
uint8_t x_75;
x_75 = !lean_is_exclusive(x_10);
if (x_75 == 0)
uint8_t x_81;
x_81 = !lean_is_exclusive(x_10);
if (x_81 == 0)
{
return x_10;
}
else
{
lean_object* x_76; lean_object* x_77; lean_object* x_78;
x_76 = lean_ctor_get(x_10, 0);
x_77 = lean_ctor_get(x_10, 1);
lean_inc(x_77);
lean_inc(x_76);
lean_object* x_82; lean_object* x_83; lean_object* x_84;
x_82 = lean_ctor_get(x_10, 0);
x_83 = lean_ctor_get(x_10, 1);
lean_inc(x_83);
lean_inc(x_82);
lean_dec(x_10);
x_78 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_78, 0, x_76);
lean_ctor_set(x_78, 1, x_77);
return x_78;
x_84 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_84, 0, x_82);
lean_ctor_set(x_84, 1, x_83);
return x_84;
}
}
}
@ -31684,6 +31733,14 @@ l_BitVec_reduceBitVecToFin___lambda__1___closed__8 = _init_l_BitVec_reduceBitVec
lean_mark_persistent(l_BitVec_reduceBitVecToFin___lambda__1___closed__8);
l_BitVec_reduceBitVecToFin___lambda__1___closed__9 = _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__9();
lean_mark_persistent(l_BitVec_reduceBitVecToFin___lambda__1___closed__9);
l_BitVec_reduceBitVecToFin___lambda__1___closed__10 = _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__10();
lean_mark_persistent(l_BitVec_reduceBitVecToFin___lambda__1___closed__10);
l_BitVec_reduceBitVecToFin___lambda__1___closed__11 = _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__11();
lean_mark_persistent(l_BitVec_reduceBitVecToFin___lambda__1___closed__11);
l_BitVec_reduceBitVecToFin___lambda__1___closed__12 = _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__12();
lean_mark_persistent(l_BitVec_reduceBitVecToFin___lambda__1___closed__12);
l_BitVec_reduceBitVecToFin___lambda__1___closed__13 = _init_l_BitVec_reduceBitVecToFin___lambda__1___closed__13();
lean_mark_persistent(l_BitVec_reduceBitVecToFin___lambda__1___closed__13);
l_BitVec_reduceBitVecToFin___closed__1 = _init_l_BitVec_reduceBitVecToFin___closed__1();
lean_mark_persistent(l_BitVec_reduceBitVecToFin___closed__1);
l_BitVec_reduceBitVecToFin___closed__2 = _init_l_BitVec_reduceBitVecToFin___closed__2();

1895
stage0/stdlib/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.c generated
View file

File diff suppressed because it is too large Load diff

54
stage0/stdlib/Lean/ToExpr.c generated
View file

@ -65,6 +65,7 @@ static lean_object* l_Lean_instToExprUInt8___closed__2;
static lean_object* l_Lean_instToExprProd___rarg___lambda__1___closed__3;
static lean_object* l_Lean_instToExprList___rarg___closed__7;
static lean_object* l___private_Lean_ToExpr_0__Lean_Name_toExprAux_go___closed__7;
static lean_object* l_Lean_instToExprFin___lambda__1___closed__6;
lean_object* l_Lean_Expr_lit___override(lean_object*);
static lean_object* l_Lean_instToExprUInt16___closed__3;
static lean_object* l_Lean_instToExprOption___rarg___lambda__1___closed__2;
@ -219,6 +220,7 @@ static lean_object* l_Lean_instToExprInt___lambda__1___closed__8;
LEAN_EXPORT lean_object* l_Lean_instToExprLiteral___lambda__1(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_ToExpr_0__Lean_List_toExprAux___at_Lean_instToExprPreresolved___spec__1(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_instToExprNat___closed__2;
static lean_object* l_Lean_instToExprFin___lambda__1___closed__7;
LEAN_EXPORT lean_object* l___private_Lean_ToExpr_0__Lean_Name_toExprAux_mkStr(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Expr_toCtorIfLit___closed__1;
static lean_object* l_Lean_instToExprUInt32___closed__1;
@ -271,6 +273,7 @@ static lean_object* l_Lean_instToExprLiteral___closed__4;
static lean_object* l_Lean_instToExprInt___closed__3;
static lean_object* l_Lean_instToExprOption___rarg___closed__2;
static lean_object* l_Lean_instToExprFin___lambda__1___closed__3;
static lean_object* l_Lean_instToExprFin___lambda__1___closed__8;
static lean_object* l_Lean_instToExprFilePath___lambda__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_instToExprUnit___lambda__1___boxed(lean_object*);
static lean_object* l_Lean_instToExprNat___closed__5;
@ -715,25 +718,56 @@ x_3 = l_Lean_Expr_const___override(x_2, x_1);
return x_3;
}
}
static lean_object* _init_l_Lean_instToExprFin___lambda__1___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_unchecked("instNeZeroSucc", 14, 14);
return x_1;
}
}
static lean_object* _init_l_Lean_instToExprFin___lambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_instToExprNat___closed__1;
x_2 = l_Lean_instToExprFin___lambda__1___closed__6;
x_3 = l_Lean_Name_mkStr2(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_instToExprFin___lambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_instToExprFin___lambda__1___closed__7;
x_3 = l_Lean_Expr_const___override(x_2, x_1);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_instToExprFin___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_3 = l_Lean_mkRawNatLit(x_2);
lean_inc(x_1);
x_4 = l_Lean_mkNatLit(x_1);
x_5 = l_Lean_instToExprFin___lambda__1___closed__3;
lean_inc(x_4);
x_6 = l_Lean_Expr_app___override(x_5, x_4);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_1, x_7);
lean_dec(x_1);
x_9 = l_Lean_mkNatLit(x_8);
x_10 = l_Lean_instToExprFin___lambda__1___closed__5;
x_10 = l_Lean_instToExprFin___lambda__1___closed__8;
x_11 = l_Lean_Expr_app___override(x_10, x_9);
x_12 = l_Lean_instToExprFin___lambda__1___closed__5;
lean_inc(x_3);
x_11 = l_Lean_mkAppB(x_10, x_9, x_3);
x_12 = l_Lean_instToExprInt_mkNat___closed__6;
x_13 = l_Lean_mkApp3(x_12, x_6, x_3, x_11);
return x_13;
x_13 = l_Lean_mkApp3(x_12, x_4, x_11, x_3);
x_14 = l_Lean_instToExprInt_mkNat___closed__6;
x_15 = l_Lean_mkApp3(x_14, x_6, x_3, x_13);
return x_15;
}
}
static lean_object* _init_l_Lean_instToExprFin___closed__1() {
@ -2008,7 +2042,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l___private_Lean_ToExpr_0__Lean_Name_toExprAux_mkStr___closed__5;
x_2 = l___private_Lean_ToExpr_0__Lean_Name_toExprAux_mkStr___closed__6;
x_3 = lean_unsigned_to_nat(129u);
x_3 = lean_unsigned_to_nat(130u);
x_4 = lean_unsigned_to_nat(11u);
x_5 = l___private_Lean_ToExpr_0__Lean_Name_toExprAux_mkStr___closed__7;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -3523,6 +3557,12 @@ l_Lean_instToExprFin___lambda__1___closed__4 = _init_l_Lean_instToExprFin___lamb
lean_mark_persistent(l_Lean_instToExprFin___lambda__1___closed__4);
l_Lean_instToExprFin___lambda__1___closed__5 = _init_l_Lean_instToExprFin___lambda__1___closed__5();
lean_mark_persistent(l_Lean_instToExprFin___lambda__1___closed__5);
l_Lean_instToExprFin___lambda__1___closed__6 = _init_l_Lean_instToExprFin___lambda__1___closed__6();
lean_mark_persistent(l_Lean_instToExprFin___lambda__1___closed__6);
l_Lean_instToExprFin___lambda__1___closed__7 = _init_l_Lean_instToExprFin___lambda__1___closed__7();
lean_mark_persistent(l_Lean_instToExprFin___lambda__1___closed__7);
l_Lean_instToExprFin___lambda__1___closed__8 = _init_l_Lean_instToExprFin___lambda__1___closed__8();
lean_mark_persistent(l_Lean_instToExprFin___lambda__1___closed__8);
l_Lean_instToExprFin___closed__1 = _init_l_Lean_instToExprFin___closed__1();
lean_mark_persistent(l_Lean_instToExprFin___closed__1);
l_Lean_instToExprBitVec___lambda__1___closed__1 = _init_l_Lean_instToExprBitVec___lambda__1___closed__1();

28
stage0/stdlib/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.c generated
View file

@ -48,7 +48,6 @@ lean_object* l_BitVec_shiftLeft(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_shiftr(lean_object*, lean_object*);
static lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Basic_0__Std_Tactic_BVDecide_reprBVBit____x40_Std_Tactic_BVDecide_Bitblast_BVExpr_Basic___hyg_287____closed__1;
static lean_object* l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Basic_0__Std_Tactic_BVDecide_reprBVBit____x40_Std_Tactic_BVDecide_Bitblast_BVExpr_Basic___hyg_287____closed__17;
lean_object* l_Fin_ofNat(lean_object*, lean_object*);
LEAN_EXPORT uint64_t l___private_Std_Tactic_BVDecide_Bitblast_BVExpr_Basic_0__Std_Tactic_BVDecide_hashBVBit____x40_Std_Tactic_BVDecide_Bitblast_BVExpr_Basic___hyg_35_(lean_object*);
LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_eval(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Tactic_BVDecide_BVUnOp_toString___closed__3;
@ -64,7 +63,6 @@ static lean_object* l_Std_Tactic_BVDecide_BVBinPred_toString___closed__1;
static lean_object* l_Std_Tactic_BVDecide_BVBinPred_instToString___closed__1;
lean_object* l_BitVec_not(lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
static lean_object* l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__2;
LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVUnOp_eval___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Std_Tactic_BVDecide_BVExpr_Assignment_getD(lean_object*, lean_object*);
static lean_object* l_Std_Tactic_BVDecide_BVBinOp_noConfusion___rarg___closed__1;
@ -624,31 +622,21 @@ return x_12;
static lean_object* _init_l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Fin_ofNat(x_1, x_1);
return x_2;
}
}
static lean_object* _init_l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
return x_4;
x_3 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
lean_ctor_set(x_3, 2, x_2);
return x_3;
}
}
static lean_object* _init_l_Std_Tactic_BVDecide_instInhabitedBVBit() {
_start:
{
lean_object* x_1;
x_1 = l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__2;
x_1 = l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__1;
return x_1;
}
}
@ -2130,8 +2118,6 @@ l_Std_Tactic_BVDecide_instToStringBVBit___closed__3 = _init_l_Std_Tactic_BVDecid
lean_mark_persistent(l_Std_Tactic_BVDecide_instToStringBVBit___closed__3);
l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__1 = _init_l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__1();
lean_mark_persistent(l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__1);
l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__2 = _init_l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__2();
lean_mark_persistent(l_Std_Tactic_BVDecide_instInhabitedBVBit___closed__2);
l_Std_Tactic_BVDecide_instInhabitedBVBit = _init_l_Std_Tactic_BVDecide_instInhabitedBVBit();
lean_mark_persistent(l_Std_Tactic_BVDecide_instInhabitedBVBit);
l_Std_Tactic_BVDecide_BVBinOp_noConfusion___rarg___closed__1 = _init_l_Std_Tactic_BVDecide_BVBinOp_noConfusion___rarg___closed__1();