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 2021-08-21 16:39:47 -07:00
parent 54316fabb4
commit ef4359a439
4 changed files with 1192 additions and 495 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
stage0/src/Lean/Elab/Term.lean generated
View file

@ -1375,7 +1375,19 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
let view := extractMacroScopes n
let rec loop (n : Name) (projs : List String) :=
match lctx.findFromUserName? { view with name := n }.review with
| some decl => some (decl.toExpr, projs)
| some decl =>
if decl.isAuxDecl && !projs.isEmpty then
/- We do not consider dot notation for local decls corresponding to recursive functions being defined.
The following example would not be elaborated correctly without this case.
```
def foo.aux := 1
def foo : Nat → Nat
| n => foo.aux -- should not be interpreted as `(foo).bar`
```
-/
none
else
some (decl.toExpr, projs)
| none => match n with
| Name.str pre s _ => loop pre (s::projs)
| _ => none

3
stage0/src/Lean/Parser/Command.lean generated
View file

@ -32,7 +32,8 @@ def visibility := «private» <|> «protected»
def «noncomputable» := leading_parser "noncomputable "
def «unsafe» := leading_parser "unsafe "
def «partial» := leading_parser "partial "
def declModifiers (inline : Bool) := leading_parser optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional «partial»
def «nonrec» := leading_parser "nonrec "
def declModifiers (inline : Bool) := leading_parser optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> optional «noncomputable» >> optional «unsafe» >> optional («partial» <|> «nonrec»)
def declId := leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}")
def declSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.typeSpec
def optDeclSig := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType

131
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -110,6 +110,7 @@ lean_object* l_Lean_Elab_Term_resolveName___lambda__2___boxed(lean_object*, lean
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___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* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___spec__12___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*);
static lean_object* l_List_forIn_loop___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__5___lambda__2___closed__1;
uint8_t l_Lean_LocalDecl_isAuxDecl(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_USize_decEq(size_t, size_t);
lean_object* lean_array_uget(lean_object*, size_t);
@ -710,6 +711,7 @@ lean_object* l_List_foldlM___at_Lean_Elab_Term_evalExpr___spec__8___boxed(lean_o
lean_object* l_Lean_Elab_Term_getMessageLog___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore___lambda__1___closed__2;
lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_logUnassignedUsingErrorInfos___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__1;
lean_object* l_Std_PersistentArray_mapMAux___at_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_mkTermElabAttributeUnsafe___closed__13;
static lean_object* l_Lean_Elab_Term_instInhabitedSavedState___closed__6;
@ -722,7 +724,6 @@ lean_object* l_Lean_Elab_Term_tryCoeThunk_x3f(lean_object*, lean_object*, lean_o
static lean_object* l_Lean_Elab_Term_instMonadTermElabM___closed__1;
static lean_object* l_Lean_Elab_Term_termElabAttribute___closed__14;
lean_object* l_Lean_Elab_Term_synthesizeInstMVarCore_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__2;
lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryLiftAndCoe_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_instMonadTermElabM___closed__2;
lean_object* l_Lean_Meta_getMVarsAtDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -826,7 +827,6 @@ lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Term_instMetaEvalTermElabM
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withMVarContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_resolveName___closed__4;
lean_object* l_Lean_Elab_Term_withoutModifyingElabMetaStateWithInfo(lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__1;
lean_object* l_Lean_Elab_Term_instMonadBacktrackSavedStateTermElabM___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_head_x21___at_Lean_Elab_Term_resolveName_x27___spec__2___closed__4;
lean_object* l_Lean_Elab_Term_instMonadLogTermElabM___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -845,6 +845,7 @@ lean_object* l_Lean_Meta_withLocalDecl___at___private_Lean_Elab_Term_0__Lean_Ela
lean_object* l_Lean_Elab_Term_Context_sectionVars___default;
static lean_object* l_Lean_Elab_Term_tryPostponeIfHasMVars___closed__2;
lean_object* l_Lean_Elab_Term_resolveId_x3f_match__1(lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__2;
lean_object* l_Lean_Elab_Term_mkFreshBinderName___rarg(lean_object*, lean_object*);
lean_object* l_Lean_evalConst___at_Lean_Elab_Term_evalExpr___spec__11(lean_object*);
static lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__14;
@ -928,6 +929,7 @@ lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_loo
lean_object* l_Lean_Elab_Term_instMetaEvalTermElabM___rarg___lambda__3(lean_object*);
lean_object* l_Lean_Elab_Term_tryCoeThunk_x3f_match__1(lean_object*);
lean_object* l_List_map___at_Lean_MessageData_instCoeListExprMessageData___spec__1(lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__3;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_throwTypeMismatchError___spec__1(lean_object*);
static lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___lambda__6___closed__1;
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_4419____closed__3;
@ -996,7 +998,6 @@ lean_object* l_Lean_Elab_Term_isTypeApp_x3f(lean_object*, lean_object*, lean_obj
static lean_object* l_Lean_Elab_Term_instToStringLVal___closed__2;
lean_object* l_Lean_commitWhenSome_x3f___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__2___at___private_Lean_Elab_Term_0__Lean_Elab_Term_tryPureCoe_x3f___spec__3(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___private_Lean_Elab_Term_0__Lean_Elab_Term_elabImplicitLambda_loop___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*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__3;
lean_object* l_Lean_Elab_Term_elabTerm___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Context_autoBoundImplicits___default;
static lean_object* l_Lean_Elab_Term_instMonadQuotationTermElabM___closed__7;
@ -1184,7 +1185,7 @@ lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object
lean_object* l_Lean_Elab_Term_throwErrorIfErrors(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_initFn____x40_Lean_Elab_Term___hyg_4419____closed__1;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398_(lean_object*);
static lean_object* l_Lean_Elab_Term_termElabAttribute___closed__10;
lean_object* l_Lean_throwError___at_Lean_Elab_Term_evalExpr___spec__13(lean_object*);
lean_object* l_Lean_Elab_Term_addAutoBoundImplicits(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -40220,30 +40221,90 @@ lean_dec(x_1);
x_16 = !lean_is_exclusive(x_10);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_object* x_17; uint8_t x_18;
x_17 = lean_ctor_get(x_10, 0);
x_18 = l_Lean_LocalDecl_toExpr(x_17);
x_18 = l_Lean_LocalDecl_isAuxDecl(x_17);
if (x_18 == 0)
{
lean_object* x_19; lean_object* x_20;
x_19 = l_Lean_LocalDecl_toExpr(x_17);
lean_dec(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_4);
lean_ctor_set(x_10, 0, x_19);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_4);
lean_ctor_set(x_10, 0, x_20);
return x_10;
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_20 = lean_ctor_get(x_10, 0);
lean_inc(x_20);
uint8_t x_21;
x_21 = l_List_isEmpty___rarg(x_4);
if (x_21 == 0)
{
lean_object* x_22;
lean_free_object(x_10);
lean_dec(x_17);
lean_dec(x_4);
x_22 = lean_box(0);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24;
x_23 = l_Lean_LocalDecl_toExpr(x_17);
lean_dec(x_17);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_4);
lean_ctor_set(x_10, 0, x_24);
return x_10;
}
}
}
else
{
lean_object* x_25; uint8_t x_26;
x_25 = lean_ctor_get(x_10, 0);
lean_inc(x_25);
lean_dec(x_10);
x_21 = l_Lean_LocalDecl_toExpr(x_20);
lean_dec(x_20);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_4);
x_23 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_23, 0, x_22);
return x_23;
x_26 = l_Lean_LocalDecl_isAuxDecl(x_25);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = l_Lean_LocalDecl_toExpr(x_25);
lean_dec(x_25);
x_28 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_28, 0, x_27);
lean_ctor_set(x_28, 1, x_4);
x_29 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_29, 0, x_28);
return x_29;
}
else
{
uint8_t x_30;
x_30 = l_List_isEmpty___rarg(x_4);
if (x_30 == 0)
{
lean_object* x_31;
lean_dec(x_25);
lean_dec(x_4);
x_31 = lean_box(0);
return x_31;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = l_Lean_LocalDecl_toExpr(x_25);
lean_dec(x_25);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_4);
x_34 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_34, 0, x_33);
return x_34;
}
}
}
}
}
@ -50501,7 +50562,7 @@ lean_dec(x_3);
return x_11;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
@ -50511,7 +50572,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__2() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__2() {
_start:
{
lean_object* x_1;
@ -50519,17 +50580,17 @@ x_1 = lean_mk_string("debug");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__3() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Term_MVarErrorInfo_logError___closed__12;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__2;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__2;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389_(lean_object* x_1) {
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -50541,7 +50602,7 @@ lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__1;
x_5 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__1;
x_6 = l_Lean_registerTraceClass(x_5, x_4);
if (lean_obj_tag(x_6) == 0)
{
@ -50549,7 +50610,7 @@ lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__3;
x_8 = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__3;
x_9 = l_Lean_registerTraceClass(x_8, x_7);
return x_9;
}
@ -51515,13 +51576,13 @@ l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed_
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__3);
l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__4 = _init_l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__4();
lean_mark_persistent(l___private_Lean_Elab_Term_0__Lean_Elab_Term_throwStuckAtUniverseCnstr___closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389____closed__3);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12389_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398____closed__3);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Term___hyg_12398_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

1539
stage0/stdlib/Lean/Parser/Command.c generated
View file

File diff suppressed because it is too large Load diff