From db325cb924dd3c4b3ef0558dbdb0e235fdd1ceb0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 20 Jun 2019 09:23:41 -0700 Subject: [PATCH] fix(stag0): missing file --- src/stage0/init/lean/toexpr.cpp | 209 ++++++++++++++++++++++++++++++++ 1 file changed, 209 insertions(+) create mode 100644 src/stage0/init/lean/toexpr.cpp diff --git a/src/stage0/init/lean/toexpr.cpp b/src/stage0/init/lean/toexpr.cpp new file mode 100644 index 0000000000..7dffdd5e94 --- /dev/null +++ b/src/stage0/init/lean/toexpr.cpp @@ -0,0 +1,209 @@ +// Lean compiler output +// Module: init.lean.toexpr +// Imports: init.lean.expr +#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 +obj* l_Lean_strToExpr(obj*); +obj* l_Lean_nameToExprAux___main___closed__3; +obj* l_Lean_nameToExprAux___main___closed__1; +obj* l_id___rarg___boxed(obj*); +extern "C" obj* lean_expr_mk_const(obj*, obj*); +obj* l_Lean_mkBinCApp(obj*, obj*, obj*); +extern "C" obj* lean_name_mk_string(obj*, obj*); +obj* l_Lean_nameToExprAux___main(obj*); +obj* l_Lean_nameToExprAux(obj*); +obj* l_Lean_nameToExprAux___main___closed__5; +obj* l_Lean_nameToExprAux___main___closed__4; +obj* l_Lean_exprToExpr; +obj* l_Lean_nameToExpr; +obj* l_Lean_natToExpr(obj*); +obj* l_Lean_nameToExprAux___main___closed__2; +extern "C" obj* lean_expr_mk_lit(obj*); +obj* _init_l_Lean_exprToExpr() { +_start: +{ +obj* x_1; +x_1 = lean::alloc_closure(reinterpret_cast(l_id___rarg___boxed), 1, 0); +return x_1; +} +} +obj* l_Lean_natToExpr(obj* x_1) { +_start: +{ +obj* x_2; obj* x_3; +x_2 = lean::alloc_cnstr(0, 1, 0); +lean::cnstr_set(x_2, 0, x_1); +x_3 = lean_expr_mk_lit(x_2); +return x_3; +} +} +obj* l_Lean_strToExpr(obj* x_1) { +_start: +{ +obj* x_2; obj* x_3; +x_2 = lean::alloc_cnstr(1, 1, 0); +lean::cnstr_set(x_2, 0, x_1); +x_3 = lean_expr_mk_lit(x_2); +return x_3; +} +} +obj* _init_l_Lean_nameToExprAux___main___closed__1() { +_start: +{ +obj* x_1; +x_1 = lean::mk_string("Lean"); +return x_1; +} +} +obj* _init_l_Lean_nameToExprAux___main___closed__2() { +_start: +{ +obj* x_1; +x_1 = lean::mk_string("Name"); +return x_1; +} +} +obj* _init_l_Lean_nameToExprAux___main___closed__3() { +_start: +{ +obj* x_1; +x_1 = lean::mk_string("anonymous"); +return x_1; +} +} +obj* _init_l_Lean_nameToExprAux___main___closed__4() { +_start: +{ +obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; +x_1 = lean::box(0); +x_2 = lean::mk_string("Lean"); +x_3 = lean_name_mk_string(x_1, x_2); +x_4 = lean::mk_string("Name"); +x_5 = lean_name_mk_string(x_3, x_4); +x_6 = lean::mk_string("mkString"); +x_7 = lean_name_mk_string(x_5, x_6); +return x_7; +} +} +obj* _init_l_Lean_nameToExprAux___main___closed__5() { +_start: +{ +obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; +x_1 = lean::box(0); +x_2 = lean::mk_string("Lean"); +x_3 = lean_name_mk_string(x_1, x_2); +x_4 = lean::mk_string("Name"); +x_5 = lean_name_mk_string(x_3, x_4); +x_6 = lean::mk_string("mkNumeral"); +x_7 = lean_name_mk_string(x_5, x_6); +return x_7; +} +} +obj* l_Lean_nameToExprAux___main(obj* x_1) { +_start: +{ +switch (lean::obj_tag(x_1)) { +case 0: +{ +obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; +x_2 = l_Lean_nameToExprAux___main___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +x_4 = l_Lean_nameToExprAux___main___closed__2; +x_5 = lean_name_mk_string(x_3, x_4); +x_6 = l_Lean_nameToExprAux___main___closed__3; +x_7 = lean_name_mk_string(x_5, x_6); +x_8 = lean::box(0); +x_9 = lean_expr_mk_const(x_7, x_8); +return x_9; +} +case 1: +{ +obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; +x_10 = lean::cnstr_get(x_1, 0); +lean::inc(x_10); +x_11 = lean::cnstr_get(x_1, 1); +lean::inc(x_11); +lean::dec(x_1); +x_12 = l_Lean_nameToExprAux___main(x_10); +x_13 = lean::alloc_cnstr(1, 1, 0); +lean::cnstr_set(x_13, 0, x_11); +x_14 = lean_expr_mk_lit(x_13); +x_15 = l_Lean_nameToExprAux___main___closed__4; +x_16 = l_Lean_mkBinCApp(x_15, x_12, x_14); +return x_16; +} +default: +{ +obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; +x_17 = lean::cnstr_get(x_1, 0); +lean::inc(x_17); +x_18 = lean::cnstr_get(x_1, 1); +lean::inc(x_18); +lean::dec(x_1); +x_19 = l_Lean_nameToExprAux___main(x_17); +x_20 = lean::alloc_cnstr(0, 1, 0); +lean::cnstr_set(x_20, 0, x_18); +x_21 = lean_expr_mk_lit(x_20); +x_22 = l_Lean_nameToExprAux___main___closed__5; +x_23 = l_Lean_mkBinCApp(x_22, x_19, x_21); +return x_23; +} +} +} +} +obj* l_Lean_nameToExprAux(obj* x_1) { +_start: +{ +obj* x_2; +x_2 = l_Lean_nameToExprAux___main(x_1); +return x_2; +} +} +obj* _init_l_Lean_nameToExpr() { +_start: +{ +obj* x_1; +x_1 = lean::alloc_closure(reinterpret_cast(l_Lean_nameToExprAux), 1, 0); +return x_1; +} +} +obj* initialize_init_lean_expr(obj*); +static bool _G_initialized = false; +obj* initialize_init_lean_toexpr(obj* w) { +if (_G_initialized) return w; +_G_initialized = true; +if (io_result_is_error(w)) return w; +w = initialize_init_lean_expr(w); +if (io_result_is_error(w)) return w; +l_Lean_exprToExpr = _init_l_Lean_exprToExpr(); +lean::mark_persistent(l_Lean_exprToExpr); +lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "exprToExpr"), l_Lean_exprToExpr); +REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "natToExpr"), 1, l_Lean_natToExpr); +REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "strToExpr"), 1, l_Lean_strToExpr); +l_Lean_nameToExprAux___main___closed__1 = _init_l_Lean_nameToExprAux___main___closed__1(); +lean::mark_persistent(l_Lean_nameToExprAux___main___closed__1); +l_Lean_nameToExprAux___main___closed__2 = _init_l_Lean_nameToExprAux___main___closed__2(); +lean::mark_persistent(l_Lean_nameToExprAux___main___closed__2); +l_Lean_nameToExprAux___main___closed__3 = _init_l_Lean_nameToExprAux___main___closed__3(); +lean::mark_persistent(l_Lean_nameToExprAux___main___closed__3); +l_Lean_nameToExprAux___main___closed__4 = _init_l_Lean_nameToExprAux___main___closed__4(); +lean::mark_persistent(l_Lean_nameToExprAux___main___closed__4); +l_Lean_nameToExprAux___main___closed__5 = _init_l_Lean_nameToExprAux___main___closed__5(); +lean::mark_persistent(l_Lean_nameToExprAux___main___closed__5); +REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "nameToExprAux"), 1, l_Lean_nameToExprAux); +l_Lean_nameToExpr = _init_l_Lean_nameToExpr(); +lean::mark_persistent(l_Lean_nameToExpr); +lean::register_constant(lean::mk_const_name(lean::mk_const_name("Lean"), "nameToExpr"), l_Lean_nameToExpr); +return w; +}