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-10-19 14:52:04 -07:00
parent 84a0cd1f59
commit 3cb0dfd38c
12 changed files with 635 additions and 468 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Lean/Compiler/IR/EmitC.lean generated
View file

@ -684,7 +684,7 @@ if isIOUnitInitFn env n then
emitLn "if (lean_io_result_is_error(res)) return res;"
emitLn "lean_dec_ref(res);"
else if d.params.size == 0 then
match getInitFnNameFor env d.name with
match getInitFnNameFor? env d.name with
| some initFn =>
emit "res = "; emitCName initFn; emitLn "(lean_io_mk_world());"
emitLn "if (lean_io_result_is_error(res)) return res;"

2
stage0/src/Lean/Compiler/IR/EmitUtil.lean generated
View file

@ -38,7 +38,7 @@ partial def collectFnBody : FnBody → M Unit
def collectInitDecl (fn : Name) : M Unit := do
let env ← read
match getInitFnNameFor env fn with
match getInitFnNameFor? env fn with
| some initFn => collect initFn
| _ => pure ()

44
stage0/src/Lean/Compiler/InitAttr.lean generated
View file

@ -22,8 +22,8 @@ match getIOTypeArg type with
| some type => isUnitType type
| _ => false
initialize initAttr : ParametricAttribute Name ←
registerParametricAttribute `init "initialization procedure for global references" $ fun declName stx => do
def registerInitAttr (attrName : Name) : IO (ParametricAttribute Name) :=
registerParametricAttribute attrName "initialization procedure for global references" fun declName stx => do
let decl ← getConstInfo declName
match attrParamSyntaxToIdentifier stx with
| some initFnName =>
@ -40,22 +40,40 @@ registerParametricAttribute `init "initialization procedure for global reference
else throwError "initialization function must have type `IO Unit`"
| _ => throwError "unexpected kind of argument"
initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init
initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit
def getInitFnNameForCore? (env : Environment) (attr : ParametricAttribute Name) (fn : Name) : Option Name :=
match attr.getParam env fn with
| some Name.anonymous => none
| some n => some n
| _ => none
@[export lean_get_builtin_init_fn_name_for]
def getBuiltinInitFnNameFor? (env : Environment) (fn : Name) : Option Name :=
getInitFnNameForCore? env builtinInitAttr fn
@[export lean_get_regular_init_fn_name_for]
def getRegularInitFnNameFor? (env : Environment) (fn : Name) : Option Name :=
getInitFnNameForCore? env regularInitAttr fn
-- Only used
def isIOUnitInitFn (env : Environment) (fn : Name) : Bool :=
match initAttr.getParam env fn with
| some Name.anonymous => true
| _ => false
let aux (attr : ParametricAttribute Name) : Bool :=
match attr.getParam env fn with
| some Name.anonymous => true
| _ => false
aux builtinInitAttr || aux regularInitAttr
@[export lean_get_init_fn_name_for]
def getInitFnNameFor (env : Environment) (fn : Name) : Option Name :=
match initAttr.getParam env fn with
| some Name.anonymous => none
| some n => some n
| _ => none
def getInitFnNameFor? (env : Environment) (fn : Name) : Option Name :=
getBuiltinInitFnNameFor? env fn <|> getRegularInitFnNameFor? env fn
def hasInitAttr (env : Environment) (fn : Name) : Bool :=
(getInitFnNameFor env fn).isSome
(getInitFnNameFor? env fn).isSome
def setInitAttr (env : Environment) (declName : Name) (initFnName : Name := Name.anonymous) : Except String Environment :=
initAttr.setParam env declName initFnName
def setBuiltinInitAttr (env : Environment) (declName : Name) (initFnName : Name := Name.anonymous) : Except String Environment :=
-- builtinInitAttr.setParam env declName initFnName -- TODO: use this one
regularInitAttr.setParam env declName initFnName
end Lean

2
stage0/src/Lean/KeyedDeclsAttribute.lean generated
View file

@ -117,7 +117,7 @@ match env.addAndCompile {} decl with
| Except.error e => do
msg ← (e.toMessageData {}).toString;
throw (IO.userError ("failed to emit registration code for builtin '" ++ toString declName ++ "': " ++ msg))
| Except.ok env => IO.ofExcept (setInitAttr env name)
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name)
/- TODO: add support for scoped attributes -/
protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDeclsAttribute γ) := do

2
stage0/src/Lean/Parser/Extension.lean generated
View file

@ -372,7 +372,7 @@ let decl := Declaration.defnDecl { name := name, lparams := [], type := type, va
match env.addAndCompile {} decl with
-- TODO: pretty print error
| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
| Except.ok env => IO.ofExcept (setInitAttr env name)
| Except.ok env => IO.ofExcept (setBuiltinInitAttr env name)
def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) (prio : Nat) : IO Environment := -- TODO: use CoreM?
declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser catName declName prio

6
stage0/stdlib/Lean/Compiler/IR.c generated
View file

@ -79,6 +79,7 @@ lean_object* l_Lean_IR_ExplicitBoxing_mkBoxedVersion(lean_object*);
lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__23;
lean_object* l_Lean_IR_inferBorrow(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__12;
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__2;
lean_object* l_Lean_IR_Decl_pushProj(lean_object*);
lean_object* l_Lean_IR_Decl_normalizeIds(lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__2;
@ -86,7 +87,6 @@ lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__26;
lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__31;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_IR_declMapExt;
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__2;
lean_object* l_Lean_IR_compile_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_IR_addBoxedVersionAux___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__19;
@ -297,7 +297,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_IR_tracePrefixOptionName;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__2;
x_2 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__2;
x_3 = l_Lean_Name_append___main(x_1, x_2);
return x_3;
}
@ -587,7 +587,7 @@ _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;
x_4 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1;
x_5 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__2;
x_5 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__2;
lean_inc(x_1);
x_6 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_4, x_5, x_1, x_2, x_3);
x_7 = lean_ctor_get(x_6, 1);

12
stage0/stdlib/Lean/Compiler/IR/EmitC.c generated
View file

@ -230,6 +230,7 @@ lean_object* l_Lean_IR_EmitC_emitFnDeclAux___lambda__2(lean_object*, lean_object
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitInc___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_isIf___boxed(lean_object*);
lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitCtorScalarSize___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitCtorScalarSize___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
@ -368,6 +369,7 @@ extern lean_object* l_String_Iterator_HasRepr___closed__2;
lean_object* l_Lean_IR_EmitC_emitIsTaggedPtr___closed__1;
lean_object* l_Nat_forMAux___main___at_Lean_IR_EmitC_emitReset___spec__1___closed__1;
lean_object* l_Lean_IR_EmitC_emitMainFn___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitBoxFn___closed__2;
lean_object* l_Lean_IR_EmitC_toCType___closed__4;
lean_object* l_Lean_IR_EmitC_emitProj___closed__1;
@ -464,7 +466,6 @@ lean_object* l_Lean_IR_EmitC_emitNumLit___boxed(lean_object*, lean_object*, lean
lean_object* l_Lean_IR_EmitC_emitUSet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitInitFn___closed__3;
lean_object* l_Lean_IR_EmitC_emitBoxFn___closed__1;
lean_object* l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitInc___closed__4;
lean_object* l_Lean_IR_EmitC_emitFnDecls_match__1(lean_object*);
lean_object* l_Lean_IR_EmitC_emitDeclAux___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -519,7 +520,6 @@ lean_object* l_Lean_IR_EmitC_emitBoxFn(lean_object*, lean_object*, lean_object*)
lean_object* l_Lean_IR_EmitC_isTailCall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_throwInvalidExportName___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitFileFooter___boxed(lean_object*, lean_object*);
lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitFnDeclAux___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_EmitC_emitFnDeclAux___lambda__3___closed__1;
lean_object* l_Lean_IR_EmitC_throwInvalidExportName___rarg___closed__1;
@ -1588,7 +1588,7 @@ x_6 = lean_ctor_get(x_4, 0);
x_7 = lean_ctor_get(x_4, 1);
x_8 = l_Lean_exportAttr;
lean_inc(x_1);
x_9 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_8, x_6, x_1);
x_9 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_8, x_6, x_1);
lean_dec(x_6);
if (lean_obj_tag(x_9) == 0)
{
@ -1663,7 +1663,7 @@ lean_inc(x_20);
lean_dec(x_4);
x_22 = l_Lean_exportAttr;
lean_inc(x_1);
x_23 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_22, x_20, x_1);
x_23 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_22, x_20, x_1);
lean_dec(x_20);
if (lean_obj_tag(x_23) == 0)
{
@ -1898,7 +1898,7 @@ x_6 = lean_ctor_get(x_4, 0);
x_7 = lean_ctor_get(x_4, 1);
x_8 = l_Lean_exportAttr;
lean_inc(x_1);
x_9 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_8, x_6, x_1);
x_9 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_8, x_6, x_1);
lean_dec(x_6);
if (lean_obj_tag(x_9) == 0)
{
@ -1965,7 +1965,7 @@ lean_inc(x_21);
lean_dec(x_4);
x_23 = l_Lean_exportAttr;
lean_inc(x_1);
x_24 = l_Lean_ParametricAttribute_getParam___at_Lean_isIOUnitInitFn___spec__1(x_23, x_21, x_1);
x_24 = l_Lean_ParametricAttribute_getParam___at_Lean_getInitFnNameForCore_x3f___spec__1(x_23, x_21, x_1);
lean_dec(x_21);
if (lean_obj_tag(x_24) == 0)
{

2
stage0/stdlib/Lean/Compiler/IR/EmitUtil.c generated
View file

@ -46,6 +46,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_IR_CollectMaps_collectParams___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_AltCore_body(lean_object*);
lean_object* lean_array_fget(lean_object*, lean_object*);
lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_IR_CollectMaps_collectFnBody_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_IR_CollectMaps_collectVar_match__1(lean_object*);
@ -84,7 +85,6 @@ lean_object* l_Std_HashMapImp_moveEntries___main___at_Lean_IR_CollectMaps_collec
lean_object* lean_nat_mul(lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_insert___at_Lean_IR_CollectMaps_collectVar___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_contains___at_Lean_IR_CollectMaps_collectJP___spec__2___boxed(lean_object*, lean_object*);
lean_object* lean_get_init_fn_name_for(lean_object*, lean_object*);
lean_object* l_Lean_Environment_allImportedModuleNames(lean_object*);
lean_object* l_Lean_IR_CollectMaps_collectDecl(lean_object*, lean_object*);
lean_object* lean_mk_array(lean_object*, lean_object*);

1011
stage0/stdlib/Lean/Compiler/InitAttr.c generated
View file

File diff suppressed because it is too large Load diff

12
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -309,6 +309,7 @@ lean_object* l_Lean_Elab_Command_elabAxiom_match__4(lean_object*);
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandMutualPreamble___closed__6;
extern lean_object* l_Lean_Elab_Command_isDefLike___closed__3;
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__2;
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualNamespace___closed__1;
lean_object* l_Lean_Elab_Command_elabAxiom_match__5(lean_object*);
@ -324,6 +325,7 @@ lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__4_
lean_object* l_List_map___main___at_Lean_resolveGlobalConst___spec__2(lean_object*);
lean_object* l_Array_anyRangeMAux___main___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualInductive___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__5;
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__1;
lean_object* l_Lean_Elab_Command_elabAxiom___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___closed__3;
lean_object* l_Lean_Elab_Command_checkValidCtorModifier(lean_object*, lean_object*, lean_object*, lean_object*);
@ -342,7 +344,6 @@ extern lean_object* l___private_Lean_Meta_Match_Match_0__Lean_Meta_Match_process
lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabAttr___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabDeclaration___closed__3;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__2;
lean_object* l_Lean_Meta_mkForallUsedOnly___at_Lean_Elab_Command_elabAxiom___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandMutualElement_match__2___rarg(lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_isMutualInductive(lean_object*);
@ -358,7 +359,6 @@ extern lean_object* l_Lean_Elab_Command_elabNamespace___closed__1;
lean_object* l_Lean_Meta_mkForallFVars___at_Lean_Elab_Term_elabForall___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabMutual___closed__1;
lean_object* l_Lean_Elab_Command_elabAxiom_match__1(lean_object*);
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__1;
extern lean_object* l___regBuiltin_Lean_Elab_Command_elabSetOption___closed__2;
lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabAttr___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f___closed__6;
@ -6478,7 +6478,7 @@ static lean_object* _init_l_Lean_Elab_Command_expandInitialize___closed__33() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__1;
x_1 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__1;
x_2 = lean_string_utf8_byte_size(x_1);
return x_2;
}
@ -6487,7 +6487,7 @@ static lean_object* _init_l_Lean_Elab_Command_expandInitialize___closed__34() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__1;
x_1 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_Elab_Command_expandInitialize___closed__33;
x_4 = lean_alloc_ctor(0, 3, 0);
@ -6694,7 +6694,7 @@ x_66 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_66, 0, x_65);
lean_ctor_set(x_66, 1, x_64);
x_67 = lean_array_push(x_21, x_66);
x_68 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__2;
x_68 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__2;
x_69 = l_Lean_addMacroScope(x_14, x_68, x_13);
x_70 = l_Lean_Elab_Command_expandInitialize___closed__34;
x_71 = lean_alloc_ctor(3, 4, 0);
@ -6776,7 +6776,7 @@ lean_inc(x_111);
x_112 = lean_ctor_get(x_2, 1);
lean_inc(x_112);
lean_dec(x_2);
x_113 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_237____closed__2;
x_113 = l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_362____closed__2;
lean_inc(x_111);
lean_inc(x_112);
x_114 = l_Lean_addMacroScope(x_112, x_113, x_111);

4
stage0/stdlib/Lean/KeyedDeclsAttribute.c generated
View file

@ -216,6 +216,7 @@ lean_object* l_Lean_Name_toExprAux___main(lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_init___rarg___closed__6;
lean_object* l_IO_ofExcept___at_Lean_KeyedDeclsAttribute_declareBuiltin___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Std_AssocList_foldlM___at_Lean_KeyedDeclsAttribute_Table_insert___spec__18(lean_object*);
extern lean_object* l_Lean_regularInitAttr;
lean_object* l_Lean_KeyedDeclsAttribute_declareBuiltin___rarg___closed__11;
lean_object* l___private_Lean_KeyedDeclsAttribute_3__addExtensionEntry___rarg(lean_object*, lean_object*);
lean_object* l_Lean_SMap_find_x3f___at_Lean_KeyedDeclsAttribute_getValues___spec__1(lean_object*);
@ -270,7 +271,6 @@ lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_KeyedDeclsAttribute_getValues___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_find_x3f___at_Lean_KeyedDeclsAttribute_Table_insert___spec__6___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ofExcept___at_Lean_KeyedDeclsAttribute_init___spec__7___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_initAttr;
lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_KeyedDeclsAttribute_Table_insert___spec__2___rarg(lean_object*, lean_object*);
lean_object* l_Std_HashMapImp_find_x3f___at_Lean_KeyedDeclsAttribute_Table_insert___spec__5___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Std_mkHashMap___at_Lean_KeyedDeclsAttribute_ExtensionState_inhabited___spec__1___rarg(lean_object*);
@ -3554,7 +3554,7 @@ lean_dec(x_5);
x_58 = lean_ctor_get(x_29, 0);
lean_inc(x_58);
lean_dec(x_29);
x_59 = l_Lean_initAttr;
x_59 = l_Lean_regularInitAttr;
x_60 = lean_box(0);
x_61 = l_Lean_ParametricAttribute_setParam___rarg(x_59, x_58, x_8, x_60);
x_62 = l_IO_ofExcept___at_Lean_KeyedDeclsAttribute_declareBuiltin___spec__1(x_61, x_6);

4
stage0/stdlib/Lean/Parser/Extension.c generated
View file

@ -343,6 +343,7 @@ lean_object* l_Lean_Parser_parserAttributeHooks;
lean_object* l___private_Lean_Parser_Extension_13__registerParserAttributeImplBuilder(lean_object*);
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_notFollowedByTermToken;
extern lean_object* l_Lean_regularInitAttr;
lean_object* l_Lean_Parser_getParserPriority(lean_object*);
lean_object* l_Lean_Parser_builtinSyntaxNodeKindSetRef;
lean_object* l_Lean_Parser_registerBuiltinNodeKind(lean_object*, lean_object*);
@ -426,7 +427,6 @@ lean_object* l_Lean_Parser_compileParserDescr___main___closed__4;
extern lean_object* l_Lean_Parser_Parser_inhabited___closed__1;
lean_object* l___private_Lean_Data_Trie_3__findAux_x3f___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_ofExcept___at___private_Lean_Parser_Extension_10__ParserExtension_addImported___spec__2(lean_object*, lean_object*);
extern lean_object* l_Lean_initAttr;
lean_object* l_Std_PersistentHashMap_containsAux___main___at___private_Lean_Parser_Extension_3__addParserCategoryCore___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldl___main___at_Lean_Parser_addLeadingParser___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Extension_10__ParserExtension_addImported(lean_object*, lean_object*, lean_object*);
@ -7719,7 +7719,7 @@ lean_dec(x_4);
x_37 = lean_ctor_get(x_28, 0);
lean_inc(x_37);
lean_dec(x_28);
x_38 = l_Lean_initAttr;
x_38 = l_Lean_regularInitAttr;
x_39 = lean_box(0);
x_40 = l_Lean_ParametricAttribute_setParam___rarg(x_38, x_37, x_8, x_39);
x_41 = l_IO_ofExcept___at_Lean_KeyedDeclsAttribute_declareBuiltin___spec__1(x_40, x_6);