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-23 12:23:22 -08:00
parent e681bd71d9
commit 09a482a2b4
11 changed files with 3102 additions and 6664 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Lean/Elab/Command.lean
View file

@ -192,9 +192,7 @@ adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after
instance : MonadMacroAdapter CommandElabM :=
{ getEnv := getEnv,
getNameGenerator := do s ← get; pure s.ngen,
getCurrMacroScope := getCurrMacroScope,
setNameGenerator := fun ngen => modify $ fun s => { ngen := ngen, .. s },
throwError := @throwError,
throwUnsupportedSyntax := @throwUnsupportedSyntax}

2
stage0/src/Init/Lean/Elab/Tactic/Basic.lean
View file

@ -176,9 +176,7 @@ adaptReader (fun (ctx : Context) => { macroStack := { before := beforeStx, after
instance : MonadMacroAdapter TacticM :=
{ getEnv := getEnv,
getNameGenerator := do s ← get; pure s.ngen,
getCurrMacroScope := getCurrMacroScope,
setNameGenerator := fun ngen => modify $ fun s => { ngen := ngen, .. s },
throwError := @throwError,
throwUnsupportedSyntax := @throwUnsupportedSyntax }

2
stage0/src/Init/Lean/Elab/Term.lean
View file

@ -465,9 +465,7 @@ private def elabTermUsing (s : State) (stx : Syntax) (expectedType? : Option Exp
instance : MonadMacroAdapter TermElabM :=
{ getEnv := getEnv,
getNameGenerator := do s ← get; pure s.ngen,
getCurrMacroScope := getCurrMacroScope,
setNameGenerator := fun ngen => modify $ fun s => { ngen := ngen, .. s },
throwError := @throwError,
throwUnsupportedSyntax := @throwUnsupportedSyntax}

11
stage0/src/Init/Lean/Elab/Util.lean
View file

@ -187,19 +187,16 @@ fun stx =>
class MonadMacroAdapter (m : Type → Type) :=
(getEnv {} : m Environment)
(getCurrMacroScope {} : m MacroScope)
(getNameGenerator {} : m NameGenerator)
(setNameGenerator {} : NameGenerator → m Unit)
(throwError {} {α : Type} : Syntax → MessageData → m α)
(throwUnsupportedSyntax {} {α : Type} : m α)
@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : Macro) (stx : Syntax) : m Syntax := do
scp ← MonadMacroAdapter.getCurrMacroScope;
env ← MonadMacroAdapter.getEnv;
ngen ← MonadMacroAdapter.getNameGenerator;
match x stx { currMacroScope := scp, mainModule := env.mainModule } { ngen := ngen } with
| EStateM.Result.error Macro.Exception.unsupportedSyntax newS => MonadMacroAdapter.throwUnsupportedSyntax
| EStateM.Result.ok stx newS => do MonadMacroAdapter.setNameGenerator newS.ngen; pure stx
| EStateM.Result.error (Macro.Exception.error msg) newS => do MonadMacroAdapter.setNameGenerator newS.ngen; MonadMacroAdapter.throwError stx msg
match x stx { currMacroScope := scp, mainModule := env.mainModule } with
| Except.error Macro.Exception.unsupportedSyntax => MonadMacroAdapter.throwUnsupportedSyntax
| Except.error (Macro.Exception.error msg) => MonadMacroAdapter.throwError stx msg
| Except.ok stx => pure stx
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab;

14
stage0/src/Init/LeanInit.lean
View file

@ -9,7 +9,7 @@ import Init.Data.Array.Basic
import Init.Data.UInt
import Init.Data.Hashable
import Init.Control.Reader
import Init.Control.EState
import Init.Control.Except
namespace Lean
/-
@ -321,23 +321,17 @@ structure Context :=
(mainModule : Name)
(currMacroScope : MacroScope)
structure State :=
(ngen : NameGenerator)
inductive Exception
| error : String → Exception
| unsupportedSyntax : Exception
end Macro
abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception Macro.State)
abbrev MacroM := ReaderT Macro.Context (ExceptT Macro.Exception Id)
def Macro.mkFreshName (namePrefix : Name) : MacroM Name := do
def Macro.addMacroScope (n : Name) : MacroM Name := do
ctx ← read;
s ← get;
let id := namePrefix ++ ctx.mainModule ++ s.ngen.curr;
modify $ fun s => { ngen := s.ngen.next, .. s };
pure id
pure $ Lean.addMacroScope ctx.mainModule n ctx.currMacroScope
instance MacroM.monadQuotation : MonadQuotation MacroM :=
{ getCurrMacroScope := fun ctx => pure ctx.currMacroScope,

3546
stage0/stdlib/Init/Lean/Elab/Command.c
View file

File diff suppressed because it is too large Load diff

31
stage0/stdlib/Init/Lean/Elab/SynthesizeSyntheticMVars.c
View file

@ -35,6 +35,7 @@ lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_5__synthesizeSy
lean_object* l_Lean_mkMVar(lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___closed__6;
lean_object* l_Lean_Elab_Term_liftTacticElabM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_9__getSomeSynthethicMVarsRef___rarg___closed__1;
lean_object* l_List_append___rarg(lean_object*, lean_object*);
@ -51,6 +52,7 @@ lean_object* l_Lean_Elab_Term_assignExprMVar(lean_object*, lean_object*, lean_ob
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_1__resumeElabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1(lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_3__synthesizePendingInstMVar(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeUsingDefault___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getOptions(lean_object*, lean_object*);
@ -64,7 +66,6 @@ lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg(lean
lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeUsingDefault___spec__1___lambda__1___closed__3;
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___closed__7;
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_4__checkWithDefault(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_7__synthesizeUsingDefault(lean_object*, lean_object*);
lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_8__reportStuckSyntheticMVars___spec__1___lambda__1___closed__3;
@ -126,6 +127,7 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSy
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_10__synthesizeSyntheticMVarsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___closed__4;
lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_8__reportStuckSyntheticMVars___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_indentExpr(lean_object*);
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_10__synthesizeSyntheticMVarsAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_6__synthesizeSyntheticMVarsStep___spec__2___closed__3;
@ -1534,6 +1536,22 @@ x_7 = l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_1__resumeElabTerm(x_1,
return x_7;
}
}
lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_apply_1(x_1, x_3);
return x_4;
}
}
lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed), 3, 0);
return x_2;
}
}
lean_object* _init_l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___lambda__1___closed__1() {
_start:
{
@ -1819,7 +1837,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_EStateM_MonadState___closed__2;
x_2 = lean_alloc_closure((void*)(l_ReaderT_lift___at_Lean_Elab_Term_Lean_Elab_MonadMacroAdapter___spec__1___rarg___boxed), 3, 1);
x_2 = lean_alloc_closure((void*)(l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -1844,6 +1862,15 @@ lean_dec(x_3);
return x_11;
}
}
lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_ReaderT_lift___at___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___spec__1___rarg(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* l___private_Init_Lean_Elab_SynthesizeSyntheticMVars_2__resumePostponed___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{

2338
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

File diff suppressed because it is too large Load diff

3371
stage0/stdlib/Init/Lean/Elab/Term.c
View file

File diff suppressed because it is too large Load diff

298
stage0/stdlib/Init/Lean/Elab/Util.c
View file

@ -30,7 +30,6 @@ lean_object* l_Lean_Elab_mkMacroAttribute(lean_object*);
lean_object* l_Lean_Elab_mkElabAttributeAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType(lean_object*);
lean_object* l_Lean_Elab_macroAttribute___closed__2;
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_String_toFormat(lean_object*);
extern lean_object* l_Lean_MessageData_ofList___closed__3;
@ -69,7 +68,7 @@ lean_object* l_List_find_x3f___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__6___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkMacroAttribute___closed__3;
lean_object* l___private_Init_Lean_Elab_Util_1__ElabAttribute_mkInitial___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1___closed__2;
@ -81,6 +80,7 @@ lean_object* l_Lean_Elab_adaptMacro___boxed(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg(lean_object*, lean_object*);
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__20(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1;
extern lean_object* l_Lean_mkAttributeImplOfConstantUnsafe___closed__3;
lean_object* l_AssocList_replace___main___at_Lean_Elab_ElabFnTable_insert___spec__19(lean_object*);
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_getMacros___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -126,7 +126,6 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__El
lean_object* l_HashMapImp_expand___at_Lean_Elab_ElabFnTable_insert___spec__16___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__2;
lean_object* l_finally___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_2__throwUnexpectedElabType___rarg___closed__3;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__1;
lean_object* l_Lean_Elab_ElabAttributeExtensionState_inhabited___closed__1;
@ -148,7 +147,7 @@ size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*);
extern lean_object* l_PersistentHashMap_insertAux___main___rarg___closed__3;
lean_object* l_Lean_Syntax_prettyPrint(lean_object*);
lean_object* l_mkHashMap___at_Lean_Elab_mkBuiltinMacroFnTable___spec__2(lean_object*);
@ -160,7 +159,7 @@ lean_object* l_Lean_Elab_mkElabAttributeAux___rarg___lambda__2(lean_object*);
lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed__2;
lean_object* lean_eval_const(lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__2;
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_Elab_mkElabAttributeAux___spec__2(lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1___closed__1;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg(lean_object*, lean_object*);
@ -216,8 +215,7 @@ lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__8
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_getMacros___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getMacros___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getMacros___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentHashMap_insertAux___main___at_Lean_Elab_ElabFnTable_insert___spec__11___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__3;
lean_object* l_Lean_Elab_macroAttribute;
@ -232,7 +230,7 @@ uint8_t l_USize_decLe(size_t, size_t);
lean_object* l_HashMapImp_insert___at_Lean_Elab_ElabFnTable_insert___spec__25___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_mkElabAttribute(lean_object*);
lean_object* l_AssocList_foldlM___main___at_Lean_Elab_ElabFnTable_insert___spec__18___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkBuiltinMacroFnTable___spec__1___closed__2;
lean_object* l_Lean_Elab_adaptMacro(lean_object*);
@ -284,7 +282,6 @@ lean_object* l_Lean_Elab_checkSyntaxNodeKind___boxed(lean_object*, lean_object*)
lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Elab_ElabFnTable_insert___spec__23(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__13(lean_object*);
lean_object* l_Lean_SMap_insert___at_Lean_Elab_ElabFnTable_insert___spec__9___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__4;
lean_object* l_Lean_Elab_checkSyntaxNodeKind(lean_object*, lean_object*);
lean_object* l_AssocList_find___main___at_Lean_Elab_ElabFnTable_insert___spec__8___rarg___boxed(lean_object*, lean_object*);
@ -316,7 +313,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__El
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1(lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__13___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__4;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_ElabFnTable_insert___spec__24(lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam(lean_object*, lean_object*, lean_object*);
@ -5529,57 +5526,60 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* _init_l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_box(1);
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_5; lean_object* x_6;
lean_object* x_4;
lean_dec(x_3);
lean_dec(x_1);
x_5 = lean_box(1);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
return x_6;
x_4 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1;
return x_4;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_2, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_2, 1);
lean_inc(x_8);
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
lean_dec(x_2);
lean_inc(x_3);
lean_inc(x_1);
x_9 = lean_apply_3(x_7, x_1, x_3, x_4);
if (lean_obj_tag(x_9) == 0)
x_7 = lean_apply_2(x_5, x_1, x_3);
if (lean_obj_tag(x_7) == 0)
{
lean_dec(x_8);
lean_dec(x_3);
lean_dec(x_1);
return x_9;
lean_dec(x_7);
x_2 = x_6;
goto _start;
}
else
{
lean_object* x_10;
x_10 = lean_ctor_get(x_9, 1);
lean_inc(x_10);
lean_dec(x_9);
x_2 = x_8;
x_4 = x_10;
goto _start;
lean_dec(x_6);
lean_dec(x_3);
lean_dec(x_1);
return x_7;
}
}
}
}
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l___private_Init_Lean_Elab_Util_7__expandMacroFns(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_5;
x_5 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_1, x_2, x_3, x_4);
return x_5;
lean_object* x_4;
x_4 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_getMacros___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
@ -5800,41 +5800,38 @@ return x_9;
}
}
}
lean_object* l_Lean_Elab_getMacros(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Elab_getMacros(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_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_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
lean_inc(x_2);
x_5 = l_Lean_Syntax_getKind(x_2);
x_6 = l_Lean_Elab_macroAttribute;
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
x_8 = l_Lean_PersistentEnvExtension_getState___rarg(x_7, x_1);
x_4 = l_Lean_Syntax_getKind(x_2);
x_5 = l_Lean_Elab_macroAttribute;
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
x_7 = l_Lean_PersistentEnvExtension_getState___rarg(x_6, x_1);
lean_dec(x_6);
x_8 = lean_ctor_get(x_7, 1);
lean_inc(x_8);
lean_dec(x_7);
x_9 = lean_ctor_get(x_8, 1);
lean_inc(x_9);
lean_dec(x_8);
x_10 = l_Lean_SMap_find_x3f___at_Lean_Elab_getMacros___spec__1(x_9, x_5);
lean_dec(x_5);
if (lean_obj_tag(x_10) == 0)
x_9 = l_Lean_SMap_find_x3f___at_Lean_Elab_getMacros___spec__1(x_8, x_4);
lean_dec(x_4);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_11; lean_object* x_12;
lean_object* x_10;
lean_dec(x_3);
lean_dec(x_2);
x_11 = lean_box(1);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_4);
return x_12;
x_10 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1;
return x_10;
}
else
{
lean_object* x_13; lean_object* x_14;
x_13 = lean_ctor_get(x_10, 0);
lean_inc(x_13);
lean_dec(x_10);
x_14 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_2, x_13, x_3, x_4);
return x_14;
lean_object* x_11; lean_object* x_12;
x_11 = lean_ctor_get(x_9, 0);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l___private_Init_Lean_Elab_Util_7__expandMacroFns___main(x_2, x_11, x_3);
return x_12;
}
}
}
@ -5898,132 +5895,90 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_getMacros___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Elab_getMacros___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_getMacros(x_1, x_2, x_3, x_4);
lean_object* x_4;
x_4 = l_Lean_Elab_getMacros(x_1, x_2, x_3);
lean_dec(x_1);
return x_5;
return x_4;
}
}
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_1, 4);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_6, 0, x_2);
x_7 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_7, 0, x_6);
x_8 = lean_apply_3(x_5, lean_box(0), x_3, x_7);
return x_8;
}
}
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_environment_main_module(x_6);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_1);
lean_inc(x_3);
x_9 = lean_apply_2(x_2, x_3, x_8);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_environment_main_module(x_1);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_2);
lean_inc(x_4);
x_11 = lean_apply_3(x_3, x_4, x_10, x_8);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
lean_dec(x_4);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = lean_ctor_get(x_5, 3);
lean_inc(x_14);
lean_object* x_10;
lean_dec(x_5);
x_15 = lean_apply_1(x_14, x_13);
x_16 = lean_alloc_closure((void*)(l_finally___rarg___lambda__1___boxed), 3, 2);
lean_closure_set(x_16, 0, x_6);
lean_closure_set(x_16, 1, x_12);
x_17 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_15, x_16);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
lean_dec(x_10);
x_12 = lean_ctor_get(x_4, 2);
lean_inc(x_12);
lean_dec(x_4);
x_13 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_13, 0, x_11);
x_14 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_14, 0, x_13);
x_15 = lean_apply_3(x_12, lean_box(0), x_3, x_14);
return x_15;
}
else
{
lean_object* x_16; lean_object* x_17;
lean_dec(x_3);
x_16 = lean_ctor_get(x_4, 3);
lean_inc(x_16);
lean_dec(x_4);
x_17 = lean_apply_1(x_16, lean_box(0));
return x_17;
}
else
{
lean_object* x_18;
lean_dec(x_6);
x_18 = lean_ctor_get(x_11, 0);
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; lean_object* x_23; lean_object* x_24;
x_19 = lean_ctor_get(x_11, 1);
lean_inc(x_19);
lean_dec(x_11);
x_20 = lean_ctor_get(x_18, 0);
lean_inc(x_20);
lean_dec(x_18);
x_21 = lean_ctor_get(x_5, 3);
lean_inc(x_21);
x_22 = lean_apply_1(x_21, x_19);
x_23 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__1___boxed), 4, 3);
lean_closure_set(x_23, 0, x_5);
lean_closure_set(x_23, 1, x_20);
lean_closure_set(x_23, 2, x_4);
x_24 = lean_apply_4(x_7, lean_box(0), lean_box(0), x_22, x_23);
return x_24;
}
else
{
lean_object* x_25; lean_object* x_26;
lean_dec(x_11);
lean_dec(x_7);
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
lean_dec(x_4);
x_25 = lean_ctor_get(x_5, 5);
lean_inc(x_25);
lean_dec(x_3);
x_18 = lean_ctor_get(x_9, 0);
lean_inc(x_18);
lean_dec(x_9);
x_19 = lean_ctor_get(x_5, 0);
lean_inc(x_19);
lean_dec(x_5);
x_26 = lean_apply_1(x_25, lean_box(0));
return x_26;
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = lean_apply_2(x_20, lean_box(0), x_18);
return x_21;
}
}
}
}
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__3(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:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_ctor_get(x_1, 2);
lean_inc(x_8);
lean_inc(x_6);
x_9 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__2), 8, 7);
lean_closure_set(x_9, 0, x_7);
lean_closure_set(x_9, 1, x_2);
lean_closure_set(x_9, 2, x_3);
lean_closure_set(x_9, 3, x_4);
lean_closure_set(x_9, 4, x_1);
lean_closure_set(x_9, 5, x_5);
lean_closure_set(x_9, 6, x_6);
x_10 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_8, x_9);
return x_10;
}
}
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__4(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* l_Lean_Elab_adaptMacro___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_1, 0);
lean_inc(x_7);
lean_inc(x_5);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__3), 7, 6);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_6);
lean_closure_set(x_8, 2, x_2);
lean_closure_set(x_8, 3, x_3);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__1), 6, 5);
lean_closure_set(x_8, 0, x_6);
lean_closure_set(x_8, 1, x_2);
lean_closure_set(x_8, 2, x_3);
lean_closure_set(x_8, 3, x_1);
lean_closure_set(x_8, 4, x_4);
lean_closure_set(x_8, 5, x_5);
x_9 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_7, x_8);
return x_9;
}
@ -6037,7 +5992,7 @@ lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_6);
lean_inc(x_5);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__4), 6, 5);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg___lambda__2), 6, 5);
lean_closure_set(x_7, 0, x_2);
lean_closure_set(x_7, 1, x_3);
lean_closure_set(x_7, 2, x_4);
@ -6055,15 +6010,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_adaptMacro___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_adaptMacro___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_adaptMacro___rarg___lambda__1(x_1, x_2, x_3, x_4);
lean_dec(x_4);
return x_5;
}
}
lean_object* l_Lean_Elab_adaptMacro___boxed(lean_object* x_1) {
_start:
{
@ -6274,6 +6220,8 @@ if (lean_io_result_is_error(res)) return res;
l_Lean_Elab_macroAttribute = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Elab_macroAttribute);
lean_dec_ref(res);
l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1 = _init_l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_7__expandMacroFns___main___closed__1);
l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1 = _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1();
lean_mark_persistent(l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__1);
l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2 = _init_l___private_Init_Lean_Elab_Util_8__regTraceClasses___closed__2();

151
stage0/stdlib/Init/LeanInit.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.LeanInit
// Imports: Init.Data.String.Basic Init.Data.Array.Basic Init.Data.UInt Init.Data.Hashable Init.Control.Reader Init.Control.EState
// Imports: Init.Data.String.Basic Init.Data.Array.Basic Init.Data.UInt Init.Data.Hashable Init.Control.Reader Init.Control.Except
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -42,7 +42,7 @@ lean_object* l_Lean_Name_HasAppend;
lean_object* l_Lean_Syntax_identToAtom___boxed(lean_object*);
lean_object* l_Lean_fieldIdxKind___closed__2;
lean_object* l_Lean_ParserDescr_orelse(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object*);
lean_object* l___private_Init_LeanInit_3__extractMainModule(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_8__decodeHexDigit___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_10__decodeDecimalLitAux___main(lean_object*, lean_object*, lean_object*);
@ -114,7 +114,7 @@ lean_object* l_Lean_mkStxNumLit(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
lean_object* l_Lean_Name_HasAppend___closed__1;
uint8_t l_Lean_Name_hasMacroScopes(lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind___closed__4;
lean_object* l_Lean_Syntax_termIdToAntiquot___closed__4;
lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
@ -130,16 +130,15 @@ lean_object* l_Lean_choiceKind___closed__1;
lean_object* l___private_Init_LeanInit_7__decodeOctalLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_choiceKind___closed__2;
lean_object* l_Lean_Macro_mkFreshName___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_num___boxed(lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object*);
lean_object* l_Lean_strLitKind;
lean_object* l_Lean_Syntax_isStrLit_x3f(lean_object*);
lean_object* l_Lean_Macro_mkFreshName(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_getSepElems(lean_object*);
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isFieldIdx_x3f(lean_object*);
lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Macro_addMacroScope(lean_object*, lean_object*);
lean_object* l_Lean_mkTermIdFrom___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getHeadInfo(lean_object*);
lean_object* l_Lean_Name_toString(lean_object*);
@ -211,7 +210,7 @@ uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Syntax_inhabited;
lean_object* l_Lean_mkAppStx___closed__5;
lean_object* l_Lean_mkHole(lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_char___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_4__extractMacroScopesAux___main(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_hasArgs(lean_object*);
@ -275,7 +274,7 @@ lean_object* l_Lean_mkAtomFrom___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_symbol(uint8_t, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_9__decodeHexLitAux(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object*);
uint8_t l_UInt32_decLe(uint32_t, uint32_t);
lean_object* l_Lean_ParserDescr_optional___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__2;
@ -1856,106 +1855,56 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Macro_mkFreshName(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Macro_addMacroScope(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_4; lean_object* x_5; uint8_t x_6;
x_4 = lean_ctor_get(x_2, 0);
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l_Lean_Name_append___main(x_1, x_4);
x_6 = !lean_is_exclusive(x_3);
if (x_6 == 0)
x_5 = l_Lean_addMacroScope(x_3, x_1, x_4);
x_6 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object* x_1) {
_start:
{
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_7 = lean_ctor_get(x_3, 0);
x_8 = lean_ctor_get(x_3, 1);
lean_inc(x_8);
lean_inc(x_7);
x_9 = lean_name_mk_numeral(x_7, x_8);
x_10 = l_Lean_Name_append___main(x_5, x_9);
lean_dec(x_5);
x_11 = lean_unsigned_to_nat(1u);
x_12 = lean_nat_add(x_8, x_11);
lean_dec(x_8);
lean_ctor_set(x_3, 1, x_12);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_10);
lean_ctor_set(x_13, 1, x_3);
return x_13;
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_3 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_3, 0, x_2);
return x_3;
}
else
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object* x_1) {
_start:
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_14 = lean_ctor_get(x_3, 0);
x_15 = lean_ctor_get(x_3, 1);
lean_inc(x_15);
lean_inc(x_14);
lean_dec(x_3);
lean_inc(x_15);
lean_inc(x_14);
x_16 = lean_name_mk_numeral(x_14, x_15);
x_17 = l_Lean_Name_append___main(x_5, x_16);
lean_dec(x_5);
x_18 = lean_unsigned_to_nat(1u);
x_19 = lean_nat_add(x_15, x_18);
lean_dec(x_15);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_14);
lean_ctor_set(x_20, 1, x_19);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_17);
lean_ctor_set(x_21, 1, x_20);
return x_21;
lean_object* x_2; lean_object* x_3;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_3, 0, x_2);
return x_3;
}
}
}
lean_object* l_Lean_Macro_mkFreshName___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Macro_mkFreshName(x_1, x_2, x_3);
lean_dec(x_1);
x_4 = lean_apply_1(x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
x_4 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
return x_4;
}
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__2(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
x_4 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
return x_4;
}
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_apply_2(x_2, x_3, x_4);
return x_5;
}
}
lean_object* _init_l_Lean_MacroM_monadQuotation___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__1___boxed), 2, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__1___boxed), 1, 0);
return x_1;
}
}
@ -1963,7 +1912,7 @@ lean_object* _init_l_Lean_MacroM_monadQuotation___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__2___boxed), 2, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__2___boxed), 1, 0);
return x_1;
}
}
@ -1971,7 +1920,7 @@ lean_object* _init_l_Lean_MacroM_monadQuotation___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__3), 4, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_MacroM_monadQuotation___lambda__3), 3, 0);
return x_1;
}
}
@ -1997,22 +1946,22 @@ x_1 = l_Lean_MacroM_monadQuotation___closed__4;
return x_1;
}
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object* x_1) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_MacroM_monadQuotation___lambda__1(x_1, x_2);
lean_object* x_2;
x_2 = l_Lean_MacroM_monadQuotation___lambda__1(x_1);
lean_dec(x_1);
return x_3;
return x_2;
}
}
lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_MacroM_monadQuotation___lambda__2___boxed(lean_object* x_1) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_MacroM_monadQuotation___lambda__2(x_1, x_2);
lean_object* x_2;
x_2 = l_Lean_MacroM_monadQuotation___lambda__2(x_1);
lean_dec(x_1);
return x_3;
return x_2;
}
}
lean_object* _init_l_Lean_choiceKind___closed__1() {
@ -4587,7 +4536,7 @@ lean_object* initialize_Init_Data_Array_Basic(lean_object*);
lean_object* initialize_Init_Data_UInt(lean_object*);
lean_object* initialize_Init_Data_Hashable(lean_object*);
lean_object* initialize_Init_Control_Reader(lean_object*);
lean_object* initialize_Init_Control_EState(lean_object*);
lean_object* initialize_Init_Control_Except(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_LeanInit(lean_object* w) {
lean_object * res;
@ -4608,7 +4557,7 @@ lean_dec_ref(res);
res = initialize_Init_Control_Reader(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Control_EState(lean_io_mk_world());
res = initialize_Init_Control_Except(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Name_inhabited = _init_l_Lean_Name_inhabited();