From d52558bf3517442d0eefff8134257a133c2d58ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Oct 2019 15:48:13 -0700 Subject: [PATCH] chore: update stage0 --- library/Init/Lean/Elaborator/Term.lean | 2 +- src/stage0/Init/Lean/Compiler/IR/Default.c | 11 +- src/stage0/Init/Lean/Elaborator/Term.c | 46 +- src/stage0/Init/Lean/Parser/Command.c | 56 +- src/stage0/Init/Lean/Parser/Module.c | 232 ++---- src/stage0/Init/Lean/Parser/Term.c | 853 +++++++++++++++------ src/stage0/Init/Lean/Parser/Transform.c | 44 +- src/stage0/Init/Lean/Path.c | 22 +- src/stage0/Init/Lean/Syntax.c | 22 +- src/stage0/Init/Lean/TypeClass/Synth.c | 20 +- 10 files changed, 793 insertions(+), 515 deletions(-) diff --git a/library/Init/Lean/Elaborator/Term.lean b/library/Init/Lean/Elaborator/Term.lean index 4afb2cb545..50bff27d27 100644 --- a/library/Init/Lean/Elaborator/Term.lean +++ b/library/Init/Lean/Elaborator/Term.lean @@ -44,7 +44,7 @@ elabTermAux stx expectedType false open Lean.Parser -@[builtinTermElab «list»] def elabList : TermElab := +@[builtinTermElab «listLit»] def elabListLit : TermElab := fun stx _ => do let openBkt := stx.getArg 0; let args := stx.getArg 1; diff --git a/src/stage0/Init/Lean/Compiler/IR/Default.c b/src/stage0/Init/Lean/Compiler/IR/Default.c index a048410669..fc873821ca 100644 --- a/src/stage0/Init/Lean/Compiler/IR/Default.c +++ b/src/stage0/Init/Lean/Compiler/IR/Default.c @@ -23,7 +23,6 @@ lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__1 lean_object* l_Array_mforAux___main___at_Lean_IR_checkDecls___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Decl_pushProj(lean_object*); lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__14; -lean_object* l_Array_mkArray(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__31; lean_object* l_Array_ummapAux___main___at___private_Init_Lean_Compiler_IR_Default_1__compileAux___spec__3(lean_object*, lean_object*); lean_object* l_Array_mforAux___main___at_Lean_IR_addBoxedVersionAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -51,6 +50,7 @@ lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__2 lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__4; lean_object* l_Array_ummapAux___main___at___private_Init_Lean_Compiler_IR_Default_1__compileAux___spec__1(lean_object*, lean_object*); +extern lean_object* l_Lean_mkOptionalNode___rarg___closed__1; lean_object* l_Array_mforAux___main___at_Lean_IR_addBoxedVersionAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_lt(lean_object*, lean_object*); lean_object* l_Lean_IR_inferBorrow(lean_object*, lean_object*, lean_object*); @@ -61,6 +61,7 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at___private_Init_Lean_Compiler_IR_Default_1__compileAux___spec__5(lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Compiler_IR_Default_1__compileAux___closed__19; +lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_IR_Decl_simpCase(lean_object*); lean_object* l_Lean_IR_Decl_insertResetReuse(lean_object*); @@ -5303,8 +5304,8 @@ else lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_dec(x_7); x_11 = l_Lean_IR_ExplicitBoxing_mkBoxedVersion(x_1); -x_12 = lean_unsigned_to_nat(1u); -x_13 = lean_mk_array(x_12, x_11); +x_12 = l_Lean_mkOptionalNode___rarg___closed__1; +x_13 = lean_array_push(x_12, x_11); x_14 = l_Lean_IR_explicitRC(x_13, x_2, x_4); x_15 = !lean_is_exclusive(x_14); if (x_15 == 0) @@ -5400,8 +5401,8 @@ else lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_dec(x_32); x_37 = l_Lean_IR_ExplicitBoxing_mkBoxedVersion(x_1); -x_38 = lean_unsigned_to_nat(1u); -x_39 = lean_mk_array(x_38, x_37); +x_38 = l_Lean_mkOptionalNode___rarg___closed__1; +x_39 = lean_array_push(x_38, x_37); x_40 = l_Lean_IR_explicitRC(x_39, x_2, x_34); x_41 = lean_ctor_get(x_40, 0); lean_inc(x_41); diff --git a/src/stage0/Init/Lean/Elaborator/Term.c b/src/stage0/Init/Lean/Elaborator/Term.c index 53e547ff7a..008c3cf08c 100644 --- a/src/stage0/Init/Lean/Elaborator/Term.c +++ b/src/stage0/Init/Lean/Elaborator/Term.c @@ -16,6 +16,7 @@ extern "C" { extern lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__1; lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg___closed__1; +lean_object* l___regBuiltinTermElab_Lean_Elab_elabList___closed__5; uint8_t lean_name_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Elab_elabList___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_mkExplicitBinder___rarg(lean_object*, lean_object*); @@ -42,6 +43,7 @@ lean_object* l_Lean_Elab_elabList___closed__1; lean_object* l_Array_uget(lean_object*, lean_object*, size_t, lean_object*); extern lean_object* l_PersistentHashMap_mkCollisionNode___rarg___closed__1; extern lean_object* l_Lean_Parser_Term_explicitBinder___elambda__1___closed__2; +lean_object* l___regBuiltinTermElab_Lean_Elab_elabList___closed__4; lean_object* l_Array_mkEmpty(lean_object*, lean_object*); lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_elabTermAux___main___spec__3(lean_object*, size_t, lean_object*); extern lean_object* l_Lean_termElabAttribute; @@ -52,6 +54,7 @@ lean_object* l_Lean_PersistentEnvExtension_getState___rarg(lean_object*, lean_ob lean_object* l_Lean_Elab_elabTermAux___main___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_elabArrow___closed__1; lean_object* l_PersistentHashMap_find___at_Lean_Elab_elabTermAux___main___spec__2(lean_object*, lean_object*); +extern lean_object* l_Lean_mkOptionalNode___rarg___closed__1; lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_elabTermAux___main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_elabTermAux___main___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Option_HasRepr___rarg___closed__3; @@ -62,10 +65,10 @@ lean_object* l_Lean_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object* l___regBuiltinTermElab_Lean_Elab_elabArrow(lean_object*); lean_object* l_AssocList_find___main___at_Lean_Elab_elabTermAux___main___spec__6___boxed(lean_object*, lean_object*); lean_object* lean_name_mk_string(lean_object*, lean_object*); -extern lean_object* l_Lean_Parser_Term_list___elambda__1___closed__2; lean_object* lean_nat_add(lean_object*, lean_object*); extern lean_object* l_Lean_nullKind; extern lean_object* l_Prod_HasRepr___rarg___closed__1; +extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2; lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* l_HashMapImp_find___at_Lean_Elab_elabTermAux___main___spec__5___boxed(lean_object*, lean_object*); extern size_t l_PersistentHashMap_insertAux___main___rarg___closed__2; @@ -86,7 +89,6 @@ lean_object* l_Array_get(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_elabTerm(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_SMap_find___at_Lean_Elab_elabTermAux___main___spec__1(lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__2; -extern lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; extern lean_object* l_panicWithPos___rarg___closed__2; extern lean_object* l_Lean_Syntax_asNode___rarg___closed__1; lean_object* l_Array_set(lean_object*, lean_object*, lean_object*, lean_object*); @@ -1506,7 +1508,7 @@ lean_object* _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("elabList"); +x_1 = lean_mk_string("list"); return x_1; } } @@ -1514,7 +1516,7 @@ lean_object* _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2; +x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2; x_2 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; @@ -1524,6 +1526,24 @@ lean_object* _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__3() { _start: { lean_object* x_1; +x_1 = lean_mk_string("elabList"); +return x_1; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltinTermElab_Lean_Elab_convertType___closed__2; +x_2 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__5() { +_start: +{ +lean_object* x_1; x_1 = lean_alloc_closure((void*)(l_Lean_Elab_elabList___boxed), 4, 0); return x_1; } @@ -1532,9 +1552,9 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_elabList(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__2; -x_3 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__2; -x_4 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__3; +x_2 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__2; +x_3 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__4; +x_4 = l___regBuiltinTermElab_Lean_Elab_elabList___closed__5; x_5 = l_Lean_addBuiltinTermElab(x_2, x_3, x_4, x_1); return x_5; } @@ -1599,7 +1619,7 @@ lean_object* l_Lean_Elab_mkExplicitBinder___rarg(lean_object* x_1, lean_object* _start: { lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 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; lean_object* x_18; -x_3 = l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; +x_3 = l_Lean_mkOptionalNode___rarg___closed__1; x_4 = lean_array_push(x_3, x_1); x_5 = l_Lean_nullKind; x_6 = lean_alloc_ctor(1, 2, 0); @@ -1685,7 +1705,7 @@ x_13 = lean_box(0); x_14 = lean_unsigned_to_nat(0u); x_15 = lean_array_get(x_13, x_8, x_14); x_16 = l_Lean_Elab_mkExplicitBinder___rarg(x_9, x_15); -x_17 = l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; +x_17 = l_Lean_mkOptionalNode___rarg___closed__1; x_18 = lean_array_push(x_17, x_16); x_19 = l_Lean_nullKind; lean_ctor_set(x_1, 1, x_18); @@ -1713,7 +1733,7 @@ x_29 = lean_box(0); x_30 = lean_unsigned_to_nat(0u); x_31 = lean_array_get(x_29, x_8, x_30); x_32 = l_Lean_Elab_mkExplicitBinder___rarg(x_9, x_31); -x_33 = l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; +x_33 = l_Lean_mkOptionalNode___rarg___closed__1; x_34 = lean_array_push(x_33, x_32); x_35 = l_Lean_nullKind; x_36 = lean_alloc_ctor(1, 2, 0); @@ -1758,7 +1778,7 @@ x_51 = lean_box(0); x_52 = lean_unsigned_to_nat(0u); x_53 = lean_array_get(x_51, x_48, x_52); x_54 = l_Lean_Elab_mkExplicitBinder___rarg(x_49, x_53); -x_55 = l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; +x_55 = l_Lean_mkOptionalNode___rarg___closed__1; x_56 = lean_array_push(x_55, x_54); x_57 = l_Lean_nullKind; if (lean_is_scalar(x_50)) { @@ -1868,6 +1888,10 @@ l___regBuiltinTermElab_Lean_Elab_elabList___closed__2 = _init_l___regBuiltinTerm lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabList___closed__2); l___regBuiltinTermElab_Lean_Elab_elabList___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__3(); lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabList___closed__3); +l___regBuiltinTermElab_Lean_Elab_elabList___closed__4 = _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__4(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabList___closed__4); +l___regBuiltinTermElab_Lean_Elab_elabList___closed__5 = _init_l___regBuiltinTermElab_Lean_Elab_elabList___closed__5(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_elabList___closed__5); w = l___regBuiltinTermElab_Lean_Elab_elabList(w); if (lean_io_result_is_error(w)) return w; l_Lean_Elab_mkExplicitBinder___rarg___closed__1 = _init_l_Lean_Elab_mkExplicitBinder___rarg___closed__1(); diff --git a/src/stage0/Init/Lean/Parser/Command.c b/src/stage0/Init/Lean/Parser/Command.c index 99905c331b..6a3d055fe0 100644 --- a/src/stage0/Init/Lean/Parser/Command.c +++ b/src/stage0/Init/Lean/Parser/Command.c @@ -93,7 +93,6 @@ lean_object* l_Lean_Parser_Command_declaration___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_visibility___closed__2; lean_object* l_Lean_Parser_Command_partial___elambda__1___rarg___closed__5; lean_object* l___regBuiltinParser_Lean_Parser_Command_reserve(lean_object*); -extern lean_object* l_Lean_Parser_Term_list___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_axiom___closed__3; extern lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Command_section(lean_object*); @@ -135,6 +134,7 @@ lean_object* l_Lean_Parser_Command_preterm___closed__5; lean_object* l_Lean_Parser_Command_commentBody___elambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__1; lean_object* l_Lean_Parser_Command_universe___elambda__1___rarg___closed__5; +extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3; lean_object* l_Lean_Parser_Command_partial___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_precedence___closed__2; @@ -145,8 +145,6 @@ lean_object* l_Lean_Parser_Command_exit___closed__3; lean_object* l_Lean_Parser_Command_inferMod___closed__2; lean_object* l_Lean_Parser_Command_precedence; lean_object* l_Lean_Parser_Command_openRenaming; -extern lean_object* l_Lean_Parser_Term_list___closed__4; -extern lean_object* l_Lean_Parser_Term_list___elambda__1___closed__10; lean_object* l_Lean_Parser_Command_mixfix___closed__1; lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__2; @@ -297,6 +295,7 @@ lean_object* l_Lean_Parser_Command_namespace; lean_object* l_Lean_Parser_Command_preterm___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Command_structImplicitBinder___closed__4; lean_object* l_Lean_Parser_Command_prefix___elambda__1___rarg(lean_object*, lean_object*); +extern lean_object* l_Lean_Parser_Term_listLit___closed__4; lean_object* l_Lean_Parser_Command_introRule___closed__6; lean_object* l_Lean_Parser_Command_constant___closed__5; lean_object* l_Lean_Parser_Command_postfix___elambda__1___rarg___closed__3; @@ -449,7 +448,6 @@ lean_object* l_Lean_Parser_Command_reserve; lean_object* l_Lean_Parser_Command_abbrev___closed__7; lean_object* l_Lean_Parser_Command_unsafe___elambda__1___rarg___closed__7; lean_object* l___regBuiltinParser_Lean_Parser_Command_resolve__name(lean_object*); -extern lean_object* l_Lean_Parser_Term_list___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_example___closed__2; extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Command_open___closed__3; @@ -625,6 +623,7 @@ lean_object* l_Lean_Parser_Command_docComment___elambda__1___closed__5; lean_object* l_Lean_Parser_Command_end; lean_object* l_Lean_Parser_Command_identPrec___closed__2; lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__5; +extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__4; lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_structFields___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__7; @@ -742,6 +741,7 @@ lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___rarg___closed lean_object* l_Lean_Parser_Command_classInductive___closed__5; lean_object* l_Lean_Parser_Command_extends___closed__2; lean_object* l_Lean_Parser_Command_structureTk; +extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_end___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Command_abbrev___closed__3; lean_object* l_Lean_Parser_Command_declModifiers___closed__2; @@ -1001,6 +1001,7 @@ lean_object* l_Lean_Parser_Command_identPrec; lean_object* l_Lean_Parser_Command_inductive___closed__1; extern lean_object* l_Lean_Parser_Term_matchAlt___closed__1; lean_object* l_Lean_Parser_Command_declSig___elambda__1(lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__10; lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Command_namespace___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_declValEqns___closed__2; @@ -1253,7 +1254,6 @@ lean_object* l_Lean_Parser_Command_end___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Command_open___closed__6; lean_object* l_Lean_Parser_Command_private___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_mkBuiltinParsingTablesRef(lean_object*); -extern lean_object* l_Lean_Parser_Term_list___elambda__1___closed__7; lean_object* l_Lean_Parser_Command_init__quot___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Command_prefix___closed__3; lean_object* _init_l_Lean_Parser_regBuiltinCommandParserAttr___closed__1() { @@ -2383,13 +2383,13 @@ lean_object* x_17; lean_object* x_18; uint8_t x_19; x_17 = lean_ctor_get(x_16, 1); lean_inc(x_17); lean_dec(x_16); -x_18 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_18 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_19 = lean_string_dec_eq(x_17, x_18); lean_dec(x_17); if (x_19 == 0) { lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; -x_20 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_20 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_20, x_12); x_22 = l_Lean_Parser_Command_attributes___elambda__1___closed__2; x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_5); @@ -2408,7 +2408,7 @@ else { lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_dec(x_16); -x_26 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_26 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_26, x_12); x_28 = l_Lean_Parser_Command_attributes___elambda__1___closed__2; x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_5); @@ -2419,7 +2419,7 @@ else { lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_dec(x_14); -x_30 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_30 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_30, x_12); x_32 = l_Lean_Parser_Command_attributes___elambda__1___closed__2; x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_5); @@ -2475,7 +2475,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Command_attributes___closed__2; -x_2 = l_Lean_Parser_Term_list___closed__4; +x_2 = l_Lean_Parser_Term_listLit___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -10647,13 +10647,13 @@ lean_object* x_67; lean_object* x_68; uint8_t x_69; x_67 = lean_ctor_get(x_66, 1); lean_inc(x_67); lean_dec(x_66); -x_68 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_68 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_69 = lean_string_dec_eq(x_67, x_68); lean_dec(x_67); if (x_69 == 0) { lean_object* x_70; lean_object* x_71; -x_70 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_70 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_71 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_70, x_62); x_37 = x_71; goto block_61; @@ -10669,7 +10669,7 @@ else { lean_object* x_72; lean_object* x_73; lean_dec(x_66); -x_72 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_72 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_73 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_72, x_62); x_37 = x_73; goto block_61; @@ -10679,7 +10679,7 @@ else { lean_object* x_74; lean_object* x_75; lean_dec(x_64); -x_74 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_74 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_75 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_74, x_62); x_37 = x_75; goto block_61; @@ -10717,13 +10717,13 @@ lean_object* x_15; lean_object* x_16; uint8_t x_17; x_15 = lean_ctor_get(x_14, 1); lean_inc(x_15); lean_dec(x_14); -x_16 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_16 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_17 = lean_string_dec_eq(x_15, x_16); lean_dec(x_15); if (x_17 == 0) { lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; -x_18 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_18 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_19 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_18, x_10); x_20 = l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2; x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_5); @@ -10742,7 +10742,7 @@ else { lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_dec(x_14); -x_24 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_24 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_24, x_10); x_26 = l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2; x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_5); @@ -10753,7 +10753,7 @@ else { lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_dec(x_12); -x_28 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_28 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_11, x_28, x_10); x_30 = l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2; x_31 = l_Lean_Parser_ParserState_mkNode(x_29, x_30, x_5); @@ -10878,7 +10878,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_Lean_Parser_Command_optDeclSig; x_2 = lean_ctor_get(x_1, 0); lean_inc(x_2); -x_3 = l_Lean_Parser_Term_list___closed__4; +x_3 = l_Lean_Parser_Term_listLit___closed__4; x_4 = l_Lean_Parser_andthenInfo(x_2, x_3); return x_4; } @@ -17387,13 +17387,13 @@ lean_object* x_36; lean_object* x_37; uint8_t x_38; x_36 = lean_ctor_get(x_35, 1); lean_inc(x_36); lean_dec(x_35); -x_37 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_37 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_38 = lean_string_dec_eq(x_36, x_37); lean_dec(x_36); if (x_38 == 0) { lean_object* x_39; lean_object* x_40; -x_39 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_39 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_40 = l_Lean_Parser_ParserState_mkErrorsAt(x_32, x_39, x_31); x_6 = x_40; goto block_24; @@ -17409,7 +17409,7 @@ else { lean_object* x_41; lean_object* x_42; lean_dec(x_35); -x_41 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_41 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_42 = l_Lean_Parser_ParserState_mkErrorsAt(x_32, x_41, x_31); x_6 = x_42; goto block_24; @@ -17419,7 +17419,7 @@ else { lean_object* x_43; lean_object* x_44; lean_dec(x_33); -x_43 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_43 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_44 = l_Lean_Parser_ParserState_mkErrorsAt(x_32, x_43, x_31); x_6 = x_44; goto block_24; @@ -17472,13 +17472,13 @@ lean_object* x_57; lean_object* x_58; uint8_t x_59; x_57 = lean_ctor_get(x_56, 1); lean_inc(x_57); lean_dec(x_56); -x_58 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_58 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_59 = lean_string_dec_eq(x_57, x_58); lean_dec(x_57); if (x_59 == 0) { lean_object* x_60; lean_object* x_61; -x_60 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_60 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_61 = l_Lean_Parser_ParserState_mkErrorsAt(x_53, x_60, x_52); x_25 = x_61; goto block_49; @@ -17494,7 +17494,7 @@ else { lean_object* x_62; lean_object* x_63; lean_dec(x_56); -x_62 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_62 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_63 = l_Lean_Parser_ParserState_mkErrorsAt(x_53, x_62, x_52); x_25 = x_63; goto block_49; @@ -17504,7 +17504,7 @@ else { lean_object* x_64; lean_object* x_65; lean_dec(x_54); -x_64 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_64 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_65 = l_Lean_Parser_ParserState_mkErrorsAt(x_53, x_64, x_52); x_25 = x_65; goto block_49; @@ -17675,7 +17675,7 @@ lean_object* _init_l_Lean_Parser_Command_attribute___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___closed__4; +x_1 = l_Lean_Parser_Term_listLit___closed__4; x_2 = l_Lean_Parser_ident___closed__1; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; diff --git a/src/stage0/Init/Lean/Parser/Module.c b/src/stage0/Init/Lean/Parser/Module.c index 8d92f807e2..75941ed605 100644 --- a/src/stage0/Init/Lean/Parser/Module.c +++ b/src/stage0/Init/Lean/Parser/Module.c @@ -26,7 +26,6 @@ lean_object* l_Lean_Parser_whitespace___main(lean_object*, lean_object*); lean_object* l_Lean_Format_pretty(lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_importPath___elambda__1___closed__1; -lean_object* l_Array_mkArray(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__2; lean_object* lean_test_module_parser(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*); @@ -60,7 +59,6 @@ lean_object* l_List_mfor___main___at___private_Init_Lean_Parser_Module_4__testMo extern lean_object* l_Lean_Options_empty; lean_object* l_Lean_Parser_mkParserState(lean_object*); lean_object* l___private_Init_Lean_Parser_Module_4__testModuleParserAux___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); -lean_object* l_Array_mkEmpty(lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_header___elambda__1___closed__2; lean_object* l_Lean_Parser_testModuleParser___lambda__1(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); @@ -68,7 +66,6 @@ lean_object* l_Lean_Parser_Module_header___closed__2; lean_object* l___private_Init_Lean_Parser_Module_3__consumeInput(lean_object*, lean_object*); lean_object* l_Lean_Parser_testModuleParser___closed__1; lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_header___closed__1; lean_object* l_Lean_Parser_Module_import___closed__3; lean_object* l_Lean_Parser_Module_header___elambda__1___closed__1; @@ -105,6 +102,7 @@ uint8_t l_List_isEmpty___rarg(lean_object*); extern lean_object* l_Lean_Parser_ident___closed__1; lean_object* l_Lean_Parser_Module_header___closed__6; lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI(lean_object*); +extern lean_object* l_Lean_mkSearchPathRef___closed__1; lean_object* l_IO_println___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__1(lean_object*, lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__3; @@ -112,7 +110,6 @@ lean_object* l_Lean_Parser_Module_prelude___closed__2; lean_object* l___private_Init_Lean_Parser_Module_4__testModuleParserAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_importPath___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*); -lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_parseCommand___main(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Parser_isEOI(lean_object*); lean_object* l_Lean_Parser_optionaInfo(lean_object*); @@ -148,7 +145,6 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_header___elamb lean_object* l_Lean_Parser_parseCommand(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Module_import___closed__1; lean_object* l_Lean_Parser_Module_prelude; -lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; lean_object* l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Module_import___elambda__1___closed__1; lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI___closed__2; @@ -585,68 +581,6 @@ lean_dec(x_1); return x_4; } } -lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { -_start: -{ -lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; -x_5 = lean_ctor_get(x_4, 0); -lean_inc(x_5); -x_6 = lean_array_get_size(x_5); -lean_dec(x_5); -x_7 = lean_ctor_get(x_4, 1); -lean_inc(x_7); -lean_inc(x_3); -x_8 = l_Lean_Parser_Module_importPath___elambda__1(x_2, x_3, x_4); -x_9 = lean_ctor_get(x_8, 3); -lean_inc(x_9); -if (lean_obj_tag(x_9) == 0) -{ -lean_object* x_10; uint8_t x_11; -lean_dec(x_6); -x_10 = lean_ctor_get(x_8, 1); -lean_inc(x_10); -x_11 = lean_nat_dec_eq(x_7, x_10); -lean_dec(x_10); -lean_dec(x_7); -if (x_11 == 0) -{ -x_4 = x_8; -goto _start; -} -else -{ -lean_object* x_13; lean_object* x_14; -lean_dec(x_3); -x_13 = l_Lean_Parser_manyAux___main___closed__1; -x_14 = l_Lean_Parser_ParserState_mkUnexpectedError(x_8, x_13); -return x_14; -} -} -else -{ -lean_object* x_15; uint8_t x_16; -lean_dec(x_9); -lean_dec(x_3); -x_15 = lean_ctor_get(x_8, 1); -lean_inc(x_15); -x_16 = lean_nat_dec_eq(x_7, x_15); -lean_dec(x_15); -if (x_16 == 0) -{ -lean_dec(x_7); -lean_dec(x_6); -return x_8; -} -else -{ -lean_object* x_17; -x_17 = l_Lean_Parser_ParserState_restore(x_8, x_6, x_7); -lean_dec(x_6); -return x_17; -} -} -} -} lean_object* _init_l_Lean_Parser_Module_import___elambda__1___closed__1() { _start: { @@ -717,114 +651,88 @@ return x_3; lean_object* l_Lean_Parser_Module_import___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_25; lean_object* x_26; lean_object* x_27; +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_14; lean_object* x_15; lean_object* x_16; x_4 = lean_ctor_get(x_3, 0); lean_inc(x_4); x_5 = lean_array_get_size(x_4); lean_dec(x_4); -x_25 = lean_ctor_get(x_3, 1); -lean_inc(x_25); +x_14 = lean_ctor_get(x_3, 1); +lean_inc(x_14); lean_inc(x_2); -x_26 = l_Lean_Parser_tokenFn(x_2, x_3); -x_27 = lean_ctor_get(x_26, 3); -lean_inc(x_27); -if (lean_obj_tag(x_27) == 0) +x_15 = l_Lean_Parser_tokenFn(x_2, x_3); +x_16 = lean_ctor_get(x_15, 3); +lean_inc(x_16); +if (lean_obj_tag(x_16) == 0) { -lean_object* x_28; lean_object* x_29; -x_28 = lean_ctor_get(x_26, 0); -lean_inc(x_28); -x_29 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_28); -lean_dec(x_28); -if (lean_obj_tag(x_29) == 2) +lean_object* x_17; lean_object* x_18; +x_17 = lean_ctor_get(x_15, 0); +lean_inc(x_17); +x_18 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_17); +lean_dec(x_17); +if (lean_obj_tag(x_18) == 2) { -lean_object* x_30; lean_object* x_31; uint8_t x_32; -x_30 = lean_ctor_get(x_29, 1); -lean_inc(x_30); -lean_dec(x_29); -x_31 = l_Lean_Parser_Module_import___elambda__1___closed__4; -x_32 = lean_string_dec_eq(x_30, x_31); -lean_dec(x_30); -if (x_32 == 0) +lean_object* x_19; lean_object* x_20; uint8_t x_21; +x_19 = lean_ctor_get(x_18, 1); +lean_inc(x_19); +lean_dec(x_18); +x_20 = l_Lean_Parser_Module_import___elambda__1___closed__4; +x_21 = lean_string_dec_eq(x_19, x_20); +lean_dec(x_19); +if (x_21 == 0) { -lean_object* x_33; lean_object* x_34; -x_33 = l_Lean_Parser_Module_import___elambda__1___closed__7; -x_34 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_33, x_25); -x_6 = x_34; -goto block_24; +lean_object* x_22; lean_object* x_23; +x_22 = l_Lean_Parser_Module_import___elambda__1___closed__7; +x_23 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_22, x_14); +x_6 = x_23; +goto block_13; } else { -lean_dec(x_25); -x_6 = x_26; -goto block_24; +lean_dec(x_14); +x_6 = x_15; +goto block_13; } } else { -lean_object* x_35; lean_object* x_36; -lean_dec(x_29); -x_35 = l_Lean_Parser_Module_import___elambda__1___closed__7; -x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_35, x_25); -x_6 = x_36; -goto block_24; +lean_object* x_24; lean_object* x_25; +lean_dec(x_18); +x_24 = l_Lean_Parser_Module_import___elambda__1___closed__7; +x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_24, x_14); +x_6 = x_25; +goto block_13; } } else { -lean_object* x_37; lean_object* x_38; -lean_dec(x_27); -x_37 = l_Lean_Parser_Module_import___elambda__1___closed__7; -x_38 = l_Lean_Parser_ParserState_mkErrorsAt(x_26, x_37, x_25); -x_6 = x_38; -goto block_24; +lean_object* x_26; lean_object* x_27; +lean_dec(x_16); +x_26 = l_Lean_Parser_Module_import___elambda__1___closed__7; +x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_26, x_14); +x_6 = x_27; +goto block_13; } -block_24: +block_13: { lean_object* x_7; x_7 = lean_ctor_get(x_6, 3); lean_inc(x_7); if (lean_obj_tag(x_7) == 0) { -lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; -x_8 = lean_ctor_get(x_6, 0); -lean_inc(x_8); -x_9 = lean_array_get_size(x_8); -lean_dec(x_8); -lean_inc(x_2); -x_10 = l_Lean_Parser_Module_importPath___elambda__1(x_1, x_2, x_6); -x_11 = lean_ctor_get(x_10, 3); -lean_inc(x_11); -if (lean_obj_tag(x_11) == 0) -{ -uint8_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; -x_12 = 0; -x_13 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1(x_12, x_1, x_2, x_10); -x_14 = l_Lean_nullKind; -x_15 = l_Lean_Parser_ParserState_mkNode(x_13, x_14, x_9); -x_16 = l_Lean_Parser_Module_import___elambda__1___closed__2; -x_17 = l_Lean_Parser_ParserState_mkNode(x_15, x_16, x_5); -return x_17; +lean_object* x_8; lean_object* x_9; lean_object* x_10; +x_8 = l_Lean_Parser_Module_importPath___elambda__1(x_1, x_2, x_6); +x_9 = l_Lean_Parser_Module_import___elambda__1___closed__2; +x_10 = l_Lean_Parser_ParserState_mkNode(x_8, x_9, x_5); +return x_10; } else { -lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; -lean_dec(x_11); -lean_dec(x_2); -x_18 = l_Lean_nullKind; -x_19 = l_Lean_Parser_ParserState_mkNode(x_10, x_18, x_9); -x_20 = l_Lean_Parser_Module_import___elambda__1___closed__2; -x_21 = l_Lean_Parser_ParserState_mkNode(x_19, x_20, x_5); -return x_21; -} -} -else -{ -lean_object* x_22; lean_object* x_23; +lean_object* x_11; lean_object* x_12; lean_dec(x_7); lean_dec(x_2); -x_22 = l_Lean_Parser_Module_import___elambda__1___closed__2; -x_23 = l_Lean_Parser_ParserState_mkNode(x_6, x_22, x_5); -return x_23; +x_11 = l_Lean_Parser_Module_import___elambda__1___closed__2; +x_12 = l_Lean_Parser_ParserState_mkNode(x_6, x_11, x_5); +return x_12; } } } @@ -889,17 +797,6 @@ x_1 = l_Lean_Parser_Module_import___closed__5; return x_1; } } -lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { -_start: -{ -uint8_t x_5; lean_object* x_6; -x_5 = lean_unbox(x_1); -lean_dec(x_1); -x_6 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_import___elambda__1___spec__1(x_5, x_2, x_3, x_4); -lean_dec(x_2); -return x_6; -} -} lean_object* l_Lean_Parser_Module_import___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { @@ -1510,15 +1407,6 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = lean_unsigned_to_nat(1u); -x_2 = lean_mk_empty_array_with_capacity(x_1); -return x_2; -} -} lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI(lean_object* x_1) { _start: { @@ -1534,7 +1422,7 @@ x_5 = l_String_splitAux___main___closed__1; x_6 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_6, 0, x_4); lean_ctor_set(x_6, 1, x_5); -x_7 = l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3; +x_7 = l_Lean_mkSearchPathRef___closed__1; x_8 = lean_array_push(x_7, x_6); x_9 = l___private_Init_Lean_Parser_Module_2__mkEOI___closed__2; x_10 = lean_alloc_ctor(1, 2, 0); @@ -2704,8 +2592,8 @@ lean_inc(x_15); x_16 = lean_ctor_get(x_13, 1); lean_inc(x_16); lean_dec(x_13); -x_17 = lean_unsigned_to_nat(1u); -x_18 = lean_mk_array(x_17, x_14); +x_17 = l_Lean_mkSearchPathRef___closed__1; +x_18 = lean_array_push(x_17, x_14); x_19 = l_Lean_Parser_parseFileAux___main(x_1, x_11, x_15, x_16, x_18, x_8); return x_19; } @@ -2734,8 +2622,8 @@ lean_inc(x_27); x_28 = lean_ctor_get(x_25, 1); lean_inc(x_28); lean_dec(x_25); -x_29 = lean_unsigned_to_nat(1u); -x_30 = lean_mk_array(x_29, x_26); +x_29 = l_Lean_mkSearchPathRef___closed__1; +x_30 = lean_array_push(x_29, x_26); x_31 = l_Lean_Parser_parseFileAux___main(x_1, x_23, x_27, x_28, x_30, x_22); return x_31; } @@ -2814,8 +2702,8 @@ lean_inc(x_49); x_50 = lean_ctor_get(x_47, 1); lean_inc(x_50); lean_dec(x_47); -x_51 = lean_unsigned_to_nat(1u); -x_52 = lean_mk_array(x_51, x_48); +x_51 = l_Lean_mkSearchPathRef___closed__1; +x_52 = lean_array_push(x_51, x_48); x_53 = l_Lean_Parser_parseFileAux___main(x_1, x_45, x_49, x_50, x_52, x_44); return x_53; } @@ -2988,8 +2876,6 @@ l___private_Init_Lean_Parser_Module_2__mkEOI___closed__1 = _init_l___private_Ini lean_mark_persistent(l___private_Init_Lean_Parser_Module_2__mkEOI___closed__1); l___private_Init_Lean_Parser_Module_2__mkEOI___closed__2 = _init_l___private_Init_Lean_Parser_Module_2__mkEOI___closed__2(); lean_mark_persistent(l___private_Init_Lean_Parser_Module_2__mkEOI___closed__2); -l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3 = _init_l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3(); -lean_mark_persistent(l___private_Init_Lean_Parser_Module_2__mkEOI___closed__3); l_Lean_Parser_testModuleParser___closed__1 = _init_l_Lean_Parser_testModuleParser___closed__1(); lean_mark_persistent(l_Lean_Parser_testModuleParser___closed__1); l_Lean_Parser_testModuleParser___closed__2 = _init_l_Lean_Parser_testModuleParser___closed__2(); diff --git a/src/stage0/Init/Lean/Parser/Term.c b/src/stage0/Init/Lean/Parser/Term.c index 6656c5a473..ca16b063f1 100644 --- a/src/stage0/Init/Lean/Parser/Term.c +++ b/src/stage0/Init/Lean/Parser/Term.c @@ -48,6 +48,7 @@ lean_object* l_Lean_Parser_Term_bnot___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_checkIsSort___elambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_arrow; +lean_object* l___regBuiltinParser_Lean_Parser_Term_arrayLit(lean_object*); lean_object* l_Lean_Parser_Term_structInstSource; lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__4; lean_object* l_Lean_Parser_regBuiltinTermParserAttr(lean_object*); @@ -114,7 +115,6 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__9; lean_object* l_Lean_Parser_Term_type___closed__3; lean_object* l_Lean_Parser_Term_namedArgument; lean_object* l_Lean_Parser_rawIdentFn(lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_array; lean_object* l_Lean_Parser_Term_lt___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_borrowed___elambda__1___rarg___closed__3; @@ -124,14 +124,12 @@ lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_show___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_orelse___closed__3; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_hole___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_hole___closed__4; lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_quotedName___closed__1; lean_object* l_Lean_Parser_Term_doElem___closed__1; lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__4; -lean_object* l_Lean_Parser_Term_array___closed__6; lean_object* l_Lean_Parser_Term_id___closed__3; lean_object* l_Lean_Parser_Term_doPat___closed__2; lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__18; @@ -152,6 +150,7 @@ lean_object* l_Lean_Parser_Term_hole___closed__1; lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__4; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__9; extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__9; lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_not; @@ -159,6 +158,7 @@ lean_object* l_Lean_Parser_Term_map; extern lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___closed__1; lean_object* l_Lean_Parser_Term_namedArgument___closed__2; lean_object* l_Lean_Parser_Term_beq___closed__2; +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4; lean_object* l_Lean_Parser_Term_bor___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_orelse___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__4; @@ -173,6 +173,7 @@ lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_ lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__11; lean_object* l_Lean_Parser_Term_fromTerm; +lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__3; extern lean_object* l_Lean_Parser_Level_hole___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___boxed(lean_object*); @@ -181,12 +182,12 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_add(lean_object*); lean_object* l_Lean_Parser_Term_bracketedDoSeq; lean_object* l_Lean_Parser_Term_haveAssign___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_let___closed__6; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_letEqns___closed__3; lean_object* l_Lean_Parser_Term_haveAssign___closed__5; lean_object* l_Lean_Parser_Term_char___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_prop___closed__1; lean_object* l_Lean_Parser_Term_app___closed__5; -lean_object* l_Lean_Parser_Term_array___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_instBinder___closed__4; lean_object* l_Lean_Parser_Term_subst___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_andM___elambda__1(lean_object*, lean_object*, lean_object*); @@ -205,9 +206,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_seqLeft(lean_object*); lean_object* l_Lean_Parser_Term_doId___closed__5; lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__3; -lean_object* l_Lean_Parser_Term_list___closed__4; lean_object* l_Lean_Parser_Term_mod___elambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__10; lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_anonymousCtor___closed__4; lean_object* l_Lean_Parser_Term_quotedName___elambda__1___rarg___closed__1; @@ -231,7 +230,6 @@ lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_id___closed__6; lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_pow___elambda__1___closed__1; -lean_object* l_Lean_Parser_Term_list___elambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_cdot___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_let; lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*); @@ -239,7 +237,9 @@ lean_object* l_Lean_Parser_Term_structInst___closed__5; extern lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__1; lean_object* l_Lean_Parser_Term_proj___closed__3; lean_object* l_Lean_Parser_Term_sort___elambda__1___rarg___closed__1; +lean_object* l_Lean_Parser_Term_listLit___closed__9; lean_object* l_Lean_Parser_Term_parenSpecial; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_seqLeft___closed__2; @@ -277,6 +277,7 @@ lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_anonymousCtor___closed__8; lean_object* l_Lean_Parser_Term_sort___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_subtype___closed__3; +lean_object* l_Lean_Parser_Term_arrayRef___closed__6; lean_object* l_Lean_Parser_Term_optIdent___elambda__1___boxed(lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_seq(lean_object*); lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__1; @@ -311,7 +312,6 @@ lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_app___closed__3; lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_doId___elambda__1(lean_object*); -lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_list___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_if(lean_object*); lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__8; @@ -321,6 +321,7 @@ lean_object* l_Lean_Parser_Term_proj___closed__6; lean_object* l_Lean_Parser_Term_borrowed___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_instBinder___closed__1; lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__5; +lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_sortApp___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_fun(lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_fcomp(lean_object*); @@ -344,6 +345,7 @@ lean_object* l_Lean_Parser_Term_type___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_do(lean_object*); lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_inaccessible___closed__4; +lean_object* l_Lean_Parser_Term_arrayRef___closed__2; lean_object* l_Lean_Parser_Term_heq___closed__1; lean_object* l_Lean_Parser_Term_sortApp; lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__2; @@ -361,6 +363,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_hole(lean_object*); lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_cdot(lean_object*); lean_object* l_Lean_Parser_Term_structInst___closed__8; +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__2; lean_object* l_Lean_Parser_Term_ge___closed__3; lean_object* l_Lean_Parser_Term_binderType___closed__1; lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*); @@ -368,13 +371,13 @@ lean_object* l_Lean_Parser_Term_namedArgument___closed__6; lean_object* l_Lean_Parser_Term_optType___closed__2; lean_object* l_Lean_Parser_Term_namedPattern___closed__6; lean_object* l_Lean_Parser_mkTermParserAttribute(lean_object*); -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4; lean_object* l_Lean_Parser_Term_equiv___closed__2; lean_object* l_Lean_Parser_Term_gt___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_seqLeft; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_tupleTail; lean_object* l_Lean_Parser_Term_quotedName___closed__2; +lean_object* l_Lean_Parser_Term_arrayRef; lean_object* l_Lean_Parser_Term_paren___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_proj___closed__8; lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1; @@ -396,6 +399,7 @@ lean_object* l_Lean_Parser_Term_suffices___closed__1; lean_object* l_Lean_Parser_Term_seqRight___closed__3; lean_object* l_Lean_Parser_Term_or___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_map___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_listLit___closed__5; lean_object* l_Lean_Parser_Term_sorry___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_doSeq; lean_object* l_Lean_Parser_Term_bor___closed__2; @@ -421,12 +425,14 @@ lean_object* l_Lean_Parser_Term_namedArgument___elambda__1___boxed(lean_object*) lean_object* l_Lean_Parser_Term_parenSpecial___closed__2; lean_object* l_Lean_Parser_Term_seq___closed__3; lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___rarg___closed__3; +lean_object* l_Lean_Parser_Term_arrayLit___closed__1; lean_object* l_Lean_Parser_Term_div___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_and___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_infixR(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_str___closed__2; lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_doLet___closed__1; +lean_object* l_Lean_Parser_Term_listLit___closed__4; extern lean_object* l_Lean_Parser_unicodeSymbolCheckPrecFn___closed__1; lean_object* l_Lean_Parser_Term_fcomp___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_doPat___closed__1; @@ -439,7 +445,9 @@ lean_object* l_Lean_Parser_Term_matchAlt___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_dollar___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__12; lean_object* l_Lean_Parser_Term_borrowed___elambda__1___rarg___closed__5; +lean_object* l_Lean_Parser_Term_arrayRef___closed__1; lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__2; +lean_object* l_Lean_Parser_Term_arrayRef___closed__5; lean_object* l_Lean_Parser_Term_prop___closed__4; lean_object* l_Lean_Parser_Term_sub___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_optType___closed__1; @@ -478,6 +486,7 @@ lean_object* l_Lean_Parser_Term_sub; lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_mul; lean_object* l_Lean_Parser_Term_parenSpecial___closed__1; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__6; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_structInstField___elambda__1___rarg(lean_object*, lean_object*); @@ -496,8 +505,8 @@ lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___boxed(lean_object*, lean_object* l_Lean_Parser_Term_ne; lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_quotedName___elambda__1___rarg___closed__5; -lean_object* l_Lean_Parser_Term_list___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_modN___elambda__1___closed__3; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__13; lean_object* l_Lean_Parser_Term_explicit___elambda__1(lean_object*, lean_object*, lean_object*); @@ -552,6 +561,7 @@ extern lean_object* l_Lean_Parser_Level_paren___closed__4; lean_object* l_Array_mkEmpty(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_add___closed__1; lean_object* l_Lean_Parser_Term_arrow___closed__2; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_letIdLhs___closed__3; lean_object* l_Lean_Parser_Term_doId___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_show___closed__2; @@ -628,14 +638,13 @@ lean_object* l_Lean_Parser_Term_explicitBinder___closed__8; lean_object* l_Lean_Parser_Term_if___closed__2; lean_object* l_Lean_Parser_Term_depArrow; extern lean_object* l_List_repr___rarg___closed__2; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__4; extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_have___closed__10; -lean_object* l_Lean_Parser_Term_list___closed__7; lean_object* l_Lean_Parser_Term_sorry___closed__2; lean_object* l_Lean_Parser_Term_suffices___closed__8; lean_object* l_Lean_Parser_Term_have___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Term_bor(lean_object*); +lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_char(lean_object*); lean_object* l_Lean_Parser_Term_structInstSource___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__6; @@ -646,7 +655,6 @@ lean_object* l_Lean_Parser_Term_subtype___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_structInstField___closed__4; lean_object* l_Lean_Parser_Term_forall___closed__4; lean_object* l_Lean_Parser_Term_bind___elambda__1___closed__1; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__1; extern lean_object* l_PersistentArray_Stats_toString___closed__4; lean_object* l_Lean_Parser_Term_mapConst___closed__1; lean_object* l_Lean_Parser_Term_uminus___elambda__1(lean_object*); @@ -666,21 +674,23 @@ lean_object* l_Lean_Parser_Term_fcomp; lean_object* l_Lean_Parser_Term_band___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_structInst___closed__12; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__1; +lean_object* l___regBuiltinParser_Lean_Parser_Term_arrayRef(lean_object*); lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_nomatch___elambda__1___rarg___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_seqRight(lean_object*); lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__3; lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_listLit___closed__7; lean_object* l_Lean_Parser_Term_doLet___closed__4; lean_object* l___regBuiltinParser_Lean_Parser_Term_suffices(lean_object*); lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__1; lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__2; lean_object* l_Lean_Parser_Term_parser_x21___closed__1; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_lt___closed__3; lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_leftArrow___closed__1; lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg___closed__5; -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__3; lean_object* l_Lean_Parser_Term_type___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_typeSpec___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_binderIdent; @@ -712,7 +722,6 @@ lean_object* l_Lean_Parser_Term_doPat___closed__8; lean_object* l_Lean_Parser_Term_doLet; lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___rarg___closed__1; extern lean_object* l_Lean_Parser_Level_num___elambda__1___rarg___closed__1; -lean_object* l_Lean_Parser_Term_list___closed__8; lean_object* l___regBuiltinParser_Lean_Parser_Term_eq(lean_object*); lean_object* l_Lean_Parser_Term_mapRev___closed__3; lean_object* l_Lean_Parser_Term_subst___elambda__1___closed__1; @@ -723,7 +732,6 @@ lean_object* l_Lean_Parser_Term_namedArgument___closed__4; lean_object* l_Lean_Parser_Term_fromTerm___closed__4; lean_object* l_Lean_Parser_Term_paren___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__6; -lean_object* l_Lean_Parser_Term_array___closed__2; lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_hole___elambda__1___rarg___closed__1; @@ -744,7 +752,6 @@ lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__2; lean_object* l_List_foldl___main___at_Lean_Parser_mkAppStx___spec__1(lean_object*); lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l___regBuiltinParser_Lean_Parser_Term_array(lean_object*); lean_object* l_Lean_Parser_Term_mul___closed__3; lean_object* l_Lean_Parser_Term_paren___closed__1; lean_object* l_Lean_Parser_Term_if; @@ -786,10 +793,10 @@ lean_object* l_Lean_Parser_Term_binderType___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_str___closed__1; lean_object* l_Lean_Parser_Term_letEqns___closed__2; -lean_object* l_Lean_Parser_Term_list___closed__6; lean_object* l_Lean_Parser_termParser___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_suffices___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_letIdLhs; +lean_object* l_Lean_Parser_Term_arrayLit; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_forall___elambda__1___spec__1___closed__1; lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_emptyC___elambda__1___rarg___closed__2; @@ -806,12 +813,10 @@ lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__3; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_forall___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_pow___closed__2; lean_object* l_Lean_Parser_Term_pow; -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__2; lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__1; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_matchAlt___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_append___elambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__6; +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitBinder___closed__6; lean_object* l___regBuiltinParser_Lean_Parser_Term_quotedName(lean_object*); lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__1; @@ -819,6 +824,7 @@ lean_object* l_Lean_Parser_Term_sort___elambda__1___rarg(lean_object*, lean_obje lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_bind___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_bne___closed__2; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_fun___closed__6; lean_object* l_Lean_Parser_Term_match___elambda__1___closed__4; lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*); @@ -834,6 +840,7 @@ lean_object* l_Lean_Parser_Term_leftArrow___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_structInst___elambda__1___closed__9; lean_object* l___regBuiltinParser_Lean_Parser_Term_subst(lean_object*); lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__5; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_gt; extern lean_object* l_Lean_Parser_levelParserAttribute; lean_object* l_Lean_Parser_Term_uminus___elambda__1___rarg___closed__1; @@ -852,7 +859,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_sorry(lean_object*); lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__4; lean_object* lean_name_mk_string(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__2; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_uminus___closed__1; lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__15; lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__4; @@ -864,12 +870,12 @@ lean_object* l_Lean_Parser_Term_ge___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_sort; lean_object* l_Lean_Parser_Term_forall___closed__7; lean_object* l_Lean_Parser_Term_binderIdent___closed__2; +lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_append___closed__3; lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_structInstSource___closed__2; lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__5; -lean_object* l_Lean_Parser_Term_list___closed__1; lean_object* l_Lean_Parser_Term_infixL___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_sort___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_gt___elambda__1(lean_object*, lean_object*, lean_object*); @@ -885,9 +891,11 @@ lean_object* l_Lean_Parser_Term_fun___elambda__1___boxed(lean_object*, lean_obje lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_structInst___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_add(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_char___elambda__1___boxed(lean_object*); +lean_object* l_Lean_Parser_Term_listLit___closed__6; lean_object* l_Lean_Parser_Term_fromTerm___closed__1; lean_object* l_Lean_Parser_Term_show___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_fromTerm___elambda__1(lean_object*); +lean_object* l_Lean_Parser_Term_arrayRef___closed__4; extern lean_object* l_Lean_nullKind; lean_object* l_Lean_Parser_Term_nomatch___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_explicitUniv___closed__9; @@ -940,7 +948,6 @@ lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_matchAlt___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_let___elambda__1___closed__3; extern lean_object* l_Lean_Parser_Level_hole___elambda__1___rarg___closed__3; -lean_object* l_Lean_Parser_Term_list___closed__9; lean_object* l_Lean_Parser_Term_letPatDecl___closed__3; lean_object* l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_structInst(lean_object*); @@ -958,9 +965,10 @@ lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg(lean_object*, lean_ lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_instBinder___closed__5; lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___rarg___closed__1; -lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_list___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_tparser_x21___closed__1; extern lean_object* l_Lean_Parser_Level_paren___elambda__1___rarg___closed__3; +lean_object* l_Lean_Parser_Term_arrayRef___closed__3; lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_have___closed__9; extern lean_object* l_Int_repr___closed__1; @@ -986,7 +994,9 @@ lean_object* l_Lean_Parser_Term_show___elambda__1___rarg(lean_object*, lean_obje lean_object* l_Lean_Parser_mkTermParserAttribute___closed__5; lean_object* l___regBuiltinParser_Lean_Parser_Term_num___closed__1; lean_object* l_Lean_Parser_Term_bind___closed__3; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_orM___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__6; lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_suffices___closed__2; lean_object* l_Lean_Parser_Term_band___closed__2; @@ -1058,6 +1068,7 @@ lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_letIdLhs___closed__4; extern lean_object* l_Lean_Parser_Level_paren___closed__2; +lean_object* l_Lean_Parser_Term_arrayLit___closed__2; lean_object* l_Lean_Parser_Term_do___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_le___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_letDecl___closed__3; @@ -1102,13 +1113,16 @@ lean_object* l_Lean_Parser_Term_doLet___elambda__1___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_id(lean_object*); lean_object* l_Lean_Parser_Term_forall___closed__2; lean_object* l___regBuiltinParser_Lean_Parser_Term_explicit(lean_object*); +lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_structInstSource___closed__3; lean_object* l_Lean_Parser_Term_sorry___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Term_bne(lean_object*); lean_object* l_Lean_Parser_Term_add___elambda__1___closed__3; +lean_object* l_Lean_Parser_Term_arrayRef___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_binderIdent___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_letEqns___closed__5; lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__2; +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__3; lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__15; lean_object* l_Lean_Parser_Term_if___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_depArrow(lean_object*); @@ -1161,13 +1175,14 @@ lean_object* l_Lean_Parser_Term_optIdent___closed__3; lean_object* l_Lean_Parser_Term_unicodeInfixR___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__6; extern lean_object* l_Sigma_HasRepr___rarg___closed__2; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_uminus; lean_object* l_Lean_Parser_Term_subtype___closed__7; lean_object* l_String_trim(lean_object*); lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_arrayLit___closed__4; lean_object* l_Lean_Parser_Term_structInst___closed__10; lean_object* l_Lean_Parser_Term_sortApp___closed__5; -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicit___closed__3; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_andM___closed__2; @@ -1190,9 +1205,8 @@ lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__1; lean_object* l_Lean_Parser_Term_binderDefault; lean_object* l_Lean_Parser_Term_explicitBinder___closed__4; lean_object* l_Lean_Parser_regBuiltinTermParserAttr___closed__1; -lean_object* l_Lean_Parser_Term_array___closed__3; lean_object* l_Lean_Parser_Term_show___closed__5; -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1; +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_simpleBinder___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_nomatch___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_sortApp___elambda__1(lean_object*, lean_object*, lean_object*); @@ -1221,6 +1235,7 @@ lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_simpleBinder___elambda__1___closed__1; lean_object* l_Lean_Parser_symbolNoWsInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_letPatDecl___elambda__1___rarg___closed__1; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_instBinder___closed__6; lean_object* l_Lean_Parser_Term_tupleTail___closed__3; lean_object* l_Lean_Parser_unicodeSymbolFn___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1260,10 +1275,12 @@ lean_object* l_Lean_Parser_Term_structInstField___closed__3; lean_object* l_Lean_Parser_Term_seqRight___elambda__1___closed__2; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___elambda__1___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_seq___closed__2; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__11; lean_object* l_Lean_Parser_Term_map___closed__1; lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_lt___elambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_arrayLit___closed__3; lean_object* l_Lean_Parser_Term_letPatDecl___closed__6; lean_object* l_Lean_Parser_Term_paren___closed__5; lean_object* l_Lean_Parser_Term_map___closed__2; @@ -1274,7 +1291,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_have(lean_object*); lean_object* l_Lean_Parser_Term_arrow___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_sub___closed__2; lean_object* l_Lean_Parser_Term_and___closed__3; -lean_object* l_Lean_Parser_Term_list; lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_tupleTail___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_gt___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___rarg___closed__6; @@ -1291,11 +1307,9 @@ lean_object* l_Lean_Parser_Term_proj___elambda__1(lean_object*, lean_object*, le lean_object* l_Array_size(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_letPatDecl; lean_object* l_Lean_Parser_Term_bracketedDoSeq___elambda__1___closed__1; -lean_object* l_Lean_Parser_Term_list___closed__3; lean_object* l_Lean_Parser_Term_seq___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_bne___closed__3; lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg___closed__4; -lean_object* l_Lean_Parser_Term_array___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_mapConstRev___closed__1; lean_object* l_Lean_Parser_Term_anonymousCtor___closed__2; @@ -1323,6 +1337,7 @@ lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___rarg___closed__8; lean_object* l_Lean_Parser_Term_matchAlt___closed__1; lean_object* l_Lean_Parser_Term_if___closed__6; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_structInstSource___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__7; lean_object* l_Lean_Parser_Term_have___closed__8; @@ -1368,6 +1383,7 @@ lean_object* l_Lean_Parser_Term_type___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_binderType___closed__4; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__12; lean_object* l_Lean_Parser_Term_structInst___closed__7; +lean_object* l_Lean_Parser_Term_arrayLit___closed__5; extern lean_object* l_Lean_Parser_ParserAttribute_inhabited___closed__4; lean_object* l_Lean_Parser_Term_bnot___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_prop___elambda__1___rarg(lean_object*, lean_object*); @@ -1378,11 +1394,9 @@ lean_object* l_Lean_Parser_Term_bnot___closed__5; lean_object* l_Lean_Parser_Term_explicitUniv___closed__7; lean_object* l_Lean_Parser_Term_optType___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_map___elambda__1(lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Term_array___closed__1; lean_object* l___regBuiltinParser_Lean_Parser_Term_app(lean_object*); lean_object* l_Lean_Parser_Term_beq___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_seq___closed__1; -lean_object* l_Lean_Parser_Term_list___closed__5; lean_object* l_Lean_Parser_Term_do___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_explicit___closed__2; lean_object* l_Lean_Parser_Term_hole___elambda__1___rarg(lean_object*, lean_object*); @@ -1410,7 +1424,6 @@ lean_object* l_Lean_Parser_Term_prop___closed__3; lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_structInstField___elambda__1___rarg___closed__1; -lean_object* l_Lean_Parser_Term_list___closed__2; lean_object* l_Lean_Parser_Term_sort___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_equiv___closed__3; lean_object* l_Lean_Parser_Term_match___closed__9; @@ -1431,21 +1444,21 @@ lean_object* l_Lean_Parser_Term_tparser_x21___elambda__1___rarg___closed__7; lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__2; lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_subtype___elambda__1___rarg___closed__1; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_checkIsSort___closed__2; lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__4; lean_object* l___regBuiltinParser_Lean_Parser_Term_show(lean_object*); lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__9; +lean_object* l_Lean_Parser_Term_listLit; lean_object* l___regBuiltinParser_Lean_Parser_Term_prod(lean_object*); lean_object* l_Lean_Parser_Term_bracketedDoSeq___closed__2; lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_char; lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_borrowed___elambda__1___rarg___closed__2; -lean_object* l_Lean_Parser_Term_array___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__4; lean_object* l___regBuiltinParser_Lean_Parser_Term_beq(lean_object*); lean_object* l_Lean_Parser_Term_implicitBinder___elambda__1___closed__1; +lean_object* l_Lean_Parser_Term_listLit___closed__1; lean_object* l_Lean_Parser_Term_binderTactic___closed__2; lean_object* l_Lean_Parser_charLitFn___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_show___elambda__1___rarg___closed__5; @@ -1461,7 +1474,6 @@ lean_object* l_Lean_Parser_Term_match___elambda__1___boxed(lean_object*, lean_ob lean_object* l_Lean_Parser_Term_id___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_instBinder___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_cons___closed__2; -lean_object* l___regBuiltinParser_Lean_Parser_Term_list(lean_object*); lean_object* l_Lean_Parser_Term_if___closed__7; lean_object* l_Lean_Parser_Term_equiv___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_andthen___closed__1; @@ -1497,6 +1509,7 @@ lean_object* l_Lean_Parser_Term_mapConstRev___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__3; lean_object* l_Lean_Parser_Term_namedPattern___closed__2; lean_object* l_Lean_Parser_Term_prod___elambda__1___closed__4; +lean_object* l_Lean_Parser_Term_listLit___closed__2; lean_object* l_Lean_Parser_Term_match___closed__4; lean_object* l_Lean_Parser_Term_namedPattern; lean_object* l_Lean_Parser_Term_optIdent___closed__1; @@ -1504,7 +1517,6 @@ lean_object* l_Lean_Parser_Term_matchAlt; lean_object* l_Lean_Parser_Term_bnot___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_cdot___elambda__1___rarg___closed__6; lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(lean_object*); -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_instBinder___closed__3; extern lean_object* l_Lean_formatEntry___closed__1; lean_object* l_Lean_Parser_Term_binderTactic___elambda__1___rarg___closed__2; @@ -1527,7 +1539,6 @@ lean_object* l_Lean_Parser_Term_le___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_nomatch___closed__4; lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_structInstField___elambda__1___boxed(lean_object*); -lean_object* l_Lean_Parser_Term_array___closed__4; lean_object* l_Lean_Parser_Term_pow___closed__3; lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_eq___closed__2; @@ -1539,6 +1550,7 @@ lean_object* l_Lean_Parser_Term_fun___closed__2; lean_object* l_Lean_Parser_Term_inaccessible___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_Term_forall___closed__6; lean_object* l_Lean_Parser_Term_implicitBinder___closed__1; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_inaccessible___closed__2; lean_object* l_Lean_Parser_Term_subst___closed__1; lean_object* l_Lean_Parser_Term_binderDefault___elambda__1(lean_object*); @@ -1549,6 +1561,7 @@ extern lean_object* l_Lean_Parser_epsilonInfo; lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__11; lean_object* l_Lean_Parser_Term_namedArgument___closed__5; lean_object* l_Lean_Parser_Term_letIdLhs___closed__2; +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_cdot___closed__2; lean_object* l_Lean_Parser_Term_uminus___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_Term_proj___closed__2; @@ -1596,6 +1609,7 @@ lean_object* l_Lean_Parser_Term_doId___closed__6; lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_forall___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__4; +lean_object* l_Lean_Parser_Term_listLit___closed__3; lean_object* l_Lean_Parser_Term_cons___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinParser_Lean_Parser_Term_andM(lean_object*); lean_object* l_Lean_Parser_Term_arrow___closed__3; @@ -1606,7 +1620,6 @@ lean_object* l_Lean_Parser_Term_mapConst___closed__2; lean_object* l_Lean_Parser_Term_simpleBinder___closed__3; lean_object* l_Lean_Parser_Term_explicitBinder___closed__7; lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__1; -lean_object* l_Lean_Parser_Term_array___closed__5; lean_object* l_Lean_Parser_Term_have___elambda__1___rarg___closed__8; lean_object* l_Lean_Parser_Term_lt___closed__2; lean_object* l_Lean_Parser_Term_let___closed__1; @@ -1620,9 +1633,10 @@ lean_object* l_Lean_Parser_Term_prop___closed__2; lean_object* l_Lean_Parser_Term_doElem; lean_object* l_Lean_Parser_Term_emptyC___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_sub___closed__1; -lean_object* l_Lean_Parser_Term_array___elambda__1___closed__1; +lean_object* l___regBuiltinParser_Lean_Parser_Term_listLit(lean_object*); lean_object* l_Lean_Parser_Term_do___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Term_andthen(lean_object*); +lean_object* l_Lean_Parser_Term_listLit___closed__8; lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___boxed(lean_object*); lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__10; lean_object* l_Lean_Parser_Term_if___elambda__1___rarg___closed__12; @@ -1654,8 +1668,8 @@ lean_object* l_Lean_Parser_Term_typeSpec; lean_object* l_Lean_Parser_Term_bracktedBinder___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_div___closed__1; lean_object* l_Lean_Parser_Term_binderIdent___closed__1; -lean_object* l_Lean_Parser_Term_array___elambda__1___closed__3; -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2(uint8_t, uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__8; +lean_object* l_Lean_Parser_Term_arrayRef___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_letPatDecl___closed__1; lean_object* l_Lean_Parser_Term_emptyC___elambda__1___rarg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_doElem___closed__5; @@ -1675,6 +1689,7 @@ lean_object* l_Lean_Parser_Term_doLet___closed__3; lean_object* l_Lean_Parser_Term_sort___elambda__1___rarg___closed__6; lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___rarg___closed__5; lean_object* l_Lean_Parser_Term_fcomp___closed__3; +lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_fun___closed__5; lean_object* l_Lean_Parser_Term_fun; lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___rarg___closed__6; @@ -1697,6 +1712,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_mul(lean_object*); lean_object* l_Lean_Parser_Term_band; lean_object* l_Lean_Parser_Term_cdot___elambda__1(lean_object*); lean_object* l_Lean_Parser_Term_doExpr; +lean_object* l_Lean_Parser_Term_listLit___elambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_suffices___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__13; lean_object* l_Lean_Parser_Term_fromTerm___closed__3; @@ -1722,7 +1738,7 @@ lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___rarg___closed__4; lean_object* l_Lean_Parser_mkBuiltinParsingTablesRef(lean_object*); lean_object* l_Lean_Parser_Term_heq___closed__2; lean_object* l_Lean_Parser_Term_heq___closed__3; -lean_object* l_Lean_Parser_Term_list___elambda__1___closed__7; +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_band___closed__3; lean_object* l_Lean_Parser_Term_app; lean_object* l_Lean_Parser_Term_optIdent___closed__2; @@ -11552,7 +11568,7 @@ x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1() { +lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1() { _start: { lean_object* x_1; lean_object* x_2; @@ -11561,39 +11577,39 @@ x_2 = l_String_trim(x_1); return x_2; } } -lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__2() { +lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Char_HasRepr___closed__1; -x_2 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1; +x_2 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__3() { +lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__2; +x_1 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__2; x_2 = l_Char_HasRepr___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4() { +lean_object* _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__3; +x_2 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__3; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2(uint8_t x_1, uint8_t x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2(uint8_t x_1, uint8_t x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { 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; @@ -11637,13 +11653,13 @@ lean_object* x_29; lean_object* x_30; uint8_t x_31; x_29 = lean_ctor_get(x_28, 1); lean_inc(x_29); lean_dec(x_28); -x_30 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1; +x_30 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1; x_31 = lean_string_dec_eq(x_29, x_30); lean_dec(x_29); if (x_31 == 0) { lean_object* x_32; lean_object* x_33; -x_32 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4; +x_32 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4; lean_inc(x_17); x_33 = l_Lean_Parser_ParserState_mkErrorsAt(x_25, x_32, x_17); x_18 = x_33; @@ -11659,7 +11675,7 @@ else { lean_object* x_34; lean_object* x_35; lean_dec(x_28); -x_34 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4; +x_34 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4; lean_inc(x_17); x_35 = l_Lean_Parser_ParserState_mkErrorsAt(x_25, x_34, x_17); x_18 = x_35; @@ -11670,7 +11686,7 @@ else { lean_object* x_36; lean_object* x_37; lean_dec(x_26); -x_36 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4; +x_36 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4; lean_inc(x_17); x_37 = l_Lean_Parser_ParserState_mkErrorsAt(x_25, x_36, x_17); x_18 = x_37; @@ -11733,7 +11749,7 @@ return x_44; } } } -lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_list___elambda__1___spec__1(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; uint8_t x_8; lean_object* x_9; @@ -11742,29 +11758,29 @@ lean_inc(x_6); x_7 = lean_array_get_size(x_6); lean_dec(x_6); x_8 = 1; -x_9 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2(x_1, x_2, x_7, x_8, x_3, x_4, x_5); +x_9 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2(x_1, x_2, x_7, x_8, x_3, x_4, x_5); return x_9; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__1() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("list"); +x_1 = lean_mk_string("listLit"); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__2() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__1; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__3() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__3() { _start: { lean_object* x_1; lean_object* x_2; @@ -11773,7 +11789,7 @@ x_2 = l_String_trim(x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__4() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__4() { _start: { lean_object* x_1; lean_object* x_2; @@ -11782,71 +11798,71 @@ x_2 = l_String_trim(x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__5() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Char_HasRepr___closed__1; -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__6() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__5; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__5; x_2 = l_Char_HasRepr___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__7() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__6; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__6; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__8() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__8() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Char_HasRepr___closed__1; -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__9() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__8; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__8; x_2 = l_Char_HasRepr___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___elambda__1___closed__10() { +lean_object* _init_l_Lean_Parser_Term_listLit___elambda__1___closed__10() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__9; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__9; x_3 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_3, 0, x_2); lean_ctor_set(x_3, 1, x_1); return x_3; } } -lean_object* l_Lean_Parser_Term_list___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_Term_listLit___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_39; lean_object* x_40; lean_object* x_41; @@ -11873,13 +11889,13 @@ lean_object* x_44; lean_object* x_45; uint8_t x_46; x_44 = lean_ctor_get(x_43, 1); lean_inc(x_44); lean_dec(x_43); -x_45 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_45 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_46 = lean_string_dec_eq(x_44, x_45); lean_dec(x_44); if (x_46 == 0) { lean_object* x_47; lean_object* x_48; -x_47 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_47 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_48 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_47, x_39); x_6 = x_48; goto block_38; @@ -11895,7 +11911,7 @@ else { lean_object* x_49; lean_object* x_50; lean_dec(x_43); -x_49 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_49 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_50 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_49, x_39); x_6 = x_50; goto block_38; @@ -11905,7 +11921,7 @@ else { lean_object* x_51; lean_object* x_52; lean_dec(x_41); -x_51 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_51 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_51, x_39); x_6 = x_52; goto block_38; @@ -11921,7 +11937,7 @@ uint8_t x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; x_8 = 0; x_9 = 1; lean_inc(x_2); -x_10 = l_Lean_Parser_sepByFn___at_Lean_Parser_Term_list___elambda__1___spec__1(x_8, x_9, x_1, x_2, x_6); +x_10 = l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1(x_8, x_9, x_1, x_2, x_6); x_11 = lean_ctor_get(x_10, 3); lean_inc(x_11); if (lean_obj_tag(x_11) == 0) @@ -11945,15 +11961,15 @@ lean_object* x_17; lean_object* x_18; uint8_t x_19; x_17 = lean_ctor_get(x_16, 1); lean_inc(x_17); lean_dec(x_16); -x_18 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_18 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_19 = lean_string_dec_eq(x_17, x_18); lean_dec(x_17); if (x_19 == 0) { lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; -x_20 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_20 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_20, x_12); -x_22 = l_Lean_Parser_Term_list___elambda__1___closed__2; +x_22 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_5); return x_23; } @@ -11961,7 +11977,7 @@ else { lean_object* x_24; lean_object* x_25; lean_dec(x_12); -x_24 = l_Lean_Parser_Term_list___elambda__1___closed__2; +x_24 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_25 = l_Lean_Parser_ParserState_mkNode(x_13, x_24, x_5); return x_25; } @@ -11970,9 +11986,9 @@ else { lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_dec(x_16); -x_26 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_26 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_26, x_12); -x_28 = l_Lean_Parser_Term_list___elambda__1___closed__2; +x_28 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_5); return x_29; } @@ -11981,9 +11997,9 @@ else { lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_dec(x_14); -x_30 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_30 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_30, x_12); -x_32 = l_Lean_Parser_Term_list___elambda__1___closed__2; +x_32 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_5); return x_33; } @@ -11993,7 +12009,7 @@ else lean_object* x_34; lean_object* x_35; lean_dec(x_11); lean_dec(x_2); -x_34 = l_Lean_Parser_Term_list___elambda__1___closed__2; +x_34 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_35 = l_Lean_Parser_ParserState_mkNode(x_10, x_34, x_5); return x_35; } @@ -12003,112 +12019,112 @@ else lean_object* x_36; lean_object* x_37; lean_dec(x_7); lean_dec(x_2); -x_36 = l_Lean_Parser_Term_list___elambda__1___closed__2; +x_36 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; x_37 = l_Lean_Parser_ParserState_mkNode(x_6, x_36, x_5); return x_37; } } } } -lean_object* _init_l_Lean_Parser_Term_list___closed__1() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_2 = l_Lean_Parser_Level_paren___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__2() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1; +x_2 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1; x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__3() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Parser_inhabited___closed__1; -x_2 = l_Lean_Parser_Term_list___closed__2; +x_2 = l_Lean_Parser_Term_listLit___closed__2; x_3 = l_Lean_Parser_sepByInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__4() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__5() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___closed__3; -x_2 = l_Lean_Parser_Term_list___closed__4; +x_1 = l_Lean_Parser_Term_listLit___closed__3; +x_2 = l_Lean_Parser_Term_listLit___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__6() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___closed__1; -x_2 = l_Lean_Parser_Term_list___closed__5; +x_1 = l_Lean_Parser_Term_listLit___closed__1; +x_2 = l_Lean_Parser_Term_listLit___closed__5; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__7() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__7() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_list___closed__6; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_listLit___closed__6; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__8() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__8() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_list___elambda__1___boxed), 3, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_listLit___elambda__1___boxed), 3, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_list___closed__9() { +lean_object* _init_l_Lean_Parser_Term_listLit___closed__9() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___closed__7; -x_2 = l_Lean_Parser_Term_list___closed__8; +x_1 = l_Lean_Parser_Term_listLit___closed__7; +x_2 = l_Lean_Parser_Term_listLit___closed__8; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_list() { +lean_object* _init_l_Lean_Parser_Term_listLit() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_list___closed__9; +x_1 = l_Lean_Parser_Term_listLit___closed__9; return x_1; } } -lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { +lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { uint8_t x_8; uint8_t x_9; uint8_t x_10; lean_object* x_11; @@ -12118,12 +12134,12 @@ x_9 = lean_unbox(x_2); lean_dec(x_2); x_10 = lean_unbox(x_4); lean_dec(x_4); -x_11 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2(x_8, x_9, x_3, x_10, x_5, x_6, x_7); +x_11 = l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2(x_8, x_9, x_3, x_10, x_5, x_6, x_7); lean_dec(x_5); return x_11; } } -lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_list___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { uint8_t x_6; uint8_t x_7; lean_object* x_8; @@ -12131,27 +12147,336 @@ x_6 = lean_unbox(x_1); lean_dec(x_1); x_7 = lean_unbox(x_2); lean_dec(x_2); -x_8 = l_Lean_Parser_sepByFn___at_Lean_Parser_Term_list___elambda__1___spec__1(x_6, x_7, x_3, x_4, x_5); +x_8 = l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1(x_6, x_7, x_3, x_4, x_5); lean_dec(x_3); return x_8; } } -lean_object* l_Lean_Parser_Term_list___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_Term_listLit___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; -x_4 = l_Lean_Parser_Term_list___elambda__1(x_1, x_2, x_3); +x_4 = l_Lean_Parser_Term_listLit___elambda__1(x_1, x_2, x_3); lean_dec(x_1); return x_4; } } -lean_object* l___regBuiltinParser_Lean_Parser_Term_list(lean_object* x_1) { +lean_object* l___regBuiltinParser_Lean_Parser_Term_listLit(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Parser_builtinTermParsingTable; -x_3 = l_Lean_Parser_Term_list___elambda__1___closed__2; -x_4 = l_Lean_Parser_Term_list; +x_3 = l_Lean_Parser_Term_listLit___elambda__1___closed__2; +x_4 = l_Lean_Parser_Term_listLit; +x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1); +return x_5; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("arrayLit"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("#["); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__3; +x_2 = l_String_trim(x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Char_HasRepr___closed__1; +x_2 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__4; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__5; +x_2 = l_Char_HasRepr___closed__1; +x_3 = lean_string_append(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__6; +x_3 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_3, 0, x_2); +lean_ctor_set(x_3, 1, x_1); +return x_3; +} +} +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_39; lean_object* x_40; lean_object* x_41; +x_4 = lean_ctor_get(x_3, 0); +lean_inc(x_4); +x_5 = lean_array_get_size(x_4); +lean_dec(x_4); +x_39 = lean_ctor_get(x_3, 1); +lean_inc(x_39); +lean_inc(x_2); +x_40 = l_Lean_Parser_tokenFn(x_2, x_3); +x_41 = lean_ctor_get(x_40, 3); +lean_inc(x_41); +if (lean_obj_tag(x_41) == 0) +{ +lean_object* x_42; lean_object* x_43; +x_42 = lean_ctor_get(x_40, 0); +lean_inc(x_42); +x_43 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_42); +lean_dec(x_42); +if (lean_obj_tag(x_43) == 2) +{ +lean_object* x_44; lean_object* x_45; uint8_t x_46; +x_44 = lean_ctor_get(x_43, 1); +lean_inc(x_44); +lean_dec(x_43); +x_45 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__4; +x_46 = lean_string_dec_eq(x_44, x_45); +lean_dec(x_44); +if (x_46 == 0) +{ +lean_object* x_47; lean_object* x_48; +x_47 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__7; +x_48 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_47, x_39); +x_6 = x_48; +goto block_38; +} +else +{ +lean_dec(x_39); +x_6 = x_40; +goto block_38; +} +} +else +{ +lean_object* x_49; lean_object* x_50; +lean_dec(x_43); +x_49 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__7; +x_50 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_49, x_39); +x_6 = x_50; +goto block_38; +} +} +else +{ +lean_object* x_51; lean_object* x_52; +lean_dec(x_41); +x_51 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__7; +x_52 = l_Lean_Parser_ParserState_mkErrorsAt(x_40, x_51, x_39); +x_6 = x_52; +goto block_38; +} +block_38: +{ +lean_object* x_7; +x_7 = lean_ctor_get(x_6, 3); +lean_inc(x_7); +if (lean_obj_tag(x_7) == 0) +{ +uint8_t x_8; uint8_t x_9; lean_object* x_10; lean_object* x_11; +x_8 = 0; +x_9 = 1; +lean_inc(x_2); +x_10 = l_Lean_Parser_sepByFn___at_Lean_Parser_Term_listLit___elambda__1___spec__1(x_8, x_9, x_1, x_2, x_6); +x_11 = lean_ctor_get(x_10, 3); +lean_inc(x_11); +if (lean_obj_tag(x_11) == 0) +{ +lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_12 = lean_ctor_get(x_10, 1); +lean_inc(x_12); +x_13 = l_Lean_Parser_tokenFn(x_2, x_10); +x_14 = lean_ctor_get(x_13, 3); +lean_inc(x_14); +if (lean_obj_tag(x_14) == 0) +{ +lean_object* x_15; lean_object* x_16; +x_15 = lean_ctor_get(x_13, 0); +lean_inc(x_15); +x_16 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_15); +lean_dec(x_15); +if (lean_obj_tag(x_16) == 2) +{ +lean_object* x_17; lean_object* x_18; uint8_t x_19; +x_17 = lean_ctor_get(x_16, 1); +lean_inc(x_17); +lean_dec(x_16); +x_18 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; +x_19 = lean_string_dec_eq(x_17, x_18); +lean_dec(x_17); +if (x_19 == 0) +{ +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_20 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; +x_21 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_20, x_12); +x_22 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_5); +return x_23; +} +else +{ +lean_object* x_24; lean_object* x_25; +lean_dec(x_12); +x_24 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_25 = l_Lean_Parser_ParserState_mkNode(x_13, x_24, x_5); +return x_25; +} +} +else +{ +lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; +lean_dec(x_16); +x_26 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; +x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_26, x_12); +x_28 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_5); +return x_29; +} +} +else +{ +lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +lean_dec(x_14); +x_30 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; +x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_13, x_30, x_12); +x_32 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_33 = l_Lean_Parser_ParserState_mkNode(x_31, x_32, x_5); +return x_33; +} +} +else +{ +lean_object* x_34; lean_object* x_35; +lean_dec(x_11); +lean_dec(x_2); +x_34 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_35 = l_Lean_Parser_ParserState_mkNode(x_10, x_34, x_5); +return x_35; +} +} +else +{ +lean_object* x_36; lean_object* x_37; +lean_dec(x_7); +lean_dec(x_2); +x_36 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_37 = l_Lean_Parser_ParserState_mkNode(x_6, x_36, x_5); +return x_37; +} +} +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__4; +x_2 = l_Lean_Parser_Level_paren___closed__1; +x_3 = l_Lean_Parser_symbolInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_arrayLit___closed__1; +x_2 = l_Lean_Parser_Term_listLit___closed__5; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_arrayLit___closed__2; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___closed__4() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_arrayLit___elambda__1___boxed), 3, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit___closed__5() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Term_arrayLit___closed__3; +x_2 = l_Lean_Parser_Term_arrayLit___closed__4; +x_3 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_3, 0, x_1); +lean_ctor_set(x_3, 1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Term_arrayLit() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Term_arrayLit___closed__5; +return x_1; +} +} +lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; +x_4 = l_Lean_Parser_Term_arrayLit___elambda__1(x_1, x_2, x_3); +lean_dec(x_1); +return x_4; +} +} +lean_object* l___regBuiltinParser_Lean_Parser_Term_arrayLit(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_Parser_builtinTermParsingTable; +x_3 = l_Lean_Parser_Term_arrayLit___elambda__1___closed__2; +x_4 = l_Lean_Parser_Term_arrayLit; x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1); return x_5; } @@ -13781,13 +14106,13 @@ lean_object* x_47; lean_object* x_48; uint8_t x_49; x_47 = lean_ctor_get(x_46, 1); lean_inc(x_47); lean_dec(x_46); -x_48 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_48 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_49 = lean_string_dec_eq(x_47, x_48); lean_dec(x_47); if (x_49 == 0) { lean_object* x_50; lean_object* x_51; -x_50 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_50 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_51 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_50, x_42); x_5 = x_51; goto block_41; @@ -13803,7 +14128,7 @@ else { lean_object* x_52; lean_object* x_53; lean_dec(x_46); -x_52 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_52 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_53 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_52, x_42); x_5 = x_53; goto block_41; @@ -13813,7 +14138,7 @@ else { lean_object* x_54; lean_object* x_55; lean_dec(x_44); -x_54 = l_Lean_Parser_Term_list___elambda__1___closed__10; +x_54 = l_Lean_Parser_Term_listLit___elambda__1___closed__10; x_55 = l_Lean_Parser_ParserState_mkErrorsAt(x_43, x_54, x_42); x_5 = x_55; goto block_41; @@ -13860,13 +14185,13 @@ lean_object* x_18; lean_object* x_19; uint8_t x_20; x_18 = lean_ctor_get(x_17, 1); lean_inc(x_18); lean_dec(x_17); -x_19 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_19 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_20 = lean_string_dec_eq(x_18, x_19); lean_dec(x_18); if (x_20 == 0) { lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; -x_21 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_21 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_22 = l_Lean_Parser_ParserState_mkErrorsAt(x_14, x_21, x_13); x_23 = l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__2; x_24 = l_Lean_Parser_ParserState_mkNode(x_22, x_23, x_4); @@ -13885,7 +14210,7 @@ else { lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_dec(x_17); -x_27 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_27 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_14, x_27, x_13); x_29 = l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__2; x_30 = l_Lean_Parser_ParserState_mkNode(x_28, x_29, x_4); @@ -13896,7 +14221,7 @@ else { lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_dec(x_15); -x_31 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_31 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_14, x_31, x_13); x_33 = l_Lean_Parser_Term_instBinder___elambda__1___rarg___closed__2; x_34 = l_Lean_Parser_ParserState_mkNode(x_32, x_33, x_4); @@ -13948,7 +14273,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = lean_box(0); -x_2 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_2 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_3 = l_Lean_Parser_symbolInfo(x_2, x_1); return x_3; } @@ -13958,7 +14283,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Parser_inhabited___closed__1; -x_2 = l_Lean_Parser_Term_list___closed__4; +x_2 = l_Lean_Parser_Term_listLit___closed__4; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } @@ -23817,44 +24142,44 @@ x_5 = l_Lean_Parser_addBuiltinTrailingParser(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* _init_l_Lean_Parser_Term_array___elambda__1___closed__1() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("array"); +x_1 = lean_mk_string("arrayRef"); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_array___elambda__1___closed__2() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_array___elambda__1___closed__1; +x_2 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array___elambda__1___closed__3() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__8; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__8; x_2 = l_Lean_Parser_symbolNoWsFn___closed__1; x_3 = lean_string_append(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array___elambda__1___closed__4() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__4() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_2 = lean_string_utf8_byte_size(x_1); return x_2; } } -lean_object* l_Lean_Parser_Term_array___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_Lean_Parser_Term_arrayRef___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_41; @@ -23877,7 +24202,7 @@ if (x_42 == 0) { lean_object* x_43; lean_object* x_44; lean_dec(x_5); -x_43 = l_Lean_Parser_Term_array___elambda__1___closed__3; +x_43 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__3; x_44 = l_Lean_Parser_ParserState_mkError(x_41, x_43); x_8 = x_44; goto block_40; @@ -23890,8 +24215,8 @@ lean_inc(x_45); x_46 = lean_ctor_get(x_45, 0); lean_inc(x_46); lean_dec(x_45); -x_47 = l_Lean_Parser_Term_list___elambda__1___closed__3; -x_48 = l_Lean_Parser_Term_array___elambda__1___closed__3; +x_47 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; +x_48 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__3; x_49 = lean_unsigned_to_nat(0u); x_50 = l_Lean_Parser_strAux___main(x_47, x_48, x_49, x_2, x_41); x_51 = lean_ctor_get(x_50, 3); @@ -23905,7 +24230,7 @@ x_52 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_52, 0, x_46); lean_ctor_set(x_52, 1, x_5); lean_ctor_set(x_52, 2, x_5); -x_53 = l_Lean_Parser_Term_array___elambda__1___closed__4; +x_53 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__4; x_54 = lean_nat_add(x_5, x_53); lean_inc(x_54); x_55 = lean_alloc_ctor(0, 3, 0); @@ -23942,7 +24267,7 @@ lean_dec(x_6); lean_dec(x_5); lean_dec(x_2); lean_dec(x_1); -x_60 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_60 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_61 = l_Lean_Parser_ParserState_mkNode(x_41, x_60, x_7); return x_61; } @@ -23981,15 +24306,15 @@ lean_object* x_19; lean_object* x_20; uint8_t x_21; x_19 = lean_ctor_get(x_18, 1); lean_inc(x_19); lean_dec(x_18); -x_20 = l_Lean_Parser_Term_list___elambda__1___closed__4; +x_20 = l_Lean_Parser_Term_listLit___elambda__1___closed__4; x_21 = lean_string_dec_eq(x_19, x_20); lean_dec(x_19); if (x_21 == 0) { lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; -x_22 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_22 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_23 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_22, x_14); -x_24 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_24 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_25 = l_Lean_Parser_ParserState_mkNode(x_23, x_24, x_7); return x_25; } @@ -23997,7 +24322,7 @@ else { lean_object* x_26; lean_object* x_27; lean_dec(x_14); -x_26 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_26 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_27 = l_Lean_Parser_ParserState_mkNode(x_15, x_26, x_7); return x_27; } @@ -24006,9 +24331,9 @@ else { lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_dec(x_18); -x_28 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_28 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_28, x_14); -x_30 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_30 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_31 = l_Lean_Parser_ParserState_mkNode(x_29, x_30, x_7); return x_31; } @@ -24017,9 +24342,9 @@ else { lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_dec(x_16); -x_32 = l_Lean_Parser_Term_list___elambda__1___closed__7; +x_32 = l_Lean_Parser_Term_listLit___elambda__1___closed__7; x_33 = l_Lean_Parser_ParserState_mkErrorsAt(x_15, x_32, x_14); -x_34 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_34 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_35 = l_Lean_Parser_ParserState_mkNode(x_33, x_34, x_7); return x_35; } @@ -24029,7 +24354,7 @@ else lean_object* x_36; lean_object* x_37; lean_dec(x_13); lean_dec(x_2); -x_36 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_36 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_37 = l_Lean_Parser_ParserState_mkNode(x_12, x_36, x_7); return x_37; } @@ -24039,88 +24364,88 @@ else lean_object* x_38; lean_object* x_39; lean_dec(x_9); lean_dec(x_2); -x_38 = l_Lean_Parser_Term_array___elambda__1___closed__2; +x_38 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; x_39 = l_Lean_Parser_ParserState_mkNode(x_8, x_38, x_7); return x_39; } } } } -lean_object* _init_l_Lean_Parser_Term_array___closed__1() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__1() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_list___elambda__1___closed__3; +x_1 = l_Lean_Parser_Term_listLit___elambda__1___closed__3; x_2 = l_Lean_Parser_Term_proj___closed__2; x_3 = l_Lean_Parser_symbolNoWsInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array___closed__2() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_array___closed__1; +x_1 = l_Lean_Parser_Term_arrayRef___closed__1; x_2 = l_Lean_Parser_Term_instBinder___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array___closed__3() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__3() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_epsilonInfo; -x_2 = l_Lean_Parser_Term_array___closed__2; +x_2 = l_Lean_Parser_Term_arrayRef___closed__2; x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array___closed__4() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_array___elambda__1___closed__2; -x_2 = l_Lean_Parser_Term_array___closed__3; +x_1 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; +x_2 = l_Lean_Parser_Term_arrayRef___closed__3; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array___closed__5() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__5() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_array___elambda__1), 3, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_arrayRef___elambda__1), 3, 0); return x_1; } } -lean_object* _init_l_Lean_Parser_Term_array___closed__6() { +lean_object* _init_l_Lean_Parser_Term_arrayRef___closed__6() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Term_array___closed__4; -x_2 = l_Lean_Parser_Term_array___closed__5; +x_1 = l_Lean_Parser_Term_arrayRef___closed__4; +x_2 = l_Lean_Parser_Term_arrayRef___closed__5; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); return x_3; } } -lean_object* _init_l_Lean_Parser_Term_array() { +lean_object* _init_l_Lean_Parser_Term_arrayRef() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Term_array___closed__6; +x_1 = l_Lean_Parser_Term_arrayRef___closed__6; return x_1; } } -lean_object* l___regBuiltinParser_Lean_Parser_Term_array(lean_object* x_1) { +lean_object* l___regBuiltinParser_Lean_Parser_Term_arrayRef(lean_object* x_1) { _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Parser_builtinTermParsingTable; -x_3 = l_Lean_Parser_Term_array___elambda__1___closed__2; -x_4 = l_Lean_Parser_Term_array; +x_3 = l_Lean_Parser_Term_arrayRef___elambda__1___closed__2; +x_4 = l_Lean_Parser_Term_arrayRef; x_5 = l_Lean_Parser_addBuiltinTrailingParser(x_2, x_3, x_4, x_1); return x_5; } @@ -29299,55 +29624,83 @@ l_Lean_Parser_Term_subtype = _init_l_Lean_Parser_Term_subtype(); lean_mark_persistent(l_Lean_Parser_Term_subtype); w = l___regBuiltinParser_Lean_Parser_Term_subtype(w); if (lean_io_result_is_error(w)) return w; -l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1(); -lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__1); -l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__2 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__2(); -lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__2); -l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__3 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__3(); -lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__3); -l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4(); -lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_list___elambda__1___spec__2___closed__4); -l_Lean_Parser_Term_list___elambda__1___closed__1 = _init_l_Lean_Parser_Term_list___elambda__1___closed__1(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__1); -l_Lean_Parser_Term_list___elambda__1___closed__2 = _init_l_Lean_Parser_Term_list___elambda__1___closed__2(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__2); -l_Lean_Parser_Term_list___elambda__1___closed__3 = _init_l_Lean_Parser_Term_list___elambda__1___closed__3(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__3); -l_Lean_Parser_Term_list___elambda__1___closed__4 = _init_l_Lean_Parser_Term_list___elambda__1___closed__4(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__4); -l_Lean_Parser_Term_list___elambda__1___closed__5 = _init_l_Lean_Parser_Term_list___elambda__1___closed__5(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__5); -l_Lean_Parser_Term_list___elambda__1___closed__6 = _init_l_Lean_Parser_Term_list___elambda__1___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__6); -l_Lean_Parser_Term_list___elambda__1___closed__7 = _init_l_Lean_Parser_Term_list___elambda__1___closed__7(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__7); -l_Lean_Parser_Term_list___elambda__1___closed__8 = _init_l_Lean_Parser_Term_list___elambda__1___closed__8(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__8); -l_Lean_Parser_Term_list___elambda__1___closed__9 = _init_l_Lean_Parser_Term_list___elambda__1___closed__9(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__9); -l_Lean_Parser_Term_list___elambda__1___closed__10 = _init_l_Lean_Parser_Term_list___elambda__1___closed__10(); -lean_mark_persistent(l_Lean_Parser_Term_list___elambda__1___closed__10); -l_Lean_Parser_Term_list___closed__1 = _init_l_Lean_Parser_Term_list___closed__1(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__1); -l_Lean_Parser_Term_list___closed__2 = _init_l_Lean_Parser_Term_list___closed__2(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__2); -l_Lean_Parser_Term_list___closed__3 = _init_l_Lean_Parser_Term_list___closed__3(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__3); -l_Lean_Parser_Term_list___closed__4 = _init_l_Lean_Parser_Term_list___closed__4(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__4); -l_Lean_Parser_Term_list___closed__5 = _init_l_Lean_Parser_Term_list___closed__5(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__5); -l_Lean_Parser_Term_list___closed__6 = _init_l_Lean_Parser_Term_list___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__6); -l_Lean_Parser_Term_list___closed__7 = _init_l_Lean_Parser_Term_list___closed__7(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__7); -l_Lean_Parser_Term_list___closed__8 = _init_l_Lean_Parser_Term_list___closed__8(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__8); -l_Lean_Parser_Term_list___closed__9 = _init_l_Lean_Parser_Term_list___closed__9(); -lean_mark_persistent(l_Lean_Parser_Term_list___closed__9); -l_Lean_Parser_Term_list = _init_l_Lean_Parser_Term_list(); -lean_mark_persistent(l_Lean_Parser_Term_list); -w = l___regBuiltinParser_Lean_Parser_Term_list(w); +l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1(); +lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__1); +l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__2 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__2(); +lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__2); +l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__3 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__3(); +lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__3); +l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4 = _init_l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4(); +lean_mark_persistent(l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_listLit___elambda__1___spec__2___closed__4); +l_Lean_Parser_Term_listLit___elambda__1___closed__1 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__1); +l_Lean_Parser_Term_listLit___elambda__1___closed__2 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__2); +l_Lean_Parser_Term_listLit___elambda__1___closed__3 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__3); +l_Lean_Parser_Term_listLit___elambda__1___closed__4 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__4); +l_Lean_Parser_Term_listLit___elambda__1___closed__5 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__5); +l_Lean_Parser_Term_listLit___elambda__1___closed__6 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__6); +l_Lean_Parser_Term_listLit___elambda__1___closed__7 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__7); +l_Lean_Parser_Term_listLit___elambda__1___closed__8 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__8); +l_Lean_Parser_Term_listLit___elambda__1___closed__9 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__9(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__9); +l_Lean_Parser_Term_listLit___elambda__1___closed__10 = _init_l_Lean_Parser_Term_listLit___elambda__1___closed__10(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___elambda__1___closed__10); +l_Lean_Parser_Term_listLit___closed__1 = _init_l_Lean_Parser_Term_listLit___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__1); +l_Lean_Parser_Term_listLit___closed__2 = _init_l_Lean_Parser_Term_listLit___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__2); +l_Lean_Parser_Term_listLit___closed__3 = _init_l_Lean_Parser_Term_listLit___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__3); +l_Lean_Parser_Term_listLit___closed__4 = _init_l_Lean_Parser_Term_listLit___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__4); +l_Lean_Parser_Term_listLit___closed__5 = _init_l_Lean_Parser_Term_listLit___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__5); +l_Lean_Parser_Term_listLit___closed__6 = _init_l_Lean_Parser_Term_listLit___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__6); +l_Lean_Parser_Term_listLit___closed__7 = _init_l_Lean_Parser_Term_listLit___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__7); +l_Lean_Parser_Term_listLit___closed__8 = _init_l_Lean_Parser_Term_listLit___closed__8(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__8); +l_Lean_Parser_Term_listLit___closed__9 = _init_l_Lean_Parser_Term_listLit___closed__9(); +lean_mark_persistent(l_Lean_Parser_Term_listLit___closed__9); +l_Lean_Parser_Term_listLit = _init_l_Lean_Parser_Term_listLit(); +lean_mark_persistent(l_Lean_Parser_Term_listLit); +w = l___regBuiltinParser_Lean_Parser_Term_listLit(w); +if (lean_io_result_is_error(w)) return w; +l_Lean_Parser_Term_arrayLit___elambda__1___closed__1 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__1); +l_Lean_Parser_Term_arrayLit___elambda__1___closed__2 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__2); +l_Lean_Parser_Term_arrayLit___elambda__1___closed__3 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__3); +l_Lean_Parser_Term_arrayLit___elambda__1___closed__4 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__4); +l_Lean_Parser_Term_arrayLit___elambda__1___closed__5 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__5); +l_Lean_Parser_Term_arrayLit___elambda__1___closed__6 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__6); +l_Lean_Parser_Term_arrayLit___elambda__1___closed__7 = _init_l_Lean_Parser_Term_arrayLit___elambda__1___closed__7(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___elambda__1___closed__7); +l_Lean_Parser_Term_arrayLit___closed__1 = _init_l_Lean_Parser_Term_arrayLit___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___closed__1); +l_Lean_Parser_Term_arrayLit___closed__2 = _init_l_Lean_Parser_Term_arrayLit___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___closed__2); +l_Lean_Parser_Term_arrayLit___closed__3 = _init_l_Lean_Parser_Term_arrayLit___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___closed__3); +l_Lean_Parser_Term_arrayLit___closed__4 = _init_l_Lean_Parser_Term_arrayLit___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___closed__4); +l_Lean_Parser_Term_arrayLit___closed__5 = _init_l_Lean_Parser_Term_arrayLit___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit___closed__5); +l_Lean_Parser_Term_arrayLit = _init_l_Lean_Parser_Term_arrayLit(); +lean_mark_persistent(l_Lean_Parser_Term_arrayLit); +w = l___regBuiltinParser_Lean_Parser_Term_arrayLit(w); if (lean_io_result_is_error(w)) return w; l_Lean_Parser_Term_explicit___elambda__1___closed__1 = _init_l_Lean_Parser_Term_explicit___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_explicit___elambda__1___closed__1); @@ -30285,29 +30638,29 @@ l_Lean_Parser_Term_arrow = _init_l_Lean_Parser_Term_arrow(); lean_mark_persistent(l_Lean_Parser_Term_arrow); w = l___regBuiltinParser_Lean_Parser_Term_arrow(w); if (lean_io_result_is_error(w)) return w; -l_Lean_Parser_Term_array___elambda__1___closed__1 = _init_l_Lean_Parser_Term_array___elambda__1___closed__1(); -lean_mark_persistent(l_Lean_Parser_Term_array___elambda__1___closed__1); -l_Lean_Parser_Term_array___elambda__1___closed__2 = _init_l_Lean_Parser_Term_array___elambda__1___closed__2(); -lean_mark_persistent(l_Lean_Parser_Term_array___elambda__1___closed__2); -l_Lean_Parser_Term_array___elambda__1___closed__3 = _init_l_Lean_Parser_Term_array___elambda__1___closed__3(); -lean_mark_persistent(l_Lean_Parser_Term_array___elambda__1___closed__3); -l_Lean_Parser_Term_array___elambda__1___closed__4 = _init_l_Lean_Parser_Term_array___elambda__1___closed__4(); -lean_mark_persistent(l_Lean_Parser_Term_array___elambda__1___closed__4); -l_Lean_Parser_Term_array___closed__1 = _init_l_Lean_Parser_Term_array___closed__1(); -lean_mark_persistent(l_Lean_Parser_Term_array___closed__1); -l_Lean_Parser_Term_array___closed__2 = _init_l_Lean_Parser_Term_array___closed__2(); -lean_mark_persistent(l_Lean_Parser_Term_array___closed__2); -l_Lean_Parser_Term_array___closed__3 = _init_l_Lean_Parser_Term_array___closed__3(); -lean_mark_persistent(l_Lean_Parser_Term_array___closed__3); -l_Lean_Parser_Term_array___closed__4 = _init_l_Lean_Parser_Term_array___closed__4(); -lean_mark_persistent(l_Lean_Parser_Term_array___closed__4); -l_Lean_Parser_Term_array___closed__5 = _init_l_Lean_Parser_Term_array___closed__5(); -lean_mark_persistent(l_Lean_Parser_Term_array___closed__5); -l_Lean_Parser_Term_array___closed__6 = _init_l_Lean_Parser_Term_array___closed__6(); -lean_mark_persistent(l_Lean_Parser_Term_array___closed__6); -l_Lean_Parser_Term_array = _init_l_Lean_Parser_Term_array(); -lean_mark_persistent(l_Lean_Parser_Term_array); -w = l___regBuiltinParser_Lean_Parser_Term_array(w); +l_Lean_Parser_Term_arrayRef___elambda__1___closed__1 = _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___elambda__1___closed__1); +l_Lean_Parser_Term_arrayRef___elambda__1___closed__2 = _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___elambda__1___closed__2); +l_Lean_Parser_Term_arrayRef___elambda__1___closed__3 = _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___elambda__1___closed__3); +l_Lean_Parser_Term_arrayRef___elambda__1___closed__4 = _init_l_Lean_Parser_Term_arrayRef___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___elambda__1___closed__4); +l_Lean_Parser_Term_arrayRef___closed__1 = _init_l_Lean_Parser_Term_arrayRef___closed__1(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__1); +l_Lean_Parser_Term_arrayRef___closed__2 = _init_l_Lean_Parser_Term_arrayRef___closed__2(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__2); +l_Lean_Parser_Term_arrayRef___closed__3 = _init_l_Lean_Parser_Term_arrayRef___closed__3(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__3); +l_Lean_Parser_Term_arrayRef___closed__4 = _init_l_Lean_Parser_Term_arrayRef___closed__4(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__4); +l_Lean_Parser_Term_arrayRef___closed__5 = _init_l_Lean_Parser_Term_arrayRef___closed__5(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__5); +l_Lean_Parser_Term_arrayRef___closed__6 = _init_l_Lean_Parser_Term_arrayRef___closed__6(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef___closed__6); +l_Lean_Parser_Term_arrayRef = _init_l_Lean_Parser_Term_arrayRef(); +lean_mark_persistent(l_Lean_Parser_Term_arrayRef); +w = l___regBuiltinParser_Lean_Parser_Term_arrayRef(w); if (lean_io_result_is_error(w)) return w; l_Lean_Parser_Term_dollar___elambda__1___closed__1 = _init_l_Lean_Parser_Term_dollar___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Term_dollar___elambda__1___closed__1); diff --git a/src/stage0/Init/Lean/Parser/Transform.c b/src/stage0/Init/Lean/Parser/Transform.c index 6890beefc0..851ab7abbd 100644 --- a/src/stage0/Init/Lean/Parser/Transform.c +++ b/src/stage0/Init/Lean/Parser/Transform.c @@ -17,7 +17,6 @@ uint8_t lean_name_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Syntax_setTailInfo___rarg(lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_Array_get_x21(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Array_mkArray(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_declareLeadingBuiltinParser___closed__1; lean_object* l_Lean_Syntax_removeParen___closed__1; extern lean_object* l_Array_mforAux___main___at_Lean_Environment_displayStats___spec__9___closed__2; @@ -33,6 +32,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* l_Array_miterateAux___main___at_Lean_Syntax_manyToSepBy___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_mkSearchPathRef___closed__1; lean_object* l_Array_set_x21(lean_object*, lean_object*, lean_object*, lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); lean_object* l_Lean_Syntax_removeParen___closed__4; @@ -154,37 +154,39 @@ uint8_t x_3; x_3 = !lean_is_exclusive(x_1); if (x_3 == 0) { -lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; +lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; x_4 = lean_ctor_get(x_1, 1); x_5 = lean_box(0); x_6 = lean_unsigned_to_nat(0u); x_7 = lean_array_get(x_5, x_4, x_6); -x_8 = lean_unsigned_to_nat(1u); -x_9 = lean_mk_array(x_8, x_7); -x_10 = l_Array_miterateAux___main___at_Lean_Syntax_manyToSepBy___spec__1(x_2, x_4, x_4, x_8, x_9); +x_8 = l_Lean_mkSearchPathRef___closed__1; +x_9 = lean_array_push(x_8, x_7); +x_10 = lean_unsigned_to_nat(1u); +x_11 = l_Array_miterateAux___main___at_Lean_Syntax_manyToSepBy___spec__1(x_2, x_4, x_4, x_10, x_9); lean_dec(x_4); -lean_ctor_set(x_1, 1, x_10); +lean_ctor_set(x_1, 1, x_11); return x_1; } else { -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; lean_object* x_18; lean_object* x_19; -x_11 = lean_ctor_get(x_1, 0); -x_12 = lean_ctor_get(x_1, 1); +lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; +x_12 = lean_ctor_get(x_1, 0); +x_13 = lean_ctor_get(x_1, 1); +lean_inc(x_13); lean_inc(x_12); -lean_inc(x_11); lean_dec(x_1); -x_13 = lean_box(0); -x_14 = lean_unsigned_to_nat(0u); -x_15 = lean_array_get(x_13, x_12, x_14); -x_16 = lean_unsigned_to_nat(1u); -x_17 = lean_mk_array(x_16, x_15); -x_18 = l_Array_miterateAux___main___at_Lean_Syntax_manyToSepBy___spec__1(x_2, x_12, x_12, x_16, x_17); -lean_dec(x_12); -x_19 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_19, 0, x_11); -lean_ctor_set(x_19, 1, x_18); -return x_19; +x_14 = lean_box(0); +x_15 = lean_unsigned_to_nat(0u); +x_16 = lean_array_get(x_14, x_13, x_15); +x_17 = l_Lean_mkSearchPathRef___closed__1; +x_18 = lean_array_push(x_17, x_16); +x_19 = lean_unsigned_to_nat(1u); +x_20 = l_Array_miterateAux___main___at_Lean_Syntax_manyToSepBy___spec__1(x_2, x_13, x_13, x_19, x_18); +lean_dec(x_13); +x_21 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_21, 0, x_12); +lean_ctor_set(x_21, 1, x_20); +return x_21; } } else diff --git a/src/stage0/Init/Lean/Path.c b/src/stage0/Init/Lean/Path.c index b01422f9f4..45416d73dd 100644 --- a/src/stage0/Init/Lean/Path.c +++ b/src/stage0/Init/Lean/Path.c @@ -24,7 +24,6 @@ lean_object* l_Lean_moduleNameOfFileName___closed__5; lean_object* lean_nat_sub(lean_object*, lean_object*); lean_object* l_IO_isDir___at_Lean_getBuiltinSearchPath___spec__3___boxed(lean_object*, lean_object*); lean_object* l_Lean_getSearchPathFromEnv___closed__1; -lean_object* l_Array_mkArray(lean_object*, lean_object*, lean_object*); extern lean_object* l_List_repr___rarg___closed__3; lean_object* l_Lean_moduleNameOfFileName___closed__4; lean_object* l_Lean_findOLean(lean_object*, lean_object*); @@ -79,12 +78,14 @@ lean_object* l_Lean_findLeanFile___closed__2; lean_object* l_IO_getEnv___at_Lean_getSearchPathFromEnv___spec__1___boxed(lean_object*, lean_object*); lean_object* l_Lean_findLeanFile(lean_object*, lean_object*, lean_object*); uint8_t lean_nat_dec_eq(lean_object*, lean_object*); +lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_findAtSearchPath___closed__2; lean_object* l_Lean_searchPathRef; lean_object* l_IO_getEnv___at_Lean_getSearchPathFromEnv___spec__1(lean_object*, lean_object*); lean_object* l_Lean_modNameToFileName___main(lean_object*); lean_object* l_IO_isDir___at_Lean_getBuiltinSearchPath___spec__3(lean_object*, lean_object*); uint32_t lean_string_utf8_get(lean_object*, lean_object*); +lean_object* l_Lean_mkSearchPathRef___closed__1; lean_object* l_IO_fileExists___at_Lean_findFile___spec__1___boxed(lean_object*, lean_object*); uint8_t lean_string_dec_eq(lean_object*, lean_object*); lean_object* l_IO_Prim_mkRef(lean_object*, lean_object*, lean_object*); @@ -225,6 +226,15 @@ return x_14; } } } +lean_object* _init_l_Lean_mkSearchPathRef___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(1u); +x_2 = lean_mk_empty_array_with_capacity(x_1); +return x_2; +} +} lean_object* l_Lean_mkSearchPathRef(lean_object* x_1) { _start: { @@ -241,8 +251,8 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_obj x_5 = lean_ctor_get(x_3, 0); x_6 = lean_box(0); lean_ctor_set(x_3, 0, x_6); -x_7 = lean_unsigned_to_nat(1u); -x_8 = lean_mk_array(x_7, x_5); +x_7 = l_Lean_mkSearchPathRef___closed__1; +x_8 = lean_array_push(x_7, x_5); x_9 = lean_io_mk_ref(x_8, x_3); return x_9; } @@ -258,8 +268,8 @@ x_12 = lean_box(0); x_13 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_13, 0, x_12); lean_ctor_set(x_13, 1, x_11); -x_14 = lean_unsigned_to_nat(1u); -x_15 = lean_mk_array(x_14, x_10); +x_14 = l_Lean_mkSearchPathRef___closed__1; +x_15 = lean_array_push(x_14, x_10); x_16 = lean_io_mk_ref(x_15, x_13); return x_16; } @@ -3584,6 +3594,8 @@ l___private_Init_Lean_Path_2__searchPathSep___closed__1 = _init_l___private_Init lean_mark_persistent(l___private_Init_Lean_Path_2__searchPathSep___closed__1); l___private_Init_Lean_Path_2__searchPathSep = _init_l___private_Init_Lean_Path_2__searchPathSep(); lean_mark_persistent(l___private_Init_Lean_Path_2__searchPathSep); +l_Lean_mkSearchPathRef___closed__1 = _init_l_Lean_mkSearchPathRef___closed__1(); +lean_mark_persistent(l_Lean_mkSearchPathRef___closed__1); w = l_Lean_mkSearchPathRef(w); if (lean_io_result_is_error(w)) return w; l_Lean_searchPathRef = lean_io_result_get_value(w); diff --git a/src/stage0/Init/Lean/Syntax.c b/src/stage0/Init/Lean/Syntax.c index ab3c801da3..21b182a8e7 100644 --- a/src/stage0/Init/Lean/Syntax.c +++ b/src/stage0/Init/Lean/Syntax.c @@ -41,7 +41,6 @@ lean_object* l_Lean_Syntax_setArg(lean_object*); extern lean_object* l_Lean_Format_paren___closed__2; lean_object* l___private_Init_Lean_Syntax_4__reprintLeaf___boxed(lean_object*, lean_object*); lean_object* l_Lean_unreachIsNodeOther(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Array_mkArray(lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Syntax_3__updateLast___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Lean_Syntax_3__updateLast___main___at_Lean_Syntax_setTailInfoAux___main___spec__1(lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_Syntax_updateLeading___spec__2(lean_object*); @@ -151,6 +150,7 @@ lean_object* l_Lean_SyntaxNode_getArg___rarg(lean_object*, lean_object*); lean_object* l_Lean_mkAtom(lean_object*); uint8_t l_UInt32_decLe(uint32_t, uint32_t); uint8_t l_Lean_Syntax_isOfKind___rarg(lean_object*, lean_object*); +lean_object* l_Lean_mkOptionalNode___rarg___closed__1; lean_object* l_Lean_Syntax_mreplace___main___at_Lean_Syntax_updateLeading___spec__1___rarg(lean_object*, lean_object*); extern lean_object* l_Lean_Format_paren___closed__1; lean_object* l_Lean_Syntax_isIdOrAtom(lean_object*); @@ -193,6 +193,7 @@ lean_object* l_Lean_Syntax_asNode(lean_object*); lean_object* l_Lean_Syntax_mreplace___main___rarg___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* l_Array_ummapAux___main___at_Lean_Syntax_updateLeading___spec__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_getTailInfo___rarg(lean_object*); +lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); lean_object* lean_mk_syntax_ident(lean_object*); lean_object* l_Lean_Syntax_isNatLit___rarg(lean_object*); lean_object* l___private_Init_Lean_Syntax_6__decodeOctalLitAux___main___boxed(lean_object*, lean_object*, lean_object*); @@ -4755,6 +4756,15 @@ x_2 = lean_alloc_closure((void*)(l_Lean_mkNullNode___rarg), 1, 0); return x_2; } } +lean_object* _init_l_Lean_mkOptionalNode___rarg___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = lean_unsigned_to_nat(1u); +x_2 = lean_mk_empty_array_with_capacity(x_1); +return x_2; +} +} lean_object* l_Lean_mkOptionalNode___rarg(lean_object* x_1) { _start: { @@ -4770,8 +4780,8 @@ lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_obj x_3 = lean_ctor_get(x_1, 0); lean_inc(x_3); lean_dec(x_1); -x_4 = lean_unsigned_to_nat(1u); -x_5 = lean_mk_array(x_4, x_3); +x_4 = l_Lean_mkOptionalNode___rarg___closed__1; +x_5 = lean_array_push(x_4, x_3); x_6 = l_Lean_nullKind; x_7 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_7, 0, x_6); @@ -4795,8 +4805,8 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; x_4 = lean_alloc_ctor(2, 2, 0); lean_ctor_set(x_4, 0, x_3); lean_ctor_set(x_4, 1, x_2); -x_5 = lean_unsigned_to_nat(1u); -x_6 = lean_mk_array(x_5, x_4); +x_5 = l_Lean_mkOptionalNode___rarg___closed__1; +x_6 = lean_array_push(x_5, x_4); x_7 = lean_alloc_ctor(1, 2, 0); lean_ctor_set(x_7, 0, x_1); lean_ctor_set(x_7, 1, x_6); @@ -5965,6 +5975,8 @@ l_Lean_Syntax_Lean_HasFormat___closed__1 = _init_l_Lean_Syntax_Lean_HasFormat___ lean_mark_persistent(l_Lean_Syntax_Lean_HasFormat___closed__1); l_Lean_Syntax_HasToString___closed__1 = _init_l_Lean_Syntax_HasToString___closed__1(); lean_mark_persistent(l_Lean_Syntax_HasToString___closed__1); +l_Lean_mkOptionalNode___rarg___closed__1 = _init_l_Lean_mkOptionalNode___rarg___closed__1(); +lean_mark_persistent(l_Lean_mkOptionalNode___rarg___closed__1); l___private_Init_Lean_Syntax_9__decodeNatLitVal___closed__1 = _init_l___private_Init_Lean_Syntax_9__decodeNatLitVal___closed__1(); lean_mark_persistent(l___private_Init_Lean_Syntax_9__decodeNatLitVal___closed__1); return w; diff --git a/src/stage0/Init/Lean/TypeClass/Synth.c b/src/stage0/Init/Lean/TypeClass/Synth.c index 58299d76a3..db60c859f7 100644 --- a/src/stage0/Init/Lean/TypeClass/Synth.c +++ b/src/stage0/Init/Lean/TypeClass/Synth.c @@ -70,7 +70,6 @@ lean_object* l_Lean_TypeClass_constNameToTypedExpr___closed__1; lean_object* l_Lean_TypeClass_synthCore___boxed(lean_object*, lean_object*); lean_object* lean_expr_mk_fvar(lean_object*); lean_object* lean_local_ctx_mk_local_decl(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t); -lean_object* l_Array_mkEmpty(lean_object*, lean_object*); lean_object* l_List_foldl___main___at_Lean_mkApp___spec__1(lean_object*, lean_object*); lean_object* l_Array_anyMAux___main___at_Lean_TypeClass_newAnswer___spec__4___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_LocalContext_mkLambda(lean_object*, lean_object*, lean_object*); @@ -95,6 +94,7 @@ lean_object* l_Lean_TypeClass_resume___closed__1; lean_object* l_Lean_TypeClass_synth___closed__1; lean_object* lean_string_append(lean_object*, lean_object*); uint8_t l_Array_anyMAux___main___at_Lean_TypeClass_newAnswer___spec__4(lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_mkOptionalNode___rarg___closed__1; extern lean_object* l_List_reprAux___main___rarg___closed__1; size_t l_USize_add(size_t, size_t); lean_object* l_Lean_TypeClass_introduceLocals___main(lean_object*, lean_object*, lean_object*, lean_object*); @@ -113,7 +113,6 @@ lean_object* l_Lean_TypeClass_generate___closed__2; uint8_t lean_nat_dec_eq(lean_object*, lean_object*); uint8_t lean_has_out_params(lean_object*, lean_object*); lean_object* l_Lean_TypeClass_generate(lean_object*); -lean_object* l_Lean_TypeClass_newSubgoal___closed__4; uint8_t l_Array_isEmpty___rarg(lean_object*); lean_object* lean_instantiate_type_lparams(lean_object*, lean_object*); lean_object* l_Array_push(lean_object*, lean_object*, lean_object*); @@ -1010,15 +1009,6 @@ x_1 = lean_mk_string("found non-class goal `"); return x_1; } } -lean_object* _init_l_Lean_TypeClass_newSubgoal___closed__4() { -_start: -{ -lean_object* x_1; lean_object* x_2; -x_1 = lean_unsigned_to_nat(1u); -x_2 = lean_mk_empty_array_with_capacity(x_1); -return x_2; -} -} lean_object* l_Lean_TypeClass_newSubgoal(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { @@ -1145,7 +1135,7 @@ x_42 = l_List_map___main___at_Lean_TypeClass_newSubgoal___spec__1(x_41); x_43 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_43, 0, x_40); lean_ctor_set(x_43, 1, x_42); -x_44 = l_Lean_TypeClass_newSubgoal___closed__4; +x_44 = l_Lean_mkOptionalNode___rarg___closed__1; x_45 = lean_array_push(x_44, x_1); x_46 = l_Array_empty___closed__1; x_47 = lean_alloc_ctor(0, 2, 0); @@ -1184,7 +1174,7 @@ x_57 = l_List_map___main___at_Lean_TypeClass_newSubgoal___spec__1(x_56); x_58 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_58, 0, x_55); lean_ctor_set(x_58, 1, x_57); -x_59 = l_Lean_TypeClass_newSubgoal___closed__4; +x_59 = l_Lean_mkOptionalNode___rarg___closed__1; x_60 = lean_array_push(x_59, x_1); x_61 = l_Array_empty___closed__1; x_62 = lean_alloc_ctor(0, 2, 0); @@ -1326,7 +1316,7 @@ x_97 = l_List_map___main___at_Lean_TypeClass_newSubgoal___spec__1(x_96); x_98 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_98, 0, x_95); lean_ctor_set(x_98, 1, x_97); -x_99 = l_Lean_TypeClass_newSubgoal___closed__4; +x_99 = l_Lean_mkOptionalNode___rarg___closed__1; x_100 = lean_array_push(x_99, x_1); x_101 = l_Array_empty___closed__1; x_102 = lean_alloc_ctor(0, 2, 0); @@ -7959,8 +7949,6 @@ l_Lean_TypeClass_newSubgoal___closed__2 = _init_l_Lean_TypeClass_newSubgoal___cl lean_mark_persistent(l_Lean_TypeClass_newSubgoal___closed__2); l_Lean_TypeClass_newSubgoal___closed__3 = _init_l_Lean_TypeClass_newSubgoal___closed__3(); lean_mark_persistent(l_Lean_TypeClass_newSubgoal___closed__3); -l_Lean_TypeClass_newSubgoal___closed__4 = _init_l_Lean_TypeClass_newSubgoal___closed__4(); -lean_mark_persistent(l_Lean_TypeClass_newSubgoal___closed__4); l_Lean_TypeClass_introduceLocals___main___closed__1 = _init_l_Lean_TypeClass_introduceLocals___main___closed__1(); lean_mark_persistent(l_Lean_TypeClass_introduceLocals___main___closed__1); l_Lean_TypeClass_introduceLocals___main___closed__2 = _init_l_Lean_TypeClass_introduceLocals___main___closed__2();