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:
Lean stage0 autoupdater 2024-08-04 19:11:50 +00:00
parent 1e9d96be22
commit 21b4377d36
34 changed files with 3825 additions and 4265 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/kernel/CMakeLists.txt generated
View file

@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
inductive.cpp trace.cpp)
inductive.cpp trace.cpp instantiate_mvars.cpp)

56
stage0/src/kernel/declaration.h generated
View file

@ -63,9 +63,9 @@ class constant_val : public object_ref {
public:
constant_val(name const & n, names const & lparams, expr const & type);
constant_val(constant_val const & other):object_ref(other) {}
constant_val(constant_val && other):object_ref(other) {}
constant_val(constant_val && other):object_ref(std::move(other)) {}
constant_val & operator=(constant_val const & other) { object_ref::operator=(other); return *this; }
constant_val & operator=(constant_val && other) { object_ref::operator=(other); return *this; }
constant_val & operator=(constant_val && other) { object_ref::operator=(std::move(other)); return *this; }
name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
@ -79,9 +79,9 @@ class axiom_val : public object_ref {
public:
axiom_val(name const & n, names const & lparams, expr const & type, bool is_unsafe);
axiom_val(axiom_val const & other):object_ref(other) {}
axiom_val(axiom_val && other):object_ref(other) {}
axiom_val(axiom_val && other):object_ref(std::move(other)) {}
axiom_val & operator=(axiom_val const & other) { object_ref::operator=(other); return *this; }
axiom_val & operator=(axiom_val && other) { object_ref::operator=(other); return *this; }
axiom_val & operator=(axiom_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
names const & get_lparams() const { return to_constant_val().get_lparams(); }
@ -105,9 +105,9 @@ class definition_val : public object_ref {
public:
definition_val(name const & n, names const & lparams, expr const & type, expr const & val, reducibility_hints const & hints, definition_safety safety, names const & all);
definition_val(definition_val const & other):object_ref(other) {}
definition_val(definition_val && other):object_ref(other) {}
definition_val(definition_val && other):object_ref(std::move(other)) {}
definition_val & operator=(definition_val const & other) { object_ref::operator=(other); return *this; }
definition_val & operator=(definition_val && other) { object_ref::operator=(other); return *this; }
definition_val & operator=(definition_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
names const & get_lparams() const { return to_constant_val().get_lparams(); }
@ -128,9 +128,9 @@ class theorem_val : public object_ref {
public:
theorem_val(name const & n, names const & lparams, expr const & type, expr const & val, names const & all);
theorem_val(theorem_val const & other):object_ref(other) {}
theorem_val(theorem_val && other):object_ref(other) {}
theorem_val(theorem_val && other):object_ref(std::move(other)) {}
theorem_val & operator=(theorem_val const & other) { object_ref::operator=(other); return *this; }
theorem_val & operator=(theorem_val && other) { object_ref::operator=(other); return *this; }
theorem_val & operator=(theorem_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
names const & get_lparams() const { return to_constant_val().get_lparams(); }
@ -148,9 +148,9 @@ class opaque_val : public object_ref {
public:
opaque_val(name const & n, names const & lparams, expr const & type, expr const & val, bool is_unsafe, names const & all);
opaque_val(opaque_val const & other):object_ref(other) {}
opaque_val(opaque_val && other):object_ref(other) {}
opaque_val(opaque_val && other):object_ref(std::move(other)) {}
opaque_val & operator=(opaque_val const & other) { object_ref::operator=(other); return *this; }
opaque_val & operator=(opaque_val && other) { object_ref::operator=(other); return *this; }
opaque_val & operator=(opaque_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
names const & get_lparams() const { return to_constant_val().get_lparams(); }
@ -179,9 +179,9 @@ class inductive_type : public object_ref {
public:
inductive_type(name const & id, expr const & type, constructors const & cnstrs);
inductive_type(inductive_type const & other):object_ref(other) {}
inductive_type(inductive_type && other):object_ref(other) {}
inductive_type(inductive_type && other):object_ref(std::move(other)) {}
inductive_type & operator=(inductive_type const & other) { object_ref::operator=(other); return *this; }
inductive_type & operator=(inductive_type && other) { object_ref::operator=(other); return *this; }
inductive_type & operator=(inductive_type && other) { object_ref::operator=(std::move(other)); return *this; }
name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(*this, 1)); }
constructors const & get_cnstrs() const { return static_cast<constructors const &>(cnstr_get_ref(*this, 2)); }
@ -205,7 +205,7 @@ class declaration : public object_ref {
public:
declaration();
declaration(declaration const & other):object_ref(other) {}
declaration(declaration && other):object_ref(other) {}
declaration(declaration && other):object_ref(std::move(other)) {}
/* low-level constructors */
explicit declaration(object * o):object_ref(o) {}
explicit declaration(b_obj_arg o, bool b):object_ref(o, b) {}
@ -213,7 +213,7 @@ public:
declaration_kind kind() const { return static_cast<declaration_kind>(obj_tag(raw())); }
declaration & operator=(declaration const & other) { object_ref::operator=(other); return *this; }
declaration & operator=(declaration && other) { object_ref::operator=(other); return *this; }
declaration & operator=(declaration && other) { object_ref::operator=(std::move(other)); return *this; }
friend bool is_eqp(declaration const & d1, declaration const & d2) { return d1.raw() == d2.raw(); }
@ -263,10 +263,10 @@ declaration mk_axiom_inferring_unsafe(environment const & env, name const & n,
class inductive_decl : public object_ref {
public:
inductive_decl(inductive_decl const & other):object_ref(other) {}
inductive_decl(inductive_decl && other):object_ref(other) {}
inductive_decl(inductive_decl && other):object_ref(std::move(other)) {}
inductive_decl(declaration const & d):object_ref(d) { lean_assert(d.is_inductive()); }
inductive_decl & operator=(inductive_decl const & other) { object_ref::operator=(other); return *this; }
inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(other); return *this; }
inductive_decl & operator=(inductive_decl && other) { object_ref::operator=(std::move(other)); return *this; }
names const & get_lparams() const { return static_cast<names const &>(cnstr_get_ref(raw(), 0)); }
nat const & get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 1)); }
inductive_types const & get_types() const { return static_cast<inductive_types const &>(cnstr_get_ref(raw(), 2)); }
@ -290,9 +290,9 @@ public:
inductive_val(name const & n, names const & lparams, expr const & type, unsigned nparams,
unsigned nindices, names const & all, names const & cnstrs, unsigned nnested, bool is_rec, bool is_unsafe, bool is_reflexive);
inductive_val(inductive_val const & other):object_ref(other) {}
inductive_val(inductive_val && other):object_ref(other) {}
inductive_val(inductive_val && other):object_ref(std::move(other)) {}
inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; }
inductive_val & operator=(inductive_val && other) { object_ref::operator=(other); return *this; }
inductive_val & operator=(inductive_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
@ -317,9 +317,9 @@ class constructor_val : public object_ref {
public:
constructor_val(name const & n, names const & lparams, expr const & type, name const & induct, unsigned cidx, unsigned nparams, unsigned nfields, bool is_unsafe);
constructor_val(constructor_val const & other):object_ref(other) {}
constructor_val(constructor_val && other):object_ref(other) {}
constructor_val(constructor_val && other):object_ref(std::move(other)) {}
constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; }
constructor_val & operator=(constructor_val && other) { object_ref::operator=(other); return *this; }
constructor_val & operator=(constructor_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_induct() const { return static_cast<name const &>(cnstr_get_ref(*this, 1)); }
unsigned get_cidx() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
@ -338,9 +338,9 @@ class recursor_rule : public object_ref {
public:
recursor_rule(name const & cnstr, unsigned nfields, expr const & rhs);
recursor_rule(recursor_rule const & other):object_ref(other) {}
recursor_rule(recursor_rule && other):object_ref(other) {}
recursor_rule(recursor_rule && other):object_ref(std::move(other)) {}
recursor_rule & operator=(recursor_rule const & other) { object_ref::operator=(other); return *this; }
recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(other); return *this; }
recursor_rule & operator=(recursor_rule && other) { object_ref::operator=(std::move(other)); return *this; }
name const & get_cnstr() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
unsigned get_nfields() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
expr const & get_rhs() const { return static_cast<expr const &>(cnstr_get_ref(*this, 2)); }
@ -365,9 +365,9 @@ public:
names const & all, unsigned nparams, unsigned nindices, unsigned nmotives,
unsigned nminors, recursor_rules const & rules, bool k, bool is_unsafe);
recursor_val(recursor_val const & other):object_ref(other) {}
recursor_val(recursor_val && other):object_ref(other) {}
recursor_val(recursor_val && other):object_ref(std::move(other)) {}
recursor_val & operator=(recursor_val const & other) { object_ref::operator=(other); return *this; }
recursor_val & operator=(recursor_val && other) { object_ref::operator=(other); return *this; }
recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
name const & get_induct() const { return get_name().get_prefix(); }
@ -398,9 +398,9 @@ class quot_val : public object_ref {
public:
quot_val(name const & n, names const & lparams, expr const & type, quot_kind k);
quot_val(quot_val const & other):object_ref(other) {}
quot_val(quot_val && other):object_ref(other) {}
quot_val(quot_val && other):object_ref(std::move(other)) {}
quot_val & operator=(quot_val const & other) { object_ref::operator=(other); return *this; }
quot_val & operator=(quot_val && other) { object_ref::operator=(other); return *this; }
quot_val & operator=(quot_val && other) { object_ref::operator=(std::move(other)); return *this; }
constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
name const & get_name() const { return to_constant_val().get_name(); }
names const & get_lparams() const { return to_constant_val().get_lparams(); }
@ -434,14 +434,14 @@ public:
constant_info(constructor_val const & v);
constant_info(recursor_val const & v);
constant_info(constant_info const & other):object_ref(other) {}
constant_info(constant_info && other):object_ref(other) {}
constant_info(constant_info && other):object_ref(std::move(other)) {}
explicit constant_info(b_obj_arg o, bool b):object_ref(o, b) {}
explicit constant_info(obj_arg o):object_ref(o) {}
constant_info_kind kind() const { return static_cast<constant_info_kind>(cnstr_tag(raw())); }
constant_info & operator=(constant_info const & other) { object_ref::operator=(other); return *this; }
constant_info & operator=(constant_info && other) { object_ref::operator=(other); return *this; }
constant_info & operator=(constant_info && other) { object_ref::operator=(std::move(other)); return *this; }
friend bool is_eqp(constant_info const & d1, constant_info const & d2) { return d1.raw() == d2.raw(); }

8
stage0/src/kernel/expr.h generated
View file

@ -50,9 +50,9 @@ public:
explicit literal(nat const & v);
literal():literal(0u) {}
literal(literal const & other):object_ref(other) {}
literal(literal && other):object_ref(other) {}
literal(literal && other):object_ref(std::move(other)) {}
literal & operator=(literal const & other) { object_ref::operator=(other); return *this; }
literal & operator=(literal && other) { object_ref::operator=(other); return *this; }
literal & operator=(literal && other) { object_ref::operator=(std::move(other)); return *this; }
static literal_kind kind(object * o) { return static_cast<literal_kind>(cnstr_tag(o)); }
literal_kind kind() const { return kind(raw()); }
@ -100,14 +100,14 @@ class expr : public object_ref {
public:
expr();
expr(expr const & other):object_ref(other) {}
expr(expr && other):object_ref(other) {}
expr(expr && other):object_ref(std::move(other)) {}
explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
explicit expr(obj_arg o):object_ref(o) {}
static expr_kind kind(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
expr_kind kind() const { return kind(raw()); }
expr & operator=(expr const & other) { object_ref::operator=(other); return *this; }
expr & operator=(expr && other) { object_ref::operator=(other); return *this; }
expr & operator=(expr && other) { object_ref::operator=(std::move(other)); return *this; }
friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); }
};

95
stage0/src/kernel/instantiate_mvars.cpp generated Normal file
View file

@ -0,0 +1,95 @@
/*
Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
*/
#include <unordered_map>
#include "runtime/option_ref.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
/*
This module is not used by the kernel. It just provides an efficient implementation of
`instantiateExprMVars`
*/
namespace lean {
extern "C" object * lean_get_lmvar_assignment(obj_arg mctx, obj_arg mid);
extern "C" object * lean_assign_lmvar(obj_arg mctx, obj_arg mid, obj_arg val);
typedef object_ref metavar_ctx;
void assign_lmvar(metavar_ctx & mctx, name const & mid, level const & l) {
object * r = lean_assign_lmvar(mctx.steal(), mid.to_obj_arg(), l.to_obj_arg());
mctx.set_box(r);
}
option_ref<level> get_lmvar_assignment(metavar_ctx & mctx, name const & mid) {
return option_ref<level>(lean_get_lmvar_assignment(mctx.to_obj_arg(), mid.to_obj_arg()));
}
class instantiate_lmvar_fn {
metavar_ctx & m_mctx;
std::unordered_map<lean_object *, lean_object *> m_cache;
inline level cache(level const & l, level && r, bool shared) {
if (shared) {
m_cache.insert(mk_pair(l.raw(), r.raw()));
}
return r;
}
public:
instantiate_lmvar_fn(metavar_ctx & mctx):m_mctx(mctx) {}
level visit(level const & l) {
if (!has_mvar(l))
return l;
bool shared = false;
if (is_shared(l)) {
auto it = m_cache.find(l.raw());
if (it != m_cache.end()) {
return level(it->second, true);
}
shared = true;
}
switch (l.kind()) {
case level_kind::Succ:
return cache(l, update_succ(l, visit(succ_of(l))), shared);
case level_kind::Max: case level_kind::IMax:
return cache(l, update_max(l, visit(level_lhs(l)), visit(level_rhs(l))), shared);
case level_kind::Zero: case level_kind::Param:
lean_unreachable();
case level_kind::MVar: {
option_ref<level> r = get_lmvar_assignment(m_mctx, mvar_id(l));
if (!r) {
return l;
} else {
level a(r.get_val());
if (!has_mvar(a)) {
return a;
} else {
level a_new = visit(a);
if (!is_eqp(a, a_new)) {
assign_lmvar(m_mctx, mvar_id(l), a_new);
}
return a_new;
}
}
}}
}
level operator()(level const & l) { return visit(l); }
};
extern "C" LEAN_EXPORT object * lean_instantiate_level_mvars(object * m, object * l) {
metavar_ctx mctx(m);
level l_new = instantiate_lmvar_fn(mctx)(level(l));
object * r = alloc_cnstr(0, 2, 0);
cnstr_set(r, 0, mctx.steal());
cnstr_set(r, 1, l_new.steal());
return r;
}
extern "C" LEAN_EXPORT object * lean_instantiate_expr_mvars(object *, object *) {
lean_internal_panic("not implemented yet");
}
}

6
stage0/src/kernel/level.h generated
View file

@ -43,14 +43,14 @@ public:
explicit level(obj_arg o):object_ref(o) {}
explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
level(level const & other):object_ref(other) {}
level(level && other):object_ref(other) {}
level(level && other):object_ref(std::move(other)) {}
level_kind kind() const {
return lean_is_scalar(raw()) ? level_kind::Zero : static_cast<level_kind>(lean_ptr_tag(raw()));
}
unsigned hash() const;
level & operator=(level const & other) { object_ref::operator=(other); return *this; }
level & operator=(level && other) { object_ref::operator=(other); return *this; }
level & operator=(level && other) { object_ref::operator=(std::move(other)); return *this; }
friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); }
@ -82,6 +82,8 @@ inline bool operator!=(level const & l1, level const & l2) { return !operator==(
struct level_hash { unsigned operator()(level const & n) const { return n.hash(); } };
struct level_eq { bool operator()(level const & n1, level const & n2) const { return n1 == n2; } };
inline bool is_shared(level const & l) { return !is_exclusive(l.raw()); }
inline optional<level> none_level() { return optional<level>(); }
inline optional<level> some_level(level const & e) { return optional<level>(e); }
inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }

8
stage0/src/kernel/local_ctx.h generated
View file

@ -27,11 +27,11 @@ class local_decl : public object_ref {
public:
local_decl();
local_decl(local_decl const & other):object_ref(other) {}
local_decl(local_decl && other):object_ref(other) {}
local_decl(local_decl && other):object_ref(std::move(other)) {}
local_decl(obj_arg o):object_ref(o) {}
local_decl(b_obj_arg o, bool):object_ref(o, true) {}
local_decl & operator=(local_decl const & other) { object_ref::operator=(other); return *this; }
local_decl & operator=(local_decl && other) { object_ref::operator=(other); return *this; }
local_decl & operator=(local_decl && other) { object_ref::operator=(std::move(other)); return *this; }
friend bool is_eqp(local_decl const & d1, local_decl const & d2) { return d1.raw() == d2.raw(); }
unsigned get_idx() const { return static_cast<nat const &>(cnstr_get_ref(raw(), 0)).get_small_value(); }
name const & get_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 1)); }
@ -54,9 +54,9 @@ public:
explicit local_ctx(obj_arg o):object_ref(o) {}
local_ctx(b_obj_arg o, bool):object_ref(o, true) {}
local_ctx(local_ctx const & other):object_ref(other) {}
local_ctx(local_ctx && other):object_ref(other) {}
local_ctx(local_ctx && other):object_ref(std::move(other)) {}
local_ctx & operator=(local_ctx const & other) { object_ref::operator=(other); return *this; }
local_ctx & operator=(local_ctx && other) { object_ref::operator=(other); return *this; }
local_ctx & operator=(local_ctx && other) { object_ref::operator=(std::move(other)); return *this; }
bool empty() const;

5
stage0/src/kernel/replace_fn.cpp generated
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <vector>
#include <memory>
#include <utility>
#include <unordered_map>
#include "kernel/replace_fn.h"
@ -21,7 +22,7 @@ class replace_rec_fn {
std::function<optional<expr>(expr const &, unsigned)> m_f;
bool m_use_cache;
expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
expr save_result(expr const & e, unsigned offset, expr r, bool shared) {
if (shared)
m_cache.insert(mk_pair(mk_pair(e.raw(), offset), r));
return r;
@ -36,7 +37,7 @@ class replace_rec_fn {
shared = true;
}
if (optional<expr> r = m_f(e, offset)) {
return save_result(e, offset, *r, shared);
return save_result(e, offset, std::move(*r), shared);
} else {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::Sort:

4
stage0/src/library/compiler/specialize.cpp generated
View file

@ -92,10 +92,10 @@ public:
object_ref(mk_cnstr(0, ns, ks)) {}
spec_info():spec_info(names(), spec_arg_kinds()) {}
spec_info(spec_info const & other):object_ref(other) {}
spec_info(spec_info && other):object_ref(other) {}
spec_info(spec_info && other):object_ref(std::move(other)) {}
spec_info(b_obj_arg o, bool b):object_ref(o, b) {}
spec_info & operator=(spec_info const & other) { object_ref::operator=(other); return *this; }
spec_info & operator=(spec_info && other) { object_ref::operator=(other); return *this; }
spec_info & operator=(spec_info && other) { object_ref::operator=(std::move(other)); return *this; }
names const & get_mutual_decls() const { return static_cast<names const &>(cnstr_get_ref(*this, 0)); }
spec_arg_kinds const & get_arg_kinds() const { return static_cast<spec_arg_kinds const &>(cnstr_get_ref(*this, 1)); }
};

4
stage0/src/library/projection.h generated
View file

@ -24,13 +24,13 @@ public:
projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit);
projection_info():projection_info(name(), 0, 0, false) {}
projection_info(projection_info const & other):object_ref(other) {}
projection_info(projection_info && other):object_ref(other) {}
projection_info(projection_info && other):object_ref(std::move(other)) {}
/* low-level constructors */
explicit projection_info(object * o):object_ref(o) {}
explicit projection_info(b_obj_arg o, bool b):object_ref(o, b) {}
explicit projection_info(object_ref const & o):object_ref(o) {}
projection_info & operator=(projection_info const & other) { object_ref::operator=(other); return *this; }
projection_info & operator=(projection_info && other) { object_ref::operator=(other); return *this; }
projection_info & operator=(projection_info && other) { object_ref::operator=(std::move(other)); return *this; }
name const & get_constructor() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
unsigned get_i() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }

4
stage0/src/runtime/array_ref.h generated
View file

@ -28,12 +28,12 @@ public:
array_ref(b_obj_arg o, bool b):object_ref(o, b) {}
array_ref():object_ref(array_mk_empty()) {}
array_ref(array_ref const & other):object_ref(other) {}
array_ref(array_ref && other):object_ref(other) {}
array_ref(array_ref && other):object_ref(std::move(other)) {}
array_ref(std::initializer_list<T> const & elems):object_ref(to_array(elems)) {}
array_ref(buffer<T> const & elems):object_ref(to_array(elems)) {}
array_ref & operator=(array_ref const & other) { object_ref::operator=(other); return *this; }
array_ref & operator=(array_ref && other) { object_ref::operator=(other); return *this; }
array_ref & operator=(array_ref && other) { object_ref::operator=(std::move(other)); return *this; }
size_t size() const { return array_size(raw()); }

4
stage0/src/runtime/list_ref.h generated
View file

@ -23,7 +23,7 @@ public:
explicit list_ref(list_ref<T> const * l) { if (l) *this = *l; }
list_ref(T const & h, list_ref<T> const & t):object_ref(mk_cnstr(1, h.raw(), t.raw())) { inc(h.raw()); inc(t.raw()); }
list_ref(list_ref const & other):object_ref(other) {}
list_ref(list_ref && other):object_ref(other) {}
list_ref(list_ref && other):object_ref(std::move(other)) {}
template<typename It> list_ref(It const & begin, It const & end):list_ref() {
auto it = end;
while (it != begin) {
@ -35,7 +35,7 @@ public:
list_ref(buffer<T> const & b):list_ref(b.begin(), b.end()) {}
list_ref & operator=(list_ref const & other) { object_ref::operator=(other); return *this; }
list_ref & operator=(list_ref && other) { object_ref::operator=(other); return *this; }
list_ref & operator=(list_ref && other) { object_ref::operator=(std::move(other)); return *this; }
explicit operator bool() const { return !is_scalar(raw()); }
friend bool is_nil(list_ref const & l) { return is_scalar(l.raw()); }

4
stage0/src/runtime/object_ref.h generated
View file

@ -35,6 +35,10 @@ public:
s.m_obj = box(0);
return *this;
}
void set_box(object * o) {
lean_assert(is_scalar(m_obj));
m_obj = o;
}
object * raw() const { return m_obj; }
object * steal() { object * r = m_obj; m_obj = box(0); return r; }
object * to_obj_arg() const { inc(m_obj); return m_obj; }

6
stage0/src/runtime/option_ref.h generated
View file

@ -16,18 +16,20 @@ public:
option_ref(b_obj_arg o, bool b):object_ref(o, b) {}
option_ref():object_ref(box(0)) {}
option_ref(option_ref const & other):object_ref(other) {}
option_ref(option_ref && other):object_ref(other) {}
option_ref(option_ref && other):object_ref(std::move(other)) {}
explicit option_ref(T const & a):object_ref(mk_cnstr(1, a.raw())) { inc(a.raw()); }
explicit option_ref(T const * a) { if (a) *this = option_ref(*a); }
explicit option_ref(option_ref<T> const * o) { if (o) *this = *o; }
explicit option_ref(optional<T> const & o):option_ref(o ? &*o : nullptr) {}
option_ref & operator=(option_ref const & other) { object_ref::operator=(other); return *this; }
option_ref & operator=(option_ref && other) { object_ref::operator=(other); return *this; }
option_ref & operator=(option_ref && other) { object_ref::operator=(std::move(other)); return *this; }
explicit operator bool() const { return !is_scalar(raw()); }
optional<T> get() const { return *this ? some(static_cast<T const &>(cnstr_get_ref(*this, 0))) : optional<T>(); }
T get_val() const { lean_assert(*this); return static_cast<T const &>(cnstr_get_ref(*this, 0)); }
/** \brief Structural equality. */
friend bool operator==(option_ref const & o1, option_ref const & o2) {
return o1.get() == o2.get();

16
stage0/src/runtime/optional.h generated
View file

@ -31,13 +31,13 @@ public:
}
optional(optional && other):m_some(other.m_some) {
if (other.m_some)
new (&m_value) T(std::forward<T>(other.m_value));
new (&m_value) T(std::move(other.m_value));
}
explicit optional(T const & v):m_some(true) {
new (&m_value) T(v);
}
explicit optional(T && v):m_some(true) {
new (&m_value) T(std::forward<T>(v));
new (&m_value) T(std::move(v));
}
template<typename... Args>
explicit optional(Args&&... args):m_some(true) {
@ -84,7 +84,7 @@ public:
m_value.~T();
m_some = other.m_some;
if (m_some)
new (&m_value) T(std::forward<T>(other.m_value));
new (&m_value) T(std::move(other.m_value));
return *this;
}
optional& operator=(T const & other) {
@ -98,7 +98,7 @@ public:
if (m_some)
m_value.~T();
m_some = true;
new (&m_value) T(std::forward<T>(other));
new (&m_value) T(std::move(other));
return *this;
}
@ -130,9 +130,9 @@ template<> class optional<P> { \
public: \
optional():m_value(nullptr) {} \
optional(optional const & other):m_value(other.m_value) {} \
optional(optional && other):m_value(std::forward<P>(other.m_value)) {} \
optional(optional && other):m_value(std::move(other.m_value)) {} \
explicit optional(P const & v):m_value(v) {} \
explicit optional(P && v):m_value(std::forward<P>(v)) {} \
explicit optional(P && v):m_value(std::move(v)) {} \
\
explicit operator bool() const { return m_value.m_ptr != nullptr; } \
P const * operator->() const { lean_assert(m_value.m_ptr); return &m_value; } \
@ -142,9 +142,9 @@ public: \
P const & value() const { lean_assert(m_value.m_ptr); return m_value; } \
P & value() { lean_assert(m_value.m_ptr); return m_value; } \
optional & operator=(optional const & other) { m_value = other.m_value; return *this; } \
optional& operator=(optional && other) { m_value = std::forward<P>(other.m_value); return *this; } \
optional& operator=(optional && other) { m_value = std::move(other.m_value); return *this; } \
optional& operator=(P const & other) { m_value = other; return *this; } \
optional& operator=(P && other) { m_value = std::forward<P>(other); return *this; } \
optional& operator=(P && other) { m_value = std::move(other); return *this; } \
friend bool operator==(optional const & o1, optional const & o2) { \
return static_cast<bool>(o1) == static_cast<bool>(o2) && (!o1 || o1.m_value == o2.m_value); \
} \

4
stage0/src/runtime/string_ref.h generated
View file

@ -17,11 +17,11 @@ public:
explicit string_ref(std::string const & s):object_ref(mk_string(s)) {}
explicit string_ref(sstream const & strm):string_ref(strm.str()) {}
string_ref(string_ref const & other):object_ref(other) {}
string_ref(string_ref && other):object_ref(other) {}
string_ref(string_ref && other):object_ref(std::move(other)) {}
explicit string_ref(obj_arg o):object_ref(o) {}
string_ref(b_obj_arg o, bool b):object_ref(o, b) {}
string_ref & operator=(string_ref const & other) { object_ref::operator=(other); return *this; }
string_ref & operator=(string_ref && other) { object_ref::operator=(other); return *this; }
string_ref & operator=(string_ref && other) { object_ref::operator=(std::move(other)); return *this; }
/* Number of bytes used to store the string in UTF8.
Remark: it does not include the null character added in the end to make it efficient to
convert to C string. */

4
stage0/src/util/kvmap.h generated
View file

@ -30,9 +30,9 @@ public:
explicit data_value(name const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::Name), v.raw())) { inc(v.raw()); }
data_value():data_value(false) {}
data_value(data_value const & other):object_ref(other) {}
data_value(data_value && other):object_ref(other) {}
data_value(data_value && other):object_ref(std::move(other)) {}
data_value & operator=(data_value const & other) { object_ref::operator=(other); return *this; }
data_value & operator=(data_value && other) { object_ref::operator=(other); return *this; }
data_value & operator=(data_value && other) { object_ref::operator=(std::move(other)); return *this; }
data_value_kind kind() const { return static_cast<data_value_kind>(cnstr_tag(raw())); }
string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }

4
stage0/src/util/name.h generated
View file

@ -74,7 +74,7 @@ public:
name(std::string const & s):name(name(), string_ref(s)) {}
name(string_ref const & s):name(name(), s) {}
name(name const & other):object_ref(other) {}
name(name && other):object_ref(other) {}
name(name && other):object_ref(std::move(other)) {}
/**
\brief Create a hierarchical name using the given strings.
Example: <code>name{"foo", "bla", "tst"}</code> creates the hierarchical
@ -97,7 +97,7 @@ public:
*/
static name mk_internal_unique_name();
name & operator=(name const & other) { object_ref::operator=(other); return *this; }
name & operator=(name && other) { object_ref::operator=(other); return *this; }
name & operator=(name && other) { object_ref::operator=(std::move(other)); return *this; }
static uint64_t hash(b_obj_arg n) {
lean_assert(lean_name_hash(n) == lean_name_hash_exported_b(n));
return lean_name_hash(n);

4
stage0/src/util/nat.h generated
View file

@ -27,10 +27,10 @@ public:
static nat of_size_t(size_t v) { return nat(lean_usize_to_nat(v)); }
nat(nat const & other):object_ref(other) {}
nat(nat && other):object_ref(other) {}
nat(nat && other):object_ref(std::move(other)) {}
nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
nat & operator=(nat && other) { object_ref::operator=(std::move(other)); return *this; }
bool is_small() const { return is_scalar(raw()); }
size_t get_small_value() const { lean_assert(is_small()); return unbox(raw()); }
bool is_zero() const { return is_small() && get_small_value() == 0; }

4
stage0/src/util/shell.cpp generated
View file

@ -310,7 +310,9 @@ options set_config_option(options const & opts, char const * in) {
<< "' cannot be set in the command line, use set_option command");
}
} else {
throw lean::exception(lean::sstream() << "invalid -D parameter, unknown configuration option '" << opt << "'");
// More options may be registered by imports, so we leave validating them to the Lean side.
// This (minor) duplication will be resolved when this file is rewritten in Lean.
return opts.update(opt, val.c_str());
}
}

8
stage0/stdlib/Init/Data/BitVec/Basic.c generated
View file

@ -3498,11 +3498,9 @@ return x_10;
}
else
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_nat_mul(x_1, x_4);
x_12 = l_BitVec_ofNat(x_11, x_4);
lean_dec(x_11);
return x_12;
lean_object* x_11;
x_11 = l_BitVec_nil___closed__1;
return x_11;
}
}
}

55
stage0/stdlib/Init/Data/BitVec/Lemmas.c generated
View file

@ -13,12 +13,17 @@
#ifdef __cplusplus
extern "C" {
#endif
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_BitVec_ofNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_BitVec_intMax___boxed(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_intMax(lean_object*);
lean_object* lean_nat_pow(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter___rarg___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_ofBoolListBE_match__1_splitter(lean_object*);
LEAN_EXPORT lean_object* l_BitVec_intMax(lean_object* x_1) {
@ -83,6 +88,56 @@ lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; uint8_t x_6;
x_5 = lean_unsigned_to_nat(0u);
x_6 = lean_nat_dec_eq(x_1, x_5);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_dec(x_3);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_1, x_7);
x_9 = lean_apply_2(x_4, x_8, x_2);
return x_9;
}
else
{
lean_object* x_10;
lean_dec(x_4);
x_10 = lean_apply_1(x_3, x_2);
return x_10;
}
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg___boxed), 4, 0);
return x_3;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_1);
return x_5;
}
}
LEAN_EXPORT lean_object* l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Init_Data_BitVec_Lemmas_0__BitVec_replicate_match__1_splitter(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init_Data_Bool(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_BitVec_Basic(uint8_t builtin, lean_object*);
lean_object* initialize_Init_Data_Fin_Lemmas(uint8_t builtin, lean_object*);

18
stage0/stdlib/Init/Data/Int/Basic.c generated
View file

@ -52,6 +52,7 @@ lean_object* lean_nat_to_int(lean_object*);
LEAN_EXPORT lean_object* l_instCoeHTCTIntOfIntCast___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Int_pow(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int___aux__Init__Data__Int__Basic______unexpand__Int__negSucc__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_instNatPow;
LEAN_EXPORT lean_object* l_Int_decLe___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_decLt___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_negSucc___boxed(lean_object*);
@ -64,6 +65,7 @@ LEAN_EXPORT lean_object* l_Int_cast___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_instLTInt;
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
static lean_object* l_Int_instNatPow___closed__1;
lean_object* l_Lean_Syntax_node2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
static lean_object* l_Int___aux__Init__Data__Int__Basic______unexpand__Int__negSucc__1___closed__1;
@ -78,7 +80,6 @@ LEAN_EXPORT lean_object* l_Int_subNatNat(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_ofNat___boxed(lean_object*);
static lean_object* l_Int___aux__Init__Data__Int__Basic______macroRules__Int__term_x2d_x5b___x2b1_x5d__1___closed__3;
LEAN_EXPORT lean_object* l_Int_subNatNat___boxed(lean_object*, lean_object*);
static lean_object* l_Int_instHPowNat___closed__1;
lean_object* lean_nat_abs(lean_object*);
lean_object* lean_int_mul(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_instDecidableEq___boxed(lean_object*, lean_object*);
@ -94,7 +95,6 @@ LEAN_EXPORT lean_object* l_Int_neg___boxed(lean_object*);
lean_object* l_Lean_Syntax_node1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_instSub;
static lean_object* l_Int_term_x2d_x5b___x2b1_x5d___closed__4;
LEAN_EXPORT lean_object* l_Int_instHPowNat;
LEAN_EXPORT lean_object* l_Int_mul___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Int_toNat(lean_object*);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
@ -1075,7 +1075,7 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l_Int_instHPowNat___closed__1() {
static lean_object* _init_l_Int_instNatPow___closed__1() {
_start:
{
lean_object* x_1;
@ -1083,11 +1083,11 @@ x_1 = lean_alloc_closure((void*)(l_Int_pow___boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Int_instHPowNat() {
static lean_object* _init_l_Int_instNatPow() {
_start:
{
lean_object* x_1;
x_1 = l_Int_instHPowNat___closed__1;
x_1 = l_Int_instNatPow___closed__1;
return x_1;
}
}
@ -1324,10 +1324,10 @@ l_Int_sign___closed__2 = _init_l_Int_sign___closed__2();
lean_mark_persistent(l_Int_sign___closed__2);
l_Int_instDvd = _init_l_Int_instDvd();
lean_mark_persistent(l_Int_instDvd);
l_Int_instHPowNat___closed__1 = _init_l_Int_instHPowNat___closed__1();
lean_mark_persistent(l_Int_instHPowNat___closed__1);
l_Int_instHPowNat = _init_l_Int_instHPowNat();
lean_mark_persistent(l_Int_instHPowNat);
l_Int_instNatPow___closed__1 = _init_l_Int_instNatPow___closed__1();
lean_mark_persistent(l_Int_instNatPow___closed__1);
l_Int_instNatPow = _init_l_Int_instNatPow();
lean_mark_persistent(l_Int_instNatPow);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

2930
stage0/stdlib/Lake/Build/Module.c generated
View file

File diff suppressed because it is too large Load diff

6
stage0/stdlib/Lean/Compiler/CSimpAttr.c generated
View file

@ -34,6 +34,7 @@ uint8_t lean_usize_dec_le(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_474____lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Compiler_CSimp_add___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_138_(lean_object*);
lean_object* l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6443____spec__4(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Compiler_hasCSimpAttribute___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_138____closed__4;
size_t lean_uint64_to_usize(uint64_t);
@ -109,7 +110,6 @@ size_t lean_hashmap_mk_idx(lean_object*, uint64_t);
LEAN_EXPORT uint8_t l_Lean_Compiler_hasCSimpAttribute(lean_object*, lean_object*);
lean_object* l_Lean_MessageData_ofExpr(lean_object*);
static lean_object* l_Lean_ScopedEnvExtension_add___at_Lean_Compiler_CSimp_add___spec__2___closed__1;
lean_object* l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6347____spec__4(lean_object*);
static lean_object* l_Lean_Compiler_CSimp_initFn____x40_Lean_Compiler_CSimpAttr___hyg_138____closed__5;
lean_object* l_Lean_Expr_constLevels_x21(lean_object*);
lean_object* l_Lean_throwError___at_Lean_AttributeImpl_erase___default___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -350,7 +350,7 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = l_Lean_SMap_switch___at_Lean_Compiler_CSimp_State_switch___spec__1(x_3);
x_6 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6347____spec__4(x_4);
x_6 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6443____spec__4(x_4);
lean_ctor_set(x_1, 1, x_6);
lean_ctor_set(x_1, 0, x_5);
return x_1;
@ -364,7 +364,7 @@ lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_1);
x_9 = l_Lean_SMap_switch___at_Lean_Compiler_CSimp_State_switch___spec__1(x_7);
x_10 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6347____spec__4(x_8);
x_10 = l_Lean_SMap_switch___at_Lean_initFn____x40_Lean_Environment___hyg_6443____spec__4(x_8);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);

1147
stage0/stdlib/Lean/Elab/Frontend.c generated
View file

File diff suppressed because it is too large Load diff

95
stage0/stdlib/Lean/Elab/Import.c generated
View file

@ -42,7 +42,7 @@ lean_object* l_Array_append___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_processHeader___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_headerToImports___spec__1(size_t, size_t, lean_object*);
static lean_object* l_Lean_Elab_parseImports___closed__1;
lean_object* l_Lean_findOLean(lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_findOLean(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_headerToImports___closed__6;
LEAN_EXPORT lean_object* l_Lean_Elab_parseImports(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
@ -894,80 +894,79 @@ return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
lean_object* x_8; lean_object* x_9; lean_object* x_10;
lean_dec(x_4);
x_8 = lean_array_uget(x_1, x_3);
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
lean_dec(x_8);
x_10 = 0;
x_11 = l_Lean_findOLean(x_9, x_10, x_5);
if (lean_obj_tag(x_11) == 0)
x_10 = l_Lean_findOLean(x_9, x_5);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_ctor_get(x_11, 0);
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_IO_println___at_Lean_Elab_printImports___spec__1(x_12, x_13);
if (lean_obj_tag(x_14) == 0)
lean_dec(x_10);
x_13 = l_IO_println___at_Lean_Elab_printImports___spec__1(x_11, x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18;
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
x_16 = 1;
x_17 = lean_usize_add(x_3, x_16);
x_18 = lean_box(0);
x_3 = x_17;
x_4 = x_18;
x_5 = x_15;
lean_object* x_14; size_t x_15; size_t x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = 1;
x_16 = lean_usize_add(x_3, x_15);
x_17 = lean_box(0);
x_3 = x_16;
x_4 = x_17;
x_5 = x_14;
goto _start;
}
else
{
uint8_t x_20;
x_20 = !lean_is_exclusive(x_14);
if (x_20 == 0)
uint8_t x_19;
x_19 = !lean_is_exclusive(x_13);
if (x_19 == 0)
{
return x_14;
return x_13;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_14, 0);
x_22 = lean_ctor_get(x_14, 1);
lean_inc(x_22);
lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_20 = lean_ctor_get(x_13, 0);
x_21 = lean_ctor_get(x_13, 1);
lean_inc(x_21);
lean_dec(x_14);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
return x_23;
lean_inc(x_20);
lean_dec(x_13);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
}
else
{
uint8_t x_24;
x_24 = !lean_is_exclusive(x_11);
if (x_24 == 0)
uint8_t x_23;
x_23 = !lean_is_exclusive(x_10);
if (x_23 == 0)
{
return x_11;
return x_10;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_11, 0);
x_26 = lean_ctor_get(x_11, 1);
lean_inc(x_26);
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_10, 0);
x_25 = lean_ctor_get(x_10, 1);
lean_inc(x_25);
lean_dec(x_11);
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
return x_27;
lean_inc(x_24);
lean_dec(x_10);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
}

958
stage0/stdlib/Lean/Environment.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -7218,7 +7218,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_Lean_isLevelMVarAssignable___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___spec__4___closed__1;
x_2 = l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___spec__4___closed__2;
x_3 = lean_unsigned_to_nat(412u);
x_3 = lean_unsigned_to_nat(426u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___spec__4___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

2
stage0/stdlib/Lean/Meta/LevelDefEq.c generated
View file

@ -2583,7 +2583,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_Lean_isLevelMVarAssignable___at_Lean_Meta_isLevelDefEqAuxImpl___spec__2___closed__1;
x_2 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_isLevelDefEqAuxImpl___spec__2___closed__2;
x_3 = lean_unsigned_to_nat(412u);
x_3 = lean_unsigned_to_nat(426u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_isLevelMVarAssignable___at_Lean_Meta_isLevelDefEqAuxImpl___spec__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

562
stage0/stdlib/Lean/Meta/Tactic/LinearArith/Solver.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c generated
View file

@ -9305,7 +9305,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_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__5___closed__1;
x_2 = l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__5___closed__2;
x_3 = lean_unsigned_to_nat(412u);
x_3 = lean_unsigned_to_nat(426u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_isLevelMVarAssignable___at___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___spec__5___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);

235
stage0/stdlib/Lean/MetavarContext.c generated
View file

@ -44,7 +44,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateMVarsCore__
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateMVarsCore___spec__11___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__34___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isLevelMVarAssignable___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MetavarContext_instInhabited;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__28___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_find_x3f___at_Lean_MetavarContext_getDecl___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -675,6 +674,7 @@ static lean_object* l_Lean_MetavarContext_MkBinding_instMonadHashMapCacheAdapter
LEAN_EXPORT lean_object* l_Lean_instantiateMVars___at___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___spec__7(lean_object*, lean_object*);
lean_object* l_Array_feraseIdx___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MetavarContext_addExprMVarDeclExp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t);
LEAN_EXPORT lean_object* lean_assign_lmvar(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentArray_0__Lean_PersistentArray_foldlFromMAux___at_Lean_instantiateLCtxMVars___spec__3___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_PersistentArray_anyM___at_Lean_exprDependsOn_x27___spec__14(lean_object*, lean_object*);
lean_object* lean_nat_to_int(lean_object*);
@ -785,6 +785,7 @@ LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_MetavarContext_MkBinding_co
LEAN_EXPORT lean_object* l_panic___at_Lean_isLevelMVarAssignable___spec__4___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_indexOfAux___at_Lean_MetavarContext_setMVarUserName___spec__3___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__16___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_instantiate_level_mvars(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at_Lean_getLevelMVarAssignment_x3f___spec__2___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___at_Lean_MetavarContext_LevelMVarToParam_visitLevel___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MVarId_assign___at_Lean_instantiateMVarsCore___spec__4(lean_object*);
@ -1044,6 +1045,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars__
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateMVarsCore___spec__16(lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__89(lean_object*, lean_object*, size_t, size_t);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_reprMetavarKind____x40_Lean_MetavarContext___hyg_123____boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_assign_mvar(lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_lower_loose_bvars(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_MetavarContext_MkBinding_instToStringException___spec__1___closed__1;
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_MVarId_assign___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1268,6 +1270,7 @@ LEAN_EXPORT lean_object* l_List_anyM___at_Lean_hasAssignableMVar___spec__1___rar
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__41___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentArray_anyMAux___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__95___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__38___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_get_lmvar_assignment(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__24(lean_object*, lean_object*, size_t, size_t);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_MetavarContext_0__Lean_MetavarContext_MkBinding_elimApp___spec__15___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visit___at_Lean_localDeclDependsOn_x27___spec__7___boxed(lean_object*, lean_object*, lean_object*);
@ -1282,6 +1285,7 @@ LEAN_EXPORT lean_object* l_Lean_MVarId_setFVarBinderInfo___rarg___lambda__1(lean
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___at_Lean_localDeclDependsOn_x27___spec__60___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_mk_metavar_ctx(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__27___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*);
static lean_object* l_Lean_instInhabitedMetavarContext___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__43___rarg(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MetavarContext_findLevelDepth_x3f___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MetavarContext_getExprAssignmentDomain___boxed(lean_object*);
@ -1343,6 +1347,7 @@ LEAN_EXPORT lean_object* l_Lean_Expr_withAppAux___at_Lean_instantiateExprMVars__
LEAN_EXPORT lean_object* l_List_mapM_loop___at_Lean_instantiateMVarsCore___spec__9___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_findExprDependsOn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux___at_Lean_MVarId_assign___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instInhabitedMetavarContext;
LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentArray_0__Lean_PersistentArray_foldlMAux___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__55___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MetavarContext_levelAssignDepth___default;
static lean_object* l_Lean_instInhabitedMetavarDecl___closed__8;
@ -1522,6 +1527,7 @@ static lean_object* l_Lean_MetavarContext_LevelMVarToParam_instMonadMCtxM___clos
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitApp___at_Lean_localDeclDependsOn_x27___spec__9(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__29___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_reverse___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_instantiateExprMVarsImp___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__26(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_localDeclDependsOn_x27___spec__24___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instantiateMVarDeclMVars___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1688,11 +1694,13 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars__
LEAN_EXPORT lean_object* l___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visit___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__75___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
lean_object* lean_instantiate_expr_mvars(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_localDeclDependsOn___spec__30(lean_object*, lean_object*, size_t, size_t);
static lean_object* l_Lean_MetavarContext_getExprAssignmentDomain___closed__1;
LEAN_EXPORT lean_object* l_Lean_MVarId_modifyDecl(lean_object*);
LEAN_EXPORT lean_object* l_Lean_assignLevelMVar___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__42___rarg(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_get_mvar_assignment(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_MVarId_modifyLCtx(lean_object*);
LEAN_EXPORT lean_object* l_ReaderT_bind___at_Lean_MetavarContext_LevelMVarToParam_instMonadMCtxM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__96___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1722,6 +1730,7 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars__
uint8_t l___private_Lean_Expr_0__Lean_beqBinderInfo____x40_Lean_Expr___hyg_404_(uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAux___at_Lean_MetavarContext_findUserName_x3f___spec__2(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PersistentArray_anyM___at_Lean_localDeclDependsOn___spec__36___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instantiateLevelMVarsImp___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__21___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getExprMVarAssignment_x3f___at___private_Lean_MetavarContext_0__Lean_DependsOn_dep_visitMain___spec__1(lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_PersistentArray_anyMAux___at_Lean_exprDependsOn_x27___spec__5(lean_object*);
@ -1730,6 +1739,7 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insert___at_Lean_MetavarContex
LEAN_EXPORT lean_object* l_Lean_MetavarContext_lDepth___default;
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__36___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_get_delayed_mvar_assignment(lean_object*, lean_object*);
lean_object* l_Lean_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Array_anyMUnsafe_any___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__106___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_panic___at_Lean_isLevelMVarAssignable___spec__4(lean_object*);
@ -1807,7 +1817,6 @@ LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars__
LEAN_EXPORT lean_object* l_Lean_MetavarContext_MkBinding_instMonadMCtxM___lambda__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__38___rarg(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_PersistentArray_anyM___at_Lean_MetavarContext_MkBinding_collectForwardDeps___spec__78(lean_object*, lean_object*);
static lean_object* l_Lean_MetavarContext_instInhabited___closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_instantiateExprMVars___spec__30___rarg___lambda__1(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_getExprMVarAssignment_x3f___at_Lean_instantiateExprMVars___spec__9___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_MetavarContext_MkBinding_instToStringException___closed__4;
@ -2640,6 +2649,33 @@ x_1 = l_Lean_instInhabitedMetavarDecl___closed__2;
return x_1;
}
}
static lean_object* _init_l_Lean_instInhabitedMetavarContext___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Lean_instInhabitedMetavarDecl___closed__2;
x_3 = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_1);
lean_ctor_set(x_3, 3, x_2);
lean_ctor_set(x_3, 4, x_2);
lean_ctor_set(x_3, 5, x_2);
lean_ctor_set(x_3, 6, x_2);
lean_ctor_set(x_3, 7, x_2);
lean_ctor_set(x_3, 8, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_instInhabitedMetavarContext() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_instInhabitedMetavarContext___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_StateT_get___at_Lean_instMonadMCtxStateMMetavarContext___spec__1(lean_object* x_1) {
_start:
{
@ -3070,6 +3106,18 @@ lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* lean_get_lmvar_assignment(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 6);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_PersistentHashMap_find_x3f___at_Lean_getLevelMVarAssignment_x3f___spec__1(x_3, x_2);
lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_findAtAux___at_Lean_MetavarContext_getExprAssignmentCore_x3f___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
@ -3315,6 +3363,18 @@ lean_dec(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* lean_get_mvar_assignment(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 7);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_PersistentHashMap_find_x3f___at_Lean_MetavarContext_getExprAssignmentCore_x3f___spec__1(x_3, x_2);
lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_getExprMVarAssignment_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -3608,6 +3668,18 @@ lean_dec(x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* lean_get_delayed_mvar_assignment(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 8);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_PersistentHashMap_find_x3f___at_Lean_MetavarContext_getDelayedMVarAssignmentCore_x3f___spec__1(x_3, x_2);
lean_dec(x_2);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_getDelayedMVarAssignment_x3f___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -4621,7 +4693,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_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__1;
x_2 = l_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__2;
x_3 = lean_unsigned_to_nat(412u);
x_3 = lean_unsigned_to_nat(426u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -4956,7 +5028,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_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__1;
x_2 = l_Lean_MetavarContext_getDecl___closed__1;
x_3 = lean_unsigned_to_nat(417u);
x_3 = lean_unsigned_to_nat(431u);
x_4 = lean_unsigned_to_nat(17u);
x_5 = l_Lean_MetavarContext_getDecl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -7129,6 +7201,56 @@ x_8 = l_Lean_PersistentHashMap_insertAux___at_Lean_assignLevelMVar___spec__2(x_1
return x_8;
}
}
LEAN_EXPORT lean_object* lean_assign_lmvar(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_1);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_1, 6);
x_6 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_5, x_2, x_3);
lean_ctor_set(x_1, 6, x_6);
return x_1;
}
else
{
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; lean_object* x_16; lean_object* x_17;
x_7 = lean_ctor_get(x_1, 0);
x_8 = lean_ctor_get(x_1, 1);
x_9 = lean_ctor_get(x_1, 2);
x_10 = lean_ctor_get(x_1, 3);
x_11 = lean_ctor_get(x_1, 4);
x_12 = lean_ctor_get(x_1, 5);
x_13 = lean_ctor_get(x_1, 6);
x_14 = lean_ctor_get(x_1, 7);
x_15 = lean_ctor_get(x_1, 8);
lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_1);
x_16 = l_Lean_PersistentHashMap_insert___at_Lean_assignLevelMVar___spec__1(x_13, x_2, x_3);
x_17 = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(x_17, 0, x_7);
lean_ctor_set(x_17, 1, x_8);
lean_ctor_set(x_17, 2, x_9);
lean_ctor_set(x_17, 3, x_10);
lean_ctor_set(x_17, 4, x_11);
lean_ctor_set(x_17, 5, x_12);
lean_ctor_set(x_17, 6, x_16);
lean_ctor_set(x_17, 7, x_14);
lean_ctor_set(x_17, 8, x_15);
return x_17;
}
}
}
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux_traverse___at_Lean_MVarId_assign___spec__3(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -7727,6 +7849,56 @@ x_8 = l_Lean_PersistentHashMap_insertAux___at_Lean_MVarId_assign___spec__2(x_1,
return x_8;
}
}
LEAN_EXPORT lean_object* lean_assign_mvar(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_1);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_1, 7);
x_6 = l_Lean_PersistentHashMap_insert___at_Lean_MVarId_assign___spec__1(x_5, x_2, x_3);
lean_ctor_set(x_1, 7, x_6);
return x_1;
}
else
{
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; lean_object* x_16; lean_object* x_17;
x_7 = lean_ctor_get(x_1, 0);
x_8 = lean_ctor_get(x_1, 1);
x_9 = lean_ctor_get(x_1, 2);
x_10 = lean_ctor_get(x_1, 3);
x_11 = lean_ctor_get(x_1, 4);
x_12 = lean_ctor_get(x_1, 5);
x_13 = lean_ctor_get(x_1, 6);
x_14 = lean_ctor_get(x_1, 7);
x_15 = lean_ctor_get(x_1, 8);
lean_inc(x_15);
lean_inc(x_14);
lean_inc(x_13);
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
lean_dec(x_1);
x_16 = l_Lean_PersistentHashMap_insert___at_Lean_MVarId_assign___spec__1(x_14, x_2, x_3);
x_17 = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(x_17, 0, x_7);
lean_ctor_set(x_17, 1, x_8);
lean_ctor_set(x_17, 2, x_9);
lean_ctor_set(x_17, 3, x_10);
lean_ctor_set(x_17, 4, x_11);
lean_ctor_set(x_17, 5, x_12);
lean_ctor_set(x_17, 6, x_13);
lean_ctor_set(x_17, 7, x_16);
lean_ctor_set(x_17, 8, x_15);
return x_17;
}
}
}
LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAux_traverse___at_Lean_assignDelayedMVar___spec__3(size_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -8332,6 +8504,14 @@ x_8 = l_Lean_PersistentHashMap_insertAux___at_Lean_assignDelayedMVar___spec__2(x
return x_8;
}
}
LEAN_EXPORT lean_object* l_Lean_instantiateLevelMVarsImp___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_instantiate_level_mvars(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_instantiateLevelMVars___rarg___lambda__1___closed__1() {
_start:
{
@ -8863,6 +9043,14 @@ lean_dec(x_3);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_instantiateExprMVarsImp___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_instantiate_expr_mvars(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_AssocList_find_x3f___at_Lean_instantiateExprMVars___spec__2(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -48935,39 +49123,12 @@ x_2 = lean_alloc_closure((void*)(l_Lean_localDeclDependsOnPred___rarg), 5, 0);
return x_2;
}
}
static lean_object* _init_l_Lean_MetavarContext_instInhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Lean_instInhabitedMetavarDecl___closed__2;
x_3 = lean_alloc_ctor(0, 9, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_1);
lean_ctor_set(x_3, 2, x_1);
lean_ctor_set(x_3, 3, x_2);
lean_ctor_set(x_3, 4, x_2);
lean_ctor_set(x_3, 5, x_2);
lean_ctor_set(x_3, 6, x_2);
lean_ctor_set(x_3, 7, x_2);
lean_ctor_set(x_3, 8, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_MetavarContext_instInhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_MetavarContext_instInhabited___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* lean_mk_metavar_ctx(lean_object* x_1) {
_start:
{
lean_object* x_2;
lean_dec(x_1);
x_2 = l_Lean_MetavarContext_instInhabited___closed__1;
x_2 = l_Lean_instInhabitedMetavarContext___closed__1;
return x_2;
}
}
@ -51738,7 +51899,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_Lean_isLevelMVarAssignable___rarg___lambda__1___closed__1;
x_2 = l_Lean_MetavarContext_getLevelDepth___closed__1;
x_3 = lean_unsigned_to_nat(920u);
x_3 = lean_unsigned_to_nat(946u);
x_4 = lean_unsigned_to_nat(14u);
x_5 = l_Lean_MetavarContext_getDecl___closed__2;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -78469,6 +78630,10 @@ l_Lean_MetavarContext_eAssignment___default = _init_l_Lean_MetavarContext_eAssig
lean_mark_persistent(l_Lean_MetavarContext_eAssignment___default);
l_Lean_MetavarContext_dAssignment___default = _init_l_Lean_MetavarContext_dAssignment___default();
lean_mark_persistent(l_Lean_MetavarContext_dAssignment___default);
l_Lean_instInhabitedMetavarContext___closed__1 = _init_l_Lean_instInhabitedMetavarContext___closed__1();
lean_mark_persistent(l_Lean_instInhabitedMetavarContext___closed__1);
l_Lean_instInhabitedMetavarContext = _init_l_Lean_instInhabitedMetavarContext();
lean_mark_persistent(l_Lean_instInhabitedMetavarContext);
l_Lean_instMonadMCtxStateMMetavarContext___closed__1 = _init_l_Lean_instMonadMCtxStateMMetavarContext___closed__1();
lean_mark_persistent(l_Lean_instMonadMCtxStateMMetavarContext___closed__1);
l_Lean_instMonadMCtxStateMMetavarContext___closed__2 = _init_l_Lean_instMonadMCtxStateMMetavarContext___closed__2();
@ -78583,10 +78748,6 @@ l_Lean_DependsOn_instMonadMCtxM = _init_l_Lean_DependsOn_instMonadMCtxM();
lean_mark_persistent(l_Lean_DependsOn_instMonadMCtxM);
l_Lean_findExprDependsOn___rarg___lambda__3___closed__1 = _init_l_Lean_findExprDependsOn___rarg___lambda__3___closed__1();
lean_mark_persistent(l_Lean_findExprDependsOn___rarg___lambda__3___closed__1);
l_Lean_MetavarContext_instInhabited___closed__1 = _init_l_Lean_MetavarContext_instInhabited___closed__1();
lean_mark_persistent(l_Lean_MetavarContext_instInhabited___closed__1);
l_Lean_MetavarContext_instInhabited = _init_l_Lean_MetavarContext_instInhabited();
lean_mark_persistent(l_Lean_MetavarContext_instInhabited);
l_Lean_MetavarContext_getLevelDepth___closed__1 = _init_l_Lean_MetavarContext_getLevelDepth___closed__1();
lean_mark_persistent(l_Lean_MetavarContext_getLevelDepth___closed__1);
l_Lean_MetavarContext_getLevelDepth___closed__2 = _init_l_Lean_MetavarContext_getLevelDepth___closed__2();

4
stage0/stdlib/Lean/Server/References.c generated
View file

@ -181,7 +181,7 @@ static lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_RefInfo_toLspRefInfo
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_visitM_x27___at_Lean_Server_findReferences___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_mkHashMap___at_Lean_Server_References_allRefs___spec__7___boxed(lean_object*);
lean_object* l_Lean_Name_mkStr3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_findModuleRefs(lean_object*, lean_object*, uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Lean_Server_findModuleRefs(lean_object*, lean_object*, uint8_t, uint8_t);
LEAN_EXPORT lean_object* l_Lean_Elab_InfoTree_visitM___at_Lean_Server_combineIdents_buildIdMap___spec__5(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_AssocList_foldlM___at_Lean_Server_ModuleRefs_toLspModuleRefs___spec__2(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_findReferences___spec__6___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -11776,7 +11776,7 @@ x_4 = lean_apply_2(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Server_findModuleRefs(lean_object* x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4) {
LEAN_EXPORT lean_object* l_Lean_Server_findModuleRefs(lean_object* x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;

1824
stage0/stdlib/Lean/Util/Path.c generated
View file

File diff suppressed because it is too large Load diff