max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-17 17:44:25 -08:00
parent d16a979931
commit ea45c6a9c5
6 changed files with 7656 additions and 8778 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Init/Lean/Elab/Quotation.lean
View file

@ -393,10 +393,6 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
fn ← toPreterm $ args.get! 0;
as ← (args.get! 1).getArgs.mapM toPreterm;
pure $ mkAppN fn as
| `Lean.Parser.Term.appCore => do
fn ← toPreterm $ args.get! 1;
as ← (args.get! 2).getArgs.mapM toPreterm;
pure $ mkAppN fn as
| `Lean.Parser.Term.if => do
let con := args.get! 2;
let yes := args.get! 4;

7
stage0/src/Init/Lean/Elab/TermApp.lean
View file

@ -402,13 +402,6 @@ fun stx expectedType? => do
(f, namedArgs, args) ← expandApp stx;
elabAppAux stx f namedArgs args expectedType?
@[builtinTermElab appCore] def elabAppCore : TermElab :=
fun stx expectedType? =>
let f := stx.getArg 1;
let args := (stx.getArg 2).getArgs;
let args := args.map Arg.stx;
elabAppAux stx f #[] args expectedType?
def elabAtom : TermElab :=
fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?

4
stage0/src/Init/Lean/Parser/Term.lean
View file

@ -114,10 +114,6 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! pushLeading >> many1 (namedArgument <|> termParser appPrec)
-- Auxiliary notation used for fixing bootstrapping issues
@[builtinTermParser] def appCore := parser! "_app_ " >> termParser appPrec >> many1 (termParser appPrec)
def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Term.type || leading.isOfKind `Lean.Parser.Term.sort)
@[builtinTermParser] def sortApp := tparser! checkIsSort >> pushLeading >> levelParser appPrec
@[builtinTermParser] def proj := tparser! pushLeading >> symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident)

15878
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

File diff suppressed because it is too large Load diff

107
stage0/stdlib/Init/Lean/Elab/TermApp.c
View file

@ -36,13 +36,11 @@ lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_
lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_TermApp_14__elabAppFn___main___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkFreshExprMVar(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__3;
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_Elab_Term_elabExplicitUniv___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_fieldIdxKind___closed__2;
extern lean_object* l_Lean_MessageData_ofList___closed__3;
lean_object* l_Array_eraseIdx___rarg(lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_TermApp_17__mergeFailures___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabAppCore(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_inferType(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__24;
lean_object* l___private_Init_Lean_Elab_TermApp_11__addLValArg___main___closed__8;
@ -178,7 +176,6 @@ lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__12;
lean_object* l_Lean_Elab_Term_elabAtom(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getStructureFields(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSortApp___closed__1;
lean_object* l___private_Init_Lean_Elab_TermApp_12__elabAppLValsAux___main(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addNamedArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -218,7 +215,6 @@ lean_object* l___private_Init_Lean_Elab_TermApp_4__elabAppArgsAux(lean_object*,
lean_object* l_Lean_Elab_Term_mkConst(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabProj(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_ofArray(lean_object*);
extern lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_TermApp_6__throwLValError___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabExplicit___closed__2;
lean_object* l___private_Init_Lean_Elab_TermApp_11__addLValArg___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -309,7 +305,6 @@ lean_object* l___private_Init_Lean_Elab_TermApp_17__mergeFailures___rarg___close
lean_object* l___private_Init_Lean_Elab_TermApp_17__mergeFailures___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_11__addLValArg___main___closed__9;
lean_object* l___private_Init_Lean_Elab_TermApp_10__mkBaseProjections___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_elabAppCore___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_tryEnsureHasType_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addNamedArg___closed__2;
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__5;
@ -329,7 +324,6 @@ uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Elab_Term_applyResult(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
uint8_t l_Lean_isStructureLike(lean_object*, lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__1;
lean_object* l_Lean_indentExpr(lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_12__elabAppLValsAux___main___closed__1;
lean_object* l___private_Init_Lean_Elab_TermApp_15__getSuccess(lean_object*);
@ -353,7 +347,6 @@ lean_object* l_Lean_Elab_Term_addNamedArg___closed__4;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSortApp___closed__3;
uint8_t l_Lean_isStructure(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_TermApp_7__resolveLValAux___closed__25;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__2;
lean_object* l_Lean_Elab_Term_Arg_inhabited;
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* _init_l_Lean_Elab_Term_Arg_inhabited___closed__1() {
@ -9188,97 +9181,6 @@ x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_elabAppCore___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_array_get_size(x_2);
x_4 = lean_nat_dec_lt(x_1, x_3);
lean_dec(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6;
lean_dec(x_1);
x_5 = l_Array_empty___closed__1;
x_6 = x_2;
return x_6;
}
else
{
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;
x_7 = lean_array_fget(x_2, x_1);
x_8 = lean_box(0);
x_9 = x_8;
x_10 = lean_array_fset(x_2, x_1, x_9);
lean_inc(x_7);
x_11 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_11, 0, x_7);
x_12 = lean_unsigned_to_nat(1u);
x_13 = lean_nat_add(x_1, x_12);
x_14 = x_11;
lean_dec(x_7);
x_15 = lean_array_fset(x_10, x_1, x_14);
lean_dec(x_1);
x_1 = x_13;
x_2 = x_15;
goto _start;
}
}
}
lean_object* l_Lean_Elab_Term_elabAppCore(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_5 = lean_unsigned_to_nat(1u);
x_6 = l_Lean_Syntax_getArg(x_1, x_5);
x_7 = lean_unsigned_to_nat(2u);
x_8 = l_Lean_Syntax_getArg(x_1, x_7);
x_9 = l_Lean_Syntax_getArgs(x_8);
lean_dec(x_8);
x_10 = lean_unsigned_to_nat(0u);
x_11 = l_Array_umapMAux___main___at_Lean_Elab_Term_elabAppCore___spec__1(x_10, x_9);
x_12 = l_Array_empty___closed__1;
x_13 = l___private_Init_Lean_Elab_TermApp_18__elabAppAux(x_1, x_6, x_12, x_11, x_2, x_3, x_4);
return x_13;
}
}
lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("elabAppCore");
return x_1;
}
}
lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_declareBuiltinTermElab___closed__4;
x_2 = l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabAppCore), 4, 0);
return x_1;
}
}
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__2;
x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__3;
x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Term_elabAtom(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -9900,15 +9802,6 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabApp___closed__3);
res = l___regBuiltinTermElab_Lean_Elab_Term_elabApp(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__1();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__1);
l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__2();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__2);
l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__3();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore___closed__3);
res = l___regBuiltinTermElab_Lean_Elab_Term_elabAppCore(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__1();
lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__1);
l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabId___closed__2();

434
stage0/stdlib/Init/Lean/Parser/Term.c
View file

@ -84,7 +84,6 @@ lean_object* l_Lean_Parser_Term_lt___elambda__1(lean_object*, lean_object*, lean
lean_object* l_Lean_Parser_Term_tupleTail___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__4;
lean_object* l___regBuiltinParser_Lean_Parser_Term_appCore(lean_object*);
lean_object* l_Lean_Parser_andthenInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_have___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__2;
@ -172,7 +171,6 @@ lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__16;
lean_object* l_Lean_Parser_Term_doExpr___closed__4;
lean_object* l_Lean_Parser_Term_where;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_quotedName___closed__1;
lean_object* l_Lean_Parser_Term_explicit___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_instBinder___closed__5;
@ -206,7 +204,6 @@ lean_object* l_Lean_Parser_Term_prod___elambda__1(lean_object*, lean_object*, le
lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__1;
lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_anonymousCtor___elambda__1___spec__1(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_type___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_appCore___closed__5;
lean_object* l_Lean_Parser_Term_and___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_doSeq___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_parser_x21___elambda__1___closed__1;
@ -382,7 +379,6 @@ lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__8;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_explicit___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_sorry___closed__2;
lean_object* l_Lean_Parser_Term_if___closed__11;
@ -428,7 +424,6 @@ lean_object* l_Lean_Parser_Term_forall___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Term_tparser_x21(lean_object*);
lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__3;
extern lean_object* l_List_repr___rarg___closed__3;
lean_object* l_Lean_Parser_Term_appCore___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Term_antiquot___closed__1;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1___rarg___closed__8;
lean_object* l_Lean_Parser_Term_quotedName___elambda__1___closed__1;
@ -941,7 +936,6 @@ lean_object* l_Lean_Parser_Term_structInstSource___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_ge___closed__3;
lean_object* l_Lean_Parser_Term_structInstSource;
lean_object* l_Lean_Parser_Term_quotedName___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_appCore___closed__6;
lean_object* l_Lean_Parser_Term_doSeq___closed__2;
lean_object* l_Lean_Parser_Term_doSeq___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doElem___closed__1;
@ -1031,7 +1025,6 @@ lean_object* l_Lean_Parser_Term_match__syntax___elambda__1(lean_object*, lean_ob
lean_object* l_Lean_Parser_Term_modN___closed__2;
lean_object* l_Lean_Parser_Term_bnot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_depArrow___closed__5;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_typeAscription___elambda__1___closed__4;
@ -1240,7 +1233,6 @@ lean_object* l_Lean_Parser_Term_if___elambda__1(lean_object*, lean_object*, lean
lean_object* l_Lean_Parser_Term_prop___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_explicitBinder___closed__6;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__2;
lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_typeAscription___closed__7;
@ -1349,7 +1341,6 @@ lean_object* l_Lean_Parser_Term_uminus___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_bor___closed__2;
lean_object* l_Lean_Parser_Term_cdot___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_dollar___closed__3;
lean_object* l_Lean_Parser_Term_appCore___closed__1;
lean_object* l_Lean_Parser_Term_bne___closed__1;
lean_object* l_Lean_Parser_Term_matchAlt___closed__4;
lean_object* l_Lean_Parser_Term_mapConst___closed__1;
@ -1429,7 +1420,6 @@ lean_object* l_Lean_Parser_Term_anonymousCtor;
lean_object* l_Lean_Parser_Term_dollarProj___closed__4;
lean_object* l_Lean_Parser_Term_iff___closed__3;
lean_object* l_Lean_Parser_Term_forall___closed__9;
lean_object* l_Lean_Parser_Term_appCore___closed__2;
lean_object* l_Lean_Parser_Term_parser_x21___closed__1;
lean_object* l_Lean_Parser_Term_inaccessible___closed__3;
lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__4;
@ -1492,7 +1482,6 @@ lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_match___closed__9;
lean_object* l_Lean_Parser_Term_tupleTail___closed__5;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_match__syntax___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__8;
lean_object* l_Lean_Parser_Term_mapRev___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_where___elambda__1___spec__2___closed__1;
lean_object* l_Lean_Parser_Term_id___closed__7;
@ -1527,7 +1516,6 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__17;
lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__1;
lean_object* l_Lean_Parser_Term_forall___closed__4;
lean_object* l_Lean_Parser_Term_add___closed__1;
lean_object* l_Lean_Parser_Term_appCore___closed__4;
lean_object* l_Lean_Parser_Term_letIdDecl___closed__3;
lean_object* l_Lean_Parser_Term_le___closed__2;
lean_object* l_Lean_Parser_Term_match___closed__8;
@ -1564,7 +1552,6 @@ lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_if___closed__6;
lean_object* l_Lean_Parser_Term_letIdDecl___closed__2;
lean_object* l_Lean_Parser_Term_char;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_structInstField___closed__5;
lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1___closed__4;
lean_object* l_Lean_mkCAppStx(lean_object*, lean_object*);
@ -1616,7 +1603,6 @@ lean_object* l_Lean_Parser_Term_parenSpecial___closed__2;
lean_object* l_Lean_Parser_Term_arrayLit___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_binderDefault___elambda__1___closed__2;
lean_object* l_String_trim(lean_object*);
lean_object* l_Lean_Parser_Term_appCore___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_structInstSource___closed__7;
lean_object* l___regBuiltinParser_Lean_Parser_Term_prop(lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_antiquot(lean_object*);
@ -1771,7 +1757,6 @@ lean_object* l_Lean_Parser_Term_if___elambda__1___closed__12;
lean_object* l_Lean_Parser_sepByFn___at_Lean_Parser_Term_structInst___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_fcomp___closed__2;
lean_object* l_Lean_Parser_Term_where___closed__3;
lean_object* l_Lean_Parser_Term_appCore;
lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_sort___elambda__1___closed__9;
lean_object* l___regBuiltinParser_Lean_Parser_Term_gt(lean_object*);
@ -1828,7 +1813,6 @@ lean_object* l_Lean_Parser_Term_ne;
lean_object* l_Lean_Parser_Term_match___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_binderIdent___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_char___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_appCore___closed__3;
lean_object* l_Lean_Parser_Term_borrowed___elambda__1___closed__6;
lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_letEqns___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Term_borrowed(lean_object*);
@ -1847,7 +1831,6 @@ lean_object* l_Lean_Parser_Term_dollar___closed__1;
lean_object* l_Lean_Parser_Term_doExpr___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_char___elambda__1___closed__4;
lean_object* l_Lean_Parser_Term_if___elambda__1___closed__11;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__6;
lean_object* l_Lean_Parser_Term_map___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_matchAlt___closed__6;
lean_object* l_Lean_Parser_Term_parenSpecial___closed__4;
@ -1887,7 +1870,6 @@ lean_object* l_Lean_Parser_Term_doLet;
lean_object* l_Lean_Parser_Term_nomatch___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_namedPattern___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_doExpr;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__9;
lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_suffices___closed__6;
lean_object* l_Lean_Parser_Term_sortApp___elambda__1___closed__2;
@ -1906,7 +1888,6 @@ lean_object* l_Lean_Parser_Term_doId___closed__6;
lean_object* l_Lean_Parser_Term_leftArrow___elambda__1(lean_object*);
lean_object* l_Lean_Parser_Term_unicodeInfixR___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_emptyC___elambda__1___closed__7;
lean_object* l_Lean_Parser_Term_appCore___elambda__1___closed__4;
lean_object* l_Lean_mkAppStx___closed__1;
lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_unicodeInfixL___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -30576,384 +30557,6 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("appCore");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_appCore___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__4() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5;
x_1 = 0;
x_2 = l_Lean_Parser_Term_appCore___elambda__1___closed__1;
x_3 = l_Lean_Parser_Term_appCore___elambda__1___closed__3;
x_4 = 1;
x_5 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_app_ ");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Term_appCore___elambda__1___closed__5;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Term_appCore___elambda__1___closed__6;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_appCore___elambda__1___closed__7;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Term_appCore___elambda__1___closed__8;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Term_appCore___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = l_Lean_Parser_Term_appCore___elambda__1___closed__4;
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
x_6 = lean_ctor_get(x_3, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
lean_inc(x_2);
lean_inc(x_1);
x_9 = lean_apply_3(x_5, x_1, x_2, x_3);
x_10 = lean_ctor_get(x_9, 3);
lean_inc(x_10);
if (lean_obj_tag(x_10) == 0)
{
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_9, 1);
lean_inc(x_12);
x_13 = lean_nat_dec_eq(x_12, x_8);
lean_dec(x_12);
if (x_13 == 0)
{
lean_dec(x_11);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_2);
lean_dec(x_1);
return x_9;
}
else
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_46; lean_object* x_47;
lean_inc(x_8);
x_14 = l_Lean_Parser_ParserState_restore(x_9, x_7, x_8);
lean_dec(x_7);
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_array_get_size(x_15);
lean_dec(x_15);
lean_inc(x_2);
x_46 = l_Lean_Parser_tokenFn(x_2, x_14);
x_47 = lean_ctor_get(x_46, 3);
lean_inc(x_47);
if (lean_obj_tag(x_47) == 0)
{
lean_object* x_48; lean_object* x_49;
x_48 = lean_ctor_get(x_46, 0);
lean_inc(x_48);
x_49 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_48);
lean_dec(x_48);
if (lean_obj_tag(x_49) == 2)
{
lean_object* x_50; lean_object* x_51; uint8_t x_52;
x_50 = lean_ctor_get(x_49, 1);
lean_inc(x_50);
lean_dec(x_49);
x_51 = l_Lean_Parser_Term_appCore___elambda__1___closed__6;
x_52 = lean_string_dec_eq(x_50, x_51);
lean_dec(x_50);
if (x_52 == 0)
{
lean_object* x_53; lean_object* x_54;
x_53 = l_Lean_Parser_Term_appCore___elambda__1___closed__9;
lean_inc(x_8);
x_54 = l_Lean_Parser_ParserState_mkErrorsAt(x_46, x_53, x_8);
x_17 = x_54;
goto block_45;
}
else
{
x_17 = x_46;
goto block_45;
}
}
else
{
lean_object* x_55; lean_object* x_56;
lean_dec(x_49);
x_55 = l_Lean_Parser_Term_appCore___elambda__1___closed__9;
lean_inc(x_8);
x_56 = l_Lean_Parser_ParserState_mkErrorsAt(x_46, x_55, x_8);
x_17 = x_56;
goto block_45;
}
}
else
{
lean_object* x_57; lean_object* x_58;
lean_dec(x_47);
x_57 = l_Lean_Parser_Term_appCore___elambda__1___closed__9;
lean_inc(x_8);
x_58 = l_Lean_Parser_ParserState_mkErrorsAt(x_46, x_57, x_8);
x_17 = x_58;
goto block_45;
}
block_45:
{
lean_object* x_18;
x_18 = lean_ctor_get(x_17, 3);
lean_inc(x_18);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_19 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
x_20 = l_Lean_Parser_appPrec;
lean_inc(x_2);
x_21 = l_Lean_Parser_categoryParserFn(x_19, x_20, x_2, x_17);
x_22 = lean_ctor_get(x_21, 3);
lean_inc(x_22);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_21, 0);
lean_inc(x_23);
x_24 = lean_array_get_size(x_23);
lean_dec(x_23);
lean_inc(x_2);
x_25 = l_Lean_Parser_categoryParserFn(x_19, x_20, x_2, x_21);
x_26 = lean_ctor_get(x_25, 3);
lean_inc(x_26);
if (lean_obj_tag(x_26) == 0)
{
uint8_t 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;
x_27 = 0;
x_28 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Term_fun___elambda__1___spec__1(x_27, x_1, x_2, x_25);
lean_dec(x_1);
x_29 = l_Lean_nullKind;
x_30 = l_Lean_Parser_ParserState_mkNode(x_28, x_29, x_24);
x_31 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_32 = l_Lean_Parser_ParserState_mkNode(x_30, x_31, x_16);
x_33 = l_Lean_Parser_mergeOrElseErrors(x_32, x_11, x_8);
lean_dec(x_8);
return x_33;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_26);
lean_dec(x_2);
lean_dec(x_1);
x_34 = l_Lean_nullKind;
x_35 = l_Lean_Parser_ParserState_mkNode(x_25, x_34, x_24);
x_36 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_37 = l_Lean_Parser_ParserState_mkNode(x_35, x_36, x_16);
x_38 = l_Lean_Parser_mergeOrElseErrors(x_37, x_11, x_8);
lean_dec(x_8);
return x_38;
}
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
lean_dec(x_22);
lean_dec(x_2);
lean_dec(x_1);
x_39 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_40 = l_Lean_Parser_ParserState_mkNode(x_21, x_39, x_16);
x_41 = l_Lean_Parser_mergeOrElseErrors(x_40, x_11, x_8);
lean_dec(x_8);
return x_41;
}
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
lean_dec(x_18);
lean_dec(x_2);
lean_dec(x_1);
x_42 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_43 = l_Lean_Parser_ParserState_mkNode(x_17, x_42, x_16);
x_44 = l_Lean_Parser_mergeOrElseErrors(x_43, x_11, x_8);
lean_dec(x_8);
return x_44;
}
}
}
}
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Term_appCore___elambda__1___closed__6;
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_namedPattern___closed__2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
lean_inc(x_2);
x_3 = l_Lean_Parser_andthenInfo(x_2, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_appCore___closed__1;
x_2 = l_Lean_Parser_Term_appCore___closed__2;
x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_2 = l_Lean_Parser_Term_appCore___closed__3;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Term_appCore___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Term_appCore___closed__4;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Term_appCore___elambda__1), 3, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Term_appCore___closed__5;
x_2 = l_Lean_Parser_Term_appCore___closed__6;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Term_appCore() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Term_appCore___closed__7;
return x_1;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Term_appCore(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = 0;
x_3 = l_Lean_Parser_regBuiltinTermParserAttr___closed__4;
x_4 = l_Lean_Parser_Term_appCore___elambda__1___closed__2;
x_5 = l_Lean_Parser_Term_appCore;
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* l_Lean_Parser_Term_checkIsSort___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -39902,43 +39505,6 @@ lean_mark_persistent(l_Lean_Parser_Term_app);
res = l___regBuiltinParser_Lean_Parser_Term_app(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_appCore___elambda__1___closed__1 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__1);
l_Lean_Parser_Term_appCore___elambda__1___closed__2 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__2);
l_Lean_Parser_Term_appCore___elambda__1___closed__3 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__3);
l_Lean_Parser_Term_appCore___elambda__1___closed__4 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__4);
l_Lean_Parser_Term_appCore___elambda__1___closed__5 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__5);
l_Lean_Parser_Term_appCore___elambda__1___closed__6 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__6);
l_Lean_Parser_Term_appCore___elambda__1___closed__7 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__7);
l_Lean_Parser_Term_appCore___elambda__1___closed__8 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__8);
l_Lean_Parser_Term_appCore___elambda__1___closed__9 = _init_l_Lean_Parser_Term_appCore___elambda__1___closed__9();
lean_mark_persistent(l_Lean_Parser_Term_appCore___elambda__1___closed__9);
l_Lean_Parser_Term_appCore___closed__1 = _init_l_Lean_Parser_Term_appCore___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__1);
l_Lean_Parser_Term_appCore___closed__2 = _init_l_Lean_Parser_Term_appCore___closed__2();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__2);
l_Lean_Parser_Term_appCore___closed__3 = _init_l_Lean_Parser_Term_appCore___closed__3();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__3);
l_Lean_Parser_Term_appCore___closed__4 = _init_l_Lean_Parser_Term_appCore___closed__4();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__4);
l_Lean_Parser_Term_appCore___closed__5 = _init_l_Lean_Parser_Term_appCore___closed__5();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__5);
l_Lean_Parser_Term_appCore___closed__6 = _init_l_Lean_Parser_Term_appCore___closed__6();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__6);
l_Lean_Parser_Term_appCore___closed__7 = _init_l_Lean_Parser_Term_appCore___closed__7();
lean_mark_persistent(l_Lean_Parser_Term_appCore___closed__7);
l_Lean_Parser_Term_appCore = _init_l_Lean_Parser_Term_appCore();
lean_mark_persistent(l_Lean_Parser_Term_appCore);
res = l___regBuiltinParser_Lean_Parser_Term_appCore(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Term_checkIsSort___closed__1 = _init_l_Lean_Parser_Term_checkIsSort___closed__1();
lean_mark_persistent(l_Lean_Parser_Term_checkIsSort___closed__1);
l_Lean_Parser_Term_checkIsSort___closed__2 = _init_l_Lean_Parser_Term_checkIsSort___closed__2();