From 0df74178d8fab31f2f240b5bc4ce57a559283b29 Mon Sep 17 00:00:00 2001 From: Lean stage0 autoupdater <> Date: Mon, 22 Dec 2025 20:55:00 +0000 Subject: [PATCH] chore: update stage0 --- stage0/src/stdlib_flags.h | 3 +- stage0/stdlib/Lean/Elab/Tactic/Grind/Main.c | 1910 ++++++++++------- stage0/stdlib/Lean/Meta/Tactic/Grind/Parser.c | 405 +++- 3 files changed, 1475 insertions(+), 843 deletions(-) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 59d89f839c..79a0e58edd 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,4 +1,3 @@ -// update me! #include "util/options.h" namespace lean { @@ -12,7 +11,7 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, true); + opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/stage0/stdlib/Lean/Elab/Tactic/Grind/Main.c b/stage0/stdlib/Lean/Elab/Tactic/Grind/Main.c index 143fb87360..abf3094e71 100644 --- a/stage0/stdlib/Lean/Elab/Tactic/Grind/Main.c +++ b/stage0/stdlib/Lean/Elab/Tactic/Grind/Main.c @@ -46,6 +46,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalGrindTraceCore___lam__3(uint8_t, LEAN_EXPORT lean_object* l___private_Lean_Data_PersistentHashMap_0__Lean_PersistentHashMap_insertAux_traverse___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4_spec__5_spec__6_spec__8(lean_object*, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_MVarId_withContext___at___00Lean_Elab_Tactic_grind_spec__2___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_elabResetGrindAttrs___regBuiltin_Lean_Elab_Tactic_elabResetGrindAttrs__1___closed__2; +lean_object* l_Lean_TSyntax_getId(lean_object*); LEAN_EXPORT lean_object* l_Lean_withExporting___at___00Lean_Elab_Tactic_elabInitGrindNorm_spec__2(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_setGrindParams___closed__0; static lean_object* l_Lean_Elab_Tactic_elabGrindPattern___closed__7; @@ -63,7 +64,7 @@ static lean_object* l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore_ static lean_object* l_Lean_Elab_Tactic_elabGrindConfig___redArg___closed__1; static lean_object* l_Lean_addTrace___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__3___redArg___closed__2; static lean_object* l_Lean_Elab_Tactic_evalGrindTrace___closed__1; -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_contains___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__1___boxed(lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0___closed__2; LEAN_EXPORT lean_object* l_Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1___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*, lean_object*); @@ -80,7 +81,7 @@ static lean_object* l_Lean_Elab_Tactic_evalGrindTraceCore___lam__1___closed__0; uint8_t lean_usize_dec_le(size_t, size_t); LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindConfig_x27(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_instantiateMVars___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrRHS_spec__0___redArg(lean_object*, lean_object*); -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___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*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___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*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT uint8_t l_Lean_PersistentHashMap_containsAtAux___at___00Lean_PersistentHashMap_containsAux___at___00Lean_PersistentHashMap_contains___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__1_spec__4_spec__10___redArg(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_indentD(lean_object*); LEAN_EXPORT lean_object* l_Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -191,7 +192,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___00__private_Lean_Ela extern lean_object* l_Lean_Meta_Grind_grindExt; LEAN_EXPORT lean_object* l_Lean_addTrace___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__3___redArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Elab_Tactic_elabGrindPattern___closed__12; -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_MessageData_hasSyntheticSorry(lean_object*); LEAN_EXPORT lean_object* l_Lean_throwError___at___00Lean_Elab_Tactic_elabGrindSuggestions_spec__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_array_fget_borrowed(lean_object*, lean_object*); @@ -427,6 +428,7 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNodeAux___at_ static lean_object* l_Lean_Elab_Tactic_elabGrindPattern___closed__1; static lean_object* l_Lean_Elab_Tactic_elabGrindConfig___redArg___closed__6; static lean_object* l_Lean_Elab_Tactic_mkGrindParams___closed__4; +static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__1; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabGrindConfigInteractive(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0(lean_object*, lean_object*, lean_object*); @@ -445,7 +447,9 @@ static lean_object* l_Lean_Elab_Tactic_evalGrind___closed__3; static lean_object* l_Lean_Elab_Tactic_elabGrindPattern___regBuiltin_Lean_Elab_Tactic_elabGrindPattern__1___closed__2; uint8_t l_Lean_Meta_Grind_Result_hasFailed(lean_object*); lean_object* l_Lean_PersistentArray_push___redArg(lean_object*, lean_object*); +static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__0; static lean_object* l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__15; +static lean_object* l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0; LEAN_EXPORT lean_object* l_Lean_addTrace___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUse___at___00Lean_Elab_Tactic_evalGrind_spec__0_spec__0_spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_LibrarySuggestions_select(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_getSepArgs(lean_object*); @@ -525,6 +529,7 @@ lean_object* l_Lean_SimplePersistentEnvExtension_getState___redArg(lean_object*, LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabGrindConfig(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_MessageData_ofConstName(lean_object*, uint8_t); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalGrindTraceCore___lam__2(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; uint8_t l_Lean_Environment_contains(lean_object*, lean_object*, uint8_t); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalGrindTrace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_withDeclNameForAuxNaming___at___00Lean_Elab_Tactic_elabInitGrindNorm_spec__1___redArg___lam__0(lean_object*, lean_object*, lean_object*); @@ -558,7 +563,7 @@ LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Gr LEAN_EXPORT lean_object* l_Lean_withExporting___at___00Lean_Elab_Tactic_elabInitGrindNorm_spec__2___redArg___lam__0___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4_spec__5_spec__6___redArg___closed__0; lean_object* l_Lean_Meta_Grind_main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -662,6 +667,7 @@ lean_object* l_List_reverse___redArg(lean_object*); lean_object* l_Lean_Elab_Tactic_addEMatchTheorem(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1___redArg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_nat_sub(lean_object*, lean_object*); +lean_object* l_Lean_Meta_Grind_getExtension_x3f(lean_object*); LEAN_EXPORT lean_object* l_Lean_withExporting___at___00Lean_Elab_Tactic_elabInitGrindNorm_spec__2___redArg(lean_object*, uint8_t, lean_object*, lean_object*); static lean_object* l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__9; lean_object* l_Lean_Elab_Term_elabTermAndSynthesize(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -670,7 +676,6 @@ lean_object* l_Lean_Meta_Grind_mkResult(lean_object*, lean_object*, lean_object* LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalGrobner___regBuiltin_Lean_Elab_Tactic_evalGrobner__1___boxed(lean_object*); static lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg___closed__1; static lean_object* l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__0; -static lean_object* l_Lean_Elab_Tactic_mkGrindParams___closed__6; static lean_object* l_Lean_Elab_Tactic_setGrindParams___closed__4; static lean_object* l_Lean_Elab_Tactic_evalGrind___closed__5; uint8_t l_Lean_isPrivateName(lean_object*); @@ -706,6 +711,7 @@ lean_object* l_Lean_Elab_Command_liftTermElabM___redArg(lean_object*, lean_objec LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_getGrindParams(lean_object*); static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_parseModifier___closed__1; LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_insertAtCollisionNode___at___00Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4_spec__5_spec__6_spec__7___redArg(lean_object*, lean_object*, lean_object*); +static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__1; lean_object* l_Lean_Meta_Grind_Theorems_mkEmpty(lean_object*); static lean_object* l_Lean_Elab_Tactic_elabGrobnerConfig___redArg___closed__2; static lean_object* l_Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3___redArg___closed__2; @@ -747,7 +753,6 @@ LEAN_EXPORT lean_object* l_Lean_PersistentHashMap_containsAux___at___00Lean_Pers LEAN_EXPORT uint8_t l_Lean_Elab_Tactic_isGrindOnly(lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalUnsafe___redArg_00___x40_Lean_Elab_Tactic_Grind_Main_84924930____hygCtx___hyg_3_(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_parseModifier___closed__2; -static lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0; LEAN_EXPORT lean_object* l_Lean_Meta_withNewMCtxDepth___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__3___redArg___lam__0(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_evalCutsat(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___00Lean_Elab_Tactic_filterSuggestionsFromGrindConfig_spec__0(uint8_t, lean_object*, size_t, size_t, lean_object*); @@ -9249,6 +9254,23 @@ x_12 = l_Lean_throwUnknownIdentifierAt___at___00Lean_throwUnknownConstantAt___at return x_12; } } +static lean_object* _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("grind", 5, 5); +return x_1; +} +} +static lean_object* _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; +x_2 = l_Lean_Name_mkStr1(x_1); +return x_2; +} +} LEAN_EXPORT lean_object* l_Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { @@ -9464,73 +9486,65 @@ return x_29; } } } -static lean_object* _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0() { +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, uint8_t 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) { _start: { -lean_object* x_1; -x_1 = l_Lean_Meta_Grind_grindExt; -return x_1; -} -} -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t 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) { -_start: +lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19; +x_16 = l_Lean_Syntax_TSepArray_getElems___redArg(x_1); +x_17 = lean_array_size(x_16); +x_18 = 0; +lean_inc(x_14); +lean_inc_ref(x_13); +lean_inc(x_12); +lean_inc_ref(x_11); +lean_inc(x_10); +lean_inc_ref(x_9); +x_19 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__0(x_2, x_7, x_17, x_18, x_16, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_19) == 0) { -lean_object* x_15; size_t x_16; size_t x_17; lean_object* x_18; -x_15 = l_Lean_Syntax_TSepArray_getElems___redArg(x_1); -x_16 = lean_array_size(x_15); -x_17 = 0; -lean_inc(x_13); -lean_inc_ref(x_12); -lean_inc(x_11); -lean_inc_ref(x_10); -lean_inc(x_9); -lean_inc_ref(x_8); -x_18 = l___private_Init_Data_Array_Basic_0__Array_mapMUnsafe_map___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__0(x_2, x_6, x_16, x_17, x_15, x_8, x_9, x_10, x_11, x_12, x_13); -if (lean_obj_tag(x_18) == 0) +lean_object* x_20; lean_object* x_21; +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +lean_dec_ref(x_19); +lean_inc(x_14); +lean_inc_ref(x_13); +lean_inc(x_12); +lean_inc_ref(x_11); +x_21 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs(x_7, x_3, x_9, x_10, x_11, x_12, x_13, x_14); +if (lean_obj_tag(x_21) == 0) { -lean_object* x_19; lean_object* x_20; -x_19 = lean_ctor_get(x_18, 0); -lean_inc(x_19); -lean_dec_ref(x_18); -lean_inc(x_13); -lean_inc_ref(x_12); -lean_inc(x_11); -lean_inc_ref(x_10); -x_20 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs(x_6, x_3, x_8, x_9, x_10, x_11, x_12, x_13); -if (lean_obj_tag(x_20) == 0) -{ -lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27; -x_21 = lean_ctor_get(x_20, 0); -lean_inc(x_21); -lean_dec_ref(x_20); -x_22 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0; -x_23 = lean_array_get_size(x_6); -x_24 = lean_array_to_list(x_19); +lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27; +x_22 = lean_ctor_get(x_21, 0); +lean_inc(x_22); +lean_dec_ref(x_21); +x_23 = lean_array_get_size(x_7); +x_24 = lean_array_to_list(x_20); x_25 = lean_box(9); x_26 = 0; -x_27 = l_Lean_Meta_Grind_Extension_addEMatchTheorem(x_22, x_4, x_23, x_24, x_25, x_26, x_5, x_21, x_10, x_11, x_12, x_13); +x_27 = l_Lean_Meta_Grind_Extension_addEMatchTheorem(x_4, x_5, x_23, x_24, x_25, x_26, x_6, x_22, x_11, x_12, x_13, x_14); return x_27; } else { uint8_t x_28; -lean_dec(x_19); -lean_dec(x_13); -lean_dec_ref(x_12); -lean_dec(x_11); -lean_dec_ref(x_10); -lean_dec(x_4); -x_28 = !lean_is_exclusive(x_20); +lean_dec(x_20); +lean_dec(x_14); +lean_dec_ref(x_13); +lean_dec(x_12); +lean_dec_ref(x_11); +lean_dec(x_5); +lean_dec_ref(x_4); +x_28 = !lean_is_exclusive(x_21); if (x_28 == 0) { -return x_20; +return x_21; } else { lean_object* x_29; lean_object* x_30; -x_29 = lean_ctor_get(x_20, 0); +x_29 = lean_ctor_get(x_21, 0); lean_inc(x_29); -lean_dec(x_20); +lean_dec(x_21); x_30 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_30, 0, x_29); return x_30; @@ -9540,24 +9554,25 @@ return x_30; else { uint8_t x_31; -lean_dec(x_13); -lean_dec_ref(x_12); -lean_dec(x_11); -lean_dec_ref(x_10); -lean_dec(x_9); -lean_dec_ref(x_8); -lean_dec(x_4); -x_31 = !lean_is_exclusive(x_18); +lean_dec(x_14); +lean_dec_ref(x_13); +lean_dec(x_12); +lean_dec_ref(x_11); +lean_dec(x_10); +lean_dec_ref(x_9); +lean_dec(x_5); +lean_dec_ref(x_4); +x_31 = !lean_is_exclusive(x_19); if (x_31 == 0) { -return x_18; +return x_19; } else { lean_object* x_32; lean_object* x_33; -x_32 = lean_ctor_get(x_18, 0); +x_32 = lean_ctor_get(x_19, 0); lean_inc(x_32); -lean_dec(x_18); +lean_dec(x_19); x_33 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_33, 0, x_32); return x_33; @@ -9565,90 +9580,94 @@ return x_33; } } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___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* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) { +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___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* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14, lean_object* x_15) { _start: { -uint8_t x_15; lean_object* x_16; -x_15 = lean_unbox(x_5); -x_16 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0(x_1, x_2, x_3, x_4, x_15, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13); +uint8_t x_16; lean_object* x_17; +x_16 = lean_unbox(x_6); +x_17 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0(x_1, x_2, x_3, x_4, x_5, x_16, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14); +lean_dec_ref(x_8); lean_dec_ref(x_7); -lean_dec_ref(x_6); lean_dec(x_3); lean_dec_ref(x_1); -return x_16; +return x_17; +} +} +static lean_object* _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__0() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("unknown `grind` attribute `", 27, 27); +return x_1; +} +} +static lean_object* _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__1() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__0; +x_2 = l_Lean_stringToMessageData(x_1); +return x_2; } } LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t 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) { _start: { lean_object* x_13; -lean_inc(x_11); -lean_inc_ref(x_10); -lean_inc(x_2); -x_13 = l_Lean_Elab_realizeGlobalConstNoOverloadWithInfo(x_1, x_2, x_10, x_11); +x_13 = l_Lean_Meta_Grind_getExtension_x3f(x_1); if (lean_obj_tag(x_13) == 0) { -lean_object* x_14; lean_object* x_15; +lean_object* x_14; x_14 = lean_ctor_get(x_13, 0); lean_inc(x_14); lean_dec_ref(x_13); +if (lean_obj_tag(x_14) == 1) +{ +lean_object* x_15; lean_object* x_16; lean_object* x_17; +lean_dec(x_1); +x_15 = lean_ctor_get(x_14, 0); +lean_inc(x_15); +lean_dec_ref(x_14); +x_16 = lean_box(0); +lean_inc(x_11); +lean_inc_ref(x_10); +x_17 = l_Lean_Elab_realizeGlobalConstNoOverloadWithInfo(x_2, x_16, x_10, x_11); +if (lean_obj_tag(x_17) == 0) +{ +lean_object* x_18; lean_object* x_19; +x_18 = lean_ctor_get(x_17, 0); +lean_inc(x_18); +lean_dec_ref(x_17); lean_inc_ref(x_10); lean_inc_ref(x_6); -lean_inc(x_14); -x_15 = l_Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1(x_14, x_6, x_7, x_8, x_9, x_10, x_11); -if (lean_obj_tag(x_15) == 0) +lean_inc(x_18); +x_19 = l_Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1(x_18, x_6, x_7, x_8, x_9, x_10, x_11); +if (lean_obj_tag(x_19) == 0) { -lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; -x_16 = lean_ctor_get(x_15, 0); -lean_inc(x_16); -lean_dec_ref(x_15); -x_17 = lean_ctor_get(x_16, 2); -lean_inc_ref(x_17); -lean_dec(x_16); -x_18 = lean_box(x_5); -x_19 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___boxed), 14, 5); -lean_closure_set(x_19, 0, x_3); -lean_closure_set(x_19, 1, x_2); -lean_closure_set(x_19, 2, x_4); -lean_closure_set(x_19, 3, x_14); -lean_closure_set(x_19, 4, x_18); -x_20 = 0; -x_21 = l_Lean_Meta_forallTelescope___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__2___redArg(x_17, x_19, x_20, x_6, x_7, x_8, x_9, x_10, x_11); -return x_21; +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +lean_dec_ref(x_19); +x_21 = lean_ctor_get(x_20, 2); +lean_inc_ref(x_21); +lean_dec(x_20); +x_22 = lean_box(x_5); +x_23 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___boxed), 15, 6); +lean_closure_set(x_23, 0, x_3); +lean_closure_set(x_23, 1, x_16); +lean_closure_set(x_23, 2, x_4); +lean_closure_set(x_23, 3, x_15); +lean_closure_set(x_23, 4, x_18); +lean_closure_set(x_23, 5, x_22); +x_24 = 0; +x_25 = l_Lean_Meta_forallTelescope___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__2___redArg(x_21, x_23, x_24, x_6, x_7, x_8, x_9, x_10, x_11); +return x_25; } else { -uint8_t x_22; -lean_dec(x_14); -lean_dec(x_11); -lean_dec_ref(x_10); -lean_dec(x_9); -lean_dec_ref(x_8); -lean_dec(x_7); -lean_dec_ref(x_6); -lean_dec(x_4); -lean_dec_ref(x_3); -lean_dec(x_2); -x_22 = !lean_is_exclusive(x_15); -if (x_22 == 0) -{ -return x_15; -} -else -{ -lean_object* x_23; lean_object* x_24; -x_23 = lean_ctor_get(x_15, 0); -lean_inc(x_23); +uint8_t x_26; +lean_dec(x_18); lean_dec(x_15); -x_24 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_24, 0, x_23); -return x_24; -} -} -} -else -{ -uint8_t x_25; lean_dec(x_11); lean_dec_ref(x_10); lean_dec(x_9); @@ -9657,21 +9676,126 @@ lean_dec(x_7); lean_dec_ref(x_6); lean_dec(x_4); lean_dec_ref(x_3); -lean_dec(x_2); -x_25 = !lean_is_exclusive(x_13); -if (x_25 == 0) +x_26 = !lean_is_exclusive(x_19); +if (x_26 == 0) { +return x_19; +} +else +{ +lean_object* x_27; lean_object* x_28; +x_27 = lean_ctor_get(x_19, 0); +lean_inc(x_27); +lean_dec(x_19); +x_28 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_28, 0, x_27); +return x_28; +} +} +} +else +{ +uint8_t x_29; +lean_dec(x_15); +lean_dec(x_11); +lean_dec_ref(x_10); +lean_dec(x_9); +lean_dec_ref(x_8); +lean_dec(x_7); +lean_dec_ref(x_6); +lean_dec(x_4); +lean_dec_ref(x_3); +x_29 = !lean_is_exclusive(x_17); +if (x_29 == 0) +{ +return x_17; +} +else +{ +lean_object* x_30; lean_object* x_31; +x_30 = lean_ctor_get(x_17, 0); +lean_inc(x_30); +lean_dec(x_17); +x_31 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_31, 0, x_30); +return x_31; +} +} +} +else +{ +lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; +lean_dec(x_14); +lean_dec(x_4); +lean_dec_ref(x_3); +lean_dec(x_2); +x_32 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__1; +x_33 = l_Lean_MessageData_ofName(x_1); +x_34 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_34, 0, x_32); +lean_ctor_set(x_34, 1, x_33); +x_35 = l_Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3___redArg___closed__3; +x_36 = lean_alloc_ctor(7, 2, 0); +lean_ctor_set(x_36, 0, x_34); +lean_ctor_set(x_36, 1, x_35); +x_37 = l_Lean_throwError___at___00Lean_Elab_Tactic_elabGrindConfig_spec__1___redArg(x_36, x_6, x_7, x_8, x_9, x_10, x_11); +lean_dec(x_11); +lean_dec_ref(x_10); +lean_dec(x_9); +lean_dec_ref(x_8); +lean_dec(x_7); +return x_37; +} +} +else +{ +uint8_t x_38; +lean_dec(x_11); +lean_dec(x_9); +lean_dec_ref(x_8); +lean_dec(x_7); +lean_dec_ref(x_6); +lean_dec(x_4); +lean_dec_ref(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_38 = !lean_is_exclusive(x_13); +if (x_38 == 0) +{ +lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; +x_39 = lean_ctor_get(x_13, 0); +x_40 = lean_ctor_get(x_10, 5); +lean_inc(x_40); +lean_dec_ref(x_10); +x_41 = lean_io_error_to_string(x_39); +x_42 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_42, 0, x_41); +x_43 = l_Lean_MessageData_ofFormat(x_42); +x_44 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_44, 0, x_40); +lean_ctor_set(x_44, 1, x_43); +lean_ctor_set(x_13, 0, x_44); return x_13; } else { -lean_object* x_26; lean_object* x_27; -x_26 = lean_ctor_get(x_13, 0); -lean_inc(x_26); +lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; +x_45 = lean_ctor_get(x_13, 0); +lean_inc(x_45); lean_dec(x_13); -x_27 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_27, 0, x_26); -return x_27; +x_46 = lean_ctor_get(x_10, 5); +lean_inc(x_46); +lean_dec_ref(x_10); +x_47 = lean_io_error_to_string(x_45); +x_48 = lean_alloc_ctor(3, 1, 0); +lean_ctor_set(x_48, 0, x_47); +x_49 = l_Lean_MessageData_ofFormat(x_48); +x_50 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_50, 0, x_46); +lean_ctor_set(x_50, 1, x_49); +x_51 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_51, 0, x_50); +return x_51; } } } @@ -9685,20 +9809,38 @@ x_14 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPatt return x_14; } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6) { +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, uint8_t x_5, lean_object* x_6, lean_object* x_7) { _start: { -lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; -x_8 = lean_box(0); -x_9 = lean_box(x_4); -x_10 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___boxed), 12, 5); -lean_closure_set(x_10, 0, x_1); -lean_closure_set(x_10, 1, x_8); -lean_closure_set(x_10, 2, x_2); -lean_closure_set(x_10, 3, x_3); -lean_closure_set(x_10, 4, x_9); -x_11 = l_Lean_Elab_Command_liftTermElabM___redArg(x_10, x_5, x_6); -return x_11; +lean_object* x_9; +if (lean_obj_tag(x_1) == 1) +{ +lean_object* x_14; lean_object* x_15; +x_14 = lean_ctor_get(x_1, 0); +x_15 = l_Lean_TSyntax_getId(x_14); +x_9 = x_15; +goto block_13; +} +else +{ +lean_object* x_16; +x_16 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__1; +x_9 = x_16; +goto block_13; +} +block_13: +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; +x_10 = lean_box(x_5); +x_11 = lean_alloc_closure((void*)(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___boxed), 12, 5); +lean_closure_set(x_11, 0, x_9); +lean_closure_set(x_11, 1, x_2); +lean_closure_set(x_11, 2, x_3); +lean_closure_set(x_11, 3, x_4); +lean_closure_set(x_11, 4, x_10); +x_12 = l_Lean_Elab_Command_liftTermElabM___redArg(x_11, x_6, x_7); +return x_12; +} } } LEAN_EXPORT lean_object* l_Lean_Meta_forallTelescope___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) { @@ -9774,16 +9916,6 @@ lean_dec(x_3); return x_9; } } -LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { -_start: -{ -uint8_t x_8; lean_object* x_9; -x_8 = lean_unbox(x_4); -x_9 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_1, x_2, x_3, x_8, x_5, x_6); -lean_dec(x_6); -return x_9; -} -} LEAN_EXPORT lean_object* l_Lean_throwUnknownIdentifierAt___at___00Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3_spec__4___redArg___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: { @@ -9833,6 +9965,17 @@ lean_dec(x_1); return x_10; } } +LEAN_EXPORT lean_object* l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___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) { +_start: +{ +uint8_t x_9; lean_object* x_10; +x_9 = lean_unbox(x_5); +x_10 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_1, x_2, x_3, x_4, x_9, x_6, x_7); +lean_dec(x_7); +lean_dec(x_1); +return x_10; +} +} LEAN_EXPORT lean_object* l_Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { @@ -9957,27 +10100,24 @@ static lean_object* _init_l_Lean_Elab_Tactic_elabGrindPattern___closed__5() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("scoped", 6, 6); +x_1 = lean_mk_string_unchecked("ident", 5, 5); return x_1; } } static lean_object* _init_l_Lean_Elab_Tactic_elabGrindPattern___closed__6() { _start: { -lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +lean_object* x_1; lean_object* x_2; x_1 = l_Lean_Elab_Tactic_elabGrindPattern___closed__5; -x_2 = l_Lean_Elab_Tactic_elabGrindPattern___closed__2; -x_3 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__0; -x_4 = l_Lean_Elab_Tactic_evalUnsafe___redArg___closed__0_00___x40_Lean_Elab_Tactic_Grind_Main_2289994934____hygCtx___hyg_3_; -x_5 = l_Lean_Name_mkStr4(x_4, x_3, x_2, x_1); -return x_5; +x_2 = l_Lean_Name_mkStr1(x_1); +return x_2; } } static lean_object* _init_l_Lean_Elab_Tactic_elabGrindPattern___closed__7() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("local", 5, 5); +x_1 = lean_mk_string_unchecked("grindPatternCnstrs", 18, 18); return x_1; } } @@ -9986,7 +10126,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = l_Lean_Elab_Tactic_elabGrindPattern___closed__7; -x_2 = l_Lean_Elab_Tactic_elabGrindPattern___closed__2; +x_2 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__1; x_3 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__0; x_4 = l_Lean_Elab_Tactic_evalUnsafe___redArg___closed__0_00___x40_Lean_Elab_Tactic_Grind_Main_2289994934____hygCtx___hyg_3_; x_5 = l_Lean_Name_mkStr4(x_4, x_3, x_2, x_1); @@ -9997,24 +10137,27 @@ static lean_object* _init_l_Lean_Elab_Tactic_elabGrindPattern___closed__9() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("ident", 5, 5); +x_1 = lean_mk_string_unchecked("scoped", 6, 6); return x_1; } } static lean_object* _init_l_Lean_Elab_Tactic_elabGrindPattern___closed__10() { _start: { -lean_object* x_1; lean_object* x_2; +lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = l_Lean_Elab_Tactic_elabGrindPattern___closed__9; -x_2 = l_Lean_Name_mkStr1(x_1); -return x_2; +x_2 = l_Lean_Elab_Tactic_elabGrindPattern___closed__2; +x_3 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__0; +x_4 = l_Lean_Elab_Tactic_evalUnsafe___redArg___closed__0_00___x40_Lean_Elab_Tactic_Grind_Main_2289994934____hygCtx___hyg_3_; +x_5 = l_Lean_Name_mkStr4(x_4, x_3, x_2, x_1); +return x_5; } } static lean_object* _init_l_Lean_Elab_Tactic_elabGrindPattern___closed__11() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("grindPatternCnstrs", 18, 18); +x_1 = lean_mk_string_unchecked("local", 5, 5); return x_1; } } @@ -10023,7 +10166,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = l_Lean_Elab_Tactic_elabGrindPattern___closed__11; -x_2 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__1; +x_2 = l_Lean_Elab_Tactic_elabGrindPattern___closed__2; x_3 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__0; x_4 = l_Lean_Elab_Tactic_evalUnsafe___redArg___closed__0_00___x40_Lean_Elab_Tactic_Grind_Main_2289994934____hygCtx___hyg_3_; x_5 = l_Lean_Name_mkStr4(x_4, x_3, x_2, x_1); @@ -10033,367 +10176,586 @@ return x_5; LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabGrindPattern(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { -lean_object* x_5; uint8_t x_6; -x_5 = l_Lean_Elab_Tactic_elabGrindPattern___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; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_38; uint8_t x_39; +x_38 = l_Lean_Elab_Tactic_elabGrindPattern___closed__1; lean_inc(x_1); -x_6 = l_Lean_Syntax_isOfKind(x_1, x_5); -if (x_6 == 0) +x_39 = l_Lean_Syntax_isOfKind(x_1, x_38); +if (x_39 == 0) { -lean_object* x_7; +lean_object* x_40; lean_dec_ref(x_2); lean_dec(x_1); -x_7 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_7; +x_40 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_40; } else { -lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; -x_8 = lean_unsigned_to_nat(0u); -x_9 = l_Lean_Syntax_getArg(x_1, x_8); -x_10 = l_Lean_Elab_Tactic_elabGrindPattern___closed__4; -lean_inc(x_9); -x_11 = l_Lean_Syntax_isOfKind(x_9, x_10); -if (x_11 == 0) +lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; +x_41 = lean_unsigned_to_nat(0u); +x_42 = l_Lean_Syntax_getArg(x_1, x_41); +x_43 = l_Lean_Elab_Tactic_elabGrindPattern___closed__4; +lean_inc(x_42); +x_44 = l_Lean_Syntax_isOfKind(x_42, x_43); +if (x_44 == 0) { -lean_object* x_12; -lean_dec(x_9); +lean_object* x_45; +lean_dec(x_42); lean_dec_ref(x_2); lean_dec(x_1); -x_12 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_12; +x_45 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_45; } else { -lean_object* x_13; uint8_t x_14; -x_13 = l_Lean_Syntax_getArg(x_9, x_8); -lean_dec(x_9); -lean_inc(x_13); -x_14 = l_Lean_Syntax_matchesNull(x_13, x_8); -if (x_14 == 0) +lean_object* x_46; uint8_t x_47; +x_46 = l_Lean_Syntax_getArg(x_42, x_41); +lean_dec(x_42); +lean_inc(x_46); +x_47 = l_Lean_Syntax_matchesNull(x_46, x_41); +if (x_47 == 0) { -lean_object* x_15; uint8_t x_16; -x_15 = lean_unsigned_to_nat(1u); -lean_inc(x_13); -x_16 = l_Lean_Syntax_matchesNull(x_13, x_15); -if (x_16 == 0) -{ -lean_object* x_17; -lean_dec(x_13); -lean_dec_ref(x_2); -lean_dec(x_1); -x_17 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_17; -} -else -{ -lean_object* x_18; lean_object* x_19; uint8_t x_20; -x_18 = l_Lean_Syntax_getArg(x_13, x_8); -lean_dec(x_13); -x_19 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; -lean_inc(x_18); -x_20 = l_Lean_Syntax_isOfKind(x_18, x_19); -if (x_20 == 0) -{ -lean_object* x_21; uint8_t x_22; -x_21 = l_Lean_Elab_Tactic_elabGrindPattern___closed__8; -x_22 = l_Lean_Syntax_isOfKind(x_18, x_21); -if (x_22 == 0) -{ -lean_object* x_23; -lean_dec_ref(x_2); -lean_dec(x_1); -x_23 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_23; -} -else -{ -lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; -x_24 = lean_unsigned_to_nat(2u); -x_25 = l_Lean_Syntax_getArg(x_1, x_24); -x_26 = l_Lean_Elab_Tactic_elabGrindPattern___closed__10; -lean_inc(x_25); -x_27 = l_Lean_Syntax_isOfKind(x_25, x_26); -if (x_27 == 0) -{ -lean_object* x_28; -lean_dec(x_25); -lean_dec_ref(x_2); -lean_dec(x_1); -x_28 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_28; -} -else -{ -lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_39; lean_object* x_40; uint8_t x_41; -x_29 = lean_unsigned_to_nat(4u); -x_30 = l_Lean_Syntax_getArg(x_1, x_29); -x_39 = lean_unsigned_to_nat(5u); -x_40 = l_Lean_Syntax_getArg(x_1, x_39); -lean_dec(x_1); -x_41 = l_Lean_Syntax_isNone(x_40); -if (x_41 == 0) -{ -uint8_t x_42; -lean_inc(x_40); -x_42 = l_Lean_Syntax_matchesNull(x_40, x_15); -if (x_42 == 0) -{ -lean_object* x_43; -lean_dec(x_40); -lean_dec(x_30); -lean_dec(x_25); -lean_dec_ref(x_2); -x_43 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_43; -} -else -{ -lean_object* x_44; lean_object* x_45; uint8_t x_46; -x_44 = l_Lean_Syntax_getArg(x_40, x_8); -lean_dec(x_40); -x_45 = l_Lean_Elab_Tactic_elabGrindPattern___closed__12; -lean_inc(x_44); -x_46 = l_Lean_Syntax_isOfKind(x_44, x_45); -if (x_46 == 0) -{ -lean_object* x_47; -lean_dec(x_44); -lean_dec(x_30); -lean_dec(x_25); -lean_dec_ref(x_2); -x_47 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_47; -} -else -{ -lean_object* x_48; -x_48 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_48, 0, x_44); -x_31 = x_48; -x_32 = x_2; -x_33 = x_3; -x_34 = lean_box(0); -goto block_38; -} -} -} -else -{ -lean_object* x_49; -lean_dec(x_40); -x_49 = lean_box(0); -x_31 = x_49; -x_32 = x_2; -x_33 = x_3; -x_34 = lean_box(0); -goto block_38; -} -block_38: -{ -lean_object* x_35; uint8_t x_36; lean_object* x_37; -x_35 = l_Lean_Syntax_getArgs(x_30); -lean_dec(x_30); -x_36 = 1; -x_37 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_25, x_35, x_31, x_36, x_32, x_33); -return x_37; -} -} -} -} -else -{ -lean_object* x_50; lean_object* x_51; lean_object* x_52; uint8_t x_53; -lean_dec(x_18); -x_50 = lean_unsigned_to_nat(2u); -x_51 = l_Lean_Syntax_getArg(x_1, x_50); -x_52 = l_Lean_Elab_Tactic_elabGrindPattern___closed__10; -lean_inc(x_51); -x_53 = l_Lean_Syntax_isOfKind(x_51, x_52); -if (x_53 == 0) -{ -lean_object* x_54; -lean_dec(x_51); -lean_dec_ref(x_2); -lean_dec(x_1); -x_54 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_54; -} -else -{ -lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_65; lean_object* x_66; uint8_t x_67; -x_55 = lean_unsigned_to_nat(4u); -x_56 = l_Lean_Syntax_getArg(x_1, x_55); -x_65 = lean_unsigned_to_nat(5u); -x_66 = l_Lean_Syntax_getArg(x_1, x_65); -lean_dec(x_1); -x_67 = l_Lean_Syntax_isNone(x_66); -if (x_67 == 0) -{ -uint8_t x_68; -lean_inc(x_66); -x_68 = l_Lean_Syntax_matchesNull(x_66, x_15); -if (x_68 == 0) -{ -lean_object* x_69; -lean_dec(x_66); -lean_dec(x_56); -lean_dec(x_51); -lean_dec_ref(x_2); -x_69 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_69; -} -else -{ -lean_object* x_70; lean_object* x_71; uint8_t x_72; -x_70 = l_Lean_Syntax_getArg(x_66, x_8); -lean_dec(x_66); -x_71 = l_Lean_Elab_Tactic_elabGrindPattern___closed__12; -lean_inc(x_70); -x_72 = l_Lean_Syntax_isOfKind(x_70, x_71); -if (x_72 == 0) -{ -lean_object* x_73; -lean_dec(x_70); -lean_dec(x_56); -lean_dec(x_51); -lean_dec_ref(x_2); -x_73 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_73; -} -else -{ -lean_object* x_74; -x_74 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_74, 0, x_70); -x_57 = x_74; -x_58 = x_2; -x_59 = x_3; -x_60 = lean_box(0); -goto block_64; -} -} -} -else -{ -lean_object* x_75; -lean_dec(x_66); -x_75 = lean_box(0); -x_57 = x_75; -x_58 = x_2; -x_59 = x_3; -x_60 = lean_box(0); -goto block_64; -} -block_64: -{ -lean_object* x_61; uint8_t x_62; lean_object* x_63; -x_61 = l_Lean_Syntax_getArgs(x_56); -lean_dec(x_56); -x_62 = 2; -x_63 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_51, x_61, x_57, x_62, x_58, x_59); -return x_63; -} -} -} -} -} -else -{ -lean_object* x_76; lean_object* x_77; lean_object* x_78; uint8_t x_79; -lean_dec(x_13); -x_76 = lean_unsigned_to_nat(2u); -x_77 = l_Lean_Syntax_getArg(x_1, x_76); -x_78 = l_Lean_Elab_Tactic_elabGrindPattern___closed__10; -lean_inc(x_77); -x_79 = l_Lean_Syntax_isOfKind(x_77, x_78); -if (x_79 == 0) -{ -lean_object* x_80; -lean_dec(x_77); -lean_dec_ref(x_2); -lean_dec(x_1); -x_80 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_80; -} -else -{ -lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_91; lean_object* x_92; uint8_t x_93; -x_81 = lean_unsigned_to_nat(4u); -x_82 = l_Lean_Syntax_getArg(x_1, x_81); -x_91 = lean_unsigned_to_nat(5u); -x_92 = l_Lean_Syntax_getArg(x_1, x_91); -lean_dec(x_1); -x_93 = l_Lean_Syntax_isNone(x_92); -if (x_93 == 0) -{ -lean_object* x_94; uint8_t x_95; -x_94 = lean_unsigned_to_nat(1u); -lean_inc(x_92); -x_95 = l_Lean_Syntax_matchesNull(x_92, x_94); +lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; uint8_t x_95; +x_48 = lean_unsigned_to_nat(1u); +lean_inc(x_46); +x_95 = l_Lean_Syntax_matchesNull(x_46, x_48); if (x_95 == 0) { lean_object* x_96; -lean_dec(x_92); -lean_dec(x_82); -lean_dec(x_77); +lean_dec(x_46); lean_dec_ref(x_2); +lean_dec(x_1); x_96 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); return x_96; } else { lean_object* x_97; lean_object* x_98; uint8_t x_99; -x_97 = l_Lean_Syntax_getArg(x_92, x_8); -lean_dec(x_92); -x_98 = l_Lean_Elab_Tactic_elabGrindPattern___closed__12; +x_97 = l_Lean_Syntax_getArg(x_46, x_41); +lean_dec(x_46); +x_98 = l_Lean_Elab_Tactic_elabGrindPattern___closed__10; lean_inc(x_97); x_99 = l_Lean_Syntax_isOfKind(x_97, x_98); if (x_99 == 0) { -lean_object* x_100; -lean_dec(x_97); -lean_dec(x_82); -lean_dec(x_77); -lean_dec_ref(x_2); -x_100 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); -return x_100; -} -else -{ -lean_object* x_101; -x_101 = lean_alloc_ctor(1, 1, 0); -lean_ctor_set(x_101, 0, x_97); -x_83 = x_101; -x_84 = x_2; -x_85 = x_3; -x_86 = lean_box(0); -goto block_90; -} -} -} -else +lean_object* x_100; uint8_t x_101; +x_100 = l_Lean_Elab_Tactic_elabGrindPattern___closed__12; +x_101 = l_Lean_Syntax_isOfKind(x_97, x_100); +if (x_101 == 0) { lean_object* x_102; -lean_dec(x_92); -x_102 = lean_box(0); -x_83 = x_102; -x_84 = x_2; -x_85 = x_3; -x_86 = lean_box(0); -goto block_90; +lean_dec_ref(x_2); +lean_dec(x_1); +x_102 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_102; } -block_90: +else { -lean_object* x_87; uint8_t x_88; lean_object* x_89; -x_87 = l_Lean_Syntax_getArgs(x_82); +lean_object* x_103; lean_object* x_104; uint8_t x_105; +x_103 = lean_unsigned_to_nat(2u); +x_104 = l_Lean_Syntax_getArg(x_1, x_103); +x_105 = l_Lean_Syntax_isNone(x_104); +if (x_105 == 0) +{ +lean_object* x_106; uint8_t x_107; +x_106 = lean_unsigned_to_nat(3u); +lean_inc(x_104); +x_107 = l_Lean_Syntax_matchesNull(x_104, x_106); +if (x_107 == 0) +{ +lean_object* x_108; +lean_dec(x_104); +lean_dec_ref(x_2); +lean_dec(x_1); +x_108 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_108; +} +else +{ +lean_object* x_109; lean_object* x_110; uint8_t x_111; +x_109 = l_Lean_Syntax_getArg(x_104, x_48); +lean_dec(x_104); +x_110 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; +lean_inc(x_109); +x_111 = l_Lean_Syntax_isOfKind(x_109, x_110); +if (x_111 == 0) +{ +lean_object* x_112; +lean_dec(x_109); +lean_dec_ref(x_2); +lean_dec(x_1); +x_112 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_112; +} +else +{ +lean_object* x_113; +x_113 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_113, 0, x_109); +x_72 = x_113; +x_73 = x_2; +x_74 = x_3; +x_75 = lean_box(0); +goto block_94; +} +} +} +else +{ +lean_object* x_114; +lean_dec(x_104); +x_114 = lean_box(0); +x_72 = x_114; +x_73 = x_2; +x_74 = x_3; +x_75 = lean_box(0); +goto block_94; +} +} +} +else +{ +lean_object* x_115; lean_object* x_116; uint8_t x_117; +lean_dec(x_97); +x_115 = lean_unsigned_to_nat(2u); +x_116 = l_Lean_Syntax_getArg(x_1, x_115); +x_117 = l_Lean_Syntax_isNone(x_116); +if (x_117 == 0) +{ +lean_object* x_118; uint8_t x_119; +x_118 = lean_unsigned_to_nat(3u); +lean_inc(x_116); +x_119 = l_Lean_Syntax_matchesNull(x_116, x_118); +if (x_119 == 0) +{ +lean_object* x_120; +lean_dec(x_116); +lean_dec_ref(x_2); +lean_dec(x_1); +x_120 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_120; +} +else +{ +lean_object* x_121; lean_object* x_122; uint8_t x_123; +x_121 = l_Lean_Syntax_getArg(x_116, x_48); +lean_dec(x_116); +x_122 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; +lean_inc(x_121); +x_123 = l_Lean_Syntax_isOfKind(x_121, x_122); +if (x_123 == 0) +{ +lean_object* x_124; +lean_dec(x_121); +lean_dec_ref(x_2); +lean_dec(x_1); +x_124 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_124; +} +else +{ +lean_object* x_125; +x_125 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_125, 0, x_121); +x_49 = x_125; +x_50 = x_2; +x_51 = x_3; +x_52 = lean_box(0); +goto block_71; +} +} +} +else +{ +lean_object* x_126; +lean_dec(x_116); +x_126 = lean_box(0); +x_49 = x_126; +x_50 = x_2; +x_51 = x_3; +x_52 = lean_box(0); +goto block_71; +} +} +} +block_71: +{ +lean_object* x_53; lean_object* x_54; lean_object* x_55; uint8_t x_56; +x_53 = lean_unsigned_to_nat(3u); +x_54 = l_Lean_Syntax_getArg(x_1, x_53); +x_55 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; +lean_inc(x_54); +x_56 = l_Lean_Syntax_isOfKind(x_54, x_55); +if (x_56 == 0) +{ +lean_object* x_57; +lean_dec(x_54); +lean_dec_ref(x_50); +lean_dec(x_49); +lean_dec(x_1); +x_57 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_57; +} +else +{ +lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; uint8_t x_62; +x_58 = lean_unsigned_to_nat(5u); +x_59 = l_Lean_Syntax_getArg(x_1, x_58); +x_60 = lean_unsigned_to_nat(6u); +x_61 = l_Lean_Syntax_getArg(x_1, x_60); +lean_dec(x_1); +x_62 = l_Lean_Syntax_isNone(x_61); +if (x_62 == 0) +{ +uint8_t x_63; +lean_inc(x_61); +x_63 = l_Lean_Syntax_matchesNull(x_61, x_48); +if (x_63 == 0) +{ +lean_object* x_64; +lean_dec(x_61); +lean_dec(x_59); +lean_dec(x_54); +lean_dec_ref(x_50); +lean_dec(x_49); +x_64 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_64; +} +else +{ +lean_object* x_65; lean_object* x_66; uint8_t x_67; +x_65 = l_Lean_Syntax_getArg(x_61, x_41); +lean_dec(x_61); +x_66 = l_Lean_Elab_Tactic_elabGrindPattern___closed__8; +lean_inc(x_65); +x_67 = l_Lean_Syntax_isOfKind(x_65, x_66); +if (x_67 == 0) +{ +lean_object* x_68; +lean_dec(x_65); +lean_dec(x_59); +lean_dec(x_54); +lean_dec_ref(x_50); +lean_dec(x_49); +x_68 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_68; +} +else +{ +lean_object* x_69; +x_69 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_69, 0, x_65); +x_27 = x_49; +x_28 = x_54; +x_29 = x_59; +x_30 = x_69; +x_31 = x_50; +x_32 = x_51; +x_33 = lean_box(0); +goto block_37; +} +} +} +else +{ +lean_object* x_70; +lean_dec(x_61); +x_70 = lean_box(0); +x_27 = x_49; +x_28 = x_54; +x_29 = x_59; +x_30 = x_70; +x_31 = x_50; +x_32 = x_51; +x_33 = lean_box(0); +goto block_37; +} +} +} +block_94: +{ +lean_object* x_76; lean_object* x_77; lean_object* x_78; uint8_t x_79; +x_76 = lean_unsigned_to_nat(3u); +x_77 = l_Lean_Syntax_getArg(x_1, x_76); +x_78 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; +lean_inc(x_77); +x_79 = l_Lean_Syntax_isOfKind(x_77, x_78); +if (x_79 == 0) +{ +lean_object* x_80; +lean_dec(x_77); +lean_dec_ref(x_73); +lean_dec(x_72); +lean_dec(x_1); +x_80 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_80; +} +else +{ +lean_object* x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; uint8_t x_85; +x_81 = lean_unsigned_to_nat(5u); +x_82 = l_Lean_Syntax_getArg(x_1, x_81); +x_83 = lean_unsigned_to_nat(6u); +x_84 = l_Lean_Syntax_getArg(x_1, x_83); +lean_dec(x_1); +x_85 = l_Lean_Syntax_isNone(x_84); +if (x_85 == 0) +{ +uint8_t x_86; +lean_inc(x_84); +x_86 = l_Lean_Syntax_matchesNull(x_84, x_48); +if (x_86 == 0) +{ +lean_object* x_87; +lean_dec(x_84); lean_dec(x_82); -x_88 = 0; -x_89 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_77, x_87, x_83, x_88, x_84, x_85); -return x_89; +lean_dec(x_77); +lean_dec_ref(x_73); +lean_dec(x_72); +x_87 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_87; +} +else +{ +lean_object* x_88; lean_object* x_89; uint8_t x_90; +x_88 = l_Lean_Syntax_getArg(x_84, x_41); +lean_dec(x_84); +x_89 = l_Lean_Elab_Tactic_elabGrindPattern___closed__8; +lean_inc(x_88); +x_90 = l_Lean_Syntax_isOfKind(x_88, x_89); +if (x_90 == 0) +{ +lean_object* x_91; +lean_dec(x_88); +lean_dec(x_82); +lean_dec(x_77); +lean_dec_ref(x_73); +lean_dec(x_72); +x_91 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_91; +} +else +{ +lean_object* x_92; +x_92 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_92, 0, x_88); +x_16 = x_72; +x_17 = x_77; +x_18 = x_82; +x_19 = x_92; +x_20 = x_73; +x_21 = x_74; +x_22 = lean_box(0); +goto block_26; +} +} +} +else +{ +lean_object* x_93; +lean_dec(x_84); +x_93 = lean_box(0); +x_16 = x_72; +x_17 = x_77; +x_18 = x_82; +x_19 = x_93; +x_20 = x_73; +x_21 = x_74; +x_22 = lean_box(0); +goto block_26; } } } } +else +{ +lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_151; lean_object* x_152; uint8_t x_153; +lean_dec(x_46); +x_127 = lean_unsigned_to_nat(1u); +x_151 = lean_unsigned_to_nat(2u); +x_152 = l_Lean_Syntax_getArg(x_1, x_151); +x_153 = l_Lean_Syntax_isNone(x_152); +if (x_153 == 0) +{ +lean_object* x_154; uint8_t x_155; +x_154 = lean_unsigned_to_nat(3u); +lean_inc(x_152); +x_155 = l_Lean_Syntax_matchesNull(x_152, x_154); +if (x_155 == 0) +{ +lean_object* x_156; +lean_dec(x_152); +lean_dec_ref(x_2); +lean_dec(x_1); +x_156 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_156; +} +else +{ +lean_object* x_157; lean_object* x_158; uint8_t x_159; +x_157 = l_Lean_Syntax_getArg(x_152, x_127); +lean_dec(x_152); +x_158 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; +lean_inc(x_157); +x_159 = l_Lean_Syntax_isOfKind(x_157, x_158); +if (x_159 == 0) +{ +lean_object* x_160; +lean_dec(x_157); +lean_dec_ref(x_2); +lean_dec(x_1); +x_160 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_160; +} +else +{ +lean_object* x_161; +x_161 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_161, 0, x_157); +x_128 = x_161; +x_129 = x_2; +x_130 = x_3; +x_131 = lean_box(0); +goto block_150; +} +} +} +else +{ +lean_object* x_162; +lean_dec(x_152); +x_162 = lean_box(0); +x_128 = x_162; +x_129 = x_2; +x_130 = x_3; +x_131 = lean_box(0); +goto block_150; +} +block_150: +{ +lean_object* x_132; lean_object* x_133; lean_object* x_134; uint8_t x_135; +x_132 = lean_unsigned_to_nat(3u); +x_133 = l_Lean_Syntax_getArg(x_1, x_132); +x_134 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; +lean_inc(x_133); +x_135 = l_Lean_Syntax_isOfKind(x_133, x_134); +if (x_135 == 0) +{ +lean_object* x_136; +lean_dec(x_133); +lean_dec_ref(x_129); +lean_dec(x_128); +lean_dec(x_1); +x_136 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_136; +} +else +{ +lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140; uint8_t x_141; +x_137 = lean_unsigned_to_nat(5u); +x_138 = l_Lean_Syntax_getArg(x_1, x_137); +x_139 = lean_unsigned_to_nat(6u); +x_140 = l_Lean_Syntax_getArg(x_1, x_139); +lean_dec(x_1); +x_141 = l_Lean_Syntax_isNone(x_140); +if (x_141 == 0) +{ +uint8_t x_142; +lean_inc(x_140); +x_142 = l_Lean_Syntax_matchesNull(x_140, x_127); +if (x_142 == 0) +{ +lean_object* x_143; +lean_dec(x_140); +lean_dec(x_138); +lean_dec(x_133); +lean_dec_ref(x_129); +lean_dec(x_128); +x_143 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_143; +} +else +{ +lean_object* x_144; lean_object* x_145; uint8_t x_146; +x_144 = l_Lean_Syntax_getArg(x_140, x_41); +lean_dec(x_140); +x_145 = l_Lean_Elab_Tactic_elabGrindPattern___closed__8; +lean_inc(x_144); +x_146 = l_Lean_Syntax_isOfKind(x_144, x_145); +if (x_146 == 0) +{ +lean_object* x_147; +lean_dec(x_144); +lean_dec(x_138); +lean_dec(x_133); +lean_dec_ref(x_129); +lean_dec(x_128); +x_147 = l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg(); +return x_147; +} +else +{ +lean_object* x_148; +x_148 = lean_alloc_ctor(1, 1, 0); +lean_ctor_set(x_148, 0, x_144); +x_5 = x_133; +x_6 = x_128; +x_7 = x_138; +x_8 = x_148; +x_9 = x_129; +x_10 = x_130; +x_11 = lean_box(0); +goto block_15; +} +} +} +else +{ +lean_object* x_149; +lean_dec(x_140); +x_149 = lean_box(0); +x_5 = x_133; +x_6 = x_128; +x_7 = x_138; +x_8 = x_149; +x_9 = x_129; +x_10 = x_130; +x_11 = lean_box(0); +goto block_15; +} +} +} +} +} +} +block_15: +{ +lean_object* x_12; uint8_t x_13; lean_object* x_14; +x_12 = l_Lean_Syntax_getArgs(x_7); +lean_dec(x_7); +x_13 = 0; +x_14 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_6, x_5, x_12, x_8, x_13, x_9, x_10); +lean_dec(x_6); +return x_14; +} +block_26: +{ +lean_object* x_23; uint8_t x_24; lean_object* x_25; +x_23 = l_Lean_Syntax_getArgs(x_18); +lean_dec(x_18); +x_24 = 1; +x_25 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_16, x_17, x_23, x_19, x_24, x_20, x_21); +lean_dec(x_16); +return x_25; +} +block_37: +{ +lean_object* x_34; uint8_t x_35; lean_object* x_36; +x_34 = l_Lean_Syntax_getArgs(x_29); +lean_dec(x_29); +x_35 = 2; +x_36 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go(x_27, x_28, x_34, x_30, x_35, x_31, x_32); +lean_dec(x_27); +return x_36; } } } @@ -10555,6 +10917,14 @@ return x_12; } } } +static lean_object* _init_l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Meta_Grind_grindExt; +return x_1; +} +} LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) { _start: { @@ -10567,7 +10937,7 @@ lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean x_11 = lean_ctor_get(x_9, 0); x_12 = lean_ctor_get(x_9, 5); lean_dec(x_12); -x_13 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0; +x_13 = l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0; x_14 = l_Lean_ScopedEnvExtension_modifyState___redArg(x_13, x_11, x_1); x_15 = l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0___closed__6; lean_ctor_set(x_9, 5, x_15); @@ -10634,7 +11004,7 @@ lean_inc(x_35); lean_inc(x_34); lean_inc(x_33); lean_dec(x_9); -x_41 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0; +x_41 = l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0; x_42 = l_Lean_ScopedEnvExtension_modifyState___redArg(x_41, x_33, x_1); x_43 = l___private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0___closed__6; x_44 = lean_alloc_ctor(0, 9, 0); @@ -12272,18 +12642,18 @@ if (x_37 == 0) { uint8_t x_38; x_38 = l_Lean_Exception_isRuntime(x_36); -x_16 = lean_box(0); +x_16 = x_24; x_17 = x_34; -x_18 = x_24; +x_18 = lean_box(0); x_19 = x_38; goto block_20; } else { lean_dec(x_36); -x_16 = lean_box(0); +x_16 = x_24; x_17 = x_34; -x_18 = x_24; +x_18 = lean_box(0); x_19 = x_37; goto block_20; } @@ -12304,13 +12674,13 @@ block_20: if (x_19 == 0) { lean_dec_ref(x_17); -x_10 = x_18; +x_10 = x_16; x_11 = lean_box(0); goto block_15; } else { -lean_dec_ref(x_18); +lean_dec_ref(x_16); lean_dec(x_8); lean_dec_ref(x_7); lean_dec(x_6); @@ -12523,7 +12893,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__0() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("grind", 5, 5); +x_1 = lean_mk_string_unchecked("debug", 5, 5); return x_1; } } @@ -12531,30 +12901,22 @@ static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string_unchecked("debug", 5, 5); +x_1 = lean_mk_string_unchecked("inj", 3, 3); return x_1; } } static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__2() { _start: { -lean_object* x_1; -x_1 = lean_mk_string_unchecked("inj", 3, 3); -return x_1; -} -} -static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__3() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Elab_Tactic_mkGrindParams___closed__2; -x_2 = l_Lean_Elab_Tactic_mkGrindParams___closed__1; -x_3 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_1 = l_Lean_Elab_Tactic_mkGrindParams___closed__1; +x_2 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_3 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_4 = l_Lean_Name_mkStr3(x_3, x_2, x_1); return x_4; } } -static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__4() { +static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__3() { _start: { lean_object* x_1; @@ -12562,7 +12924,7 @@ x_1 = l_Lean_Meta_Grind_instInhabitedExtensionState_default; return x_1; } } -static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__5() { +static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__4() { _start: { lean_object* x_1; lean_object* x_2; @@ -12571,11 +12933,11 @@ x_2 = lean_mk_empty_array_with_capacity(x_1); return x_2; } } -static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__6() { +static lean_object* _init_l_Lean_Elab_Tactic_mkGrindParams___closed__5() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_1 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_2 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_2, 0, x_1); return x_2; @@ -12844,7 +13206,7 @@ lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; uint x_83 = lean_ctor_get(x_82, 0); lean_inc(x_83); lean_dec_ref(x_82); -x_84 = l_Lean_Elab_Tactic_mkGrindParams___closed__3; +x_84 = l_Lean_Elab_Tactic_mkGrindParams___closed__2; x_85 = l_Lean_isTracingEnabledFor___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__2___redArg(x_84, x_78); x_86 = lean_ctor_get(x_85, 0); lean_inc(x_86); @@ -12910,7 +13272,7 @@ x_104 = lean_ctor_get(x_83, 7); lean_inc_ref(x_104); x_105 = lean_ctor_get(x_83, 8); lean_inc(x_105); -x_106 = l_Lean_Elab_Tactic_mkGrindParams___closed__4; +x_106 = l_Lean_Elab_Tactic_mkGrindParams___closed__3; x_107 = lean_unsigned_to_nat(0u); x_108 = lean_array_get_borrowed(x_106, x_98, x_107); x_109 = lean_ctor_get(x_108, 4); @@ -12988,7 +13350,7 @@ if (x_128 == 0) { lean_object* x_129; lean_dec(x_4); -x_129 = l_Lean_Elab_Tactic_mkGrindParams___closed__5; +x_129 = l_Lean_Elab_Tactic_mkGrindParams___closed__4; x_72 = x_120; x_73 = x_129; x_74 = x_121; @@ -13007,7 +13369,7 @@ x_130 = lean_box(x_128); x_131 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_mkGrindParams___lam__0___boxed), 7, 1); lean_closure_set(x_131, 0, x_130); x_132 = lean_unsigned_to_nat(100u); -x_133 = l_Lean_Elab_Tactic_mkGrindParams___closed__6; +x_133 = l_Lean_Elab_Tactic_mkGrindParams___closed__5; x_134 = lean_box(0); x_135 = lean_alloc_ctor(0, 4, 0); lean_ctor_set(x_135, 0, x_132); @@ -15149,7 +15511,7 @@ return x_1; LEAN_EXPORT lean_object* l_Lean_logAt___at___00Lean_logWarningAt___at___00Lean_Elab_Tactic_evalGrindCore_spec__0_spec__0___redArg(lean_object* x_1, lean_object* x_2, uint8_t x_3, uint8_t x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) { _start: { -lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_50; lean_object* x_51; uint8_t x_52; uint8_t x_53; lean_object* x_54; uint8_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_77; lean_object* x_78; lean_object* x_79; uint8_t x_80; uint8_t x_81; lean_object* x_82; uint8_t x_83; lean_object* x_84; lean_object* x_88; lean_object* x_89; uint8_t x_90; lean_object* x_91; uint8_t x_92; lean_object* x_93; uint8_t x_94; uint8_t x_100; lean_object* x_101; uint8_t x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; uint8_t x_106; uint8_t x_107; uint8_t x_109; uint8_t x_125; +uint8_t x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_50; uint8_t x_51; uint8_t x_52; lean_object* x_53; uint8_t x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_77; uint8_t x_78; uint8_t x_79; lean_object* x_80; uint8_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_88; uint8_t x_89; uint8_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; uint8_t x_94; uint8_t x_100; lean_object* x_101; uint8_t x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; uint8_t x_106; uint8_t x_107; uint8_t x_109; uint8_t x_125; x_100 = 2; x_125 = l_Lean_instBEqMessageSeverity_beq(x_3, x_100); if (x_125 == 0) @@ -15184,14 +15546,14 @@ lean_ctor_set(x_25, 0, x_21); lean_ctor_set(x_25, 1, x_22); x_26 = lean_alloc_ctor(4, 2, 0); lean_ctor_set(x_26, 0, x_25); -lean_ctor_set(x_26, 1, x_14); +lean_ctor_set(x_26, 1, x_15); x_27 = lean_alloc_ctor(0, 5, 3); -lean_ctor_set(x_27, 0, x_11); -lean_ctor_set(x_27, 1, x_10); +lean_ctor_set(x_27, 0, x_14); +lean_ctor_set(x_27, 1, x_13); lean_ctor_set(x_27, 2, x_16); -lean_ctor_set(x_27, 3, x_13); +lean_ctor_set(x_27, 3, x_11); lean_ctor_set(x_27, 4, x_26); -lean_ctor_set_uint8(x_27, sizeof(void*)*5, x_15); +lean_ctor_set_uint8(x_27, sizeof(void*)*5, x_10); lean_ctor_set_uint8(x_27, sizeof(void*)*5 + 1, x_12); lean_ctor_set_uint8(x_27, sizeof(void*)*5 + 2, x_4); x_28 = l_Lean_MessageLog_add(x_27, x_24); @@ -15229,14 +15591,14 @@ lean_ctor_set(x_41, 0, x_21); lean_ctor_set(x_41, 1, x_22); x_42 = lean_alloc_ctor(4, 2, 0); lean_ctor_set(x_42, 0, x_41); -lean_ctor_set(x_42, 1, x_14); +lean_ctor_set(x_42, 1, x_15); x_43 = lean_alloc_ctor(0, 5, 3); -lean_ctor_set(x_43, 0, x_11); -lean_ctor_set(x_43, 1, x_10); +lean_ctor_set(x_43, 0, x_14); +lean_ctor_set(x_43, 1, x_13); lean_ctor_set(x_43, 2, x_16); -lean_ctor_set(x_43, 3, x_13); +lean_ctor_set(x_43, 3, x_11); lean_ctor_set(x_43, 4, x_42); -lean_ctor_set_uint8(x_43, sizeof(void*)*5, x_15); +lean_ctor_set_uint8(x_43, sizeof(void*)*5, x_10); lean_ctor_set_uint8(x_43, sizeof(void*)*5 + 1, x_12); lean_ctor_set_uint8(x_43, sizeof(void*)*5 + 2, x_4); x_44 = l_Lean_MessageLog_add(x_43, x_38); @@ -15267,24 +15629,24 @@ if (x_60 == 0) { lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; x_61 = lean_ctor_get(x_59, 0); -lean_inc_ref(x_54); -x_62 = l_Lean_FileMap_toPosition(x_54, x_56); -lean_dec(x_56); -x_63 = l_Lean_FileMap_toPosition(x_54, x_57); +lean_inc_ref(x_55); +x_62 = l_Lean_FileMap_toPosition(x_55, x_53); +lean_dec(x_53); +x_63 = l_Lean_FileMap_toPosition(x_55, x_57); lean_dec(x_57); x_64 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_64, 0, x_63); x_65 = l_Lean_addTrace___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__3___redArg___closed__1; -if (x_52 == 0) +if (x_54 == 0) { lean_free_object(x_59); lean_dec_ref(x_50); -x_10 = x_62; -x_11 = x_51; -x_12 = x_53; -x_13 = x_65; -x_14 = x_61; -x_15 = x_55; +x_10 = x_51; +x_11 = x_65; +x_12 = x_52; +x_13 = x_62; +x_14 = x_56; +x_15 = x_61; x_16 = x_64; x_17 = x_7; x_18 = x_8; @@ -15302,7 +15664,7 @@ lean_object* x_67; lean_dec_ref(x_64); lean_dec_ref(x_62); lean_dec(x_61); -lean_dec_ref(x_51); +lean_dec_ref(x_56); lean_dec_ref(x_7); x_67 = lean_box(0); lean_ctor_set(x_59, 0, x_67); @@ -15311,12 +15673,12 @@ return x_59; else { lean_free_object(x_59); -x_10 = x_62; -x_11 = x_51; -x_12 = x_53; -x_13 = x_65; -x_14 = x_61; -x_15 = x_55; +x_10 = x_51; +x_11 = x_65; +x_12 = x_52; +x_13 = x_62; +x_14 = x_56; +x_15 = x_61; x_16 = x_64; x_17 = x_7; x_18 = x_8; @@ -15331,23 +15693,23 @@ lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean x_68 = lean_ctor_get(x_59, 0); lean_inc(x_68); lean_dec(x_59); -lean_inc_ref(x_54); -x_69 = l_Lean_FileMap_toPosition(x_54, x_56); -lean_dec(x_56); -x_70 = l_Lean_FileMap_toPosition(x_54, x_57); +lean_inc_ref(x_55); +x_69 = l_Lean_FileMap_toPosition(x_55, x_53); +lean_dec(x_53); +x_70 = l_Lean_FileMap_toPosition(x_55, x_57); lean_dec(x_57); x_71 = lean_alloc_ctor(1, 1, 0); lean_ctor_set(x_71, 0, x_70); x_72 = l_Lean_addTrace___at___00__private_Lean_ExtraModUses_0__Lean_recordExtraModUseCore___at___00Lean_recordExtraModUseFromDecl___at___00Lean_Elab_Tactic_elabGrindConfig_spec__0_spec__0_spec__3___redArg___closed__1; -if (x_52 == 0) +if (x_54 == 0) { lean_dec_ref(x_50); -x_10 = x_69; -x_11 = x_51; -x_12 = x_53; -x_13 = x_72; -x_14 = x_68; -x_15 = x_55; +x_10 = x_51; +x_11 = x_72; +x_12 = x_52; +x_13 = x_69; +x_14 = x_56; +x_15 = x_68; x_16 = x_71; x_17 = x_7; x_18 = x_8; @@ -15365,7 +15727,7 @@ lean_object* x_74; lean_object* x_75; lean_dec_ref(x_71); lean_dec_ref(x_69); lean_dec(x_68); -lean_dec_ref(x_51); +lean_dec_ref(x_56); lean_dec_ref(x_7); x_74 = lean_box(0); x_75 = lean_alloc_ctor(0, 1, 0); @@ -15374,12 +15736,12 @@ return x_75; } else { -x_10 = x_69; -x_11 = x_51; -x_12 = x_53; -x_13 = x_72; -x_14 = x_68; -x_15 = x_55; +x_10 = x_51; +x_11 = x_72; +x_12 = x_52; +x_13 = x_69; +x_14 = x_56; +x_15 = x_68; x_16 = x_71; x_17 = x_7; x_18 = x_8; @@ -15392,18 +15754,18 @@ goto block_49; block_87: { lean_object* x_85; -x_85 = l_Lean_Syntax_getTailPos_x3f(x_78, x_83); -lean_dec(x_78); +x_85 = l_Lean_Syntax_getTailPos_x3f(x_83, x_78); +lean_dec(x_83); if (lean_obj_tag(x_85) == 0) { lean_inc(x_84); x_50 = x_77; -x_51 = x_79; -x_52 = x_80; -x_53 = x_81; -x_54 = x_82; -x_55 = x_83; -x_56 = x_84; +x_51 = x_78; +x_52 = x_79; +x_53 = x_84; +x_54 = x_81; +x_55 = x_80; +x_56 = x_82; x_57 = x_84; goto block_76; } @@ -15414,12 +15776,12 @@ x_86 = lean_ctor_get(x_85, 0); lean_inc(x_86); lean_dec_ref(x_85); x_50 = x_77; -x_51 = x_79; -x_52 = x_80; -x_53 = x_81; -x_54 = x_82; -x_55 = x_83; -x_56 = x_84; +x_51 = x_78; +x_52 = x_79; +x_53 = x_84; +x_54 = x_81; +x_55 = x_80; +x_56 = x_82; x_57 = x_86; goto block_76; } @@ -15429,18 +15791,18 @@ block_99: lean_object* x_95; lean_object* x_96; x_95 = l_Lean_replaceRef(x_1, x_93); lean_dec(x_93); -x_96 = l_Lean_Syntax_getPos_x3f(x_95, x_92); +x_96 = l_Lean_Syntax_getPos_x3f(x_95, x_89); if (lean_obj_tag(x_96) == 0) { lean_object* x_97; x_97 = lean_unsigned_to_nat(0u); x_77 = x_88; -x_78 = x_95; -x_79 = x_89; -x_80 = x_90; -x_81 = x_94; -x_82 = x_91; -x_83 = x_92; +x_78 = x_89; +x_79 = x_94; +x_80 = x_91; +x_81 = x_90; +x_82 = x_92; +x_83 = x_95; x_84 = x_97; goto block_87; } @@ -15451,12 +15813,12 @@ x_98 = lean_ctor_get(x_96, 0); lean_inc(x_98); lean_dec_ref(x_96); x_77 = x_88; -x_78 = x_95; -x_79 = x_89; -x_80 = x_90; -x_81 = x_94; -x_82 = x_91; -x_83 = x_92; +x_78 = x_89; +x_79 = x_94; +x_80 = x_91; +x_81 = x_90; +x_82 = x_92; +x_83 = x_95; x_84 = x_98; goto block_87; } @@ -15466,10 +15828,10 @@ block_108: if (x_107 == 0) { x_88 = x_104; -x_89 = x_101; +x_89 = x_106; x_90 = x_102; -x_91 = x_103; -x_92 = x_106; +x_91 = x_101; +x_92 = x_103; x_93 = x_105; x_94 = x_3; goto block_99; @@ -15477,10 +15839,10 @@ goto block_99; else { x_88 = x_104; -x_89 = x_101; +x_89 = x_106; x_90 = x_102; -x_91 = x_103; -x_92 = x_106; +x_91 = x_101; +x_92 = x_103; x_93 = x_105; x_94 = x_100; goto block_99; @@ -15506,11 +15868,11 @@ x_119 = l_Lean_instBEqMessageSeverity_beq(x_3, x_118); if (x_119 == 0) { lean_inc(x_113); -lean_inc_ref(x_111); lean_inc_ref(x_110); -x_101 = x_110; +lean_inc_ref(x_111); +x_101 = x_111; x_102 = x_114; -x_103 = x_111; +x_103 = x_110; x_104 = x_117; x_105 = x_113; x_106 = x_109; @@ -15523,11 +15885,11 @@ lean_object* x_120; uint8_t x_121; x_120 = l_Lean_logAt___at___00Lean_logWarningAt___at___00Lean_Elab_Tactic_evalGrindCore_spec__0_spec__0___redArg___closed__0; x_121 = l_Lean_Option_get___at___00Lean_Elab_addMacroStack___at___00Lean_throwError___at___00Lean_Elab_Tactic_elabGrindConfig_spec__1_spec__5_spec__10(x_112, x_120); lean_inc(x_113); -lean_inc_ref(x_111); lean_inc_ref(x_110); -x_101 = x_110; +lean_inc_ref(x_111); +x_101 = x_111; x_102 = x_114; -x_103 = x_111; +x_103 = x_110; x_104 = x_117; x_105 = x_113; x_106 = x_109; @@ -15856,7 +16218,7 @@ static lean_object* _init_l_Lean_Elab_Tactic_isGrindOnly___closed__0() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; -x_1 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_1 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_2 = l_Lean_Elab_Tactic_elabGrindPattern___regBuiltin_Lean_Elab_Tactic_elabGrindPattern__1___closed__2; x_3 = l_List_mapM_loop___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_elabCnstrs_spec__0___closed__0; x_4 = l_Lean_Elab_Tactic_evalUnsafe___redArg___closed__0_00___x40_Lean_Elab_Tactic_Grind_Main_2289994934____hygCtx___hyg_3_; @@ -17331,18 +17693,18 @@ if (lean_is_scalar(x_14)) { lean_ctor_set_tag(x_64, 1); } lean_ctor_set(x_64, 0, x_60); -x_20 = lean_box(0); -x_21 = x_44; -x_22 = x_49; -x_23 = x_47; -x_24 = x_53; -x_25 = x_46; +x_20 = x_64; +x_21 = x_47; +x_22 = x_45; +x_23 = x_51; +x_24 = x_46; +x_25 = x_52; x_26 = x_50; -x_27 = x_52; -x_28 = x_51; -x_29 = x_64; -x_30 = x_45; -x_31 = x_48; +x_27 = x_49; +x_28 = x_48; +x_29 = lean_box(0); +x_30 = x_53; +x_31 = x_44; x_32 = x_41; goto block_39; } @@ -17354,18 +17716,18 @@ lean_object* x_65; lean_dec(x_56); lean_dec(x_14); x_65 = lean_box(0); -x_20 = lean_box(0); -x_21 = x_44; -x_22 = x_49; -x_23 = x_47; -x_24 = x_53; -x_25 = x_46; +x_20 = x_65; +x_21 = x_47; +x_22 = x_45; +x_23 = x_51; +x_24 = x_46; +x_25 = x_52; x_26 = x_50; -x_27 = x_52; -x_28 = x_51; -x_29 = x_65; -x_30 = x_45; -x_31 = x_48; +x_27 = x_49; +x_28 = x_48; +x_29 = lean_box(0); +x_30 = x_53; +x_31 = x_44; x_32 = x_12; goto block_39; } @@ -17446,39 +17808,39 @@ goto block_66; block_39: { lean_object* x_33; -lean_inc(x_24); -lean_inc_ref(x_27); -lean_inc(x_28); +lean_inc(x_30); +lean_inc_ref(x_25); +lean_inc(x_23); lean_inc_ref(x_26); -lean_inc(x_22); -lean_inc_ref(x_31); -x_33 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindConfig_x27___redArg(x_19, x_32, x_25, x_31, x_22, x_26, x_28, x_27, x_24); +lean_inc(x_27); +lean_inc_ref(x_28); +x_33 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindConfig_x27___redArg(x_19, x_32, x_24, x_28, x_27, x_26, x_23, x_25, x_30); if (lean_obj_tag(x_33) == 0) { lean_object* x_34; lean_object* x_35; x_34 = lean_ctor_get(x_33, 0); lean_inc(x_34); lean_dec_ref(x_33); -x_35 = l_Lean_Elab_Tactic_evalGrindCore(x_1, x_34, x_21, x_30, x_29, x_25, x_23, x_31, x_22, x_26, x_28, x_27, x_24); -lean_dec(x_30); -lean_dec(x_21); +x_35 = l_Lean_Elab_Tactic_evalGrindCore(x_1, x_34, x_31, x_22, x_20, x_24, x_21, x_28, x_27, x_26, x_23, x_25, x_30); +lean_dec(x_22); +lean_dec(x_31); lean_dec(x_1); return x_35; } else { uint8_t x_36; -lean_dec_ref(x_31); +lean_dec(x_31); lean_dec(x_30); -lean_dec(x_29); -lean_dec(x_28); -lean_dec_ref(x_27); +lean_dec_ref(x_28); +lean_dec(x_27); lean_dec_ref(x_26); lean_dec_ref(x_25); -lean_dec(x_24); +lean_dec_ref(x_24); lean_dec(x_23); lean_dec(x_22); lean_dec(x_21); +lean_dec(x_20); lean_dec(x_1); x_36 = !lean_is_exclusive(x_33); if (x_36 == 0) @@ -17729,7 +18091,7 @@ _start: { lean_object* x_6; lean_object* x_7; uint8_t x_8; x_6 = l_Lean_Syntax_getArg(x_1, x_2); -x_7 = l_Lean_Elab_Tactic_elabGrindPattern___closed__10; +x_7 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; x_8 = l_Lean_Syntax_isOfKind(x_6, x_7); if (x_8 == 0) { @@ -17859,7 +18221,7 @@ lean_dec_ref(x_15); x_26 = l_Lean_Meta_Grind_Action_mkGrindSeq(x_20); x_27 = l_Lean_SourceInfo_fromRef(x_25, x_5); lean_dec(x_25); -x_28 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_28 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_29 = l_Lean_Name_mkStr4(x_6, x_7, x_8, x_28); lean_inc(x_27); x_30 = lean_alloc_ctor(2, 2, 0); @@ -17897,7 +18259,7 @@ lean_dec_ref(x_15); x_41 = l_Lean_Meta_Grind_Action_mkGrindSeq(x_20); x_42 = l_Lean_SourceInfo_fromRef(x_40, x_5); lean_dec(x_40); -x_43 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_43 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_44 = l_Lean_Name_mkStr4(x_6, x_7, x_8, x_43); lean_inc(x_42); x_45 = lean_alloc_ctor(2, 2, 0); @@ -18408,7 +18770,7 @@ lean_inc(x_30); lean_dec_ref(x_16); x_31 = l_Lean_SourceInfo_fromRef(x_30, x_29); lean_dec(x_30); -x_32 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_32 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_33 = l_Lean_Name_mkStr4(x_5, x_6, x_7, x_32); lean_inc(x_31); x_34 = lean_alloc_ctor(2, 2, 0); @@ -18465,7 +18827,7 @@ lean_inc(x_53); lean_dec_ref(x_16); x_54 = l_Lean_SourceInfo_fromRef(x_53, x_4); lean_dec(x_53); -x_55 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_55 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_56 = l_Lean_Name_mkStr4(x_5, x_6, x_7, x_55); lean_inc(x_54); x_57 = lean_alloc_ctor(2, 2, 0); @@ -18540,7 +18902,7 @@ lean_inc(x_74); lean_dec_ref(x_16); x_75 = l_Lean_SourceInfo_fromRef(x_74, x_73); lean_dec(x_74); -x_76 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_76 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_77 = l_Lean_Name_mkStr4(x_5, x_6, x_7, x_76); lean_inc(x_75); x_78 = lean_alloc_ctor(2, 2, 0); @@ -18598,7 +18960,7 @@ lean_inc(x_98); lean_dec_ref(x_16); x_99 = l_Lean_SourceInfo_fromRef(x_98, x_4); lean_dec(x_98); -x_100 = l_Lean_Elab_Tactic_mkGrindParams___closed__0; +x_100 = l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0; x_101 = l_Lean_Name_mkStr4(x_5, x_6, x_7, x_100); lean_inc(x_99); x_102 = lean_alloc_ctor(2, 2, 0); @@ -19002,7 +19364,7 @@ else lean_object* x_45; lean_object* x_46; uint8_t x_47; x_45 = l_Lean_Syntax_getArg(x_27, x_5); lean_dec(x_27); -x_46 = l_Lean_Elab_Tactic_elabGrindPattern___closed__10; +x_46 = l_Lean_Elab_Tactic_elabGrindPattern___closed__6; x_47 = l_Lean_Syntax_isOfKind(x_45, x_46); if (x_47 == 0) { @@ -19200,7 +19562,7 @@ return x_19; } else { -lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t 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; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_51; lean_object* x_52; uint8_t x_53; +lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; uint8_t x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34; lean_object* x_35; lean_object* x_36; lean_object* x_51; lean_object* x_52; uint8_t x_53; x_20 = lean_unsigned_to_nat(1u); x_21 = l_Lean_Syntax_getArg(x_2, x_20); x_51 = l_Lean_Elab_Tactic_evalGrind___closed__3; @@ -19231,7 +19593,7 @@ return x_54; } else { -lean_object* x_55; lean_object* x_56; uint8_t x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; uint8_t x_61; uint8_t x_62; lean_object* x_63; uint8_t x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; uint8_t x_80; uint8_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; uint8_t x_93; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_176; uint8_t x_177; +lean_object* x_55; lean_object* x_56; uint8_t x_57; lean_object* x_58; uint8_t x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; uint8_t x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; uint8_t x_69; lean_object* x_70; lean_object* x_71; uint8_t x_80; uint8_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; lean_object* x_90; lean_object* x_91; lean_object* x_92; uint8_t x_93; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_156; lean_object* x_157; lean_object* x_158; lean_object* x_159; lean_object* x_160; lean_object* x_161; lean_object* x_162; lean_object* x_163; lean_object* x_164; lean_object* x_165; lean_object* x_176; uint8_t x_177; x_55 = lean_unsigned_to_nat(0u); x_56 = lean_unsigned_to_nat(2u); x_176 = l_Lean_Syntax_getArg(x_2, x_56); @@ -19306,14 +19668,14 @@ x_74 = lean_nat_dec_lt(x_55, x_72); if (x_74 == 0) { x_22 = x_57; -x_23 = lean_box(0); +x_23 = x_58; x_24 = x_59; -x_25 = x_71; -x_26 = x_60; -x_27 = x_61; +x_25 = x_60; +x_26 = x_61; +x_27 = lean_box(0); x_28 = x_63; x_29 = x_64; -x_30 = x_65; +x_30 = x_71; x_31 = x_66; x_32 = x_67; x_33 = x_68; @@ -19329,14 +19691,14 @@ x_75 = lean_nat_dec_le(x_72, x_72); if (x_75 == 0) { x_22 = x_57; -x_23 = lean_box(0); +x_23 = x_58; x_24 = x_59; -x_25 = x_71; -x_26 = x_60; -x_27 = x_61; +x_25 = x_60; +x_26 = x_61; +x_27 = lean_box(0); x_28 = x_63; x_29 = x_64; -x_30 = x_65; +x_30 = x_71; x_31 = x_66; x_32 = x_67; x_33 = x_68; @@ -19353,16 +19715,16 @@ x_77 = lean_usize_of_nat(x_72); lean_inc_ref(x_5); lean_inc_ref(x_4); lean_inc_ref(x_3); -x_78 = l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___00Lean_Elab_Tactic_evalGrindTraceCore_spec__1(x_3, x_4, x_5, x_55, x_20, x_6, x_62, x_56, x_71, x_76, x_77, x_73); +x_78 = l___private_Init_Data_Array_Basic_0__Array_foldlMUnsafe_fold___at___00Lean_Elab_Tactic_evalGrindTraceCore_spec__1(x_3, x_4, x_5, x_55, x_20, x_6, x_65, x_56, x_71, x_76, x_77, x_73); x_22 = x_57; -x_23 = lean_box(0); +x_23 = x_58; x_24 = x_59; -x_25 = x_71; -x_26 = x_60; -x_27 = x_61; +x_25 = x_60; +x_26 = x_61; +x_27 = lean_box(0); x_28 = x_63; x_29 = x_64; -x_30 = x_65; +x_30 = x_71; x_31 = x_66; x_32 = x_67; x_33 = x_68; @@ -19375,50 +19737,50 @@ goto block_50; } block_97: { -if (lean_obj_tag(x_92) == 1) +if (lean_obj_tag(x_83) == 1) { lean_object* x_94; lean_object* x_95; -x_94 = lean_ctor_get(x_92, 0); +x_94 = lean_ctor_get(x_83, 0); lean_inc(x_94); -lean_dec_ref(x_92); +lean_dec_ref(x_83); x_95 = l_Lean_Syntax_TSepArray_getElems___redArg(x_94); lean_dec(x_94); x_57 = x_80; -x_58 = lean_box(0); -x_59 = x_83; +x_58 = x_82; +x_59 = x_93; x_60 = x_84; -x_61 = x_81; -x_62 = x_80; -x_63 = x_85; -x_64 = x_93; -x_65 = x_86; -x_66 = x_87; -x_67 = x_88; -x_68 = x_89; -x_69 = x_90; -x_70 = x_91; +x_61 = x_85; +x_62 = lean_box(0); +x_63 = x_87; +x_64 = x_88; +x_65 = x_80; +x_66 = x_89; +x_67 = x_90; +x_68 = x_91; +x_69 = x_81; +x_70 = x_92; x_71 = x_95; goto block_79; } else { lean_object* x_96; -lean_dec(x_92); +lean_dec(x_83); x_96 = l_Lean_Elab_Tactic_evalGrindCore___closed__4; x_57 = x_80; -x_58 = lean_box(0); -x_59 = x_83; +x_58 = x_82; +x_59 = x_93; x_60 = x_84; -x_61 = x_81; -x_62 = x_80; -x_63 = x_85; -x_64 = x_93; -x_65 = x_86; -x_66 = x_87; -x_67 = x_88; -x_68 = x_89; -x_69 = x_90; -x_70 = x_91; +x_61 = x_85; +x_62 = lean_box(0); +x_63 = x_87; +x_64 = x_88; +x_65 = x_80; +x_66 = x_89; +x_67 = x_90; +x_68 = x_91; +x_69 = x_81; +x_70 = x_92; x_71 = x_96; goto block_79; } @@ -19454,17 +19816,17 @@ if (lean_obj_tag(x_98) == 0) { x_80 = x_113; x_81 = x_112; -x_82 = lean_box(0); -x_83 = x_105; -x_84 = x_102; -x_85 = x_106; -x_86 = x_107; +x_82 = x_101; +x_83 = x_99; +x_84 = x_106; +x_85 = x_107; +x_86 = lean_box(0); x_87 = x_110; -x_88 = x_101; -x_89 = x_104; -x_90 = x_103; -x_91 = x_100; -x_92 = x_99; +x_88 = x_100; +x_89 = x_105; +x_90 = x_104; +x_91 = x_103; +x_92 = x_102; x_93 = x_113; goto block_97; } @@ -19473,17 +19835,17 @@ else lean_dec_ref(x_98); x_80 = x_113; x_81 = x_112; -x_82 = lean_box(0); -x_83 = x_105; -x_84 = x_102; -x_85 = x_106; -x_86 = x_107; +x_82 = x_101; +x_83 = x_99; +x_84 = x_106; +x_85 = x_107; +x_86 = lean_box(0); x_87 = x_110; -x_88 = x_101; -x_89 = x_104; -x_90 = x_103; -x_91 = x_100; -x_92 = x_99; +x_88 = x_100; +x_89 = x_105; +x_90 = x_104; +x_91 = x_103; +x_92 = x_102; x_93 = x_53; goto block_97; } @@ -19584,17 +19946,17 @@ if (lean_obj_tag(x_98) == 0) { x_80 = x_150; x_81 = x_142; -x_82 = lean_box(0); -x_83 = x_105; -x_84 = x_102; -x_85 = x_106; -x_86 = x_107; +x_82 = x_101; +x_83 = x_99; +x_84 = x_106; +x_85 = x_107; +x_86 = lean_box(0); x_87 = x_151; -x_88 = x_101; -x_89 = x_104; -x_90 = x_103; -x_91 = x_100; -x_92 = x_99; +x_88 = x_100; +x_89 = x_105; +x_90 = x_104; +x_91 = x_103; +x_92 = x_102; x_93 = x_150; goto block_97; } @@ -19603,17 +19965,17 @@ else lean_dec_ref(x_98); x_80 = x_150; x_81 = x_142; -x_82 = lean_box(0); -x_83 = x_105; -x_84 = x_102; -x_85 = x_106; -x_86 = x_107; +x_82 = x_101; +x_83 = x_99; +x_84 = x_106; +x_85 = x_107; +x_86 = lean_box(0); x_87 = x_151; -x_88 = x_101; -x_89 = x_104; -x_90 = x_103; -x_91 = x_100; -x_92 = x_99; +x_88 = x_100; +x_89 = x_105; +x_90 = x_104; +x_91 = x_103; +x_92 = x_102; x_93 = x_53; goto block_97; } @@ -19730,22 +20092,22 @@ goto block_155; block_50: { lean_object* x_37; -x_37 = l_Lean_Elab_Tactic_getMainGoal___redArg(x_32, x_33, x_24, x_28, x_30); +x_37 = l_Lean_Elab_Tactic_getMainGoal___redArg(x_23, x_32, x_31, x_25, x_26); if (lean_obj_tag(x_37) == 0) { lean_object* x_38; lean_object* x_39; x_38 = lean_ctor_get(x_37, 0); lean_inc(x_38); lean_dec_ref(x_37); -lean_inc(x_30); -lean_inc_ref(x_28); -lean_inc(x_24); -lean_inc_ref(x_33); -lean_inc(x_34); -lean_inc_ref(x_26); +lean_inc(x_26); +lean_inc_ref(x_25); +lean_inc(x_31); +lean_inc_ref(x_32); +lean_inc(x_33); +lean_inc_ref(x_35); lean_inc(x_38); -x_39 = l_Lean_Elab_Tactic_mkGrindParams(x_31, x_29, x_25, x_38, x_26, x_34, x_33, x_24, x_28, x_30); -lean_dec_ref(x_25); +x_39 = l_Lean_Elab_Tactic_mkGrindParams(x_28, x_24, x_30, x_38, x_35, x_33, x_32, x_31, x_25, x_26); +lean_dec_ref(x_30); if (lean_obj_tag(x_39) == 0) { lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; @@ -19762,7 +20124,7 @@ lean_closure_set(x_42, 4, x_4); lean_closure_set(x_42, 5, x_5); lean_closure_set(x_42, 6, x_40); lean_closure_set(x_42, 7, x_20); -x_43 = l_Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1___redArg(x_27, x_38, x_42, x_35, x_32, x_26, x_34, x_33, x_24, x_28, x_30); +x_43 = l_Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1___redArg(x_34, x_38, x_42, x_29, x_23, x_35, x_33, x_32, x_31, x_25, x_26); return x_43; } else @@ -19771,13 +20133,13 @@ uint8_t x_44; lean_dec(x_38); lean_dec_ref(x_36); lean_dec_ref(x_35); -lean_dec(x_34); -lean_dec_ref(x_33); -lean_dec(x_32); -lean_dec(x_30); -lean_dec_ref(x_28); -lean_dec_ref(x_26); -lean_dec(x_24); +lean_dec(x_33); +lean_dec_ref(x_32); +lean_dec(x_31); +lean_dec_ref(x_29); +lean_dec(x_26); +lean_dec_ref(x_25); +lean_dec(x_23); lean_dec(x_21); lean_dec_ref(x_5); lean_dec_ref(x_4); @@ -19804,15 +20166,15 @@ else uint8_t x_47; lean_dec_ref(x_36); lean_dec_ref(x_35); -lean_dec(x_34); -lean_dec_ref(x_33); -lean_dec(x_32); -lean_dec_ref(x_31); -lean_dec(x_30); +lean_dec(x_33); +lean_dec_ref(x_32); +lean_dec(x_31); +lean_dec_ref(x_30); +lean_dec_ref(x_29); lean_dec_ref(x_28); -lean_dec_ref(x_26); +lean_dec(x_26); lean_dec_ref(x_25); -lean_dec(x_24); +lean_dec(x_23); lean_dec(x_21); lean_dec_ref(x_5); lean_dec_ref(x_4); @@ -21203,8 +21565,14 @@ l_Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_g lean_mark_persistent(l_Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3___redArg___closed__3); l_Lean_mkUnknownIdentifierMessage___at___00Lean_throwUnknownIdentifierAt___at___00Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3_spec__4_spec__5___closed__0 = _init_l_Lean_mkUnknownIdentifierMessage___at___00Lean_throwUnknownIdentifierAt___at___00Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3_spec__4_spec__5___closed__0(); lean_mark_persistent(l_Lean_mkUnknownIdentifierMessage___at___00Lean_throwUnknownIdentifierAt___at___00Lean_throwUnknownConstantAt___at___00Lean_throwUnknownConstant___at___00Lean_getConstVal___at___00__private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go_spec__1_spec__1_spec__3_spec__4_spec__5___closed__0); -l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0 = _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0(); -lean_mark_persistent(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__0___closed__0); +l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0 = _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0(); +lean_mark_persistent(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__0); +l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__1 = _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__1(); +lean_mark_persistent(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___closed__1); +l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__0 = _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__0(); +lean_mark_persistent(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__0); +l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__1 = _init_l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__1(); +lean_mark_persistent(l___private_Lean_Elab_Tactic_Grind_Main_0__Lean_Elab_Tactic_elabGrindPattern_go___lam__1___closed__1); l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg___closed__0 = _init_l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg___closed__0(); lean_mark_persistent(l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg___closed__0); l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg___closed__1 = _init_l_Lean_Elab_throwUnsupportedSyntax___at___00Lean_Elab_Tactic_elabGrindPattern_spec__0___redArg___closed__1(); @@ -21254,6 +21622,8 @@ l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__0___closed__1 = _init_l_L lean_mark_persistent(l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__0___closed__1); l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__0___closed__2 = _init_l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__0___closed__2(); lean_mark_persistent(l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__0___closed__2); +l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0 = _init_l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0(); +lean_mark_persistent(l_Lean_Elab_Tactic_elabResetGrindAttrs___redArg___lam__1___closed__0); l_Lean_Elab_Tactic_elabResetGrindAttrs___regBuiltin_Lean_Elab_Tactic_elabResetGrindAttrs__1___closed__0 = _init_l_Lean_Elab_Tactic_elabResetGrindAttrs___regBuiltin_Lean_Elab_Tactic_elabResetGrindAttrs__1___closed__0(); lean_mark_persistent(l_Lean_Elab_Tactic_elabResetGrindAttrs___regBuiltin_Lean_Elab_Tactic_elabResetGrindAttrs__1___closed__0); l_Lean_Elab_Tactic_elabResetGrindAttrs___regBuiltin_Lean_Elab_Tactic_elabResetGrindAttrs__1___closed__1 = _init_l_Lean_Elab_Tactic_elabResetGrindAttrs___regBuiltin_Lean_Elab_Tactic_elabResetGrindAttrs__1___closed__1(); @@ -21314,8 +21684,6 @@ l_Lean_Elab_Tactic_mkGrindParams___closed__4 = _init_l_Lean_Elab_Tactic_mkGrindP lean_mark_persistent(l_Lean_Elab_Tactic_mkGrindParams___closed__4); l_Lean_Elab_Tactic_mkGrindParams___closed__5 = _init_l_Lean_Elab_Tactic_mkGrindParams___closed__5(); lean_mark_persistent(l_Lean_Elab_Tactic_mkGrindParams___closed__5); -l_Lean_Elab_Tactic_mkGrindParams___closed__6 = _init_l_Lean_Elab_Tactic_mkGrindParams___closed__6(); -lean_mark_persistent(l_Lean_Elab_Tactic_mkGrindParams___closed__6); l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4_spec__5_spec__6___redArg___closed__0 = _init_l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4_spec__5_spec__6___redArg___closed__0(); lean_mark_persistent(l_Lean_PersistentHashMap_insertAux___at___00Lean_PersistentHashMap_insert___at___00Lean_MVarId_assign___at___00__private_Lean_Meta_Tactic_Grind_Main_0__Lean_Meta_Grind_withProtectedMCtx_main___at___00Lean_Meta_Grind_withProtectedMCtx___at___00Lean_Elab_Tactic_grind_spec__1_spec__1_spec__4_spec__5_spec__6___redArg___closed__0); l_Lean_Elab_Tactic_grind___lam__1___closed__0 = _init_l_Lean_Elab_Tactic_grind___lam__1___closed__0(); diff --git a/stage0/stdlib/Lean/Meta/Tactic/Grind/Parser.c b/stage0/stdlib/Lean/Meta/Tactic/Grind/Parser.c index c8ac89bb10..fa146d2a54 100644 --- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Parser.c +++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Parser.c @@ -31,14 +31,18 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_isValue_parenthesizer_ static lean_object* l_Lean_Parser_Command_GrindCnstr_defEq_parenthesizer___closed__4; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_notDefEq_formatter__51___boxed(lean_object*); static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__10; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__25; LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_notValue; static lean_object* l_Lean_Parser_Command_grindPatternCnstrs___closed__5; lean_object* l_Lean_Parser_Term_attrKind_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__18; +static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__17; static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue_formatter___closed__5; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_notDefEq_parenthesizer__113___boxed(lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Command_initGrindNorm___regBuiltin_Lean_Parser_Command_initGrindNorm_formatter__5___boxed(lean_object*); static lean_object* l_Lean_Parser_Command_GrindCnstr_maxInsts_parenthesizer___closed__2; static lean_object* l_Lean_Parser_Command_GrindCnstr_sizeLt___closed__10; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__22; static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue___closed__12; static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue___closed__2; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -176,6 +180,7 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_check_formatter___closed__1 static lean_object* l_Lean_Parser_Command_GrindCnstr_maxInsts_parenthesizer___closed__3; static lean_object* l_Lean_Parser_Command_GrindCnstr_defEq___closed__3; static lean_object* l_Lean_Parser_Command_GrindCnstr_check_parenthesizer___closed__0; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__24; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_maxInsts_parenthesizer__101___boxed(lean_object*); static lean_object* l_Lean_Parser_Command_initGrindNorm___closed__3; static lean_object* l_Lean_Parser_Command_GrindCnstr_isGround_parenthesizer___closed__2; @@ -235,6 +240,7 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_sizeLt_parenthesizer___clos LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_guard_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_guard; static lean_object* l_Lean_Parser_Command_GrindCnstr_defEq___closed__1; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__21; lean_object* l_Lean_Parser_mkAntiquot_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__9; static lean_object* l_Lean_Parser_Command_GrindCnstr_guard_parenthesizer___closed__6; @@ -295,10 +301,12 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_genLt___closed__7; static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue___closed__1; static lean_object* l_Lean_Parser_Command_grindPatternCnstr_formatter___closed__3; static lean_object* l_Lean_Parser_Command_GrindCnstr_isGround_formatter___closed__0; +static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__13; extern lean_object* l_Lean_PrettyPrinter_parenthesizerAttribute; static lean_object* l_Lean_Parser_Command_GrindCnstr_guard___closed__4; LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_check_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Command_grindPatternCnstrs_parenthesizer___closed__4; +static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__16; static lean_object* l_Lean_Parser_Command_GrindCnstr_check___closed__2; static lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_isValue_formatter__7___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_genLt_formatter__35(); @@ -371,10 +379,12 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_depthLt_parenthesizer_ LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_check_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_many1Indent_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Parser_Command_grindPattern___closed__19; static lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_defEq_parenthesizer__117___closed__0; static lean_object* l_Lean_Parser_Command_GrindCnstr_notValue___closed__8; static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__10; static lean_object* l_Lean_Parser_Command_GrindCnstr_notDefEq_formatter___closed__0; +static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__14; static lean_object* l_Lean_Parser_Command_grindPatternCnstr___closed__4; LEAN_EXPORT lean_object* l_Lean_Parser_Command_initGrindNorm___regBuiltin_Lean_Parser_Command_initGrindNorm_parenthesizer__9(); static lean_object* l_Lean_Parser_Command_initGrindNorm___closed__4; @@ -403,6 +413,7 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_notDefEq___closed__10; static lean_object* l_Lean_Parser_Command_GrindCnstr_notStrictValue___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_guard_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_notStrictValue_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__15; static lean_object* l_Lean_Parser_Command_GrindCnstr_maxInsts___closed__3; LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_maxInsts_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Command_GrindCnstr_defEq___closed__7; @@ -419,6 +430,7 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue_parenthesizer___clo static lean_object* l_Lean_Parser_Command_grindPatternCnstr___closed__2; static lean_object* l_Lean_Parser_Command_grindPatternCnstrs_formatter___closed__3; static lean_object* l_Lean_Parser_Command_GrindCnstr_defEq___closed__8; +static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__14; static lean_object* l_Lean_Parser_Command_GrindCnstr_sizeLt_parenthesizer___closed__0; lean_object* l_Lean_Parser_checkColGe(lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_parenthesizer__127(); @@ -479,6 +491,7 @@ lean_object* l_Lean_Parser_leadingNode_formatter___boxed(lean_object*, lean_obje lean_object* l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Command_GrindCnstr_isGround_parenthesizer___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_notDefEq; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__23; static lean_object* l_Lean_Parser_Command_GrindCnstr_depthLt___closed__1; static lean_object* l_Lean_Parser_Command_GrindCnstr_isStrictValue___closed__6; static lean_object* l_Lean_Parser_Command_GrindCnstr_isStrictValue___closed__8; @@ -498,10 +511,12 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue_parenthesizer___clo static lean_object* l_Lean_Parser_Command_GrindCnstr_maxInsts___closed__7; static lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_notValue_parenthesizer__77___closed__0; static lean_object* l_Lean_Parser_Command_GrindCnstr_notDefEq___closed__0; +static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__13; static lean_object* l_Lean_Parser_Command_GrindCnstr_notValue_parenthesizer___closed__3; static lean_object* l_Lean_Parser_Command_grindPatternCnstr___closed__0; static lean_object* l_Lean_Parser_Command_GrindCnstr_sizeLt_formatter___closed__0; LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_isGround; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__26; static lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_isValue_formatter__7___closed__2; lean_object* l_Lean_Parser_ident_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_withCache(lean_object*, lean_object*); @@ -532,6 +547,7 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_isGround___closed__2; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_docString__3___boxed(lean_object*); static lean_object* l_Lean_Parser_Command_GrindCnstr_depthLt___closed__4; static lean_object* l_Lean_Parser_Command_GrindCnstr_notValue___closed__3; +static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__15; lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_Parser_Command_grindPatternCnstr_parenthesizer___closed__2; static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue___closed__3; @@ -550,6 +566,7 @@ static lean_object* l_Lean_Parser_Command_GrindCnstr_isStrictValue___closed__1; static lean_object* l_Lean_Parser_Command_GrindCnstr_depthLt___closed__3; static lean_object* l_Lean_Parser_Command_GrindCnstr_notDefEq_parenthesizer___closed__1; static lean_object* l_Lean_Parser_Command_GrindCnstr_notDefEq___closed__6; +static lean_object* l_Lean_Parser_Command_grindPattern_parenthesizer___closed__16; static lean_object* l_Lean_Parser_Command_GrindCnstr_check___closed__0; static lean_object* l_Lean_Parser_Command_GrindCnstr_sizeLt_formatter___closed__8; static lean_object* l_Lean_Parser_Command_GrindCnstr_isStrictValue___closed__7; @@ -563,6 +580,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPatternCnstr_parenthesizer__ lean_object* l_Lean_PrettyPrinter_Parenthesizer_orelse_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_notValue_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__18; static lean_object* l_Lean_Parser_Command_GrindCnstr_notValue_formatter___closed__1; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_defEq_parenthesizer__117(); static lean_object* l_Lean_Parser_Command_grindPatternCnstr_parenthesizer___closed__1; @@ -605,6 +623,7 @@ extern lean_object* l_Lean_Parser_numLit; lean_object* l_Lean_Name_mkStr1(lean_object*); extern lean_object* l_Lean_PrettyPrinter_formatterAttribute; lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l_Lean_Parser_Command_grindPattern_formatter___closed__17; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_parenthesizer__127___boxed(lean_object*); static lean_object* l_Lean_Parser_Command_GrindCnstr_isValue___closed__0; static lean_object* l_Lean_Parser_Command_GrindCnstr_isStrictValue_formatter___closed__3; @@ -625,6 +644,7 @@ LEAN_EXPORT lean_object* l_Lean_Parser_Command_GrindCnstr_depthLt_formatter(lean static lean_object* l_Lean_Parser_Command_grindPattern___closed__18; static lean_object* l_Lean_Parser_Command_grindPattern___closed__14; static lean_object* l_Lean_Parser_Command_GrindCnstr_check___closed__6; +static lean_object* l_Lean_Parser_Command_grindPattern___closed__20; LEAN_EXPORT lean_object* l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_GrindCnstr_defEq_parenthesizer__117___boxed(lean_object*); static lean_object* l_Lean_Parser_Command_GrindCnstr_genLt_parenthesizer___closed__0; static lean_object* l_Lean_Parser_Command_grindPatternCnstrs___closed__12; @@ -2532,40 +2552,103 @@ static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__6() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_darrow; +x_1 = lean_mk_string_unchecked("[", 1, 1); return x_1; } } static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__7() { _start: { +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__6; +x_2 = l_Lean_Parser_symbol(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__8() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string_unchecked("]", 1, 1); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__8; +x_2 = l_Lean_Parser_symbol(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__10() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern___closed__9; +x_2 = l_Lean_Parser_Command_GrindCnstr_isValue___closed__9; +x_3 = l_Lean_Parser_andthen(x_2, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__11() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern___closed__10; +x_2 = l_Lean_Parser_Command_grindPattern___closed__7; +x_3 = l_Lean_Parser_andthen(x_2, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__12() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__11; +x_2 = l_Lean_Parser_optional(x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__13() { +_start: +{ +lean_object* x_1; +x_1 = l_Lean_Parser_darrow; +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__14() { +_start: +{ lean_object* x_1; x_1 = lean_mk_string_unchecked(",", 1, 1); return x_1; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__8() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__15() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_grindPattern___closed__7; +x_1 = l_Lean_Parser_Command_grindPattern___closed__14; x_2 = l_Lean_Parser_symbol(x_1); return x_2; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__9() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__16() { _start: { uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_1 = 0; -x_2 = l_Lean_Parser_Command_grindPattern___closed__8; -x_3 = l_Lean_Parser_Command_grindPattern___closed__7; +x_2 = l_Lean_Parser_Command_grindPattern___closed__15; +x_3 = l_Lean_Parser_Command_grindPattern___closed__14; x_4 = l_Lean_Parser_Command_GrindCnstr_guard___closed__7; x_5 = l_Lean_Parser_sepBy1(x_4, x_3, x_2, x_1); return x_5; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__10() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__17() { _start: { lean_object* x_1; lean_object* x_2; @@ -2574,82 +2657,92 @@ x_2 = l_Lean_Parser_optional(x_1); return x_2; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__11() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__18() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__10; -x_2 = l_Lean_Parser_Command_grindPattern___closed__9; +x_1 = l_Lean_Parser_Command_grindPattern___closed__17; +x_2 = l_Lean_Parser_Command_grindPattern___closed__16; x_3 = l_Lean_Parser_andthen(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__12() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__19() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__11; -x_2 = l_Lean_Parser_Command_grindPattern___closed__6; +x_1 = l_Lean_Parser_Command_grindPattern___closed__18; +x_2 = l_Lean_Parser_Command_grindPattern___closed__13; x_3 = l_Lean_Parser_andthen(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__13() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__20() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__12; +x_1 = l_Lean_Parser_Command_grindPattern___closed__19; x_2 = l_Lean_Parser_Command_GrindCnstr_isValue___closed__9; x_3 = l_Lean_Parser_andthen(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__14() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__21() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__13; +x_1 = l_Lean_Parser_Command_grindPattern___closed__20; +x_2 = l_Lean_Parser_Command_grindPattern___closed__12; +x_3 = l_Lean_Parser_andthen(x_2, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__22() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern___closed__21; x_2 = l_Lean_Parser_Command_grindPattern___closed__5; x_3 = l_Lean_Parser_andthen(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__15() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__23() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__14; +x_1 = l_Lean_Parser_Command_grindPattern___closed__22; x_2 = l_Lean_Parser_Command_grindPattern___closed__3; x_3 = l_Lean_Parser_andthen(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__16() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__24() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_grindPattern___closed__15; +x_1 = l_Lean_Parser_Command_grindPattern___closed__23; x_2 = lean_unsigned_to_nat(1024u); x_3 = l_Lean_Parser_Command_grindPattern___closed__1; x_4 = l_Lean_Parser_leadingNode(x_3, x_2, x_1); return x_4; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__17() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__25() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__16; +x_1 = l_Lean_Parser_Command_grindPattern___closed__24; x_2 = l_Lean_Parser_Command_grindPattern___closed__2; x_3 = l_Lean_Parser_withAntiquot(x_2, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__18() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern___closed__26() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern___closed__17; +x_1 = l_Lean_Parser_Command_grindPattern___closed__25; x_2 = l_Lean_Parser_Command_grindPattern___closed__1; x_3 = l_Lean_Parser_withCache(x_2, x_1); return x_3; @@ -2659,7 +2752,7 @@ static lean_object* _init_l_Lean_Parser_Command_grindPattern() { _start: { lean_object* x_1; -x_1 = l_Lean_Parser_Command_grindPattern___closed__18; +x_1 = l_Lean_Parser_Command_grindPattern___closed__26; return x_1; } } @@ -4641,16 +4734,18 @@ return x_2; static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__3() { _start: { -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_darrow_formatter___boxed), 5, 0); -return x_1; +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__6; +x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; } } static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__4() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_grindPattern___closed__7; +x_1 = l_Lean_Parser_Command_grindPattern___closed__8; x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter___boxed), 6, 1); lean_closure_set(x_2, 0, x_1); return x_2; @@ -4659,10 +4754,62 @@ return x_2; static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__5() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__4; +x_2 = l_Lean_Parser_Command_GrindCnstr_isValue_formatter___closed__2; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); +lean_closure_set(x_3, 0, x_2); +lean_closure_set(x_3, 1, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__5; +x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__3; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); +lean_closure_set(x_3, 0, x_2); +lean_closure_set(x_3, 1, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__6; +x_2 = lean_alloc_closure((void*)(l_Lean_Parser_optional_formatter___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__8() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_darrow_formatter___boxed), 5, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__14; +x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_formatter___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__10() { +_start: +{ uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = 0; -x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__4; -x_3 = l_Lean_Parser_Command_grindPattern___closed__7; +x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__9; +x_3 = l_Lean_Parser_Command_grindPattern___closed__14; x_4 = l_Lean_Parser_Command_GrindCnstr_guard_formatter___closed__2; x_5 = lean_box(x_1); x_6 = lean_alloc_closure((void*)(l_Lean_Parser_sepBy1_formatter___boxed), 9, 4); @@ -4673,7 +4820,7 @@ lean_closure_set(x_6, 3, x_5); return x_6; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__6() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__11() { _start: { lean_object* x_1; lean_object* x_2; @@ -4683,35 +4830,35 @@ lean_closure_set(x_2, 0, x_1); return x_2; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__7() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__6; -x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__5; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__11; +x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__10; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__8() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__13() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__7; -x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__3; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__12; +x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__8; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__9() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__8; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__13; x_2 = l_Lean_Parser_Command_GrindCnstr_isValue_formatter___closed__2; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); @@ -4719,11 +4866,23 @@ lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__10() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__15() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__9; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__14; +x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__7; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); +lean_closure_set(x_3, 0, x_2); +lean_closure_set(x_3, 1, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__16() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__15; x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__2; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); @@ -4731,11 +4890,11 @@ lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__11() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__17() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__10; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__16; x_2 = l_Lean_Parser_Command_grindPattern_formatter___closed__1; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_andthen_formatter___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); @@ -4743,11 +4902,11 @@ lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__12() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_formatter___closed__18() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__11; +x_1 = l_Lean_Parser_Command_grindPattern_formatter___closed__17; x_2 = lean_unsigned_to_nat(1024u); x_3 = l_Lean_Parser_Command_grindPattern___closed__1; x_4 = lean_alloc_closure((void*)(l_Lean_Parser_leadingNode_formatter___boxed), 8, 3); @@ -4762,7 +4921,7 @@ _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; x_6 = l_Lean_Parser_Command_grindPattern_formatter___closed__0; -x_7 = l_Lean_Parser_Command_grindPattern_formatter___closed__12; +x_7 = l_Lean_Parser_Command_grindPattern_formatter___closed__18; x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x_4); return x_8; } @@ -6703,16 +6862,18 @@ return x_2; static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__3() { _start: { -lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_Lean_Parser_darrow_parenthesizer___boxed), 5, 0); -return x_1; +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__6; +x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_parenthesizer___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; } } static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__4() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Parser_Command_grindPattern___closed__7; +x_1 = l_Lean_Parser_Command_grindPattern___closed__8; x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_parenthesizer___boxed), 6, 1); lean_closure_set(x_2, 0, x_1); return x_2; @@ -6721,10 +6882,62 @@ return x_2; static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__5() { _start: { +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__4; +x_2 = l_Lean_Parser_Command_GrindCnstr_isValue_parenthesizer___closed__2; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); +lean_closure_set(x_3, 0, x_2); +lean_closure_set(x_3, 1, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__6() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__5; +x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__3; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); +lean_closure_set(x_3, 0, x_2); +lean_closure_set(x_3, 1, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__7() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__6; +x_2 = lean_alloc_closure((void*)(l_Lean_Parser_optional_parenthesizer___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__8() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Parser_darrow_parenthesizer___boxed), 5, 0); +return x_1; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__9() { +_start: +{ +lean_object* x_1; lean_object* x_2; +x_1 = l_Lean_Parser_Command_grindPattern___closed__14; +x_2 = lean_alloc_closure((void*)(l_Lean_Parser_symbol_parenthesizer___boxed), 6, 1); +lean_closure_set(x_2, 0, x_1); +return x_2; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__10() { +_start: +{ uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = 0; -x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__4; -x_3 = l_Lean_Parser_Command_grindPattern___closed__7; +x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__9; +x_3 = l_Lean_Parser_Command_grindPattern___closed__14; x_4 = l_Lean_Parser_Command_GrindCnstr_guard_parenthesizer___closed__2; x_5 = lean_box(x_1); x_6 = lean_alloc_closure((void*)(l_Lean_Parser_sepBy1_parenthesizer___boxed), 9, 4); @@ -6735,7 +6948,7 @@ lean_closure_set(x_6, 3, x_5); return x_6; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__6() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__11() { _start: { lean_object* x_1; lean_object* x_2; @@ -6745,35 +6958,35 @@ lean_closure_set(x_2, 0, x_1); return x_2; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__7() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__6; -x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__5; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__11; +x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__10; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__8() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__13() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__7; -x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__3; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12; +x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__8; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__9() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__8; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__13; x_2 = l_Lean_Parser_Command_GrindCnstr_isValue_parenthesizer___closed__2; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); @@ -6781,11 +6994,23 @@ lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__10() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__15() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__9; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__14; +x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__7; +x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); +lean_closure_set(x_3, 0, x_2); +lean_closure_set(x_3, 1, x_1); +return x_3; +} +} +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__16() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__15; x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__2; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); @@ -6793,11 +7018,11 @@ lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__11() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__17() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__10; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__16; x_2 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__1; x_3 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_andthen_parenthesizer___boxed), 7, 2); lean_closure_set(x_3, 0, x_2); @@ -6805,11 +7030,11 @@ lean_closure_set(x_3, 1, x_1); return x_3; } } -static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12() { +static lean_object* _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__18() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; -x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__11; +x_1 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__17; x_2 = lean_unsigned_to_nat(1024u); x_3 = l_Lean_Parser_Command_grindPattern___closed__1; x_4 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_leadingNode_parenthesizer___boxed), 8, 3); @@ -6824,7 +7049,7 @@ _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; x_6 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__0; -x_7 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12; +x_7 = l_Lean_Parser_Command_grindPattern_parenthesizer___closed__18; x_8 = l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(x_6, x_7, x_1, x_2, x_3, x_4); return x_8; } @@ -7743,6 +7968,22 @@ l_Lean_Parser_Command_grindPattern___closed__17 = _init_l_Lean_Parser_Command_gr lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__17); l_Lean_Parser_Command_grindPattern___closed__18 = _init_l_Lean_Parser_Command_grindPattern___closed__18(); lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__18); +l_Lean_Parser_Command_grindPattern___closed__19 = _init_l_Lean_Parser_Command_grindPattern___closed__19(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__19); +l_Lean_Parser_Command_grindPattern___closed__20 = _init_l_Lean_Parser_Command_grindPattern___closed__20(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__20); +l_Lean_Parser_Command_grindPattern___closed__21 = _init_l_Lean_Parser_Command_grindPattern___closed__21(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__21); +l_Lean_Parser_Command_grindPattern___closed__22 = _init_l_Lean_Parser_Command_grindPattern___closed__22(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__22); +l_Lean_Parser_Command_grindPattern___closed__23 = _init_l_Lean_Parser_Command_grindPattern___closed__23(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__23); +l_Lean_Parser_Command_grindPattern___closed__24 = _init_l_Lean_Parser_Command_grindPattern___closed__24(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__24); +l_Lean_Parser_Command_grindPattern___closed__25 = _init_l_Lean_Parser_Command_grindPattern___closed__25(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__25); +l_Lean_Parser_Command_grindPattern___closed__26 = _init_l_Lean_Parser_Command_grindPattern___closed__26(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern___closed__26); l_Lean_Parser_Command_grindPattern = _init_l_Lean_Parser_Command_grindPattern(); lean_mark_persistent(l_Lean_Parser_Command_grindPattern); l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern__1___closed__0 = _init_l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern__1___closed__0(); @@ -8027,6 +8268,18 @@ l_Lean_Parser_Command_grindPattern_formatter___closed__11 = _init_l_Lean_Parser_ lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__11); l_Lean_Parser_Command_grindPattern_formatter___closed__12 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__12(); lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__12); +l_Lean_Parser_Command_grindPattern_formatter___closed__13 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__13(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__13); +l_Lean_Parser_Command_grindPattern_formatter___closed__14 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__14(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__14); +l_Lean_Parser_Command_grindPattern_formatter___closed__15 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__15(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__15); +l_Lean_Parser_Command_grindPattern_formatter___closed__16 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__16(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__16); +l_Lean_Parser_Command_grindPattern_formatter___closed__17 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__17(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__17); +l_Lean_Parser_Command_grindPattern_formatter___closed__18 = _init_l_Lean_Parser_Command_grindPattern_formatter___closed__18(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_formatter___closed__18); l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_formatter__65___closed__0 = _init_l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_formatter__65___closed__0(); lean_mark_persistent(l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_formatter__65___closed__0); if (builtin) {res = l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_formatter__65(); @@ -8294,6 +8547,18 @@ l_Lean_Parser_Command_grindPattern_parenthesizer___closed__11 = _init_l_Lean_Par lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__11); l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12(); lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__12); +l_Lean_Parser_Command_grindPattern_parenthesizer___closed__13 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__13(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__13); +l_Lean_Parser_Command_grindPattern_parenthesizer___closed__14 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__14(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__14); +l_Lean_Parser_Command_grindPattern_parenthesizer___closed__15 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__15(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__15); +l_Lean_Parser_Command_grindPattern_parenthesizer___closed__16 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__16(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__16); +l_Lean_Parser_Command_grindPattern_parenthesizer___closed__17 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__17(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__17); +l_Lean_Parser_Command_grindPattern_parenthesizer___closed__18 = _init_l_Lean_Parser_Command_grindPattern_parenthesizer___closed__18(); +lean_mark_persistent(l_Lean_Parser_Command_grindPattern_parenthesizer___closed__18); l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_parenthesizer__127___closed__0 = _init_l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_parenthesizer__127___closed__0(); lean_mark_persistent(l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_parenthesizer__127___closed__0); if (builtin) {res = l_Lean_Parser_Command_grindPattern___regBuiltin_Lean_Parser_Command_grindPattern_parenthesizer__127();