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-12 11:30:15 -08:00
parent d15f3431dc
commit 783460af4b
24 changed files with 22802 additions and 11725 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
stage0/src/Init/Lean/Elab/App.lean
View file

@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Elab.Term
import Init.Lean.Elab.Binders
namespace Lean
namespace Elab
@ -185,11 +186,20 @@ unless (ctx.explicit || ctx.foundExplicit || ctx.typeMVars.isEmpty) $ do
isDefEq ctx.ref expectedType eTypeBody;
pure ()
private def nextArgIsHole (ctx : ElabAppArgsCtx) : Bool :=
if h : ctx.argIdx < ctx.args.size then
match ctx.args.get ⟨ctx.argIdx, h⟩ with
| Arg.stx (Syntax.node `Lean.Parser.Term.hole _) => true
| _ => false
else
false
/- Elaborate function application arguments. -/
private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermElabM Expr
| ctx, e, eType => do
let finalize : Unit → TermElabM Expr := fun _ => do {
-- all user explicit arguments have been consumed
trace `Elab.app.finalize ctx.ref $ fun _ => e;
match ctx.expectedType? with
| none => pure ()
| some expectedType => do {
@ -226,16 +236,26 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
else
throwError ctx.ref ("explicit parameter '" ++ n ++ "' is missing, unused named arguments " ++ toString (ctx.namedArgs.map $ fun narg => narg.name))
};
if ctx.explicit then
processExplictArg ()
else match c.binderInfo with
| BinderInfo.implicit => do
a ← mkFreshExprMVar ctx.ref d;
typeMVars ← condM (isType ctx.ref a) (pure $ ctx.typeMVars.push a.mvarId!) (pure ctx.typeMVars);
elabAppArgsAux { typeMVars := typeMVars, .. ctx } (mkApp e a) (b.instantiate1 a)
| BinderInfo.instImplicit => do
a ← mkFreshExprMVar ctx.ref d MetavarKind.synthetic;
elabAppArgsAux { instMVars := ctx.instMVars.push a.mvarId!, .. ctx } (mkApp e a) (b.instantiate1 a)
match c.binderInfo with
| BinderInfo.implicit =>
if ctx.explicit then
processExplictArg ()
else do
a ← mkFreshExprMVar ctx.ref d;
typeMVars ← condM (isTypeFormer ctx.ref a) (pure $ ctx.typeMVars.push a.mvarId!) (pure ctx.typeMVars);
elabAppArgsAux { typeMVars := typeMVars, .. ctx } (mkApp e a) (b.instantiate1 a)
| BinderInfo.instImplicit =>
if ctx.explicit && nextArgIsHole ctx then do
/- Recall that if '@' has been used, and the argument is '_', then we still use
type class resolution -/
a ← mkFreshExprMVar ctx.ref d MetavarKind.synthetic;
elabAppArgsAux { argIdx := ctx.argIdx + 1, instMVars := ctx.instMVars.push a.mvarId!, .. ctx } (mkApp e a) (b.instantiate1 a)
else if ctx.explicit then
processExplictArg ()
else do
a ← mkFreshExprMVar ctx.ref d MetavarKind.synthetic;
elabAppArgsAux { instMVars := ctx.instMVars.push a.mvarId!, .. ctx } (mkApp e a) (b.instantiate1 a)
| _ =>
processExplictArg ()
| _ =>
@ -250,6 +270,7 @@ private def elabAppArgs (ref : Syntax) (f : Expr) (namedArgs : Array NamedArg) (
(expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
fType ← inferType ref f;
fType ← instantiateMVars ref fType;
trace `Elab.app.args ref $ fun _ => "explicit: " ++ toString explicit ++ ", " ++ f ++ " : " ++ fType;
tryPostponeIfMVar fType;
elabAppArgsAux {ref := ref, args := args, expectedType? := expectedType?, explicit := explicit, namedArgs := namedArgs } f fType
@ -460,8 +481,6 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
else if f.getKind == choiceKind then
f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit acc) acc
else match_syntax f with
| `(@$id:id) =>
elabAppFn id lvals namedArgs args expectedType? true acc
| `($(e).$idx:fieldIdx) =>
let idx := idx.isFieldIdx?.get!;
elabAppFn (f.getArg 0) (LVal.fieldIdx idx :: lvals) namedArgs args expectedType? explicit acc
@ -474,6 +493,17 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
-- Remark: `id.<namedPattern>` should already have been expanded
us ← if us.isEmpty then pure [] else elabExplicitUniv (us.get! 0);
elabAppFnId ref id us lvals namedArgs args expectedType? explicit acc
| `(@($f:fun)) => do
s ← observing $ do {
if lvals.isEmpty && namedArgs.isEmpty && args.isEmpty then
elabFunCore f expectedType? true
else do
f ← elabFunCore f none true;
elabAppLVals ref f lvals namedArgs args expectedType? true
};
pure $ acc.push s
| `(@$f) =>
elabAppFn f lvals namedArgs args expectedType? true acc
| _ => do
s ← observing $ do {
f ← elabTerm f none;
@ -557,6 +587,11 @@ fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/
@[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom
@[builtinTermElab «fun»] def elabFun : TermElab :=
fun stx expectedType? => do
f ← elabFunCore stx expectedType? false;
elabAppArgs stx f #[] #[] none false
@[builtinTermElab sortApp] def elabSortApp : TermElab :=
fun stx _ => do
u ← elabLevel (stx.getArg 1);

86
stage0/src/Init/Lean/Elab/Binders.lean
View file

@ -9,6 +9,7 @@ import Init.Lean.Elab.Term
namespace Lean
namespace Elab
namespace Term
/--
Given syntax of the forms
a) (`:` term)?
@ -236,19 +237,82 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
We update the `body` syntax when expanding the pattern notation.
Example: `fun (a, b) => a + b` expands into `fun _a_1 => match _a_1 with | (a, b) => a + b`.
See local function `processAsPattern` at `expandFunBindersAux`. -/
private def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElabM (Array Syntax × Syntax) :=
def expandFunBinders (binders : Array Syntax) (body : Syntax) : TermElabM (Array Syntax × Syntax) :=
expandFunBindersAux binders body 0 #[]
@[builtinTermElab «fun»] def elabFun : TermElab :=
fun stx expectedType? => do
-- `fun` term+ `=>` term
let binders := (stx.getArg 1).getArgs;
let body := stx.getArg 3;
(binders, body) ← expandFunBinders binders body;
elabBinders binders $ fun xs => do
-- TODO: expected type
e ← elabTerm body none;
mkLambda stx xs e
namespace FunBinders
structure State :=
(implicitArgs : Array Expr := #[])
(fvars : Array Expr := #[])
(lctx : LocalContext)
(localInsts : LocalInstances)
(expectedType? : Option Expr := none)
(explicit : Bool := false)
private def propagateExpectedType (ref : Syntax) (fvar : Expr) (fvarType : Expr) (s : State) : TermElabM State := do
match s.expectedType? with
| none => pure s
| some expectedType => do
expectedType ← whnfForall ref expectedType;
match expectedType with
| Expr.forallE _ d b _ => do
isDefEq ref fvarType d;
let b := b.instantiate1 fvar;
pure { expectedType? := some b, .. s }
| _ => pure { expectedType? := none, .. s }
private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat → State → TermElabM State
| i, s =>
if h : i < binderViews.size then
let binderView := binderViews.get ⟨i, h⟩;
withLCtx s.lctx s.localInsts $ do
type ← elabType binderView.type;
fvarId ← mkFreshFVarId;
let fvar := mkFVar fvarId;
let fvars := s.fvars.push fvar;
-- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
s ← propagateExpectedType binderView.id fvar type s;
className? ← isClass binderView.type type;
match className? with
| none => elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, .. s }
| some className => do
resetSynthInstanceCache;
let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId };
elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, localInsts := localInsts, .. s }
else
pure s
partial def elabFunBindersAux (binders : Array Syntax) : Nat → State → TermElabM State
| i, s =>
if h : i < binders.size then do
binderViews ← matchBinder (binders.get ⟨i, h⟩);
s ← elabFunBinderViews binderViews 0 s;
elabFunBindersAux (i+1) s
else
pure s
end FunBinders
def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (explicit : Bool) (x : Array Expr → Option Expr → TermElabM α) : TermElabM α :=
if binders.isEmpty then x #[] expectedType?
else do
lctx ← getLCtx;
localInsts ← getLocalInsts;
s ← FunBinders.elabFunBindersAux binders 0 { lctx := lctx, localInsts := localInsts, expectedType? := expectedType?, explicit := explicit };
resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) $ withLCtx s.lctx s.localInsts $
x s.fvars s.expectedType?
def elabFunCore (stx : Syntax) (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
-- `fun` term+ `=>` term
let binders := (stx.getArg 1).getArgs;
let body := stx.getArg 3;
(binders, body) ← expandFunBinders binders body;
elabFunBinders binders expectedType? explicit $ fun xs expectedType? => do {
e ← elabTerm body expectedType?;
mkLambda stx xs e
}
/-
Recall that

1
stage0/src/Init/Lean/Elab/Definition.lean
View file

@ -83,6 +83,7 @@ withUsedWhen ref vars xs e dummyExpr cond k
def mkDef (view : DefView) (declName : Name) (explictLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (val : Expr)
: TermElabM (Option Declaration) := do
let ref := view.ref;
Term.synthesizeSyntheticMVars;
val ← Term.ensureHasType view.val type val;
Term.synthesizeSyntheticMVars false;
type ← Term.instantiateMVars ref type;

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

@ -264,6 +264,7 @@ fun ctx s =>
def ppGoal (ref : Syntax) (mvarId : MVarId) : TermElabM Format := liftMetaM ref $ Meta.ppGoal mvarId
def isType (ref : Syntax) (e : Expr) : TermElabM Bool := liftMetaM ref $ Meta.isType e
def isTypeFormer (ref : Syntax) (e : Expr) : TermElabM Bool := liftMetaM ref $ Meta.isTypeFormer e
def isDefEq (ref : Syntax) (t s : Expr) : TermElabM Bool := liftMetaM ref $ Meta.approxDefEq $ Meta.isDefEq t s
def inferType (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.inferType e
def whnf (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.whnf e
@ -737,30 +738,45 @@ partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone := true)
| some elabFns => elabTermUsing s stx expectedType? catchExPostpone elabFns
| none => throwError stx ("elaboration function for '" ++ toString k ++ "' has not been implemented")
/-- Return true with `expectedType` is of the form `{a : α} → β` or `[a : α] → β` -/
def isImplicitForall? (expectedType? : Option Expr) : Option Expr :=
match expectedType? with
| some type@(Expr.forallE _ _ _ c) => if c.binderInfo.isExplicit then none else some type
| _ => none
private def isExplicit (stx : Syntax) : Bool :=
match_syntax stx with
| `(@$f) => true
| _ => false
/-
WIP
def elabImplicitForallAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do
private def isExplicitApp (stx : Syntax) : Bool :=
stx.getKind == `Lean.Parser.Term.app && isExplicit (stx.getArg 0)
/--
Return true with `expectedType` is of the form `{a : α} → β` or `[a : α] → β`, and
`stx` is not `@f` nor `@f arg1 ...` -/
def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : TermElabM (Option Expr) :=
if isExplicit stx || isExplicitApp stx then pure none
else match expectedType? with
| some expectedType => do
expectedType ← whnfForall stx expectedType;
match expectedType with
| Expr.forallE _ _ _ c => pure $ if c.binderInfo.isExplicit then none else some expectedType
| _ => pure $ none
| _ => pure $ none
def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do
body ← elabTermAux expectedType catchExPostpone stx;
mkLambda stx fvars body
-- body ← ensureHasType stx expectedType body;
r ← mkLambda stx fvars body;
trace `Elab.implicitForall stx $ fun _ => r;
pure r
def elabImplicitForall (stx : Syntax) (catchExPostpone : Bool) : Expr → Array Expr → TermElabM Expr
partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) : Expr → Array Expr → TermElabM Expr
| type@(Expr.forallE n d b c), fvars =>
if c.binderInfo.isExplicit then
let type := type.instantiateRev fvars;
elabImplicitForallAux stx catchExPostpone type fvars
else
let d := d.instantiateRev fvars;
withLocalDecl stx n c.binderInfo d $ fun fvar => elabImplicitForall b (fvars.push fvar)
elabImplicitLambdaAux stx catchExPostpone type fvars
else withFreshMacroScope $ do
n ← MonadQuotation.addMacroScope n;
withLocalDecl stx n c.binderInfo d $ fun fvar => do
type ← whnfForall stx (b.instantiate1 fvar);
elabImplicitLambda type (fvars.push fvar)
| type, fvars =>
let type := type.instantiateRev fvars;
elabImplicitForallAux stx catchExPostpone type fvars
-/
elabImplicitLambdaAux stx catchExPostpone type fvars
/--
Main function for elaborating terms.
@ -775,9 +791,10 @@ def elabImplicitForall (stx : Syntax) (catchExPostpone : Bool) : Expr → Array
and returned.
The option `catchExPostpone == false` is used to implement `resumeElabTerm`
to prevent the creation of another synthetic metavariable when resuming the elaboration. -/
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr :=
match isImplicitForall? expectedType? with
| some expectedType => elabTermAux expectedType? catchExPostpone stx -- elabImplicitForall stx catchExPostpone expectedType #[]
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := do
implicit? ← useImplicitLambda? stx expectedType?;
match implicit? with
| some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[]
| none => elabTermAux expectedType? catchExPostpone stx
/-- Adapt a syntax transformation to a regular, term-producing elaborator. -/

125
stage0/src/Init/Lean/Meta/ExprDefEq.lean
View file

@ -369,26 +369,28 @@ let mvarId := mvar.mvarId!;
ctx ← read;
mctx ← getMCtx;
if mvarId == ctx.mvarId then throw Exception.occursCheck
else match mctx.findDecl? mvarId with
| none => throw $ Exception.unknownExprMVar mvarId
| some mvarDecl =>
if ctx.hasCtxLocals then
throw $ Exception.useFOApprox -- It is not a pattern, then we fail and fall back to FO unification
else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then
/- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned.
We "substract" variables being abstracted because we use `elimMVarDeps` -/
pure mvar
else if mvarDecl.depth != mctx.depth || mvarDecl.kind.isSyntheticOpaque then throw $ Exception.readOnlyMVarWithBiggerLCtx mvarId
else if ctx.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then do
mvarType ← check mvarDecl.type;
/- Create an auxiliary metavariable with a smaller context and "checked" type.
Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
a metavariable that we also need to reduce the context. -/
newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
pure newMVar
else
pure mvar
else match mctx.getExprAssignment? mvarId with
| some v => check v
| none => match mctx.findDecl? mvarId with
| none => throw $ Exception.unknownExprMVar mvarId
| some mvarDecl =>
if ctx.hasCtxLocals then
throw $ Exception.useFOApprox -- It is not a pattern, then we fail and fall back to FO unification
else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then
/- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned.
We "substract" variables being abstracted because we use `elimMVarDeps` -/
pure mvar
else if mvarDecl.depth != mctx.depth || mvarDecl.kind.isSyntheticOpaque then throw $ Exception.readOnlyMVarWithBiggerLCtx mvarId
else if ctx.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then do
mvarType ← check mvarDecl.type;
/- Create an auxiliary metavariable with a smaller context and "checked" type.
Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
a metavariable that we also need to reduce the context. -/
newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
modify $ fun s => { mctx := s.mctx.assignExpr mvarId newMVar, .. s };
pure newMVar
else
pure mvar
/-
Auxiliary function used to "fix" subterms of the form `?m x_1 ... x_n` where `x_i`s are free variables,
@ -426,15 +428,16 @@ partial def check : Expr → CheckAssignmentM Expr
args ← args.mapM (visit check);
pure $ mkAppN f args)
(fun ex => match ex with
| Exception.outOfScopeFVar _ => do
eType ← liftMetaM $ inferType e;
mvarType ← check eType;
/- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
Note that `mvarType` may be different from `eType`. -/
newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
condM (liftMetaM $ assignToConstFun f args.size newMVar)
(pure newMVar)
(throw ex)
| Exception.outOfScopeFVar _ =>
condM (liftMetaM $ isDelayedAssigned f.mvarId!) (throw ex) $ do
eType ← liftMetaM $ inferType e;
mvarType ← check eType;
/- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
Note that `mvarType` may be different from `eType`. -/
newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
condM (liftMetaM $ assignToConstFun f args.size newMVar)
(pure newMVar)
(throw ex)
| _ => throw ex)
else do
f ← visit check f;
@ -540,66 +543,10 @@ else do
v ← instantiateMVars v;
checkAssignmentAux mvarId mvarDecl fvars hasCtxLocals v
/-
We try to unify arguments before we try to unify the functions.
The motivation is the following: the universe constraints in
the arguments propagate to the function. -/
private partial def isDefEqFOApprox (f₁ f₂ : Expr) (args₁ args₂ : Array Expr) : Nat → Nat → MetaM Bool
| i₁, i₂ =>
if h : i₂ < args₂.size then
let arg₁ := args₁.get! i₁;
let arg₂ := args₂.get ⟨i₂, h⟩;
condM (isExprDefEqAux arg₁ arg₂)
(isDefEqFOApprox (i₁+1) (i₂+1))
(pure false)
else
isExprDefEqAux f₁ f₂
private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
let vArgs := v.getAppArgs;
if vArgs.isEmpty then
/- ?m a_1 ... a_k =?= t, where t is not an application -/
pure false
else if args.size > vArgs.size then
/-
?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
reduces to
?m a_1 ... a_i =?= f
a_{i+1} =?= b_1
...
a_{i+k} =?= b_k
-/
let f₁ := mkAppRange mvar 0 (args.size - vArgs.size) args;
let i₁ := args.size - vArgs.size;
isDefEqFOApprox f₁ v.getAppFn args vArgs i₁ 0
else if args.size < vArgs.size then
/-
?m a_1 ... a_k =?= f b_1 ... b_i b_{i+1} ... b_{i+k}
reduces to
?m =?= f b_1 ... b_i
a_1 =?= b_{i+1}
...
a_k =?= b_{i+k}
-/
let vFn := mkAppRange v.getAppFn 0 (vArgs.size - args.size) vArgs;
let i₂ := vArgs.size - args.size;
isDefEqFOApprox mvar vFn args vArgs 0 i₂
else
/-
?m a_1 ... a_k =?= f b_1 ... b_k
reduces to
?m =?= f
a_1 =?= b_1
...
a_k =?= b_k
-/
isDefEqFOApprox mvar v.getAppFn args vArgs 0 0
match v with
| Expr.app f a _ => isExprDefEqAux args.back a <&&> isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
| _ => pure false
/-
Auxiliary method for applying first-order unification. It is an approximation.
@ -1033,7 +980,7 @@ pure false
/- Remove unnecessary let-decls -/
private def consumeLet : Expr → Expr
| e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then b else consumeLet b
| e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b
| e => e
partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool

1
stage0/src/Init/Lean/Parser/Command.lean
View file

@ -81,6 +81,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
@[builtinCommandParser] def «universe» := parser! "universe " >> ident
@[builtinCommandParser] def «universes» := parser! "universes " >> many1 ident
@[builtinCommandParser] def check := parser! "#check " >> termParser
@[builtinCommandParser] def check_failure := parser! "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
@[builtinCommandParser] def synth := parser! "#synth " >> termParser
@[builtinCommandParser] def exit := parser! "#exit"
@[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident

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

@ -359,6 +359,11 @@ if n.hasMacroScopes then
else
mkNameNum (mkNameStr (mkNameStr n "_@" ++ mainModule) "_hyg") scp
@[inline] def MonadQuotation.addMacroScope {m : Type → Type} [MonadQuotation m] [Monad m] (n : Name) : m Name := do
mainModule ← getMainModule;
scp ← getCurrMacroScope;
pure $ addMacroScope mainModule n scp
namespace Macro
structure Context :=

13874
stage0/stdlib/Init/Lean/Elab/App.c
View file

File diff suppressed because it is too large Load diff

3035
stage0/stdlib/Init/Lean/Elab/Binders.c
View file

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

@ -14,7 +14,6 @@
extern "C" {
#endif
lean_object* l_Lean_Elab_Term_elabModN___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Term_12__mkPairsAux___main___closed__5;
lean_object* l_Lean_Elab_Term_elabBAnd___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabseqLeft___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getEnv___rarg(lean_object*);
@ -29,6 +28,7 @@ lean_object* l_Lean_Elab_Term_elabAdd___closed__1;
extern lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabModN___closed__1;
lean_object* l_Lean_Elab_Term_elabIff(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__5;
lean_object* l_Lean_Elab_Term_expandIf___closed__3;
extern lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__1;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabGE(lean_object*);
@ -167,6 +167,7 @@ extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabLT___closed__1;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__19;
extern uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabMapConstRev___closed__1;
extern lean_object* l_Lean_Parser_Term_proj___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_add___elambda__1___closed__1;
@ -183,7 +184,6 @@ lean_object* l_Lean_Elab_Term_tryPostponeIfNoneOrMVar(lean_object*, lean_object*
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabModN(lean_object*);
extern lean_object* l_Lean_Parser_Term_div___elambda__1___closed__2;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_expandSubtype(lean_object*);
extern uint8_t l_Lean_Elab_Term_elabParen___closed__4;
lean_object* l_Lean_Elab_Term_expandSubtype___closed__6;
lean_object* lean_array_fget(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__3;
@ -219,6 +219,7 @@ lean_object* l_Lean_Elab_Term_elabseq___closed__3;
extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
extern lean_object* l_Lean_Expr_heq_x3f___closed__2;
lean_object* l_Lean_Elab_Term_elabDiv___closed__2;
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_expandIf___closed__4;
extern lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__1;
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabseq(lean_object*);
@ -244,7 +245,6 @@ lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabOrElse___closed__1;
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__8;
lean_object* l_Lean_Elab_Term_expandIf___closed__9;
lean_object* l_Lean_Elab_Term_elabProd___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinMacro_Lean_Elab_Term_elabPow(lean_object*);
extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_elabMapRev___closed__1;
@ -705,7 +705,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = l_Lean_Elab_Term_elabParen___closed__4;
x_6 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
@ -2015,7 +2015,7 @@ lean_ctor_set(x_53, 1, x_76);
lean_ctor_set(x_53, 0, x_77);
lean_ctor_set(x_3, 8, x_53);
x_78 = 1;
x_79 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_78, x_74, x_3, x_62);
x_79 = l_Lean_Elab_Term_elabTerm(x_74, x_2, x_78, x_3, x_62);
return x_79;
}
else
@ -2066,7 +2066,7 @@ lean_ctor_set_uint8(x_94, sizeof(void*)*10, x_90);
lean_ctor_set_uint8(x_94, sizeof(void*)*10 + 1, x_91);
lean_ctor_set_uint8(x_94, sizeof(void*)*10 + 2, x_92);
x_95 = 1;
x_96 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_95, x_74, x_94, x_62);
x_96 = l_Lean_Elab_Term_elabTerm(x_74, x_2, x_95, x_94, x_62);
return x_96;
}
}
@ -2167,7 +2167,7 @@ lean_ctor_set_uint8(x_130, sizeof(void*)*10, x_124);
lean_ctor_set_uint8(x_130, sizeof(void*)*10 + 1, x_125);
lean_ctor_set_uint8(x_130, sizeof(void*)*10 + 2, x_126);
x_131 = 1;
x_132 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_131, x_113, x_130, x_101);
x_132 = l_Lean_Elab_Term_elabTerm(x_113, x_2, x_131, x_130, x_101);
return x_132;
}
}
@ -4678,7 +4678,7 @@ lean_object* l_Lean_Elab_Term_elabProd(lean_object* x_1, lean_object* x_2, lean_
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l___private_Init_Lean_Elab_Term_12__mkPairsAux___main___closed__5;
x_4 = l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__5;
x_5 = l_Lean_Elab_Term_elabInfixOp(x_4, x_1, x_2, x_3);
return x_5;
}

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

@ -179,6 +179,7 @@ lean_object* l_Lean_Elab_Command_Lean_Elab_MonadMacroAdapter___closed__1;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
lean_object* l_Lean_Elab_Command_State_inhabited___closed__1;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
lean_object* l_Lean_Elab_Command_declareBuiltinCommandElab___closed__4;
lean_object* l___private_Init_Data_Array_QSort_1__partitionAux___main___at_Lean_Elab_Command_sortDeclLevelParams___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -199,7 +200,6 @@ lean_object* l_Lean_Elab_Command_Lean_Elab_MonadMacroAdapter___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Term_10__elabTermUsing___main___closed__3;
lean_object* l_Lean_Elab_Command_mkBuiltinCommandElabTable(lean_object*);
lean_object* l_Lean_Elab_Command_addOpenDecl(lean_object*, lean_object*, lean_object*);
extern uint8_t l_Lean_Elab_Term_elabParen___closed__4;
extern lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariables___closed__3;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__9;
@ -249,6 +249,7 @@ lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getPos___at_Lean_Elab_Command_throwError___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___lambda__1(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
uint8_t l___private_Init_Lean_Elab_Command_15__checkEndHeader___main(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
uint8_t l_PersistentHashMap_contains___at_Lean_Elab_Command_addBuiltinCommandElab___spec__4(lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabCheck___closed__3;
lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel(lean_object*);
@ -270,7 +271,6 @@ extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_addBuiltinCommandElab___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_CommandElabCoreM_monadState;
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___lambda__1___closed__4;
lean_object* l_Lean_Elab_getMacros(lean_object*, lean_object*, lean_object*, lean_object*);
@ -9903,7 +9903,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = l_Lean_Elab_Term_elabParen___closed__4;
x_6 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
@ -10081,7 +10081,7 @@ if (x_11 == 0)
{
uint8_t x_14;
lean_dec(x_9);
x_14 = l_Lean_Elab_Term_elabParen___closed__4;
x_14 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16;
@ -17375,7 +17375,7 @@ _start:
uint8_t x_7; lean_object* x_8;
x_7 = 1;
lean_inc(x_5);
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_7, x_2, x_5, x_6);
x_8 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_7, x_5, x_6);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
@ -17523,8 +17523,8 @@ x_4 = lean_unsigned_to_nat(1u);
x_5 = l_Lean_Syntax_getArg(x_1, x_4);
x_6 = lean_box(0);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabCheck___lambda__1___boxed), 6, 3);
lean_closure_set(x_7, 0, x_6);
lean_closure_set(x_7, 1, x_5);
lean_closure_set(x_7, 0, x_5);
lean_closure_set(x_7, 1, x_6);
lean_closure_set(x_7, 2, x_1);
lean_inc(x_2);
x_8 = l___private_Init_Lean_Elab_Command_2__getState(x_2, x_3);
@ -18005,7 +18005,7 @@ lean_object* x_6; uint8_t x_7; lean_object* x_8;
x_6 = lean_box(0);
x_7 = 1;
lean_inc(x_4);
x_8 = l_Lean_Elab_Term_elabTermAux___main(x_6, x_7, x_1, x_4, x_5);
x_8 = l_Lean_Elab_Term_elabTerm(x_1, x_6, x_7, x_4, x_5);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;

339
stage0/stdlib/Init/Lean/Elab/Definition.c
View file

@ -66,11 +66,11 @@ lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
lean_object* l_Lean_Elab_Command_DefKind_isTheorem___boxed(lean_object*);
lean_object* l_Lean_Elab_Command_expandDeclId(lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_declValSimple___elambda__1___closed__2;
lean_object* l_Lean_Expr_fvarId_x21(lean_object*);
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__2;
lean_object* l_Lean_Elab_Command_mkDef___lambda__1___closed__1;
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabDefLike___spec__4(lean_object*, lean_object*, lean_object*);
@ -1732,135 +1732,92 @@ return x_92;
lean_object* l_Lean_Elab_Command_mkDef(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, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_1, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_1, 5);
lean_inc(x_11);
lean_inc(x_6);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_6);
x_11 = 1;
x_12 = lean_box(0);
lean_inc(x_8);
lean_inc(x_11);
x_13 = l_Lean_Elab_Term_ensureHasType(x_11, x_12, x_7, x_8, x_9);
x_13 = l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_11, x_12, x_8, x_9);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_14 = lean_ctor_get(x_13, 0);
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = 0;
x_17 = lean_box(0);
x_15 = lean_ctor_get(x_1, 5);
lean_inc(x_15);
lean_inc(x_6);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_6);
lean_inc(x_8);
x_18 = l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_16, x_17, x_8, x_15);
if (lean_obj_tag(x_18) == 0)
lean_inc(x_15);
x_17 = l_Lean_Elab_Term_ensureHasType(x_15, x_16, x_7, x_8, x_14);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_19 = lean_ctor_get(x_18, 1);
lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21;
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_18);
lean_dec(x_17);
x_20 = 0;
lean_inc(x_8);
x_20 = l_Lean_Elab_Term_instantiateMVars(x_10, x_6, x_8, x_19);
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
x_22 = lean_ctor_get(x_20, 1);
x_21 = l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux___main(x_20, x_12, x_8, x_19);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27;
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_20);
lean_dec(x_21);
lean_inc(x_8);
x_23 = l_Lean_Elab_Term_instantiateMVars(x_11, x_14, x_8, x_22);
x_24 = !lean_is_exclusive(x_23);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26; uint8_t x_27; uint8_t x_28;
x_25 = lean_ctor_get(x_23, 0);
x_26 = lean_ctor_get(x_23, 1);
x_27 = lean_ctor_get_uint8(x_1, sizeof(void*)*6);
x_28 = l_Lean_Elab_Command_DefKind_isExample(x_27);
if (x_28 == 0)
{
uint8_t x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
lean_free_object(x_23);
x_29 = l_Lean_Elab_Command_DefKind_isDefOrOpaque(x_27);
x_30 = lean_box(x_27);
x_23 = l_Lean_Elab_Term_instantiateMVars(x_10, x_6, x_8, x_22);
x_24 = lean_ctor_get(x_23, 0);
lean_inc(x_24);
x_25 = lean_ctor_get(x_23, 1);
lean_inc(x_25);
lean_inc(x_21);
lean_inc(x_5);
lean_inc(x_10);
x_31 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDef___lambda__1___boxed), 12, 9);
lean_closure_set(x_31, 0, x_10);
lean_closure_set(x_31, 1, x_5);
lean_closure_set(x_31, 2, x_21);
lean_closure_set(x_31, 3, x_25);
lean_closure_set(x_31, 4, x_11);
lean_closure_set(x_31, 5, x_3);
lean_closure_set(x_31, 6, x_30);
lean_closure_set(x_31, 7, x_2);
lean_closure_set(x_31, 8, x_1);
x_32 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_25, x_21, x_29, x_31, x_8, x_26);
lean_dec(x_5);
lean_dec(x_10);
return x_32;
}
else
{
lean_object* x_33;
lean_dec(x_25);
lean_dec(x_21);
lean_dec(x_11);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_33 = lean_box(0);
lean_ctor_set(x_23, 0, x_33);
return x_23;
}
}
else
{
lean_object* x_34; lean_object* x_35; uint8_t x_36; uint8_t x_37;
x_34 = lean_ctor_get(x_23, 0);
x_35 = lean_ctor_get(x_23, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_23);
x_36 = lean_ctor_get_uint8(x_1, sizeof(void*)*6);
x_37 = l_Lean_Elab_Command_DefKind_isExample(x_36);
if (x_37 == 0)
lean_inc(x_8);
x_26 = l_Lean_Elab_Term_instantiateMVars(x_15, x_18, x_8, x_25);
x_27 = !lean_is_exclusive(x_26);
if (x_27 == 0)
{
uint8_t x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_38 = l_Lean_Elab_Command_DefKind_isDefOrOpaque(x_36);
x_39 = lean_box(x_36);
lean_inc(x_34);
lean_inc(x_21);
lean_object* x_28; lean_object* x_29; uint8_t x_30; uint8_t x_31;
x_28 = lean_ctor_get(x_26, 0);
x_29 = lean_ctor_get(x_26, 1);
x_30 = lean_ctor_get_uint8(x_1, sizeof(void*)*6);
x_31 = l_Lean_Elab_Command_DefKind_isExample(x_30);
if (x_31 == 0)
{
uint8_t x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
lean_free_object(x_26);
x_32 = l_Lean_Elab_Command_DefKind_isDefOrOpaque(x_30);
x_33 = lean_box(x_30);
lean_inc(x_28);
lean_inc(x_24);
lean_inc(x_5);
lean_inc(x_10);
x_40 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDef___lambda__1___boxed), 12, 9);
lean_closure_set(x_40, 0, x_10);
lean_closure_set(x_40, 1, x_5);
lean_closure_set(x_40, 2, x_21);
lean_closure_set(x_40, 3, x_34);
lean_closure_set(x_40, 4, x_11);
lean_closure_set(x_40, 5, x_3);
lean_closure_set(x_40, 6, x_39);
lean_closure_set(x_40, 7, x_2);
lean_closure_set(x_40, 8, x_1);
x_41 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_34, x_21, x_38, x_40, x_8, x_35);
x_34 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDef___lambda__1___boxed), 12, 9);
lean_closure_set(x_34, 0, x_10);
lean_closure_set(x_34, 1, x_5);
lean_closure_set(x_34, 2, x_24);
lean_closure_set(x_34, 3, x_28);
lean_closure_set(x_34, 4, x_15);
lean_closure_set(x_34, 5, x_3);
lean_closure_set(x_34, 6, x_33);
lean_closure_set(x_34, 7, x_2);
lean_closure_set(x_34, 8, x_1);
x_35 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_28, x_24, x_32, x_34, x_8, x_29);
lean_dec(x_5);
lean_dec(x_10);
return x_41;
return x_35;
}
else
{
lean_object* x_42; lean_object* x_43;
lean_dec(x_34);
lean_dec(x_21);
lean_dec(x_11);
lean_object* x_36;
lean_dec(x_28);
lean_dec(x_24);
lean_dec(x_15);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_5);
@ -1868,51 +1825,71 @@ lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_42 = lean_box(0);
x_43 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_35);
return x_43;
}
x_36 = lean_box(0);
lean_ctor_set(x_26, 0, x_36);
return x_26;
}
}
else
{
uint8_t x_44;
lean_dec(x_14);
lean_dec(x_11);
lean_object* x_37; lean_object* x_38; uint8_t x_39; uint8_t x_40;
x_37 = lean_ctor_get(x_26, 0);
x_38 = lean_ctor_get(x_26, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_26);
x_39 = lean_ctor_get_uint8(x_1, sizeof(void*)*6);
x_40 = l_Lean_Elab_Command_DefKind_isExample(x_39);
if (x_40 == 0)
{
uint8_t x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44;
x_41 = l_Lean_Elab_Command_DefKind_isDefOrOpaque(x_39);
x_42 = lean_box(x_39);
lean_inc(x_37);
lean_inc(x_24);
lean_inc(x_5);
lean_inc(x_10);
x_43 = lean_alloc_closure((void*)(l_Lean_Elab_Command_mkDef___lambda__1___boxed), 12, 9);
lean_closure_set(x_43, 0, x_10);
lean_closure_set(x_43, 1, x_5);
lean_closure_set(x_43, 2, x_24);
lean_closure_set(x_43, 3, x_37);
lean_closure_set(x_43, 4, x_15);
lean_closure_set(x_43, 5, x_3);
lean_closure_set(x_43, 6, x_42);
lean_closure_set(x_43, 7, x_2);
lean_closure_set(x_43, 8, x_1);
x_44 = l_Lean_Elab_Command_withUsedWhen___rarg(x_10, x_4, x_5, x_37, x_24, x_41, x_43, x_8, x_38);
lean_dec(x_5);
lean_dec(x_10);
return x_44;
}
else
{
lean_object* x_45; lean_object* x_46;
lean_dec(x_37);
lean_dec(x_24);
lean_dec(x_15);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_44 = !lean_is_exclusive(x_18);
if (x_44 == 0)
{
return x_18;
x_45 = lean_box(0);
x_46 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_38);
return x_46;
}
}
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_18, 0);
x_46 = lean_ctor_get(x_18, 1);
lean_inc(x_46);
lean_inc(x_45);
uint8_t x_47;
lean_dec(x_18);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}
else
{
uint8_t x_48;
lean_dec(x_11);
lean_dec(x_15);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_6);
@ -1921,23 +1898,87 @@ lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_48 = !lean_is_exclusive(x_13);
if (x_48 == 0)
x_47 = !lean_is_exclusive(x_21);
if (x_47 == 0)
{
return x_21;
}
else
{
lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_48 = lean_ctor_get(x_21, 0);
x_49 = lean_ctor_get(x_21, 1);
lean_inc(x_49);
lean_inc(x_48);
lean_dec(x_21);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
return x_50;
}
}
}
else
{
uint8_t x_51;
lean_dec(x_15);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_51 = !lean_is_exclusive(x_17);
if (x_51 == 0)
{
return x_17;
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_17, 0);
x_53 = lean_ctor_get(x_17, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_17);
x_54 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
return x_54;
}
}
}
else
{
uint8_t x_55;
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_55 = !lean_is_exclusive(x_13);
if (x_55 == 0)
{
return x_13;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_13, 0);
x_50 = lean_ctor_get(x_13, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_13, 0);
x_57 = lean_ctor_get(x_13, 1);
lean_inc(x_57);
lean_inc(x_56);
lean_dec(x_13);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
return x_58;
}
}
}
@ -2025,7 +2066,7 @@ lean_dec(x_1);
x_15 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_15, 0, x_2);
x_16 = 1;
x_17 = l_Lean_Elab_Term_elabTermAux___main(x_15, x_16, x_14, x_3, x_4);
x_17 = l_Lean_Elab_Term_elabTerm(x_14, x_15, x_16, x_3, x_4);
return x_17;
}
}

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

@ -72,6 +72,7 @@ extern lean_object* l_Lean_Expr_Inhabited___closed__1;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getLevel(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_DoNotation_12__processDoElems(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__6;
@ -82,7 +83,6 @@ extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux__
lean_object* l_Array_back___at___private_Init_Lean_Elab_DoNotation_10__mkBind___spec__1___boxed(lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Binders_10__expandFunBindersAux___main___closed__2;
extern lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__2;
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__11;
extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__3;
lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4670,7 +4670,7 @@ lean_ctor_set(x_34, 0, x_4);
x_35 = 1;
lean_inc(x_7);
lean_inc(x_34);
x_36 = l_Lean_Elab_Term_elabTermAux___main(x_34, x_35, x_33, x_7, x_8);
x_36 = l_Lean_Elab_Term_elabTerm(x_33, x_34, x_35, x_7, x_8);
if (lean_obj_tag(x_36) == 0)
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
@ -4791,9 +4791,9 @@ x_65 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_65, 0, x_64);
x_66 = 1;
lean_inc(x_7);
lean_inc(x_60);
lean_inc(x_65);
x_67 = l_Lean_Elab_Term_elabTermAux___main(x_65, x_66, x_60, x_7, x_63);
lean_inc(x_60);
x_67 = l_Lean_Elab_Term_elabTerm(x_60, x_65, x_66, x_7, x_63);
if (lean_obj_tag(x_67) == 0)
{
lean_object* x_68; lean_object* x_69; lean_object* x_70;
@ -5302,7 +5302,7 @@ lean_ctor_set(x_62, 0, x_61);
lean_ctor_set(x_62, 1, x_60);
lean_ctor_set(x_3, 8, x_62);
x_63 = 1;
x_64 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_63, x_58, x_3, x_49);
x_64 = l_Lean_Elab_Term_elabTerm(x_58, x_2, x_63, x_3, x_49);
return x_64;
}
else
@ -5354,7 +5354,7 @@ lean_ctor_set_uint8(x_80, sizeof(void*)*10, x_75);
lean_ctor_set_uint8(x_80, sizeof(void*)*10 + 1, x_76);
lean_ctor_set_uint8(x_80, sizeof(void*)*10 + 2, x_77);
x_81 = 1;
x_82 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_81, x_58, x_80, x_49);
x_82 = l_Lean_Elab_Term_elabTerm(x_58, x_2, x_81, x_80, x_49);
return x_82;
}
}

20
stage0/stdlib/Init/Lean/Elab/Match.c
View file

@ -24,14 +24,14 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMatch___closed__1;
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Elab_Term_getMainModule___rarg(lean_object*);
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
extern uint8_t l_Lean_Elab_Term_elabParen___closed__4;
extern uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
extern lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__3;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Match_1__expandSimpleMatch___closed__1;
lean_object* l_Lean_Elab_Term_throwUnsupportedSyntax___rarg(lean_object*);
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMatch___closed__2;
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Match_1__expandSimpleMatch___closed__3;
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*);
uint8_t l_coeDecidableEq(uint8_t);
@ -164,7 +164,7 @@ lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_30);
lean_ctor_set(x_6, 8, x_32);
x_33 = 1;
x_34 = l_Lean_Elab_Term_elabTermAux___main(x_5, x_33, x_28, x_6, x_11);
x_34 = l_Lean_Elab_Term_elabTerm(x_28, x_5, x_33, x_6, x_11);
return x_34;
}
else
@ -216,7 +216,7 @@ lean_ctor_set_uint8(x_50, sizeof(void*)*10, x_45);
lean_ctor_set_uint8(x_50, sizeof(void*)*10 + 1, x_46);
lean_ctor_set_uint8(x_50, sizeof(void*)*10 + 2, x_47);
x_51 = 1;
x_52 = l_Lean_Elab_Term_elabTermAux___main(x_5, x_51, x_28, x_50, x_11);
x_52 = l_Lean_Elab_Term_elabTerm(x_28, x_5, x_51, x_50, x_11);
return x_52;
}
}
@ -301,7 +301,7 @@ lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
lean_ctor_set(x_7, 8, x_40);
x_41 = 1;
x_42 = l_Lean_Elab_Term_elabTermAux___main(x_6, x_41, x_36, x_7, x_12);
x_42 = l_Lean_Elab_Term_elabTerm(x_36, x_6, x_41, x_7, x_12);
return x_42;
}
else
@ -353,7 +353,7 @@ lean_ctor_set_uint8(x_58, sizeof(void*)*10, x_53);
lean_ctor_set_uint8(x_58, sizeof(void*)*10 + 1, x_54);
lean_ctor_set_uint8(x_58, sizeof(void*)*10 + 2, x_55);
x_59 = 1;
x_60 = l_Lean_Elab_Term_elabTermAux___main(x_6, x_59, x_36, x_58, x_12);
x_60 = l_Lean_Elab_Term_elabTerm(x_36, x_6, x_59, x_58, x_12);
return x_60;
}
}
@ -769,7 +769,7 @@ if (x_54 == 0)
{
uint8_t x_55;
lean_dec(x_52);
x_55 = l_Lean_Elab_Term_elabParen___closed__4;
x_55 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_55 == 0)
{
lean_object* x_56;
@ -1064,7 +1064,7 @@ if (x_127 == 0)
{
uint8_t x_128;
lean_dec(x_126);
x_128 = l_Lean_Elab_Term_elabParen___closed__4;
x_128 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_128 == 0)
{
lean_object* x_129;
@ -1395,7 +1395,7 @@ if (x_215 == 0)
{
uint8_t x_216;
lean_dec(x_214);
x_216 = l_Lean_Elab_Term_elabParen___closed__4;
x_216 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_216 == 0)
{
lean_object* x_217;
@ -1683,7 +1683,7 @@ if (x_285 == 0)
{
uint8_t x_286;
lean_dec(x_284);
x_286 = l_Lean_Elab_Term_elabParen___closed__4;
x_286 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_286 == 0)
{
lean_object* x_287;

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

@ -134,6 +134,7 @@ lean_object* l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__3;
lean_object* l_Lean_Elab_Term_Quotation_HeadInfo_Inhabited___closed__2;
lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__23;
extern lean_object* l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__7;
extern lean_object* l_Lean_Parser_Term_num___elambda__1___closed__1;
lean_object* l_List_range(lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_8__explodeHeadPat___lambda__1___closed__2;
@ -176,7 +177,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__2___
extern lean_object* l_Nat_HasOfNat___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_13__toPreterm___main___closed__5;
lean_object* l_Lean_Elab_Term_Quotation_match__syntax_expand(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_elabParen___closed__5;
lean_object* l_Lean_Elab_Term_Quotation_oldExpandMatchSyntax___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_11__letBindRhss___main___closed__8;
lean_object* l___private_Init_Lean_Elab_Quotation_1__quoteName___main(lean_object*);
@ -200,6 +200,7 @@ lean_object* l_List_head_x21___at___private_Init_Lean_Elab_Quotation_9__compileS
extern lean_object* l_Lean_mkTermIdFromIdent___closed__2;
lean_object* l_Array_foldlStepMAux___main___at_Lean_Elab_Term_elabParen___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkMData(lean_object*, lean_object*);
extern uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__19;
lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_14__oldRunTermElabM___rarg___closed__3;
@ -220,7 +221,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed
extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__1;
lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__8(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_setPos(lean_object*, lean_object*);
extern uint8_t l_Lean_Elab_Term_elabParen___closed__4;
extern lean_object* l_Lean_Elab_Term_elabParen___closed__4;
lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__8___closed__4;
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_Quotation_elabStxQuot___closed__2;
lean_object* lean_array_fget(lean_object*, lean_object*);
@ -262,7 +263,6 @@ lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__22;
lean_object* l_Lean_Elab_Term_Quotation_isAntiquotSplice___boxed(lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Term_12__mkPairsAux___main___closed__7;
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__1;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_Quotation_match__syntax_expand___spec__1___closed__4;
@ -821,7 +821,7 @@ x_7 = lean_apply_1(x_2, x_5);
x_8 = l_Lean_mkAppStx___closed__9;
x_9 = lean_array_push(x_8, x_6);
x_10 = lean_array_push(x_9, x_7);
x_11 = l___private_Init_Lean_Elab_Term_12__mkPairsAux___main___closed__7;
x_11 = l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__7;
x_12 = l_Lean_mkCAppStx(x_11, x_10);
return x_12;
}
@ -2014,7 +2014,7 @@ x_9 = l___private_Init_Lean_Elab_Quotation_2__quoteList___main___at___private_In
x_10 = l_Lean_mkAppStx___closed__9;
x_11 = lean_array_push(x_10, x_8);
x_12 = lean_array_push(x_11, x_9);
x_13 = l___private_Init_Lean_Elab_Term_12__mkPairsAux___main___closed__7;
x_13 = l___private_Init_Lean_Elab_Term_14__mkPairsAux___main___closed__7;
x_14 = l_Lean_mkCAppStx(x_13, x_12);
x_15 = lean_array_push(x_10, x_14);
x_16 = lean_array_push(x_15, x_5);
@ -5846,7 +5846,7 @@ x_68 = l_Lean_Syntax_isOfKind(x_66, x_67);
if (x_68 == 0)
{
uint8_t x_69;
x_69 = l_Lean_Elab_Term_elabParen___closed__4;
x_69 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_69 == 0)
{
lean_dec(x_66);
@ -5923,7 +5923,7 @@ if (x_86 == 0)
{
uint8_t x_87;
lean_dec(x_85);
x_87 = l_Lean_Elab_Term_elabParen___closed__4;
x_87 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_87 == 0)
{
lean_dec(x_84);
@ -11195,7 +11195,7 @@ if (x_31 == 0)
{
uint8_t x_32;
lean_dec(x_29);
x_32 = l_Lean_Elab_Term_elabParen___closed__4;
x_32 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_32 == 0)
{
lean_object* x_33; uint8_t x_34;
@ -15308,7 +15308,7 @@ lean_dec(x_142);
lean_dec(x_2);
x_148 = l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
x_149 = lean_name_mk_string(x_27, x_148);
x_150 = l_Lean_Elab_Term_elabParen___closed__5;
x_150 = l_Lean_Elab_Term_elabParen___closed__4;
x_151 = lean_name_mk_string(x_149, x_150);
x_152 = lean_box(0);
x_153 = l_Lean_mkConst(x_151, x_152);
@ -17748,7 +17748,7 @@ lean_dec(x_842);
lean_dec(x_2);
x_848 = l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
x_849 = lean_name_mk_string(x_27, x_848);
x_850 = l_Lean_Elab_Term_elabParen___closed__5;
x_850 = l_Lean_Elab_Term_elabParen___closed__4;
x_851 = lean_name_mk_string(x_849, x_850);
x_852 = lean_box(0);
x_853 = l_Lean_mkConst(x_851, x_852);
@ -19604,7 +19604,7 @@ lean_dec(x_1352);
lean_dec(x_2);
x_1358 = l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
x_1359 = lean_name_mk_string(x_27, x_1358);
x_1360 = l_Lean_Elab_Term_elabParen___closed__5;
x_1360 = l_Lean_Elab_Term_elabParen___closed__4;
x_1361 = lean_name_mk_string(x_1359, x_1360);
x_1362 = lean_box(0);
x_1363 = l_Lean_mkConst(x_1361, x_1362);
@ -21493,7 +21493,7 @@ lean_dec(x_1868);
lean_dec(x_2);
x_1874 = l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
x_1875 = lean_name_mk_string(x_27, x_1874);
x_1876 = l_Lean_Elab_Term_elabParen___closed__5;
x_1876 = l_Lean_Elab_Term_elabParen___closed__4;
x_1877 = lean_name_mk_string(x_1875, x_1876);
x_1878 = lean_box(0);
x_1879 = l_Lean_mkConst(x_1877, x_1878);
@ -23414,7 +23414,7 @@ lean_dec(x_2391);
lean_dec(x_2);
x_2397 = l___private_Init_Lean_Compiler_InitAttr_2__isUnitType___closed__1;
x_2398 = lean_name_mk_string(x_27, x_2397);
x_2399 = l_Lean_Elab_Term_elabParen___closed__5;
x_2399 = l_Lean_Elab_Term_elabParen___closed__4;
x_2400 = lean_name_mk_string(x_2398, x_2399);
x_2401 = lean_box(0);
x_2402 = l_Lean_mkConst(x_2400, x_2401);

6
stage0/stdlib/Init/Lean/Elab/StructInst.c
View file

@ -153,6 +153,7 @@ lean_object* l_Lean_Elab_Term_StructInst_Field_isSimple(lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_Struct_fields___boxed(lean_object*);
lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_toSyntax(uint8_t, lean_object*);
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_StructInst_4__elabModifyOp___closed__2;
lean_object* l___private_Init_Lean_Elab_StructInst_13__isSimpleField_x3f___boxed(lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_StructInst_ExpandNonAtomicExplicitSource_main___spec__1___closed__5;
@ -172,7 +173,6 @@ lean_object* l___private_Init_Lean_Elab_StructInst_14__getFieldIdx___closed__1;
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_StructInst_Field_toSyntax___spec__1(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__3___closed__2;
size_t l_Lean_Name_hash(lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l___private_Init_Lean_Elab_StructInst_14__getFieldIdx___closed__2;
lean_object* l_List_head_x21___at___private_Init_Lean_Elab_StructInst_18__expandStruct___main___spec__5(lean_object*);
@ -14710,7 +14710,7 @@ lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_33);
lean_ctor_set(x_3, 8, x_35);
x_36 = 1;
x_37 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_36, x_31, x_3, x_30);
x_37 = l_Lean_Elab_Term_elabTerm(x_31, x_2, x_36, x_3, x_30);
return x_37;
}
else
@ -14762,7 +14762,7 @@ lean_ctor_set_uint8(x_53, sizeof(void*)*10, x_48);
lean_ctor_set_uint8(x_53, sizeof(void*)*10 + 1, x_49);
lean_ctor_set_uint8(x_53, sizeof(void*)*10 + 2, x_50);
x_54 = 1;
x_55 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_54, x_31, x_53, x_30);
x_55 = l_Lean_Elab_Term_elabTerm(x_31, x_2, x_54, x_53, x_30);
return x_55;
}
}

10
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

@ -181,6 +181,7 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__16;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
extern lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__49;
extern uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__105;
extern lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__2;
lean_object* l___private_Init_Lean_Elab_Syntax_7__antiquote___main(lean_object*, lean_object*);
@ -195,7 +196,6 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__100;
lean_object* l_Lean_Elab_Term_checkLeftRec___closed__4;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__53;
lean_object* l_Lean_Elab_Command_expandMacroHeadIntoPattern(lean_object*, lean_object*, lean_object*);
extern uint8_t l_Lean_Elab_Term_elabParen___closed__4;
lean_object* l_Lean_Elab_Command_elabNoKindMacroRulesAux___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_Elab_Term_toParserDescrAux___main___spec__2(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__42;
@ -10846,7 +10846,7 @@ x_8 = l_Lean_Syntax_isOfKind(x_6, x_7);
if (x_8 == 0)
{
uint8_t x_9;
x_9 = l_Lean_Elab_Term_elabParen___closed__4;
x_9 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_9 == 0)
{
lean_object* x_10; lean_object* x_11;
@ -11818,7 +11818,7 @@ if (x_18 == 0)
{
uint8_t x_21;
lean_dec(x_16);
x_21 = l_Lean_Elab_Term_elabParen___closed__4;
x_21 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_21 == 0)
{
lean_object* x_22; lean_object* x_23;
@ -11965,7 +11965,7 @@ if (x_63 == 0)
{
uint8_t x_66;
lean_dec(x_62);
x_66 = l_Lean_Elab_Term_elabParen___closed__4;
x_66 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_66 == 0)
{
lean_object* x_67; lean_object* x_68;
@ -12621,7 +12621,7 @@ if (x_44 == 0)
{
uint8_t x_45;
lean_dec(x_27);
x_45 = l_Lean_Elab_Term_elabParen___closed__4;
x_45 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_45 == 0)
{
lean_dec(x_15);

10
stage0/stdlib/Init/Lean/Elab/SyntheticMVars.c
View file

@ -56,6 +56,7 @@ lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg(lean
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_11__synthesizeSyntheticMVarsAux(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_2__resumePostponed___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__8;
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___closed__4;
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_6__synthesizeSyntheticMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -66,7 +67,6 @@ lean_object* l_List_lengthAux___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_10__getSomeSynthethicMVarsRef___rarg___lambda__1___boxed(lean_object*);
lean_object* l_Lean_Elab_Tactic_getUnsolvedGoals(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_4__synthesizePendingCoeInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forM___main___at___private_Init_Lean_Elab_SyntheticMVars_9__reportStuckSyntheticMVars___spec__1___lambda__1___closed__1;
lean_object* l_Lean_Elab_Term_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_SyntheticMVars_7__synthesizeSyntheticMVarsStep___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1432,7 +1432,7 @@ if (x_7 == 0)
uint8_t x_8; lean_object* x_9;
x_8 = 0;
lean_ctor_set_uint8(x_4, sizeof(void*)*10 + 1, x_8);
x_9 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_8, x_1, x_4, x_5);
x_9 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_8, x_4, x_5);
return x_9;
}
else
@ -1476,7 +1476,7 @@ lean_ctor_set(x_23, 9, x_19);
lean_ctor_set_uint8(x_23, sizeof(void*)*10, x_20);
lean_ctor_set_uint8(x_23, sizeof(void*)*10 + 1, x_22);
lean_ctor_set_uint8(x_23, sizeof(void*)*10 + 2, x_21);
x_24 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_22, x_1, x_23, x_5);
x_24 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_22, x_23, x_5);
return x_24;
}
}
@ -1489,7 +1489,7 @@ if (x_25 == 0)
uint8_t x_26; lean_object* x_27;
lean_ctor_set_uint8(x_4, sizeof(void*)*10 + 1, x_3);
x_26 = 0;
x_27 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_26, x_1, x_4, x_5);
x_27 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_26, x_4, x_5);
return x_27;
}
else
@ -1533,7 +1533,7 @@ lean_ctor_set_uint8(x_40, sizeof(void*)*10, x_38);
lean_ctor_set_uint8(x_40, sizeof(void*)*10 + 1, x_3);
lean_ctor_set_uint8(x_40, sizeof(void*)*10 + 2, x_39);
x_41 = 0;
x_42 = l_Lean_Elab_Term_elabTermAux___main(x_2, x_41, x_1, x_40, x_5);
x_42 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_41, x_40, x_5);
return x_42;
}
}

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

@ -144,6 +144,7 @@ lean_object* l_Lean_Elab_Tactic_getMainGoal___closed__2;
lean_object* l___private_Init_Lean_Elab_Tactic_Basic_3__getIntrosSize(lean_object*);
lean_object* l_Lean_Elab_Tactic_monadLog___closed__3;
extern lean_object* l_Array_forMAux___main___at_Lean_Meta_clear___spec__5___closed__8;
extern uint8_t l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
extern lean_object* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
lean_object* l_Lean_Meta_intro(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_tagUntaggedGoals___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -158,7 +159,6 @@ extern lean_object* l_Lean_Meta_dbgTrace___rarg___closed__1;
extern lean_object* l___private_Init_Lean_Elab_Term_10__elabTermUsing___main___closed__3;
lean_object* l_List_findM_x3f___main___at_Lean_Elab_Tactic_evalCase___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTactic___main___closed__2;
extern uint8_t l_Lean_Elab_Term_elabParen___closed__4;
extern lean_object* l_Lean_Elab_Term_withIncRecDepth___rarg___closed__2;
lean_object* l_Lean_Elab_Tactic_evalCase(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SMap_find_x3f___at_Lean_Elab_Tactic_evalTactic___main___spec__1___boxed(lean_object*, lean_object*);
@ -14267,7 +14267,7 @@ if (x_12 == 0)
if (x_10 == 0)
{
uint8_t x_13;
x_13 = l_Lean_Elab_Term_elabParen___closed__4;
x_13 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_13 == 0)
{
lean_object* x_14;
@ -15699,7 +15699,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = l_Lean_Elab_Term_elabParen___closed__4;
x_6 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_6 == 0)
{
lean_object* x_7;
@ -15809,7 +15809,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = l_Lean_Elab_Term_elabParen___closed__4;
x_6 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_6 == 0)
{
lean_object* x_7;
@ -16476,7 +16476,7 @@ x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = l_Lean_Elab_Term_elabParen___closed__4;
x_6 = l___private_Init_Lean_Elab_Term_11__isExplicit___closed__1;
if (x_6 == 0)
{
lean_object* x_7;

30
stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c
View file

@ -30,9 +30,9 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine___closed__3;
lean_object* l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Tactic_declareBuiltinTactic___closed__3;
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_apply___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTermAux___main(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalRefine(lean_object*);
lean_object* l_Lean_Elab_Tactic_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply(lean_object*);
@ -83,8 +83,8 @@ x_7 = 0;
lean_ctor_set_uint8(x_4, sizeof(void*)*10 + 1, x_7);
x_8 = 1;
lean_inc(x_4);
lean_inc(x_2);
x_9 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_8, x_2, x_4, x_5);
lean_inc(x_1);
x_9 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_8, x_4, x_5);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
@ -102,8 +102,8 @@ lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Elab_Term_instantiateMVars(x_2, x_10, x_4, x_14);
lean_dec(x_2);
x_15 = l_Lean_Elab_Term_instantiateMVars(x_1, x_10, x_4, x_14);
lean_dec(x_1);
return x_15;
}
else
@ -111,7 +111,7 @@ else
uint8_t x_16;
lean_dec(x_10);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_16 = !lean_is_exclusive(x_13);
if (x_16 == 0)
{
@ -136,7 +136,7 @@ else
{
uint8_t x_20;
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_20 = !lean_is_exclusive(x_9);
if (x_20 == 0)
{
@ -200,8 +200,8 @@ lean_ctor_set_uint8(x_37, sizeof(void*)*10 + 1, x_36);
lean_ctor_set_uint8(x_37, sizeof(void*)*10 + 2, x_35);
x_38 = 1;
lean_inc(x_37);
lean_inc(x_2);
x_39 = l_Lean_Elab_Term_elabTermAux___main(x_1, x_38, x_2, x_37, x_5);
lean_inc(x_1);
x_39 = l_Lean_Elab_Term_elabTerm(x_1, x_2, x_38, x_37, x_5);
if (lean_obj_tag(x_39) == 0)
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
@ -219,8 +219,8 @@ lean_object* x_44; lean_object* x_45;
x_44 = lean_ctor_get(x_43, 1);
lean_inc(x_44);
lean_dec(x_43);
x_45 = l_Lean_Elab_Term_instantiateMVars(x_2, x_40, x_37, x_44);
lean_dec(x_2);
x_45 = l_Lean_Elab_Term_instantiateMVars(x_1, x_40, x_37, x_44);
lean_dec(x_1);
return x_45;
}
else
@ -228,7 +228,7 @@ else
lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49;
lean_dec(x_40);
lean_dec(x_37);
lean_dec(x_2);
lean_dec(x_1);
x_46 = lean_ctor_get(x_43, 0);
lean_inc(x_46);
x_47 = lean_ctor_get(x_43, 1);
@ -255,7 +255,7 @@ else
{
lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53;
lean_dec(x_37);
lean_dec(x_2);
lean_dec(x_1);
x_50 = lean_ctor_get(x_39, 0);
lean_inc(x_50);
x_51 = lean_ctor_get(x_39, 1);
@ -286,8 +286,8 @@ _start:
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_box(x_3);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_elabTerm___lambda__1___boxed), 5, 3);
lean_closure_set(x_7, 0, x_2);
lean_closure_set(x_7, 1, x_1);
lean_closure_set(x_7, 0, x_1);
lean_closure_set(x_7, 1, x_2);
lean_closure_set(x_7, 2, x_6);
x_8 = l_Lean_Elab_Tactic_liftTermElabM___rarg(x_7, x_4, x_5);
return x_8;

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

File diff suppressed because it is too large Load diff

14700
stage0/stdlib/Init/Lean/Meta/ExprDefEq.c
View file

File diff suppressed because it is too large Load diff

463
stage0/stdlib/Init/Lean/Parser/Command.c
View file

@ -14,6 +14,7 @@
extern "C" {
#endif
lean_object* l_Lean_Parser_Command_attrInstance___closed__6;
lean_object* l_Lean_Parser_Command_check__failure___closed__5;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_example___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_init__quot___closed__3;
@ -36,6 +37,7 @@ lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_structure___closed__3;
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_constant___closed__6;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_visibility___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__8;
lean_object* l_Lean_Parser_Command_protected___elambda__1___closed__1;
@ -123,6 +125,7 @@ lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_structFields_
lean_object* l_Lean_Parser_Command_introRule___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_init__quot___closed__5;
lean_object* l_Lean_Parser_Command_extends___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_synth___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__7;
@ -264,6 +267,7 @@ lean_object* l_Lean_Parser_Command_export___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_variables___closed__1;
lean_object* l_Lean_Parser_Command_openRenamingItem___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_check__failure___closed__3;
lean_object* l_Lean_Parser_Command_instance___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_docComment___closed__2;
lean_object* l_Lean_Parser_regBuiltinCommandParserAttr___closed__2;
@ -421,6 +425,7 @@ lean_object* l_Lean_Parser_Command_declModifiers___closed__14;
lean_object* l_Lean_Parser_Command_constant___closed__2;
lean_object* l_Lean_Parser_Command_export___closed__9;
lean_object* l_Lean_Parser_noFirstTokenInfo(lean_object*);
lean_object* l_Lean_Parser_Command_check__failure___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_set__option___elambda__1___closed__2;
lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
lean_object* l_Lean_Parser_Command_example___elambda__1(lean_object*, lean_object*);
@ -455,6 +460,7 @@ lean_object* l_Lean_Parser_Command_universes___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_structExplicitBinder;
lean_object* l_Lean_Parser_Command_axiom___closed__7;
lean_object* l_Lean_Parser_Command_optDeclSig___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_check__failure___closed__4;
lean_object* l_Lean_Parser_Command_structureTk___elambda__1___closed__5;
uint8_t l_Lean_Parser_tryAnti(lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Command_exit(lean_object*);
@ -481,6 +487,7 @@ lean_object* l_Lean_Parser_Command_classInductive___closed__3;
lean_object* l_Lean_Parser_Command_optDeclSig;
lean_object* l_Lean_Parser_Command_def___closed__3;
lean_object* l_Lean_Parser_Command_extends___elambda__1(lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Command_check__failure(lean_object*);
lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_section___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_introRule___closed__4;
@ -543,6 +550,7 @@ lean_object* l_Lean_Parser_Command_visibility___closed__3;
lean_object* l_Lean_Parser_Command_unsafe___closed__1;
lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_partial___closed__5;
lean_object* l_Lean_Parser_Command_check__failure___closed__1;
lean_object* l_Lean_Parser_Command_classTk___closed__2;
lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__9;
extern lean_object* l_Lean_Parser_rawIdent;
@ -587,6 +595,7 @@ lean_object* l_Lean_Parser_Command_axiom___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Command_universe(lean_object*);
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_partial___closed__1;
lean_object* l_Lean_Parser_Command_abbrev___elambda__1___closed__3;
@ -792,11 +801,13 @@ extern lean_object* l_Lean_Parser_Term_structInstArrayRef___elambda__1___closed_
lean_object* l_Lean_Parser_Command_resolve__name___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_private___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_declModifiers___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_check__failure___closed__6;
lean_object* l_Lean_Parser_Command_constant___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__9;
lean_object* l_Lean_Parser_Command_attrInstance___elambda__1(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Parser_Parser_2__sepByFnAux___main___at_Lean_Parser_Term_explicitUniv___elambda__1___spec__2___closed__4;
lean_object* l_Lean_Parser_categoryParser(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_structImplicitBinder___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structure___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_structCtor___closed__3;
@ -811,10 +822,12 @@ lean_object* l_Lean_Parser_Command_openSimple___elambda__1(lean_object*, lean_ob
lean_object* l_Lean_Parser_Command_structureTk___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_declSig___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_universe___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_check__failure___closed__2;
lean_object* l_Lean_Parser_Command_declaration;
lean_object* l_Lean_Parser_Command_structExplicitBinder___closed__6;
lean_object* l_Lean_Parser_Command_declId___closed__7;
lean_object* l_Lean_Parser_Command_openOnly___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__8;
lean_object* l_Lean_Parser_sepBy1Fn___at_Lean_Parser_Command_openRenaming___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_structInstBinder___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_introRule___closed__6;
@ -862,6 +875,7 @@ lean_object* l_Lean_Parser_Command_instance___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_noncomputable___closed__4;
lean_object* l_Lean_Parser_Command_structInstBinder___elambda__1___closed__2;
lean_object* l___regBuiltinParser_Lean_Parser_Term_stxQuot(lean_object*);
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_openOnly___closed__6;
lean_object* l_Lean_Parser_Command_structFields___closed__7;
lean_object* l_Lean_Parser_Command_export___elambda__1___closed__9;
@ -897,6 +911,7 @@ lean_object* l_Lean_Parser_Command_attrArg___closed__1;
lean_object* l_Lean_Parser_Command_partial___closed__2;
lean_object* l_Lean_Parser_Command_attribute___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_openHiding___closed__1;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_def___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_inductive___elambda__1___closed__2;
lean_object* l_Lean_Parser_Command_export___elambda__1___closed__2;
@ -1041,6 +1056,8 @@ lean_object* l_Lean_Parser_Command_exit___closed__2;
lean_object* l_Lean_Parser_Command_openOnly___closed__4;
lean_object* l_Lean_Parser_Command_noncomputable___closed__2;
lean_object* l_Lean_Parser_Command_theorem___elambda__1___closed__3;
lean_object* l_Lean_Parser_Command_check__failure;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_open___closed__8;
lean_object* l_Lean_Parser_Command_unsafe___elambda__1___closed__8;
lean_object* l_Lean_Parser_Command_synth___elambda__1___closed__8;
@ -1081,6 +1098,7 @@ lean_object* l_Lean_Parser_Term_stxQuot___closed__9;
lean_object* l_Lean_Parser_Command_open___closed__9;
lean_object* l_Lean_Parser_Command_example___closed__2;
lean_object* l_Lean_Parser_Command_instance___closed__7;
lean_object* l_Lean_Parser_Command_check__failure___elambda__1___closed__1;
lean_object* l_Lean_Parser_Command_attribute___closed__4;
lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_declSig;
@ -25734,6 +25752,416 @@ x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("check_failure");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_docComment___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_check__failure___elambda__1___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__1;
x_2 = l_Lean_Parser_Command_check__failure___elambda__1___closed__3;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("#check_failure ");
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__5;
x_2 = l_String_trim(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_Command_check__failure___elambda__1___closed__6;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__8() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__7;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Command_check__failure___elambda__1___closed__8;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_Command_check__failure___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t x_5;
x_3 = l_Lean_Parser_Command_check__failure___elambda__1___closed__4;
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_inc(x_2);
lean_inc(x_1);
x_5 = l_Lean_Parser_tryAnti(x_1, x_2);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_18; lean_object* x_19; lean_object* x_20;
lean_dec(x_4);
x_6 = lean_ctor_get(x_2, 0);
lean_inc(x_6);
x_7 = lean_array_get_size(x_6);
lean_dec(x_6);
x_18 = lean_ctor_get(x_2, 1);
lean_inc(x_18);
lean_inc(x_1);
x_19 = l_Lean_Parser_tokenFn(x_1, x_2);
x_20 = lean_ctor_get(x_19, 3);
lean_inc(x_20);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_19, 0);
lean_inc(x_21);
x_22 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_21);
lean_dec(x_21);
if (lean_obj_tag(x_22) == 2)
{
lean_object* x_23; lean_object* x_24; uint8_t x_25;
x_23 = lean_ctor_get(x_22, 1);
lean_inc(x_23);
lean_dec(x_22);
x_24 = l_Lean_Parser_Command_check__failure___elambda__1___closed__6;
x_25 = lean_string_dec_eq(x_23, x_24);
lean_dec(x_23);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27;
x_26 = l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
x_27 = l_Lean_Parser_ParserState_mkErrorsAt(x_19, x_26, x_18);
x_8 = x_27;
goto block_17;
}
else
{
lean_dec(x_18);
x_8 = x_19;
goto block_17;
}
}
else
{
lean_object* x_28; lean_object* x_29;
lean_dec(x_22);
x_28 = l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
x_29 = l_Lean_Parser_ParserState_mkErrorsAt(x_19, x_28, x_18);
x_8 = x_29;
goto block_17;
}
}
else
{
lean_object* x_30; lean_object* x_31;
lean_dec(x_20);
x_30 = l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
x_31 = l_Lean_Parser_ParserState_mkErrorsAt(x_19, x_30, x_18);
x_8 = x_31;
goto block_17;
}
block_17:
{
lean_object* x_9;
x_9 = lean_ctor_get(x_8, 3);
lean_inc(x_9);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_10 = l_Lean_Parser_termParser___closed__2;
x_11 = lean_unsigned_to_nat(0u);
x_12 = l_Lean_Parser_categoryParser___elambda__1(x_10, x_11, x_1, x_8);
x_13 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_14 = l_Lean_Parser_ParserState_mkNode(x_12, x_13, x_7);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
lean_dec(x_9);
lean_dec(x_1);
x_15 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_16 = l_Lean_Parser_ParserState_mkNode(x_8, x_15, x_7);
return x_16;
}
}
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_32 = lean_ctor_get(x_2, 0);
lean_inc(x_32);
x_33 = lean_array_get_size(x_32);
lean_dec(x_32);
x_34 = lean_ctor_get(x_2, 1);
lean_inc(x_34);
lean_inc(x_1);
x_35 = lean_apply_2(x_4, x_1, x_2);
x_36 = lean_ctor_get(x_35, 3);
lean_inc(x_36);
if (lean_obj_tag(x_36) == 0)
{
lean_dec(x_34);
lean_dec(x_33);
lean_dec(x_1);
return x_35;
}
else
{
lean_object* x_37; lean_object* x_38; uint8_t x_39;
x_37 = lean_ctor_get(x_36, 0);
lean_inc(x_37);
lean_dec(x_36);
x_38 = lean_ctor_get(x_35, 1);
lean_inc(x_38);
x_39 = lean_nat_dec_eq(x_38, x_34);
lean_dec(x_38);
if (x_39 == 0)
{
lean_dec(x_37);
lean_dec(x_34);
lean_dec(x_33);
lean_dec(x_1);
return x_35;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_55; lean_object* x_56;
lean_inc(x_34);
x_40 = l_Lean_Parser_ParserState_restore(x_35, x_33, x_34);
lean_dec(x_33);
x_41 = lean_ctor_get(x_40, 0);
lean_inc(x_41);
x_42 = lean_array_get_size(x_41);
lean_dec(x_41);
lean_inc(x_1);
x_55 = l_Lean_Parser_tokenFn(x_1, x_40);
x_56 = lean_ctor_get(x_55, 3);
lean_inc(x_56);
if (lean_obj_tag(x_56) == 0)
{
lean_object* x_57; lean_object* x_58;
x_57 = lean_ctor_get(x_55, 0);
lean_inc(x_57);
x_58 = l_Array_back___at_Lean_Parser_checkStackTopFn___spec__1(x_57);
lean_dec(x_57);
if (lean_obj_tag(x_58) == 2)
{
lean_object* x_59; lean_object* x_60; uint8_t x_61;
x_59 = lean_ctor_get(x_58, 1);
lean_inc(x_59);
lean_dec(x_58);
x_60 = l_Lean_Parser_Command_check__failure___elambda__1___closed__6;
x_61 = lean_string_dec_eq(x_59, x_60);
lean_dec(x_59);
if (x_61 == 0)
{
lean_object* x_62; lean_object* x_63;
x_62 = l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
lean_inc(x_34);
x_63 = l_Lean_Parser_ParserState_mkErrorsAt(x_55, x_62, x_34);
x_43 = x_63;
goto block_54;
}
else
{
x_43 = x_55;
goto block_54;
}
}
else
{
lean_object* x_64; lean_object* x_65;
lean_dec(x_58);
x_64 = l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
lean_inc(x_34);
x_65 = l_Lean_Parser_ParserState_mkErrorsAt(x_55, x_64, x_34);
x_43 = x_65;
goto block_54;
}
}
else
{
lean_object* x_66; lean_object* x_67;
lean_dec(x_56);
x_66 = l_Lean_Parser_Command_check__failure___elambda__1___closed__9;
lean_inc(x_34);
x_67 = l_Lean_Parser_ParserState_mkErrorsAt(x_55, x_66, x_34);
x_43 = x_67;
goto block_54;
}
block_54:
{
lean_object* x_44;
x_44 = lean_ctor_get(x_43, 3);
lean_inc(x_44);
if (lean_obj_tag(x_44) == 0)
{
lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50;
x_45 = l_Lean_Parser_termParser___closed__2;
x_46 = lean_unsigned_to_nat(0u);
x_47 = l_Lean_Parser_categoryParser___elambda__1(x_45, x_46, x_1, x_43);
x_48 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_49 = l_Lean_Parser_ParserState_mkNode(x_47, x_48, x_42);
x_50 = l_Lean_Parser_mergeOrElseErrors(x_49, x_37, x_34);
lean_dec(x_34);
return x_50;
}
else
{
lean_object* x_51; lean_object* x_52; lean_object* x_53;
lean_dec(x_44);
lean_dec(x_1);
x_51 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_52 = l_Lean_Parser_ParserState_mkNode(x_43, x_51, x_42);
x_53 = l_Lean_Parser_mergeOrElseErrors(x_52, x_37, x_34);
lean_dec(x_34);
return x_53;
}
}
}
}
}
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_Command_check__failure___elambda__1___closed__6;
x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___closed__2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_check__failure___closed__1;
x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_2 = l_Lean_Parser_Command_check__failure___closed__2;
x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Parser_Command_check__failure___elambda__1___closed__4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l_Lean_Parser_Command_check__failure___closed__3;
x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_check__failure___elambda__1), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_Command_check__failure___closed__4;
x_2 = l_Lean_Parser_Command_check__failure___closed__5;
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_Command_check__failure() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Parser_Command_check__failure___closed__6;
return x_1;
}
}
lean_object* l___regBuiltinParser_Lean_Parser_Command_check__failure(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6;
x_2 = l_Lean_Parser_regBuiltinCommandParserAttr___closed__4;
x_3 = l_Lean_Parser_Command_check__failure___elambda__1___closed__2;
x_4 = 1;
x_5 = l_Lean_Parser_Command_check__failure;
x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
lean_object* _init_l_Lean_Parser_Command_synth___elambda__1___closed__1() {
_start:
{
@ -35161,6 +35589,41 @@ lean_mark_persistent(l_Lean_Parser_Command_check);
res = l___regBuiltinParser_Lean_Parser_Command_check(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Command_check__failure___elambda__1___closed__1 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__1);
l_Lean_Parser_Command_check__failure___elambda__1___closed__2 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__2();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__2);
l_Lean_Parser_Command_check__failure___elambda__1___closed__3 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__3();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__3);
l_Lean_Parser_Command_check__failure___elambda__1___closed__4 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__4);
l_Lean_Parser_Command_check__failure___elambda__1___closed__5 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__5);
l_Lean_Parser_Command_check__failure___elambda__1___closed__6 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__6);
l_Lean_Parser_Command_check__failure___elambda__1___closed__7 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__7);
l_Lean_Parser_Command_check__failure___elambda__1___closed__8 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__8();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__8);
l_Lean_Parser_Command_check__failure___elambda__1___closed__9 = _init_l_Lean_Parser_Command_check__failure___elambda__1___closed__9();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___elambda__1___closed__9);
l_Lean_Parser_Command_check__failure___closed__1 = _init_l_Lean_Parser_Command_check__failure___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___closed__1);
l_Lean_Parser_Command_check__failure___closed__2 = _init_l_Lean_Parser_Command_check__failure___closed__2();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___closed__2);
l_Lean_Parser_Command_check__failure___closed__3 = _init_l_Lean_Parser_Command_check__failure___closed__3();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___closed__3);
l_Lean_Parser_Command_check__failure___closed__4 = _init_l_Lean_Parser_Command_check__failure___closed__4();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___closed__4);
l_Lean_Parser_Command_check__failure___closed__5 = _init_l_Lean_Parser_Command_check__failure___closed__5();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___closed__5);
l_Lean_Parser_Command_check__failure___closed__6 = _init_l_Lean_Parser_Command_check__failure___closed__6();
lean_mark_persistent(l_Lean_Parser_Command_check__failure___closed__6);
l_Lean_Parser_Command_check__failure = _init_l_Lean_Parser_Command_check__failure();
lean_mark_persistent(l_Lean_Parser_Command_check__failure);
res = l___regBuiltinParser_Lean_Parser_Command_check__failure(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Command_synth___elambda__1___closed__1 = _init_l_Lean_Parser_Command_synth___elambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_synth___elambda__1___closed__1);
l_Lean_Parser_Command_synth___elambda__1___closed__2 = _init_l_Lean_Parser_Command_synth___elambda__1___closed__2();

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

@ -187,6 +187,7 @@ lean_object* l___private_Init_LeanInit_10__decodeDecimalLitAux___boxed(lean_obje
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_MonadQuotation_addMacroScope___rarg___lambda__2(lean_object*, lean_object*, lean_object*, 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*);
@ -279,6 +280,7 @@ lean_object* l_Lean_Syntax_isNameLit_x3f___boxed(lean_object*);
lean_object* l___private_Init_LeanInit_12__decodeQuotedChar___boxed__const__2;
lean_object* l_Lean_mkHole___closed__1;
lean_object* l_Lean_Name_hasMacroScopes___boxed(lean_object*);
lean_object* l_Lean_MonadQuotation_addMacroScope___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isIdBeginEscape___boxed(lean_object*);
lean_object* l_Lean_mkStxStrLit(lean_object*, lean_object*);
lean_object* lean_nat_mul(lean_object*, lean_object*);
@ -341,6 +343,7 @@ lean_object* l_Lean_Name_toStringWithSep___main(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*);
uint8_t l_UInt32_decLe(uint32_t, uint32_t);
lean_object* l_Lean_MonadQuotation_addMacroScope(lean_object*);
lean_object* l_Lean_mkAppStx___closed__2;
lean_object* l_Lean_Name_hasMacroScopes___main___boxed(lean_object*);
lean_object* l_Lean_Name_hasMacroScopes___main___closed__1;
@ -355,6 +358,7 @@ lean_object* l___private_Init_LeanInit_11__decodeNatLitVal(lean_object*);
lean_object* l_Lean_Syntax_isFieldIdx_x3f___boxed(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_mkAppStx___closed__1;
lean_object* l_Lean_MonadQuotation_addMacroScope___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_LeanInit_3__extractImported___main(lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_string_hash(lean_object*);
lean_object* l___private_Init_LeanInit_1__eraseMacroScopesAux___main___boxed(lean_object*);
@ -2622,6 +2626,62 @@ return x_35;
}
}
}
lean_object* l_Lean_MonadQuotation_addMacroScope___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
lean_dec(x_5);
x_7 = l_Lean_addMacroScope(x_2, x_3, x_4);
x_8 = lean_apply_2(x_6, lean_box(0), x_7);
return x_8;
}
}
lean_object* l_Lean_MonadQuotation_addMacroScope___rarg___lambda__2(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_dec(x_1);
x_7 = lean_alloc_closure((void*)(l_Lean_MonadQuotation_addMacroScope___rarg___lambda__1), 4, 3);
lean_closure_set(x_7, 0, x_2);
lean_closure_set(x_7, 1, x_5);
lean_closure_set(x_7, 2, x_3);
x_8 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_6, x_7);
return x_8;
}
}
lean_object* l_Lean_MonadQuotation_addMacroScope___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_2, 1);
lean_inc(x_4);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_inc(x_4);
x_6 = lean_alloc_closure((void*)(l_Lean_MonadQuotation_addMacroScope___rarg___lambda__2), 5, 4);
lean_closure_set(x_6, 0, x_1);
lean_closure_set(x_6, 1, x_2);
lean_closure_set(x_6, 2, x_3);
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_MonadQuotation_addMacroScope(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_MonadQuotation_addMacroScope___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Macro_addMacroScope(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{