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

chore(frontends/lean): delete lean_environment

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-13 13:03:14 -07:00
parent 02f90485e6
commit 99e3cdc01b
13 changed files with 604 additions and 694 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/CMakeLists.txt
View file

@ -6,5 +6,4 @@ inductive_cmds.cpp pp.cpp structure_cmd.cpp structure_instance.cpp
init_module.cpp type_util.cpp decl_attributes.cpp
prenum.cpp print_cmd.cpp elaborator.cpp
match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
brackets.cpp json.cpp typed_expr.cpp choice.cpp lean_elaborator.cpp
lean_environment.cpp)
brackets.cpp json.cpp typed_expr.cpp choice.cpp lean_elaborator.cpp)

3
src/frontends/lean/init_module.cpp
View file

@ -24,7 +24,6 @@ Author: Leonardo de Moura
#include "frontends/lean/util.h"
#include "frontends/lean/brackets.h"
#include "frontends/lean/choice.h"
#include "frontends/lean/lean_environment.h"
namespace lean {
void initialize_frontend_lean_module() {
@ -48,10 +47,8 @@ void initialize_frontend_lean_module() {
initialize_notation_cmd();
initialize_frontend_lean_util();
initialize_brackets();
initialize_lean_environment();
}
void finalize_frontend_lean_module() {
finalize_lean_environment();
finalize_brackets();
finalize_frontend_lean_util();
finalize_notation_cmd();

19
src/frontends/lean/lean_elaborator.cpp
View file

@ -27,7 +27,6 @@ Lean interface to the old elaborator/elaboration parts of the parser
#include "frontends/lean/util.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/simple_pos_info_provider.h"
#include "frontends/lean/lean_environment.h"
namespace lean {
struct resolve_names_fn : public replace_visitor {
@ -454,7 +453,7 @@ object_ref to_obj(name_generator const & ngen) {
// TODO(Sebastian): replace `string` with `message` in the new runtime
extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_arg vm_cmd, b_obj_arg vm_st) {
auto vm_e = cnstr_get(vm_st, 0);
auto env = to_environment(vm_e);
environment env(vm_e, true);
auto filename = string_to_std(vm_filename);
std::stringstream in;
auto ngen = to_name_generator(cnstr_get(vm_st, 1));
@ -530,14 +529,14 @@ extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_
}
object * args[] = {
to_lean_environment(p.env()),
to_obj(s->m_ngen).steal(),
vm_lds.steal(),
vm_eds.steal(),
cnstr_get(vm_st, 4),
cnstr_get(vm_st, 5),
cnstr_get(vm_st, 6),
cnstr_get(vm_st, 7)
p.env().get_obj_arg(),
to_obj(s->m_ngen).steal(),
vm_lds.steal(),
vm_eds.steal(),
cnstr_get(vm_st, 4),
cnstr_get(vm_st, 5),
cnstr_get(vm_st, 6),
cnstr_get(vm_st, 7)
};
inc(cnstr_get(vm_st, 4));
inc(cnstr_get(vm_st, 5));

65
src/frontends/lean/lean_environment.cpp
View file

@ -1,65 +0,0 @@
/*
Copyright (c) 2018 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
Lean interface to the kernel environment type and extensions
*/
#include <string>
#include <iostream>
#include "library/replace_visitor.h"
#include "library/placeholder.h"
#include "library/explicit.h"
#include "library/annotation.h"
#include "util/timeit.h"
#include "library/locals.h"
#include "library/trace.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/definition_cmds.h"
#include "frontends/lean/brackets.h"
#include "frontends/lean/choice.h"
#include "frontends/lean/inductive_cmds.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/util.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/simple_pos_info_provider.h"
namespace lean {
void env_finalizer(void * env) {
delete static_cast<environment*>(env);
}
void env_foreach(void * /* env */, b_obj_arg /* fn */) {
// TODO(leo, kha)
throw exception("unimplemented: sharing `environment` across threads");
}
static external_object_class * g_env_class = nullptr;
environment const & to_environment(b_obj_arg o) {
lean_assert(external_class(o) == g_env_class);
return *static_cast<environment *>(external_data(o));
}
obj_res to_lean_environment(environment const & env) {
return alloc_external(g_env_class, new environment(env));
}
extern "C" obj_res lean_environment_mk_empty(b_obj_arg) {
return to_lean_environment(environment());
}
extern "C" uint8 lean_environment_contains(b_obj_arg lean_environment, b_obj_arg vm_n) {
return static_cast<uint8>(static_cast<bool>(to_environment(lean_environment).find(name(vm_n, true))));
}
void initialize_lean_environment() {
g_env_class = register_external_object_class(env_finalizer, env_foreach);
}
void finalize_lean_environment() {
}
}

17
src/frontends/lean/lean_environment.h
View file

@ -1,17 +0,0 @@
/*
Copyright (c) 2018 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
Lean interface to the kernel environment type and extensions
*/
#pragma once
#include "kernel/environment.h"
namespace lean {
environment const & to_environment(b_obj_arg o);
obj_res to_lean_environment(environment const & env);
void initialize_lean_environment();
void finalize_lean_environment();
}

16
src/kernel/environment.cpp
View file

@ -42,11 +42,11 @@ environment::environment(unsigned trust_lvl):
}
unsigned environment::trust_lvl() const {
return environment_trust_level_core(object_ref::get());
return environment_trust_level_core(get_obj_arg());
}
bool environment::is_quot_initialized() const {
return environment_quot_init_core(object_ref::get()) != 0;
return environment_quot_init_core(get_obj_arg()) != 0;
}
void environment::mark_quot_initialized() {
@ -61,11 +61,11 @@ template<typename T> optional<T> to_optional(obj_arg o) {
}
optional<constant_info> environment::find(name const & n) const {
return to_optional<constant_info>(environment_find_core(object_ref::get(), n.get()));
return to_optional<constant_info>(environment_find_core(get_obj_arg(), n.get_obj_arg()));
}
constant_info environment::get(name const & n) const {
object * o = environment_find_core(object_ref::get(), n.get());
object * o = environment_find_core(get_obj_arg(), n.get_obj_arg());
if (is_scalar(o))
throw unknown_constant_exception(*this, n);
constant_info r(cnstr_get(o, 0), true);
@ -127,11 +127,11 @@ static void check_constant_val(environment const & env, constant_val const & v,
}
void environment::add_core(constant_info const & info) {
m_obj = environment_add_core(m_obj, info.get());
m_obj = environment_add_core(m_obj, info.get_obj_arg());
}
environment environment::add(constant_info const & info) const {
return environment(environment_add_core(object_ref::get(), info.get()));
return environment(environment_add_core(get_obj_arg(), info.get_obj_arg()));
}
environment environment::add_axiom(declaration const & d, bool check) const {
@ -275,7 +275,7 @@ unsigned environment::register_extension(environment_extension * initial) {
}
environment_extension const & environment::get_extension(unsigned id) const {
object * r = get_extension_core(object_ref::get(), box(id));
object * r = get_extension_core(get_obj_arg(), box(id));
if (is_scalar(r)) { throw exception("invalid extension id"); }
object * ext = cnstr_get(r, 0);
dec(r);
@ -283,7 +283,7 @@ environment_extension const & environment::get_extension(unsigned id) const {
}
environment environment::update(unsigned id, environment_extension * ext) const {
object * r = set_extension_core(object_ref::get(), box(id), to_object(ext));
object * r = set_extension_core(get_obj_arg(), box(id), to_object(ext));
if (is_scalar(r)) { throw exception("invalid extension id"); }
environment env(cnstr_get(r, 0), true);
dec(r);

5
src/shell/lean.cpp
View file

@ -39,7 +39,6 @@ Author: Leonardo de Moura
#include "frontends/lean/pp.h"
#include "frontends/lean/json.h"
#include "frontends/lean/util.h"
#include "frontends/lean/lean_environment.h"
#include "library/trace.h"
#include "init/init.h"
#include "frontends/lean/simple_pos_info_provider.h"
@ -506,14 +505,14 @@ int main(int argc, char ** argv) {
scope_message_log scope_log(l);
// res : estate.result io.error io.world (prod (list syntax) environment)
object_ref res { lean_process_file(mk_string(mod_fn), mk_string(contents), static_cast<uint8>(json_output),
to_lean_environment(env), io_mk_world()) };
env.get_obj_arg(), io_mk_world()) };
if (io_result_is_error(res.raw())) {
// estate.result.error _
ok = false;
} else {
// estate.result.ok (prod (list syntax) environment) io.world
ok = true;
env = to_environment(cnstr_get(io_result_get_value(res.raw()), 1));
env = environment(cnstr_get(io_result_get_value(res.raw()), 1), true);
}
} else {
message_log l;

639
src/stage0/init/lean/elaborator.cpp generated
View file

File diff suppressed because it is too large Load diff

35
src/stage0/init/lean/environment.cpp generated
View file

@ -138,6 +138,7 @@ uint8 environment_quot_init_core(obj*);
obj* l_Lean_SMap_switch___at___private_init_lean_environment_1__switch___spec__1(obj*);
extern obj* l_NonScalar_Inhabited;
obj* l_List_foldl___main___rarg(obj*, obj*, obj*);
obj* l_Lean_Environment_contains___boxed(obj*, obj*);
obj* l___private_init_lean_environment_3__isQuotInit___boxed(obj*);
obj* l_Lean_PersistentEnvExtension_addEntry___boxed(obj*, obj*);
obj* l_Lean_PersistentEnvExtension_getState___boxed(obj*, obj*);
@ -189,6 +190,7 @@ extern obj* l_Lean_Name_toString___closed__1;
namespace lean {
uint8 nat_dec_le(obj*, obj*);
}
uint8 l_Lean_Environment_contains(obj*, obj*);
namespace lean {
uint32 environment_trust_level_core(obj*);
}
@ -1939,6 +1941,39 @@ lean::dec(x_1);
return x_2;
}
}
uint8 l_Lean_Environment_contains(obj* x_0, obj* x_1) {
_start:
{
obj* x_2; obj* x_5;
x_2 = lean::cnstr_get(x_0, 1);
lean::inc(x_2);
lean::dec(x_0);
x_5 = l_Lean_SMap_find___main___at_Lean_Environment_find___spec__1(x_2, x_1);
if (lean::obj_tag(x_5) == 0)
{
uint8 x_6;
x_6 = 0;
return x_6;
}
else
{
uint8 x_8;
lean::dec(x_5);
x_8 = 1;
return x_8;
}
}
}
obj* l_Lean_Environment_contains___boxed(obj* x_0, obj* x_1) {
_start:
{
uint8 x_2; obj* x_3;
x_2 = l_Lean_Environment_contains(x_0, x_1);
x_3 = lean::box(x_2);
lean::dec(x_1);
return x_3;
}
}
obj* l_Lean_SMap_switch___at___private_init_lean_environment_1__switch___spec__1(obj* x_0) {
_start:
{

56
src/stage0/init/lean/expander.cpp generated
View file

@ -33,7 +33,6 @@ obj* l_Lean_Parser_Syntax_flipScopes___main(obj*, obj*);
obj* l_Lean_Expander_mixfixToNotationSpec___closed__5;
obj* l_Lean_Expander_coeBinderBracketedBinder___closed__1;
obj* l_Lean_Expander_expandBracketedBinder___main(obj*, obj*);
obj* l_Lean_Expander_Declaration_transform___boxed(obj*, obj*);
obj* l_DList_singleton___elambda__1___rarg(obj*, obj*);
obj* l_Lean_Parser_Syntax_mreplace___main___at_Lean_Parser_Syntax_replace___spec__1(obj*, obj*);
extern obj* l_Lean_Parser_Term_hole_HasView;
@ -63,7 +62,6 @@ obj* l_Lean_Expander_assume_transform___boxed(obj*, obj*);
extern obj* l_Lean_Parser_command_mixfix;
obj* l_Lean_Expander_paren_transform(obj*, obj*);
obj* l_Lean_Expander_mkNotationTransformer___lambda__1(obj*, obj*);
obj* l_Lean_Expander_Declaration_transform___closed__1;
extern obj* l_Lean_Parser_command_reserveMixfix_HasView;
obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__17(uint8, obj*, obj*);
obj* l_Lean_Expander_let_transform___boxed(obj*, obj*);
@ -115,6 +113,7 @@ obj* l_Lean_Expander_coeSimpleBinderBinders(obj*);
extern obj* l_Lean_Parser_command_axiom_HasView;
obj* l_Lean_Expander_paren_transform___closed__1;
obj* l_Lean_Expander_TransformM_MonadReader;
extern obj* l_Lean_Parser_command_declaration_HasView;
extern obj* l_Lean_Parser_command_variables_HasView;
obj* l_List_mfor___main___at_Lean_Expander_mkNotationTransformer___spec__4___closed__1;
obj* l_Lean_Expander_mixfixToNotationSpec___closed__6;
@ -166,6 +165,7 @@ obj* l_Lean_Expander_bindingAnnotationUpdate_Parser(obj*, obj*, obj*, obj*, obj*
obj* l_Lean_Expander_introRule_transform(obj*, obj*);
obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__18(uint8, obj*, obj*);
extern obj* l_Lean_Parser_Term_depArrow_HasView;
obj* l_Lean_Expander_declaration_transform(obj*, obj*);
obj* l_RBNode_insert___at_Lean_Expander_builtinTransformers___spec__1(obj*, obj*, obj*);
obj* l_Lean_Expander_Subtype_transform(obj*, obj*);
obj* l_Lean_Parser_Syntax_getPos(obj*);
@ -203,6 +203,8 @@ extern obj* l_Lean_Parser_Term_Subtype;
obj* l_Lean_Expander_binderIdentToIdent___main___boxed(obj*);
uint8 l_RBNode_isRed___main___rarg(obj*);
obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__3(uint8, obj*, obj*);
obj* l_Lean_Expander_declaration_transform___boxed(obj*, obj*);
obj* l_Lean_Expander_declaration_transform___closed__3;
obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__1___boxed(obj*, obj*, obj*);
obj* l_Lean_Expander_mkSimpleBinder___closed__6;
obj* l_List_mmap___main___at___private_init_lean_expander_2__expandCore___main___spec__5(obj*, obj*, obj*, obj*);
@ -210,7 +212,6 @@ obj* l_Lean_Expander_error___rarg___lambda__1___boxed(obj*, obj*, obj*, obj*, ob
extern obj* l_Lean_Parser_identUnivs;
obj* l_List_lookup___main___at_Lean_Expander_mkNotationTransformer___spec__7___boxed(obj*, obj*);
obj* l_Lean_Expander_ExpanderConfig_HasLift___boxed(obj*);
extern obj* l_Lean_Parser_command_Declaration;
extern obj* l_Lean_Parser_Term_Subtype_HasView;
obj* l_Lean_Expander_ExpanderConfig_HasLift(obj*);
obj* l_Lean_Expander_globId(obj*);
@ -250,6 +251,7 @@ obj* l_Lean_Expander_coeBindersExtBinders(obj*);
obj* l_List_map___main___at_Lean_Expander_coeMixedBindersBindersExt___spec__2___boxed(obj*);
obj* l_Lean_Expander_universes_transform(obj*, obj*);
obj* l_Lean_Expander_getOptType___main___boxed(obj*);
extern obj* l_Lean_Parser_command_declaration;
obj* l_Lean_Expander_coeBinderBracketedBinder___closed__2;
obj* l_Lean_Expander_getOptType(obj*);
extern obj* l_Lean_Parser_TermParserM_Monad;
@ -266,9 +268,9 @@ obj* l_List_map___main___at_Lean_Expander_coeMixedBindersBindersExt___spec__2___
extern obj* l_Lean_Parser_Term_anonymousConstructor_HasView;
obj* l_Lean_Expander_TransformM_MonadExcept;
obj* l_Lean_Expander_let_transform___closed__1;
obj* l_Lean_Expander_Declaration_transform___closed__2;
obj* l_Lean_Expander_mkSimpleBinder___closed__3;
obj* l_Lean_Expander_introRule_transform___boxed(obj*, obj*);
obj* l_Lean_Expander_declaration_transform___closed__2;
obj* l_Lean_Expander_error___at___private_init_lean_expander_1__popStxArg___spec__1(obj*);
obj* l_Lean_Parser_number_View_ofNat(obj*);
obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__1(uint8, obj*, obj*);
@ -280,6 +282,7 @@ obj* l_Lean_Expander_Subtype_transform___boxed(obj*, obj*);
obj* l_List_foldr___main___at_Lean_Expander_expandBinders___spec__3___boxed(obj*, obj*, obj*);
obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__11(obj*, obj*);
obj* l_List_map___main___at___private_init_lean_expander_2__expandCore___main___spec__4(obj*, obj*);
obj* l_Lean_Expander_declaration_transform___closed__1;
extern obj* l_Lean_Parser_Term_arrow_HasView;
obj* l_Lean_Expander_mkSimpleBinder___closed__7;
obj* l_ExceptT_Monad___rarg(obj*);
@ -298,9 +301,7 @@ obj* l_List_map___main___at_Lean_Expander_expandBracketedBinder___main___spec__1
obj* l_Lean_Expander_variable_transform___boxed(obj*, obj*);
obj* l_Lean_Expander_axiom_transform___boxed(obj*, obj*);
obj* l_Lean_Expander_coeIdentsBindersExt___boxed(obj*);
obj* l_Lean_Expander_Declaration_transform(obj*, obj*);
obj* l_Lean_Expander_coeMixedBindersBindersExt___rarg(obj*, obj*);
obj* l_Lean_Expander_Declaration_transform___closed__3;
obj* l_Lean_Expander_mixfix_transform(obj*, obj*);
extern obj* l_Lean_Parser_Term_pi;
obj* l_List_mmap___main___at_Lean_Expander_variables_transform___spec__1(obj*, obj*);
@ -324,7 +325,6 @@ extern obj* l_Lean_Parser_Term_match_HasView;
obj* l_RBNode_find___main___at___private_init_lean_expander_2__expandCore___main___spec__2(obj*, obj*);
obj* l_Lean_Expander_mixfixToNotationSpec(obj*, obj*, obj*);
obj* l_Lean_Parser_Substring_ofString(obj*);
extern obj* l_Lean_Parser_command_Declaration_HasView;
obj* l_Lean_Expander_mkSimpleBinder___closed__4;
obj* l_Lean_Expander_noExpansion___closed__1;
obj* l_Lean_Expander_binderIdentToIdent___main(obj*);
@ -4872,7 +4872,7 @@ obj* _init_l_Lean_Expander_mixfixToNotationSpec___closed__7() {
_start:
{
obj* x_0;
x_0 = lean::mk_string("invalid `infixr` Declaration, given precedence must greater than zero");
x_0 = lean::mk_string("invalid `infixr` declaration, given precedence must greater than zero");
return x_0;
}
}
@ -9980,7 +9980,7 @@ lean::dec(x_1);
return x_2;
}
}
obj* _init_l_Lean_Expander_Declaration_transform___closed__1() {
obj* _init_l_Lean_Expander_declaration_transform___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25;
@ -10034,7 +10034,7 @@ lean::cnstr_set(x_25, 0, x_24);
return x_25;
}
}
obj* _init_l_Lean_Expander_Declaration_transform___closed__2() {
obj* _init_l_Lean_Expander_declaration_transform___closed__2() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_6; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12;
@ -10063,7 +10063,7 @@ lean::cnstr_set(x_12, 1, x_3);
return x_12;
}
}
obj* _init_l_Lean_Expander_Declaration_transform___closed__3() {
obj* _init_l_Lean_Expander_declaration_transform___closed__3() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_6;
@ -10081,11 +10081,11 @@ lean::cnstr_set(x_6, 0, x_5);
return x_6;
}
}
obj* l_Lean_Expander_Declaration_transform(obj* x_0, obj* x_1) {
obj* l_Lean_Expander_declaration_transform(obj* x_0, obj* x_1) {
_start:
{
obj* x_2; obj* x_3; obj* x_5; obj* x_6;
x_2 = l_Lean_Parser_command_Declaration_HasView;
x_2 = l_Lean_Parser_command_declaration_HasView;
x_3 = lean::cnstr_get(x_2, 0);
lean::inc(x_3);
x_5 = lean::apply_1(x_3, x_0);
@ -10193,7 +10193,7 @@ lean::cnstr_set(x_50, 0, x_49);
if (lean::obj_tag(x_36) == 0)
{
obj* x_51; obj* x_52; obj* x_53; obj* x_54; obj* x_55; obj* x_56;
x_51 = l_Lean_Expander_Declaration_transform___closed__1;
x_51 = l_Lean_Expander_declaration_transform___closed__1;
if (lean::is_scalar(x_44)) {
x_52 = lean::alloc_cnstr(0, 5, 0);
} else {
@ -10241,7 +10241,7 @@ if (lean::is_exclusive(x_57)) {
lean::dec(x_57);
x_66 = lean::box(0);
}
x_67 = l_Lean_Expander_Declaration_transform___closed__2;
x_67 = l_Lean_Expander_declaration_transform___closed__2;
x_68 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_68, 0, x_67);
lean::cnstr_set(x_68, 1, x_62);
@ -10361,7 +10361,7 @@ if (lean::is_exclusive(x_87)) {
x_116 = lean::cnstr_get(x_2, 1);
lean::inc(x_116);
lean::dec(x_2);
x_119 = l_Lean_Expander_Declaration_transform___closed__3;
x_119 = l_Lean_Expander_declaration_transform___closed__3;
if (lean::is_scalar(x_104)) {
x_120 = lean::alloc_cnstr(0, 8, 0);
} else {
@ -10384,7 +10384,7 @@ lean::cnstr_set(x_121, 0, x_120);
if (lean::obj_tag(x_107) == 0)
{
obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127;
x_122 = l_Lean_Expander_Declaration_transform___closed__1;
x_122 = l_Lean_Expander_declaration_transform___closed__1;
if (lean::is_scalar(x_115)) {
x_123 = lean::alloc_cnstr(0, 5, 0);
} else {
@ -10428,7 +10428,7 @@ if (lean::is_exclusive(x_128)) {
lean::dec(x_128);
x_137 = lean::box(0);
}
x_138 = l_Lean_Expander_Declaration_transform___closed__2;
x_138 = l_Lean_Expander_declaration_transform___closed__2;
x_139 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_139, 0, x_138);
lean::cnstr_set(x_139, 1, x_133);
@ -10479,11 +10479,11 @@ return x_149;
}
}
}
obj* l_Lean_Expander_Declaration_transform___boxed(obj* x_0, obj* x_1) {
obj* l_Lean_Expander_declaration_transform___boxed(obj* x_0, obj* x_1) {
_start:
{
obj* x_2;
x_2 = l_Lean_Expander_Declaration_transform(x_0, x_1);
x_2 = l_Lean_Expander_declaration_transform(x_0, x_1);
lean::dec(x_1);
return x_2;
}
@ -12757,8 +12757,8 @@ x_34 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_axiom_transfo
x_35 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_35, 0, x_33);
lean::cnstr_set(x_35, 1, x_34);
x_36 = l_Lean_Parser_command_Declaration;
x_37 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_Declaration_transform___boxed), 2, 0);
x_36 = l_Lean_Parser_command_declaration;
x_37 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expander_declaration_transform___boxed), 2, 0);
x_38 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_38, 0, x_36);
lean::cnstr_set(x_38, 1, x_37);
@ -13871,12 +13871,12 @@ lean::mark_persistent(l_Lean_Expander_if_transform___closed__3);
lean::mark_persistent(l_Lean_Expander_let_transform___closed__1);
l_Lean_Expander_axiom_transform___closed__1 = _init_l_Lean_Expander_axiom_transform___closed__1();
lean::mark_persistent(l_Lean_Expander_axiom_transform___closed__1);
l_Lean_Expander_Declaration_transform___closed__1 = _init_l_Lean_Expander_Declaration_transform___closed__1();
lean::mark_persistent(l_Lean_Expander_Declaration_transform___closed__1);
l_Lean_Expander_Declaration_transform___closed__2 = _init_l_Lean_Expander_Declaration_transform___closed__2();
lean::mark_persistent(l_Lean_Expander_Declaration_transform___closed__2);
l_Lean_Expander_Declaration_transform___closed__3 = _init_l_Lean_Expander_Declaration_transform___closed__3();
lean::mark_persistent(l_Lean_Expander_Declaration_transform___closed__3);
l_Lean_Expander_declaration_transform___closed__1 = _init_l_Lean_Expander_declaration_transform___closed__1();
lean::mark_persistent(l_Lean_Expander_declaration_transform___closed__1);
l_Lean_Expander_declaration_transform___closed__2 = _init_l_Lean_Expander_declaration_transform___closed__2();
lean::mark_persistent(l_Lean_Expander_declaration_transform___closed__2);
l_Lean_Expander_declaration_transform___closed__3 = _init_l_Lean_Expander_declaration_transform___closed__3();
lean::mark_persistent(l_Lean_Expander_declaration_transform___closed__3);
l_Lean_Expander_variable_transform___closed__1 = _init_l_Lean_Expander_variable_transform___closed__1();
lean::mark_persistent(l_Lean_Expander_variable_transform___closed__1);
l_Lean_Expander_bindingAnnotationUpdate = _init_l_Lean_Expander_bindingAnnotationUpdate();

226
src/stage0/init/lean/parser/command.cpp generated
View file

@ -207,6 +207,7 @@ obj* l_Lean_Parser_command_include_HasView;
obj* l_Lean_Parser_command_boolOptionValue_HasView_x_27___lambda__1(obj*);
obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__3___boxed(obj*);
obj* l_Lean_Parser_command_variables_HasView_x_27___lambda__1(obj*);
extern obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens;
extern obj* l_Lean_Parser_noKind;
obj* l_Lean_Parser_command_setOption_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_openSpec_renaming_HasView_x_27___lambda__1___closed__3;
@ -264,8 +265,6 @@ obj* l_Lean_Parser_command_open;
obj* l_Lean_Parser_command_openSpec_renaming_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_section_HasView;
obj* l_Lean_Parser_command_namespace_Parser___closed__1;
extern obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_Declaration_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_end_HasView_x_27___lambda__1___closed__1;
obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__4___rarg___boxed(obj*, obj*);
obj* l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3(obj*, obj*, obj*, obj*);
@ -336,7 +335,6 @@ obj* l_Lean_Parser_command_attribute_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_open_HasView_x_27___lambda__1___closed__3;
obj* l_Option_toMonad___main___at_Lean_Parser_indexed___spec__2___rarg(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_optionValue_HasView;
obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_List_map___main___at_Lean_Parser_command_structBinderContent_HasView_x_27___elambda__1___spec__1(obj*);
obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__6(obj*);
obj* l_Lean_Parser_Term_binder_Parser(obj*, obj*, obj*, obj*, obj*);
@ -345,6 +343,7 @@ obj* l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Le
obj* l_Lean_Parser_command_attribute_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_commandParser_run___lambda__1___boxed(obj*, obj*, obj*);
obj* l_Lean_Parser_command_variable_HasView_x_27;
obj* l_Lean_Parser_command_declaration_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_notation_Parser(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_setOption_Parser(obj*, obj*, obj*, obj*);
extern obj* l_Lean_Parser_stringLit_HasView;
@ -361,6 +360,7 @@ extern obj* l_Lean_Parser_command_mixfix_Parser_Lean_Parser_HasTokens;
obj* l_RBNode_find___main___at_Lean_Parser_commandParser_run___spec__4(obj*);
obj* l_Lean_Parser_command_setOption_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_omit_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_boolOptionValue_HasView;
extern obj* l_Lean_Parser_Combinators_many___rarg___closed__1;
obj* l_Lean_Parser_command_Parser_Lean_Parser_HasTokens;
@ -4130,7 +4130,7 @@ lean::inc(x_28);
x_31 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_31, 0, x_28);
lean::cnstr_set(x_31, 1, x_14);
x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_32, 0, x_31);
lean::inc(x_12);
x_34 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_many___at_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens___spec__2), 5, 1);
@ -4180,7 +4180,7 @@ lean::inc(x_28);
x_57 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_57, 0, x_28);
lean::cnstr_set(x_57, 1, x_55);
x_58 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_58 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_58, 0, x_57);
x_59 = lean::mk_string("->");
x_60 = l_String_trim(x_59);
@ -4435,7 +4435,7 @@ lean::inc(x_24);
x_27 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_27, 0, x_24);
lean::cnstr_set(x_27, 1, x_10);
x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_28, 0, x_27);
lean::inc(x_8);
x_30 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_many___at_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens___spec__2), 5, 1);
@ -4485,7 +4485,7 @@ lean::inc(x_24);
x_53 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_53, 0, x_24);
lean::cnstr_set(x_53, 1, x_51);
x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_54 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_54, 0, x_53);
x_55 = lean::mk_string("->");
x_56 = l_String_trim(x_55);
@ -10122,7 +10122,7 @@ lean::cnstr_set(x_21, 1, x_20);
x_22 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_22, 0, x_13);
lean::cnstr_set(x_22, 1, x_21);
x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_23, 0, x_22);
x_24 = lean::mk_string("[");
x_25 = l_String_trim(x_24);
@ -10227,7 +10227,7 @@ lean::cnstr_set(x_17, 1, x_16);
x_18 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_18, 0, x_9);
lean::cnstr_set(x_18, 1, x_17);
x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_19, 0, x_18);
x_20 = lean::mk_string("[");
x_21 = l_String_trim(x_20);
@ -12125,7 +12125,7 @@ return x_4;
obj* _init_l_Lean_Parser_command_setOption_Parser_Lean_Parser_HasView() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36;
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37;
x_0 = l_Lean_Parser_CommandParserM_Monad(lean::box(0));
x_1 = l_Lean_Parser_CommandParserM_MonadExcept(lean::box(0));
x_2 = l_Lean_Parser_CommandParserM_Lean_Parser_MonadParsec(lean::box(0));
@ -12141,73 +12141,75 @@ x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolCore___at
lean::closure_set(x_10, 0, x_5);
lean::closure_set(x_10, 1, x_9);
lean::closure_set(x_10, 2, x_8);
x_11 = lean::mk_string("True");
x_11 = lean::mk_string("true");
x_12 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
lean::closure_set(x_12, 0, x_11);
x_13 = lean::box(0);
lean::inc(x_12);
x_15 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_15, 0, x_12);
lean::cnstr_set(x_15, 1, x_13);
x_13 = lean::mk_string("false");
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
lean::closure_set(x_14, 0, x_13);
x_15 = lean::box(0);
x_16 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_16, 0, x_12);
lean::cnstr_set(x_16, 0, x_14);
lean::cnstr_set(x_16, 1, x_15);
x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_17, 0, x_16);
lean::closure_set(x_17, 1, x_9);
x_18 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_18, 0, x_17);
lean::cnstr_set(x_18, 1, x_13);
x_19 = l_Lean_Parser_command_boolOptionValue;
x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_20, 0, x_19);
lean::closure_set(x_20, 1, x_18);
x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
x_22 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_22, 0, x_21);
lean::cnstr_set(x_22, 1, x_13);
x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
x_24 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_24, 0, x_23);
lean::cnstr_set(x_24, 1, x_22);
x_17 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_17, 0, x_12);
lean::cnstr_set(x_17, 1, x_16);
x_18 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_18, 0, x_17);
lean::closure_set(x_18, 1, x_9);
x_19 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_19, 0, x_18);
lean::cnstr_set(x_19, 1, x_15);
x_20 = l_Lean_Parser_command_boolOptionValue;
x_21 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_21, 0, x_20);
lean::closure_set(x_21, 1, x_19);
x_22 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
x_23 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_23, 0, x_22);
lean::cnstr_set(x_23, 1, x_15);
x_24 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
x_25 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_25, 0, x_20);
lean::cnstr_set(x_25, 1, x_24);
x_26 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_26, 0, x_25);
lean::closure_set(x_26, 1, x_9);
x_27 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_27, 0, x_26);
lean::cnstr_set(x_27, 1, x_13);
x_28 = l_Lean_Parser_command_optionValue;
x_29 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_29, 0, x_28);
lean::closure_set(x_29, 1, x_27);
x_30 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_30, 0, x_29);
lean::cnstr_set(x_30, 1, x_13);
x_31 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
x_32 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_32, 0, x_31);
lean::cnstr_set(x_32, 1, x_30);
lean::cnstr_set(x_25, 0, x_24);
lean::cnstr_set(x_25, 1, x_23);
x_26 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_26, 0, x_21);
lean::cnstr_set(x_26, 1, x_25);
x_27 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_27, 0, x_26);
lean::closure_set(x_27, 1, x_9);
x_28 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_28, 0, x_27);
lean::cnstr_set(x_28, 1, x_15);
x_29 = l_Lean_Parser_command_optionValue;
x_30 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_30, 0, x_29);
lean::closure_set(x_30, 1, x_28);
x_31 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_31, 0, x_30);
lean::cnstr_set(x_31, 1, x_15);
x_32 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
x_33 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_33, 0, x_10);
lean::cnstr_set(x_33, 1, x_32);
x_34 = l_Lean_Parser_command_setOption;
x_35 = l_Lean_Parser_command_setOption_HasView;
x_36 = l_Lean_Parser_Combinators_node_view___rarg(x_0, x_1, x_2, x_3, x_34, x_33, x_35);
lean::dec(x_33);
lean::cnstr_set(x_33, 0, x_32);
lean::cnstr_set(x_33, 1, x_31);
x_34 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_34, 0, x_10);
lean::cnstr_set(x_34, 1, x_33);
x_35 = l_Lean_Parser_command_setOption;
x_36 = l_Lean_Parser_command_setOption_HasView;
x_37 = l_Lean_Parser_Combinators_node_view___rarg(x_0, x_1, x_2, x_3, x_35, x_34, x_36);
lean::dec(x_34);
lean::dec(x_3);
lean::dec(x_2);
lean::dec(x_1);
lean::dec(x_0);
return x_36;
return x_37;
}
}
obj* _init_l_Lean_Parser_command_setOption_Parser___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29;
obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_27; obj* x_28; obj* x_29; obj* x_30;
x_0 = lean::mk_string("setOption");
x_1 = l_String_trim(x_0);
lean::dec(x_0);
@ -12219,59 +12221,61 @@ x_6 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolCore___at_
lean::closure_set(x_6, 0, x_1);
lean::closure_set(x_6, 1, x_5);
lean::closure_set(x_6, 2, x_4);
x_7 = lean::mk_string("True");
x_7 = lean::mk_string("true");
x_8 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
lean::closure_set(x_8, 0, x_7);
x_9 = lean::box(0);
lean::inc(x_8);
x_11 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_11, 0, x_8);
lean::cnstr_set(x_11, 1, x_9);
x_9 = lean::mk_string("false");
x_10 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_symbolOrIdent___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__1___boxed), 5, 1);
lean::closure_set(x_10, 0, x_9);
x_11 = lean::box(0);
x_12 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_12, 0, x_8);
lean::cnstr_set(x_12, 0, x_10);
lean::cnstr_set(x_12, 1, x_11);
x_13 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_13, 0, x_12);
lean::closure_set(x_13, 1, x_5);
x_14 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_14, 0, x_13);
lean::cnstr_set(x_14, 1, x_9);
x_15 = l_Lean_Parser_command_boolOptionValue;
x_16 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_16, 0, x_15);
lean::closure_set(x_16, 1, x_14);
x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
x_18 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_18, 0, x_17);
lean::cnstr_set(x_18, 1, x_9);
x_19 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
x_20 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_20, 0, x_19);
lean::cnstr_set(x_20, 1, x_18);
x_13 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_13, 0, x_8);
lean::cnstr_set(x_13, 1, x_12);
x_14 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_14, 0, x_13);
lean::closure_set(x_14, 1, x_5);
x_15 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_15, 0, x_14);
lean::cnstr_set(x_15, 1, x_11);
x_16 = l_Lean_Parser_command_boolOptionValue;
x_17 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_17, 0, x_16);
lean::closure_set(x_17, 1, x_15);
x_18 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_number_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__3___boxed), 4, 0);
x_19 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_19, 0, x_18);
lean::cnstr_set(x_19, 1, x_11);
x_20 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_stringLit_Parser___at_Lean_Parser_command_setOption_Parser_Lean_Parser_HasTokens___spec__2___boxed), 4, 0);
x_21 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_21, 0, x_16);
lean::cnstr_set(x_21, 1, x_20);
x_22 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_22, 0, x_21);
lean::closure_set(x_22, 1, x_5);
x_23 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_23, 0, x_22);
lean::cnstr_set(x_23, 1, x_9);
x_24 = l_Lean_Parser_command_optionValue;
x_25 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_25, 0, x_24);
lean::closure_set(x_25, 1, x_23);
x_26 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_26, 0, x_25);
lean::cnstr_set(x_26, 1, x_9);
x_27 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
x_28 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_28, 0, x_27);
lean::cnstr_set(x_28, 1, x_26);
lean::cnstr_set(x_21, 0, x_20);
lean::cnstr_set(x_21, 1, x_19);
x_22 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_22, 0, x_17);
lean::cnstr_set(x_22, 1, x_21);
x_23 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_choiceAux___main___at_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens___spec__2), 6, 2);
lean::closure_set(x_23, 0, x_22);
lean::closure_set(x_23, 1, x_5);
x_24 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_24, 0, x_23);
lean::cnstr_set(x_24, 1, x_11);
x_25 = l_Lean_Parser_command_optionValue;
x_26 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_26, 0, x_25);
lean::closure_set(x_26, 1, x_24);
x_27 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_27, 0, x_26);
lean::cnstr_set(x_27, 1, x_11);
x_28 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1___boxed), 4, 0);
x_29 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_29, 0, x_6);
lean::cnstr_set(x_29, 1, x_28);
return x_29;
lean::cnstr_set(x_29, 0, x_28);
lean::cnstr_set(x_29, 1, x_27);
x_30 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_30, 0, x_6);
lean::cnstr_set(x_30, 1, x_29);
return x_30;
}
}
obj* l_Lean_Parser_command_setOption_Parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
@ -12366,7 +12370,7 @@ lean::dec(x_70);
x_75 = l_Lean_Parser_command_variable_Parser_Lean_Parser_HasTokens;
x_76 = l_Lean_Parser_tokenMapCons_tokens___rarg(x_75, x_73);
lean::dec(x_73);
x_78 = l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens;
x_78 = l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens;
x_79 = l_Lean_Parser_tokenMapCons_tokens___rarg(x_78, x_76);
lean::dec(x_76);
x_81 = l_Lean_Parser_tokenMapCons_tokens___rarg(x_78, x_79);
@ -12409,7 +12413,7 @@ obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_5; obj* x_6; obj* x_7; obj* x_9;
x_0 = lean::box(0);
x_1 = lean::mk_string("/--");
x_2 = lean_name_mk_string(x_0, x_1);
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser), 4, 0);
x_3 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser), 4, 0);
lean::inc(x_3);
x_5 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_5, 0, x_2);

212
src/stage0/init/lean/parser/declaration.cpp generated
View file

@ -51,14 +51,12 @@ obj* nat_sub(obj*, obj*);
}
obj* l_Lean_Parser_command_defLike_kind_HasView;
obj* l_Lean_Parser_command_equation_HasView;
obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2(obj*);
obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_declVal_HasView_x_27___lambda__1___closed__1;
obj* l___private_init_lean_parser_token_4__ident_x_27(obj*, obj*, obj*);
extern obj* l_Lean_Parser_Term_binderDefault_HasView;
obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__6;
obj* l_Lean_Parser_command_example_HasView_x_27;
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_declVal_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1___closed__3;
uint8 l_String_isEmpty(obj*);
@ -70,12 +68,12 @@ obj* l_Lean_Parser_MonadParsec_strCore___at_Lean_Parser_command_docComment_Parse
obj* l_Lean_Parser_command_univParams_HasView_x_27___lambda__1___closed__1;
extern obj* l_Lean_Parser_Combinators_choiceAux___main___rarg___closed__1;
obj* l_Lean_Parser_command_extends_HasView_x_27___lambda__1___closed__3;
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_axiom_HasView_x_27;
obj* l_Lean_Parser_command_declAttributes_HasView_x_27___lambda__1___closed__2;
extern obj* l_Lean_Parser_Term_paren_HasView_x_27___elambda__1___closed__2;
obj* l_Lean_Parser_command_oldUnivParams_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_command_simpleDeclVal;
obj* l_Lean_Parser_command_Declaration_inner;
obj* l_Lean_Parser_Combinators_sepBy1_tokens___rarg(obj*, obj*);
obj* l_Lean_Parser_command_declVal_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_Term_Parser_Lean_Parser_HasTokens(obj*);
@ -93,7 +91,6 @@ extern obj* l_Lean_Parser_finishCommentBlock___closed__2;
obj* l_Lean_Parser_termParser_run(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_declModifiers_HasView_x_27___elambda__1___closed__1;
obj* l_Lean_Parser_command_optDeclSig_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_command_Declaration_Parser___closed__1;
obj* l_Lean_Parser_command_defLike_HasView_x_27;
obj* l_Lean_Parser_command_structureFieldBlock_Parser___closed__1;
obj* l_Lean_Parser_command_structure_Parser(obj*, obj*, obj*, obj*);
@ -133,6 +130,7 @@ obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_relaxedInferModifier_HasView_x_27;
obj* l_Lean_Parser_MonadParsec_error___at___private_init_lean_parser_token_1__finishCommentBlockAux___main___spec__1___rarg(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
extern obj* l_Lean_Parser_ident_Parser___at_Lean_Parser_command_NotationSpec_foldAction_Parser_Lean_Parser_HasTokens___spec__4___rarg___closed__1;
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_constantKeyword;
obj* l_Lean_Parser_command_defLike;
obj* l_Lean_Parser_command_structExplicitBinderContent_HasView;
@ -166,6 +164,7 @@ obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasView___lambda__2(
obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_command_oldUnivParams;
obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2(obj*);
obj* l_Lean_Parser_command_axiom_HasView_x_27___elambda__2(obj*);
obj* l_Lean_Parser_command_structBinderContent_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_structExplicitBinderContent_HasView_x_27;
@ -174,12 +173,12 @@ obj* l_Lean_Parser_command_instance_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_simpleDeclVal_HasView_x_27___elambda__2___closed__1;
obj* l_Lean_Parser_command_structureCtor_HasView;
obj* l_Lean_Parser_withTrailing___at_Lean_Parser_token___spec__3(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_Declaration_HasView_x_27;
obj* l_Lean_Parser_command_visibility_HasView_x_27;
obj* l_Lean_Parser_command_declAttributes_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_instance_HasView_x_27;
obj* l_Lean_Parser_command_declModifiers_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_axiom_HasView;
obj* l_Lean_Parser_command_declaration_HasView;
obj* l_Lean_Parser_Combinators_many___at_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens___spec__2(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_declSig_Parser_Lean_Parser_HasTokens;
extern obj* l_Lean_Parser_Level_leading_HasView_x_27___elambda__1___closed__3;
@ -196,6 +195,7 @@ obj* l_Lean_Parser_command_declSig_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_Syntax_asNode___main(obj*);
obj* l_Lean_Parser_command_inferModifier_HasView;
obj* l_Lean_Parser_command_inductive_HasView;
obj* l_Lean_Parser_command_declaration_HasView_x_27;
extern obj* l_Lean_Parser_detailIdentPartEscaped_HasView_x_27___elambda__1___closed__2;
obj* l_Lean_Parser_command_attrInstance_HasView;
obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__4;
@ -216,6 +216,7 @@ obj* l_Lean_Parser_command_oldUnivParams_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_optDeclSig_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Term_Parser(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_declAttributes_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_declaration_inner_HasView;
obj* l_Lean_Parser_command_declVal_HasView_x_27;
extern obj* l_Lean_Parser_Term_binderContent_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_structureKw_HasView;
@ -243,12 +244,14 @@ obj* string_append(obj*, obj*);
obj* l_Lean_Parser_command_instImplicitBinder;
obj* l_String_OldIterator_next___main(obj*);
obj* l_Lean_Parser_command_declModifiers_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_declaration_inner;
obj* l_Lean_Parser_command_structBinderContent_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_attrInstance_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___elambda__1___closed__3;
extern obj* l___private_init_lean_parser_token_1__finishCommentBlockAux___main___closed__1;
obj* l_Lean_Parser_command_inferModifier;
obj* l_Lean_Parser_command_extends_HasView_x_27;
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27;
obj* l_Lean_Parser_command_declModifiers_HasView_x_27___elambda__1(obj*);
extern obj* l_Lean_Parser_command_notation_HasView_x_27___elambda__1___closed__1;
obj* l_Lean_Parser_command_declModifiers_HasView;
@ -262,7 +265,6 @@ obj* l_Lean_Parser_command_introRule_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_strictImplicitBinder_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_optDeclSig_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__5;
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27;
obj* l_Lean_Parser_command_structImplicitBinder_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_structBinderContent_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_strictInferModifier_HasView;
@ -271,6 +273,7 @@ extern obj* l_Char_HasRepr___closed__1;
obj* l_List_mfoldl___main___at_Lean_Parser_command_docComment_Parser___spec__3(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_introRule_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_structBinderContent_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_declModifiers_Parser___closed__1;
extern obj* l_Lean_Parser_noKind;
obj* l_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasView;
@ -320,6 +323,7 @@ obj* l_Lean_Parser_ParsecT_tryMkRes___rarg(obj*);
obj* l_Lean_Parser_command_declSig_HasView_x_27___elambda__2___closed__2;
obj* l_Lean_Parser_command_declModifiers_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_oldUnivParams_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_relaxedInferModifier_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_instance_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_introRule_HasView_x_27___lambda__1___closed__2;
@ -334,7 +338,6 @@ extern obj* l_Lean_Parser_Term_optType_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_attrInstance;
obj* l_ReaderT_lift___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__8___boxed(obj*);
obj* l_Lean_Parser_command_docComment_HasView_x_27___elambda__1___closed__1;
obj* l_Lean_Parser_command_Declaration;
obj* l_Lean_Parser_command_structExplicitBinderContent_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_structureFieldBlock_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__2;
@ -353,10 +356,8 @@ uint8 string_dec_eq(obj*, obj*);
obj* l_Lean_Parser_command_declSig_HasView_x_27___elambda__2(obj*);
obj* l_Lean_Parser_command_declSig_HasView_x_27;
obj* l_Lean_Parser_command_docComment_HasView;
obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__3;
obj* l_Lean_Parser_command_Declaration_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_structExplicitBinderContent_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_instImplicitBinder_HasView;
obj* l_Lean_Parser_command_declModifiers_HasView_x_27___lambda__1___closed__3;
@ -376,7 +377,6 @@ obj* l_Lean_Parser_command_structureFieldBlock_HasView_x_27___lambda__1___closed
obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_MonadParsec_strCore___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__2(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_inferModifier_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_Declaration_inner_HasView;
obj* l_Lean_Parser_CommandParserM_Lean_Parser_MonadParsec(obj*);
obj* l_Lean_Parser_command_declVal_Parser___closed__1;
obj* l_Lean_Parser_command_relaxedInferModifier_HasView_x_27___lambda__1___closed__1;
@ -386,6 +386,7 @@ obj* l_Lean_Parser_command_example_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_equation_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___elambda__1___closed__1;
obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___elambda__1___closed__4;
obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_docComment_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_MonadParsec_error___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__4___boxed(obj*);
obj* l_Lean_Parser_command_declVal;
@ -398,12 +399,13 @@ obj* l_String_trim(obj*);
obj* l_Lean_Parser_command_axiom_HasView_x_27___elambda__2___closed__1;
obj* l_Lean_Parser_ParsecT_bindMkRes___rarg(obj*, obj*);
obj* l_Lean_Parser_command_declModifiers;
obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1;
obj* l_Lean_Parser_command_structure_HasView;
obj* l_Lean_Parser_command_declModifiers_HasView_x_27;
extern obj* l_Lean_Parser_Term_binderDefault_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_structureFieldBlock_HasView;
extern obj* l_Lean_Parser_number_HasView_x_27___elambda__1___closed__6;
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_declaration;
obj* l_Lean_Parser_command_docComment_Parser_Lean_Parser_HasView___lambda__1___boxed(obj*, obj*, obj*, obj*, obj*);
obj* l___private_init_lean_parser_combinators_2__sepByAux___main___at_Lean_Parser_command_declAttributes_Parser_Lean_Parser_HasTokens___spec__2(obj*, obj*, uint8, uint8, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_instance;
@ -436,13 +438,13 @@ obj* l_Lean_Parser_command_constantKeyword_HasView;
obj* l_Lean_Parser_command_docComment;
obj* l_Lean_Parser_command_declVal_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_command_structExplicitBinder_HasView_x_27___lambda__1___closed__3;
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_ParsecT_lookahead___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasView___spec__1___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Combinators_sepBy1___at_Lean_Parser_command_declAttributes_Parser_Lean_Parser_HasTokens___spec__1(obj*, obj*, uint8, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_structureFieldBlock_HasView_x_27;
obj* l_Lean_Parser_MonadParsec_error___at_Lean_Parser_command_docComment_Parser_Lean_Parser_HasTokens___spec__4(obj*);
extern obj* l_Lean_Parser_number_HasView_x_27___elambda__1___closed__4;
obj* l___private_init_lean_parser_combinators_2__sepByAux___main___at_Lean_Parser_command_declAttributes_Parser_Lean_Parser_HasTokens___spec__2___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1;
obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_defLike_kind;
obj* l_Lean_Parser_command_attrInstance_HasView_x_27___elambda__1(obj*);
@ -460,8 +462,9 @@ obj* l_Lean_Parser_command_attrInstance_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_inferModifier_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_constantKeyword_HasView_x_27;
extern uint8 l_True_Decidable;
obj* l_Lean_Parser_command_declaration_Parser___closed__1;
obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2;
obj* l_Lean_Parser_ident_Parser___at_Lean_Parser_command_introRule_Parser_Lean_Parser_HasTokens___spec__1(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2;
obj* l_Lean_Parser_command_declAttributes_HasView;
obj* l_Lean_Parser_command_structImplicitBinder_HasView_x_27___lambda__1___closed__3;
obj* l_Lean_Parser_command_univParams_HasView;
@ -473,9 +476,7 @@ obj* l_Lean_Parser_command_docComment_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_docComment_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_oldUnivParams_HasView_x_27;
obj* l_Lean_Parser_command_optDeclSig_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_structureFieldBlock_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__1(obj*);
extern obj* l_Lean_Parser_Term_typeSpec_HasView;
obj* l_Lean_Parser_command_constantKeyword_HasView_x_27___lambda__1(obj*);
obj* l_List_map___main___at_Lean_Parser_command_structBinderContent_HasView_x_27___elambda__1___spec__1(obj*);
@ -490,13 +491,14 @@ obj* l_Lean_Parser_command_constantKeyword_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_defLike_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_identUnivParams_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_introRule_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_command_declaration_Parser(obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_CommandParserM_Monad(obj*);
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_structureCtor_HasView_x_27;
obj* l_Lean_Parser_command_visibility_HasView_x_27___lambda__1___closed__4;
obj* l_Lean_Parser_command_structure_HasView_x_27___lambda__1___closed__5;
obj* l_Lean_Parser_command_optDeclSig_Parser___closed__1;
obj* l_Lean_Parser_command_identUnivParams_Parser_Lean_Parser_HasTokens;
obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView;
obj* l_Lean_Parser_command_defLike_kind_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_structExplicitBinder_HasView_x_27;
obj* l_Lean_Parser_command_structureFieldBlock_HasView_x_27___lambda__1___closed__2;
@ -506,9 +508,7 @@ obj* l_Lean_Parser_command_defLike_HasView_x_27___lambda__1___closed__2;
obj* l_Lean_Parser_command_structExplicitBinderContent;
obj* l_Lean_Parser_Term_typeSpec_Parser(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_Substring_ofString(obj*);
obj* l_Lean_Parser_command_Declaration_HasView;
obj* l_Lean_Parser_command_instance_HasView;
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1(obj*);
obj* l_List_map___main___at_Lean_Parser_Term_tuple_HasView_x_27___elambda__1___spec__1(obj*);
obj* l_Lean_Parser_command_oldUnivParams_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_optDeclSig_HasView;
@ -517,6 +517,7 @@ obj* l_Lean_Parser_command_strictImplicitBinder_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_structExplicitBinder_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_visibility;
obj* l_Lean_Parser_command_structureKw_HasView_x_27___lambda__1(obj*);
obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1(obj*, obj*, obj*, obj*, obj*);
obj* l_Lean_Parser_command_inductive_HasView_x_27;
extern obj* l_Lean_Parser_Combinators_many___rarg___closed__1;
obj* l_Lean_Parser_command_example;
@ -543,7 +544,6 @@ obj* l_Lean_Parser_command_structureCtor_HasView_x_27___elambda__1(obj*);
obj* l_Lean_Parser_command_constantKeyword_HasView_x_27___lambda__1___closed__1;
obj* l_Lean_Parser_command_structExplicitBinder;
extern obj* l_String_splitAux___main___closed__1;
obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView;
namespace lean {
obj* string_length(obj*);
}
@ -26230,7 +26230,7 @@ x_0 = l_Lean_Parser_command_inductive_HasView_x_27;
return x_0;
}
}
obj* _init_l_Lean_Parser_command_Declaration_inner() {
obj* _init_l_Lean_Parser_command_declaration_inner() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10;
@ -26241,14 +26241,14 @@ x_3 = lean::mk_string("Parser");
x_4 = lean_name_mk_string(x_2, x_3);
x_5 = lean::mk_string("command");
x_6 = lean_name_mk_string(x_4, x_5);
x_7 = lean::mk_string("Declaration");
x_7 = lean::mk_string("declaration");
x_8 = lean_name_mk_string(x_6, x_7);
x_9 = lean::mk_string("inner");
x_10 = lean_name_mk_string(x_8, x_9);
return x_10;
}
}
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___elambda__1(obj* x_0) {
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___elambda__1(obj* x_0) {
_start:
{
obj* x_1;
@ -26273,7 +26273,7 @@ x_12 = l_Lean_Parser_Syntax_mkNode(x_11, x_10);
x_13 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_13, 0, x_12);
lean::cnstr_set(x_13, 1, x_1);
x_14 = l_Lean_Parser_command_Declaration_inner;
x_14 = l_Lean_Parser_command_declaration_inner;
x_15 = l_Lean_Parser_Syntax_mkNode(x_14, x_13);
return x_15;
}
@ -26296,7 +26296,7 @@ x_26 = l_Lean_Parser_Syntax_mkNode(x_25, x_24);
x_27 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_27, 0, x_26);
lean::cnstr_set(x_27, 1, x_1);
x_28 = l_Lean_Parser_command_Declaration_inner;
x_28 = l_Lean_Parser_command_declaration_inner;
x_29 = l_Lean_Parser_Syntax_mkNode(x_28, x_27);
return x_29;
}
@ -26319,7 +26319,7 @@ x_40 = l_Lean_Parser_Syntax_mkNode(x_39, x_38);
x_41 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_41, 0, x_40);
lean::cnstr_set(x_41, 1, x_1);
x_42 = l_Lean_Parser_command_Declaration_inner;
x_42 = l_Lean_Parser_command_declaration_inner;
x_43 = l_Lean_Parser_Syntax_mkNode(x_42, x_41);
return x_43;
}
@ -26342,7 +26342,7 @@ x_54 = l_Lean_Parser_Syntax_mkNode(x_53, x_52);
x_55 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_55, 0, x_54);
lean::cnstr_set(x_55, 1, x_1);
x_56 = l_Lean_Parser_command_Declaration_inner;
x_56 = l_Lean_Parser_command_declaration_inner;
x_57 = l_Lean_Parser_Syntax_mkNode(x_56, x_55);
return x_57;
}
@ -26365,7 +26365,7 @@ x_68 = l_Lean_Parser_Syntax_mkNode(x_67, x_66);
x_69 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_69, 0, x_68);
lean::cnstr_set(x_69, 1, x_1);
x_70 = l_Lean_Parser_command_Declaration_inner;
x_70 = l_Lean_Parser_command_declaration_inner;
x_71 = l_Lean_Parser_Syntax_mkNode(x_70, x_69);
return x_71;
}
@ -26388,14 +26388,14 @@ x_82 = l_Lean_Parser_Syntax_mkNode(x_81, x_80);
x_83 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_83, 0, x_82);
lean::cnstr_set(x_83, 1, x_1);
x_84 = l_Lean_Parser_command_Declaration_inner;
x_84 = l_Lean_Parser_command_declaration_inner;
x_85 = l_Lean_Parser_Syntax_mkNode(x_84, x_83);
return x_85;
}
}
}
}
obj* _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1() {
obj* _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6;
@ -26410,7 +26410,7 @@ lean::cnstr_set(x_6, 0, x_5);
return x_6;
}
}
obj* _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2() {
obj* _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10;
@ -26421,14 +26421,14 @@ x_3 = lean::mk_string("Parser");
x_4 = lean_name_mk_string(x_2, x_3);
x_5 = lean::mk_string("command");
x_6 = lean_name_mk_string(x_4, x_5);
x_7 = lean::mk_string("Declaration");
x_7 = lean::mk_string("declaration");
x_8 = lean_name_mk_string(x_6, x_7);
x_9 = lean::mk_string("inner");
x_10 = lean_name_mk_string(x_8, x_9);
return x_10;
}
}
obj* l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1(obj* x_0) {
obj* l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1(obj* x_0) {
_start:
{
obj* x_1;
@ -26436,7 +26436,7 @@ x_1 = l_Lean_Parser_Syntax_asNode___main(x_0);
if (lean::obj_tag(x_1) == 0)
{
obj* x_2;
x_2 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_2 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_2;
}
else
@ -26450,14 +26450,14 @@ lean::inc(x_6);
x_8 = lean::cnstr_get(x_3, 1);
lean::inc(x_8);
lean::dec(x_3);
x_11 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2;
x_11 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2;
x_12 = lean_name_dec_eq(x_6, x_11);
lean::dec(x_6);
if (x_12 == 0)
{
obj* x_15;
lean::dec(x_8);
x_15 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_15 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_15;
}
else
@ -26465,7 +26465,7 @@ else
if (lean::obj_tag(x_8) == 0)
{
obj* x_16;
x_16 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_16 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_16;
}
else
@ -26483,7 +26483,7 @@ x_22 = l_Lean_Parser_Syntax_asNode___main(x_19);
if (lean::obj_tag(x_22) == 0)
{
obj* x_23;
x_23 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_23 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_23;
}
else
@ -26499,7 +26499,7 @@ case 0:
{
obj* x_30;
lean::dec(x_24);
x_30 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_30 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_30;
}
case 1:
@ -26507,7 +26507,7 @@ case 1:
obj* x_33;
lean::dec(x_27);
lean::dec(x_24);
x_33 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_33 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_33;
}
default:
@ -26529,7 +26529,7 @@ if (x_43 == 0)
obj* x_47;
lean::dec(x_34);
lean::dec(x_39);
x_47 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_47 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_47;
}
else
@ -26538,7 +26538,7 @@ if (lean::obj_tag(x_34) == 0)
{
obj* x_49;
lean::dec(x_39);
x_49 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_49 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_49;
}
else
@ -26662,7 +26662,7 @@ obj* x_109;
lean::dec(x_50);
lean::dec(x_34);
lean::dec(x_39);
x_109 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_109 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_109;
}
}
@ -26676,7 +26676,7 @@ else
obj* x_112;
lean::dec(x_8);
lean::dec(x_17);
x_112 = l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1;
x_112 = l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1;
return x_112;
}
}
@ -26684,27 +26684,27 @@ return x_112;
}
}
}
obj* _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27() {
obj* _init_l_Lean_Parser_command_declaration_inner_HasView_x_27() {
_start:
{
obj* x_0; obj* x_1; obj* x_2;
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1), 1, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_inner_HasView_x_27___elambda__1), 1, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1), 1, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_inner_HasView_x_27___elambda__1), 1, 0);
x_2 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_2, 0, x_0);
lean::cnstr_set(x_2, 1, x_1);
return x_2;
}
}
obj* _init_l_Lean_Parser_command_Declaration_inner_HasView() {
obj* _init_l_Lean_Parser_command_declaration_inner_HasView() {
_start:
{
obj* x_0;
x_0 = l_Lean_Parser_command_Declaration_inner_HasView_x_27;
x_0 = l_Lean_Parser_command_declaration_inner_HasView_x_27;
return x_0;
}
}
obj* _init_l_Lean_Parser_command_Declaration() {
obj* _init_l_Lean_Parser_command_declaration() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8;
@ -26715,12 +26715,12 @@ x_3 = lean::mk_string("Parser");
x_4 = lean_name_mk_string(x_2, x_3);
x_5 = lean::mk_string("command");
x_6 = lean_name_mk_string(x_4, x_5);
x_7 = lean::mk_string("Declaration");
x_7 = lean::mk_string("declaration");
x_8 = lean_name_mk_string(x_6, x_7);
return x_8;
}
}
obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__1(obj* x_0) {
obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__1(obj* x_0) {
_start:
{
obj* x_1; obj* x_3; obj* x_6; obj* x_7; obj* x_10; obj* x_11; obj* x_12; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20;
@ -26734,7 +26734,7 @@ x_7 = lean::cnstr_get(x_6, 1);
lean::inc(x_7);
lean::dec(x_6);
x_10 = lean::apply_1(x_7, x_1);
x_11 = l_Lean_Parser_command_Declaration_inner_HasView;
x_11 = l_Lean_Parser_command_declaration_inner_HasView;
x_12 = lean::cnstr_get(x_11, 1);
lean::inc(x_12);
lean::dec(x_11);
@ -26746,12 +26746,12 @@ lean::cnstr_set(x_17, 1, x_16);
x_18 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_18, 0, x_10);
lean::cnstr_set(x_18, 1, x_17);
x_19 = l_Lean_Parser_command_Declaration;
x_19 = l_Lean_Parser_command_declaration;
x_20 = l_Lean_Parser_Syntax_mkNode(x_19, x_18);
return x_20;
}
}
obj* _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1() {
obj* _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_10; obj* x_11;
@ -26761,7 +26761,7 @@ lean::inc(x_1);
lean::dec(x_0);
x_4 = lean::box(3);
x_5 = lean::apply_1(x_1, x_4);
x_6 = l_Lean_Parser_command_Declaration_inner_HasView;
x_6 = l_Lean_Parser_command_declaration_inner_HasView;
x_7 = lean::cnstr_get(x_6, 0);
lean::inc(x_7);
lean::dec(x_6);
@ -26772,11 +26772,11 @@ lean::cnstr_set(x_11, 1, x_10);
return x_11;
}
}
obj* _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2() {
obj* _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2() {
_start:
{
obj* x_0; obj* x_1; obj* x_4; obj* x_5;
x_0 = l_Lean_Parser_command_Declaration_inner_HasView;
x_0 = l_Lean_Parser_command_declaration_inner_HasView;
x_1 = lean::cnstr_get(x_0, 0);
lean::inc(x_1);
lean::dec(x_0);
@ -26785,7 +26785,7 @@ x_5 = lean::apply_1(x_1, x_4);
return x_5;
}
}
obj* l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2(obj* x_0) {
obj* l_Lean_Parser_command_declaration_HasView_x_27___elambda__2(obj* x_0) {
_start:
{
obj* x_1;
@ -26793,7 +26793,7 @@ x_1 = l_Lean_Parser_Syntax_asNode___main(x_0);
if (lean::obj_tag(x_1) == 0)
{
obj* x_2;
x_2 = l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1;
x_2 = l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1;
return x_2;
}
else
@ -26808,7 +26808,7 @@ lean::dec(x_3);
if (lean::obj_tag(x_6) == 0)
{
obj* x_9;
x_9 = l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1;
x_9 = l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1;
return x_9;
}
else
@ -26827,7 +26827,7 @@ x_19 = lean::apply_1(x_16, x_10);
if (lean::obj_tag(x_12) == 0)
{
obj* x_20; obj* x_21;
x_20 = l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2;
x_20 = l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2;
x_21 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_21, 0, x_19);
lean::cnstr_set(x_21, 1, x_20);
@ -26839,7 +26839,7 @@ obj* x_22; obj* x_25; obj* x_26; obj* x_29; obj* x_30;
x_22 = lean::cnstr_get(x_12, 0);
lean::inc(x_22);
lean::dec(x_12);
x_25 = l_Lean_Parser_command_Declaration_inner_HasView;
x_25 = l_Lean_Parser_command_declaration_inner_HasView;
x_26 = lean::cnstr_get(x_25, 0);
lean::inc(x_26);
lean::dec(x_25);
@ -26853,27 +26853,27 @@ return x_30;
}
}
}
obj* _init_l_Lean_Parser_command_Declaration_HasView_x_27() {
obj* _init_l_Lean_Parser_command_declaration_HasView_x_27() {
_start:
{
obj* x_0; obj* x_1; obj* x_2;
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2), 1, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__1), 1, 0);
x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_HasView_x_27___elambda__2), 1, 0);
x_1 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_HasView_x_27___elambda__1), 1, 0);
x_2 = lean::alloc_cnstr(0, 2, 0);
lean::cnstr_set(x_2, 0, x_0);
lean::cnstr_set(x_2, 1, x_1);
return x_2;
}
}
obj* _init_l_Lean_Parser_command_Declaration_HasView() {
obj* _init_l_Lean_Parser_command_declaration_HasView() {
_start:
{
obj* x_0;
x_0 = l_Lean_Parser_command_Declaration_HasView_x_27;
x_0 = l_Lean_Parser_command_declaration_HasView_x_27;
return x_0;
}
}
obj* _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens() {
obj* _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_4; obj* x_5; obj* x_7; obj* x_8; obj* x_10; obj* x_11; obj* x_13; obj* x_14; obj* x_16; obj* x_17; obj* x_19; obj* x_22; obj* x_25; obj* x_28; obj* x_31; obj* x_33; obj* x_35; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_46; obj* x_48; obj* x_51; obj* x_53; obj* x_54; obj* x_56; obj* x_57; obj* x_58; obj* x_60; obj* x_62; obj* x_65; obj* x_67; obj* x_68; obj* x_70; obj* x_73; obj* x_75; obj* x_76; obj* x_78; obj* x_80; obj* x_82; obj* x_84; obj* x_86; obj* x_87; obj* x_89; obj* x_92; obj* x_94; obj* x_95; obj* x_97; obj* x_99; obj* x_100; obj* x_102; obj* x_104; obj* x_107; obj* x_109; obj* x_111; obj* x_112; obj* x_113; obj* x_115; obj* x_116; obj* x_117; obj* x_119; obj* x_122; obj* x_124; obj* x_126; obj* x_129; obj* x_132; obj* x_134; obj* x_135; obj* x_136; obj* x_139; obj* x_142; obj* x_145; obj* x_148; obj* x_151; obj* x_153; obj* x_155; obj* x_157; obj* x_159; obj* x_160; obj* x_162;
@ -27044,7 +27044,7 @@ lean::dec(x_160);
return x_162;
}
}
obj* l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
obj* l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
_start:
{
obj* x_5; obj* x_6; obj* x_7; obj* x_9; obj* x_11; obj* x_12; obj* x_13;
@ -27071,7 +27071,7 @@ lean::cnstr_set(x_13, 1, x_9);
return x_13;
}
}
obj* _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView() {
obj* _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView() {
_start:
{
obj* x_0; obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_21; obj* x_22; obj* x_23; obj* x_24; obj* x_27; obj* x_28; obj* x_29; obj* x_30; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; obj* x_42; obj* x_43; obj* x_44; obj* x_45; uint8 x_46; obj* x_47; obj* x_49; obj* x_50; obj* x_51; obj* x_52; obj* x_55; obj* x_56; obj* x_58; obj* x_60; obj* x_61; obj* x_62; obj* x_63; obj* x_64; obj* x_65; obj* x_68; obj* x_69; obj* x_72; obj* x_73; obj* x_75; obj* x_77; obj* x_78; obj* x_79; obj* x_80; obj* x_81; obj* x_82; obj* x_85; obj* x_86; obj* x_87; obj* x_88; obj* x_89; obj* x_90; obj* x_91; obj* x_94; obj* x_95; obj* x_96; obj* x_97; obj* x_98; obj* x_99; obj* x_100; obj* x_101; obj* x_103; obj* x_104; obj* x_105; obj* x_106; obj* x_107; obj* x_108; obj* x_111; obj* x_112; obj* x_114; obj* x_115; obj* x_116; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; obj* x_142; obj* x_143; obj* x_144; obj* x_145; obj* x_146; obj* x_147; obj* x_148; obj* x_149; obj* x_150; obj* x_151; obj* x_152; obj* x_153;
@ -27304,7 +27304,7 @@ lean::cnstr_set(x_121, 1, x_35);
x_122 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_122, 0, x_114);
lean::cnstr_set(x_122, 1, x_121);
x_123 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_123 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_123, 0, x_122);
x_124 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_notationLike_Parser), 5, 0);
x_125 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_termParser_run), 5, 1);
@ -27362,7 +27362,7 @@ lean::closure_set(x_144, 1, x_9);
x_145 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_145, 0, x_144);
lean::cnstr_set(x_145, 1, x_35);
x_146 = l_Lean_Parser_command_Declaration_inner;
x_146 = l_Lean_Parser_command_declaration_inner;
x_147 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_147, 0, x_146);
lean::closure_set(x_147, 1, x_145);
@ -27373,8 +27373,8 @@ x_149 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declMo
x_150 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_150, 0, x_149);
lean::cnstr_set(x_150, 1, x_148);
x_151 = l_Lean_Parser_command_Declaration;
x_152 = l_Lean_Parser_command_Declaration_HasView;
x_151 = l_Lean_Parser_command_declaration;
x_152 = l_Lean_Parser_command_declaration_HasView;
x_153 = l_Lean_Parser_Combinators_node_view___rarg(x_0, x_1, x_2, x_3, x_151, x_150, x_152);
lean::dec(x_150);
lean::dec(x_3);
@ -27384,7 +27384,7 @@ lean::dec(x_0);
return x_153;
}
}
obj* _init_l_Lean_Parser_command_Declaration_Parser___closed__1() {
obj* _init_l_Lean_Parser_command_declaration_Parser___closed__1() {
_start:
{
obj* x_0; obj* x_1; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_23; obj* x_24; obj* x_25; obj* x_26; obj* x_29; obj* x_30; obj* x_31; obj* x_32; obj* x_33; obj* x_34; obj* x_35; obj* x_36; obj* x_37; obj* x_38; obj* x_39; obj* x_40; obj* x_41; uint8 x_42; obj* x_43; obj* x_45; obj* x_46; obj* x_47; obj* x_48; obj* x_51; obj* x_52; obj* x_54; obj* x_56; obj* x_57; obj* x_58; obj* x_59; obj* x_60; obj* x_61; obj* x_64; obj* x_65; obj* x_68; obj* x_69; obj* x_71; obj* x_73; obj* x_74; obj* x_75; obj* x_76; obj* x_77; obj* x_78; obj* x_81; obj* x_82; obj* x_83; obj* x_84; obj* x_85; obj* x_86; obj* x_87; obj* x_90; obj* x_91; obj* x_92; obj* x_93; obj* x_94; obj* x_95; obj* x_96; obj* x_97; obj* x_99; obj* x_100; obj* x_101; obj* x_102; obj* x_103; obj* x_104; obj* x_107; obj* x_108; obj* x_110; obj* x_111; obj* x_112; obj* x_115; obj* x_116; obj* x_117; obj* x_118; obj* x_119; obj* x_120; obj* x_121; obj* x_122; obj* x_123; obj* x_124; obj* x_125; obj* x_126; obj* x_127; obj* x_128; obj* x_129; obj* x_130; obj* x_131; obj* x_132; obj* x_133; obj* x_134; obj* x_135; obj* x_136; obj* x_137; obj* x_138; obj* x_139; obj* x_140; obj* x_141; obj* x_142; obj* x_143; obj* x_144; obj* x_145; obj* x_146;
@ -27613,7 +27613,7 @@ lean::cnstr_set(x_117, 1, x_31);
x_118 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_118, 0, x_110);
lean::cnstr_set(x_118, 1, x_117);
x_119 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
x_119 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView___lambda__1), 5, 1);
lean::closure_set(x_119, 0, x_118);
x_120 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_command_notationLike_Parser), 5, 0);
x_121 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_termParser_run), 5, 1);
@ -27671,7 +27671,7 @@ lean::closure_set(x_140, 1, x_5);
x_141 = lean::alloc_cnstr(1, 2, 0);
lean::cnstr_set(x_141, 0, x_140);
lean::cnstr_set(x_141, 1, x_31);
x_142 = l_Lean_Parser_command_Declaration_inner;
x_142 = l_Lean_Parser_command_declaration_inner;
x_143 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2), 6, 2);
lean::closure_set(x_143, 0, x_142);
lean::closure_set(x_143, 1, x_141);
@ -27685,12 +27685,12 @@ lean::cnstr_set(x_146, 1, x_144);
return x_146;
}
}
obj* l_Lean_Parser_command_Declaration_Parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
obj* l_Lean_Parser_command_declaration_Parser(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
_start:
{
obj* x_4; obj* x_5; obj* x_6;
x_4 = l_Lean_Parser_command_Declaration;
x_5 = l_Lean_Parser_command_Declaration_Parser___closed__1;
x_4 = l_Lean_Parser_command_declaration;
x_5 = l_Lean_Parser_command_declaration_Parser___closed__1;
x_6 = l_Lean_Parser_Combinators_node___at_Lean_Parser_command_docComment_Parser___spec__2(x_4, x_5, x_0, x_1, x_2, x_3);
return x_6;
}
@ -28229,31 +28229,31 @@ lean::mark_persistent(l_Lean_Parser_command_inductive_HasView_x_27___lambda__1__
lean::mark_persistent(l_Lean_Parser_command_inductive_HasView_x_27);
l_Lean_Parser_command_inductive_HasView = _init_l_Lean_Parser_command_inductive_HasView();
lean::mark_persistent(l_Lean_Parser_command_inductive_HasView);
l_Lean_Parser_command_Declaration_inner = _init_l_Lean_Parser_command_Declaration_inner();
lean::mark_persistent(l_Lean_Parser_command_Declaration_inner);
l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1 = _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1();
lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__1);
l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2 = _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2();
lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView_x_27___lambda__1___closed__2);
l_Lean_Parser_command_Declaration_inner_HasView_x_27 = _init_l_Lean_Parser_command_Declaration_inner_HasView_x_27();
lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView_x_27);
l_Lean_Parser_command_Declaration_inner_HasView = _init_l_Lean_Parser_command_Declaration_inner_HasView();
lean::mark_persistent(l_Lean_Parser_command_Declaration_inner_HasView);
l_Lean_Parser_command_Declaration = _init_l_Lean_Parser_command_Declaration();
lean::mark_persistent(l_Lean_Parser_command_Declaration);
l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1 = _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1();
lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__1);
l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2 = _init_l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2();
lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView_x_27___elambda__2___closed__2);
l_Lean_Parser_command_Declaration_HasView_x_27 = _init_l_Lean_Parser_command_Declaration_HasView_x_27();
lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView_x_27);
l_Lean_Parser_command_Declaration_HasView = _init_l_Lean_Parser_command_Declaration_HasView();
lean::mark_persistent(l_Lean_Parser_command_Declaration_HasView);
l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens = _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens();
lean::mark_persistent(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasTokens);
l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView = _init_l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView();
lean::mark_persistent(l_Lean_Parser_command_Declaration_Parser_Lean_Parser_HasView);
l_Lean_Parser_command_Declaration_Parser___closed__1 = _init_l_Lean_Parser_command_Declaration_Parser___closed__1();
lean::mark_persistent(l_Lean_Parser_command_Declaration_Parser___closed__1);
l_Lean_Parser_command_declaration_inner = _init_l_Lean_Parser_command_declaration_inner();
lean::mark_persistent(l_Lean_Parser_command_declaration_inner);
l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1 = _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1();
lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__1);
l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2 = _init_l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2();
lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView_x_27___lambda__1___closed__2);
l_Lean_Parser_command_declaration_inner_HasView_x_27 = _init_l_Lean_Parser_command_declaration_inner_HasView_x_27();
lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView_x_27);
l_Lean_Parser_command_declaration_inner_HasView = _init_l_Lean_Parser_command_declaration_inner_HasView();
lean::mark_persistent(l_Lean_Parser_command_declaration_inner_HasView);
l_Lean_Parser_command_declaration = _init_l_Lean_Parser_command_declaration();
lean::mark_persistent(l_Lean_Parser_command_declaration);
l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1 = _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1();
lean::mark_persistent(l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__1);
l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2 = _init_l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2();
lean::mark_persistent(l_Lean_Parser_command_declaration_HasView_x_27___elambda__2___closed__2);
l_Lean_Parser_command_declaration_HasView_x_27 = _init_l_Lean_Parser_command_declaration_HasView_x_27();
lean::mark_persistent(l_Lean_Parser_command_declaration_HasView_x_27);
l_Lean_Parser_command_declaration_HasView = _init_l_Lean_Parser_command_declaration_HasView();
lean::mark_persistent(l_Lean_Parser_command_declaration_HasView);
l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens = _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens();
lean::mark_persistent(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasTokens);
l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView = _init_l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView();
lean::mark_persistent(l_Lean_Parser_command_declaration_Parser_Lean_Parser_HasView);
l_Lean_Parser_command_declaration_Parser___closed__1 = _init_l_Lean_Parser_command_declaration_Parser___closed__1();
lean::mark_persistent(l_Lean_Parser_command_declaration_Parser___closed__1);
return w;
}

2
src/util/object_ref.h
View file

@ -35,7 +35,7 @@ public:
}
object * raw() const { return m_obj; }
object * steal() { object * r = m_obj; m_obj = box(0); return r; }
object * get() const { inc(m_obj); return m_obj; }
object * get_obj_arg() const { inc(m_obj); return m_obj; }
static void swap(object_ref & a, object_ref & b) { std::swap(a.m_obj, b.m_obj); }
};