From c7b54229299f7ba3a1abf382fac9102334d5944d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Sep 2020 15:47:58 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Elab/Tactic/Basic.lean | 8 +- stage0/src/Lean/Parser/Term.lean | 2 +- stage0/stdlib/Lean/Elab/Tactic/Basic.c | 145 ++++++++++++------ stage0/stdlib/Lean/Parser/Syntax.c | 4 +- stage0/stdlib/Lean/Parser/Tactic.c | 6 +- stage0/stdlib/Lean/Parser/Term.c | 77 ++-------- .../stdlib/Lean/PrettyPrinter/Parenthesizer.c | 57 +++++-- 7 files changed, 165 insertions(+), 134 deletions(-) diff --git a/stage0/src/Lean/Elab/Tactic/Basic.lean b/stage0/src/Lean/Elab/Tactic/Basic.lean index 6bad41ac85..9157c8fcab 100644 --- a/stage0/src/Lean/Elab/Tactic/Basic.lean +++ b/stage0/src/Lean/Elab/Tactic/Basic.lean @@ -243,17 +243,19 @@ modifyMCtx fun mctx => (mctx, 1); mctx -@[builtinTactic seq] def evalSeq : Tactic := +def evalSeq : Tactic := fun stx => (stx.getArg 0).forSepArgsM evalTactic @[builtinTactic seq1] def evalSeq1 : Tactic := evalSeq -@[builtinTactic paren] def evalParen : Tactic := -fun stx => evalSeq1 (stx.getArg 1) +@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := evalSeq @[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => withRef (stx.getArg 2) $ focus $ (stx.getArg 1).forSepArgsM evalTactic +@[builtinTactic paren] def evalParen : Tactic := +fun stx => evalSeq1 (stx.getArg 1) + @[builtinTactic tacticSeq] def evalTacticSeq : Tactic := fun stx => evalTactic (stx.getArg 0) diff --git a/stage0/src/Lean/Parser/Term.lean b/stage0/src/Lean/Parser/Term.lean index f693c408ec..87897608f0 100644 --- a/stage0/src/Lean/Parser/Term.lean +++ b/stage0/src/Lean/Parser/Term.lean @@ -256,7 +256,7 @@ stx.isAntiquot || stx.isIdent end Term -def Tactic.seq1Unbox := nodeSepBy1Unbox `Lean.Parser.Tactic.seq tacticParser "; " true +def Tactic.seq1Unbox := nodeSepBy1Unbox `Lean.Parser.Tactic.seq1 tacticParser "; " true @[builtinTermParser] def Tactic.quot : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.seq1Unbox >> ")" @[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")" diff --git a/stage0/stdlib/Lean/Elab/Tactic/Basic.c b/stage0/stdlib/Lean/Elab/Tactic/Basic.c index 2a2a76c33b..e4eeb50cb2 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Basic.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Basic.c @@ -38,6 +38,7 @@ lean_object* l_Lean_Elab_Tactic_withMainMVarContext___rarg(lean_object*, lean_ob lean_object* l_Lean_Elab_Tactic_mkTacticAttribute___closed__3; lean_object* lean_nat_div(lean_object*, lean_object*); extern lean_object* l_Lean_KeyedDeclsAttribute_KeyedDeclsAttribute_inhabited___closed__1; +lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_withIncRecDepth___rarg___lambda__2___closed__2; lean_object* l_Lean_Elab_Tactic_evalIntros___closed__1; @@ -92,6 +93,7 @@ lean_object* l_Lean_Elab_Tactic_liftMetaM___rarg(lean_object*, lean_object*, lea lean_object* l_Lean_Elab_Tactic_evalCase___closed__1; lean_object* l_Lean_Elab_Tactic_done(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_mkMVar(lean_object*); +lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Array_empty___closed__1; extern lean_object* l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1; uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*); @@ -122,6 +124,7 @@ lean_object* l_ReaderT_bind___at_Lean_Meta_Lean_MonadLCtx___spec__2___rarg(lean_ lean_object* l_Lean_Elab_Tactic_ensureHasType___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalIntro(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalCase___closed__5; +lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3; lean_object* l_Lean_Elab_Tactic_evalCase___closed__3; lean_object* l___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___closed__1; lean_object* l_Lean_Meta_getMVars___at_Lean_Elab_Tactic_ensureHasNoMVars___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -139,6 +142,7 @@ lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Elab_Tactic_evalTactic__ extern lean_object* l_String_splitAux___main___closed__1; lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__12___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_evalDone___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_object*); lean_object* l_Lean_MetavarContext_renameMVar(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_reportUnsolvedGoals___closed__3; lean_object* l_Lean_Elab_Tactic_mkTacticAttribute___closed__4; @@ -194,7 +198,6 @@ lean_object* l_Lean_Elab_Tactic_try_x3f___rarg(lean_object*, lean_object*, lean_ lean_object* l_Lean_Elab_Tactic_evalTacticSeqBracketed___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_ensureHasNoMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq(lean_object*); lean_object* l_Lean_Elab_Tactic_TacticM_run_x27(lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__1; lean_object* l_Lean_Meta_intro1Core(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -235,13 +238,13 @@ extern lean_object* l___private_Lean_Elab_Term_11__elabUsingElabFns___closed__6; lean_object* l_Lean_Name_append___main(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq(lean_object*); lean_object* l_Lean_Elab_Tactic_TacticM_run(lean_object*); -lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1; lean_object* l___regBuiltin_Lean_Elab_Tactic_evalFailIfSuccess(lean_object*); lean_object* l_Std_AssocList_find_x3f___main___at_Lean_Elab_Tactic_evalTactic___main___spec__6(lean_object*, lean_object*); lean_object* l_Lean_Elab_Tactic_SavedState_inhabited; lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Tactic_evalTactic___main___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__3; lean_object* l_Lean_Elab_Tactic_evalSeq___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2; lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSkip(lean_object*); lean_object* l___private_Init_Data_Array_QSort_1__qpartitionAux___main___at___private_Lean_Elab_Tactic_Basic_5__sortFVarIds___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_Expr_hasExprMVar(lean_object*); @@ -271,6 +274,7 @@ size_t l_Lean_Name_hash(lean_object*); lean_object* l_Lean_Elab_Tactic_getMainGoal___closed__1; lean_object* l_List_erase___main___at_Lean_Elab_Tactic_evalCase___spec__1___boxed(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalChoice___closed__1; +lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1; lean_object* l___regBuiltin_Lean_Elab_Tactic_evalAssumption___closed__1; lean_object* lean_st_mk_ref(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDone___closed__2; @@ -7732,25 +7736,6 @@ lean_dec(x_1); return x_11; } } -lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1() { -_start: -{ -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalSeq___boxed), 10, 0); -return x_1; -} -} -lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSeq(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_Elab_Tactic_tacticElabAttribute; -x_3 = l___private_Lean_Elab_Binders_16__expandMatchAltsIntoMatchAux___main___closed__7; -x_4 = l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1; -x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); -return x_5; -} -} lean_object* l_Lean_Elab_Tactic_evalSeq1(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* x_8, lean_object* x_9, lean_object* x_10) { _start: { @@ -7805,51 +7790,56 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* l_Lean_Elab_Tactic_evalParen(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* x_8, lean_object* x_9, lean_object* x_10) { -_start: -{ -lean_object* x_11; lean_object* x_12; lean_object* x_13; -x_11 = lean_unsigned_to_nat(1u); -x_12 = l_Lean_Syntax_getArg(x_1, x_11); -x_13 = l_Lean_Elab_Tactic_evalSeq(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); -lean_dec(x_12); -return x_13; -} -} -lean_object* l_Lean_Elab_Tactic_evalParen___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* x_8, lean_object* x_9, lean_object* x_10) { +lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented(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* x_8, lean_object* x_9, lean_object* x_10) { _start: { lean_object* x_11; -x_11 = l_Lean_Elab_Tactic_evalParen(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); +x_11 = l_Lean_Elab_Tactic_evalSeq(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); +return x_11; +} +} +lean_object* l_Lean_Elab_Tactic_evalTacticSeq1Indented___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* x_8, lean_object* x_9, lean_object* x_10) { +_start: +{ +lean_object* x_11; +x_11 = l_Lean_Elab_Tactic_evalTacticSeq1Indented(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); lean_dec(x_1); return x_11; } } -lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1() { +lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("tacticSeq1Indented"); +return x_1; +} +} +lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1; -x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__19; +x_2 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2() { +lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalParen___boxed), 10, 0); +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTacticSeq1Indented___boxed), 10, 0); return x_1; } } -lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_object* x_1) { +lean_object* l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented(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_Elab_Tactic_tacticElabAttribute; -x_3 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1; -x_4 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2; +x_3 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2; +x_4 = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -7962,6 +7952,55 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* l_Lean_Elab_Tactic_evalParen(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* x_8, lean_object* x_9, lean_object* x_10) { +_start: +{ +lean_object* x_11; lean_object* x_12; lean_object* x_13; +x_11 = lean_unsigned_to_nat(1u); +x_12 = l_Lean_Syntax_getArg(x_1, x_11); +x_13 = l_Lean_Elab_Tactic_evalSeq(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); +lean_dec(x_12); +return x_13; +} +} +lean_object* l_Lean_Elab_Tactic_evalParen___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* x_8, lean_object* x_9, lean_object* x_10) { +_start: +{ +lean_object* x_11; +x_11 = l_Lean_Elab_Tactic_evalParen(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10); +lean_dec(x_1); +return x_11; +} +} +lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_Elab_Term_Quotation_elabTacticQuot___closed__1; +x_2 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__19; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalParen___boxed), 10, 0); +return x_1; +} +} +lean_object* l___regBuiltin_Lean_Elab_Tactic_evalParen(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_Elab_Tactic_tacticElabAttribute; +x_3 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1; +x_4 = l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2; +x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); +return x_5; +} +} lean_object* l_Lean_Elab_Tactic_evalTacticSeq(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* x_8, lean_object* x_9, lean_object* x_10) { _start: { @@ -15115,11 +15154,6 @@ if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l_Lean_Elab_Tactic_focus___rarg___closed__1 = _init_l_Lean_Elab_Tactic_focus___rarg___closed__1(); lean_mark_persistent(l_Lean_Elab_Tactic_focus___rarg___closed__1); -l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1(); -lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq___closed__1); -res = l___regBuiltin_Lean_Elab_Tactic_evalSeq(lean_io_mk_world()); -if (lean_io_result_is_error(res)) return res; -lean_dec_ref(res); l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__1); l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__2(); @@ -15129,11 +15163,13 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalSeq1___closed__3); res = l___regBuiltin_Lean_Elab_Tactic_evalSeq1(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1(); -lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1); -l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2(); -lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2); -res = l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_io_mk_world()); +l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__1); +l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__2); +l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented___closed__3); +res = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq1Indented(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___closed__1(); @@ -15145,6 +15181,13 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed___cl res = l___regBuiltin_Lean_Elab_Tactic_evalTacticSeqBracketed(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__1); +l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalParen___closed__2); +res = l___regBuiltin_Lean_Elab_Tactic_evalParen(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__1); l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2 = _init_l___regBuiltin_Lean_Elab_Tactic_evalTacticSeq___closed__2(); diff --git a/stage0/stdlib/Lean/Parser/Syntax.c b/stage0/stdlib/Lean/Parser/Syntax.c index e4500063f5..b8509b9209 100644 --- a/stage0/stdlib/Lean/Parser/Syntax.c +++ b/stage0/stdlib/Lean/Parser/Syntax.c @@ -151,6 +151,7 @@ lean_object* l___regBuiltin_Lean_Parser_Syntax_num_formatter(lean_object*); lean_object* l_Lean_Parser_Syntax_try_formatter___closed__4; lean_object* l_Lean_Parser_Command_macroHead; lean_object* l_Lean_Parser_Command_mixfix_parenthesizer___closed__10; +extern lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__2; lean_object* l_Lean_Parser_Syntax_paren___closed__4; lean_object* l_Lean_Parser_Command_elab_parenthesizer___closed__10; lean_object* l_Lean_Parser_Syntax_many1___elambda__1___closed__2; @@ -430,7 +431,6 @@ 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; @@ -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__3; +x_24 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; 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 e089a4c7c0..c236546f23 100644 --- a/stage0/stdlib/Lean/Parser/Tactic.c +++ b/stage0/stdlib/Lean/Parser/Tactic.c @@ -733,6 +733,7 @@ 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*); @@ -1696,7 +1697,6 @@ 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_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*); @@ -26568,7 +26568,7 @@ lean_object* l_Lean_Parser_Tactic_seq1_formatter(lean_object* x_1, lean_object* _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_6 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +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); return x_8; @@ -26680,7 +26680,7 @@ lean_object* l_Lean_Parser_Tactic_seq1_parenthesizer(lean_object* x_1, lean_obje _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; -x_6 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__2; +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); return x_8; diff --git a/stage0/stdlib/Lean/Parser/Term.c b/stage0/stdlib/Lean/Parser/Term.c index 000cf22810..14e6cc81c7 100644 --- a/stage0/stdlib/Lean/Parser/Term.c +++ b/stage0/stdlib/Lean/Parser/Term.c @@ -624,7 +624,6 @@ lean_object* l_Lean_Parser_Term_bracketedBinder_formatter___boxed(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; @@ -1755,6 +1754,7 @@ 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; @@ -2612,7 +2612,6 @@ lean_object* l_Lean_Parser_Term_byTactic___closed__5; lean_object* l_Lean_Parser_Term_proj___closed__7; lean_object* l_Lean_Parser_Term_app_formatter___closed__1; lean_object* l_Lean_Parser_Term_if___elambda__1___closed__4; -lean_object* l_Lean_Parser_Tactic_seq1Unbox___closed__4; lean_object* l_Lean_Parser_Term_structInst_parenthesizer___closed__12; lean_object* l_Lean_Parser_Term_decide___elambda__1(lean_object*, lean_object*); lean_object* l_Lean_Parser_Term_str_parenthesizer___closed__1; @@ -3286,7 +3285,6 @@ lean_object* l_Lean_Parser_Term_app___closed__1; lean_object* l_Lean_Parser_Term_emptyC___closed__5; lean_object* l___regBuiltin_Lean_Parser_Term_have_formatter(lean_object*); lean_object* l_Lean_Parser_Term_unreachable_parenthesizer___closed__1; -lean_object* l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1; lean_object* l_Lean_Parser_Term_panic_formatter___closed__1; lean_object* l_Lean_Parser_Term_mod_formatter___closed__1; lean_object* l_Lean_Parser_Term_attrInstance_formatter___closed__1; @@ -4111,7 +4109,6 @@ 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*); @@ -5945,24 +5942,6 @@ x_7 = l___private_Lean_Parser_Basic_2__sepByFnAux___main___at_Lean_Parser_Tactic 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* l_Lean_Parser_Tactic_seq1___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -5973,7 +5952,7 @@ 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_seq1___elambda__1___spec__1(x_5, x_1, x_2); -x_7 = l_Lean_Parser_Tactic_seq1___elambda__1___closed__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; } @@ -5994,7 +5973,7 @@ 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_1 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; x_2 = l_Lean_Parser_Tactic_seq1___closed__1; x_3 = l_Lean_Parser_nodeInfo(x_1, x_2); return x_3; @@ -76343,16 +76322,6 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } } -lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1() { -_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_Term_seq___elambda__1___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} lean_object* l_Lean_Parser_Tactic_seq1Unbox___elambda__1(lean_object* x_1, lean_object* x_2) { _start: { @@ -76363,7 +76332,7 @@ 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_seq1___elambda__1___spec__1(x_5, x_1, x_2); -x_7 = l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1; +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); x_9 = lean_ctor_get(x_8, 3); lean_inc(x_9); @@ -76408,23 +76377,13 @@ 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; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1; -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; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__1; +x_1 = l_Lean_Parser_Tactic_seq1___closed__2; x_2 = l_Lean_Parser_withResultOfInfo(x_1); return x_2; } } -lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() { +lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__2() { _start: { lean_object* x_1; @@ -76432,12 +76391,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__4() { +lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3() { _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_seq1Unbox___closed__3; +x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__1; +x_2 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; x_3 = lean_alloc_ctor(0, 2, 0); lean_ctor_set(x_3, 0, x_1); lean_ctor_set(x_3, 1, x_2); @@ -76448,7 +76407,7 @@ lean_object* _init_l_Lean_Parser_Tactic_seq1Unbox() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__4; +x_1 = l_Lean_Parser_Tactic_seq1Unbox___closed__3; return x_1; } } @@ -76621,7 +76580,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__3; +x_13 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; lean_inc(x_1); x_14 = l_Lean_Parser_toggleInsideQuotFn(x_13, x_1, x_11); x_15 = lean_ctor_get(x_14, 3); @@ -76837,7 +76796,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__3; +x_73 = l_Lean_Parser_Tactic_seq1Unbox___closed__2; lean_inc(x_1); x_74 = l_Lean_Parser_toggleInsideQuotFn(x_73, x_1, x_71); x_75 = lean_ctor_get(x_74, 3); @@ -77056,7 +77015,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_Parser_Tactic_seq1Unbox___elambda__1___closed__1; +x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; 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); @@ -77177,7 +77136,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_Parser_Tactic_seq1Unbox___elambda__1___closed__1; +x_6 = l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__5; 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); @@ -78215,10 +78174,6 @@ 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___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(); @@ -84825,16 +84780,12 @@ lean_mark_persistent(l___regBuiltin_Lean_Parser_Term_return_parenthesizer___clos res = l___regBuiltin_Lean_Parser_Term_return_parenthesizer(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1 = _init_l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1(); -lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___elambda__1___closed__1); l_Lean_Parser_Tactic_seq1Unbox___closed__1 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__1(); lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__1); l_Lean_Parser_Tactic_seq1Unbox___closed__2 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__2(); lean_mark_persistent(l_Lean_Parser_Tactic_seq1Unbox___closed__2); l_Lean_Parser_Tactic_seq1Unbox___closed__3 = _init_l_Lean_Parser_Tactic_seq1Unbox___closed__3(); 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 = _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 c2c2064267..c4733445dc 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c @@ -213,6 +213,7 @@ 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; @@ -437,6 +438,7 @@ 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*); @@ -6888,22 +6890,51 @@ 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("seq1"); +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; -x_5 = l_Lean_myMacro____x40_Lean_Util_Trace___hyg_45____closed__22; +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; x_6 = lean_array_push(x_5, x_1); -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); +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); lean_ctor_set(x_11, 0, x_10); -lean_ctor_set(x_11, 1, x_4); -return x_11; +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_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__2(lean_object* x_1) { @@ -9647,6 +9678,10 @@ 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();