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:
Leonardo de Moura 2020-04-03 16:51:39 -07:00
parent b5f258773b
commit c6d77423d1
16 changed files with 838 additions and 186 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Init/Data.lean
View file

@ -14,6 +14,7 @@ import Init.Data.Array
import Init.Data.ByteArray
import Init.Data.Fin
import Init.Data.UInt
import Init.Data.Float
import Init.Data.RBTree
import Init.Data.RBMap
import Init.Data.Option

58
stage0/src/Init/Data/Float.lean Normal file
View file

@ -0,0 +1,58 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Core
import Init.Data.ToString
structure FloatSpec :=
(float : Type)
(val : float)
(lt : float → float → Prop)
(le : float → float → Prop)
(decEq : DecidableEq float)
(decLt : DecidableRel lt)
(decLe : DecidableRel le)
-- Just show FloatSpec is inhabited.
constant floatSpec : FloatSpec := {
float := Unit,
val := (),
lt := fun _ _ => True,
le := fun _ _ => True,
decEq := inferInstanceAs (DecidableEq Unit),
decLt := fun _ _ => inferInstanceAs (Decidable True),
decLe := fun _ _ => inferInstanceAs (Decidable True)
}
def Float : Type := floatSpec.float
instance : Inhabited Float := ⟨floatSpec.val⟩
/- @[extern "lean_float_of_nat"] -/ constant Float.ofNat : (@& Nat) → Float := arbitrary _
/- @[extern c inline "#1 + #2"] -/ constant Float.add : Float → Float → Float := arbitrary _
/- @[extern c inline "#1 - #2"] -/ constant Float.sub : Float → Float → Float := arbitrary _
/- @[extern c inline "#1 * #2"] -/ constant Float.mul : Float → Float → Float := arbitrary _
/- @[extern c inline "#1 / #2"] -/ constant Float.div : Float → Float → Float := arbitrary _
def Float.lt : Float → Float → Prop := floatSpec.lt
def Float.le : Float → Float → Prop := floatSpec.le
instance : HasZero Float := ⟨Float.ofNat 0⟩
instance : HasOne Float := ⟨Float.ofNat 1⟩
instance : HasOfNat Float := ⟨Float.ofNat⟩
instance : HasAdd Float := ⟨Float.add⟩
instance : HasSub Float := ⟨Float.sub⟩
instance : HasMul Float := ⟨Float.mul⟩
instance : HasDiv Float := ⟨Float.div⟩
instance : HasLess Float := ⟨Float.lt⟩
instance : HasLessEq Float := ⟨Float.le⟩
/- @[extern c inline "#1 == #2"] -/ constant Float.decEq (a b : Float) : Decidable (a = b) := floatSpec.decEq a b
/- @[extern c inline "#1 < #2"] -/ constant Float.decLt (a b : Float) : Decidable (a < b) := floatSpec.decLt a b
/- @[extern c inline "#1 <= #2"] -/ constant Float.decLe (a b : Float) : Decidable (a ≤ b) := floatSpec.decLe a b
/- @[extern "lean_float_to_string"] -/ constant Float.toString : Float → String := arbitrary _
instance : HasToString Float := ⟨Float.toString⟩

8
stage0/src/Init/Lean/Compiler/IR/EmitC.lean
View file

@ -311,7 +311,7 @@ emit "lean_ctor_set_usize("; emit x; emit ", "; emit n; emit ", "; emit y; emitL
def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit := do
match t with
| IRType.float => throw "floats are not supported yet"
| IRType.float => emit "lean_ctor_set_float"
| IRType.uint8 => emit "lean_ctor_set_uint8"
| IRType.uint16 => emit "lean_ctor_set_uint16"
| IRType.uint32 => emit "lean_ctor_set_uint32"
@ -386,7 +386,7 @@ emitLhs z; emit "lean_ctor_get_usize("; emit x; emit ", "; emit i; emitLn ");"
def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit := do
emitLhs z;
match t with
| IRType.float => throw "floats are not supported yet"
| IRType.float => emit "lean_ctor_get_float"
| IRType.uint8 => emit "lean_ctor_get_uint8"
| IRType.uint16 => emit "lean_ctor_get_uint16"
| IRType.uint32 => emit "lean_ctor_get_uint32"
@ -447,7 +447,7 @@ match xType with
| IRType.usize => emit "lean_box_usize"
| IRType.uint32 => emit "lean_box_uint32"
| IRType.uint64 => emit "lean_box_uint64"
| IRType.float => throw "floats are not supported yet"
| IRType.float => emit "lean_box_float"
| other => emit "lean_box"
def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do
@ -459,7 +459,7 @@ match t with
| IRType.usize => emit "lean_unbox_usize"
| IRType.uint32 => emit "lean_unbox_uint32"
| IRType.uint64 => emit "lean_unbox_uint64"
| IRType.float => throw "floats are not supported yet"
| IRType.float => emit "lean_unbox_float"
| other => emit "lean_unbox";
emit "("; emit x; emitLn ");"

26
stage0/src/library/compiler/ir.cpp
View file

@ -117,8 +117,10 @@ static ir::type to_ir_type(expr const & e) {
return ir::type::UInt64;
} else if (const_name(e) == get_usize_name()) {
return ir::type::USize;
} else if (const_name(e) == get_float_name()) {
return ir::type::Float;
}
} else if (is_pi(e)) {
} else if (is_pi(e)) {
return ir::type::Object;
}
throw exception("IR unsupported type");
@ -334,6 +336,16 @@ class to_ir_fn {
return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), size_to_ir_type(sz), b);
}
ir::fn_body visit_fset(local_decl const & decl, ir::fn_body const & b) {
expr val = *decl.get_value();
buffer<expr> args;
expr const & fn = get_app_args(val, args);
lean_assert(args.size() == 2);
unsigned n, offset;
lean_verify(is_llnf_fset(fn, n, offset));
return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float, b);
}
ir::fn_body visit_uset(local_decl const & decl, ir::fn_body const & b) {
expr val = *decl.get_value();
buffer<expr> args;
@ -360,6 +372,14 @@ class to_ir_fn {
return mk_vdecl(decl, v, b);
}
ir::fn_body visit_fproj(local_decl const & decl, ir::fn_body const & b) {
expr val = *decl.get_value();
unsigned n, offset;
lean_verify(is_llnf_fproj(get_app_fn(val), n, offset));
ir::expr v = ir::mk_sproj(n, offset, to_var_id(app_arg(val)));
return mk_vdecl(decl, v, b);
}
ir::fn_body visit_uproj(local_decl const & decl, ir::fn_body const & b) {
expr val = *decl.get_value();
unsigned n;
@ -391,12 +411,16 @@ class to_ir_fn {
return visit_papp(decl, b);
else if (is_llnf_sset(fn))
return visit_sset(decl, b);
else if (is_llnf_fset(fn))
return visit_fset(decl, b);
else if (is_llnf_uset(fn))
return visit_uset(decl, b);
else if (is_llnf_proj(fn))
return visit_proj(decl, b);
else if (is_llnf_sproj(fn))
return visit_sproj(decl, b);
else if (is_llnf_fproj(fn))
return visit_fproj(decl, b);
else if (is_llnf_uproj(fn))
return visit_uproj(decl, b);
else if (is_constant(fn))

54
stage0/src/library/compiler/llnf.cpp
View file

@ -32,10 +32,12 @@ static expr * g_closure = nullptr;
static char const * g_cnstr = "_cnstr";
static name * g_reuse = nullptr;
static name * g_reset = nullptr;
static name * g_fset = nullptr;
static name * g_sset = nullptr;
static name * g_uset = nullptr;
static name * g_proj = nullptr;
static name * g_sproj = nullptr;
static name * g_fproj = nullptr;
static name * g_uproj = nullptr;
static expr * g_jmp = nullptr;
static name * g_box = nullptr;
@ -57,6 +59,17 @@ static bool is_llnf_unary_primitive(expr const & e, name const & prefix, unsigne
return true;
}
static bool is_llnf_binary_primitive(expr const & e, name const & prefix, unsigned & i1, unsigned & i2) {
if (!is_constant(e)) return false;
name const & n2 = const_name(e);
if (n2.is_atomic() || !n2.is_numeral()) return false;
i2 = n2.get_numeral().get_small_value();
name const & n1 = n2.get_prefix();
if (n1.is_atomic() || !n1.is_numeral() || n1.get_prefix() != prefix) return false;
i1 = n1.get_numeral().get_small_value();
return true;
}
static bool is_llnf_ternary_primitive(expr const & e, name const & prefix, unsigned & i1, unsigned & i2, unsigned & i3) {
if (!is_constant(e)) return false;
name const & n3 = const_name(e);
@ -145,6 +158,9 @@ bool is_llnf_reset(expr const & e, unsigned & n) { return is_llnf_unary_primitiv
expr mk_llnf_sset(unsigned sz, unsigned n, unsigned offset) { return mk_constant(name(name(name(*g_sset, sz), n), offset)); }
bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset) { return is_llnf_ternary_primitive(e, *g_sset, sz, n, offset); }
expr mk_llnf_fset(unsigned n, unsigned offset) { return mk_constant(name(name(*g_fset, n), offset)); }
bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fset, n, offset); }
/* The `_uset.<n>` instruction sets a `usize` value in a constructor object at offset `sizeof(void*)*n`. */
expr mk_llnf_uset(unsigned n) { return mk_constant(name(*g_uset, n)); }
bool is_llnf_uset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_uset, n); }
@ -157,6 +173,9 @@ bool is_llnf_proj(expr const & e, unsigned & idx) { return is_llnf_unary_primiti
expr mk_llnf_sproj(unsigned sz, unsigned n, unsigned offset) { return mk_constant(name(name(name(*g_sproj, sz), n), offset)); }
bool is_llnf_sproj(expr const & e, unsigned & sz, unsigned & n, unsigned & offset) { return is_llnf_ternary_primitive(e, *g_sproj, sz, n, offset); }
expr mk_llnf_fproj(unsigned n, unsigned offset) { return mk_constant(name(name(*g_sproj, n), offset)); }
bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fproj, n, offset); }
/* The `_uproj.<idx>` instruction retrieves an `usize` field in a constructor object at offset `sizeof(void*)*idx` */
expr mk_llnf_uproj(unsigned idx) { return mk_constant(name(*g_uproj, idx)); }
bool is_llnf_uproj(expr const & e, unsigned & idx) { return is_llnf_unary_primitive(e, *g_uproj, idx); }
@ -197,9 +216,11 @@ bool is_llnf_op(expr const & e) {
is_llnf_reuse(e) ||
is_llnf_reset(e) ||
is_llnf_sset(e) ||
is_llnf_fset(e) ||
is_llnf_uset(e) ||
is_llnf_proj(e) ||
is_llnf_sproj(e) ||
is_llnf_fproj(e) ||
is_llnf_uproj(e) ||
is_llnf_jmp(e) ||
is_llnf_box(e) ||
@ -482,6 +503,10 @@ class to_lambda_pure_fn {
return mk_app(mk_llnf_sproj(size, num, offset), major);
}
expr mk_fproj(expr const & major, unsigned num, unsigned offset) {
return mk_app(mk_llnf_fproj(num, offset), major);
}
expr mk_uproj(expr const & major, unsigned idx) {
return mk_app(mk_llnf_uproj(idx), major);
}
@ -490,6 +515,10 @@ class to_lambda_pure_fn {
return mk_app(mk_llnf_sset(size, num, offset), major, v);
}
expr mk_fset(expr const & major, unsigned num, unsigned offset, expr const & v) {
return mk_app(mk_llnf_fset(num, offset), major, v);
}
expr mk_uset(expr const & major, unsigned idx, expr const & v) {
return mk_app(mk_llnf_uset(idx), major, v);
}
@ -551,7 +580,11 @@ class to_lambda_pure_fn {
fields.push_back(mk_let_decl(info.get_type(), mk_uproj(major, info.m_idx)));
break;
case field_info::Scalar:
fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
if (info.is_float()) {
fields.push_back(mk_let_decl(info.get_type(), mk_fproj(major, info.m_idx, info.m_offset)));
} else {
fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
}
break;
}
minor = binding_body(minor);
@ -644,7 +677,11 @@ class to_lambda_pure_fn {
if (first) {
r = mk_let_decl(mk_enf_object_type(), r);
}
r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
if (info.is_float()) {
r = mk_let_decl(mk_enf_object_type(), mk_fset(r, info.m_idx, info.m_offset, args[j]));
} else {
r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
}
first = false;
break;
case field_info::USize:
@ -686,8 +723,13 @@ class to_lambda_pure_fn {
return mk_app(mk_llnf_uproj(info.m_idx), visit(proj_expr(e)));
break;
case field_info::Scalar:
if (proj_idx(e) == i)
return mk_sproj(visit(proj_expr(e)), info.m_size, info.m_idx, info.m_offset);
if (proj_idx(e) == i) {
if (info.is_float()) {
return mk_fproj(visit(proj_expr(e)), info.m_idx, info.m_offset);
} else {
return mk_sproj(visit(proj_expr(e)), info.m_size, info.m_idx, info.m_offset);
}
}
break;
}
i++;
@ -778,9 +820,11 @@ void initialize_llnf() {
g_reuse = new name("_reuse");
g_reset = new name("_reset");
g_sset = new name("_sset");
g_fset = new name("_fset");
g_uset = new name("_uset");
g_proj = new name("_proj");
g_sproj = new name("_sproj");
g_fproj = new name("_sproj");
g_uproj = new name("_uproj");
g_jmp = new expr(mk_constant("_jmp"));
g_box = new name("_box");
@ -796,8 +840,10 @@ void finalize_llnf() {
delete g_reuse;
delete g_reset;
delete g_sset;
delete g_fset;
delete g_proj;
delete g_sproj;
delete g_fproj;
delete g_uset;
delete g_uproj;
delete g_jmp;

5
stage0/src/library/compiler/llnf.h
View file

@ -22,8 +22,10 @@ bool is_llnf_reuse(expr const & e, unsigned & cidx, unsigned & nusize, unsigned
bool is_llnf_reset(expr const & e, unsigned & n);
bool is_llnf_proj(expr const & e, unsigned & idx);
bool is_llnf_sproj(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset);
bool is_llnf_uproj(expr const & e, unsigned & idx);
bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset);
bool is_llnf_uset(expr const & e, unsigned & n);
bool is_llnf_jmp(expr const & e);
bool is_llnf_unbox(expr const & e, unsigned & n);
@ -37,8 +39,10 @@ inline bool is_llnf_reuse(expr const & e) { unsigned d1, d2, d3; bool u; return
inline bool is_llnf_reset(expr const & e) { unsigned i; return is_llnf_reset(e, i); }
inline bool is_llnf_proj(expr const & e) { unsigned d; return is_llnf_proj(e, d); }
inline bool is_llnf_sproj(expr const & e) { unsigned d1, d2, d3; return is_llnf_sproj(e, d1, d2, d3); }
inline bool is_llnf_fproj(expr const & e) { unsigned d1, d2; return is_llnf_fproj(e, d1, d2); }
inline bool is_llnf_uproj(expr const & e) { unsigned d; return is_llnf_uproj(e, d); }
inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_sset(e, d1, d2, d3); }
inline bool is_llnf_fset(expr const & e) { unsigned d1, d2; return is_llnf_fset(e, d1, d2); }
inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
inline bool is_llnf_unbox(expr const & e) { unsigned n; return is_llnf_unbox(e, n); }
@ -61,6 +65,7 @@ struct field_info {
field_info(unsigned sz, unsigned num, unsigned offset, expr const & type):
m_kind(Scalar), m_size(sz), m_idx(num), m_offset(offset), m_type(type) {}
expr get_type() const { return m_type; }
bool is_float() const { return is_constant(m_type, get_float_name()); }
static field_info mk_irrelevant() { return field_info(); }
static field_info mk_object(unsigned idx) { return field_info(idx); }
static field_info mk_usize() { return field_info(0, true); }

5
stage0/src/library/compiler/util.cpp
View file

@ -370,6 +370,7 @@ bool is_runtime_builtin_type(name const & n) {
n == get_uint32_name() ||
n == get_uint64_name() ||
n == get_usize_name() ||
n == get_float_name() ||
n == get_thunk_name() ||
n == get_task_name() ||
n == get_array_name() ||
@ -385,7 +386,8 @@ bool is_runtime_scalar_type(name const & n) {
n == get_uint16_name() ||
n == get_uint32_name() ||
n == get_uint64_name() ||
n == get_usize_name();
n == get_usize_name() ||
n == get_float_name();
}
bool is_llnf_unboxed_type(expr const & type) {
@ -758,6 +760,7 @@ void initialize_compiler_util() {
g_builtin_scalar_size->emplace_back(get_uint16_name(), 2);
g_builtin_scalar_size->emplace_back(get_uint32_name(), 4);
g_builtin_scalar_size->emplace_back(get_uint64_name(), 8);
g_builtin_scalar_size->emplace_back(get_float_name(), 8);
}
void finalize_compiler_util() {

4
stage0/src/library/constants.cpp
View file

@ -57,6 +57,7 @@ name const * g_eq_of_heq = nullptr;
name const * g_eq_true_intro = nullptr;
name const * g_eq_false_intro = nullptr;
name const * g_eq_self_iff_true = nullptr;
name const * g_float = nullptr;
name const * g_lean_message_data = nullptr;
name const * g_lean_monad_tracer_trace = nullptr;
name const * g_false = nullptr;
@ -247,6 +248,7 @@ void initialize_constants() {
g_eq_true_intro = new name{"eqTrueIntro"};
g_eq_false_intro = new name{"eqFalseIntro"};
g_eq_self_iff_true = new name{"eqSelfIffTrue"};
g_float = new name{"Float"};
g_lean_message_data = new name{"Lean", "MessageData"};
g_lean_monad_tracer_trace = new name{"Lean", "MonadTracer", "trace"};
g_false = new name{"False"};
@ -438,6 +440,7 @@ void finalize_constants() {
delete g_eq_true_intro;
delete g_eq_false_intro;
delete g_eq_self_iff_true;
delete g_float;
delete g_lean_message_data;
delete g_lean_monad_tracer_trace;
delete g_false;
@ -628,6 +631,7 @@ name const & get_eq_of_heq_name() { return *g_eq_of_heq; }
name const & get_eq_true_intro_name() { return *g_eq_true_intro; }
name const & get_eq_false_intro_name() { return *g_eq_false_intro; }
name const & get_eq_self_iff_true_name() { return *g_eq_self_iff_true; }
name const & get_float_name() { return *g_float; }
name const & get_lean_message_data_name() { return *g_lean_message_data; }
name const & get_lean_monad_tracer_trace_name() { return *g_lean_monad_tracer_trace; }
name const & get_false_name() { return *g_false; }

1
stage0/src/library/constants.h
View file

@ -59,6 +59,7 @@ name const & get_eq_of_heq_name();
name const & get_eq_true_intro_name();
name const & get_eq_false_intro_name();
name const & get_eq_self_iff_true_name();
name const & get_float_name();
name const & get_lean_message_data_name();
name const & get_lean_monad_tracer_trace_name();
name const & get_false_name();

1
stage0/src/library/constants.txt
View file

@ -52,6 +52,7 @@ eqOfHEq
eqTrueIntro
eqFalseIntro
eqSelfIffTrue
Float
Lean.MessageData
Lean.MonadTracer.trace
False

25
stage0/src/runtime/lean.h
View file

@ -703,6 +703,11 @@ static inline uint64_t lean_ctor_get_uint64(b_lean_obj_arg o, unsigned offset) {
return *((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
}
static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) {
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
}
static inline void lean_ctor_set_usize(b_lean_obj_arg o, unsigned i, size_t v) {
assert(i >= lean_ctor_num_objs(o));
*((size_t*)(lean_ctor_obj_cptr(o) + i)) = v;
@ -728,6 +733,11 @@ static inline void lean_ctor_set_uint64(b_lean_obj_arg o, unsigned offset, uint6
*((uint64_t*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
}
static inline void lean_ctor_set_float(b_lean_obj_arg o, unsigned offset, double v) {
assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
*((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
}
/* Closures */
static inline void * lean_closure_fun(lean_object * o) { return lean_to_closure(o)->m_fun; }
@ -1612,6 +1622,11 @@ static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2;
static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; }
size_t lean_usize_mix_hash(size_t a1, size_t a2);
/* Float */
double lean_float_of_nat(b_lean_obj_arg a);
lean_obj_res lean_float_to_string(double a);
/* Boxing primitives */
static inline lean_obj_res lean_box_uint32(uint32_t v) {
@ -1656,6 +1671,16 @@ static inline size_t lean_unbox_usize(b_lean_obj_arg o) {
return lean_ctor_get_usize(o, 0);
}
static inline lean_obj_res lean_box_float(double v) {
lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(double));
lean_ctor_set_float(r, 0, v);
return r;
}
static inline uint64_t lean_unbox_float(b_lean_obj_arg o) {
return lean_ctor_get_float(o, 0);
}
/* Debugging helper functions */
lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);

17
stage0/src/runtime/object.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include <vector>
#include <deque>
#include <cmath>
#include "runtime/object.h"
#include "runtime/thread.h"
#include "runtime/utf8.h"
@ -1445,6 +1446,22 @@ extern "C" usize lean_usize_mix_hash(usize a1, usize a2) {
return hash(static_cast<uint32>(a1), static_cast<uint32>(a2));
}
// =======================================
// Float
extern "C" double lean_float_of_nat(b_lean_obj_arg a) {
if (lean_is_scalar(a)) {
return (double)lean_unbox(a);
} else {
return std::nan(""); // TODO(Leo): improve
}
}
lean_obj_res lean_float_to_string(double a) {
return mk_string(std::to_string(a));
}
// =======================================
// Strings

2
stage0/stdlib/CMakeLists.txt
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Init/Data.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.Fin Init.Data.UInt Init.Data.RBTree Init.Data.RBMap Init.Data.Option Init.Data.HashMap Init.Data.Random Init.Data.Queue Init.Data.Stack
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.RBTree Init.Data.RBMap Init.Data.Option Init.Data.HashMap Init.Data.Random Init.Data.Queue Init.Data.Stack
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -23,6 +23,7 @@ lean_object* initialize_Init_Data_Array(lean_object*);
lean_object* initialize_Init_Data_ByteArray(lean_object*);
lean_object* initialize_Init_Data_Fin(lean_object*);
lean_object* initialize_Init_Data_UInt(lean_object*);
lean_object* initialize_Init_Data_Float(lean_object*);
lean_object* initialize_Init_Data_RBTree(lean_object*);
lean_object* initialize_Init_Data_RBMap(lean_object*);
lean_object* initialize_Init_Data_Option(lean_object*);
@ -65,6 +66,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_UInt(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Float(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_RBTree(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

496
stage0/stdlib/Init/Data/Float.c Normal file
View file

@ -0,0 +1,496 @@
// Lean compiler output
// Module: Init.Data.Float
// Imports: Init.Core Init.Data.ToString
#include "runtime/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
uint8_t l_floatSpec___elambda__1(lean_object*, lean_object*);
lean_object* l_Float_ofNat(lean_object*);
lean_object* l_Float_HasDiv___closed__1;
lean_object* l_Float_HasLessEq;
lean_object* l_Float_HasOne;
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Float_div___boxed(lean_object*, lean_object*);
uint8_t l_Float_decEq(lean_object*, lean_object*);
lean_object* l_floatSpec___closed__1;
uint8_t l_Float_decLe(lean_object*, lean_object*);
lean_object* l_floatSpec___closed__2;
lean_object* l_Float_HasMul;
lean_object* l_Float_HasAdd;
lean_object* l_Float_Inhabited;
lean_object* l_Float_HasOfNat;
lean_object* l_Float_HasToString;
uint8_t l_Float_decLt(lean_object*, lean_object*);
uint8_t l_floatSpec___elambda__2(lean_object*, lean_object*);
lean_object* l_floatSpec___elambda__2___boxed(lean_object*, lean_object*);
extern uint8_t l_True_Decidable;
lean_object* l_Float_mul___boxed(lean_object*, lean_object*);
lean_object* l_Float_ofNat___boxed(lean_object*);
lean_object* l_Float_toString(lean_object*);
lean_object* l_Float_div(lean_object*, lean_object*);
lean_object* l_Float_HasOfNat___closed__1;
lean_object* l_Float_decLt___boxed(lean_object*, lean_object*);
lean_object* l_Float_sub(lean_object*, lean_object*);
lean_object* l_floatSpec___elambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Float_add(lean_object*, lean_object*);
lean_object* l_floatSpec___closed__3;
lean_object* l_Float_HasToString___closed__1;
lean_object* l_Float_HasSub;
lean_object* l_Float_HasSub___closed__1;
lean_object* l_Float_HasLess;
lean_object* l_Float_HasDiv;
lean_object* l_Float_decLe___boxed(lean_object*, lean_object*);
lean_object* l_Float_sub___boxed(lean_object*, lean_object*);
lean_object* l_floatSpec;
lean_object* l_Float_toString___boxed(lean_object*);
lean_object* l_Float_decEq___boxed(lean_object*, lean_object*);
lean_object* l_Float_HasAdd___closed__1;
lean_object* l_Float_HasZero;
lean_object* l_Float_HasMul___closed__1;
lean_object* l_Float_add___boxed(lean_object*, lean_object*);
lean_object* l_Float_mul(lean_object*, lean_object*);
uint8_t l_floatSpec___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_True_Decidable;
return x_3;
}
}
uint8_t l_floatSpec___elambda__2(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
}
lean_object* _init_l_floatSpec___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_floatSpec___elambda__2___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_floatSpec___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_floatSpec___elambda__1___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_floatSpec___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_floatSpec___closed__1;
x_3 = l_floatSpec___closed__2;
x_4 = lean_alloc_ctor(0, 4, 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);
lean_ctor_set(x_4, 3, x_3);
return x_4;
}
}
lean_object* _init_l_floatSpec() {
_start:
{
lean_object* x_1;
x_1 = l_floatSpec___closed__3;
return x_1;
}
}
lean_object* l_floatSpec___elambda__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_floatSpec___elambda__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_floatSpec___elambda__2___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_floatSpec___elambda__2(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* _init_l_Float_Inhabited() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
lean_object* l_Float_ofNat(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_box(0);
return x_2;
}
}
lean_object* l_Float_ofNat___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Float_ofNat(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Float_add(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
lean_object* l_Float_add___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Float_add(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Float_sub(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
lean_object* l_Float_sub___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Float_sub(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Float_mul(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
lean_object* l_Float_mul___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Float_mul(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Float_div(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
lean_object* l_Float_div___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Float_div(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* _init_l_Float_HasZero() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
lean_object* _init_l_Float_HasOne() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
lean_object* _init_l_Float_HasOfNat___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Float_ofNat___boxed), 1, 0);
return x_1;
}
}
lean_object* _init_l_Float_HasOfNat() {
_start:
{
lean_object* x_1;
x_1 = l_Float_HasOfNat___closed__1;
return x_1;
}
}
lean_object* _init_l_Float_HasAdd___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Float_add___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Float_HasAdd() {
_start:
{
lean_object* x_1;
x_1 = l_Float_HasAdd___closed__1;
return x_1;
}
}
lean_object* _init_l_Float_HasSub___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Float_sub___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Float_HasSub() {
_start:
{
lean_object* x_1;
x_1 = l_Float_HasSub___closed__1;
return x_1;
}
}
lean_object* _init_l_Float_HasMul___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Float_mul___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Float_HasMul() {
_start:
{
lean_object* x_1;
x_1 = l_Float_HasMul___closed__1;
return x_1;
}
}
lean_object* _init_l_Float_HasDiv___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Float_div___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Float_HasDiv() {
_start:
{
lean_object* x_1;
x_1 = l_Float_HasDiv___closed__1;
return x_1;
}
}
lean_object* _init_l_Float_HasLess() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
lean_object* _init_l_Float_HasLessEq() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
uint8_t l_Float_decEq(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
}
lean_object* l_Float_decEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Float_decEq(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Float_decLt(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_True_Decidable;
return x_3;
}
}
lean_object* l_Float_decLt___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Float_decLt(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_Float_decLe(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_True_Decidable;
return x_3;
}
}
lean_object* l_Float_decLe___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Float_decLe(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Float_toString(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_String_splitAux___main___closed__1;
return x_2;
}
}
lean_object* l_Float_toString___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Float_toString(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Float_HasToString___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Float_toString___boxed), 1, 0);
return x_1;
}
}
lean_object* _init_l_Float_HasToString() {
_start:
{
lean_object* x_1;
x_1 = l_Float_HasToString___closed__1;
return x_1;
}
}
lean_object* initialize_Init_Core(lean_object*);
lean_object* initialize_Init_Data_ToString(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Data_Float(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Core(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_ToString(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_floatSpec___closed__1 = _init_l_floatSpec___closed__1();
lean_mark_persistent(l_floatSpec___closed__1);
l_floatSpec___closed__2 = _init_l_floatSpec___closed__2();
lean_mark_persistent(l_floatSpec___closed__2);
l_floatSpec___closed__3 = _init_l_floatSpec___closed__3();
lean_mark_persistent(l_floatSpec___closed__3);
l_floatSpec = _init_l_floatSpec();
lean_mark_persistent(l_floatSpec);
l_Float_Inhabited = _init_l_Float_Inhabited();
lean_mark_persistent(l_Float_Inhabited);
l_Float_HasZero = _init_l_Float_HasZero();
lean_mark_persistent(l_Float_HasZero);
l_Float_HasOne = _init_l_Float_HasOne();
lean_mark_persistent(l_Float_HasOne);
l_Float_HasOfNat___closed__1 = _init_l_Float_HasOfNat___closed__1();
lean_mark_persistent(l_Float_HasOfNat___closed__1);
l_Float_HasOfNat = _init_l_Float_HasOfNat();
lean_mark_persistent(l_Float_HasOfNat);
l_Float_HasAdd___closed__1 = _init_l_Float_HasAdd___closed__1();
lean_mark_persistent(l_Float_HasAdd___closed__1);
l_Float_HasAdd = _init_l_Float_HasAdd();
lean_mark_persistent(l_Float_HasAdd);
l_Float_HasSub___closed__1 = _init_l_Float_HasSub___closed__1();
lean_mark_persistent(l_Float_HasSub___closed__1);
l_Float_HasSub = _init_l_Float_HasSub();
lean_mark_persistent(l_Float_HasSub);
l_Float_HasMul___closed__1 = _init_l_Float_HasMul___closed__1();
lean_mark_persistent(l_Float_HasMul___closed__1);
l_Float_HasMul = _init_l_Float_HasMul();
lean_mark_persistent(l_Float_HasMul);
l_Float_HasDiv___closed__1 = _init_l_Float_HasDiv___closed__1();
lean_mark_persistent(l_Float_HasDiv___closed__1);
l_Float_HasDiv = _init_l_Float_HasDiv();
lean_mark_persistent(l_Float_HasDiv);
l_Float_HasLess = _init_l_Float_HasLess();
lean_mark_persistent(l_Float_HasLess);
l_Float_HasLessEq = _init_l_Float_HasLessEq();
lean_mark_persistent(l_Float_HasLessEq);
l_Float_HasToString___closed__1 = _init_l_Float_HasToString___closed__1();
lean_mark_persistent(l_Float_HasToString___closed__1);
l_Float_HasToString = _init_l_Float_HasToString();
lean_mark_persistent(l_Float_HasToString);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

315
stage0/stdlib/Init/Lean/Compiler/IR/EmitC.c
View file

@ -232,6 +232,7 @@ lean_object* l_Lean_IR_EmitC_hasMainFn(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitOffset___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitFnDeclAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_IR_FnBody_isTerminal(lean_object*);
lean_object* l_Lean_IR_EmitC_emitUnbox___closed__5;
lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__23;
lean_object* l_Lean_IR_EmitC_emitIf___closed__2;
lean_object* l_Lean_IR_EmitC_emitArgs(lean_object*, lean_object*, lean_object*);
@ -374,6 +375,7 @@ lean_object* l_Lean_IR_EmitC_emitMainFn___closed__37;
lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitTailCall___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitSetTag___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitMainFnIfNeeded___boxed(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitSProj___closed__5;
lean_object* l_Lean_IR_EmitC_toCType___closed__11;
lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__3;
lean_object* l_Lean_IR_EmitC_emitReuse(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
@ -542,6 +544,7 @@ lean_object* l_Lean_IR_EmitC_emitFileHeader___closed__20;
lean_object* l_Lean_IR_EmitC_getEnv(lean_object*, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_IR_EmitC_declareParams___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_getJPParams(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitBoxFn___closed__5;
lean_object* l_Lean_IR_EmitC_emitMainFn___closed__16;
lean_object* l_Lean_IR_EmitC_emitPartialApp___closed__1;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -5624,7 +5627,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSSet___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("floats are not supported yet");
x_1 = lean_mk_string("lean_ctor_set_float");
return x_1;
}
}
@ -5676,15 +5679,10 @@ switch (lean_obj_tag(x_5)) {
case 0:
{
lean_object* x_42; lean_object* x_43;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_42 = l_Lean_IR_EmitC_emitSSet___closed__1;
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_7);
return x_43;
x_43 = lean_string_append(x_7, x_42);
x_8 = x_43;
goto block_41;
}
case 1:
{
@ -7095,7 +7093,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_ctor_get_uint8");
x_1 = lean_mk_string("lean_ctor_get_float");
return x_1;
}
}
@ -7103,7 +7101,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_ctor_get_uint16");
x_1 = lean_mk_string("lean_ctor_get_uint8");
return x_1;
}
}
@ -7111,7 +7109,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_ctor_get_uint32");
x_1 = lean_mk_string("lean_ctor_get_uint16");
return x_1;
}
}
@ -7119,6 +7117,14 @@ lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_ctor_get_uint32");
return x_1;
}
}
lean_object* _init_l_Lean_IR_EmitC_emitSProj___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_ctor_get_uint64");
return x_1;
}
@ -7131,106 +7137,87 @@ x_34 = l_Lean_IR_EmitC_emitLhs(x_1, x_6, x_7);
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_35;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_35 = !lean_is_exclusive(x_34);
if (x_35 == 0)
{
lean_object* x_36; lean_object* x_37;
x_36 = lean_ctor_get(x_34, 0);
lean_dec(x_36);
x_37 = l_Lean_IR_EmitC_emitSSet___closed__1;
lean_ctor_set_tag(x_34, 1);
lean_ctor_set(x_34, 0, x_37);
return x_34;
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_34, 1);
lean_inc(x_35);
lean_dec(x_34);
x_36 = l_Lean_IR_EmitC_emitSProj___closed__1;
x_37 = lean_string_append(x_35, x_36);
x_8 = x_37;
goto block_33;
}
else
case 1:
{
lean_object* x_38; lean_object* x_39; lean_object* x_40;
x_38 = lean_ctor_get(x_34, 1);
lean_inc(x_38);
lean_dec(x_34);
x_39 = l_Lean_IR_EmitC_emitSSet___closed__1;
x_40 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
return x_40;
x_39 = l_Lean_IR_EmitC_emitSProj___closed__2;
x_40 = lean_string_append(x_38, x_39);
x_8 = x_40;
goto block_33;
}
}
case 1:
case 2:
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_34, 1);
lean_inc(x_41);
lean_dec(x_34);
x_42 = l_Lean_IR_EmitC_emitSProj___closed__1;
x_42 = l_Lean_IR_EmitC_emitSProj___closed__3;
x_43 = lean_string_append(x_41, x_42);
x_8 = x_43;
goto block_33;
}
case 2:
case 3:
{
lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_44 = lean_ctor_get(x_34, 1);
lean_inc(x_44);
lean_dec(x_34);
x_45 = l_Lean_IR_EmitC_emitSProj___closed__2;
x_45 = l_Lean_IR_EmitC_emitSProj___closed__4;
x_46 = lean_string_append(x_44, x_45);
x_8 = x_46;
goto block_33;
}
case 3:
case 4:
{
lean_object* x_47; lean_object* x_48; lean_object* x_49;
x_47 = lean_ctor_get(x_34, 1);
lean_inc(x_47);
lean_dec(x_34);
x_48 = l_Lean_IR_EmitC_emitSProj___closed__3;
x_48 = l_Lean_IR_EmitC_emitSProj___closed__5;
x_49 = lean_string_append(x_47, x_48);
x_8 = x_49;
goto block_33;
}
case 4:
{
lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_50 = lean_ctor_get(x_34, 1);
lean_inc(x_50);
lean_dec(x_34);
x_51 = l_Lean_IR_EmitC_emitSProj___closed__4;
x_52 = lean_string_append(x_50, x_51);
x_8 = x_52;
goto block_33;
}
default:
{
uint8_t x_53;
uint8_t x_50;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_53 = !lean_is_exclusive(x_34);
if (x_53 == 0)
x_50 = !lean_is_exclusive(x_34);
if (x_50 == 0)
{
lean_object* x_54; lean_object* x_55;
x_54 = lean_ctor_get(x_34, 0);
lean_dec(x_54);
x_55 = l_Lean_IR_EmitC_emitSSet___closed__6;
lean_object* x_51; lean_object* x_52;
x_51 = lean_ctor_get(x_34, 0);
lean_dec(x_51);
x_52 = l_Lean_IR_EmitC_emitSSet___closed__6;
lean_ctor_set_tag(x_34, 1);
lean_ctor_set(x_34, 0, x_55);
lean_ctor_set(x_34, 0, x_52);
return x_34;
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_34, 1);
lean_inc(x_56);
lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_53 = lean_ctor_get(x_34, 1);
lean_inc(x_53);
lean_dec(x_34);
x_57 = l_Lean_IR_EmitC_emitSSet___closed__6;
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_56);
return x_58;
x_54 = l_Lean_IR_EmitC_emitSSet___closed__6;
x_55 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_53);
return x_55;
}
}
}
@ -8226,7 +8213,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_box");
x_1 = lean_mk_string("lean_box_float");
return x_1;
}
}
@ -8234,7 +8221,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_box_uint32");
x_1 = lean_mk_string("lean_box");
return x_1;
}
}
@ -8242,7 +8229,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_box_uint64");
x_1 = lean_mk_string("lean_box_uint32");
return x_1;
}
}
@ -8250,6 +8237,14 @@ lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_box_uint64");
return x_1;
}
}
lean_object* _init_l_Lean_IR_EmitC_emitBoxFn___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_box_usize");
return x_1;
}
@ -8260,56 +8255,58 @@ _start:
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_IR_EmitC_emitSSet___closed__1;
x_5 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_5, 0, x_4);
lean_ctor_set(x_5, 1, x_3);
return x_5;
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_4 = l_Lean_IR_EmitC_emitBoxFn___closed__1;
x_5 = lean_string_append(x_3, x_4);
x_6 = lean_box(0);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
return x_7;
}
case 3:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = l_Lean_IR_EmitC_emitBoxFn___closed__2;
x_7 = lean_string_append(x_3, x_6);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_7);
return x_9;
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_8 = l_Lean_IR_EmitC_emitBoxFn___closed__3;
x_9 = lean_string_append(x_3, x_8);
x_10 = lean_box(0);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
return x_11;
}
case 4:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = l_Lean_IR_EmitC_emitBoxFn___closed__3;
x_11 = lean_string_append(x_3, x_10);
x_12 = lean_box(0);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_11);
return x_13;
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = l_Lean_IR_EmitC_emitBoxFn___closed__4;
x_13 = lean_string_append(x_3, x_12);
x_14 = lean_box(0);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
return x_15;
}
case 5:
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = l_Lean_IR_EmitC_emitBoxFn___closed__4;
x_15 = lean_string_append(x_3, x_14);
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
return x_17;
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_16 = l_Lean_IR_EmitC_emitBoxFn___closed__5;
x_17 = lean_string_append(x_3, x_16);
x_18 = lean_box(0);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);
return x_19;
}
default:
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = l_Lean_IR_EmitC_emitBoxFn___closed__1;
x_19 = lean_string_append(x_3, x_18);
x_20 = lean_box(0);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = l_Lean_IR_EmitC_emitBoxFn___closed__2;
x_21 = lean_string_append(x_3, x_20);
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
return x_23;
}
}
}
@ -8327,15 +8324,12 @@ return x_4;
lean_object* l_Lean_IR_EmitC_emitBox(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
lean_object* x_6; lean_object* x_7; lean_object* x_8; uint8_t x_9;
x_6 = l_Lean_IR_EmitC_emitLhs(x_1, x_4, x_5);
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = l_Lean_IR_EmitC_emitBoxFn(x_3, x_4, x_7);
if (lean_obj_tag(x_8) == 0)
{
uint8_t x_9;
x_9 = !lean_is_exclusive(x_8);
if (x_9 == 0)
{
@ -8385,30 +8379,6 @@ lean_ctor_set(x_35, 1, x_33);
return x_35;
}
}
else
{
uint8_t x_36;
lean_dec(x_2);
x_36 = !lean_is_exclusive(x_8);
if (x_36 == 0)
{
return x_8;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_8, 0);
x_38 = lean_ctor_get(x_8, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_8);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
}
}
lean_object* l_Lean_IR_EmitC_emitBox___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
@ -8424,7 +8394,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox");
x_1 = lean_mk_string("lean_unbox_float");
return x_1;
}
}
@ -8432,7 +8402,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox_uint32");
x_1 = lean_mk_string("lean_unbox");
return x_1;
}
}
@ -8440,7 +8410,7 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox_uint64");
x_1 = lean_mk_string("lean_unbox_uint32");
return x_1;
}
}
@ -8448,6 +8418,14 @@ lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox_uint64");
return x_1;
}
}
lean_object* _init_l_Lean_IR_EmitC_emitUnbox___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("lean_unbox_usize");
return x_1;
}
@ -8460,76 +8438,59 @@ x_20 = l_Lean_IR_EmitC_emitLhs(x_1, x_4, x_5);
switch (lean_obj_tag(x_2)) {
case 0:
{
uint8_t x_21;
lean_dec(x_3);
x_21 = !lean_is_exclusive(x_20);
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23;
x_22 = lean_ctor_get(x_20, 0);
lean_dec(x_22);
x_23 = l_Lean_IR_EmitC_emitSSet___closed__1;
lean_ctor_set_tag(x_20, 1);
lean_ctor_set(x_20, 0, x_23);
return x_20;
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_20, 1);
lean_inc(x_21);
lean_dec(x_20);
x_22 = l_Lean_IR_EmitC_emitUnbox___closed__1;
x_23 = lean_string_append(x_21, x_22);
x_6 = x_23;
goto block_19;
}
else
case 3:
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_20, 1);
lean_inc(x_24);
lean_dec(x_20);
x_25 = l_Lean_IR_EmitC_emitSSet___closed__1;
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
return x_26;
x_25 = l_Lean_IR_EmitC_emitUnbox___closed__3;
x_26 = lean_string_append(x_24, x_25);
x_6 = x_26;
goto block_19;
}
}
case 3:
case 4:
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_20, 1);
lean_inc(x_27);
lean_dec(x_20);
x_28 = l_Lean_IR_EmitC_emitUnbox___closed__2;
x_28 = l_Lean_IR_EmitC_emitUnbox___closed__4;
x_29 = lean_string_append(x_27, x_28);
x_6 = x_29;
goto block_19;
}
case 4:
case 5:
{
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_20, 1);
lean_inc(x_30);
lean_dec(x_20);
x_31 = l_Lean_IR_EmitC_emitUnbox___closed__3;
x_31 = l_Lean_IR_EmitC_emitUnbox___closed__5;
x_32 = lean_string_append(x_30, x_31);
x_6 = x_32;
goto block_19;
}
case 5:
default:
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_20, 1);
lean_inc(x_33);
lean_dec(x_20);
x_34 = l_Lean_IR_EmitC_emitUnbox___closed__4;
x_34 = l_Lean_IR_EmitC_emitUnbox___closed__2;
x_35 = lean_string_append(x_33, x_34);
x_6 = x_35;
goto block_19;
}
default:
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_20, 1);
lean_inc(x_36);
lean_dec(x_20);
x_37 = l_Lean_IR_EmitC_emitUnbox___closed__1;
x_38 = lean_string_append(x_36, x_37);
x_6 = x_38;
goto block_19;
}
}
block_19:
{
@ -13547,6 +13508,8 @@ l_Lean_IR_EmitC_emitSProj___closed__3 = _init_l_Lean_IR_EmitC_emitSProj___closed
lean_mark_persistent(l_Lean_IR_EmitC_emitSProj___closed__3);
l_Lean_IR_EmitC_emitSProj___closed__4 = _init_l_Lean_IR_EmitC_emitSProj___closed__4();
lean_mark_persistent(l_Lean_IR_EmitC_emitSProj___closed__4);
l_Lean_IR_EmitC_emitSProj___closed__5 = _init_l_Lean_IR_EmitC_emitSProj___closed__5();
lean_mark_persistent(l_Lean_IR_EmitC_emitSProj___closed__5);
l_Lean_IR_EmitC_emitExternCall___closed__1 = _init_l_Lean_IR_EmitC_emitExternCall___closed__1();
lean_mark_persistent(l_Lean_IR_EmitC_emitExternCall___closed__1);
l_Nat_forMAux___main___at_Lean_IR_EmitC_emitPartialApp___spec__1___closed__1 = _init_l_Nat_forMAux___main___at_Lean_IR_EmitC_emitPartialApp___spec__1___closed__1();
@ -13573,6 +13536,8 @@ l_Lean_IR_EmitC_emitBoxFn___closed__3 = _init_l_Lean_IR_EmitC_emitBoxFn___closed
lean_mark_persistent(l_Lean_IR_EmitC_emitBoxFn___closed__3);
l_Lean_IR_EmitC_emitBoxFn___closed__4 = _init_l_Lean_IR_EmitC_emitBoxFn___closed__4();
lean_mark_persistent(l_Lean_IR_EmitC_emitBoxFn___closed__4);
l_Lean_IR_EmitC_emitBoxFn___closed__5 = _init_l_Lean_IR_EmitC_emitBoxFn___closed__5();
lean_mark_persistent(l_Lean_IR_EmitC_emitBoxFn___closed__5);
l_Lean_IR_EmitC_emitUnbox___closed__1 = _init_l_Lean_IR_EmitC_emitUnbox___closed__1();
lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__1);
l_Lean_IR_EmitC_emitUnbox___closed__2 = _init_l_Lean_IR_EmitC_emitUnbox___closed__2();
@ -13581,6 +13546,8 @@ l_Lean_IR_EmitC_emitUnbox___closed__3 = _init_l_Lean_IR_EmitC_emitUnbox___closed
lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__3);
l_Lean_IR_EmitC_emitUnbox___closed__4 = _init_l_Lean_IR_EmitC_emitUnbox___closed__4();
lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__4);
l_Lean_IR_EmitC_emitUnbox___closed__5 = _init_l_Lean_IR_EmitC_emitUnbox___closed__5();
lean_mark_persistent(l_Lean_IR_EmitC_emitUnbox___closed__5);
l_Lean_IR_EmitC_emitIsShared___closed__1 = _init_l_Lean_IR_EmitC_emitIsShared___closed__1();
lean_mark_persistent(l_Lean_IR_EmitC_emitIsShared___closed__1);
l_Lean_IR_EmitC_emitIsTaggedPtr___closed__1 = _init_l_Lean_IR_EmitC_emitIsTaggedPtr___closed__1();