From 35d25dfaafa2fbd136eb7c0f03c4247df744f6ad Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Jan 2022 17:18:49 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Lean/Elab/Match.lean | 2 +- stage0/src/Lean/Elab/PatternVar.lean | 2 +- stage0/src/Lean/Meta/Match/Basic.lean | 4 +- .../PrettyPrinter/Delaborator/Builtins.lean | 10 + stage0/stdlib/Lean/Elab/Match.c | 2 +- stage0/stdlib/Lean/Elab/PatternVar.c | 91 +++-- stage0/stdlib/Lean/Meta/Match/Basic.c | 2 +- .../Lean/PrettyPrinter/Delaborator/Builtins.c | 367 +++++++++++++++++- 8 files changed, 421 insertions(+), 59 deletions(-) diff --git a/stage0/src/Lean/Elab/Match.lean b/stage0/src/Lean/Elab/Match.lean index ca0fd3b86a..6a3a98cd4a 100644 --- a/stage0/src/Lean/Elab/Match.lean +++ b/stage0/src/Lean/Elab/Match.lean @@ -494,7 +494,7 @@ partial def main (e : Expr) : M Pattern := do return Pattern.arrayLit α (← lits.mapM main) | none => -- TODO: namedPattern will have 4 arguments - if e.isAppOfArity ``_root_.namedPattern 3 then + if e.isAppOfArity ``_root_.namedPatternOld 3 then let p ← main <| e.getArg! 2 match e.getArg! 1 with | Expr.fvar fvarId _ => return Pattern.as fvarId p diff --git a/stage0/src/Lean/Elab/PatternVar.lean b/stage0/src/Lean/Elab/PatternVar.lean index 5201014f28..3f6dfa888c 100644 --- a/stage0/src/Lean/Elab/PatternVar.lean +++ b/stage0/src/Lean/Elab/PatternVar.lean @@ -210,7 +210,7 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc discard <| processVar id let pat := stx[3] let pat ← collect pat - `(_root_.namedPattern $id $pat) + ``(_root_.namedPatternOld $id $pat) else if k == ``Lean.Parser.Term.binop then let lhs ← collect stx[2] let rhs ← collect stx[3] diff --git a/stage0/src/Lean/Meta/Match/Basic.lean b/stage0/src/Lean/Meta/Match/Basic.lean index 31ac648dd3..49e82e8f21 100644 --- a/stage0/src/Lean/Meta/Match/Basic.lean +++ b/stage0/src/Lean/Meta/Match/Basic.lean @@ -45,7 +45,7 @@ where | as fvarId p => -- TODO if annotate then - mkAppM `namedPattern #[mkFVar fvarId, (← visit p)] + mkAppM ``namedPatternOld #[mkFVar fvarId, (← visit p)] else visit p | arrayLit type xs => @@ -278,7 +278,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do return Pattern.arrayLit α (← lits.mapM toPattern) | none => -- TODO: `namedPattern` will have 4 arguments - if e.isAppOfArity ``namedPattern 3 then + if e.isAppOfArity ``namedPatternOld 3 then let p ← toPattern <| e.getArg! 2 match e.getArg! 1 with | Expr.fvar fvarId _ => return Pattern.as fvarId p diff --git a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index fa4a258d10..83325fdc9e 100644 --- a/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -685,6 +685,16 @@ where | none => withBindingBodyUnusedName fun h => do return (← delab, h.getId) +@[builtinDelab app.namedPatternOld] +def delabNamedPatternOld : Delab := do + -- Note: we keep this as a delaborator because it accesses the DelabM context + guard (← read).inPattern + guard $ (← getExpr).getAppNumArgs == 3 + let x ← withAppFn $ withAppArg delab + let p ← withAppArg delab + guard x.isIdent + `($x:ident@$p:term) + @[builtinDelab app.namedPattern] def delabNamedPattern : Delab := do -- Note: we keep this as a delaborator because it accesses the DelabM context diff --git a/stage0/stdlib/Lean/Elab/Match.c b/stage0/stdlib/Lean/Elab/Match.c index 9301f87282..def3d0fb53 100644 --- a/stage0/stdlib/Lean/Elab/Match.c +++ b/stage0/stdlib/Lean/Elab/Match.c @@ -16346,7 +16346,7 @@ static lean_object* _init_l_Lean_Elab_Term_ToDepElimPattern_main___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("namedPattern"); +x_1 = lean_mk_string("namedPatternOld"); return x_1; } } diff --git a/stage0/stdlib/Lean/Elab/PatternVar.c b/stage0/stdlib/Lean/Elab/PatternVar.c index 3c2aecb01f..ae874babbb 100644 --- a/stage0/stdlib/Lean/Elab/PatternVar.c +++ b/stage0/stdlib/Lean/Elab/PatternVar.c @@ -275,6 +275,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___lambda__4 lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_nameToPattern___closed__12; static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__16; +static lean_object* l_Lean_Elab_Term_CollectPatternVars_collect___closed__24; size_t lean_usize_of_nat(lean_object*); extern lean_object* l_Lean_NameSet_empty; lean_object* l_Lean_ConstantInfo_type(lean_object*); @@ -6323,7 +6324,7 @@ static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___lambda__ _start: { lean_object* x_1; -x_1 = lean_mk_string("_root_.namedPattern"); +x_1 = lean_mk_string("_root_.namedPatternOld"); return x_1; } } @@ -6372,7 +6373,7 @@ static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___lambda__ _start: { lean_object* x_1; -x_1 = lean_mk_string("namedPattern"); +x_1 = lean_mk_string("namedPatternOld"); return x_1; } } @@ -7020,14 +7021,22 @@ return x_3; static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__9() { _start: { +lean_object* x_1; +x_1 = lean_mk_string("namedPattern"); +return x_1; +} +} +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__10() { +_start: +{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8; -x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___lambda__3___closed__6; +x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__9; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__10() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__11() { _start: { lean_object* x_1; @@ -7035,17 +7044,17 @@ x_1 = lean_mk_string("binop"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__11() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__12() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8; -x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__10; +x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__11; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__12() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__13() { _start: { lean_object* x_1; @@ -7053,17 +7062,17 @@ x_1 = lean_mk_string("inaccessible"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__13() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__14() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8; -x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__12; +x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__13; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__14() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__15() { _start: { lean_object* x_1; @@ -7071,17 +7080,17 @@ x_1 = lean_mk_string("quotedName"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__15() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__16() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8; -x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__14; +x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__15; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__16() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__17() { _start: { lean_object* x_1; @@ -7089,17 +7098,17 @@ x_1 = lean_mk_string("doubleQuotedName"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__17() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__18() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8; -x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__16; +x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__17; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__18() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__19() { _start: { lean_object* x_1; @@ -7107,16 +7116,16 @@ x_1 = lean_mk_string("invalid pattern, notation is ambiguous"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__19() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__20() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__18; +x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__19; x_2 = l_Lean_stringToMessageData(x_1); return x_2; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__20() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__21() { _start: { lean_object* x_1; @@ -7124,17 +7133,17 @@ x_1 = lean_mk_string("typeAscription"); return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__21() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__22() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___closed__8; -x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__20; +x_2 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__21; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__22() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__23() { _start: { lean_object* x_1; @@ -7142,11 +7151,11 @@ x_1 = lean_mk_string("invalid struct instance pattern, 'with' is not allowed in return x_1; } } -static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__23() { +static lean_object* _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__24() { _start: { lean_object* x_1; lean_object* x_2; -x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__22; +x_1 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__23; x_2 = l_Lean_stringToMessageData(x_1); return x_2; } @@ -7200,17 +7209,17 @@ x_27 = lean_name_eq(x_10, x_26); if (x_27 == 0) { lean_object* x_28; uint8_t x_29; -x_28 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__9; +x_28 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__10; x_29 = lean_name_eq(x_10, x_28); if (x_29 == 0) { lean_object* x_30; uint8_t x_31; -x_30 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__11; +x_30 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__12; x_31 = lean_name_eq(x_10, x_30); if (x_31 == 0) { lean_object* x_32; uint8_t x_33; -x_32 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__13; +x_32 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__14; x_33 = lean_name_eq(x_10, x_32); if (x_33 == 0) { @@ -7235,12 +7244,12 @@ x_41 = lean_name_eq(x_10, x_40); if (x_41 == 0) { lean_object* x_42; uint8_t x_43; -x_42 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__15; +x_42 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__16; x_43 = lean_name_eq(x_10, x_42); if (x_43 == 0) { lean_object* x_44; uint8_t x_45; -x_44 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__17; +x_44 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__18; x_45 = lean_name_eq(x_10, x_44); if (x_45 == 0) { @@ -7260,7 +7269,7 @@ return x_49; else { lean_object* x_50; lean_object* x_51; lean_object* x_52; -x_50 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__19; +x_50 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__20; x_51 = lean_alloc_closure((void*)(l_Lean_throwError___at___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___spec__1___boxed), 9, 2); lean_closure_set(x_51, 0, x_50); lean_closure_set(x_51, 1, x_2); @@ -7408,7 +7417,7 @@ lean_object* x_86; lean_object* x_87; lean_object* x_88; uint8_t x_89; x_86 = l_Lean_Syntax_getArg(x_84, x_82); lean_dec(x_84); x_87 = l_Lean_Syntax_getKind(x_86); -x_88 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__21; +x_88 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__22; x_89 = lean_name_eq(x_87, x_88); lean_dec(x_87); if (x_89 == 0) @@ -7484,7 +7493,7 @@ if (x_103 == 0) { lean_object* x_104; lean_object* x_105; lean_object* x_106; lean_dec(x_1); -x_104 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__23; +x_104 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__24; x_105 = lean_alloc_closure((void*)(l_Lean_Elab_Term_CollectPatternVars_collect___lambda__7___boxed), 11, 4); lean_closure_set(x_105, 0, x_101); lean_closure_set(x_105, 1, x_104); @@ -7610,17 +7619,17 @@ x_140 = lean_name_eq(x_10, x_139); if (x_140 == 0) { lean_object* x_141; uint8_t x_142; -x_141 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__9; +x_141 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__10; x_142 = lean_name_eq(x_10, x_141); if (x_142 == 0) { lean_object* x_143; uint8_t x_144; -x_143 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__11; +x_143 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__12; x_144 = lean_name_eq(x_10, x_143); if (x_144 == 0) { lean_object* x_145; uint8_t x_146; -x_145 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__13; +x_145 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__14; x_146 = lean_name_eq(x_10, x_145); if (x_146 == 0) { @@ -7645,12 +7654,12 @@ x_154 = lean_name_eq(x_10, x_153); if (x_154 == 0) { lean_object* x_155; uint8_t x_156; -x_155 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__15; +x_155 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__16; x_156 = lean_name_eq(x_10, x_155); if (x_156 == 0) { lean_object* x_157; uint8_t x_158; -x_157 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__17; +x_157 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__18; x_158 = lean_name_eq(x_10, x_157); if (x_158 == 0) { @@ -7670,7 +7679,7 @@ return x_162; else { lean_object* x_163; lean_object* x_164; lean_object* x_165; -x_163 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__19; +x_163 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__20; x_164 = lean_alloc_closure((void*)(l_Lean_throwError___at___private_Lean_Elab_PatternVar_0__Lean_Elab_Term_CollectPatternVars_finalize___spec__1___boxed), 9, 2); lean_closure_set(x_164, 0, x_163); lean_closure_set(x_164, 1, x_2); @@ -7818,7 +7827,7 @@ lean_object* x_199; lean_object* x_200; lean_object* x_201; uint8_t x_202; x_199 = l_Lean_Syntax_getArg(x_197, x_195); lean_dec(x_197); x_200 = l_Lean_Syntax_getKind(x_199); -x_201 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__21; +x_201 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__22; x_202 = lean_name_eq(x_200, x_201); lean_dec(x_200); if (x_202 == 0) @@ -7894,7 +7903,7 @@ if (x_216 == 0) { lean_object* x_217; lean_object* x_218; lean_object* x_219; lean_dec(x_1); -x_217 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__23; +x_217 = l_Lean_Elab_Term_CollectPatternVars_collect___closed__24; x_218 = lean_alloc_closure((void*)(l_Lean_Elab_Term_CollectPatternVars_collect___lambda__7___boxed), 11, 4); lean_closure_set(x_218, 0, x_214); lean_closure_set(x_218, 1, x_217); @@ -10991,6 +11000,8 @@ l_Lean_Elab_Term_CollectPatternVars_collect___closed__22 = _init_l_Lean_Elab_Ter lean_mark_persistent(l_Lean_Elab_Term_CollectPatternVars_collect___closed__22); l_Lean_Elab_Term_CollectPatternVars_collect___closed__23 = _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__23(); lean_mark_persistent(l_Lean_Elab_Term_CollectPatternVars_collect___closed__23); +l_Lean_Elab_Term_CollectPatternVars_collect___closed__24 = _init_l_Lean_Elab_Term_CollectPatternVars_collect___closed__24(); +lean_mark_persistent(l_Lean_Elab_Term_CollectPatternVars_collect___closed__24); l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__1 = _init_l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__1(); lean_mark_persistent(l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__1); l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__2 = _init_l_Lean_addTrace___at_Lean_Elab_Term_CollectPatternVars_main___spec__1___closed__2(); diff --git a/stage0/stdlib/Lean/Meta/Match/Basic.c b/stage0/stdlib/Lean/Meta/Match/Basic.c index 4d72533e0d..f57e026908 100644 --- a/stage0/stdlib/Lean/Meta/Match/Basic.c +++ b/stage0/stdlib/Lean/Meta/Match/Basic.c @@ -1154,7 +1154,7 @@ static lean_object* _init_l_Lean_Meta_Match_Pattern_toExpr_visit___closed__1() { _start: { lean_object* x_1; -x_1 = lean_mk_string("namedPattern"); +x_1 = lean_mk_string("namedPatternOld"); return x_1; } } diff --git a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c index cc9df7f0b7..13cb9f16cd 100644 --- a/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c +++ b/stage0/stdlib/Lean/PrettyPrinter/Delaborator/Builtins.c @@ -190,6 +190,7 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_withMDataOptions(lean_ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__8; LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLit(lean_object*); +LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object*); uint8_t lean_name_eq(lean_object*, lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte___lambda__1___closed__4; lean_object* lean_private_to_user_name(lean_object*); @@ -270,7 +271,6 @@ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__1___ lean_object* l_Lean_Expr_appArg_x21(lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabDo___lambda__1___closed__4; LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__2___lambda__1(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_PrettyPrinter_Delaborator_delabNamedPattern___closed__2; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabConst___spec__1(size_t, size_t, lean_object*); LEAN_EXPORT uint8_t l_Array_anyMUnsafe_any___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__6(lean_object*, lean_object*, size_t, size_t); LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__4(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -296,7 +296,6 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_reifyName___closed__4; static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLam___closed__1; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__7(lean_object*, lean_object*, size_t, size_t, lean_object*); static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabPSigma___closed__3; -static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1; LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__12(lean_object*); static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppImplicit___closed__1; LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_nextExtraPos___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -588,6 +587,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___c extern lean_object* l_Lean_instInhabitedSyntax; uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_getUnusedName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5; LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_unexpandStructureInstance___spec__5(lean_object*, lean_object*, size_t, size_t, lean_object*); uint8_t l_Lean_isLetFun(lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSigmaCore___lambda__1___closed__10; @@ -597,6 +597,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMData___closed__3; static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__4; LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall(lean_object*); lean_object* l_Lean_mkSepArray(lean_object*, lean_object*); +static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__2___closed__2; LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabSort(lean_object*); LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_SubExpr_withBindingBody___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_skippingBinders_loop_visitLambda___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -604,6 +605,7 @@ LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOp static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabForall___closed__1; lean_object* l_Lean_Expr_consumeMData(lean_object*); lean_object* l_Lean_PrettyPrinter_Delaborator_returnsPi___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3; extern lean_object* l_Lean_Meta_instMonadMetaM; LEAN_EXPORT lean_object* l_panic___at_Lean_PrettyPrinter_Delaborator_withMDataOptions___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*); @@ -644,6 +646,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar lean_object* l_Lean_PrettyPrinter_Delaborator_withBindingBodyUnusedName___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_PrettyPrinter_Delaborator_delabAppMatch___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__7; +static lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1; static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabLam___closed__3; LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabSigma(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__8; @@ -711,6 +714,7 @@ LEAN_EXPORT uint8_t l_Lean_PrettyPrinter_Delaborator_hasIdent(lean_object*, lean LEAN_EXPORT lean_object* l_Array_mapIdxM_map___at___private_Lean_PrettyPrinter_Delaborator_Builtins_0__Lean_PrettyPrinter_Delaborator_delabPatterns___spec__5___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* l_Lean_Expr_getAppNumArgsAux(lean_object*, lean_object*); static lean_object* l_Array_foldrMUnsafe_fold___at_Lean_PrettyPrinter_Delaborator_delabForall___spec__1___closed__1; +LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSigmaCore___lambda__1___closed__7; LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_withMDatasOptions(lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabMVar___closed__2; @@ -747,6 +751,7 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabOfNat___c static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__9; uint8_t lean_nat_dec_le(lean_object*, lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13; +static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4; LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppImplicit___lambda__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* l_Lean_mkApp(lean_object*, lean_object*); LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -766,6 +771,7 @@ static lean_object* l_Lean_PrettyPrinter_Delaborator_delabAppMatch___lambda__6__ LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabDIte_delabBranch___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkStr___closed__2; static lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__1___closed__4; +static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1; static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun___lambda__1___closed__4; uint8_t l_Lean_BinderInfo_isExplicit(uint8_t); lean_object* l_Lean_Syntax_getKind(lean_object*); @@ -800,6 +806,7 @@ static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNameMkNum LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetFun(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_getPPMotivesAll(lean_object*); LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabLit(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +static lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; lean_object* l_Lean_getPPMatch___boxed(lean_object*); static lean_object* l_Lean_PrettyPrinter_Delaborator_delabLetE___closed__2; static lean_object* l_Lean_PrettyPrinter_Delaborator_delabOfScientific___lambda__1___closed__2; @@ -27791,7 +27798,7 @@ x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1); return x_6; } } -static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1() { +static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1() { _start: { lean_object* x_1; @@ -27799,16 +27806,337 @@ x_1 = lean_mk_string("namedPattern"); return x_1; } } -static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2() { +static lean_object* _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__7; -x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1; +x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } +LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(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_ctor_get_uint8(x_1, sizeof(void*)*5); +if (x_8 == 0) +{ +lean_object* x_75; uint8_t x_76; +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_75 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_7); +x_76 = !lean_is_exclusive(x_75); +if (x_76 == 0) +{ +return x_75; +} +else +{ +lean_object* x_77; lean_object* x_78; lean_object* x_79; +x_77 = lean_ctor_get(x_75, 0); +x_78 = lean_ctor_get(x_75, 1); +lean_inc(x_78); +lean_inc(x_77); +lean_dec(x_75); +x_79 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_79, 0, x_77); +lean_ctor_set(x_79, 1, x_78); +return x_79; +} +} +else +{ +x_9 = x_7; +goto block_74; +} +block_74: +{ +lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; +x_10 = l_Lean_PrettyPrinter_Delaborator_SubExpr_getExpr___at_Lean_PrettyPrinter_Delaborator_getExprKind___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_9); +x_11 = lean_ctor_get(x_10, 0); +lean_inc(x_11); +x_12 = lean_ctor_get(x_10, 1); +lean_inc(x_12); +lean_dec(x_10); +x_13 = lean_unsigned_to_nat(0u); +x_14 = l_Lean_Expr_getAppNumArgsAux(x_11, x_13); +lean_dec(x_11); +x_15 = lean_unsigned_to_nat(3u); +x_16 = lean_nat_dec_eq(x_14, x_15); +lean_dec(x_14); +if (x_16 == 0) +{ +lean_object* x_69; uint8_t x_70; +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_69 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_12); +x_70 = !lean_is_exclusive(x_69); +if (x_70 == 0) +{ +return x_69; +} +else +{ +lean_object* x_71; lean_object* x_72; lean_object* x_73; +x_71 = lean_ctor_get(x_69, 0); +x_72 = lean_ctor_get(x_69, 1); +lean_inc(x_72); +lean_inc(x_71); +lean_dec(x_69); +x_73 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_73, 0, x_71); +lean_ctor_set(x_73, 1, x_72); +return x_73; +} +} +else +{ +x_17 = x_12; +goto block_68; +} +block_68: +{ +lean_object* x_18; lean_object* x_19; +x_18 = l_Lean_PrettyPrinter_Delaborator_delabMData___closed__1; +lean_inc(x_6); +lean_inc(x_5); +lean_inc(x_4); +lean_inc(x_3); +lean_inc(x_2); +lean_inc(x_1); +x_19 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppFn___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__4(x_18, x_1, x_2, x_3, x_4, x_5, x_6, x_17); +if (lean_obj_tag(x_19) == 0) +{ +lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; +x_20 = lean_ctor_get(x_19, 0); +lean_inc(x_20); +x_21 = lean_ctor_get(x_19, 1); +lean_inc(x_21); +lean_dec(x_19); +x_22 = l_Lean_PrettyPrinter_Delaborator_delabAppExplicit___lambda__4___closed__2; +lean_inc(x_6); +lean_inc(x_5); +x_23 = l_Lean_PrettyPrinter_Delaborator_SubExpr_withAppArg___at_Lean_PrettyPrinter_Delaborator_delabLetFun___spec__1(x_22, x_1, x_2, x_3, x_4, x_5, x_6, x_21); +if (lean_obj_tag(x_23) == 0) +{ +lean_object* x_24; lean_object* x_25; uint8_t x_26; +x_24 = lean_ctor_get(x_23, 0); +lean_inc(x_24); +x_25 = lean_ctor_get(x_23, 1); +lean_inc(x_25); +lean_dec(x_23); +x_26 = l_Lean_Syntax_isIdent(x_20); +if (x_26 == 0) +{ +lean_object* x_27; uint8_t x_28; +lean_dec(x_24); +lean_dec(x_20); +lean_dec(x_6); +lean_dec(x_5); +x_27 = l_Lean_PrettyPrinter_Delaborator_failure___rarg(x_25); +x_28 = !lean_is_exclusive(x_27); +if (x_28 == 0) +{ +return x_27; +} +else +{ +lean_object* x_29; lean_object* x_30; lean_object* x_31; +x_29 = lean_ctor_get(x_27, 0); +x_30 = lean_ctor_get(x_27, 1); +lean_inc(x_30); +lean_inc(x_29); +lean_dec(x_27); +x_31 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_31, 0, x_29); +lean_ctor_set(x_31, 1, x_30); +return x_31; +} +} +else +{ +lean_object* x_32; uint8_t x_33; +x_32 = l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_PrettyPrinter_Delaborator_delab___spec__3___rarg(x_5, x_6, x_25); +lean_dec(x_6); +x_33 = !lean_is_exclusive(x_32); +if (x_33 == 0) +{ +lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; +x_34 = lean_ctor_get(x_32, 0); +x_35 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__10; +x_36 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_36, 0, x_34); +lean_ctor_set(x_36, 1, x_35); +x_37 = l_Lean_PrettyPrinter_Delaborator_delabConst___closed__14; +x_38 = lean_array_push(x_37, x_20); +x_39 = lean_array_push(x_38, x_36); +x_40 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13; +x_41 = lean_array_push(x_39, x_40); +x_42 = lean_array_push(x_41, x_24); +x_43 = lean_box(2); +x_44 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; +x_45 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_45, 0, x_43); +lean_ctor_set(x_45, 1, x_44); +lean_ctor_set(x_45, 2, x_42); +lean_ctor_set(x_32, 0, x_45); +return x_32; +} +else +{ +lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; +x_46 = lean_ctor_get(x_32, 0); +x_47 = lean_ctor_get(x_32, 1); +lean_inc(x_47); +lean_inc(x_46); +lean_dec(x_32); +x_48 = l_Lean_PrettyPrinter_Delaborator_maybeAddBlockImplicit___closed__10; +x_49 = lean_alloc_ctor(2, 2, 0); +lean_ctor_set(x_49, 0, x_46); +lean_ctor_set(x_49, 1, x_48); +x_50 = l_Lean_PrettyPrinter_Delaborator_delabConst___closed__14; +x_51 = lean_array_push(x_50, x_20); +x_52 = lean_array_push(x_51, x_49); +x_53 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13; +x_54 = lean_array_push(x_52, x_53); +x_55 = lean_array_push(x_54, x_24); +x_56 = lean_box(2); +x_57 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; +x_58 = lean_alloc_ctor(1, 3, 0); +lean_ctor_set(x_58, 0, x_56); +lean_ctor_set(x_58, 1, x_57); +lean_ctor_set(x_58, 2, x_55); +x_59 = lean_alloc_ctor(0, 2, 0); +lean_ctor_set(x_59, 0, x_58); +lean_ctor_set(x_59, 1, x_47); +return x_59; +} +} +} +else +{ +uint8_t x_60; +lean_dec(x_20); +lean_dec(x_6); +lean_dec(x_5); +x_60 = !lean_is_exclusive(x_23); +if (x_60 == 0) +{ +return x_23; +} +else +{ +lean_object* x_61; lean_object* x_62; lean_object* x_63; +x_61 = lean_ctor_get(x_23, 0); +x_62 = lean_ctor_get(x_23, 1); +lean_inc(x_62); +lean_inc(x_61); +lean_dec(x_23); +x_63 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_63, 0, x_61); +lean_ctor_set(x_63, 1, x_62); +return x_63; +} +} +} +else +{ +uint8_t x_64; +lean_dec(x_6); +lean_dec(x_5); +lean_dec(x_4); +lean_dec(x_3); +lean_dec(x_2); +lean_dec(x_1); +x_64 = !lean_is_exclusive(x_19); +if (x_64 == 0) +{ +return x_19; +} +else +{ +lean_object* x_65; lean_object* x_66; lean_object* x_67; +x_65 = lean_ctor_get(x_19, 0); +x_66 = lean_ctor_get(x_19, 1); +lean_inc(x_66); +lean_inc(x_65); +lean_dec(x_19); +x_67 = lean_alloc_ctor(1, 2, 0); +lean_ctor_set(x_67, 0, x_65); +lean_ctor_set(x_67, 1, x_66); +return x_67; +} +} +} +} +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("namedPatternOld"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__2; +x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("delabNamedPatternOld"); +return x_1; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__6; +x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +static lean_object* _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld), 7, 0); +return x_1; +} +} +LEAN_EXPORT lean_object* l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; +x_2 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabFVar___closed__9; +x_3 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; +x_4 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4; +x_5 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5; +x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1); +return x_6; +} +} LEAN_EXPORT lean_object* l_Lean_PrettyPrinter_Delaborator_delabNamedPattern(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: { @@ -27977,7 +28305,7 @@ x_40 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13; x_41 = lean_array_push(x_39, x_40); x_42 = lean_array_push(x_41, x_24); x_43 = lean_box(2); -x_44 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2; +x_44 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; x_45 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_45, 0, x_43); lean_ctor_set(x_45, 1, x_44); @@ -28004,7 +28332,7 @@ x_53 = l_Lean_PrettyPrinter_Delaborator_delabSort___closed__13; x_54 = lean_array_push(x_52, x_53); x_55 = lean_array_push(x_54, x_24); x_56 = lean_box(2); -x_57 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2; +x_57 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2; x_58 = lean_alloc_ctor(1, 3, 0); lean_ctor_set(x_58, 0, x_56); lean_ctor_set(x_58, 1, x_57); @@ -28079,7 +28407,7 @@ _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabAppExplicit___closed__2; -x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1; +x_2 = l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } @@ -29808,7 +30136,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__1; x_2 = l_Lean_PrettyPrinter_Delaborator_delabDoElems___closed__5; -x_3 = lean_unsigned_to_nat(736u); +x_3 = lean_unsigned_to_nat(746u); x_4 = lean_unsigned_to_nat(40u); x_5 = l_Lean_PrettyPrinter_Delaborator_delabFVar___closed__3; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5); @@ -32239,10 +32567,23 @@ lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte___c res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabDIte(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); -l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1(); -lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1); -l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2(); -lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2); +l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1(); +lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1); +l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2 = _init_l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2(); +lean_mark_persistent(l_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__1); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__2); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__3); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__4); +l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5(); +lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld___closed__5); +res = l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPatternOld(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1(); lean_mark_persistent(l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__1); l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2 = _init_l___regBuiltin_Lean_PrettyPrinter_Delaborator_delabNamedPattern___closed__2();