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

fix(stage0): missing files

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-21 16:39:07 -07:00
parent 91745cd16b
commit 89259d012b
2 changed files with 132 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
src/stage0/init/lean/compiler/initattr.cpp generated Normal file
View file

@ -0,0 +1,84 @@
// Lean compiler output
// Module: init.lean.compiler.initattr
// Imports: init.lean.environment
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
typedef lean::uint8 uint8; typedef lean::uint16 uint16;
typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#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
extern "C" obj* lean_get_init_fn_name_for(obj*, obj*);
obj* l_Lean_hasInitAttr___boxed(obj*, obj*);
extern "C" uint8 lean_is_io_unit_init(obj*, obj*);
uint8 l_Lean_hasInitAttr(obj*, obj*);
obj* l_Lean_getInitFnNameFor___boxed(obj*, obj*);
obj* l_Lean_isIOUnitInitFn___boxed(obj*, obj*);
obj* l_Lean_isIOUnitInitFn___boxed(obj* x_0, obj* x_1) {
_start:
{
uint8 x_2; obj* x_3;
x_2 = lean_is_io_unit_init(x_0, x_1);
x_3 = lean::box(x_2);
lean::dec(x_0);
lean::dec(x_1);
return x_3;
}
}
obj* l_Lean_getInitFnNameFor___boxed(obj* x_0, obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean_get_init_fn_name_for(x_0, x_1);
lean::dec(x_0);
lean::dec(x_1);
return x_2;
}
}
uint8 l_Lean_hasInitAttr(obj* x_0, obj* x_1) {
_start:
{
obj* x_2;
x_2 = lean_get_init_fn_name_for(x_0, x_1);
if (lean::obj_tag(x_2) == 0)
{
uint8 x_3;
x_3 = 0;
return x_3;
}
else
{
uint8 x_5;
lean::dec(x_2);
x_5 = 1;
return x_5;
}
}
}
obj* l_Lean_hasInitAttr___boxed(obj* x_0, obj* x_1) {
_start:
{
uint8 x_2; obj* x_3;
x_2 = l_Lean_hasInitAttr(x_0, x_1);
x_3 = lean::box(x_2);
lean::dec(x_0);
lean::dec(x_1);
return x_3;
}
}
obj* initialize_init_lean_environment(obj*);
static bool _G_initialized = false;
obj* initialize_init_lean_compiler_initattr(obj* w) {
if (_G_initialized) return w;
_G_initialized = true;
if (io_result_is_error(w)) return w;
w = initialize_init_lean_environment(w);
if (io_result_is_error(w)) return w;
return w;
}

48
src/stage0/init/lean/runtime.cpp generated Normal file
View file

@ -0,0 +1,48 @@
// Lean compiler output
// Module: init.lean.runtime
// Imports: init.core
#include "runtime/object.h"
#include "runtime/apply.h"
typedef lean::object obj; typedef lean::usize usize;
typedef lean::uint8 uint8; typedef lean::uint16 uint16;
typedef lean::uint32 uint32; typedef lean::uint64 uint64;
#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
extern "C" obj* lean_closure_max_args(obj*);
obj* l_Lean_closureMaxArgs;
obj* l_Lean_closureMaxArgsFn___boxed(obj*);
obj* l_Lean_closureMaxArgsFn___boxed(obj* x_0) {
_start:
{
obj* x_1;
x_1 = lean_closure_max_args(x_0);
return x_1;
}
}
obj* _init_l_Lean_closureMaxArgs() {
_start:
{
obj* x_0; obj* x_1;
x_0 = lean::box(0);
x_1 = lean_closure_max_args(x_0);
return x_1;
}
}
obj* initialize_init_core(obj*);
static bool _G_initialized = false;
obj* initialize_init_lean_runtime(obj* w) {
if (_G_initialized) return w;
_G_initialized = true;
if (io_result_is_error(w)) return w;
w = initialize_init_core(w);
if (io_result_is_error(w)) return w;
l_Lean_closureMaxArgs = _init_l_Lean_closureMaxArgs();
lean::mark_persistent(l_Lean_closureMaxArgs);
return w;
}