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-08-22 14:46:12 -07:00
parent 095d022fe2
commit 0c6c3fb3b8
42 changed files with 9578 additions and 28421 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
stage0/src/Lean/CoreM.lean generated
View file

@ -8,6 +8,7 @@ import Init.Control.StateRef
import Lean.Util.RecDepth
import Lean.Util.Trace
import Lean.Environment
import Lean.Exception
import Lean.InternalExceptionId
import Lean.Eval
@ -27,22 +28,7 @@ structure Context :=
(maxRecDepth : Nat := 1000)
(ref : Syntax := Syntax.missing)
inductive Exception
| error (ref : Syntax) (msg : MessageData)
| internal (id : InternalExceptionId)
def Exception.toMessageData : Exception → MessageData
| Exception.error _ msg => msg
| Exception.internal id => id.toString
def Exception.getRef : Exception → Syntax
| Exception.error ref _ => ref
| Exception.internal _ => Syntax.missing
instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
abbrev ECoreM (ε : Type) := ReaderT Context $ StateRefT State $ EIO ε
abbrev CoreM := ECoreM Exception
abbrev CoreM := ReaderT Context $ StateRefT State $ EIO Exception
instance CoreM.inhabited {α} : Inhabited (CoreM α) :=
⟨fun _ _ => throw $ arbitrary _⟩
@ -52,9 +38,7 @@ ctx ← read; pure ctx.ref
@[inline] def liftIOCore {α} (x : IO α) : CoreM α := do
ref ← getRef;
adaptExcept
(fun (err : IO.Error) => Exception.error ref (toString err))
(liftM x : ECoreM IO.Error α)
liftM $ (adaptExcept (fun (err : IO.Error) => Exception.error ref (toString err)) x : EIO Exception α)
instance : MonadIO CoreM :=
{ liftIO := @liftIOCore }
@ -171,10 +155,10 @@ traceState.traces.forM $ fun m => liftIO $ IO.println $ format m
def resetTraceState : CoreM Unit :=
modify fun s => { s with traceState := {} }
@[inline] def ECoreM.run {ε α} (x : ECoreM ε α) (ctx : Context) (s : State) : EIO ε (α × State) :=
@[inline] def CoreM.run {α} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
(x.run ctx).run s
@[inline] def ECoreM.run' {ε α} (x : ECoreM ε α) (ctx : Context) (s : State) : EIO ε α :=
@[inline] def CoreM.run' {α} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
Prod.fst <$> x.run ctx s
@[inline] def CoreM.toIO {α} (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) :=
@ -191,7 +175,7 @@ instance hasEval {α} [MetaHasEval α] : MetaHasEval (CoreM α) :=
end Core
export Core (CoreM Exception Exception.error Exception.internal)
export Core (CoreM)
@[inline] def catchInternalId {α} {m : Type → Type} [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exception → m α) : m α :=
catch x fun ex => match ex with

2
stage0/src/Lean/Elab/App.lean generated
View file

@ -362,7 +362,7 @@ match eType.getAppFn, lval with
| _, _ =>
throwLValError e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
private partial def resolveLValLoop (e : Expr) (lval : LVal) : Expr → Array Core.Exception → TermElabM LValResolution
private partial def resolveLValLoop (e : Expr) (lval : LVal) : Expr → Array Exception → TermElabM LValResolution
| eType, previousExceptions => do
eType ← whnfCore eType;
tryPostponeIfMVar eType;

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

@ -65,7 +65,7 @@ let scope := s.scopes.head!;
def liftCoreM {α} (x : CoreM α) : CommandElabM α := do
s ← get;
ctx ← read;
let Eα := Except Core.Exception α;
let Eα := Except Exception α;
let x : CoreM Eα := catch (do a ← x; pure $ Except.ok a) (fun ex => pure $ Except.error ex);
let x : EIO Exception (Eα × Core.State) := (ReaderT.run x (mkCoreContext ctx s)).run { env := s.env, ngen := s.ngen };
(ea, coreS) ← liftM x;

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

@ -160,7 +160,7 @@ setTraceState {};
finally (liftMetaMCore x) (liftMetaMFinalizer oldTraceState)
@[inline] def liftCoreM {α} (x : CoreM α) : TermElabM α :=
liftMetaM $ Meta.liftCoreM x
liftMetaM $ liftM x
def getEnv : TermElabM Environment := do s ← getThe Core.State; pure s.env
def getMCtx : TermElabM MetavarContext := do s ← getThe Meta.State; pure s.mctx

26
stage0/src/Lean/Exception.lean generated Normal file
View file

@ -0,0 +1,26 @@
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Message
import Lean.InternalExceptionId
namespace Lean
/- Exception type used in most Lean monads -/
inductive Exception
| error (ref : Syntax) (msg : MessageData)
| internal (id : InternalExceptionId)
def Exception.toMessageData : Exception → MessageData
| Exception.error _ msg => msg
| Exception.internal id => id.toString
def Exception.getRef : Exception → Syntax
| Exception.error ref _ => ref
| Exception.internal _ => Syntax.missing
instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
end Lean

35
stage0/src/Lean/Meta/Basic.lean generated
View file

@ -130,24 +130,19 @@ structure Context :=
(lctx : LocalContext := {})
(localInstances : LocalInstances := #[])
open Core (ECoreM Exception)
abbrev MetaM := ReaderT Context $ StateRefT State $ CoreM
@[inline] def liftCoreM {α} (x : CoreM α) : MetaM α :=
liftM $ x
@[inline] def mapCoreM (f : forall {α}, CoreM α → CoreM α) {α} : MetaM α → MetaM α :=
monadMap @f
instance : MonadIO MetaM :=
{ liftIO := fun α x => liftCoreM $ liftIO x }
{ liftIO := fun α x => liftM (liftIO x : CoreM α) }
instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
⟨fun _ _ => arbitrary _⟩
def getRef : MetaM Syntax :=
liftCoreM Core.getRef
liftM Core.getRef
def addContext (msg : MessageData) : MetaM MessageData := do
ctxCore ← readThe Core.Context;
@ -159,13 +154,13 @@ pure $ MessageData.withContext { env := sCore.env, mctx := s.mctx, lctx := ctx.l
def throwError {α} (msg : MessageData) : MetaM α := do
ref ← getRef;
msg ← addContext msg;
throw $ Core.Exception.error ref msg
throw $ Exception.error ref msg
def throwIsDefEqStuck {α} : MetaM α :=
throw $ Core.Exception.internal isDefEqStuckExceptionId
throw $ Exception.internal isDefEqStuckExceptionId
def checkRecDepth : MetaM Unit :=
liftCoreM $ Core.checkRecDepth
liftM $ Core.checkRecDepth
@[inline] def withIncRecDepth {α} (x : MetaM α) : MetaM α := do
mapCoreM (fun α => Core.withIncRecDepth) x
@ -189,25 +184,25 @@ def setMCtx (mctx : MetavarContext) : MetaM Unit :=
modify $ fun s => { s with mctx := mctx }
@[inline] def getOptions : MetaM Options :=
liftCoreM Core.getOptions
liftM Core.getOptions
@[inline] def getEnv : MetaM Environment :=
liftCoreM Core.getEnv
liftM Core.getEnv
def setEnv (env : Environment) : MetaM Unit :=
liftCoreM $ Core.setEnv env
liftM $ Core.setEnv env
def getNGen : MetaM NameGenerator :=
liftCoreM Core.getNGen
liftM Core.getNGen
def setNGen (ngen : NameGenerator) : MetaM Unit :=
liftCoreM $ Core.setNGen ngen
liftM $ Core.setNGen ngen
def getTraceState : MetaM TraceState :=
liftCoreM $ Core.getTraceState
liftM $ Core.getTraceState
def setTraceState (traceState : TraceState) : MetaM Unit :=
liftCoreM $ Core.setTraceState traceState
liftM $ Core.setTraceState traceState
def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
IO.mkRef $ fun _ => throwError "whnf implementation was not set"
@ -254,7 +249,7 @@ withIncRecDepth do
fn mvarId
def mkFreshId : MetaM Name := do
liftCoreM Core.mkFreshId
liftM Core.mkFreshId
private def mkFreshExprMVarAtCore
(mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name) (kind : MetavarKind) : MetaM Expr := do
@ -285,7 +280,7 @@ modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
pure $ mkLevelMVar mvarId
@[inline] def ofExcept {α ε} [HasToString ε] (x : Except ε α) : MetaM α :=
liftCoreM $ Core.ofExcept x
liftM $ Core.ofExcept x
@[inline] def shouldReduceAll : MetaM Bool := do
ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
@ -882,7 +877,7 @@ opts ← getOptions;
mctx ← getMCtx;
lctx ← getLCtx;
match Lean.mkAuxDefinition env opts mctx lctx name type value with
| Except.error ex => liftCoreM $ Core.throwKernelException ex
| Except.error ex => liftM $ Core.throwKernelException ex
| Except.ok (e, env, mctx) => do setEnv env; setMCtx mctx; pure e
/-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/

40
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -368,26 +368,13 @@ structure Context :=
(hasCtxLocals : Bool)
(rhs : Expr)
/-
inductive Exception
| occursCheck
| useFOApprox
| outOfScopeFVar (fvarId : FVarId)
| readOnlyMVarWithBiggerLCtx (mvarId : MVarId)
| unknownExprMVar (mvarId : MVarId)
| meta (ex : Meta.Exception)
-/
abbrev CheckAssignmentM := ReaderT Context $ StateRefT State $ MetaM
@[inline] def liftMetaM {α} (x : MetaM α) : CheckAssignmentM α :=
liftM x
def throwCheckAssignmentFailure {α} : CheckAssignmentM α :=
throw $ Core.Exception.internal checkAssignmentExceptionId
throw $ Exception.internal checkAssignmentExceptionId
def throwOutOfScopeFVar {α} : CheckAssignmentM α :=
throw $ Core.Exception.internal outOfScopeExceptionId
throw $ Exception.internal outOfScopeExceptionId
private def findCached? (e : Expr) : CheckAssignmentM (Option Expr) := do
s ← get;
@ -402,15 +389,12 @@ instance : MonadCache Expr Expr CheckAssignmentM :=
@[inline] private def visit (f : Expr → CheckAssignmentM Expr) (e : Expr) : CheckAssignmentM Expr :=
if !e.hasExprMVar && !e.hasFVar then pure e else checkCache e f
@[inline] private def readMeta : CheckAssignmentM Meta.Context := do
liftMetaM read
private def addAssignmentInfo (msg : MessageData) : CheckAssignmentM MessageData := do
ctx ← read;
pure $ msg ++ " @ " ++ mkMVar ctx.mvarId ++ " " ++ ctx.fvars ++ " := " ++ ctx.rhs
@[specialize] def checkFVar (check : Expr → CheckAssignmentM Expr) (fvar : Expr) : CheckAssignmentM Expr := do
ctxMeta ← readMeta;
ctxMeta ← readThe Meta.Context;
ctx ← read;
if ctx.mvarDecl.lctx.containsFVar fvar then pure fvar
else do
@ -424,10 +408,10 @@ else do
throwOutOfScopeFVar
@[inline] def getMCtx : CheckAssignmentM MetavarContext := do
liftMetaM Meta.getMCtx
liftM Meta.getMCtx
def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) : CheckAssignmentM Expr := do
liftMetaM $ mkFreshExprMVarAt lctx localInsts type
liftM $ mkFreshExprMVarAt lctx localInsts type
@[specialize] def checkMVar (check : Expr → CheckAssignmentM Expr) (mvar : Expr) : CheckAssignmentM Expr := do
let mvarId := mvar.mvarId!;
@ -439,7 +423,7 @@ if mvarId == ctx.mvarId then do
else match mctx.getExprAssignment? mvarId with
| some v => check v
| none => match mctx.findDecl? mvarId with
| none => liftMetaM $ throwUnknownMVar mvarId
| none => liftM $ throwUnknownMVar mvarId
| some mvarDecl =>
if ctx.hasCtxLocals then
throwCheckAssignmentFailure -- It is not a pattern, then we fail and fall back to FO unification
@ -451,14 +435,14 @@ else match mctx.getExprAssignment? mvarId with
traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx $ addAssignmentInfo (mkMVar mvarId);
throwCheckAssignmentFailure
else do
ctxMeta ← readMeta;
ctxMeta ← readThe Meta.Context;
if ctxMeta.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;
liftMetaM $ modify (fun s => { s with mctx := s.mctx.assignExpr mvarId newMVar });
modifyThe Meta.State (fun s => { s with mctx := s.mctx.assignExpr mvarId newMVar });
pure newMVar
else
pure mvar
@ -491,7 +475,7 @@ partial def check : Expr → CheckAssignmentM Expr
| e@(Expr.mvar _ _) => visit (checkMVar check) e
| Expr.localE _ _ _ _ => unreachable!
| e@(Expr.app _ _ _) => e.withApp $ fun f args => do
ctxMeta ← readMeta;
ctxMeta ← readThe Meta.Context;
if f.isMVar && ctxMeta.config.ctxApprox && args.all Expr.isFVar then do
f ← visit (checkMVar check) f;
catchInternalId outOfScopeExceptionId
@ -499,14 +483,14 @@ partial def check : Expr → CheckAssignmentM Expr
args ← args.mapM (visit check);
pure $ mkAppN f args)
(fun ex =>
condM (liftMetaM $ isDelayedAssigned f.mvarId!) (throw ex) do
eType ← liftMetaM $ inferType e;
condM (liftM $ isDelayedAssigned f.mvarId!) (throw ex) do
eType ← liftM $ 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`. -/
ctx ← read;
newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType;
condM (liftMetaM $ assignToConstFun f args.size newMVar)
condM (liftM $ assignToConstFun f args.size newMVar)
(pure newMVar)
(throw ex))
else do

19
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -154,9 +154,6 @@ structure State :=
abbrev SynthM := StateRefT State MetaM
@[inline] def liftMetaM {α} (x : MetaM α) : SynthM α :=
liftM x
@[inline] def mapMetaM (f : forall {α}, MetaM α → MetaM α) {α} : SynthM α → SynthM α :=
monadMap @f
@ -205,7 +202,7 @@ else do
def newSubgoal (mctx : MetavarContext) (key : Expr) (mvar : Expr) (waiter : Waiter) : SynthM Unit :=
withMCtx mctx $ do
trace! `Meta.synthInstance.newSubgoal key;
node? ← liftMetaM $ mkGeneratorNode? key mvar;
node? ← liftM $ mkGeneratorNode? key mvar;
match node? with
| none => pure ()
| some node =>
@ -232,8 +229,8 @@ match entry? with
We must instantiate assigned metavariables before we invoke `mkTableKey`. -/
def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : SynthM Expr :=
withMCtx mctx $ do
mvarType ← liftMetaM $ inferType mvar;
mvarType ← liftMetaM $ instantiateMVars mvarType;
mvarType ← liftM $ inferType mvar;
mvarType ← liftM $ instantiateMVars mvarType;
pure $ mkTableKey mctx mvarType
/- See `getSubgoals` and `getSubgoalsAux`
@ -317,13 +314,13 @@ forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do
If it succeeds, the result is a new updated metavariable context and a new list of subgoals.
A subgoal is created for each instance implicit parameter of `inst`. -/
def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : SynthM (Option (MetavarContext × List Expr)) :=
liftMetaM $ traceCtx `Meta.synthInstance.tryResolve $ Meta.withMCtx mctx $ tryResolveCore mvar inst
liftM $ traceCtx `Meta.synthInstance.tryResolve $ Meta.withMCtx mctx $ tryResolveCore mvar inst
/--
Assign a precomputed answer to `mvar`.
If it succeeds, the result is a new updated metavariable context and a new list of subgoals. -/
def tryAnswer (mctx : MetavarContext) (mvar : Expr) (answer : Answer) : SynthM (Option MetavarContext) :=
liftMetaM $ Meta.withMCtx mctx $ do
liftM $ Meta.withMCtx mctx $ do
(_, _, val) ← openAbstractMVarsResult answer.result;
condM (isDefEq mvar val)
(do mctx ← getMCtx; pure $ some mctx)
@ -335,7 +332,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
if answer.result.paramNames.isEmpty && answer.result.numMVars == 0 then do
modify $ fun s => { s with result := answer.result.expr }
else do
(_, _, answerExpr) ← liftMetaM $ openAbstractMVarsResult answer.result;
(_, _, answerExpr) ← liftM $ openAbstractMVarsResult answer.result;
trace! `Meta.synthInstance ("skip answer containing metavariables " ++ answerExpr);
pure ()
| Waiter.consumerNode cNode => modify $ fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
@ -359,7 +356,7 @@ Meta.withMCtx cNode.mctx do
That is, `cNode.subgoals == []`.
And then, store it in the tabled entries map, and wakeup waiters. -/
def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
answer ← liftMetaM $ mkAnswer cNode;
answer ← liftM $ mkAnswer cNode;
-- Remark: `answer` does not contain assignable or assigned metavariables.
let key := cNode.key;
entry ← getEntry key;
@ -425,7 +422,7 @@ match cNode.subgoals with
match result? with
| none => pure ()
| some mctx => do
liftMetaM $ Meta.withMCtx mctx $ traceM `Meta.synthInstance.resume $ do {
liftM $ Meta.withMCtx mctx $ traceM `Meta.synthInstance.resume $ do {
goal ← inferType cNode.mvar;
subgoal ← inferType mvar;
pure (goal ++ " <== " ++ subgoal)

5
stage0/src/Lean/PrettyPrinter.lean generated
View file

@ -13,8 +13,9 @@ namespace PrettyPrinter
def ppTerm (stx : Syntax) : CoreM Format :=
parenthesizeTerm stx >>= formatTerm
def ppExpr (e : Expr) : MetaM Format :=
delab e >>= Meta.liftCoreM ∘ ppTerm
def ppExpr (e : Expr) : MetaM Format := do
stx ← delab e;
liftM $ ppTerm stx
def ppCommand (stx : Syntax) : CoreM Format :=
parenthesizeCommand stx >>= formatCommand

17
stage0/src/Lean/PrettyPrinter/Backtrack.lean generated Normal file
View file

@ -0,0 +1,17 @@
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.InternalExceptionId
namespace Lean
namespace PrettyPrinter
/- Auxiliary internal exception for backtracking the pretty printer.
See `orelse.parenthesizer` for example -/
def registerBacktrackId : IO InternalExceptionId := registerInternalExceptionId `backtrackFormatter
@[init registerBacktrackId] constant backtrackExceptionId : InternalExceptionId := arbitrary _
end PrettyPrinter
end Lean

28
stage0/src/Lean/PrettyPrinter/Formatter.lean generated
View file

@ -17,6 +17,7 @@ import Lean.CoreM
import Lean.Parser.Extension
import Lean.KeyedDeclsAttribute
import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Backtrack
namespace Lean
namespace PrettyPrinter
@ -34,12 +35,17 @@ structure State :=
-- Note, however, that the stack is reversed because of the right-to-left traversal.
(stack : Array Format := #[])
-- see `orelse.parenthesizer`
structure BacktrackException := mk
end Formatter
abbrev FormatterM := ReaderT Formatter.Context $ StateT Formatter.State $ ExceptT Formatter.BacktrackException CoreM
abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State $ CoreM
@[inline] def FormatterM.orelse {α} (p₁ p₂ : FormatterM α) : FormatterM α := do
s ← get;
catchInternalId backtrackExceptionId
p₁
(fun _ => do set s; p₂)
instance Formatter.orelse {α} : HasOrelse (FormatterM α) := ⟨FormatterM.orelse⟩
abbrev Formatter := FormatterM Unit
@ -78,6 +84,9 @@ open Lean.Core
open Lean.Parser
open Lean.Format
def throwBacktrack {α} : FormatterM α :=
throw $ Exception.internal backtrackExceptionId
instance FormatterM.monadTraverser : Syntax.MonadTraverser FormatterM := ⟨{
get := State.stxTrav <$> get,
set := fun t => modify (fun st => { st with stxTrav := t }),
@ -240,8 +249,7 @@ def checkKind (k : SyntaxNodeKind) : FormatterM Unit := do
stx ← getCur;
when (k != stx.getKind) $ do {
trace! `PrettyPrinter.format.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
-- HACK; see `orelse.formatter`
throw ⟨⟩
throwBacktrack
}
@[combinatorFormatter Lean.Parser.node]
@ -406,9 +414,11 @@ open Formatter
def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
table ← Parser.builtinTokenTable.get;
Except.ok (_, st) ← formatter { table := table } { stxTrav := Syntax.Traverser.fromSyntax stx }
| Core.throwError "format: uncaught backtrack exception";
pure $ st.stack.get! 0
catchInternalId backtrackExceptionId
(do
(_, st) ← (formatter { table := table }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
pure $ st.stack.get! 0)
(fun _ => Core.throwError "format: uncaught backtrack exception")
def formatTerm := format $ categoryParser.formatter `term
def formatCommand := format $ categoryParser.formatter `command

34
stage0/src/Lean/PrettyPrinter/Parenthesizer.lean generated
View file

@ -75,6 +75,7 @@ import Lean.CoreM
import Lean.KeyedDeclsAttribute
import Lean.Parser.Extension
import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Backtrack
namespace Lean
namespace PrettyPrinter
@ -96,15 +97,19 @@ structure State :=
-- true iff we have already visited a token on this parser level; used for detecting trailing parsers
(visitedToken : Bool := false)
-- see `orelse.parenthesizer`
structure BacktrackException := mk
end Parenthesizer
abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateT Parenthesizer.State $ ExceptT Parenthesizer.BacktrackException CoreM
abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateRefT Parenthesizer.State $ CoreM
abbrev Parenthesizer := ParenthesizerM Unit
@[inline] def ParenthesizerM.orelse {α} (p₁ p₂ : ParenthesizerM α) : ParenthesizerM α := do
s ← get;
catchInternalId backtrackExceptionId
p₁
(fun _ => do set s; p₂)
instance Parenthesizer.orelse {α} : HasOrelse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩
unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
KeyedDeclsAttribute.init {
builtinName := `builtinParenthesizer,
@ -160,6 +165,9 @@ namespace Parenthesizer
open Lean.Core
open Lean.Format
def throwBacktrack {α} : ParenthesizerM α :=
throw $ Exception.internal backtrackExceptionId
instance ParenthesizerM.monadTraverser : Syntax.MonadTraverser ParenthesizerM := ⟨{
get := State.stxTrav <$> get,
set := fun t => modify (fun st => { st with stxTrav := t }),
@ -296,7 +304,7 @@ def term.parenthesizer : CategoryParenthesizer | prec => do
stx ← getCur;
-- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot`
if stx.getKind == nullKind then
throw ⟨⟩
throwBacktrack
else do
maybeParenthesize `term (fun stx => Unhygienic.run `(($stx))) prec $
parenthesizeCategoryCore `term prec
@ -329,7 +337,7 @@ stx ← getCur;
when (k != stx.getKind) $ do {
trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
-- HACK; see `orelse.parenthesizer`
throw ⟨⟩
throwBacktrack
};
visitArgs p
@ -352,7 +360,7 @@ stx ← getCur;
when (k != stx.getKind) $ do {
trace! `PrettyPrinter.parenthesize.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'");
-- HACK; see `orelse.parenthesizer`
throw ⟨⟩
throwBacktrack
};
visitArgs $ do {
p;
@ -439,10 +447,12 @@ end Parenthesizer
open Parenthesizer
/-- Add necessary parentheses in `stx` parsed by `parser`. -/
def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax := do
Except.ok (_, st) ← parenthesizer {} { stxTrav := Syntax.Traverser.fromSyntax stx }
| Core.throwError "parenthesize: uncaught backtrack exception";
pure st.stxTrav.cur
def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :=
catchInternalId backtrackExceptionId
(do
(_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx };
pure st.stxTrav.cur)
(fun _ => Core.throwError "parenthesize: uncaught backtrack exception")
def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0
def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command 0

4
stage0/src/Lean/Util/Sorry.lean generated
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Message
import Lean.CoreM
import Lean.Exception
namespace Lean
@ -55,7 +55,7 @@ partial def MessageData.hasSyntheticSorry : MessageData → Bool
| MessageData.node msgs => msgs.any MessageData.hasSyntheticSorry
| _ => false
def Core.Exception.hasSyntheticSorry : Exception → Bool
def Exception.hasSyntheticSorry : Exception → Bool
| Exception.error _ msg => msg.hasSyntheticSorry
| _ => false

2
stage0/src/library/abstract_context_cache.cpp generated
View file

@ -20,7 +20,7 @@ Author: Leonardo de Moura
#endif
#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 100
#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 5000
#endif
namespace lean {

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

121
stage0/stdlib/Lean/CoreM.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.CoreM
// Imports: Init Init.System.IO Init.Control.StateRef Lean.Util.RecDepth Lean.Util.Trace Lean.Environment Lean.InternalExceptionId Lean.Eval
// Imports: Init Init.System.IO Init.Control.StateRef Lean.Util.RecDepth Lean.Util.Trace Lean.Environment Lean.Exception Lean.InternalExceptionId Lean.Eval
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -16,7 +16,6 @@ extern "C" {
lean_object* l_Lean_Core_getConstInfo___closed__5;
lean_object* l_Lean_Core_throwKernelException___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_compileDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_InternalExceptionId_toString(lean_object*);
extern lean_object* l_Lean_InternalExceptionId_toString___closed__1;
lean_object* lean_io_error_to_string(lean_object*);
lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
@ -29,10 +28,8 @@ lean_object* l_Lean_Core_getEnv___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Core_replaceRef(lean_object*, lean_object*);
lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_Core_addContext(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_ECoreM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_dbg_trace(lean_object*, lean_object*);
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
lean_object* l_Lean_Core_Exception_toMessageData(lean_object*);
lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Core_Context_replaceRef___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Core_resetTraceState___rarg(lean_object*, lean_object*);
@ -71,13 +68,14 @@ lean_object* l_Lean_Core_mkFreshId___rarg___boxed(lean_object*, lean_object*);
uint8_t l_List_elem___main___at_Lean_catchInternalIds___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Core_CoreM_inhabited(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_checkRecDepth___closed__1;
extern lean_object* l_Lean_Exception_inhabited___closed__1;
lean_object* l_Lean_Core_checkRecDepth___closed__2;
lean_object* l_Lean_Core_addDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_withIncRecDepth(lean_object*);
lean_object* l_Lean_Core_tracer___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_KernelException_toMessageData(lean_object*, lean_object*);
lean_object* l_Lean_Core_CoreM_run_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_checkRecDepth(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_Exception_getRef(lean_object*);
lean_object* l_Lean_Core_getEnv___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Lean_catchInternalIds(lean_object*, lean_object*);
lean_object* l_Lean_Core_setEnv___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -87,6 +85,7 @@ lean_object* l_Lean_Core_modifyEnv___boxed(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_Core_checkRecDepth___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_resetTraceState___boxed(lean_object*);
lean_object* l_Std_PersistentArray_forMAux___main___at_Lean_Core_printTraces___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_CoreM_run(lean_object*);
lean_object* l_Nat_repr(lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
lean_object* l_Lean_Core_getNGen(lean_object*);
@ -94,7 +93,6 @@ lean_object* l_Lean_Core_dbgTrace___rarg___closed__1;
lean_object* l___private_Lean_CoreM_1__getTraceState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_catchInternalId___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_getConstInfo___closed__3;
lean_object* l_Lean_Core_ECoreM_run(lean_object*, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_Core_printTraces___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_getRef(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_replaceRef___boxed(lean_object*, lean_object*);
@ -129,6 +127,7 @@ lean_object* l_Lean_Core_throwError___rarg___boxed(lean_object*, lean_object*, l
lean_object* l_Lean_Core_throwError(lean_object*);
lean_object* l_IO_print___at_Lean_Core_printTraces___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Core_tracer___closed__4;
lean_object* l_Lean_Core_CoreM_run___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_Context_incCurrRecDepth(lean_object*);
lean_object* l_Lean_Core_getEnv___boxed(lean_object*);
lean_object* l_Lean_getMaxRecDepth(lean_object*);
@ -140,7 +139,6 @@ extern lean_object* l_Lean_EnvExtension_setState___closed__1;
lean_object* l_Lean_Core_getTraceState(lean_object*);
lean_object* l_Lean_Core_getOptions(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_addDecl(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_Exception_inhabited___closed__1;
lean_object* l_Lean_Core_tracer___closed__1;
lean_object* l_Lean_Core_CoreM_toIO(lean_object*);
lean_object* l_Lean_Syntax_getPos(lean_object*);
@ -155,7 +153,6 @@ lean_object* l_Lean_catchInternalId(lean_object*, lean_object*);
lean_object* l_Lean_Core_hasEval___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_Array_forMAux___main___at_Lean_Core_printTraces___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_tracer___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_ECoreM_run_x27(lean_object*, lean_object*);
lean_object* l_Lean_catchInternalId___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_setTraceState(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_tracer___closed__2;
@ -163,20 +160,17 @@ lean_object* l_Lean_Core_liftIOCore(lean_object*);
lean_object* l_List_elem___main___at_Lean_catchInternalIds___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_MetavarContext_Inhabited___closed__1;
lean_object* l_Lean_Core_getConstInfo___closed__4;
lean_object* l_Lean_Core_CoreM_run_x27(lean_object*);
lean_object* lean_compile_decl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_Exception_inhabited;
lean_object* l_Lean_Core_setNGen___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_getTraceState___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Core_MonadIO___closed__1;
lean_object* l_Lean_catchInternalId___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_addContext___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_MessageData_Inhabited___closed__1;
lean_object* l_Lean_Core_ECoreM_run_x27___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_dbgTrace___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_Core_addAndCompile(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_getNGen___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Core_Exception_getRef___boxed(lean_object*);
lean_object* l_Lean_Core_CoreM_toIO___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_CoreM_1__getTraceState___boxed(lean_object*);
lean_object* l_Lean_Core_liftIOCore___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -206,84 +200,11 @@ x_1 = l_Lean_Core_State_inhabited___closed__1;
return x_1;
}
}
lean_object* l_Lean_Core_Exception_toMessageData(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
lean_dec(x_1);
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_InternalExceptionId_toString(x_3);
x_5 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
}
}
lean_object* l_Lean_Core_Exception_getRef(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
}
lean_object* l_Lean_Core_Exception_getRef___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Core_Exception_getRef(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Core_Exception_inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_MessageData_Inhabited___closed__1;
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_Core_Exception_inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Core_Exception_inhabited___closed__1;
return x_1;
}
}
lean_object* l_Lean_Core_CoreM_inhabited___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_inhabited___closed__1;
x_2 = l_Lean_Exception_inhabited___closed__1;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -2630,7 +2551,7 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Core_ECoreM_run___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Core_CoreM_run___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
@ -2705,15 +2626,15 @@ return x_22;
}
}
}
lean_object* l_Lean_Core_ECoreM_run(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Core_CoreM_run(lean_object* x_1) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_Core_ECoreM_run___rarg), 4, 0);
return x_3;
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Core_CoreM_run___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Core_ECoreM_run_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Lean_Core_CoreM_run_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
@ -2781,12 +2702,12 @@ return x_19;
}
}
}
lean_object* l_Lean_Core_ECoreM_run_x27(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Core_CoreM_run_x27(lean_object* x_1) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Lean_Core_ECoreM_run_x27___rarg), 4, 0);
return x_3;
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Core_CoreM_run_x27___rarg), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Core_CoreM_toIO___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@ -3307,6 +3228,7 @@ lean_object* initialize_Init_Control_StateRef(lean_object*);
lean_object* initialize_Lean_Util_RecDepth(lean_object*);
lean_object* initialize_Lean_Util_Trace(lean_object*);
lean_object* initialize_Lean_Environment(lean_object*);
lean_object* initialize_Lean_Exception(lean_object*);
lean_object* initialize_Lean_InternalExceptionId(lean_object*);
lean_object* initialize_Lean_Eval(lean_object*);
static bool _G_initialized = false;
@ -3332,6 +3254,9 @@ lean_dec_ref(res);
res = initialize_Lean_Environment(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Exception(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_InternalExceptionId(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
@ -3342,10 +3267,6 @@ l_Lean_Core_State_inhabited___closed__1 = _init_l_Lean_Core_State_inhabited___cl
lean_mark_persistent(l_Lean_Core_State_inhabited___closed__1);
l_Lean_Core_State_inhabited = _init_l_Lean_Core_State_inhabited();
lean_mark_persistent(l_Lean_Core_State_inhabited);
l_Lean_Core_Exception_inhabited___closed__1 = _init_l_Lean_Core_Exception_inhabited___closed__1();
lean_mark_persistent(l_Lean_Core_Exception_inhabited___closed__1);
l_Lean_Core_Exception_inhabited = _init_l_Lean_Core_Exception_inhabited();
lean_mark_persistent(l_Lean_Core_Exception_inhabited);
l_Lean_Core_MonadIO___closed__1 = _init_l_Lean_Core_MonadIO___closed__1();
lean_mark_persistent(l_Lean_Core_MonadIO___closed__1);
l_Lean_Core_MonadIO = _init_l_Lean_Core_MonadIO();

20
stage0/stdlib/Lean/Elab/App.c generated
View file

@ -77,7 +77,6 @@ lean_object* l___private_Lean_Elab_App_5__getForallBody(lean_object*, lean_objec
lean_object* l___private_Lean_Elab_App_14__resolveLValLoop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Term_elabApp___closed__1;
lean_object* l_Lean_Core_Exception_toMessageData(lean_object*);
uint8_t l___private_Lean_Elab_App_9__nextArgIsHole(lean_object*);
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_12__throwLValError___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -182,7 +181,6 @@ lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_5__getForallBody___main(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_17__addLValArg___main___closed__6;
lean_object* l_Lean_Core_Exception_getRef(lean_object*);
lean_object* l___private_Lean_Elab_App_4__tryCoeFun___closed__5;
lean_object* l_Lean_Elab_Term_elabTerm(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_logException(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -325,6 +323,7 @@ lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__10;
lean_object* l_Lean_Elab_Term_whnfCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_25__elabAppAux___closed__1;
lean_object* l___private_Lean_Elab_App_13__resolveLValAux___closed__20;
lean_object* l_Lean_Exception_getRef(lean_object*);
lean_object* l___private_Lean_Elab_App_4__tryCoeFun___closed__2;
lean_object* l___private_Lean_Elab_App_12__throwLValError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_App_20__elabAppFnId___spec__1___rarg(lean_object*);
@ -426,6 +425,7 @@ uint8_t l_Lean_isStructure(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_11__elabAppArgs___closed__2;
lean_object* l___private_Lean_Elab_App_11__elabAppArgs(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_App_10__elabAppArgsAux___main___closed__7;
lean_object* l_Lean_Exception_toMessageData(lean_object*);
lean_object* l___private_Lean_Elab_App_21__elabAppFn___main___closed__3;
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_Arg_inhabited;
@ -13176,14 +13176,14 @@ if (x_10 == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_9, 0);
x_12 = l_Lean_Core_Exception_getRef(x_1);
x_12 = l_Lean_Exception_getRef(x_1);
x_13 = l_Lean_Syntax_getPos(x_12);
lean_dec(x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14;
lean_dec(x_11);
x_14 = l_Lean_Core_Exception_toMessageData(x_1);
x_14 = l_Lean_Exception_toMessageData(x_1);
lean_ctor_set(x_9, 0, x_14);
return x_9;
}
@ -13226,7 +13226,7 @@ x_30 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__8;
x_31 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
x_32 = l_Lean_Core_Exception_toMessageData(x_1);
x_32 = l_Lean_Exception_toMessageData(x_1);
x_33 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
@ -13237,7 +13237,7 @@ else
{
lean_object* x_34;
lean_dec(x_15);
x_34 = l_Lean_Core_Exception_toMessageData(x_1);
x_34 = l_Lean_Exception_toMessageData(x_1);
lean_ctor_set(x_9, 0, x_34);
return x_9;
}
@ -13251,14 +13251,14 @@ x_36 = lean_ctor_get(x_9, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_dec(x_9);
x_37 = l_Lean_Core_Exception_getRef(x_1);
x_37 = l_Lean_Exception_getRef(x_1);
x_38 = l_Lean_Syntax_getPos(x_37);
lean_dec(x_37);
if (lean_obj_tag(x_38) == 0)
{
lean_object* x_39; lean_object* x_40;
lean_dec(x_35);
x_39 = l_Lean_Core_Exception_toMessageData(x_1);
x_39 = l_Lean_Exception_toMessageData(x_1);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_36);
@ -13303,7 +13303,7 @@ x_56 = l_Lean_Meta_SynthInstance_getInstances___lambda__1___closed__8;
x_57 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
x_58 = l_Lean_Core_Exception_toMessageData(x_1);
x_58 = l_Lean_Exception_toMessageData(x_1);
x_59 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
@ -13316,7 +13316,7 @@ else
{
lean_object* x_61; lean_object* x_62;
lean_dec(x_41);
x_61 = l_Lean_Core_Exception_toMessageData(x_1);
x_61 = l_Lean_Exception_toMessageData(x_1);
x_62 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_62, 0, x_61);
lean_ctor_set(x_62, 1, x_36);

6
stage0/stdlib/Lean/Elab/Command.c generated
View file

@ -250,6 +250,7 @@ lean_object* l_Lean_Elab_Command_elabCheck___boxed(lean_object*, lean_object*, l
lean_object* l_Lean_Elab_Command_Lean_Elab_MonadMacroAdapter___closed__9;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEvalUnsafe___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Exception_inhabited___closed__1;
extern lean_object* l_Lean_EnvExtension_Inhabited___rarg___closed__1;
extern lean_object* l_Lean_Core_checkRecDepth___closed__2;
lean_object* l_Lean_getOptionDecl(lean_object*, lean_object*);
@ -520,7 +521,6 @@ lean_object* l_Lean_Elab_Command_mkCommandElabAttribute___closed__2;
lean_object* l_Std_PersistentHashMap_findAtAux___main___at_Lean_Elab_Command_elabCommand___main___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elbChoice___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabNamespace(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Core_Exception_inhabited___closed__1;
lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_elabOpen(lean_object*);
lean_object* l___private_Lean_Elab_Command_4__getVarDecls___boxed(lean_object*);
@ -5861,7 +5861,7 @@ lean_object* _init_l_Lean_Elab_Command_CommandElabM_inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Core_Exception_inhabited___closed__1;
x_1 = l_Lean_Exception_inhabited___closed__1;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Command_CommandElabM_inhabited___lambda__1___boxed), 4, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -15194,7 +15194,7 @@ lean_object* l_Lean_Elab_Command_elabEval___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_inhabited___closed__1;
x_2 = l_Lean_Exception_inhabited___closed__1;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);

4
stage0/stdlib/Lean/Elab/Inductive.c generated
View file

@ -150,6 +150,7 @@ lean_object* l___private_Lean_Elab_Inductive_11__checkHeaders___main(lean_object
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_32__applyInferMod___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_restoreSynthInstanceCache(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at___private_Lean_Elab_Inductive_31__mkCtor2InferMod___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___closed__10;
lean_object* l_List_map___main___at___private_Lean_Elab_Inductive_32__applyInferMod___spec__1___closed__1;
lean_object* l___private_Lean_Elab_Inductive_14__withInductiveLocalDecls___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldlM___main___at___private_Lean_Elab_Inductive_22__collectUniverses___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -247,7 +248,6 @@ lean_object* l___private_Lean_Elab_Inductive_33__mkInductiveDecl(lean_object*, l
lean_object* l___private_Lean_Elab_Inductive_23__updateResultingUniverse___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Inductive_23__updateResultingUniverse___closed__1;
lean_object* l_Lean_Core_Context_replaceRef(lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Formatter_checkKind___closed__11;
lean_object* l___private_Lean_Elab_Inductive_19__getResultingUniverse___closed__1;
lean_object* l_Lean_Elab_Command_shouldInferResultUniverse___closed__2;
lean_object* l_Lean_Elab_Command_accLevelAtCtor___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -2552,7 +2552,7 @@ x_74 = l___private_Lean_Elab_Inductive_9__checkParamsAndResultType___main___clos
x_75 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_75, 0, x_74);
lean_ctor_set(x_75, 1, x_73);
x_76 = l_Lean_PrettyPrinter_Formatter_checkKind___closed__11;
x_76 = l_Lean_PrettyPrinter_Formatter_checkKind___closed__10;
x_77 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_77, 0, x_75);
lean_ctor_set(x_77, 1, x_76);

26
stage0/stdlib/Lean/Elab/Match.c generated
View file

@ -41,6 +41,7 @@ lean_object* l_Lean_mkSort(lean_object*);
lean_object* l_Lean_Elab_Term_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_37__mkNewDiscrs___main___closed__4;
lean_object* l_Std_RBNode_insert___at_Lean_NameSet_insert___spec__1(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_12__addAssignmentInfo___closed__4;
lean_object* l___private_Init_LeanInit_14__mapSepElemsMAux___main___at___private_Lean_Elab_Match_20__collect___main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabMatch(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
@ -116,6 +117,7 @@ lean_object* lean_io_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabMatchAltView___lambda__1___closed__1;
lean_object* l_Lean_annotation_x3f(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Match_41__expandMatchDiscr_x3f___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
lean_object* l___private_Lean_Elab_Match_20__collect___main___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabInaccessible(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_Monad___rarg(lean_object*);
@ -133,7 +135,6 @@ lean_object* l___private_Lean_Elab_Match_40__mkNewAlts(lean_object*, lean_object
lean_object* l_Lean_MessageData_ofList(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at___private_Lean_Elab_Match_13__getNumExplicitCtorParams___spec__5___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__1;
lean_object* l___private_Lean_Elab_Match_22__withPatternVarsAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
@ -390,7 +391,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_expandMacros
extern lean_object* l_Lean_nullKind___closed__2;
lean_object* l_Array_findIdxAux___main___at___private_Lean_Elab_Match_29__mkLocalDeclFor___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_List_toString___at_Lean_Elab_Term_elabMatchAltView___spec__1(lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_13__addAssignmentInfo___closed__4;
extern lean_object* l_Lean_Meta_mkEqRefl___closed__2;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___lambda__1___closed__5;
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Match_32__elabMatchAux___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -494,7 +494,6 @@ lean_object* l___private_Lean_Elab_Match_35__mkMatchType___main___closed__4;
lean_object* l___private_Lean_Elab_Match_3__expandMatchOptTypeAux___main___closed__4;
lean_object* l_Lean_Parser_registerBuiltinNodeKind(lean_object*, lean_object*);
extern lean_object* l_Lean_mkHole___closed__1;
lean_object* l_Lean_Elab_Term_expandMacrosInPatterns___closed__3;
lean_object* l___regBuiltin_Lean_Elab_Term_elabMatch___closed__1;
lean_object* l___private_Lean_Elab_Match_9__registerAuxiliaryNodeKind___closed__1;
lean_object* l_Array_umapMAux___main___at___private_Lean_Elab_Match_31__withElaboratedLHS___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1797,7 +1796,7 @@ x_79 = l___private_Lean_Elab_Match_6__elabDiscrsAux___main___closed__16;
x_80 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_78);
x_81 = l___private_Lean_Meta_ExprDefEq_13__addAssignmentInfo___closed__4;
x_81 = l___private_Lean_Meta_ExprDefEq_12__addAssignmentInfo___closed__4;
x_82 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_82, 0, x_80);
lean_ctor_set(x_82, 1, x_81);
@ -2561,7 +2560,7 @@ lean_object* _init_l_Lean_Elab_Term_expandMacrosInPatterns___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__1;
x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
@ -2575,15 +2574,6 @@ x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Elab_Term_expandMacrosInPatterns___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_expandMacrosInPatterns___closed__2;
x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Term_expandMacrosInPatterns(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -2596,8 +2586,8 @@ lean_inc(x_11);
lean_dec(x_9);
x_12 = x_1;
x_13 = l_Lean_MetavarContext_MkBinding_mkBinding___closed__1;
x_14 = l_Lean_Elab_Term_expandMacrosInPatterns___closed__1;
x_15 = l_Lean_Elab_Term_expandMacrosInPatterns___closed__3;
x_14 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
x_15 = l_Lean_Elab_Term_expandMacrosInPatterns___closed__2;
x_16 = lean_unsigned_to_nat(0u);
x_17 = lean_alloc_closure((void*)(l_Array_umapMAux___main___at_Lean_Elab_Term_expandMacrosInPatterns___spec__3), 13, 6);
lean_closure_set(x_17, 0, x_13);
@ -6251,7 +6241,7 @@ lean_object* _init_l___private_Lean_Elab_Match_16__processIdAux___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Term_expandMacrosInPatterns___closed__3;
x_1 = l_Lean_Elab_Term_expandMacrosInPatterns___closed__2;
x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
@ -27102,8 +27092,6 @@ l_Lean_Elab_Term_expandMacrosInPatterns___closed__1 = _init_l_Lean_Elab_Term_exp
lean_mark_persistent(l_Lean_Elab_Term_expandMacrosInPatterns___closed__1);
l_Lean_Elab_Term_expandMacrosInPatterns___closed__2 = _init_l_Lean_Elab_Term_expandMacrosInPatterns___closed__2();
lean_mark_persistent(l_Lean_Elab_Term_expandMacrosInPatterns___closed__2);
l_Lean_Elab_Term_expandMacrosInPatterns___closed__3 = _init_l_Lean_Elab_Term_expandMacrosInPatterns___closed__3();
lean_mark_persistent(l_Lean_Elab_Term_expandMacrosInPatterns___closed__3);
l_Lean_Elab_Term_mkInaccessible___closed__1 = _init_l_Lean_Elab_Term_mkInaccessible___closed__1();
lean_mark_persistent(l_Lean_Elab_Term_mkInaccessible___closed__1);
l_Lean_Elab_Term_mkInaccessible___closed__2 = _init_l_Lean_Elab_Term_mkInaccessible___closed__2();

22
stage0/stdlib/Lean/Elab/StructInst.c generated
View file

@ -112,6 +112,7 @@ extern lean_object* l___private_Lean_Elab_Quotation_4__getHeadInfo___elambda__3_
lean_object* l_List_foldlM___main___at___private_Lean_Elab_StructInst_24__elabStruct___main___spec__1___closed__2;
lean_object* l_Lean_Elab_Term_StructInst_FieldLHS_inhabited___closed__1;
lean_object* l___private_Lean_Elab_StructInst_16__mkSubstructSource___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__3;
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_10__expandParentFields___spec__2___closed__5;
@ -135,7 +136,6 @@ lean_object* l_Nat_max(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_List_mapM___main___at___private_Lean_Elab_StructInst_10__expandParentFields___spec__2___closed__3;
extern lean_object* l_Lean_formatKVMap___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__1;
extern lean_object* l_Lean_Name_inhabited;
extern lean_object* l_Lean_Expr_getAppArgs___closed__1;
lean_object* l_Lean_Elab_Term_StructInst_formatField(lean_object*, lean_object*);
@ -480,7 +480,6 @@ lean_object* l___private_Lean_Elab_StructInst_4__elabModifyOp___closed__21;
lean_object* l___private_Lean_Elab_StructInst_14__getFieldIdx(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_5__getStructName___rarg___closed__5;
lean_object* l_Lean_Core_setTraceState(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_17__groupFields___closed__4;
lean_object* l_Lean_Elab_Term_getOptions___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_StructInst_18__addMissingFields___at___private_Lean_Elab_StructInst_19__expandStruct___main___spec__10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_Elab_Term_StructInst_formatStruct___main___spec__1___closed__1;
@ -14639,7 +14638,7 @@ lean_object* _init_l___private_Lean_Elab_StructInst_17__groupFields___closed__1(
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__1;
x_1 = l_Lean_PrettyPrinter_Formatter_categoryParser_formatter___closed__2;
x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
@ -14662,15 +14661,6 @@ x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
}
lean_object* _init_l___private_Lean_Elab_StructInst_17__groupFields___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_17__groupFields___closed__3;
x_2 = l_ReaderT_Monad___rarg(x_1);
return x_2;
}
}
lean_object* l___private_Lean_Elab_StructInst_17__groupFields(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:
{
@ -14686,7 +14676,7 @@ lean_inc(x_13);
lean_inc(x_11);
x_14 = l_Lean_getStructureFields(x_11, x_13);
x_15 = l_Lean_Elab_Term_StructInst_Struct_ref(x_2);
x_16 = l___private_Lean_Elab_StructInst_17__groupFields___closed__4;
x_16 = l___private_Lean_Elab_StructInst_17__groupFields___closed__3;
lean_inc(x_15);
lean_inc(x_2);
x_17 = lean_alloc_closure((void*)(l___private_Lean_Elab_StructInst_17__groupFields___lambda__4), 15, 7);
@ -15108,7 +15098,7 @@ lean_closure_set(x_17, 5, x_14);
lean_closure_set(x_17, 6, x_1);
x_18 = l_Lean_Core_Context_replaceRef(x_15, x_7);
lean_dec(x_15);
x_19 = l___private_Lean_Elab_StructInst_17__groupFields___closed__4;
x_19 = l___private_Lean_Elab_StructInst_17__groupFields___closed__3;
x_20 = lean_unsigned_to_nat(0u);
x_21 = l_Array_iterateMAux___main___rarg(x_19, lean_box(0), x_14, x_17, x_20, x_16);
x_22 = lean_apply_7(x_21, x_3, x_4, x_5, x_6, x_18, x_8, x_12);
@ -24207,7 +24197,7 @@ lean_object* _init_l_Lean_Elab_Term_StructInst_DefaultFields_step___main___close
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_StructInst_17__groupFields___closed__4;
x_1 = l___private_Lean_Elab_StructInst_17__groupFields___closed__3;
x_2 = l_StateT_Monad___rarg(x_1);
return x_2;
}
@ -26221,8 +26211,6 @@ l___private_Lean_Elab_StructInst_17__groupFields___closed__2 = _init_l___private
lean_mark_persistent(l___private_Lean_Elab_StructInst_17__groupFields___closed__2);
l___private_Lean_Elab_StructInst_17__groupFields___closed__3 = _init_l___private_Lean_Elab_StructInst_17__groupFields___closed__3();
lean_mark_persistent(l___private_Lean_Elab_StructInst_17__groupFields___closed__3);
l___private_Lean_Elab_StructInst_17__groupFields___closed__4 = _init_l___private_Lean_Elab_StructInst_17__groupFields___closed__4();
lean_mark_persistent(l___private_Lean_Elab_StructInst_17__groupFields___closed__4);
l___private_Lean_Elab_StructInst_20__mkCtorHeaderAux___main___closed__1 = _init_l___private_Lean_Elab_StructInst_20__mkCtorHeaderAux___main___closed__1();
lean_mark_persistent(l___private_Lean_Elab_StructInst_20__mkCtorHeaderAux___main___closed__1);
l___private_Lean_Elab_StructInst_20__mkCtorHeaderAux___main___closed__2 = _init_l___private_Lean_Elab_StructInst_20__mkCtorHeaderAux___main___closed__2();

4
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

@ -366,6 +366,7 @@ lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__89;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__47;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax___closed__5;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
lean_object* l___private_Lean_Elab_Syntax_7__elabKind___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax___closed__14;
lean_object* l_Nat_pred(lean_object*);
@ -395,7 +396,6 @@ lean_object* l_Lean_Elab_Command_expandElab___closed__23;
extern lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__1;
lean_object* l___private_Lean_Elab_Syntax_6__declareSyntaxCatQuotParser___closed__42;
extern lean_object* l___private_Lean_Elab_Util_4__regTraceClasses___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__52;
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_quot___elambda__1___closed__1;
@ -744,7 +744,7 @@ lean_dec(x_6);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9;
x_9 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__12;
x_9 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
return x_9;
}
else

4
stage0/stdlib/Lean/Elab/Tactic/Induction.c generated
View file

@ -18,6 +18,7 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_5__getGeneralizingFVarIds___
extern lean_object* l_Lean_Core_getConstInfo___closed__5;
lean_object* l_Lean_Elab_Tactic_evalCases(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Name_toString___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__28;
lean_object* l_Nat_foldMAux___main___at___private_Lean_Elab_Tactic_Induction_14__getRecInfo___spec__2___closed__2;
lean_object* l___private_Lean_Elab_Tactic_Induction_13__getRecInfoDefault___closed__1;
lean_object* l___private_Lean_Elab_Tactic_Induction_17__checkCasesResultAux___main___closed__3;
@ -219,7 +220,6 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_16__processResult___closed__
lean_object* l___private_Lean_Elab_Tactic_Induction_16__processResult___closed__1;
uint8_t l_Lean_Syntax_isOfKind(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__29;
extern lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main___closed__2;
lean_object* l_Lean_Elab_Tactic_getRecFromUsing___closed__4;
extern lean_object* l_Lean_mkHole___closed__2;
@ -7126,7 +7126,7 @@ lean_ctor_set(x_38, 0, x_37);
x_39 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_39, 0, x_35);
lean_ctor_set(x_39, 1, x_38);
x_40 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__29;
x_40 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__28;
x_41 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);

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

@ -330,6 +330,7 @@ lean_object* l_Lean_Elab_Term_elabByTactic(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_Elab_Term_observing(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkLet___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_withoutMacroStackAtErr(lean_object*);
extern lean_object* l_Lean_Exception_inhabited___closed__1;
lean_object* l_Lean_Elab_Term_withMacroExpansion(lean_object*);
lean_object* l_Lean_Elab_Term_getMessageLog(lean_object*);
lean_object* l_Lean_Elab_Term_State_inhabited___closed__1;
@ -395,6 +396,7 @@ lean_object* l_Lean_Elab_Term_getFVarLocalDecl_x21(lean_object*, lean_object*, l
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabTacticBlock___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_levelMVarToParam___lambda__1___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Exception_hasSyntheticSorry(lean_object*);
lean_object* l_Lean_SMap_empty___at_Lean_Elab_Term_termElabAttribute___spec__1___closed__1;
lean_object* l_Lean_Elab_Term_withTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_getMVarDecl___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -495,7 +497,6 @@ lean_object* l_Lean_Elab_Term_withLocalDecl___rarg(lean_object*, uint8_t, lean_o
lean_object* l_Lean_Elab_Term_getMainModule(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_mkTermElabAttribute(lean_object*);
lean_object* l___private_Lean_Elab_Term_27__mkConsts(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Core_Exception_hasSyntheticSorry(lean_object*);
extern lean_object* l_Lean_numLitKind___closed__2;
lean_object* l_Lean_Elab_Term_SavedState_inhabited___closed__1;
lean_object* l_Lean_Elab_Term_elabTacticBlock___closed__2;
@ -743,7 +744,6 @@ lean_object* l_Lean_Elab_Term_setNGen___boxed(lean_object*, lean_object*, lean_o
lean_object* l_Lean_Elab_Term_modifyEnv___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_resolveGlobalName___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Elab_Term_18__isLambdaWithImplicit(lean_object*);
extern lean_object* l_Lean_Core_Exception_inhabited___closed__1;
lean_object* l_Lean_Elab_Term_expandArrayLit___closed__6;
lean_object* l_Lean_Elab_Term_MonadIO(lean_object*);
lean_object* l_Lean_Elab_Term_logException___closed__2;
@ -1050,7 +1050,7 @@ lean_object* _init_l_Lean_Elab_Term_TermElabM_inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Core_Exception_inhabited___closed__1;
x_1 = l_Lean_Exception_inhabited___closed__1;
x_2 = lean_alloc_closure((void*)(l_Lean_Elab_Term_TermElabM_inhabited___lambda__1___boxed), 8, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
@ -14920,7 +14920,7 @@ x_21 = l_Lean_Meta_mkSorry___closed__2;
x_22 = l_Lean_mkConst(x_21, x_20);
x_23 = l_Lean_Meta_mkSorry___closed__4;
x_24 = l_Lean_mkAppB(x_22, x_13, x_23);
x_25 = l_Lean_Core_Exception_hasSyntheticSorry(x_1);
x_25 = l_Lean_Exception_hasSyntheticSorry(x_1);
if (x_25 == 0)
{
lean_object* x_26;
@ -15006,7 +15006,7 @@ x_39 = l_Lean_Meta_mkSorry___closed__2;
x_40 = l_Lean_mkConst(x_39, x_38);
x_41 = l_Lean_Meta_mkSorry___closed__4;
x_42 = l_Lean_mkAppB(x_40, x_13, x_41);
x_43 = l_Lean_Core_Exception_hasSyntheticSorry(x_1);
x_43 = l_Lean_Exception_hasSyntheticSorry(x_1);
if (x_43 == 0)
{
lean_object* x_44;
@ -15139,7 +15139,7 @@ x_64 = l_Lean_Meta_mkSorry___closed__2;
x_65 = l_Lean_mkConst(x_64, x_63);
x_66 = l_Lean_Meta_mkSorry___closed__4;
x_67 = l_Lean_mkAppB(x_65, x_57, x_66);
x_68 = l_Lean_Core_Exception_hasSyntheticSorry(x_1);
x_68 = l_Lean_Exception_hasSyntheticSorry(x_1);
if (x_68 == 0)
{
lean_object* x_69;
@ -15225,7 +15225,7 @@ x_82 = l_Lean_Meta_mkSorry___closed__2;
x_83 = l_Lean_mkConst(x_82, x_81);
x_84 = l_Lean_Meta_mkSorry___closed__4;
x_85 = l_Lean_mkAppB(x_83, x_57, x_84);
x_86 = l_Lean_Core_Exception_hasSyntheticSorry(x_1);
x_86 = l_Lean_Exception_hasSyntheticSorry(x_1);
if (x_86 == 0)
{
lean_object* x_87;

121
stage0/stdlib/Lean/Exception.c generated Normal file
View file

@ -0,0 +1,121 @@
// Lean compiler output
// Module: Lean.Exception
// Imports: Init Lean.Message Lean.InternalExceptionId
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_InternalExceptionId_toString(lean_object*);
lean_object* l_Lean_Exception_inhabited;
lean_object* l_Lean_Exception_inhabited___closed__1;
lean_object* l_Lean_Exception_getRef___boxed(lean_object*);
lean_object* l_Lean_Exception_getRef(lean_object*);
extern lean_object* l_Lean_MessageData_Inhabited___closed__1;
lean_object* l_Lean_Exception_toMessageData(lean_object*);
lean_object* l_Lean_Exception_toMessageData(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
lean_dec(x_1);
return x_2;
}
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_InternalExceptionId_toString(x_3);
x_5 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
}
}
lean_object* l_Lean_Exception_getRef(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
return x_2;
}
else
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
}
}
lean_object* l_Lean_Exception_getRef___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Exception_getRef(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Exception_inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_MessageData_Inhabited___closed__1;
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_Exception_inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Exception_inhabited___closed__1;
return x_1;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Message(lean_object*);
lean_object* initialize_Lean_InternalExceptionId(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Exception(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Message(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_InternalExceptionId(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Exception_inhabited___closed__1 = _init_l_Lean_Exception_inhabited___closed__1();
lean_mark_persistent(l_Lean_Exception_inhabited___closed__1);
l_Lean_Exception_inhabited = _init_l_Lean_Exception_inhabited();
lean_mark_persistent(l_Lean_Exception_inhabited);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

33
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -46,7 +46,6 @@ lean_object* l_Lean_LocalDecl_userName(lean_object*);
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MetavarContext_instantiateMVars(lean_object*, lean_object*);
lean_object* l_Lean_Meta_liftCoreM(lean_object*);
lean_object* l_Lean_Meta_InfoCacheKey_Inhabited;
extern lean_object* l_Lean_InternalExceptionId_toString___closed__1;
lean_object* l_Lean_Meta_getEnv(lean_object*, lean_object*, lean_object*);
@ -159,7 +158,6 @@ lean_object* l_Lean_Meta_setTraceState(lean_object*, lean_object*, lean_object*,
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive_x3f___main___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkAuxDefinition(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_liftCoreM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withTransparency___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_setEnv(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_2__liftMkBindingM___rarg___closed__3;
@ -210,6 +208,7 @@ lean_object* l_Lean_Meta_mkSynthPendingRef(lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwIsDefEqStuck(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getEnv___rarg___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Exception_inhabited___closed__1;
lean_object* l_Lean_Meta_mkWHNFRef___lambda__1___closed__1;
lean_object* l_Lean_Meta_MetaM_toIO(lean_object*);
lean_object* l_Lean_Meta_withMVarContext___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -421,13 +420,11 @@ lean_object* l_Lean_LocalContext_addDecl(lean_object*, lean_object*);
lean_object* l_Array_isEqvAux___main___at_Lean_Meta_withLocalContext___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_instantiateLocalDeclMVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqAuxRef;
extern lean_object* l_Lean_Core_Exception_inhabited___closed__1;
lean_object* l_Lean_Meta_throwError___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_TransparencyMode_HasBeq;
lean_object* l_Lean_Meta_lambdaTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getExprMVarAssignment_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_6__forallMetaTelescopeReducingAux(uint8_t, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_liftCoreM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDeclD___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_assignLevelMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withReducible___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1051,32 +1048,6 @@ x_1 = l_Lean_Meta_State_inhabited___closed__5;
return x_1;
}
}
lean_object* l_Lean_Meta_liftCoreM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = lean_apply_3(x_1, x_4, x_5, x_6);
return x_7;
}
}
lean_object* l_Lean_Meta_liftCoreM(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_liftCoreM___rarg___boxed), 6, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_liftCoreM___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_Meta_liftCoreM___rarg(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
lean_object* l_Lean_Meta_mapCoreM(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -1187,7 +1158,7 @@ lean_object* l_Lean_Meta_MetaM_inhabited___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_inhabited___closed__1;
x_2 = l_Lean_Exception_inhabited___closed__1;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);

4
stage0/stdlib/Lean/Meta/Check.c generated
View file

@ -28,7 +28,6 @@ lean_object* lean_environment_find(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_addContext(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
lean_object* l_Lean_Core_Exception_toMessageData(lean_object*);
lean_object* l___private_Lean_Meta_Check_2__checkLambdaLet___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_Monad___rarg(lean_object*);
lean_object* l_Array_forMAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -120,6 +119,7 @@ lean_object* l___private_Lean_Meta_Check_5__getFunctionDomain(lean_object*, lean
lean_object* l___private_Lean_Meta_Check_2__checkLambdaLet___at___private_Lean_Meta_Check_7__checkAux___main___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Check_2__checkLambdaLet(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_check(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Exception_toMessageData(lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_Lean_Meta_getFVarLocalDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_KernelException_toMessageData___closed__39;
@ -5039,7 +5039,7 @@ lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_33 = lean_ctor_get(x_22, 1);
lean_inc(x_33);
lean_dec(x_22);
x_34 = l_Lean_Core_Exception_toMessageData(x_7);
x_34 = l_Lean_Exception_toMessageData(x_7);
x_35 = l_Lean_MonadTracerAdapter_addTrace___at_Lean_Meta_isTypeCorrect___spec__1(x_21, x_34, x_2, x_3, x_4, x_5, x_33);
lean_dec(x_5);
lean_dec(x_4);

6
stage0/stdlib/Lean/Meta/EqnCompiler/Match.c generated
View file

@ -31,6 +31,7 @@ lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l___private_Lean_Meta_EqnCompiler_Match_23__unify_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Lean_Meta_EqnCompiler_Match_6__hasAsPattern(lean_object*);
lean_object* l_Lean_mkSort(lean_object*);
extern lean_object* l___private_Lean_Meta_ExprDefEq_12__addAssignmentInfo___closed__4;
lean_object* l_List_map___main___at_Lean_Meta_Match_Example_applyFVarSubst___main___spec__2(lean_object*, lean_object*);
lean_object* l_List_map___main___at___private_Lean_Meta_EqnCompiler_Match_24__expandVarIntoCtor_x3f___spec__3(lean_object*, lean_object*);
lean_object* l_List_foldr___main___at___private_Lean_Meta_EqnCompiler_Match_7__hasCtorPattern___spec__1___boxed(lean_object*, lean_object*);
@ -346,7 +347,6 @@ lean_object* l___private_Lean_Meta_EqnCompiler_Match_40__getUnusedLevelParam___c
lean_object* l_Lean_LocalDecl_fvarId(lean_object*);
uint8_t l___private_Lean_Meta_EqnCompiler_Match_7__hasCtorPattern(lean_object*);
extern lean_object* l_Std_HashSet_Inhabited___closed__1;
extern lean_object* l___private_Lean_Meta_ExprDefEq_13__addAssignmentInfo___closed__4;
lean_object* l___private_Lean_Meta_EqnCompiler_Match_40__getUnusedLevelParam___closed__1;
uint8_t l___private_Lean_Meta_EqnCompiler_Match_15__isArrayLitTransition(lean_object*);
lean_object* l_Lean_Meta_Match_Pattern_toMessageData___main___closed__5;
@ -718,7 +718,7 @@ lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l___private_Lean_Meta_ExprDefEq_13__addAssignmentInfo___closed__4;
x_5 = l___private_Lean_Meta_ExprDefEq_12__addAssignmentInfo___closed__4;
x_6 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);
@ -3034,7 +3034,7 @@ lean_inc(x_3);
x_4 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_dec(x_2);
x_5 = l___private_Lean_Meta_ExprDefEq_13__addAssignmentInfo___closed__4;
x_5 = l___private_Lean_Meta_ExprDefEq_12__addAssignmentInfo___closed__4;
x_6 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_6, 0, x_1);
lean_ctor_set(x_6, 1, x_5);

1412
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

4
stage0/stdlib/Lean/Meta/RecursorInfo.c generated
View file

@ -62,7 +62,6 @@ lean_object* l_Array_findIdxAux___main___at___private_Lean_Meta_RecursorInfo_9__
lean_object* l_List_toString___at_Lean_Meta_RecursorInfo_HasToString___spec__7(lean_object*);
lean_object* l_Lean_Core_getEnv___rarg(lean_object*, lean_object*);
extern lean_object* l_Array_empty___closed__1;
lean_object* l_Array_back___at___private_Lean_Meta_ExprDefEq_15__processAssignmentFOApproxAux___spec__1(lean_object*);
lean_object* lean_io_mk_ref(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___closed__13;
lean_object* lean_io_ref_get(lean_object*, lean_object*);
@ -193,6 +192,7 @@ lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_List_repr___rarg___closed__2;
lean_object* l_Nat_foldMAux___main___at___private_Lean_Meta_RecursorInfo_7__getIndicesPos___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_toString___at_Lean_Meta_RecursorInfo_HasToString___spec__7___boxed(lean_object*);
lean_object* l_Array_back___at___private_Lean_Meta_ExprDefEq_14__processAssignmentFOApproxAux___spec__1(lean_object*);
extern lean_object* l_List_reprAux___main___rarg___closed__1;
lean_object* l___private_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___closed__3;
lean_object* l___private_Lean_Meta_RecursorInfo_11__checkMotiveResultType___closed__4;
@ -2877,7 +2877,7 @@ x_11 = l_Array_isEmpty___rarg(x_5);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = l_Array_back___at___private_Lean_Meta_ExprDefEq_15__processAssignmentFOApproxAux___spec__1(x_5);
x_12 = l_Array_back___at___private_Lean_Meta_ExprDefEq_14__processAssignmentFOApproxAux___spec__1(x_5);
x_13 = lean_unsigned_to_nat(0u);
x_14 = l_Array_findIdxAux___main___at___private_Lean_Meta_RecursorInfo_5__getMajorPosDepElim___spec__2(x_12, x_3, x_13);
if (lean_obj_tag(x_14) == 0)

38
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

@ -34,7 +34,6 @@ lean_object* l___private_Lean_Expr_3__getAppArgsAux___main(lean_object*, lean_ob
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l___private_Lean_Meta_SynthInstance_6__preprocessOutParam___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_liftMetaM(lean_object*);
lean_object* l_Lean_Meta_SynthInstance_generate___closed__5;
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -117,7 +116,6 @@ lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_M
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_getInstances(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_replace___main___at_Lean_Meta_SynthInstance_MkTableKey_normExpr___main___spec__8(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_liftMetaM___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_findEntry_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_2__addNode___at___private_Lean_Meta_LevelDefEq_10__processPostponedStep___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findAux___main___at_Lean_Meta_synthInstance_x3f___spec__6___boxed(lean_object*, lean_object*, lean_object*);
@ -142,6 +140,7 @@ uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_getTop___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_findAux___main___at_Lean_Meta_synthInstance_x3f___spec__6(lean_object*, size_t, lean_object*);
lean_object* l_Lean_Meta_abstractMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Exception_inhabited___closed__1;
lean_object* l_Lean_Meta_SynthInstance_synth___main___closed__6;
lean_object* l___private_Lean_Meta_SynthInstance_3__preprocess___closed__1;
lean_object* l_Lean_Meta_SynthInstance_tryResolve(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -214,7 +213,6 @@ lean_object* l_Lean_Meta_whnf(lean_object*, lean_object*, lean_object*, lean_obj
lean_object* l_Lean_Meta_SynthInstance_resume___closed__3;
lean_object* l_Lean_mkFVar(lean_object*);
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
lean_object* l_Lean_Meta_SynthInstance_liftMetaM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_foldlM___main___at_Lean_Meta_SynthInstance_newSubgoal___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_Meta_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_AssocList_replace___main___at_Lean_Meta_SynthInstance_newSubgoal___spec__6(lean_object*, lean_object*, lean_object*);
@ -281,7 +279,6 @@ uint8_t l_Lean_TagAttribute_hasTag(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insertAux___main___at_Lean_Meta_synthInstance_x3f___spec__2(lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_getResult___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Core_getOptions(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Core_Exception_inhabited___closed__1;
lean_object* l_Array_umapMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_register_option(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_SynthInstance_synth___main___closed__2;
@ -2159,31 +2156,6 @@ x_1 = l_Lean_Meta_SynthInstance_Answer_inhabited___closed__1;
return x_1;
}
}
lean_object* l_Lean_Meta_SynthInstance_liftMetaM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = lean_apply_5(x_1, x_3, x_4, x_5, x_6, x_7);
return x_8;
}
}
lean_object* l_Lean_Meta_SynthInstance_liftMetaM(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_SynthInstance_liftMetaM___rarg___boxed), 7, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_SynthInstance_liftMetaM___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8;
x_8 = l_Lean_Meta_SynthInstance_liftMetaM___rarg(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
lean_dec(x_2);
return x_8;
}
}
lean_object* l_Lean_Meta_SynthInstance_mapMetaM(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:
{
@ -2197,7 +2169,7 @@ lean_object* l_Lean_Meta_SynthInstance_SynthM_inhabited___rarg(lean_object* x_1)
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_inhabited___closed__1;
x_2 = l_Lean_Exception_inhabited___closed__1;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -2616,7 +2588,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Array_umapMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__2___closed__1;
x_2 = lean_unsigned_to_nat(180u);
x_2 = lean_unsigned_to_nat(177u);
x_3 = lean_unsigned_to_nat(13u);
x_4 = l_Array_umapMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__2___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -4556,7 +4528,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Array_umapMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__2___closed__1;
x_2 = lean_unsigned_to_nat(225u);
x_2 = lean_unsigned_to_nat(222u);
x_3 = lean_unsigned_to_nat(16u);
x_4 = l_Lean_Meta_SynthInstance_getEntry___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -10808,7 +10780,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Array_umapMAux___main___at_Lean_Meta_SynthInstance_getInstances___spec__2___closed__1;
x_2 = lean_unsigned_to_nat(422u);
x_2 = lean_unsigned_to_nat(419u);
x_3 = lean_unsigned_to_nat(16u);
x_4 = l_Lean_Meta_SynthInstance_resume___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);

6
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

@ -110,6 +110,7 @@ lean_object* l___private_Lean_Meta_WHNF_4__whnfHeadPredAux___main___at_Lean_Meta
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_setWHNFRef(lean_object*);
lean_object* l___private_Lean_Meta_WHNF_1__useWHNFCache___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Exception_inhabited___closed__1;
lean_object* lean_nat_sub(lean_object*, lean_object*);
extern lean_object* l_Std_PersistentHashMap_insertAux___main___rarg___closed__3;
lean_object* l_Array_shrink___main___rarg(lean_object*, lean_object*);
@ -215,7 +216,6 @@ uint8_t l_Array_anyRangeMAux___main___at_Lean_Meta_unfoldDefinition_x3f___spec__
extern lean_object* l_Lean_Meta_whnfRef;
lean_object* l_Lean_Meta_synthPending(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_reduceBoolNative___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Core_Exception_inhabited___closed__1;
lean_object* l_Lean_Meta_reduceBinNatOp___closed__12;
lean_object* l_Lean_Meta_getExprMVarAssignment_x3f___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_WHNF_reduceQuotRec___at_Lean_Meta_whnfCore___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -11470,7 +11470,7 @@ lean_object* l_Lean_Meta_reduceBoolNative___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_inhabited___closed__1;
x_2 = l_Lean_Exception_inhabited___closed__1;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
@ -11502,7 +11502,7 @@ lean_object* l_Lean_Meta_reduceNatNative___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_inhabited___closed__1;
x_2 = l_Lean_Exception_inhabited___closed__1;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);

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

@ -3346,6 +3346,7 @@ lean_object* x_5;
x_5 = l_Lean_Parser_Command_commentBody_parenthesizer___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
@ -3374,6 +3375,7 @@ lean_object* x_6;
x_6 = l_Lean_Parser_Command_commentBody_formatter(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_6;
}
}

22
stage0/stdlib/Lean/Parser/Level.c generated
View file

@ -167,7 +167,7 @@ lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__22;
lean_object* l_Lean_Parser_Level_paren;
lean_object* l___regBuiltin_Lean_Parser_Level_addLit_formatter___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_checkPrec_formatter___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkPrec_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_dollarSymbol_parenthesizer(lean_object*);
lean_object* l_Lean_Name_append___main(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__2;
@ -256,7 +256,7 @@ extern lean_object* l_Option_HasRepr___rarg___closed__3;
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__3;
lean_object* l_Lean_Parser_ident___elambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_max___closed__4;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Level_addLit_formatter(lean_object*);
extern lean_object* l_Lean_Parser_numLit;
@ -267,7 +267,7 @@ lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__11;
lean_object* l___regBuiltin_Lean_Parser_Level_hole_parenthesizer___closed__1;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_level_parenthesizer___lambda__1___closed__2;
lean_object* l_Lean_Parser_Level_hole___closed__6;
lean_object* l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_max;
lean_object* l_Lean_Parser_Level_num;
@ -287,7 +287,7 @@ lean_object* l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__26;
extern lean_object* l___private_Init_Util_1__mkPanicMessage___closed__2;
extern lean_object* l_Lean_Parser_epsilonInfo;
lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__6;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_mkHole___closed__1;
lean_object* l_Lean_Parser_categoryParser___elambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_pushNone_formatter___boxed(lean_object*);
@ -298,7 +298,7 @@ lean_object* l_Lean_Parser_leadingNode_formatter(lean_object*, lean_object*, lea
lean_object* l_Lean_Parser_antiquotExpr_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ident_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_hole_parenthesizer___closed__1;
lean_object* l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Level_paren_formatter___closed__5;
lean_object* l_Lean_Parser_levelParser_formatter___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinParser_Lean_Parser_Level_hole(lean_object*);
@ -997,6 +997,7 @@ lean_object* x_6;
x_6 = l_Lean_Parser_dollarSymbol_formatter(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_6;
}
}
@ -1146,7 +1147,7 @@ lean_object* _init_l_Lean_Parser_mkAntiquot_formatter___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkNoWsBefore_formatter___boxed), 4, 0);
return x_1;
}
}
@ -1226,7 +1227,7 @@ lean_object* _init_l_Lean_Parser_mkAntiquot_formatter___closed__11() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkNoImmediateColon_formatter___boxed), 4, 0);
return x_1;
}
}
@ -1379,7 +1380,7 @@ lean_object* _init_l_Lean_Parser_leadingNode_formatter___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkPrec_formatter___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkPrec_formatter___boxed), 4, 0);
return x_1;
}
}
@ -1543,6 +1544,7 @@ lean_object* x_5;
x_5 = l_Lean_Parser_dollarSymbol_parenthesizer___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
@ -1674,7 +1676,7 @@ lean_object* _init_l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkNoWsBefore_parenthesizer___boxed), 4, 0);
return x_1;
}
}
@ -1848,7 +1850,7 @@ lean_object* _init_l_Lean_Parser_mkAntiquot_parenthesizer___rarg___closed__19()
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesizer___boxed), 4, 0);
return x_1;
}
}

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

@ -47,6 +47,7 @@ lean_object* l_Lean_Parser_Module_import;
lean_object* l_Lean_Parser_Module_import___elambda__1___closed__2;
lean_object* l___private_Lean_Parser_Module_1__mkErrorMessage___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Module_prelude_formatter___closed__2;
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__15;
lean_object* l_Lean_Parser_Module_header___closed__4;
lean_object* l___private_Lean_Parser_Module_2__mkEOI(lean_object*);
lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
@ -205,7 +206,6 @@ lean_object* l_Lean_Parser_Module_import___elambda__1___closed__7;
lean_object* l_Lean_Parser_Module_header___closed__3;
lean_object* l_IO_print___at___private_Lean_Parser_Module_4__testModuleParserAux___main___spec__4(lean_object*, lean_object*);
lean_object* l_String_trim(lean_object*);
extern lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__16;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_optional_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Parser_Module_4__testModuleParserAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Handle_mk___at_Lean_Parser_parseFile___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -2701,7 +2701,7 @@ _start:
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; lean_object* x_10;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__16;
x_3 = l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__15;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);

2
stage0/stdlib/Lean/Parser/Tactic.c generated
View file

@ -1208,6 +1208,7 @@ lean_object* x_5;
x_5 = l_Lean_Parser_Tactic_underscore_parenthesizer___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
@ -1235,6 +1236,7 @@ lean_object* x_6;
x_6 = l_Lean_Parser_Tactic_underscore_formatter(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_6;
}
}

24
stage0/stdlib/Lean/Parser/Term.c generated
View file

@ -319,7 +319,7 @@ lean_object* l___regBuiltinParser_Lean_Parser_Term_pow(lean_object*);
lean_object* l___regBuiltin_Lean_Parser_Term_match__syntax_formatter___closed__1;
lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_match_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__3;
lean_object* l_Lean_Parser_Term_doExpr___closed__4;
lean_object* l_Lean_Parser_Term_letEqnsDecl___closed__1;
@ -936,7 +936,7 @@ lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_obj
lean_object* l_Lean_Parser_Term_unicodeInfixR_parenthesizer___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_not_parenthesizer___closed__3;
lean_object* l_Lean_Parser_Term_implicitBinder___closed__4;
lean_object* l_Lean_PrettyPrinter_Formatter_checkStackTop_formatter___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkStackTop_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Tactic_nonEmptySeq___closed__4;
lean_object* l_Lean_Parser_Term_fun___elambda__1___closed__11;
lean_object* l_Lean_PrettyPrinter_Formatter_symbolNoWs_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1142,7 +1142,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_hole_parenthesizer___closed__1;
lean_object* l_Lean_Parser_Term_suffices___elambda__1___closed__5;
lean_object* l_Lean_Parser_Term_add___elambda__1___closed__2;
lean_object* l_Lean_Parser_Term_have___elambda__1___closed__6;
lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_seqRight___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_seqLeft_formatter___closed__1;
lean_object* l_Lean_Parser_Term_doElem___closed__3;
@ -1555,7 +1555,7 @@ lean_object* l_Lean_Parser_Term_letIdDecl___elambda__1(lean_object*, lean_object
lean_object* l___regBuiltin_Lean_Parser_Level_quot_formatter___closed__1;
lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_explicit_parenthesizer___closed__4;
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_app_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_not___elambda__1___closed__1;
lean_object* l_Lean_Parser_Term_doElem___closed__4;
@ -3513,7 +3513,7 @@ lean_object* l___regBuiltin_Lean_Parser_Term_append_parenthesizer(lean_object*);
lean_object* l_Lean_Parser_Term_subst_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___regBuiltinParser_Lean_Parser_Level_num___closed__1;
lean_object* l___regBuiltin_Lean_Parser_Term_bnot_parenthesizer(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGe_parenthesizer___boxed(lean_object*);
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkColGe_parenthesizer___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Term_app___closed__2;
lean_object* l_Lean_Parser_Term_namedArgument_parenthesizer___closed__5;
lean_object* l___regBuiltin_Lean_Parser_Term_heq_formatter(lean_object*);
@ -6520,7 +6520,7 @@ lean_object* _init_l_Lean_Parser_Term_type_parenthesizer___closed__4() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkWsBefore_parenthesizer___boxed), 4, 0);
return x_1;
}
}
@ -35754,6 +35754,7 @@ lean_object* x_6;
x_6 = l_Lean_Parser_darrow_formatter(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_6;
}
}
@ -35945,6 +35946,7 @@ lean_object* x_5;
x_5 = l_Lean_Parser_darrow_parenthesizer___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
@ -41387,7 +41389,7 @@ lean_object* _init_l_Lean_Parser_Term_matchAlts_formatter___lambda__1___closed__
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkColGe_formatter___boxed), 4, 0);
return x_1;
}
}
@ -41786,7 +41788,7 @@ lean_object* _init_l_Lean_Parser_Term_matchAlts_parenthesizer___lambda__1___clos
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkColGe_parenthesizer___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkColGe_parenthesizer___boxed), 4, 0);
return x_1;
}
}
@ -52620,6 +52622,7 @@ lean_object* x_6;
x_6 = l_Lean_Parser_Term_leftArrow_formatter(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_6;
}
}
@ -52724,6 +52727,7 @@ lean_object* x_5;
x_5 = l_Lean_Parser_Term_leftArrow_parenthesizer___rarg(x_1, x_2, x_3, x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
@ -61468,7 +61472,7 @@ lean_object* _init_l_Lean_Parser_Term_explicitUniv_formatter___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkStackTop_formatter___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Formatter_checkStackTop_formatter___boxed), 4, 0);
return x_1;
}
}
@ -61567,7 +61571,7 @@ lean_object* _init_l_Lean_Parser_Term_explicitUniv_parenthesizer___closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed), 4, 0);
return x_1;
}
}

75
stage0/stdlib/Lean/PrettyPrinter/Backtrack.c generated Normal file
View file

@ -0,0 +1,75 @@
// Lean compiler output
// Module: Lean.PrettyPrinter.Backtrack
// Imports: Init Lean.InternalExceptionId
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_PrettyPrinter_registerBacktrackId___closed__2;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_registerInternalExceptionId(lean_object*, lean_object*);
lean_object* l_Lean_PrettyPrinter_registerBacktrackId___closed__1;
lean_object* l_Lean_PrettyPrinter_registerBacktrackId(lean_object*);
lean_object* l_Lean_PrettyPrinter_backtrackExceptionId;
lean_object* _init_l_Lean_PrettyPrinter_registerBacktrackId___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("backtrackFormatter");
return x_1;
}
}
lean_object* _init_l_Lean_PrettyPrinter_registerBacktrackId___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_PrettyPrinter_registerBacktrackId___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_PrettyPrinter_registerBacktrackId(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_PrettyPrinter_registerBacktrackId___closed__2;
x_3 = l_Lean_registerInternalExceptionId(x_2, x_1);
return x_3;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_InternalExceptionId(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_PrettyPrinter_Backtrack(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_InternalExceptionId(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_PrettyPrinter_registerBacktrackId___closed__1 = _init_l_Lean_PrettyPrinter_registerBacktrackId___closed__1();
lean_mark_persistent(l_Lean_PrettyPrinter_registerBacktrackId___closed__1);
l_Lean_PrettyPrinter_registerBacktrackId___closed__2 = _init_l_Lean_PrettyPrinter_registerBacktrackId___closed__2();
lean_mark_persistent(l_Lean_PrettyPrinter_registerBacktrackId___closed__2);
res = l_Lean_PrettyPrinter_registerBacktrackId(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_PrettyPrinter_backtrackExceptionId = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_PrettyPrinter_backtrackExceptionId);
lean_dec_ref(res);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

7995
stage0/stdlib/Lean/PrettyPrinter/Formatter.c generated
View file

File diff suppressed because it is too large Load diff

2
stage0/stdlib/Lean/PrettyPrinter/Meta.c generated
View file

@ -2864,6 +2864,7 @@ lean_object* x_7;
x_7 = l_Lean_PrettyPrinter_Formatter_interpretParserDescr___main___elambda__12(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_7;
}
}
@ -2874,6 +2875,7 @@ lean_object* x_7;
x_7 = l_Lean_PrettyPrinter_Formatter_interpretParserDescr___main___elambda__13(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
return x_7;
}
}

27766
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c generated
View file

File diff suppressed because it is too large Load diff

16
stage0/stdlib/Lean/Util/Sorry.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Util.Sorry
// Imports: Init Lean.Message Lean.CoreM
// Imports: Init Lean.Message Lean.Exception
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -22,7 +22,6 @@ uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_MessageData_hasSyntheticSorry___main___boxed(lean_object*);
uint8_t l_Lean_Expr_hasSorry___main(lean_object*);
lean_object* l_Lean_MessageData_hasSyntheticSorry___boxed(lean_object*);
lean_object* l_Lean_Core_Exception_hasSyntheticSorry___boxed(lean_object*);
lean_object* lean_array_get_size(lean_object*);
uint8_t l_Lean_Expr_hasSyntheticSorry(lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -32,10 +31,10 @@ lean_object* l_Lean_Expr_isSyntheticSorry___closed__1;
lean_object* l_Lean_Expr_hasSyntheticSorry___boxed(lean_object*);
lean_object* l_Lean_Expr_isSyntheticSorry___boxed(lean_object*);
uint8_t l_Lean_MessageData_hasSorry___main(lean_object*);
uint8_t l_Lean_Exception_hasSyntheticSorry(lean_object*);
uint8_t l_Array_anyRangeMAux___main___at_Lean_MessageData_hasSorry___main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasSyntheticSorry___main(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
uint8_t l_Lean_Core_Exception_hasSyntheticSorry(lean_object*);
lean_object* l_Array_anyRangeMAux___main___at_Lean_MessageData_hasSorry___main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isSorry___closed__1;
uint8_t l_Lean_MessageData_hasSyntheticSorry(lean_object*);
@ -43,6 +42,7 @@ lean_object* l_Array_anyRangeMAux___main___at_Lean_MessageData_hasSyntheticSorry
lean_object* l_Lean_MessageData_hasSorry___boxed(lean_object*);
lean_object* l_Lean_Expr_isSorry___boxed(lean_object*);
extern lean_object* l_Bool_HasRepr___closed__2;
lean_object* l_Lean_Exception_hasSyntheticSorry___boxed(lean_object*);
uint8_t l_Lean_Expr_hasSorry(lean_object*);
lean_object* l_Lean_Expr_hasSorry___boxed(lean_object*);
lean_object* l_Lean_Expr_hasSyntheticSorry___main___boxed(lean_object*);
@ -890,7 +890,7 @@ x_3 = lean_box(x_2);
return x_3;
}
}
uint8_t l_Lean_Core_Exception_hasSyntheticSorry(lean_object* x_1) {
uint8_t l_Lean_Exception_hasSyntheticSorry(lean_object* x_1) {
_start:
{
if (lean_obj_tag(x_1) == 0)
@ -908,11 +908,11 @@ return x_4;
}
}
}
lean_object* l_Lean_Core_Exception_hasSyntheticSorry___boxed(lean_object* x_1) {
lean_object* l_Lean_Exception_hasSyntheticSorry___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = l_Lean_Core_Exception_hasSyntheticSorry(x_1);
x_2 = l_Lean_Exception_hasSyntheticSorry(x_1);
lean_dec(x_1);
x_3 = lean_box(x_2);
return x_3;
@ -920,7 +920,7 @@ return x_3;
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Message(lean_object*);
lean_object* initialize_Lean_CoreM(lean_object*);
lean_object* initialize_Lean_Exception(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Util_Sorry(lean_object* w) {
lean_object * res;
@ -932,7 +932,7 @@ lean_dec_ref(res);
res = initialize_Lean_Message(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_CoreM(lean_io_mk_world());
res = initialize_Lean_Exception(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Expr_isSorry___closed__1 = _init_l_Lean_Expr_isSorry___closed__1();