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-02-01 01:04:38 -08:00
parent a370eb3167
commit 460dcfec19
13 changed files with 6465 additions and 7733 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -207,18 +207,19 @@ partial def elabCommand : Syntax → CommandElabM Unit
else do
trace `Elab.step stx $ fun _ => stx;
s ← get;
let table := (commandElabAttribute.ext.getState s.env).table;
let k := stx.getKind;
match table.find? k with
| some elabFns => elabCommandUsing s stx elabFns
| none => do
env ← getEnv;
stx' ← catch
(adaptMacro (getMacros env) stx)
stxNew? ← catch
(do newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx))
(fun ex => match ex with
| Exception.unsupportedSyntax => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
| Exception.unsupportedSyntax => pure none
| _ => throw ex);
withMacroExpansion stx stx' $ elabCommand stx'
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabCommand stxNew
| _ => do
let table := (commandElabAttribute.ext.getState s.env).table;
let k := stx.getKind;
match table.find? k with
| some elabFns => elabCommandUsing s stx elabFns
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
| _ => throwError stx "unexpected command"
/-- Adapt a syntax transformation to a regular, command-producing elaborator. -/

21
stage0/src/Init/Lean/Elab/DoNotation.lean
View file

@ -50,7 +50,7 @@ private partial def hasLiftMethod : Syntax → Bool
else args.any hasLiftMethod
| _ => false
private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) TermElabM Syntax
private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) MacroM Syntax
| stx@(Syntax.node k args) =>
if k == `Lean.Parser.Term.do then pure stx
else if k == `Lean.Parser.Term.liftMethod then withFreshMacroScope $ do
@ -65,7 +65,7 @@ private partial def expandLiftMethodAux : Syntax → StateT (Array Syntax) TermE
pure $ Syntax.node k args
| stx => pure stx
private def expandLiftMethod (stx : Syntax) : TermElabM (Option (Array Syntax)) :=
private def expandLiftMethod (stx : Syntax) : MacroM (Option (Array Syntax)) :=
if hasLiftMethod stx then do
(stx, doElems) ← (expandLiftMethodAux stx).run #[];
let doElems := doElems.push stx;
@ -74,16 +74,16 @@ else
pure none
/- Expand `doLet`, `doPat`, nonterminal `doExpr`s, and `liftMethod` -/
private partial def expandDoElems : Bool → Array Syntax → Nat → TermElabM (Option Syntax)
private partial def expandDoElemsAux : Bool → Array Syntax → Nat → MacroM (Option Syntax)
| modified, doElems, i =>
let mkRest : Unit → TermElabM Syntax := fun _ => do {
let mkRest : Unit → MacroM Syntax := fun _ => do {
let restElems := doElems.extract (i+2) doElems.size;
if restElems.size == 1 then
pure $ (restElems.get! 0).getArg 0
else
`(do { $restElems* })
};
let addPrefix (rest : Syntax) : TermElabM (Option Syntax) := do {
let addPrefix (rest : Syntax) : MacroM (Option Syntax) := do {
if i == 0 then
pure rest
else
@ -100,7 +100,7 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → TermElabM
let pre := doElems.extract 0 i;
let doElems := pre ++ doElemsNew ++ post;
tmp ← `(do { $doElems* });
expandDoElems true doElems i
expandDoElemsAux true doElems i
| none =>
if doElem.getKind == `Lean.Parser.Term.doLet then do
let letDecl := doElem.getArg 1;
@ -126,14 +126,17 @@ private partial def expandDoElems : Bool → Array Syntax → Nat → TermElabM
auxDo ← `(do x ← $term; $(Syntax.missing));
let doElemNew := (getDoElems auxDo).get! 0;
let doElems := doElems.set! i doElemNew;
expandDoElems true doElems (i+2)
expandDoElemsAux true doElems (i+2)
else
expandDoElems modified doElems (i+2)
expandDoElemsAux modified doElems (i+2)
else if modified then
`(do { $doElems* })
else
pure none
private partial def expandDoElems (doElems : Array Syntax) : MacroM (Option Syntax) :=
expandDoElemsAux false doElems 0
private def ensureDoElemType (ref : Syntax) (expectedMonad : Expr) (expectedType : Expr) (val : Expr) : TermElabM Expr := do
-- TODO: try MonadLift
ensureHasType ref expectedType val
@ -215,7 +218,7 @@ fun stx expectedType? => do
let ref := stx;
tryPostponeIfNoneOrMVar expectedType?;
let doElems := getDoElems stx;
stxNew? ← expandDoElems false doElems 0;
stxNew? ← liftMacroM $ expandDoElems doElems;
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabTerm stxNew expectedType?
| none => do

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

@ -480,18 +480,19 @@ partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone := true)
| stx => withFreshMacroScope $ withIncRecDepth stx $ do
trace `Elab.step stx $ fun _ => stx;
s ← get;
let table := (termElabAttribute.ext.getState s.env).table;
let k := stx.getKind;
match table.find? k with
| some elabFns => elabTermUsing s stx expectedType? catchExPostpone elabFns
| none => do
env ← getEnv;
stx' ← catch
(adaptMacro (getMacros env) stx)
(fun ex => match ex with
| Exception.ex Elab.Exception.unsupportedSyntax => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
| _ => throw ex);
withMacroExpansion stx stx' $ elabTermAux stx'
stxNew? ← catch
(do newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx))
(fun ex => match ex with
| Exception.ex Elab.Exception.unsupportedSyntax => pure none
| _ => throw ex);
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew $ elabTermAux stxNew
| _ =>
let table := (termElabAttribute.ext.getState s.env).table;
let k := stx.getKind;
match table.find? k with
| some elabFns => elabTermUsing s stx expectedType? catchExPostpone elabFns
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
/--
Main function for elaborating terms.

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

@ -231,14 +231,17 @@ class MonadMacroAdapter (m : Type → Type) :=
(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
@[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : MacroM α) : m α := do
scp ← MonadMacroAdapter.getCurrMacroScope;
env ← MonadMacroAdapter.getEnv;
next ← MonadMacroAdapter.getNextMacroScope;
match x stx { currMacroScope := scp, mainModule := env.mainModule } next with
match x { currMacroScope := scp, mainModule := env.mainModule } next with
| EStateM.Result.error Macro.Exception.unsupportedSyntax _ => MonadMacroAdapter.throwUnsupportedSyntax
| EStateM.Result.error (Macro.Exception.error msg) _ => MonadMacroAdapter.throwError stx msg
| EStateM.Result.ok stx nextMacroScope => do MonadMacroAdapter.setNextMacroScope nextMacroScope; pure stx
| EStateM.Result.error (Macro.Exception.error ref msg) _ => MonadMacroAdapter.throwError ref msg
| EStateM.Result.ok a nextMacroScope => do MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : Macro) (stx : Syntax) : m Syntax :=
liftMacroM (x stx)
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab;

5
stage0/src/Init/Lean/Hygiene.lean
View file

@ -36,9 +36,4 @@ instance MonadQuotation : MonadQuotation Unhygienic := {
protected def run {α : Type} (x : Unhygienic α) : α := run x firstFrontendMacroScope (firstFrontendMacroScope+1)
end Unhygienic
instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
{ getCurrMacroScope := liftM (getCurrMacroScope : m MacroScope),
getMainModule := liftM (getMainModule : m Name),
withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }
end Lean

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

@ -366,7 +366,7 @@ structure Context :=
(currMacroScope : MacroScope)
inductive Exception
| error : String → Exception
| error : Syntax → String → Exception
| unsupportedSyntax : Exception
end Macro
@ -380,6 +380,9 @@ pure $ Lean.addMacroScope ctx.mainModule n ctx.currMacroScope
def Macro.throwUnsupported {α} : MacroM α :=
throw Macro.Exception.unsupportedSyntax
def Macro.throwError {α} (ref : Syntax) (msg : String) : MacroM α :=
throw $ Macro.Exception.error ref msg
@[inline] protected def Macro.withFreshMacroScope {α} (x : MacroM α) : MacroM α := do
fresh ← modifyGet (fun s => (s, s+1));
adaptReader (fun (ctx : Macro.Context) => { currMacroScope := fresh, .. ctx }) x
@ -389,6 +392,11 @@ instance MacroM.monadQuotation : MonadQuotation MacroM :=
getMainModule := fun ctx => pure ctx.mainModule,
withFreshMacroScope := @Macro.withFreshMacroScope }
instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
{ getCurrMacroScope := liftM (getCurrMacroScope : m MacroScope),
getMainModule := liftM (getMainModule : m Name),
withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }
abbrev Macro := Syntax → MacroM Syntax
/- Helper functions for processing Syntax programmatically -/

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

File diff suppressed because it is too large Load diff

6229
stage0/stdlib/Init/Lean/Elab/DoNotation.c
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

@ -63,6 +63,7 @@ lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_getMacros___spec__1___boxed(lea
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabFnTable_insert___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_HashMapImp_moveEntries___main___at_Lean_Elab_ElabFnTable_insert___spec__17(lean_object*);
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_ElabFnTable_insert___spec__2(lean_object*);
lean_object* l___private_Init_Lean_Elab_Util_8__regTraceClasses(lean_object*);
@ -112,6 +113,7 @@ lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
extern lean_object* l_Lean_mkAttributeImplOfConstant___closed__1;
lean_object* l_Lean_Elab_macroAttribute___closed__5;
lean_object* l_Lean_Elab_liftMacroM___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKind___closed__2;
lean_object* l___private_Init_Lean_Elab_Util_3__mkElabFnOfConstantUnsafe___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__5;
@ -141,6 +143,7 @@ lean_object* l_finally___rarg___lambda__1___boxed(lean_object*, lean_object*, le
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;
lean_object* l_Lean_Elab_liftMacroM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3(lean_object*);
lean_object* l_PersistentHashMap_find_x3f___at_Lean_Elab_getMacros___spec__2___boxed(lean_object*, lean_object*);
@ -175,6 +178,7 @@ lean_object* l_List_foldl___main___at_Lean_Elab_addMacroStack___spec__1___closed
lean_object* lean_eval_const(lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinMacroAttr___lambda__1___closed__3;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Elab_mkElabAttributeAux___spec__3___rarg___closed__2;
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__3(lean_object*, 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*, 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;
@ -200,6 +204,7 @@ lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean
lean_object* l_Lean_SMap_empty___at_Lean_Elab_mkBuiltinMacroFnTable___spec__1___closed__1;
size_t l_USize_mul(size_t, size_t);
lean_object* l_List_redLength___main___rarg(lean_object*);
lean_object* l_Lean_Elab_liftMacroM(lean_object*, lean_object*);
lean_object* l_Lean_Elab_addMacroStack___closed__1;
lean_object* l_mkHashMapImp___rarg(lean_object*);
lean_object* l_Lean_Elab_syntaxNodeKindOfAttrParam___closed__3;
@ -340,6 +345,7 @@ lean_object* l_PersistentHashMap_empty___at_Lean_Elab_mkElabAttributeAux___spec_
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1___closed__3;
lean_object* l_Lean_Elab_builtinMacroFnTable;
lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1___closed__2;
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkAppStx___closed__2;
lean_object* l_Lean_Elab_mkMacroAttribute___closed__1;
lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
@ -6596,6 +6602,141 @@ lean_dec(x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_liftMacroM___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, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_environment_main_module(x_1);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_2);
x_10 = lean_apply_2(x_3, x_9, x_7);
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; lean_object* x_16;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = lean_ctor_get(x_4, 3);
lean_inc(x_13);
lean_dec(x_4);
x_14 = lean_apply_1(x_13, x_12);
x_15 = lean_alloc_closure((void*)(l_finally___rarg___lambda__1___boxed), 3, 2);
lean_closure_set(x_15, 0, x_5);
lean_closure_set(x_15, 1, x_11);
x_16 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_14, x_15);
return x_16;
}
else
{
lean_object* x_17;
lean_dec(x_6);
lean_dec(x_5);
x_17 = lean_ctor_get(x_10, 0);
lean_inc(x_17);
lean_dec(x_10);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = lean_ctor_get(x_4, 4);
lean_inc(x_20);
lean_dec(x_4);
x_21 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_21, 0, x_19);
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_21);
x_23 = lean_apply_3(x_20, lean_box(0), x_18, x_22);
return x_23;
}
else
{
lean_object* x_24; lean_object* x_25;
x_24 = lean_ctor_get(x_4, 5);
lean_inc(x_24);
lean_dec(x_4);
x_25 = lean_apply_1(x_24, lean_box(0));
return x_25;
}
}
}
}
lean_object* l_Lean_Elab_liftMacroM___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, 2);
lean_inc(x_7);
lean_inc(x_5);
x_8 = lean_alloc_closure((void*)(l_Lean_Elab_liftMacroM___rarg___lambda__1), 7, 6);
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;
}
}
lean_object* l_Lean_Elab_liftMacroM___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_inc(x_4);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_liftMacroM___rarg___lambda__2), 6, 5);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, x_5);
lean_closure_set(x_7, 2, x_2);
lean_closure_set(x_7, 3, x_3);
lean_closure_set(x_7, 4, x_4);
x_8 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_6, x_7);
return x_8;
}
}
lean_object* l_Lean_Elab_liftMacroM___rarg(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;
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_inc(x_4);
x_6 = lean_alloc_closure((void*)(l_Lean_Elab_liftMacroM___rarg___lambda__3), 5, 4);
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_3);
lean_closure_set(x_6, 2, x_1);
lean_closure_set(x_6, 3, x_4);
x_7 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_5, x_6);
return x_7;
}
}
lean_object* l_Lean_Elab_liftMacroM(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_Elab_liftMacroM___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Lean_Elab_liftMacroM___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Elab_liftMacroM(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
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, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -6604,12 +6745,10 @@ 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);
@ -6635,29 +6774,30 @@ lean_inc(x_18);
lean_dec(x_11);
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_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_18, 0);
lean_inc(x_19);
lean_dec(x_18);
x_20 = lean_ctor_get(x_5, 4);
x_20 = lean_ctor_get(x_18, 1);
lean_inc(x_20);
lean_dec(x_18);
x_21 = lean_ctor_get(x_5, 4);
lean_inc(x_21);
lean_dec(x_5);
x_21 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_21, 0, x_19);
x_22 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_22, 0, x_21);
x_23 = lean_apply_3(x_20, lean_box(0), x_4, x_22);
return x_23;
x_22 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_22, 0, x_20);
x_23 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_23, 0, x_22);
x_24 = lean_apply_3(x_21, lean_box(0), x_19, x_23);
return x_24;
}
else
{
lean_object* x_24; lean_object* x_25;
lean_dec(x_4);
x_24 = lean_ctor_get(x_5, 5);
lean_inc(x_24);
lean_object* x_25; lean_object* x_26;
x_25 = lean_ctor_get(x_5, 5);
lean_inc(x_25);
lean_dec(x_5);
x_25 = lean_apply_1(x_24, lean_box(0));
return x_25;
x_26 = lean_apply_1(x_25, lean_box(0));
return x_26;
}
}
}

65
stage0/stdlib/Init/Lean/Hygiene.c
View file

@ -17,22 +17,17 @@ lean_object* l_Lean_Unhygienic_MonadQuotation___lambda__1___boxed(lean_object*,
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__3;
lean_object* l_Lean_Unhygienic_run(lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__5;
lean_object* l_Lean_monadQuotationTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__6;
lean_object* l_Lean_Unhygienic_run___rarg(lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__4;
lean_object* l_Lean_monadQuotationTrans(lean_object*, lean_object*);
lean_object* l_ReaderT_read___at_Lean_Unhygienic_MonadQuotation___spec__1(lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_firstFrontendMacroScope;
lean_object* l_Lean_monadQuotationTrans___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation;
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__1;
lean_object* l_ReaderT_pure___at_Lean_Unhygienic_MonadQuotation___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Unhygienic_MonadQuotation___closed__2;
lean_object* l_ReaderT_pure___at_Lean_Unhygienic_MonadQuotation___spec__2(lean_object*);
lean_object* l_Lean_Unhygienic_run___rarg___closed__1;
@ -190,66 +185,6 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Unhygienic_run___rarg), 1, 0);
return x_2;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_1, 2);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_2(x_4, lean_box(0), x_3);
return x_5;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__2(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;
x_5 = lean_alloc_closure((void*)(l_Lean_monadQuotationTrans___rarg___lambda__1), 3, 1);
lean_closure_set(x_5, 0, x_1);
x_6 = lean_apply_3(x_2, lean_box(0), x_5, x_4);
return x_6;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg(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;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_inc(x_2);
x_5 = lean_apply_2(x_2, lean_box(0), x_4);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
x_7 = lean_apply_2(x_2, lean_box(0), x_6);
x_8 = lean_alloc_closure((void*)(l_Lean_monadQuotationTrans___rarg___lambda__2), 4, 2);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_3);
x_9 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_9, 0, x_5);
lean_ctor_set(x_9, 1, x_7);
lean_ctor_set(x_9, 2, x_8);
return x_9;
}
}
lean_object* l_Lean_monadQuotationTrans(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_monadQuotationTrans___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Lean_monadQuotationTrans___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_monadQuotationTrans(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init_Control(lean_object*);
lean_object* initialize_Init_LeanInit(lean_object*);
lean_object* initialize_Init_Lean_Syntax(lean_object*);

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

@ -109,6 +109,7 @@ lean_object* l_Lean_mkAppStx___closed__4;
lean_object* l_Array_filterSepElems___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkIdentFrom___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_decodeStrLitAux___main___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited;
lean_object* l_Lean_mkTermIdFromIdent___closed__1;
lean_object* l_Lean_nameLitKind;
@ -123,6 +124,7 @@ lean_object* l___private_Init_LeanInit_4__extractMainModule___main(lean_object*,
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1(lean_object*);
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l_Array_foldlStepMAux___main___at_Array_getSepElems___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind___closed__2;
lean_object* l_Lean_Syntax_getKind___closed__1;
lean_object* l_Lean_Name_hashable;
@ -185,7 +187,9 @@ lean_object* l_Array_getSepElems___rarg(lean_object*);
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___boxed(lean_object*);
lean_object* l_Lean_reservedMacroScope;
lean_object* l___private_Init_LeanInit_10__decodeDecimalLitAux___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Macro_throwError(lean_object*);
lean_object* l_Lean_mkNullNode(lean_object*);
lean_object* l_Lean_monadQuotationTrans(lean_object*, lean_object*);
lean_object* l_Lean_strLitKind___closed__2;
lean_object* l_Lean_NameGenerator_Inhabited___closed__1;
size_t l_Lean_Name_hash(lean_object*);
@ -216,6 +220,7 @@ lean_object* l_Lean_Syntax_isCharLit_x3f___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_2__assembleParts(lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_nullKind___closed__1;
lean_object* l_Lean_monadQuotationTrans___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_decodeStrLit___boxed(lean_object*);
lean_object* l_Lean_addMacroScope(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isIdEndEscape(uint32_t);
@ -240,12 +245,15 @@ lean_object* l_Lean_identKind;
lean_object* l_Lean_mkCTermId(lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Syntax_inhabited;
lean_object* l_Lean_Macro_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__5;
lean_object* l_Lean_Macro_throwError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkHole(lean_object*);
lean_object* l_Lean_MacroM_monadQuotation___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_3__extractImported(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_5__extractMacroScopesAux___main(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_hasArgs(lean_object*);
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_String_quote(lean_object*);
uint8_t l_Char_isAlphanum(uint32_t);
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar(lean_object*, lean_object*);
@ -2661,6 +2669,36 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_Macro_throwError___rarg(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;
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_2);
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;
}
}
lean_object* l_Lean_Macro_throwError(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Macro_throwError___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Macro_throwError___rarg___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_Macro_throwError___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
return x_5;
}
}
lean_object* l_Lean_Macro_withFreshMacroScope___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -2787,6 +2825,66 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_1, 2);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_apply_2(x_4, lean_box(0), x_3);
return x_5;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg___lambda__2(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;
x_5 = lean_alloc_closure((void*)(l_Lean_monadQuotationTrans___rarg___lambda__1), 3, 1);
lean_closure_set(x_5, 0, x_1);
x_6 = lean_apply_3(x_2, lean_box(0), x_5, x_4);
return x_6;
}
}
lean_object* l_Lean_monadQuotationTrans___rarg(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;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_inc(x_2);
x_5 = lean_apply_2(x_2, lean_box(0), x_4);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
x_7 = lean_apply_2(x_2, lean_box(0), x_6);
x_8 = lean_alloc_closure((void*)(l_Lean_monadQuotationTrans___rarg___lambda__2), 4, 2);
lean_closure_set(x_8, 0, x_1);
lean_closure_set(x_8, 1, x_3);
x_9 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_9, 0, x_5);
lean_ctor_set(x_9, 1, x_7);
lean_ctor_set(x_9, 2, x_8);
return x_9;
}
}
lean_object* l_Lean_monadQuotationTrans(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_monadQuotationTrans___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Lean_monadQuotationTrans___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_monadQuotationTrans(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_mkIdentFrom(lean_object* x_1, lean_object* x_2) {
_start:
{