diff --git a/stage0/src/Lean/Parser/Tactic.lean b/stage0/src/Lean/Parser/Tactic.lean index 59e813d3b3..e1a44fc336 100644 --- a/stage0/src/Lean/Parser/Tactic.lean +++ b/stage0/src/Lean/Parser/Tactic.lean @@ -74,7 +74,6 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match def withIds : Parser := optional (" with " >> many1 ident') @[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds -def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true @[builtinTacticParser] def paren := parser! "(" >> seq1 >> ")" @[builtinTacticParser] def nestedTactic := tacticSeqBracketed @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1 diff --git a/stage0/src/Lean/Parser/Term.lean b/stage0/src/Lean/Parser/Term.lean index 346e4b0cf4..7baa65f125 100644 --- a/stage0/src/Lean/Parser/Term.lean +++ b/stage0/src/Lean/Parser/Term.lean @@ -28,6 +28,10 @@ def tacticSeqBracketed : Parser := parser! "{" >> sepBy tacticParser "; " true >> "}" def tacticSeq := nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented + +/- Raw sequence for quotation and grouping -/ +def seq1 := parser! sepBy1 tacticParser "; " true + end Tactic def darrow : Parser := " => " diff --git a/stage0/stdlib/Lean/Parser/Syntax.c b/stage0/stdlib/Lean/Parser/Syntax.c index 51440a0e83..e4500063f5 100644 --- a/stage0/stdlib/Lean/Parser/Syntax.c +++ b/stage0/stdlib/Lean/Parser/Syntax.c @@ -430,6 +430,7 @@ lean_object* l_Lean_Parser_Syntax_ident___closed__5; lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__6; lean_object* l_Lean_Parser_Command_notation___closed__6; lean_object* l_Lean_Parser_Command_infixl_formatter___closed__2; +extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__3; lean_object* l_Lean_Parser_Command_mixfix___closed__9; lean_object* l_Lean_Parser_Syntax_try_parenthesizer___closed__4; lean_object* l_Lean_Parser_maxSymbol_formatter___closed__3; @@ -986,7 +987,6 @@ lean_object* l_Lean_Parser_Command_mixfix___closed__5; lean_object* l_Lean_Parser_Syntax_cat_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Command_elab__rules___elambda__1___closed__2; lean_object* l_Lean_Parser_Command_syntaxAbbrev___closed__3; -extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__4; lean_object* l_Lean_Parser_Command_notation_formatter___closed__4; extern lean_object* l_Lean_Parser_Term_str_parenthesizer___closed__1; lean_object* l_Lean_Parser_Syntax_notFollowedBy___closed__7; @@ -23476,7 +23476,7 @@ lean_inc(x_23); if (lean_obj_tag(x_23) == 0) { lean_object* x_24; lean_object* x_25; lean_object* x_26; -x_24 = l_Lean_Parser_Tactic_seq1Unbox___closed__4; +x_24 = l_Lean_Parser_Tactic_seq1Unbox___closed__3; lean_inc(x_1); x_25 = l_Lean_Parser_toggleInsideQuotFn(x_24, x_1, x_22); x_26 = lean_ctor_get(x_25, 3); diff --git a/stage0/stdlib/Lean/Parser/Tactic.c b/stage0/stdlib/Lean/Parser/Tactic.c index c7a70c1633..f5640a6762 100644 --- a/stage0/stdlib/Lean/Parser/Tactic.c +++ b/stage0/stdlib/Lean/Parser/Tactic.c @@ -117,6 +117,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlt___closed__6; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__5; lean_object* l_Lean_Parser_Tactic_locationWildcard_parenthesizer___closed__2; +lean_object* l_Lean_Parser_Tactic_seq1_formatter___closed__3; extern lean_object* l_Lean_Parser_notFollowedByFn___closed__1; lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_traceState_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -130,6 +131,7 @@ lean_object* l_Lean_Parser_Tactic_matchAlts_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_orelse___closed__1; lean_object* l_Lean_Parser_Tactic_failIfSuccess___closed__6; lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2; lean_object* l_Lean_Parser_Tactic_underscore___closed__2; lean_object* l_Lean_Parser_Tactic_location___closed__7; lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__9; @@ -170,7 +172,6 @@ lean_object* l___regBuiltinParser_Lean_Parser_Tactic_admit(lean_object*); lean_object* l_Lean_Parser_Tactic_rewriteSeq___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_intro_formatter___closed__5; lean_object* l_Lean_Parser_Tactic_admit; -extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__2; extern lean_object* l_Lean_Parser_Term_show___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_case_formatter___closed__4; lean_object* l___regBuiltin_Lean_Parser_Tactic_rewriteSeq_formatter___closed__1; @@ -260,6 +261,7 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_have_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_change_parenthesizer___closed__3; lean_object* l_Lean_Parser_Tactic_injection___closed__8; lean_object* l_Lean_Parser_Tactic_changeWith___closed__5; +extern lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_matchAlts___closed__1; lean_object* l_Lean_Parser_Tactic_paren_parenthesizer___closed__2; lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*); @@ -333,7 +335,7 @@ lean_object* lean_array_get_size(lean_object*); lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__3; lean_object* l_Lean_Parser_Tactic_location___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_let___elambda__1___closed__1; -lean_object* l_Lean_Parser_Tactic_seq1; +extern lean_object* l_Lean_Parser_Tactic_seq1; extern lean_object* l_Lean_Parser_Term_subtype_formatter___closed__6; lean_object* l_Lean_Parser_Tactic_refine_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_revert_formatter(lean_object*); @@ -385,6 +387,7 @@ lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1(lean_object*, lean_obj lean_object* l_Lean_Parser_Tactic_revert___closed__1; lean_object* l_Lean_Parser_Tactic_location___elambda__1___closed__4; lean_object* l_Lean_Parser_Tactic_skip___closed__1; +lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3; lean_object* l_Lean_Parser_Tactic_intro___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_sufficesDecl___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_rwRule_formatter___closed__3; @@ -554,6 +557,7 @@ lean_object* l_Lean_Parser_Tactic_clear___closed__3; lean_object* l_Lean_Parser_Tactic_cases___elambda__1___closed__8; lean_object* l_Lean_Parser_Tactic_refine___elambda__1___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Tactic_generalize(lean_object*); +extern lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__3; extern lean_object* l_Lean_Parser_identNoAntiquot___closed__1; lean_object* l_Lean_Parser_Tactic_intros___closed__8; lean_object* l_Lean_Parser_Tactic_allGoals___elambda__1___closed__3; @@ -734,7 +738,6 @@ lean_object* l_Lean_Parser_Tactic_revert___closed__5; extern lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__2; lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__9; -extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_match_parenthesizer___closed__7; lean_object* l_Lean_Parser_Tactic_rwRuleSeq_formatter___closed__4; lean_object* l_Lean_Parser_Tactic_induction_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -971,7 +974,6 @@ lean_object* l___regBuiltin_Lean_Parser_Tactic_intros_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_apply; extern lean_object* l_Lean_Parser_antiquotNestedExpr_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_rwRuleSeq_formatter___closed__2; -lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_assumption___closed__5; lean_object* l___regBuiltin_Lean_Parser_Tactic_orelse_formatter(lean_object*); lean_object* l_Lean_Parser_Tactic_changeWith_formatter___closed__2; @@ -1328,7 +1330,6 @@ lean_object* l_Lean_Parser_Tactic_show_formatter___closed__2; lean_object* l___regBuiltin_Lean_Parser_Tactic_revert_parenthesizer___closed__1; lean_object* l_Lean_Parser_Tactic_locationWildcard___elambda__1___closed__5; lean_object* l_Lean_Parser_Tactic_withAlts_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_Tactic_seq1___closed__1; lean_object* l_Lean_Parser_Tactic_intros; lean_object* l_Lean_Parser_Tactic_rewriteSeq___closed__3; lean_object* l_Lean_Parser_Tactic_matchAlt_formatter___closed__2; @@ -1460,7 +1461,6 @@ lean_object* l_Lean_Parser_Tactic_ident_x27_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_failIfSuccess___elambda__1___closed__8; lean_object* l_Lean_Parser_Tactic_refine_x21___elambda__1___closed__1; lean_object* l_Lean_Parser_Tactic_matchAlts___closed__2; -lean_object* l_Lean_Parser_Tactic_seq1___closed__2; lean_object* l_Lean_Parser_Tactic_exact_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__7; lean_object* l_Lean_Parser_Tactic_refine_x21___closed__6; @@ -1701,6 +1701,8 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(lean_object*, lean_object* l_Lean_Parser_Tactic_admit_formatter___closed__1; lean_object* l_Lean_Parser_Tactic_introMatch_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Tactic_rwRule___elambda__1___closed__3; +extern lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +lean_object* l_Lean_Parser_Tactic_seq1_formatter___closed__2; lean_object* l_Lean_Parser_Tactic_rewrite_formatter___closed__8; lean_object* l_Lean_Parser_andthenFn(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_paren_formatter(lean_object*); @@ -26014,49 +26016,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object* x_1, lean_object* x_2) { -_start: -{ -lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_3 = lean_ctor_get(x_2, 0); -lean_inc(x_3); -x_4 = lean_array_get_size(x_3); -lean_dec(x_3); -x_5 = 1; -x_6 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(x_5, x_1, x_2); -x_7 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; -x_8 = l_Lean_Parser_ParserState_mkNode(x_6, x_7, x_4); -return x_8; -} -} -lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1___elambda__1), 2, 0); -return x_1; -} -} -lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__2() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; -x_2 = l_Lean_Parser_Tactic_seq1___closed__1; -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_Tactic_seq1() { -_start: -{ -lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_seq1___closed__2; -return x_1; -} -} lean_object* _init_l_Lean_Parser_Tactic_paren___elambda__1___closed__1() { _start: { @@ -26602,6 +26561,21 @@ return x_7; lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__1() { _start: { +lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__1; +x_2 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__3; +x_3 = 1; +x_4 = lean_box(x_3); +x_5 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_formatter___boxed), 8, 3); +lean_closure_set(x_5, 0, x_1); +lean_closure_set(x_5, 1, x_2); +lean_closure_set(x_5, 2, x_4); +return x_5; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__2() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__4; x_2 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3; @@ -26611,13 +26585,27 @@ lean_closure_set(x_3, 1, x_2); return x_3; } } +lean_object* _init_l_Lean_Parser_Tactic_seq1_formatter___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +x_2 = lean_unsigned_to_nat(1024u); +x_3 = l_Lean_Parser_Tactic_seq1_formatter___closed__2; +x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3); +lean_closure_set(x_4, 0, x_1); +lean_closure_set(x_4, 1, x_2); +lean_closure_set(x_4, 2, x_3); +return x_4; +} +} lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; -x_7 = l_Lean_Parser_Tactic_seq1_formatter___closed__1; -x_8 = l_Lean_PrettyPrinter_Formatter_node_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5); +x_6 = l_Lean_Parser_Tactic_seq1_formatter___closed__1; +x_7 = l_Lean_Parser_Tactic_seq1_formatter___closed__3; +x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5); return x_8; } } @@ -26714,6 +26702,19 @@ return x_5; lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1() { _start: { +lean_object* x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__3; +x_2 = 1; +x_3 = lean_box(x_2); +x_4 = lean_alloc_closure((void*)(l_Lean_Parser_mkAntiquot_parenthesizer___rarg___boxed), 7, 2); +lean_closure_set(x_4, 0, x_1); +lean_closure_set(x_4, 1, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__2; x_2 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3; @@ -26723,13 +26724,27 @@ lean_closure_set(x_3, 1, x_2); return x_3; } } +lean_object* _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +x_2 = lean_unsigned_to_nat(1024u); +x_3 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2; +x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3); +lean_closure_set(x_4, 0, x_1); +lean_closure_set(x_4, 1, x_2); +lean_closure_set(x_4, 2, x_3); +return x_4; +} +} lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; -x_7 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1; -x_8 = l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5); +x_6 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1; +x_7 = l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3; +x_8 = l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5); return x_8; } } @@ -32194,12 +32209,6 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer__ res = l___regBuiltin_Lean_Parser_Tactic_injection_parenthesizer(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_Lean_Parser_Tactic_seq1___closed__1 = _init_l_Lean_Parser_Tactic_seq1___closed__1(); -lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__1); -l_Lean_Parser_Tactic_seq1___closed__2 = _init_l_Lean_Parser_Tactic_seq1___closed__2(); -lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__2); -l_Lean_Parser_Tactic_seq1 = _init_l_Lean_Parser_Tactic_seq1(); -lean_mark_persistent(l_Lean_Parser_Tactic_seq1); l_Lean_Parser_Tactic_paren___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_paren___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_paren___elambda__1___closed__1); l_Lean_Parser_Tactic_paren___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_paren___elambda__1___closed__2(); @@ -32225,6 +32234,10 @@ if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Parser_Tactic_seq1_formatter___closed__1 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__1); +l_Lean_Parser_Tactic_seq1_formatter___closed__2 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__2); +l_Lean_Parser_Tactic_seq1_formatter___closed__3 = _init_l_Lean_Parser_Tactic_seq1_formatter___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1_formatter___closed__3); l_Lean_Parser_Tactic_paren_formatter___closed__1 = _init_l_Lean_Parser_Tactic_paren_formatter___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_paren_formatter___closed__1); l_Lean_Parser_Tactic_paren_formatter___closed__2 = _init_l_Lean_Parser_Tactic_paren_formatter___closed__2(); @@ -32242,6 +32255,10 @@ if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__1); +l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__2); +l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3 = _init_l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1_parenthesizer___closed__3); l_Lean_Parser_Tactic_paren_parenthesizer___closed__1 = _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_paren_parenthesizer___closed__1); l_Lean_Parser_Tactic_paren_parenthesizer___closed__2 = _init_l_Lean_Parser_Tactic_paren_parenthesizer___closed__2(); diff --git a/stage0/stdlib/Lean/Parser/Term.c b/stage0/stdlib/Lean/Parser/Term.c index ef34a161f6..5a64fea896 100644 --- a/stage0/stdlib/Lean/Parser/Term.c +++ b/stage0/stdlib/Lean/Parser/Term.c @@ -36,6 +36,7 @@ lean_object* l_Lean_Parser_Term_nativeDecide___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_sufficesDecl_formatter___closed__1; lean_object* l_Lean_Parser_Term_letDecl_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_tupleTail_parenthesizer___closed__2; +lean_object* l_Lean_Parser_Tactic_seq1___closed__3; lean_object* l_Lean_Parser_Term_matchAlt___closed__5; lean_object* l_Lean_Parser_Term_instBinder_parenthesizer___closed__2; lean_object* l_Lean_Parser_Term_subtype_parenthesizer___closed__6; @@ -292,6 +293,7 @@ lean_object* l_Lean_Parser_Term_bracketedBinder(uint8_t); lean_object* l_Lean_Parser_Term_structInstLVal_parenthesizer___closed__5; lean_object* l_Lean_Parser_Term_structInst___closed__6; lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_unreachable_parenthesizer(lean_object*); lean_object* l___regBuiltin_Lean_Parser_Tactic_quot_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_explicitUniv_formatter___closed__1; @@ -340,6 +342,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__1; lean_object* l_Lean_Parser_Term_ellipsis_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_match_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__4; lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3; lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__2; @@ -618,10 +621,10 @@ lean_object* l_Lean_Parser_Term_infixR_parenthesizer___rarg(lean_object*, lean_o lean_object* l_Lean_Parser_Term_simpleBinder_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_attrInstance___closed__7; lean_object* l_Lean_Parser_Term_bracketedBinder_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Level_quot_formatter___closed__2; lean_object* l_Lean_Parser_Term_depArrow___elambda__1___closed__8; lean_object* l_Lean_Parser_Term_letrec_formatter___closed__5; +lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__1; lean_object* l_Lean_Parser_nonReservedSymbolFn(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_fromTerm___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__4; @@ -782,6 +785,7 @@ lean_object* l_Lean_Parser_Term_matchAlt_formatter(lean_object*, lean_object*, l lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__3; lean_object* l_Lean_Parser_Term_matchAlt___closed__7; lean_object* l_Lean_Parser_Term_syntheticHole_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_seq1; lean_object* l_Lean_Parser_Term_suffices___closed__8; lean_object* l_Lean_Parser_Term_subtype_formatter___closed__6; lean_object* l_Lean_Parser_Term_app___elambda__1(lean_object*, lean_object*); @@ -963,6 +967,7 @@ lean_object* l_Lean_Parser_mkAntiquot_formatter___boxed(lean_object*, lean_objec lean_object* l_Lean_Parser_leadingNode_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_forall_parenthesizer___closed__8; lean_object* l_Lean_Parser_Term_let_x21_formatter___closed__3; +lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_matchAlts_formatter___closed__7; lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_fun___elambda__1___spec__1(lean_object*, lean_object*); @@ -1319,6 +1324,7 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_forall___elambda lean_object* l_Lean_Parser_Term_mapRev_formatter___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_iff_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_listLit_formatter___closed__2; +lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__3; lean_object* l___regBuiltinParser_Lean_Parser_Term_parser_x21(lean_object*); lean_object* l_Lean_Parser_Term_subtype_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_fromTerm___closed__1; @@ -1350,6 +1356,7 @@ lean_object* l_Lean_Parser_Term_letrec___closed__2; lean_object* l_Lean_Parser_Term_return___closed__6; lean_object* l_Lean_Parser_Term_letIdLhs___closed__5; lean_object* l_Lean_Parser_Term_byTactic___elambda__1___closed__8; +lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1; lean_object* l_Lean_Parser_Level_quot___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_dbgTrace; lean_object* l_Lean_Parser_Term_match_parenthesizer___closed__2; @@ -1452,7 +1459,6 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__7; lean_object* l___regBuiltin_Lean_Parser_Term_dollarProj_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_fromTerm___closed__2; -lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__5; lean_object* l_Lean_Parser_symbolFn___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_funBinder_quot_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_type___elambda__1___closed__5; @@ -1725,6 +1731,7 @@ extern lean_object* l_Lean_strLitKind___closed__1; lean_object* l_Lean_Parser_Term_unreachable___closed__5; lean_object* l_Lean_PrettyPrinter_Formatter_toggleInsideQuot_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_seq_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_paren_formatter___closed__1; lean_object* l_Lean_Parser_Term_structInst_formatter___closed__1; lean_object* l_Lean_Parser_Term_structInstArrayRef___closed__1; @@ -1746,7 +1753,6 @@ lean_object* l_Lean_Parser_Term_subtype; lean_object* l_Lean_PrettyPrinter_Formatter_node_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Parser_Term_depArrow_formatter___closed__1; lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__9; -extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; lean_object* l_Lean_Parser_Term_nativeDecide___closed__5; lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__9; lean_object* l_Lean_Parser_Term_match_formatter___closed__1; @@ -2022,6 +2028,7 @@ lean_object* l_Lean_PrettyPrinter_Formatter_symbol_formatter(lean_object*, lean_ lean_object* l_Lean_Parser_Tactic_quot___closed__6; lean_object* l_Lean_Parser_Term_ne___closed__2; lean_object* l_Lean_Parser_Term_have_parenthesizer___closed__1; +lean_object* l_Lean_Parser_Tactic_seq1___closed__5; lean_object* l_Lean_Parser_Term_fcomp___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_type_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___closed__3; @@ -2326,7 +2333,6 @@ lean_object* l_Lean_Parser_Term_sort_formatter___closed__2; lean_object* l___regBuiltin_Lean_Parser_Term_and_formatter(lean_object*); lean_object* l_Lean_Parser_Term_instBinder_formatter___closed__4; lean_object* l_Lean_Parser_Term_not___elambda__1___closed__8; -lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_match__syntax___closed__4; lean_object* l_Lean_Parser_Term_ellipsis___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_show___closed__7; @@ -2625,6 +2631,7 @@ lean_object* l_Lean_Parser_Term_infixR(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_let_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_seqLeft___closed__3; lean_object* l_Lean_Parser_Term_band_formatter___closed__1; +lean_object* l_Lean_Parser_Tactic_seq1___closed__4; lean_object* l_Lean_Parser_Term_forall_formatter___closed__6; lean_object* l_Lean_Parser_charLit___elambda__1(lean_object*, lean_object*); lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Term_letrec___elambda__1___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -3220,6 +3227,7 @@ lean_object* l_Lean_Parser_Term_fun_parenthesizer___closed__3; lean_object* l___regBuiltin_Lean_Parser_Term_cdot_formatter(lean_object*); lean_object* l_Lean_Parser_Term_explicit_formatter___closed__3; lean_object* l_Lean_Parser_Term_not___closed__1; +lean_object* l_Lean_Parser_Tactic_seq1___closed__1; lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___closed__3; lean_object* l___regBuiltin_Lean_Parser_Level_quot_parenthesizer(lean_object*); lean_object* l_Lean_Parser_Term_uminus___closed__1; @@ -3446,6 +3454,7 @@ lean_object* l_Lean_Parser_Term_structInstField_parenthesizer___closed__4; lean_object* l_Lean_Parser_Term_fcomp___closed__3; lean_object* l_Lean_Parser_Term_sort_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_attrInstance_parenthesizer___closed__5; +lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(uint8_t, lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_anonymousCtor_parenthesizer___closed__2; extern lean_object* l_Lean_mkHole___closed__2; lean_object* l_Lean_Parser_Term_type___closed__5; @@ -3553,6 +3562,7 @@ lean_object* l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser lean_object* l_Lean_Parser_Term_bor___elambda__1___closed__4; lean_object* l_Lean_Parser_Term_attrInstance___elambda__1___closed__3; lean_object* l_Lean_Parser_Term_hole___closed__3; +lean_object* l_Lean_Parser_Tactic_seq1___closed__2; lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_explicitBinder_formatter___closed__7; lean_object* l_Lean_Parser_Term_byTactic___closed__6; @@ -3761,6 +3771,7 @@ lean_object* l_Lean_Parser_Term_matchAlts_formatter(uint8_t, lean_object*, lean_ lean_object* l_Lean_Parser_Term_binderTactic_parenthesizer___closed__3; lean_object* l_Lean_Parser_Level_quot_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_matchDiscr___closed__9; +lean_object* l_Lean_Parser_Tactic_seq1___closed__6; lean_object* l_Lean_Parser_Term_anonymousCtor___elambda__1___closed__5; lean_object* l_Lean_Parser_Term_proj___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_sort_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -3822,7 +3833,6 @@ lean_object* l_Lean_Parser_Term_syntheticHole_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_show_parenthesizer___closed__1; lean_object* l_Lean_Parser_Term_parenSpecial_formatter___closed__3; lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__1; -extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4; lean_object* l_Lean_Parser_Term_dollar___closed__1; lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__1; lean_object* l___regBuiltin_Lean_Parser_Term_match_formatter(lean_object*); @@ -4095,6 +4105,7 @@ lean_object* l_Lean_Parser_Term_explicitBinder_formatter___closed__5; lean_object* l_Lean_Parser_Term_namedArgument_formatter___closed__3; lean_object* l_Lean_Parser_Term_letrec_formatter___closed__8; lean_object* l_Lean_Parser_Term_let_x21___closed__4; +lean_object* l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; lean_object* l_Lean_Parser_Term_match_formatter___closed__5; lean_object* l___regBuiltin_Lean_Parser_Term_andthen_formatter(lean_object*); uint8_t l_Lean_Syntax_isIdent(lean_object*); @@ -4514,6 +4525,24 @@ x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic return x_7; } } +lean_object* _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("seq"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -4540,7 +4569,7 @@ lean_ctor_set(x_11, 0, x_10); lean_ctor_set(x_1, 4, x_11); x_12 = 0; x_13 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__1(x_12, x_1, x_2); -x_14 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_14 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_15 = l_Lean_Parser_ParserState_mkNode(x_13, x_14, x_4); return x_15; } @@ -4574,7 +4603,7 @@ lean_ctor_set(x_25, 4, x_24); lean_ctor_set_uint8(x_25, sizeof(void*)*5, x_20); x_26 = 0; x_27 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__1(x_26, x_25, x_2); -x_28 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_28 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_29 = l_Lean_Parser_ParserState_mkNode(x_27, x_28, x_4); return x_29; } @@ -4625,7 +4654,7 @@ lean_object* _init_l_Lean_Parser_Tactic_tacticSeq1Indented___closed__5() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_2 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__4; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; @@ -5600,6 +5629,256 @@ x_1 = l_Lean_Parser_Tactic_tacticSeq___closed__6; return x_1; } } +lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7; +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_6 = 0; +x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___spec__2(x_1, x_5, x_6, x_2, x_3); +return x_7; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("seq1"); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__3() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +x_2 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_2, 0, x_1); +return x_2; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__1; +x_2 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__3; +x_3 = 1; +x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3); +return x_4; +} +} +lean_object* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object* x_1, lean_object* x_2) { +_start: +{ +lean_object* x_3; lean_object* x_4; uint8_t x_5; +x_3 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__4; +x_4 = lean_ctor_get(x_3, 1); +lean_inc(x_4); +lean_inc(x_2); +lean_inc(x_1); +x_5 = l_Lean_Parser_tryAnti(x_1, x_2); +if (x_5 == 0) +{ +lean_object* x_6; lean_object* x_7; lean_object* x_8; +lean_dec(x_4); +x_6 = lean_unsigned_to_nat(1024u); +x_7 = l_Lean_Parser_checkPrecFn(x_6, x_1, x_2); +x_8 = lean_ctor_get(x_7, 3); +lean_inc(x_8); +if (lean_obj_tag(x_8) == 0) +{ +lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; +x_9 = lean_ctor_get(x_7, 0); +lean_inc(x_9); +x_10 = lean_array_get_size(x_9); +lean_dec(x_9); +x_11 = 1; +x_12 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_11, x_1, x_7); +x_13 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +x_14 = l_Lean_Parser_ParserState_mkNode(x_12, x_13, x_10); +return x_14; +} +else +{ +lean_dec(x_8); +lean_dec(x_1); +return x_7; +} +} +else +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; +x_15 = lean_ctor_get(x_2, 0); +lean_inc(x_15); +x_16 = lean_array_get_size(x_15); +lean_dec(x_15); +x_17 = lean_ctor_get(x_2, 1); +lean_inc(x_17); +lean_inc(x_1); +x_18 = lean_apply_2(x_4, x_1, x_2); +x_19 = lean_ctor_get(x_18, 3); +lean_inc(x_19); +if (lean_obj_tag(x_19) == 0) +{ +lean_dec(x_17); +lean_dec(x_16); +lean_dec(x_1); +return x_18; +} +else +{ +lean_object* x_20; lean_object* x_21; uint8_t x_22; +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +lean_dec(x_19); +x_21 = lean_ctor_get(x_18, 1); +lean_inc(x_21); +x_22 = lean_nat_dec_eq(x_21, x_17); +lean_dec(x_21); +if (x_22 == 0) +{ +lean_dec(x_20); +lean_dec(x_17); +lean_dec(x_16); +lean_dec(x_1); +return x_18; +} +else +{ +lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; +lean_inc(x_17); +x_23 = l_Lean_Parser_ParserState_restore(x_18, x_16, x_17); +lean_dec(x_16); +x_24 = lean_unsigned_to_nat(1024u); +x_25 = l_Lean_Parser_checkPrecFn(x_24, x_1, x_23); +x_26 = lean_ctor_get(x_25, 3); +lean_inc(x_26); +if (lean_obj_tag(x_26) == 0) +{ +lean_object* x_27; lean_object* x_28; uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; +x_27 = lean_ctor_get(x_25, 0); +lean_inc(x_27); +x_28 = lean_array_get_size(x_27); +lean_dec(x_27); +x_29 = 1; +x_30 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_29, x_1, x_25); +x_31 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_28); +x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_20, x_17, x_29); +lean_dec(x_17); +return x_33; +} +else +{ +uint8_t x_34; lean_object* x_35; +lean_dec(x_26); +lean_dec(x_1); +x_34 = 1; +x_35 = l_Lean_Parser_mergeOrElseErrors(x_25, x_20, x_17, x_34); +lean_dec(x_17); +return x_35; +} +} +} +} +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2; +x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_seq1___closed__1; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___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_Tactic_seq1___closed__2; +x_3 = l_Lean_Parser_andthenInfo(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; +x_1 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__4; +x_2 = lean_ctor_get(x_1, 0); +lean_inc(x_2); +x_3 = l_Lean_Parser_Tactic_seq1___closed__3; +x_4 = l_Lean_Parser_orelseInfo(x_2, x_3); +return x_4; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1___elambda__1), 2, 0); +return x_1; +} +} +lean_object* _init_l_Lean_Parser_Tactic_seq1___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_seq1___closed__4; +x_2 = l_Lean_Parser_Tactic_seq1___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_Tactic_seq1() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_Tactic_seq1___closed__6; +return x_1; +} +} +lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +_start: +{ +uint8_t x_4; lean_object* x_5; +x_4 = lean_unbox(x_1); +lean_dec(x_1); +x_5 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_4, x_2, x_3); +return x_5; +} +} lean_object* _init_l_Lean_Parser_darrow___elambda__1___closed__1() { _start: { @@ -6703,7 +6982,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_formatter(lean_object* x_1, _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_7 = l_Lean_Parser_Tactic_tacticSeq1Indented_formatter___closed__5; x_8 = l_Lean_PrettyPrinter_Formatter_node_formatter(x_6, x_7, x_1, x_2, x_3, x_4, x_5); return x_8; @@ -7020,7 +7299,7 @@ lean_object* l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer(lean_object* _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_7 = l_Lean_Parser_Tactic_tacticSeq1Indented_parenthesizer___closed__5; x_8 = l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4, x_5); return x_8; @@ -70968,7 +71247,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_mkAppStx___closed__6; -x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4; +x_2 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } @@ -75841,19 +76120,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3) { -_start: -{ -lean_object* x_4; lean_object* x_5; uint8_t x_6; lean_object* x_7; -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_6 = 0; -x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeqBracketed___elambda__1___spec__2(x_1, x_5, x_6, x_2, x_3); -return x_7; -} -} lean_object* l_Lean_Parser_Tactic_seq1Unbox___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -75863,8 +76129,8 @@ lean_inc(x_3); x_4 = lean_array_get_size(x_3); lean_dec(x_3); x_5 = 1; -x_6 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(x_5, x_1, x_2); -x_7 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_6 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1___elambda__1___spec__1(x_5, x_1, x_2); +x_7 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_8 = l_Lean_Parser_ParserState_mkNode(x_6, x_7, x_4); x_9 = lean_ctor_get(x_8, 3); lean_inc(x_9); @@ -75909,35 +76175,23 @@ return x_8; lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__1() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1; -x_2 = lean_ctor_get(x_1, 0); -lean_inc(x_2); -x_3 = l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2; -x_4 = l_Lean_Parser_sepBy1Info(x_2, x_3); -return x_4; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; +x_2 = l_Lean_Parser_Tactic_seq1___closed__1; +x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); +return x_3; } } lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__2() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; -x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__1; -x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); -return x_3; -} -} -lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() { -_start: -{ lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; +x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__1; x_2 = l_Lean_Parser_withResultOfInfo(x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__4() { +lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() { _start: { lean_object* x_1; @@ -75945,12 +76199,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Tactic_seq1Unbox___elambda__1), 2 return x_1; } } -lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__5() { +lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__4() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__3; -x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__4; +x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; +x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__3; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -75961,20 +76215,10 @@ lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__5; +x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__4; return x_1; } } -lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) { -_start: -{ -uint8_t x_4; lean_object* x_5; -x_4 = lean_unbox(x_1); -lean_dec(x_1); -x_5 = l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Tactic_seq1Unbox___elambda__1___spec__1(x_4, x_2, x_3); -return x_5; -} -} lean_object* _init_l_Lean_Parser_Tactic_quot___elambda__1___closed__1() { _start: { @@ -76144,7 +76388,7 @@ lean_inc(x_12); if (lean_obj_tag(x_12) == 0) { lean_object* x_13; lean_object* x_14; lean_object* x_15; -x_13 = l_Lean_Parser_Tactic_seq1Unbox___closed__4; +x_13 = l_Lean_Parser_Tactic_seq1Unbox___closed__3; lean_inc(x_1); x_14 = l_Lean_Parser_toggleInsideQuotFn(x_13, x_1, x_11); x_15 = lean_ctor_get(x_14, 3); @@ -76360,7 +76604,7 @@ lean_inc(x_72); if (lean_obj_tag(x_72) == 0) { lean_object* x_73; lean_object* x_74; lean_object* x_75; -x_73 = l_Lean_Parser_Tactic_seq1Unbox___closed__4; +x_73 = l_Lean_Parser_Tactic_seq1Unbox___closed__3; lean_inc(x_1); x_74 = l_Lean_Parser_toggleInsideQuotFn(x_73, x_1, x_71); x_75 = lean_ctor_get(x_74, 3); @@ -76579,7 +76823,7 @@ lean_object* l_Lean_Parser_Tactic_seq1Unbox_formatter(lean_object* x_1, lean_obj _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; -x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_7 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__4; x_8 = l_Lean_Parser_Tactic_tacticSeqBracketed_formatter___closed__3; x_9 = l_Lean_PrettyPrinter_Formatter_nodeSepBy1Unbox_formatter(x_6, x_7, x_8, x_1, x_2, x_3, x_4, x_5); @@ -76700,7 +76944,7 @@ lean_object* l_Lean_Parser_Tactic_seq1Unbox_parenthesizer(lean_object* x_1, lean _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; -x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; +x_6 = l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2; x_7 = l_Lean_Parser_Tactic_tacticSeqBracketed_parenthesizer___closed__2; x_8 = l_Lean_Parser_antiquotNestedExpr_parenthesizer___closed__3; x_9 = l_Lean_PrettyPrinter_Parenthesizer_nodeSepBy1Unbox_parenthesizer(x_6, x_7, x_8, x_1, x_2, x_3, x_4, x_5); @@ -77650,6 +77894,10 @@ l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacti lean_mark_persistent(l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__4); l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__5 = _init_l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__5(); lean_mark_persistent(l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___spec__2___closed__5); +l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__1); +l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq1Indented___elambda__1___closed__2); l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq1Indented___closed__1); l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2 = _init_l_Lean_Parser_Tactic_tacticSeq1Indented___closed__2(); @@ -77726,6 +77974,28 @@ l_Lean_Parser_Tactic_tacticSeq___closed__6 = _init_l_Lean_Parser_Tactic_tacticSe lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq___closed__6); l_Lean_Parser_Tactic_tacticSeq = _init_l_Lean_Parser_Tactic_tacticSeq(); lean_mark_persistent(l_Lean_Parser_Tactic_tacticSeq); +l_Lean_Parser_Tactic_seq1___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__1); +l_Lean_Parser_Tactic_seq1___elambda__1___closed__2 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__2); +l_Lean_Parser_Tactic_seq1___elambda__1___closed__3 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__3); +l_Lean_Parser_Tactic_seq1___elambda__1___closed__4 = _init_l_Lean_Parser_Tactic_seq1___elambda__1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___elambda__1___closed__4); +l_Lean_Parser_Tactic_seq1___closed__1 = _init_l_Lean_Parser_Tactic_seq1___closed__1(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__1); +l_Lean_Parser_Tactic_seq1___closed__2 = _init_l_Lean_Parser_Tactic_seq1___closed__2(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__2); +l_Lean_Parser_Tactic_seq1___closed__3 = _init_l_Lean_Parser_Tactic_seq1___closed__3(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__3); +l_Lean_Parser_Tactic_seq1___closed__4 = _init_l_Lean_Parser_Tactic_seq1___closed__4(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__4); +l_Lean_Parser_Tactic_seq1___closed__5 = _init_l_Lean_Parser_Tactic_seq1___closed__5(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__5); +l_Lean_Parser_Tactic_seq1___closed__6 = _init_l_Lean_Parser_Tactic_seq1___closed__6(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1___closed__6); +l_Lean_Parser_Tactic_seq1 = _init_l_Lean_Parser_Tactic_seq1(); +lean_mark_persistent(l_Lean_Parser_Tactic_seq1); l_Lean_Parser_darrow___elambda__1___closed__1 = _init_l_Lean_Parser_darrow___elambda__1___closed__1(); lean_mark_persistent(l_Lean_Parser_darrow___elambda__1___closed__1); l_Lean_Parser_darrow___elambda__1___closed__2 = _init_l_Lean_Parser_darrow___elambda__1___closed__2(); @@ -84320,8 +84590,6 @@ l_Lean_Parser_Tactic_seq1Unbox___closed__3 = _init_l_Lean_Parser_Tactic_seq1Unbo lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__3); l_Lean_Parser_Tactic_seq1Unbox___closed__4 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__4(); lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__4); -l_Lean_Parser_Tactic_seq1Unbox___closed__5 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__5(); -lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__5); l_Lean_Parser_Tactic_seq1Unbox = _init_l_Lean_Parser_Tactic_seq1Unbox(); lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox); l_Lean_Parser_Tactic_quot___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_quot___elambda__1___closed__1(); diff --git a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c index 86a1253885..c2c2064267 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c @@ -213,7 +213,6 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_sepBy1_parenthesizer(lean_object extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__34; lean_object* l_Lean_PrettyPrinter_Parenthesizer_node_parenthesizer___lambda__1___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_categoryParserOfStack_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_getConstInfo___rarg___lambda__1___closed__5; extern lean_object* l_Lean_Unhygienic_MonadQuotation___closed__4; @@ -438,7 +437,6 @@ extern lean_object* l_Lean_mkAppStx___closed__2; lean_object* l___private_Lean_PrettyPrinter_Parenthesizer_1__regTraceClasses(lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1; lean_object* l_ReaderT_bind___at_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___spec__1(lean_object*, lean_object*); -lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4; lean_object* l_Lean_Syntax_Traverser_left(lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_quotedSymbol_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbolNoWs_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*); @@ -6890,51 +6888,22 @@ x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4() { -_start: -{ -lean_object* x_1; -x_1 = lean_mk_string("seq"); -return x_1; -} -} -lean_object* _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2; -x_2 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1(lean_object* 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; 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_5 = l_Array_empty___closed__1; +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_5 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__22; x_6 = lean_array_push(x_5, x_1); -x_7 = l_Lean_nullKind___closed__2; -x_8 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_8, 0, x_7); -lean_ctor_set(x_8, 1, x_6); -x_9 = lean_array_push(x_5, x_8); -x_10 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; -x_11 = lean_alloc_ctor(1, 2, 0); +x_7 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__34; +x_8 = lean_array_push(x_6, x_7); +x_9 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3; +x_10 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_10, 0, x_9); +lean_ctor_set(x_10, 1, x_8); +x_11 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_11, 0, x_10); -lean_ctor_set(x_11, 1, x_9); -x_12 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__22; -x_13 = lean_array_push(x_12, x_11); -x_14 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__34; -x_15 = lean_array_push(x_13, x_14); -x_16 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3; -x_17 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_17, 0, x_16); -lean_ctor_set(x_17, 1, x_15); -x_18 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_18, 0, x_17); -lean_ctor_set(x_18, 1, x_4); -return x_18; +lean_ctor_set(x_11, 1, x_4); +return x_11; } } lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__2(lean_object* x_1) { @@ -9678,10 +9647,6 @@ l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2 lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2); l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3(); lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__3); -l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4(); -lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__4); -l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5(); -lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5); l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1(); lean_mark_persistent(l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__1); l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2 = _init_l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___closed__2();