chore: update stage0

This commit is contained in:
Sebastian Ullrich 2021-06-22 10:39:39 +02:00
parent 0948742da1
commit de0bf36587
78 changed files with 79715 additions and 97353 deletions

View file

@ -192,10 +192,6 @@ if(LLVM)
include_directories(${LLVM_INCLUDE_DIRS})
set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_LLVM")
set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_LLVM")
# Find the libraries that correspond to the LLVM components
# that we wish to use and define llvm_libs
llvm_map_components_to_libnames(llvm_libs nativecodegen)
else()
#message(WARNING "Disabling LLVM support. JIT compilation will not be available")
endif()
@ -471,9 +467,6 @@ if(PREV_STAGE)
endif()
target_link_libraries(leancpp INTERFACE ${EXTRA_LIBS})
if(LLVM)
target_link_libraries(leancpp INTERFACE ${llvm_libs})
endif()
configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" @ONLY)
install(FILES "${CMAKE_BINARY_DIR}/bin/leanc"

View file

@ -23,7 +23,7 @@ universes u v
pure b
else match i with
| 0 => pure b
| i+1 => match ← f j b with
| i+1 => match (← f j b) with
| ForInStep.done b => pure b
| ForInStep.yield b => loop i (j + range.step) b
loop range.stop range.start init

View file

@ -201,6 +201,10 @@ macro_rules
else
`(%[ $elems,* | List.nil ])
-- TODO: should be `infix:50 " matches " => fun e p => match e with | p => true | _ => false`
macro:50 e:term:51 " matches " p:term:51 : term =>
`(match $e:term with | $p:term => true | _ => false)
namespace Parser.Tactic
syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic

View file

@ -54,7 +54,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
: IpcM (List (Notification PublishDiagnosticsParams)) := do
writeRequest ⟨waitForDiagnosticsId, "textDocument/waitForDiagnostics", WaitForDiagnosticsParams.mk target version⟩
let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
match ←readMessage with
match (←readMessage) with
| Message.response id _ =>
if id == waitForDiagnosticsId then []
else loop

View file

@ -144,12 +144,8 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
registerCustomErrorIfMVar type ref "failed to infer binder type"
private def addLocalVarInfoCore (lctx : LocalContext) (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
if (← getInfoState).enabled then
pushInfoTree <| InfoTree.node (children := {}) <| Info.ofTermInfo { lctx := lctx, expr := fvar, stx, expectedType? := none }
private def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
addLocalVarInfoCore (← getLCtx) stx fvar
addTermInfo (lctx? := some (← getLCtx)) stx fvar
private def ensureAtomicBinderName (binderView : BinderView) : TermElabM Unit :=
let n := binderView.id.getId.eraseMacroScopes
@ -341,7 +337,7 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat
We do not believe this is an useful feature, and it would complicate the logic here.
-/
let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi
addLocalVarInfoCore lctx binderView.id fvar
addTermInfo (lctx? := some lctx) binderView.id fvar
let s ← withRef binderView.id <| propagateExpectedType fvar type s
let s := { s with lctx := lctx }
match (← isClass? type) with

View file

@ -226,7 +226,7 @@ where
@[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro
| `(()) => `(Unit.unit)
| `(($e : $type)) => do
match ← expandCDot? e with
match (← expandCDot? e) with
| some e => `(($e : $type))
| none => Macro.throwUnsupported
| `(($e)) => return (← expandCDot? e).getD e

View file

@ -207,11 +207,26 @@ private def addTraceAsMessages : CommandElabM Unit := do
traceState.traces := {}
}
private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → CommandElabM Unit
private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : Std.PersistentArray InfoTree) : CommandElabM InfoTree := do
let ctx ← read
let s ← get
let scope := s.scopes.head!
let tree := InfoTree.node (Info.ofCommandInfo { elaborator, stx }) trees
let tree := InfoTree.context {
env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
} tree
if checkTraceOption (← getOptions) `Elab.info then
let fmt ← tree.format
trace[Elab.info] fmt
return tree
private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit
| [] => throwError "unexpected syntax{indentD stx}"
| (elabFn::elabFns) =>
catchInternalId unsupportedSyntaxExceptionId
(do elabFn stx; addTraceAsMessages)
(do
withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.decl stx) <| elabFn.value stx
addTraceAsMessages)
(fun _ => do set s; addTraceAsMessages; elabCommandUsing s stx elabFns)
/- Elaborate `x` with `stx` on the macro stack -/
@ -248,19 +263,8 @@ register_builtin_option showPartialSyntaxErrors : Bool := {
builtin_initialize registerTraceClass `Elab.command
partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
let mkInfoTree trees := do
let ctx ← read
let s ← get
let scope := s.scopes.head!
let tree := InfoTree.node (Info.ofCommandInfo { stx := stx }) trees
let tree := InfoTree.context {
env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
} tree
if checkTraceOption (← getOptions) `Elab.info then
logTrace `Elab.info m!"{← tree.format}"
return tree
let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
withLogging <| withRef stx <| withInfoTreeContext (mkInfoTree := mkInfoTree) <| withIncRecDepth <| withFreshMacroScope do
withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
runLinters stx
match stx with
| Syntax.node k args =>
@ -271,13 +275,13 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
else do
trace `Elab.command fun _ => stx;
let s ← get
let stxNew? ← catchInternalId unsupportedSyntaxExceptionId
(do let newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx))
(fun ex => pure none)
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew <| elabCommand stxNew
match (← liftMacroM <| expandMacroImpl? s.env stx) with
| some (decl, stxNew) =>
withInfoTreeContext (mkInfoTree := mkInfoTree decl stx) do
withMacroExpansion stx stxNew do
elabCommand stxNew
| _ =>
match commandElabAttribute.getValues s.env k with
match commandElabAttribute.getEntries s.env k with
| [] => throwError "elaboration function for '{k}' has not been implemented"
| elabFns => elabCommandUsing s stx elabFns
| _ => throwError "unexpected command"

View file

@ -9,6 +9,9 @@ import Lean.Elab.Match
import Lean.Elab.Quotation.Util
import Lean.Parser.Do
-- HACK: avoid code explosion until heuristics are improved
set_option compiler.reuse false
namespace Lean.Elab.Term
open Lean.Parser.Term
open Meta

View file

@ -27,7 +27,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
let ctx ← read
let s ← get
let cmdCtx : Command.Context := { cmdPos := s.cmdPos, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap }
match ← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState with
match (← liftM <| EIO.toIO' <| (x cmdCtx).run s.commandState) with
| Except.error e => throw <| IO.Error.userError s!"unexpected internal error: {← e.toMessageData.toString}"
| Except.ok (a, sNew) => setCommandState sNew; return a

View file

@ -2,7 +2,7 @@
Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Leonardo de Moura
Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Data.Position
import Lean.Expr
@ -27,15 +27,19 @@ structure ContextInfo where
openDecls : List OpenDecl := []
deriving Inhabited
structure TermInfo where
/-- An elaboration step -/
structure ElabInfo where
elaborator : Name
stx : Syntax
deriving Inhabited
structure TermInfo extends ElabInfo where
lctx : LocalContext -- The local context when the term was elaborated.
expectedType? : Option Expr
expr : Expr
stx : Syntax
deriving Inhabited
structure CommandInfo where
stx : Syntax
structure CommandInfo extends ElabInfo where
deriving Inhabited
inductive CompletionInfo where
@ -65,18 +69,17 @@ structure FieldInfo where
/- We store the list of goals before and after the execution of a tactic.
We also store the metavariable context at each time since, we want to unassigned metavariables
at tactic execution time to be displayed as `?m...`. -/
structure TacticInfo where
structure TacticInfo extends ElabInfo where
mctxBefore : MetavarContext
goalsBefore : List MVarId
stx : Syntax
mctxAfter : MetavarContext
goalsAfter : List MVarId
deriving Inhabited
structure MacroExpansionInfo where
lctx : LocalContext -- The local context when the macro was expanded.
before : Syntax
after : Syntax
stx : Syntax
output : Syntax
deriving Inhabited
inductive Info where
@ -152,15 +155,21 @@ where fmtPos pos info :=
| SourceInfo.original .. => pos
| _ => f!"{pos}†"
private def formatElabInfo (ctx : ContextInfo) (info : ElabInfo) : Format :=
if info.elaborator.isAnonymous then
formatStxRange ctx info.stx
else
f!"{formatStxRange ctx info.stx} @ {info.elaborator}"
def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO α :=
ctx.runMetaM info.lctx x
def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
info.runMetaM ctx do
try
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange ctx info.stx}"
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatElabInfo ctx info.toElabInfo}"
catch _ =>
return f!"{← Meta.ppExpr info.expr} : <failed-to-infer-type> @ {formatStxRange ctx info.stx}"
return f!"{← Meta.ppExpr info.expr} : <failed-to-infer-type> @ {formatElabInfo ctx info.toElabInfo}"
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with
@ -169,7 +178,7 @@ def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Forma
| _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
return f!"command @ {formatStxRange ctx info.stx}"
return f!"command @ {formatElabInfo ctx info.toElabInfo}"
def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do
ctx.runMetaM info.lctx do
@ -186,12 +195,12 @@ def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
let ctxA := { ctx with mctx := info.mctxAfter }
let goalsBefore ← ctxB.ppGoals info.goalsBefore
let goalsAfter ← ctxA.ppGoals info.goalsAfter
return f!"Tactic @ {formatStxRange ctx info.stx}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
return f!"Tactic @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do
let before ← ctx.ppSyntax info.lctx info.before
let after ← ctx.ppSyntax info.lctx info.after
return f!"Macro expansion\n{before}\n===>\n{after}"
let stx ← ctx.ppSyntax info.lctx info.stx
let output ← ctx.ppSyntax info.lctx info.output
return f!"Macro expansion\n{stx}\n===>\n{output}"
def Info.format (ctx : ContextInfo) : Info → IO Format
| ofTacticInfo i => i.format ctx
@ -201,6 +210,14 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
| ofFieldInfo i => i.format ctx
| ofCompletionInfo i => i.format ctx
def Info.toElabInfo? : Info → Option ElabInfo
| ofTacticInfo i => some i.toElabInfo
| ofTermInfo i => some i.toElabInfo
| ofCommandInfo i => some i.toElabInfo
| ofMacroExpansionInfo i => none
| ofFieldInfo i => none
| ofCompletionInfo i => none
/--
Helper function for propagating the tactic metavariable context to its children nodes.
We need this function because we preserve `TacticInfo` nodes during backtracking *and* their
@ -259,14 +276,15 @@ def addCompletionInfo (info : CompletionInfo) : m Unit := do
def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) (expectedType? : Option Expr := none) : m Name := do
let n ← resolveGlobalConstNoOverload id
if (← getInfoState).enabled then
pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
-- we do not store a specific elaborator since identifiers are special-cased by the server anyway
pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
return n
def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) (expectedType? : Option Expr := none) : m (List Name) := do
let ns ← resolveGlobalConst id
if (← getInfoState).enabled then
for n in ns do
pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
pushInfoLeaf <| Info.ofTermInfo { elaborator := Name.anonymous, lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
return ns
@[inline] def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
@ -305,12 +323,11 @@ def assignInfoHoleId (mvarId : MVarId) (infoTree : InfoTree) : m Unit := do
modifyInfoState fun s => { s with assignment := s.assignment.insert mvarId infoTree }
end
def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLCtx m] (before after : Syntax) (x : m α) : m α :=
def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLCtx m] (stx output : Syntax) (x : m α) : m α :=
let mkInfo : m Info := do
return Info.ofMacroExpansionInfo {
lctx := (← getLCtx)
before := before
after := after
stx, output
}
withInfoContext x mkInfo

View file

@ -741,7 +741,7 @@ private def elabPatterns (patternStxs : Array Syntax) (matchType : Expr) : Excep
restoreState s
match (← liftM <| commitIfNoErrors? <| withoutErrToSorry do elabTermAndSynthesize patternStx (← eraseIndices d)) with
| some pattern =>
match ← findDiscrRefinementPath pattern d |>.run with
match (← findDiscrRefinementPath pattern d |>.run) with
| some path =>
trace[Meta.debug] "refinement path: {path}"
restoreState s
@ -987,7 +987,7 @@ where
: TermElabM (Array Expr × Expr × Array (AltLHS × Expr) × Bool) := do
let s ← saveState
let (discrs', matchType', altViews', refined) ← generalize discrs matchType altViews generalizing?
match ← altViews'.mapM (fun altView => elabMatchAltView altView matchType') |>.run with
match (← altViews'.mapM (fun altView => elabMatchAltView altView matchType') |>.run) with
| Except.ok alts => return (discrs', matchType', alts, first?.isSome || refined)
| Except.error { patternIdx := patternIdx, pathToIndex := pathToIndex, ex := ex } =>
trace[Meta.debug] "pathToIndex: {toString pathToIndex}"
@ -1332,7 +1332,7 @@ builtin_initialize
@[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? => do
match stx with
| `(nomatch $discrExpr) =>
match ← isLocalIdent? discrExpr with
match (← isLocalIdent? discrExpr) with
| some _ =>
let expectedType ← waitExpectedType expectedType?
let discr := Syntax.node ``Lean.Parser.Term.matchDiscr #[mkNullNode, discrExpr]

View file

@ -22,7 +22,7 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) : MetaM (Option Expr
| i+1, type => do
let x := xs[i]
let type ← mkForallFVars #[x] type;
match ← mkInhabitant? type with
match (← mkInhabitant? type) with
| none => loop i type
| some val => pure $ some (← mkLambdaFVars xs[0:i] val)
loop xs.size type
@ -30,13 +30,13 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) : MetaM (Option Expr
/- TODO: add a global IO.Ref to let users customize/extend this procedure -/
def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do
match ← mkInhabitant? type with
match (← mkInhabitant? type) with
| some val => mkLambdaFVars xs val
| none =>
match ← findAssumption? xs type with
match (← findAssumption? xs type) with
| some x => mkLambdaFVars xs x
| none =>
match ← mkFnInhabitant? xs type with
match (← mkFnInhabitant? xs type) with
| some val => pure val
| none => throwError "failed to compile partial definition '{declName}', failed to show that type is inhabited"

View file

@ -159,13 +159,13 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA
let numFixed := if indexMinPos < numFixed then indexMinPos else numFixed
let fixedParams := xs.extract 0 numFixed
let ys := xs.extract numFixed xs.size
match ← hasBadIndexDep? ys indIndices with
match (← hasBadIndexDep? ys indIndices) with
| some (index, y) =>
orelse'
(throwError "argument #{i+1} was not used because its type is an inductive family{indentExpr xType}\nand index{indentExpr index}\ndepends on the non index{indentExpr y}")
(loop (i+1))
| none =>
match ← hasBadParamDep? ys indParams with
match (← hasBadParamDep? ys indParams) with
| some (indParam, y) =>
orelse'
(throwError "argument #{i+1} was not used because its type is an inductive datatype{indentExpr xType}\nand parameter{indentExpr indParam}\ndepends on{indentExpr y}")
@ -390,7 +390,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
throwError "could not solve using backwards chaining {MessageData.ofGoal main.mvarId!}"
else
return mkAppN (← loop f) (← args.mapM loop)
match ←matchMatcherApp? e with
match (←matchMatcherApp? e) with
| some matcherApp =>
if !recArgHasLooseBVarsAt recFnName recArgInfo e then
processApp e

View file

@ -433,7 +433,7 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar
-- looks simple enough/created by this function, skip
return (floatedLetDecls, (pats, rhs))
withFreshMacroScope do
match ← getPatternsVars pats.toArray with
match (← getPatternsVars pats.toArray) with
| #[] =>
-- no antiquotations => introduce Unit parameter to preserve evaluation order
let rhs' ← `(rhs Unit.unit)

View file

@ -58,7 +58,7 @@ partial def precheck : Precheck := fun stx => do
return
if !hasQuotedIdent stx then
return -- we only precheck identifiers, so there is nothing to check here
if let some stx' ← liftMacroM <| Macro.expandMacro? stx then
if let some stx' ← liftMacroM <| expandMacro? stx then
precheck stx'
return
throwErrorAt stx "no macro or `[quotPrecheck]` instance for syntax kind '{stx.getKind}' found{indentD stx}

View file

@ -5,6 +5,7 @@ Authors: Leonardo de Moura
-/
import Lean.Elab.Command
import Lean.Parser.Syntax
import Lean.Elab.Util
namespace Lean.Elab.Term
/-
@ -279,8 +280,13 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
else
kind == `Lean.Parser.Syntax.atom
def resolveSyntaxKind (k : Name) : CommandElabM Name := do
checkSyntaxNodeKindAtNamespaces k (← getCurrNamespace)
<|>
throwError "invalid syntax node kind '{k}'"
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
let `($attrKind:attrKind syntax $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) ← pure stx
let `($[$doc?:docComment]? $attrKind:attrKind syntax $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) ← pure stx
| throwUnsupportedSyntax
let cat := catStx.getId.eraseMacroScopes
unless (Parser.isParserCategory (← getEnv) cat) do
@ -301,10 +307,10 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
let declName := mkIdentFrom stx name
let d ←
if let some lhsPrec := lhsPrec? then
`(@[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName : Lean.TrailingParserDescr :=
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName : Lean.TrailingParserDescr :=
ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
else
`(@[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName : Lean.ParserDescr :=
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName : Lean.ParserDescr :=
ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
trace `Elab fun _ => d
withMacroExpansion stx d <| elabCommand d
@ -327,7 +333,7 @@ private def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
Remark: `k` is the user provided kind with the current namespace included.
Recall that syntax node kinds contain the current namespace.
-/
def elabMacroRulesAux (attrKind : Syntax) (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
def elabMacroRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
let alts ← alts.mapM fun alt => match alt with
| `(matchAltExpr| | $pats,* => $rhs) => do
let pat := pats.elemsAndSeps[0]
@ -347,7 +353,7 @@ def elabMacroRulesAux (attrKind : Syntax) (k : SyntaxNodeKind) (alts : Array Syn
else
throwErrorAt alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
| _ => throwUnsupportedSyntax
`(@[$attrKind:attrKind macro $(Lean.mkIdent k)] def myMacro : Macro :=
`($[$doc?:docComment]? @[$attrKind:attrKind macro $(Lean.mkIdent k)] def myMacro : Macro :=
fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
@ -359,30 +365,33 @@ def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
pure quoted.getKind
| _ => throwUnsupportedSyntax
def elabNoKindMacroRulesAux (attrKind : Syntax) (alts : Array Syntax) : CommandElabM Syntax := do
/--
Infer syntax kind `k` from first pattern, put alternatives of same kind into new `macro/elab_rules (kind := k)` via `mkCmd (some k)`,
leave remaining alternatives (via `mkCmd none`) to be recursively expanded. -/
private def expandNoKindMacroRulesAux (alts : Array Syntax) (cmdName : String) (mkCmd : Option Name → Array Syntax → CommandElabM Syntax) : CommandElabM Syntax := do
let mut k ← inferMacroRulesAltKind alts[0]
if k.isStr && k.getString! == "antiquot" then
k := k.getPrefix
if k == choiceKind then
throwErrorAt alts[0]
"invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
"invalid {cmdName} alternative, multiple interpretations for pattern (solution: specify node kind using `{cmdName} (kind := ...) ...`)"
else
let altsK ← alts.filterM fun alt => return checkRuleKind (← inferMacroRulesAltKind alt) k
let altsNotK ← alts.filterM fun alt => return !checkRuleKind (← inferMacroRulesAltKind alt) k
let defCmd ← elabMacroRulesAux attrKind k altsK
if altsNotK.isEmpty then
pure defCmd
mkCmd k altsK
else
`($defCmd:command $attrKind:attrKind macro_rules $altsNotK:matchAlt*)
mkNullNode #[← mkCmd k altsK, ← mkCmd none altsNotK]
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
adaptExpander fun stx => match stx with
| `($attrKind:attrKind macro_rules $alts:matchAlt*) =>
elabNoKindMacroRulesAux attrKind alts
| `($attrKind:attrKind macro_rules (kind := $kind) | $x:ident => $rhs) =>
`(@[$attrKind:attrKind macro $kind] def myMacro : Macro := fun $x:ident => $rhs)
| `($attrKind:attrKind macro_rules (kind := $kind) $alts:matchAlt*) =>
do elabMacroRulesAux attrKind ((← getCurrNamespace) ++ kind.getId) alts
| `($[$doc?:docComment]? $attrKind:attrKind macro_rules $alts:matchAlt*) =>
expandNoKindMacroRulesAux alts "macro_rules" fun kind? alts =>
`($[$doc?:docComment]? $attrKind:attrKind macro_rules $[(kind := $(mkIdent <$> kind?))]? $alts:matchAlt*)
| `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) | $x:ident => $rhs) =>
`($[$doc?:docComment]? @[$attrKind:attrKind macro $kind] def myMacro : Macro := fun $x:ident => $rhs)
| `($[$doc?:docComment]? $attrKind:attrKind macro_rules (kind := $kind) $alts:matchAlt*) =>
do elabMacroRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) alts
| _ => throwUnsupportedSyntax
@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
@ -535,42 +544,38 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := do
where mkSplicePat kind id suffix :=
mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix]
/- «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail) -/
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro := fun stx => do
let attrKind := stx[0]
let prec := stx[2].getOptional?
let name? ← expandOptNamedName stx[3]
let prio ← expandOptNamedPrio stx[4]
let head := stx[5]
let args := stx[6].getArgs
let cat := stx[8]
-- build parser
let stxPart ← expandMacroArgIntoSyntaxItem head
let stxParts ← args.mapM expandMacroArgIntoSyntaxItem
let stxParts := #[stxPart] ++ stxParts
-- name
let name ← match name? with
| some name => pure name
| none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build macro rules
let patHead ← expandMacroArgIntoPattern head
let patArgs ← args.mapM expandMacroArgIntoPattern
/- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) (#[patHead] ++ patArgs)
if stx.getArgs.size == 11 then
-- `stx` is of the form `macro $head $args* : $cat => term`
let rhs := stx[10]
let stxCmd ← `(Parser.Command.syntax| $attrKind:attrKind syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat)
let macroRulesCmd ← `(macro_rules | `($pat) => $rhs)
return mkNullNode #[stxCmd, macroRulesCmd]
else
-- `stx` is of the form `macro $head $args* : $cat => `( $body )`
let rhsBody := stx[11]
let stxCmd ← `(Parser.Command.syntax| $attrKind:attrKind syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat)
let macroRulesCmd ← `(macro_rules | `($pat) => `($rhsBody))
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro
| `($[$doc?:docComment]? $attrKind:attrKind
macro$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $head:macroArg $args:macroArg* :
$cat => $rhs) => do
let prio ← evalOptPrio prio?
-- build parser
let stxPart ← expandMacroArgIntoSyntaxItem head
let stxParts ← args.mapM expandMacroArgIntoSyntaxItem
let stxParts := #[stxPart] ++ stxParts
-- name
let name ← match name? with
| some name => pure name.getId
| none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build macro rules
let patHead ← expandMacroArgIntoPattern head
let patArgs ← args.mapM expandMacroArgIntoPattern
/- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) (#[patHead] ++ patArgs)
let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind
syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat)
let macroRulesCmd ←
if rhs.getArgs.size == 1 then
-- `rhs` is a `term`
let rhs := rhs[0]
`($[$doc?:docComment]? macro_rules | `($pat) => $rhs)
else
-- `rhs` is of the form `` `( $body ) ``
let rhsBody := rhs[1]
`($[$doc?:docComment]? macro_rules | `($pat) => `($rhsBody))
return mkNullNode #[stxCmd, macroRulesCmd]
| _ => Macro.throwUnsupported
builtin_initialize
registerTraceClass `Elab.syntax
@ -581,69 +586,83 @@ builtin_initialize
| throwError "expected type must be known"
x expectedType
/-
def elabTail := try (" : " >> ident) >> darrow >> termParser
def «elab» := leading_parser suppressInsideQuot (Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
-/
def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
let ref := stx
let attrKind := stx[0]
let prec := stx[2].getOptional?
let name? ← liftMacroM <| expandOptNamedName stx[3]
let prio ← liftMacroM <| expandOptNamedPrio stx[4]
let head := stx[5]
let args := stx[6].getArgs
let cat := stx[8]
let expectedTypeSpec := stx[9]
let rhs := stx[11]
let catName := cat.getId
-- build parser
let stxPart ← liftMacroM <| expandMacroArgIntoSyntaxItem head
let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem
let stxParts := #[stxPart] ++ stxParts
-- name
let name ← match name? with
| some name => pure name
| none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build pattern for syntax `match`
let patHead ← liftMacroM <| expandMacroArgIntoPattern head
let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern
let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs)
let stxCmd ← `(Parser.Command.syntax|
$attrKind:attrKind syntax $(prec)? (name := $(mkIdentFrom stx name):ident) (priority := $(quote prio):numLit) $[$stxParts]* : $cat)
let elabCmd ←
if expectedTypeSpec.hasArgs then
if catName == `term then
let expId := expectedTypeSpec[1]
`(@[termElab $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Term.TermElab :=
fun stx expectedType? => match stx with
| `($pat) => Lean.Elab.Command.withExpectedType expectedType? fun $expId => $rhs
| _ => throwUnsupportedSyntax)
def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeKind) (cat? expty? : Option Syntax) (alts : Array Syntax) : CommandElabM Syntax := do
let alts ← alts.mapM fun alt => match alt with
| `(matchAltExpr| | $pats,* => $rhs) => do
let pat := pats.elemsAndSeps[0]
if !pat.isQuot then
throwUnsupportedSyntax
let quoted := getQuotContent pat
let k' := quoted.getKind
if checkRuleKind k' k then
pure alt
else if k' == choiceKind then
match quoted.getArgs.find? fun quotAlt => checkRuleKind quotAlt.getKind k with
| none => throwErrorAt alt "invalid elab_rules alternative, expected syntax node kind '{k}'"
| some quoted =>
let pat := pat.setArg 1 quoted
let pats := pats.elemsAndSeps.set! 0 pat
`(matchAltExpr| | $pats,* => $rhs)
else
throwErrorAt expectedTypeSpec "syntax category '{catName}' does not support expected type specification"
else if catName == `term then
`(@[termElab $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Term.TermElab :=
fun stx _ => match stx with
| `($pat) => $rhs
| _ => throwUnsupportedSyntax)
else if catName == `command then
`(@[commandElab $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Command.CommandElab :=
fun
| `($pat) => $rhs
| _ => throwUnsupportedSyntax)
else if catName == `tactic then
`(@[tactic $(mkIdentFrom stx name):ident] def elabFn : Lean.Elab.Tactic.Tactic :=
fun
| `(tactic|$pat) => $rhs
| _ => throwUnsupportedSyntax)
throwErrorAt alt "invalid elab_rules alternative, unexpected syntax node kind '{k'}'"
| _ => throwUnsupportedSyntax
let catName ← match cat?, expty? with
| some cat, _ => cat.getId
| _, some _ => `term
-- TODO: infer category from quotation kind, possibly even kind of quoted syntax?
| _, _ => throwError "invalid elab_rules command, specify category using `elab_rules : <cat> ...`"
if let some expId := expty? then
if catName == `term then
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Term.TermElab :=
fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
$alts:matchAlt* | _ => throwUnsupportedSyntax)
else
-- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.
-- If users want this feature, they add their own `elab` macro that uses this one as a fallback.
throwError "unsupported syntax category '{catName}'"
return mkNullNode #[stxCmd, elabCmd]
throwErrorAt expId "syntax category '{catName}' does not support expected type specification"
else if catName == `term then
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Term.TermElab :=
fun stx _ => match stx with
$alts:matchAlt* | _ => throwUnsupportedSyntax)
else if catName == `command then
`($[$doc?:docComment]? @[commandElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Command.CommandElab :=
fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
else if catName == `tactic then
`($[$doc?:docComment]? @[tactic $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Tactic.Tactic :=
fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
else
-- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.
-- If users want this feature, they add their own `elab_rules` macro that uses this one as a fallback.
throwError "unsupported syntax category '{catName}'"
@[builtinCommandElab «elab»] def elabElab : CommandElab :=
adaptExpander fun stx => do
expandElab (← getCurrNamespace) stx
@[builtinCommandElab «elab_rules»] def elabElabRules : CommandElab :=
adaptExpander fun stx => match stx with
| `($[$doc?:docComment]? $attrKind:attrKind elab_rules $[: $cat?]? $[<= $expty?]? $alts:matchAlt*) =>
expandNoKindMacroRulesAux alts "elab_rules" fun kind? alts =>
`($[$doc?:docComment]? $attrKind:attrKind elab_rules $[(kind := $(mkIdent <$> kind?))]? $[: $cat?]? $[<= $expty?]? $alts:matchAlt*)
| `($[$doc?:docComment]? $attrKind:attrKind elab_rules (kind := $kind) $[: $cat?]? $[<= $expty?]? $alts:matchAlt*) =>
do elabElabRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) cat? expty? alts
| _ => throwUnsupportedSyntax
@[builtinMacro Lean.Parser.Command.elab]
def expandElab : Macro
| `($[$doc?:docComment]? $attrKind:attrKind
elab$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $head:macroArg $args:macroArg* :
$cat $[<= $expectedType?]? => $rhs) => do
let prio ← evalOptPrio prio?
let catName := cat.getId
-- build parser
let stxPart ← expandMacroArgIntoSyntaxItem head
let stxParts ← args.mapM expandMacroArgIntoSyntaxItem
let stxParts := #[stxPart] ++ stxParts
-- name
let name ← match name? with
| some name => pure name.getId
| none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-- build pattern for syntax `match`
let patHead ← expandMacroArgIntoPattern head
let patArgs ← args.mapM expandMacroArgIntoPattern
let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) (#[patHead] ++ patArgs)
`($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat
$[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs)
| _ => Macro.throwUnsupported
end Lean.Elab.Command

View file

@ -36,7 +36,9 @@ def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit :=
namespace Tactic
structure Context where
main : MVarId
main : MVarId
-- declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree
elaborator : Name
structure State where
goals : List MVarId
@ -90,7 +92,7 @@ def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
else
throw ex
try
aux.runCore' { main := mvarId } { goals := [mvarId] }
aux.runCore' { main := mvarId, elaborator := Name.anonymous } { goals := [mvarId] }
finally
modify fun s => { s with syntheticMVars := savedSyntheticMVars }
@ -109,33 +111,9 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
@[builtinInit mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic
/-
Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define
the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages,
and this is bad when rethrowing the exception at the `catch` block in these methods.
We marked these places with a `(*)` in these methods.
-/
private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tactic) : TacticM Unit := do
let rec loop : List Tactic → TacticM Unit
| [] => throwErrorAt stx "unexpected syntax {indentD stx}"
| evalFn::evalFns => do
try
evalFn stx
catch
| ex@(Exception.error _ _) =>
match evalFns with
| [] => throw ex -- (*)
| evalFns => s.restore; loop evalFns
| ex@(Exception.internal id _) =>
if id == unsupportedSyntaxExceptionId then
s.restore; loop evalFns
else
throw ex
loop tactics
def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info :=
return Info.ofTacticInfo {
elaborator := (← read).elaborator
mctxBefore := mctxBefore
goalsBefore := goalsBefore
stx := stx
@ -151,23 +129,50 @@ def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do
@[inline] def withTacticInfoContext (stx : Syntax) (x : TacticM α) : TacticM α := do
withInfoContext x (← mkInitialTacticInfo stx)
/-
Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define
the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages,
and this is bad when rethrowing the exception at the `catch` block in these methods.
We marked these places with a `(*)` in these methods.
-/
private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List (KeyedDeclsAttribute.AttributeEntry Tactic)) : TacticM Unit := do
let rec loop
| [] => throwErrorAt stx "unexpected syntax {indentD stx}"
| evalFn::evalFns => do
try
withReader ({ · with elaborator := evalFn.decl }) <| withTacticInfoContext stx <| evalFn.value stx
catch
| ex@(Exception.error _ _) =>
match evalFns with
| [] => throw ex -- (*)
| evalFns => s.restore; loop evalFns
| ex@(Exception.internal id _) =>
if id == unsupportedSyntaxExceptionId then
s.restore; loop evalFns
else
throw ex
loop tactics
mutual
partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit :=
let rec loop : List Macro → TacticM Unit
partial def expandTacticMacroFns (stx : Syntax) (macros : List (KeyedDeclsAttribute.AttributeEntry Macro)) : TacticM Unit :=
let rec loop
| [] => throwErrorAt stx "tactic '{stx.getKind}' has not been implemented"
| m::ms => do
let scp ← getCurrMacroScope
try
let stx' ← adaptMacro m stx
evalTactic stx'
withReader ({ · with elaborator := m.decl }) do
withTacticInfoContext stx do
let stx' ← adaptMacro m.value stx
evalTactic stx'
catch ex =>
if ms.isEmpty then throw ex -- (*)
loop ms
loop macros
partial def expandTacticMacro (stx : Syntax) : TacticM Unit := do
expandTacticMacroFns stx (macroAttribute.getValues (← getEnv) stx.getKind)
expandTacticMacroFns stx (macroAttribute.getEntries (← getEnv) stx.getKind)
partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
@ -178,13 +183,13 @@ mutual
else do
trace[Elab.step] "{stx}"
let s ← Tactic.saveState
match tacticElabAttribute.getValues (← getEnv) stx.getKind with
match tacticElabAttribute.getEntries (← getEnv) stx.getKind with
| [] => expandTacticMacro stx
| evalFns => evalTacticUsing s stx evalFns
| _ => throwError m!"unexpected tactic{indentD stx}"
partial def evalTactic (stx : Syntax) : TacticM Unit :=
withTacticInfoContext stx (evalTacticAux stx)
evalTacticAux stx
end

View file

@ -23,7 +23,7 @@ private def checkUnusedIds (mvarId : MVarId) (unusedIds : List Name) : MetaM Uni
let fvarId ← elabAsFVar stx[1]
let ids := getInjectionNewIds stx[2]
liftMetaTactic fun mvarId => do
match ← Meta.injection mvarId fvarId ids (!ids.isEmpty) with
match (← Meta.injection mvarId fvarId ids (!ids.isEmpty)) with
| Meta.InjectionResult.solved => checkUnusedIds mvarId ids; pure []
| Meta.InjectionResult.subgoal mvarId' _ unusedIds => checkUnusedIds mvarId unusedIds; pure [mvarId']

View file

@ -1,7 +1,7 @@
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.ResolveName
import Lean.Util.Sorry
@ -390,10 +390,9 @@ open Level (LevelElabM)
def liftLevelM (x : LevelElabM α) : TermElabM α := do
let ctx ← read
let ref ← getRef
let mctx ← getMCtx
let ngen ← getNGen
let lvlCtx : Level.Context := { options := (← getOptions), ref := ref, autoBoundImplicit := ctx.autoBoundImplicit }
let lvlCtx : Level.Context := { options := (← getOptions), ref := (← getRef), autoBoundImplicit := ctx.autoBoundImplicit }
match (x lvlCtx).run { ngen := ngen, mctx := mctx, levelNames := (← getLevelNames) } with
| EStateM.Result.ok a newS => setMCtx newS.mctx; setNGen newS.ngen; setLevelNames newS.levelNames; pure a
| EStateM.Result.error ex _ => throw ex
@ -933,51 +932,80 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed (← saveContext))
pure mvar
def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
return (← get).syntheticMVars.find? fun d => d.mvarId == mvarId
def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) : TermElabM (Sum Info MVarId) := do
let isHole? : TermElabM (Option MVarId) := do
match e with
| Expr.mvar mvarId _ =>
match (← getSyntheticMVarDecl? mvarId) with
| some { kind := SyntheticMVarKind.tactic .., .. } => return mvarId
| some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId
| _ => return none
| _ => pure none
match (← isHole?) with
| none => return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType? }
| some mvarId => return Sum.inr mvarId
def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) : TermElabM Unit := do
withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx?) |> discard
/-
Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
an error is found. -/
private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool)
: List TermElab → TermElabM Expr
: List (KeyedDeclsAttribute.AttributeEntry TermElab) → TermElabM Expr
| [] => do throwError "unexpected syntax{indentD stx}"
| (elabFn::elabFns) => do
| (elabFn::elabFns) =>
try
elabFn stx expectedType?
-- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
withInfoContext' (mkInfo := mkTermInfo elabFn.decl (expectedType? := expectedType?) stx)
(try
elabFn.value stx expectedType?
catch ex => match ex with
| Exception.error ref msg =>
if (← read).errToSorry then
exceptionToSorry ex expectedType?
else
throw ex
| Exception.internal id _ =>
if (← read).errToSorry && id == abortTermExceptionId then
exceptionToSorry ex expectedType?
else if id == unsupportedSyntaxExceptionId then
throw ex -- to outer try
else if catchExPostpone && id == postponeExceptionId then
/- If `elab` threw `Exception.postpone`, we reset any state modifications.
For example, we want to make sure pending synthetic metavariables created by `elab` before
it threw `Exception.postpone` are discarded.
Note that we are also discarding the messages created by `elab`.
For example, consider the expression.
`((f.x a1).x a2).x a3`
Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
and new metavariables are created for the nested functions. -/
s.restore
postponeElabTerm stx expectedType?
else
throw ex)
catch ex => match ex with
| Exception.error ref msg =>
if (← read).errToSorry then
exceptionToSorry ex expectedType?
| Exception.internal id _ =>
if id == unsupportedSyntaxExceptionId then
s.restore -- also removes the info tree created above
elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
else
throw ex
| Exception.internal id _ =>
if (← read).errToSorry && id == abortTermExceptionId then
exceptionToSorry ex expectedType?
else if id == unsupportedSyntaxExceptionId then
s.restore
elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
else if catchExPostpone && id == postponeExceptionId then
/- If `elab` threw `Exception.postpone`, we reset any state modifications.
For example, we want to make sure pending synthetic metavariables created by `elab` before
it threw `Exception.postpone` are discarded.
Note that we are also discarding the messages created by `elab`.
For example, consider the expression.
`((f.x a1).x a2).x a3`
Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
and new metavariables are created for the nested functions. -/
s.restore
postponeElabTerm stx expectedType?
else
throw ex
| _ => throw ex
private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : TermElabM Expr := do
let s ← saveState
let k := stx.getKind
match termElabAttribute.getValues (← getEnv) k with
match termElabAttribute.getEntries (← getEnv) k with
| [] => throwError "elaboration function for '{k}' has not been implemented{indentD stx}"
| elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
@ -1107,40 +1135,21 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
checkMaxHeartbeats "elaborator"
withNestedTraces do
let env ← getEnv
let stxNew? ← catchInternalId unsupportedSyntaxExceptionId
(do let newStx ← adaptMacro (getMacros env) stx; pure (some newStx))
(fun _ => pure none)
match stxNew? with
| some stxNew => withMacroExpansion stx stxNew <| withRef stxNew <| elabTermAux expectedType? catchExPostpone implicitLambda stxNew
match (← liftMacroM (expandMacroImpl? env stx)) with
| some (decl, stxNew) =>
withInfoContext' (mkInfo := mkTermInfo decl (expectedType? := expectedType?) stx) <|
withMacroExpansion stx stxNew <|
withRef stxNew <|
elabTermAux expectedType? catchExPostpone implicitLambda stxNew
| _ =>
let implicit? ← if implicitLambda && (← read).implicitLambda then useImplicitLambda? stx expectedType? else pure none
match implicit? with
| some expectedType => elabImplicitLambda stx catchExPostpone expectedType
| none => elabUsingElabFns stx expectedType? catchExPostpone
def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) : TermElabM Unit := do
if (← getInfoState).enabled then
pushInfoLeaf <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx, expectedType? }
def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
return (← get).syntheticMVars.find? fun d => d.mvarId == mvarId
def mkTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) : TermElabM (Sum Info MVarId) := do
let isHole? : TermElabM (Option MVarId) := do
match e with
| Expr.mvar mvarId _ =>
match (← getSyntheticMVarDecl? mvarId) with
| some { kind := SyntheticMVarKind.tactic .., .. } => return mvarId
| some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId
| _ => return none
| _ => pure none
match (← isHole?) with
| none => return Sum.inl <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx, expectedType? }
| some mvarId => return Sum.inr mvarId
/-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/
def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do
addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), expectedType? } (field? := field?) (expectedType? := expectedType?)
addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), elaborator := Name.anonymous, expectedType? } (field? := field?) (expectedType? := expectedType?)
/--
Main function for elaborating terms.
@ -1160,7 +1169,7 @@ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr)
We use this flag to implement, for example, the `@` modifier. If `Context.implicitLambda == false`, then this parameter has no effect.
-/
def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx) (mkTermInfo stx (expectedType? := expectedType?))
withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
let e ← elabTerm stx expectedType? catchExPostpone implicitLambda

View file

@ -34,13 +34,6 @@ def expandOptNamedPrio (stx : Syntax) : MacroM Nat :=
| `(Parser.Command.namedPrio| (priority := $prio)) => evalPrio prio
| _ => Macro.throwUnsupported
def expandOptNamedName (stx : Syntax) : MacroM (Option Name) := do
if stx.isNone then
return none
else match stx[0] with
| `(Parser.Command.namedName| (name := $name)) => return name.getId
| _ => Macro.throwUnsupported
structure MacroStackElem where
before : Syntax
after : Syntax
@ -73,23 +66,22 @@ def addMacroStack {m} [Monad m] [MonadOptions m] (msgData : MessageData) (macroS
msgData ++ Format.line ++ "while expanding" ++ indentD elem.before)
msgData
def checkSyntaxNodeKind (k : Name) : AttrM Name := do
def checkSyntaxNodeKind [Monad m] [MonadEnv m] [MonadError m] (k : Name) : m Name := do
if Parser.isValidSyntaxNodeKind (← getEnv) k then pure k
else throwError "failed"
def checkSyntaxNodeKindAtNamespacesAux (k : Name) : Name → AttrM Name
| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespacesAux k p
def checkSyntaxNodeKindAtNamespaces [Monad m] [MonadEnv m] [MonadError m] (k : Name) : Name → m Name
| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
| Name.anonymous => checkSyntaxNodeKind k
| _ => throwError "failed"
def checkSyntaxNodeKindAtNamespaces (k : Name) : AttrM Name := do
def checkSyntaxNodeKindAtCurrentNamespaces (k : Name) : AttrM Name := do
let ctx ← read
checkSyntaxNodeKindAtNamespacesAux k ctx.currNamespace
checkSyntaxNodeKindAtNamespaces k ctx.currNamespace
def syntaxNodeKindOfAttrParam (defaultParserNamespace : Name) (stx : Syntax) : AttrM SyntaxNodeKind := do
let k ← Attribute.Builtin.getId stx
checkSyntaxNodeKind k
<|>
checkSyntaxNodeKindAtNamespaces k
checkSyntaxNodeKindAtCurrentNamespaces k
<|>
checkSyntaxNodeKind (defaultParserNamespace ++ k)
<|>
@ -119,17 +111,19 @@ constant mkMacroAttribute : IO (KeyedDeclsAttribute Macro)
builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute
private def expandMacroFns (stx : Syntax) : List Macro → MacroM Syntax
| [] => throw Macro.Exception.unsupportedSyntax
| m::ms => do
/--
Try to expand macro at syntax tree root and return macro declaration name and new syntax if successful.
Return none if all macros threw `Macro.Exception.unsupportedSyntax`.
-/
def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Syntax)) := fun stx => do
for e in macroAttribute.getEntries env stx.getKind do
try
m stx
let stx' ← e.value stx
return (e.decl, stx')
catch
| Macro.Exception.unsupportedSyntax => expandMacroFns stx ms
| Macro.Exception.unsupportedSyntax => pure ()
| ex => throw ex
def getMacros (env : Environment) : Macro := fun stx =>
expandMacroFns stx (macroAttribute.getValues env stx.getKind)
return none
class MonadMacroAdapter (m : Type → Type) where
getCurrMacroScope : m MacroScope
@ -142,20 +136,16 @@ instance (m n) [MonadLift m n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)
}
private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syntax) := do
try
let newStx ← getMacros env stx
pure (some newStx)
catch
| Macro.Exception.unsupportedSyntax => pure none
| ex => throw ex
@[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : MacroM α) : m α := do
def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : MacroM α) : m α := do
let env ← getEnv
let currNamespace ← getCurrNamespace
let openDecls ← getOpenDecls
let methods := Macro.mkMethods {
expandMacro? := expandMacro? env
-- TODO: record recursive expansions in info tree?
expandMacro? := fun stx => do
match (← expandMacroImpl? env stx) with
| some (_, stx) => some stx
| none => none
hasDecl := fun declName => return env.contains declName
getCurrNamespace := return currNamespace
resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n

View file

@ -29,15 +29,15 @@ structure Unhygienic.Context where
corresponding to `withFreshMacroScope` calls. -/
abbrev Unhygienic := ReaderT Lean.Unhygienic.Context $ StateM MacroScope
namespace Unhygienic
instance : MonadQuotation Unhygienic := {
getRef := do (← read).ref,
withRef := fun ref => withReader ({ · with ref := ref }),
getCurrMacroScope := do (← read).scope,
getMainModule := pure `UnhygienicMain,
instance : MonadQuotation Unhygienic where
getRef := do (← read).ref
withRef := fun ref => withReader ({ · with ref := ref })
getCurrMacroScope := do (← read).scope
getMainModule := pure `UnhygienicMain
withFreshMacroScope := fun x => do
let fresh ← modifyGet fun n => (n, n + 1)
withReader ({ · with scope := fresh}) x
}
protected def run {α : Type} (x : Unhygienic α) : α := (x ⟨Syntax.missing, firstFrontendMacroScope⟩).run' (firstFrontendMacroScope+1)
end Unhygienic

View file

@ -16,7 +16,7 @@ def synthesizeArgs (lemmaName : Name) (xs : Array Expr) (bis : Array BinderInfo)
return false
else if (← instantiateMVars x).isMVar then
if (← isProp type) then
match ← discharge? type with
match (← discharge? type) with
| some proof =>
unless (← isDefEq x proof) do
trace[Meta.Tactic.simp.discharge] "{lemmaName}, failed to assign proof{indentExpr type}"
@ -30,7 +30,7 @@ def synthesizeArgs (lemmaName : Name) (xs : Array Expr) (bis : Array BinderInfo)
return true
where
synthesizeInstance (x type : Expr) : SimpM Bool := do
match ← trySynthInstance type with
match (← trySynthInstance type) with
| LOption.some val =>
if (← isDefEq x val) then
return true

View file

@ -68,25 +68,26 @@ def optKind : Parser := optional ("(" >> nonReservedSymbol "kind" >> ":=" >> ide
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtinCommandParser] def «notation» := leading_parser Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := leading_parser Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident
def macroArgSimple := leading_parser ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
def macroArgSymbol := leading_parser strLit >> optional (atomic <| checkNoWsBefore >> "%" >> checkNoWsBefore >> ident)
def macroArg := macroArgSymbol <|> atomic macroArgSimple
def macroArg := leading_parser macroArgSymbol <|> atomic macroArgSimple
def macroHead := macroArg
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> incQuotDepth Tactic.seq1 >> ")" <|> termParser)
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> incQuotDepth (many1Unbox commandParser) >> ")" <|> termParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> incQuotDepth (categoryParserOfStack 2) >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
@[builtinCommandParser] def «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)
def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> termParser
def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1
def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> macroRhs (many1Unbox commandParser)
def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> macroRhs (categoryParserOfStack 2)
def macroTail := leading_parser macroTailTactic <|> macroTailCommand <|> macroTailDefault
@[builtinCommandParser] def «macro» := leading_parser suppressInsideQuot (optional docComment >> Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail)
@[builtinCommandParser] def «elab_rules» := leading_parser suppressInsideQuot ("elab_rules" >> optKind >> optional (" : " >> ident) >> Term.matchAlts)
@[builtinCommandParser] def «elab_rules» := leading_parser suppressInsideQuot (optional docComment >> Term.attrKind >> "elab_rules" >> optKind >> optional (" : " >> ident) >> optional (" <= " >> ident) >> Term.matchAlts)
def elabHead := macroHead
def elabArg := macroArg
def elabTail := atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
@[builtinCommandParser] def «elab» := leading_parser suppressInsideQuot (Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
def elabTail := leading_parser atomic (" : " >> ident >> optional (" <= " >> ident)) >> darrow >> termParser
@[builtinCommandParser] def «elab» := leading_parser suppressInsideQuot (optional docComment >> Term.attrKind >> "elab " >> optPrecedence >> optNamedName >> optNamedPrio >> elabHead >> many elabArg >> elabTail)
end Command

View file

@ -39,7 +39,7 @@ def setReducibleAttribute {m} [Monad m] [MonadEnv m] (declName : Name) : m Unit
setReducibilityStatus declName ReducibilityStatus.reducible
def isReducible {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
match ← getReducibilityStatus declName with
match (← getReducibilityStatus declName) with
| ReducibilityStatus.reducible => true
| _ => false

View file

@ -146,7 +146,7 @@ section Initialization
let opts := {} -- TODO
let inputCtx := Parser.mkInputContext m.text.source "<input>"
let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx
let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with
let leanpkgPath ← match (← IO.getEnv "LEAN_SYSROOT") with
| some path => pure <| System.FilePath.mk path / "bin" / "leanpkg"
| _ => pure <| (← appDir) / "leanpkg"
let leanpkgPath := leanpkgPath.withExtension System.FilePath.exeExtension

View file

@ -63,35 +63,45 @@ partial def handleDefinition (goToType? : Bool) (p : TextDocumentPositionParams)
let doc ← readDoc
let text := doc.meta.text
let hoverPos := text.lspPosToUtf8Pos p.position
let locationLinksFromDecl i n := do
let mod? ← findModuleOf? n
let modUri? ← match mod? with
| some modName =>
let modFname? ← rc.srcSearchPath.findWithExt "lean" modName
pure <| modFname?.map toFileUri
| none => pure <| some doc.meta.uri
let ranges? ← findDeclarationRanges? n
if let (some ranges, some modUri) := (ranges?, modUri?) then
let declRangeToLspRange (r : DeclarationRange) : Lsp.Range :=
{ start := ⟨r.pos.line - 1, r.charUtf16⟩
«end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ }
let ll : LocationLink := {
originSelectionRange? := (·.toLspRange text) <$> i.range?
targetUri := modUri
targetRange := declRangeToLspRange ranges.range
targetSelectionRange := declRangeToLspRange ranges.selectionRange
}
return #[ll]
return #[]
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure #[]) fun snap => do
for t in snap.cmdState.infoState.trees do
if let some (ci, Info.ofTermInfo i) := t.hoverableInfoAt? hoverPos then
let mut expr := i.expr
if goToType? then
expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType expr)
if let some n := expr.constName? then
let mod? ← ci.runMetaM i.lctx <| findModuleOf? n
let modUri? ← match mod? with
| some modName =>
let modFname? ← rc.srcSearchPath.findWithExt "lean" modName
pure <| modFname?.map toFileUri
| none => pure <| some doc.meta.uri
let ranges? ← ci.runMetaM i.lctx <| findDeclarationRanges? n
if let (some ranges, some modUri) := (ranges?, modUri?) then
let declRangeToLspRange (r : DeclarationRange) : Lsp.Range :=
{ start := ⟨r.pos.line - 1, r.charUtf16⟩
«end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ }
let ll : LocationLink := {
originSelectionRange? := some ⟨text.utf8PosToLspPos i.stx.getPos?.get!,
text.utf8PosToLspPos i.stx.getTailPos?.get!⟩
targetUri := modUri
targetRange := declRangeToLspRange ranges.range
targetSelectionRange := declRangeToLspRange ranges.selectionRange
}
return #[ll]
if let some (ci, i) := t.hoverableInfoAt? hoverPos then
if let Info.ofTermInfo ti := i then
let mut expr := ti.expr
if goToType? then
expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType expr)
if let some n := expr.constName? then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
if let some ei := i.toElabInfo? then
if ci.env.contains ei.elaborator then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
if ci.env.contains ei.stx.getKind then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
return #[]
open Elab in
@ -121,13 +131,6 @@ partial def handlePlainGoal (p : PlainGoalParams)
return none
def hasRange (stx : Syntax) : Bool :=
stx.getPos?.isSome && stx.getTailPos?.isSome
def rangeOfSyntax! (text : FileMap) (stx : Syntax) : Range :=
⟨text.utf8PosToLspPos <| stx.getPos?.get!,
text.utf8PosToLspPos <| stx.getTailPos?.get!⟩
open Elab in
partial def handlePlainTermGoal (p : PlainTermGoalParams)
: RequestM (RequestTask (Option PlainTermGoal)) := do
@ -137,11 +140,11 @@ partial def handlePlainTermGoal (p : PlainTermGoalParams)
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure none) fun snap => do
for t in snap.cmdState.infoState.trees do
if let some (ci, Info.ofTermInfo i) := t.termGoalAt? hoverPos then
if let some (ci, i@(Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
let goal ← ci.runMetaM i.lctx <| open Meta in do
let ty ← instantiateMVars <| i.expectedType?.getD (← inferType i.expr)
let ty ← instantiateMVars <| ti.expectedType?.getD (← inferType ti.expr)
withPPInaccessibleNames <| Meta.ppGoal (← mkFreshExprMVar ty).mvarId!
let range := if hasRange i.stx then rangeOfSyntax! text i.stx else ⟨p.position, p.position⟩
let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
return some { goal := toString goal, range }
return none
@ -151,12 +154,12 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
let text := doc.meta.text
let pos := text.lspPosToUtf8Pos p.position
let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight
| stx@`(doElem|return%$i $e) =>
if stx.getPos?.get! <= pos && pos < stx.getTailPos?.get! then
some { range := doRange?.getD (rangeOfSyntax! text i), kind? := DocumentHighlightKind.text }
else
highlightReturn? doRange? e
| `(do%$i $elems) => highlightReturn? (rangeOfSyntax! text i) elems
| stx@`(doElem|return%$i $e) => do
if let some range := i.getRange? then
if range.contains pos then
return some { range := doRange?.getD (range.toLspRange text), kind? := DocumentHighlightKind.text }
highlightReturn? doRange? e
| `(do%$i $elems) => highlightReturn? (i.getRange?.get!.toLspRange text) elems
| stx => stx.getArgs.findSome? (highlightReturn? doRange?)
withWaitFindSnap doc (fun s => s.endPos > pos)
@ -191,26 +194,25 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
| `(namespace $id) => sectionLikeToDocumentSymbols text stx stxs (id.getId.toString) SymbolKind.namespace id
| `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "<section>") SymbolKind.namespace (id.getD stx)
| `(end $(id)?) => ([], stx::stxs)
| _ =>
| _ => do
let (syms, stxs') := toDocumentSymbols text stxs
if stx.isOfKind ``Lean.Parser.Command.declaration && hasRange stx then
unless stx.isOfKind ``Lean.Parser.Command.declaration do
return (syms, stxs')
if let some stxRange := stx.getRange? then
let (name, selection) := match stx with
| `($dm:declModifiers $ak:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $val) =>
((·.getId.toString) <$> id |>.getD s!"instance {sig.reprint.getD ""}", id.getD sig)
| _ => match stx[1][1] with
| `(declId|$id:ident$[.{$ls,*}]?) => (id.getId.toString, id)
| _ => (stx[1][0].isIdOrAtom?.getD "<unknown>", stx[1][0])
if hasRange selection then
(DocumentSymbol.mk {
if let some selRange := selection.getRange? then
return (DocumentSymbol.mk {
name := name
kind := SymbolKind.method
range := rangeOfSyntax! text stx
selectionRange := rangeOfSyntax! text selection
range := stxRange.toLspRange text
selectionRange := selRange.toLspRange text
} :: syms, stxs')
else
(syms, stxs')
else
(syms, stxs')
return (syms, stxs')
sectionLikeToDocumentSymbols (text : FileMap) (stx : Syntax) (stxs : List Syntax) (name : String) (kind : SymbolKind) (selection : Syntax) :=
let (syms, stxs') := toDocumentSymbols text stxs
-- discard `end`
@ -219,12 +221,12 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
| endStx::_ => endStx
| [] => (stx::stxs').getLast!
-- we can assume that commands always have at least one position (see `parseCommand`)
let range := rangeOfSyntax! text (mkNullNode #[stx, endStx])
let range := (mkNullNode #[stx, endStx]).getRange?.get!.toLspRange text
(DocumentSymbol.mk {
name
kind
range
selectionRange := if hasRange selection then rangeOfSyntax! text selection else range
selectionRange := selection.getRange? |>.map (·.toLspRange text) |>.getD range
children? := syms.toArray
} :: syms', stxs'')
end
@ -276,16 +278,16 @@ where
else
stx.getArgs.forM go
highlightId (stx : Syntax) : ReaderT SemanticTokensContext (StateT SemanticTokensState RequestM) _ := do
if let (some pos, some tailPos) := (stx.getPos?, stx.getTailPos?) then
if let some range := stx.getRange? then
for t in (← read).infoState.trees do
for ti in t.deepestNodes (fun
| _, i@(Elab.Info.ofTermInfo ti), _ => match i.pos? with
| some ipos => if pos <= ipos && ipos < tailPos then some ti else none
| some ipos => if range.contains ipos then some ti else none
| _ => none
| _, _, _ => none) do
match ti.expr with
| Expr.fvar .. => addToken ti.stx SemanticTokenType.variable
| _ => if ti.stx.getPos?.get! > pos then addToken ti.stx SemanticTokenType.property
| _ => if ti.stx.getPos?.get! > range.start then addToken ti.stx SemanticTokenType.property
highlightKeyword stx := do
if let Syntax.atom info val := stx then
if val.bsize > 0 && val[0].isAlpha then
@ -347,4 +349,4 @@ builtin_initialize
registerLspRequestHandler "$/lean/plainGoal" PlainGoalParams (Option PlainGoal) handlePlainGoal
registerLspRequestHandler "$/lean/plainTermGoal" PlainTermGoalParams (Option PlainTermGoal) handlePlainTermGoal
end Lean.Server.FileWorker
end Lean.Server.FileWorker

View file

@ -8,6 +8,19 @@ import Lean.DocString
import Lean.Elab.InfoTree
import Lean.Util.Sorry
protected structure String.Range where
start : String.Pos
stop : String.Pos
deriving Inhabited, Repr
def String.Range.contains (r : String.Range) (pos : String.Pos) : Bool :=
r.start <= pos && pos < r.stop
def Lean.Syntax.getRange? (stx : Syntax) (originalOnly := false) : Option String.Range :=
match stx.getPos? originalOnly, stx.getTailPos? originalOnly with
| some start, some stop => some { start, stop }
| _, _ => none
namespace Lean.Elab
/--
@ -57,16 +70,27 @@ def Info.stx : Info → Syntax
| ofTacticInfo i => i.stx
| ofTermInfo i => i.stx
| ofCommandInfo i => i.stx
| ofMacroExpansionInfo i => i.before
| ofMacroExpansionInfo i => i.stx
| ofFieldInfo i => i.stx
| ofCompletionInfo i => i.stx
def Info.lctx : Info → LocalContext
| Info.ofTermInfo i => i.lctx
| Info.ofFieldInfo i => i.lctx
| _ => LocalContext.empty
def Info.pos? (i : Info) : Option String.Pos :=
i.stx.getPos? (originalOnly := true)
def Info.tailPos? (i : Info) : Option String.Pos :=
i.stx.getTailPos? (originalOnly := true)
def Info.range? (i : Info) : Option String.Range :=
i.stx.getRange? (originalOnly := true)
def Info.contains (i : Info) (pos : String.Pos) : Bool :=
i.range?.any (·.contains pos)
def Info.size? (i : Info) : Option Nat := OptionM.run do
let pos ← i.pos?
let tailPos ← i.tailPos?
@ -95,57 +119,57 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
/-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) :=
t.smallestInfo? fun i =>
if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
if pos ≤ hoverPos ∧ hoverPos < tailPos then
match i with
| Info.ofTermInfo ti =>
!ti.expr.isSyntheticSorry &&
-- TODO: see if we can get rid of this
#[identKind,
strLitKind,
charLitKind,
numLitKind,
scientificLitKind,
nameLitKind,
fieldIdxKind,
interpolatedStrLitKind,
interpolatedStrKind
].contains i.stx.getKind
| Info.ofFieldInfo _ => true
| _ => false
else false
else false
t.smallestInfo? fun i => do
if let Info.ofTermInfo ti := i then
if ti.expr.isSyntheticSorry then
return false
if i matches Info.ofFieldInfo _ || i.toElabInfo?.isSome then
return i.contains hoverPos
return false
/-- Construct a hover popup, if any, from an info node in a context.-/
def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
let lctx ← match i with
| Info.ofTermInfo i => i.lctx
| Info.ofFieldInfo i => i.lctx
| _ => return none
ci.runMetaM lctx do
ci.runMetaM i.lctx do
let mut fmts := #[]
if let some f ← fmtTerm? then
fmts := fmts.push f
if let some f ← fmtDoc? then
fmts := fmts.push f
if fmts.isEmpty then
none
else
f!"\n***\n".joinSep fmts.toList
where
fmtTerm? := do
match i with
| Info.ofTermInfo ti =>
let tp ← Meta.inferType ti.expr
let eFmt ← Meta.ppExpr ti.expr
let tpFmt ← Meta.ppExpr tp
let hoverFmt := f!"```lean
{eFmt} : {tpFmt}
-- try not to show too scary internals
let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else tpFmt
return some f!"```lean
{fmt}
```"
if let some n := ti.expr.constName? then
if let some doc ← findDocString? n then
return f!"{hoverFmt}\n***\n{doc}"
return hoverFmt
| Info.ofFieldInfo fi =>
let tp ← Meta.inferType fi.val
let tpFmt ← Meta.ppExpr tp
return f!"```lean
return some f!"```lean
{fi.name} : {tpFmt}
```"
| _ => return none
fmtDoc? := do
if let Info.ofTermInfo ti := i then
if let some n := ti.expr.constName? then
return ← findDocString? n
if let some ei := i.toElabInfo? then
return ← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind
return none
isAtomicFormat : Format → Bool
| Std.Format.text _ => true
| Std.Format.group f _ => isAtomicFormat f
| Std.Format.nest _ f => isAtomicFormat f
| _ => false
structure GoalsAtResult where
ctxInfo : ContextInfo
@ -208,10 +232,9 @@ partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option
else
headFns
t.smallestInfo? fun i => do
if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
if pos ≤ hoverPos ∧ hoverPos < tailPos then
if let Info.ofTermInfo ti := i then
return !ti.stx.isIdent || !headFns.contains pos
if i.contains hoverPos then
if let Info.ofTermInfo ti := i then
return !ti.stx.isIdent || !headFns.contains i.pos?.get!
false
where
/- Returns the position of the head function symbol, if it is an identifier. -/

View file

@ -75,7 +75,7 @@ def mapTask (t : Task α) (f : α → RequestM β) : RequestM (RequestTask β) :
def bindTask (t : Task α) (f : α → RequestM (RequestTask β)) : RequestM (RequestTask β) := fun rc => do
let t ← IO.bindTask t fun a => do
match ← f a rc with
match (← f a rc) with
| Except.error e => return Task.pure <| Except.ok <| Except.error e
| Except.ok t => return t.map Except.ok
return t.map fun

View file

@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Marc Huisinga
-/
import Lean.Data.Position
import Lean.Data.Lsp
import Lean.Server.InfoUtils
import Init.System.FilePath
namespace IO
@ -163,3 +164,6 @@ def takeWhile (p : α → Bool) : List α → List α
| hd :: tl => if p hd then hd :: takeWhile p tl else []
end List
def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range :=
⟨text.utf8PosToLspPos r.start, text.utf8PosToLspPos r.stop⟩

View file

@ -185,7 +185,7 @@ def topDown (stx : Syntax) (firstChoiceOnly := false) : TopDown := ⟨firstChoic
partial instance : ForIn m TopDown Syntax where
forIn := fun ⟨firstChoiceOnly, stx⟩ init f => do
let rec @[specialize] loop stx b [Inhabited (typeOf% b)] := do
match ← f stx b with
match (← f stx b) with
| ForInStep.yield b' =>
let mut b := b'
if let Syntax.node k args := stx then
@ -193,12 +193,12 @@ partial instance : ForIn m TopDown Syntax where
return ← loop args[0] b
else
for arg in args do
match ← loop arg b with
match (← loop arg b) with
| ForInStep.yield b' => b := b'
| ForInStep.done b' => return ForInStep.done b'
return ForInStep.yield b
| ForInStep.done b => return ForInStep.done b
match ← @loop stx init ⟨init⟩ with
match (← @loop stx init ⟨init⟩) with
| ForInStep.yield b => return b
| ForInStep.done b => return b

View file

@ -53,7 +53,7 @@ protected def max : RBNode α β → Option (Sigma (fun k => β k))
match (← f k v b) with
| r@(ForInStep.done _) => return r
| ForInStep.yield b => visit r b
match ← visit as init with
match (← visit as init) with
| ForInStep.done b => pure b
| ForInStep.yield b => pure b

View file

@ -1,8 +1,32 @@
add_library(shell OBJECT lean.cpp)
if(LLVM)
if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
set(LLVM_SYSTEM_LIBS "-lz -ltinfo")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
# macOS doesn't have -Bstatic, so let cmake search for the libraries
find_library(LIBZ NAMES z REQUIRED)
find_library(NCURSES NAMES ncurses REQUIRED)
set(LLVM_SYSTEM_LIBS "${LIBZ} ${NCURSES}")
else()
set(LLVM_SYSTEM_LIBS "-lz")
endif()
if(${STATIC} AND NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin"))
set(LEAN_EXE_LINKER_FLAGS "`${LLVM_TOOLS_BINARY_DIR}/llvm-config --link-static --ldflags --libs nativecodegen` -Wl,-Bstatic ${LLVM_SYSTEM_LIBS} -Wl,-Bdynamic")
else()
set(LEAN_EXE_LINKER_FLAGS "`${LLVM_TOOLS_BINARY_DIR}/llvm-config --ldflags --libs nativecodegen` ${LLVM_SYSTEM_LIBS}")
endif()
if (${CMAKE_SYSTEM_NAME} MATCHES "Windows")
set(LEAN_EXE_LINKER_FLAGS "${LEAN_EXE_LINKER_FLAGS} -lole32 -luuid")
endif()
else()
set(LEAN_EXE_LINKER_FLAGS "")
endif()
string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
add_custom_command(OUTPUT ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}
COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc ${CMAKE_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} $<TARGET_OBJECTS:shell> -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
COMMAND sh -c "LEANC_GMP=${GMP_LIBRARIES} LEAN_CXX='${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}' ${CMAKE_BINARY_DIR}/bin/leanc $<TARGET_OBJECTS:shell> ${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXE_LINKER_FLAGS} ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} -o ${CMAKE_BINARY_DIR}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"
VERBATIM
DEPENDS Init Std Lean leancpp shell)
add_custom_target(lean ALL

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -144,6 +144,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabAxiom_match__4___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualNamespace(lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_classInductiveSyntaxToView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__1(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandDeclIdNamespace_x3f_match__1(lean_object*);
@ -339,7 +340,6 @@ static lean_object* l_Lean_Elab_Command_expandInitCmd___closed__15;
static lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___closed__1;
uint8_t l_Lean_Syntax_isNone(lean_object*);
static lean_object* l_Lean_Elab_Command_expandInitCmd___closed__18;
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Modifiers_addAttribute(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@ -3337,7 +3337,7 @@ else
{
lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_9 = l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__2___closed__2;
x_10 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_9, x_3, x_4, x_5);
x_10 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_9, x_3, x_4, x_5);
x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
@ -3392,7 +3392,7 @@ else
{
lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_9 = l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__3___closed__2;
x_10 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_9, x_3, x_4, x_5);
x_10 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_9, x_3, x_4, x_5);
x_11 = !lean_is_exclusive(x_10);
if (x_11 == 0)
{
@ -3447,7 +3447,7 @@ else
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___closed__2;
x_9 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_8, x_2, x_3, x_4);
x_9 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_8, x_2, x_3, x_4);
x_10 = !lean_is_exclusive(x_9);
if (x_10 == 0)
{
@ -3767,7 +3767,7 @@ lean_object* x_15; lean_object* x_16; uint8_t x_17;
lean_dec(x_2);
lean_dec(x_1);
x_15 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___lambda__2___closed__2;
x_16 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_15, x_6, x_7, x_8);
x_16 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_15, x_6, x_7, x_8);
x_17 = !lean_is_exclusive(x_16);
if (x_17 == 0)
{
@ -3963,7 +3963,7 @@ lean_dec(x_38);
lean_dec(x_15);
lean_dec(x_14);
x_58 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__3___closed__2;
x_59 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_58, x_36, x_7, x_39);
x_59 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_58, x_36, x_7, x_39);
x_60 = !lean_is_exclusive(x_59);
if (x_60 == 0)
{
@ -7323,7 +7323,7 @@ x_33 = l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__1___clos
x_34 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
x_35 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_34, x_5, x_6, x_27);
x_35 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_34, x_5, x_6, x_27);
x_36 = !lean_is_exclusive(x_35);
if (x_36 == 0)
{
@ -7426,7 +7426,7 @@ x_70 = l_Array_forInUnsafe_loop___at_Lean_Elab_Command_elabAttr___spec__1___clos
x_71 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_71, 0, x_69);
lean_ctor_set(x_71, 1, x_70);
x_72 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_71, x_5, x_6, x_64);
x_72 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_71, x_5, x_6, x_64);
x_73 = lean_ctor_get(x_72, 0);
lean_inc(x_73);
x_74 = lean_ctor_get(x_72, 1);

File diff suppressed because it is too large Load diff

View file

@ -182,13 +182,13 @@ static lean_object* l_Lean_getConstInfoCtor___at_Lean_Elab_Deriving_BEq_mkMatch_
lean_object* l_Lean_Elab_registerBuiltinDerivingHandler(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Deriving_BEq_0__Lean_Elab_Deriving_BEq_mkBEqInstanceCmds___closed__10;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__4___closed__11;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__5___lambda__1___closed__10;
static lean_object* l_Lean_Elab_Deriving_BEq_mkMutualBlock___closed__2;
lean_object* l_Lean_getConstInfoCtor___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_BEq_mkMutualBlock(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_BEq_mkMutualBlock___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_getConstInfoCtor___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__1___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Elab_Deriving_mkInductArgNames___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__5___lambda__1___closed__2;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_BEq_mkMatch_mkAlts___spec__4___closed__12;
@ -5417,7 +5417,7 @@ x_29 = 0;
x_30 = lean_usize_of_nat(x_22);
lean_dec(x_22);
x_31 = lean_box(0);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
lean_dec(x_2);
lean_dec(x_20);
if (lean_obj_tag(x_32) == 0)
@ -5522,7 +5522,7 @@ x_56 = 0;
x_57 = lean_usize_of_nat(x_47);
lean_dec(x_47);
x_58 = lean_box(0);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
lean_dec(x_2);
lean_dec(x_45);
if (lean_obj_tag(x_59) == 0)

View file

@ -57,6 +57,7 @@ static lean_object* l_Lean_Elab_elabDeriving___closed__7;
static lean_object* l_Lean_Elab_defaultHandler___closed__6;
lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_elabDeriving___spec__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_elabDeriving___spec__8(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_LocalContext_empty;
static lean_object* l_Lean_Elab_elabDeriving___closed__3;
lean_object* l_Lean_ConstantInfo_levelParams(lean_object*);
@ -132,7 +133,6 @@ lean_object* lean_st_ref_set(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_elabDeriving___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_getConstInfo___at_Lean_Elab_elabDeriving___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabDeriving(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_getOptDerivingClasses___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinDerivingHandler(lean_object*, lean_object*, lean_object*);
@ -863,7 +863,7 @@ x_10 = l_Lean_throwUnknownConstant___at_Lean_Elab_elabDeriving___spec__5___close
x_11 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_11, x_2, x_3, x_4);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_11, x_2, x_3, x_4);
return x_12;
}
}
@ -1359,94 +1359,98 @@ lean_inc(x_8);
x_19 = l_Lean_mkConstWithLevelParams___at_Lean_Elab_elabDeriving___spec__6(x_8, x_4, x_5, x_18);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26;
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
x_22 = l_Lean_LocalContext_empty;
x_23 = lean_alloc_ctor(0, 4, 0);
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_3);
lean_ctor_set(x_23, 2, x_20);
lean_ctor_set(x_23, 3, x_1);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
x_25 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Command_elabEnd___spec__3(x_24, x_4, x_5, x_21);
lean_ctor_set(x_23, 1, x_1);
x_24 = l_Lean_LocalContext_empty;
x_25 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
lean_ctor_set(x_25, 2, x_3);
lean_ctor_set(x_25, 3, x_20);
x_26 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_26, 0, x_25);
x_27 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Command_elabEnd___spec__3(x_26, x_4, x_5, x_21);
lean_dec(x_4);
x_26 = !lean_is_exclusive(x_25);
if (x_26 == 0)
x_28 = !lean_is_exclusive(x_27);
if (x_28 == 0)
{
lean_object* x_27;
x_27 = lean_ctor_get(x_25, 0);
lean_object* x_29;
x_29 = lean_ctor_get(x_27, 0);
lean_dec(x_29);
lean_ctor_set(x_27, 0, x_8);
return x_27;
}
else
{
lean_object* x_30; lean_object* x_31;
x_30 = lean_ctor_get(x_27, 1);
lean_inc(x_30);
lean_dec(x_27);
lean_ctor_set(x_25, 0, x_8);
return x_25;
}
else
{
lean_object* x_28; lean_object* x_29;
x_28 = lean_ctor_get(x_25, 1);
lean_inc(x_28);
lean_dec(x_25);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_8);
lean_ctor_set(x_29, 1, x_28);
return x_29;
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_8);
lean_ctor_set(x_31, 1, x_30);
return x_31;
}
}
else
{
uint8_t x_30;
uint8_t x_32;
lean_dec(x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_30 = !lean_is_exclusive(x_19);
if (x_30 == 0)
x_32 = !lean_is_exclusive(x_19);
if (x_32 == 0)
{
return x_19;
}
else
{
lean_object* x_31; lean_object* x_32; lean_object* x_33;
x_31 = lean_ctor_get(x_19, 0);
x_32 = lean_ctor_get(x_19, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_19, 0);
x_34 = lean_ctor_get(x_19, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_19);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
return x_33;
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
}
else
{
uint8_t x_34;
uint8_t x_36;
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_34 = !lean_is_exclusive(x_7);
if (x_34 == 0)
x_36 = !lean_is_exclusive(x_7);
if (x_36 == 0)
{
return x_7;
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_35 = lean_ctor_get(x_7, 0);
x_36 = lean_ctor_get(x_7, 1);
lean_inc(x_36);
lean_inc(x_35);
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_7, 0);
x_38 = lean_ctor_get(x_7, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_7);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
return x_37;
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
}

View file

@ -222,7 +222,6 @@ extern lean_object* l_Lean_instInhabitedName;
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinDerivingHandler(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__5;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__28;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__30;
static lean_object* l_Lean_Elab_Deriving_DecEq_initFn____x40_Lean_Elab_Deriving_DecEq___hyg_2438____closed__1;
@ -230,6 +229,7 @@ lean_object* l_Lean_Elab_Deriving_DecEq_mkAuxFunction(lean_object*, lean_object*
static lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_DecEq_mkMatch_mkAlts___spec__6___lambda__1___closed__1;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__14;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__93;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_DecEq_mkAuxFunction___closed__17;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__33;
static lean_object* l_Lean_Elab_Deriving_DecEq_mkMatch_mkSameCtorRhs___closed__18;
@ -7364,7 +7364,7 @@ x_31 = 0;
x_32 = lean_usize_of_nat(x_24);
lean_dec(x_24);
x_33 = lean_box(0);
x_34 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_22, x_31, x_32, x_33, x_2, x_3, x_23);
x_34 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_22, x_31, x_32, x_33, x_2, x_3, x_23);
lean_dec(x_2);
lean_dec(x_22);
if (lean_obj_tag(x_34) == 0)
@ -7469,7 +7469,7 @@ x_58 = 0;
x_59 = lean_usize_of_nat(x_49);
lean_dec(x_49);
x_60 = lean_box(0);
x_61 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_47, x_58, x_59, x_60, x_2, x_3, x_48);
x_61 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_47, x_58, x_59, x_60, x_2, x_3, x_48);
lean_dec(x_2);
lean_dec(x_47);
if (lean_obj_tag(x_61) == 0)

View file

@ -381,13 +381,13 @@ static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mk
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__3___closed__4;
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__5___lambda__1___closed__48;
static lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__5___lambda__2___closed__4;
static lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__3___closed__14;
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__5___lambda__1___closed__34;
lean_object* l_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts_match__3(lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler_mkAlts___spec__5___lambda__1___closed__5;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler___lambda__1___closed__19;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkToJsonInstanceHandler___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*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Deriving_FromToJson_mkFromJsonInstanceHandler_mkAlts___spec__5___lambda__1___closed__41;
@ -6473,7 +6473,7 @@ x_35 = 0;
x_36 = lean_usize_of_nat(x_28);
lean_dec(x_28);
x_37 = lean_box(0);
x_38 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_26, x_35, x_36, x_37, x_2, x_3, x_27);
x_38 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_26, x_35, x_36, x_37, x_2, x_3, x_27);
lean_dec(x_2);
lean_dec(x_26);
if (lean_obj_tag(x_38) == 0)
@ -6578,7 +6578,7 @@ x_62 = 0;
x_63 = lean_usize_of_nat(x_53);
lean_dec(x_53);
x_64 = lean_box(0);
x_65 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_51, x_62, x_63, x_64, x_2, x_3, x_52);
x_65 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_51, x_62, x_63, x_64, x_2, x_3, x_52);
lean_dec(x_2);
lean_dec(x_51);
if (lean_obj_tag(x_65) == 0)
@ -6741,7 +6741,7 @@ x_96 = 0;
x_97 = lean_usize_of_nat(x_89);
lean_dec(x_89);
x_98 = lean_box(0);
x_99 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_87, x_96, x_97, x_98, x_2, x_3, x_88);
x_99 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_87, x_96, x_97, x_98, x_2, x_3, x_88);
lean_dec(x_2);
lean_dec(x_87);
if (lean_obj_tag(x_99) == 0)
@ -6846,7 +6846,7 @@ x_123 = 0;
x_124 = lean_usize_of_nat(x_114);
lean_dec(x_114);
x_125 = lean_box(0);
x_126 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_112, x_123, x_124, x_125, x_2, x_3, x_113);
x_126 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_112, x_123, x_124, x_125, x_2, x_3, x_113);
lean_dec(x_2);
lean_dec(x_112);
if (lean_obj_tag(x_126) == 0)
@ -12233,7 +12233,7 @@ x_35 = 0;
x_36 = lean_usize_of_nat(x_28);
lean_dec(x_28);
x_37 = lean_box(0);
x_38 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_26, x_35, x_36, x_37, x_2, x_3, x_27);
x_38 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_26, x_35, x_36, x_37, x_2, x_3, x_27);
lean_dec(x_2);
lean_dec(x_26);
if (lean_obj_tag(x_38) == 0)
@ -12338,7 +12338,7 @@ x_62 = 0;
x_63 = lean_usize_of_nat(x_53);
lean_dec(x_53);
x_64 = lean_box(0);
x_65 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_51, x_62, x_63, x_64, x_2, x_3, x_52);
x_65 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_51, x_62, x_63, x_64, x_2, x_3, x_52);
lean_dec(x_2);
lean_dec(x_51);
if (lean_obj_tag(x_65) == 0)
@ -12501,7 +12501,7 @@ x_96 = 0;
x_97 = lean_usize_of_nat(x_89);
lean_dec(x_89);
x_98 = lean_box(0);
x_99 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_87, x_96, x_97, x_98, x_2, x_3, x_88);
x_99 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_87, x_96, x_97, x_98, x_2, x_3, x_88);
lean_dec(x_2);
lean_dec(x_87);
if (lean_obj_tag(x_99) == 0)
@ -12606,7 +12606,7 @@ x_123 = 0;
x_124 = lean_usize_of_nat(x_114);
lean_dec(x_114);
x_125 = lean_box(0);
x_126 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_112, x_123, x_124, x_125, x_2, x_3, x_113);
x_126 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_112, x_123, x_124, x_125, x_2, x_3, x_113);
lean_dec(x_2);
lean_dec(x_112);
if (lean_obj_tag(x_126) == 0)

View file

@ -180,8 +180,8 @@ lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_registerBuiltinDerivingHandler(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_Hashable_mkHashFuncs___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__4___closed__17;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Elab_Deriving_mkInductArgNames___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Hashable_mkMatch_mkAlts___spec__3___closed__2;
static lean_object* l_Lean_Elab_Deriving_Hashable_mkHashFuncs___closed__2;
@ -4274,7 +4274,7 @@ x_29 = 0;
x_30 = lean_usize_of_nat(x_22);
lean_dec(x_22);
x_31 = lean_box(0);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
lean_dec(x_2);
lean_dec(x_20);
if (lean_obj_tag(x_32) == 0)
@ -4379,7 +4379,7 @@ x_56 = 0;
x_57 = lean_usize_of_nat(x_47);
lean_dec(x_47);
x_58 = lean_box(0);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
lean_dec(x_2);
lean_dec(x_45);
if (lean_obj_tag(x_59) == 0)

View file

@ -189,9 +189,9 @@ lean_object* l_Lean_Elab_registerBuiltinDerivingHandler(lean_object*, lean_objec
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__13;
lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__1;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_pop(lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Deriving_Ord_mkOrdInstanceHandler___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_Ord_mkAuxFunction(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__14;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Ord_mkMatch_mkAlts___spec__5___closed__28;
@ -5528,7 +5528,7 @@ x_29 = 0;
x_30 = lean_usize_of_nat(x_22);
lean_dec(x_22);
x_31 = lean_box(0);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
lean_dec(x_2);
lean_dec(x_20);
if (lean_obj_tag(x_32) == 0)
@ -5633,7 +5633,7 @@ x_56 = 0;
x_57 = lean_usize_of_nat(x_47);
lean_dec(x_47);
x_58 = lean_box(0);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
lean_dec(x_2);
lean_dec(x_45);
if (lean_obj_tag(x_59) == 0)

View file

@ -248,7 +248,6 @@ static lean_object* l___private_Lean_Elab_Deriving_Repr_0__Lean_Elab_Deriving_Re
static lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__3___lambda__1___closed__51;
static lean_object* l_Lean_Elab_Deriving_Repr_mkAuxFunction___lambda__1___closed__18;
static lean_object* l_Lean_Elab_Deriving_Repr_mkAuxFunction___lambda__1___closed__15;
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Deriving_Repr_mkMutualBlock___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Deriving_Repr_mkMutualBlock___closed__1;
static lean_object* l_Lean_Elab_Deriving_Repr_mkReprHeader___rarg___closed__16;
@ -261,6 +260,7 @@ lean_object* l_Lean_Elab_Deriving_Repr_mkAuxFunction___boxed(lean_object*, lean_
static lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__3___lambda__1___closed__24;
lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__4___boxed(lean_object**);
lean_object* l_List_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForInduct_mkAlts___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_List_head_x21___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__1___closed__1;
static lean_object* l_Std_Range_forIn_loop___at_Lean_Elab_Deriving_Repr_mkBodyForStruct___spec__4___closed__1;
lean_object* l_Lean_Meta_forallTelescopeReducing___at_Lean_Elab_Deriving_mkInductArgNames___spec__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -7417,7 +7417,7 @@ x_29 = 0;
x_30 = lean_usize_of_nat(x_22);
lean_dec(x_22);
x_31 = lean_box(0);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
x_32 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_20, x_29, x_30, x_31, x_2, x_3, x_21);
lean_dec(x_2);
lean_dec(x_20);
if (lean_obj_tag(x_32) == 0)
@ -7522,7 +7522,7 @@ x_56 = 0;
x_57 = lean_usize_of_nat(x_47);
lean_dec(x_47);
x_58 = lean_box(0);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__13(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
x_59 = l_Array_foldlMUnsafe_fold___at_Lean_Elab_Command_elabCommand___spec__12(x_45, x_56, x_57, x_58, x_2, x_3, x_46);
lean_dec(x_2);
lean_dec(x_45);
if (lean_obj_tag(x_59) == 0)

File diff suppressed because one or more lines are too long

View file

@ -71,7 +71,6 @@ lean_object* l_Lean_Elab_Term_elabForIn_match__1(lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__12;
lean_object* lean_st_ref_take(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabBinRel___lambda__3___closed__2;
lean_object* l_Lean_Elab_withMacroExpansionInfo___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__2(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_elabBinOp_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabBinRel___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn_getMonad___closed__6;
@ -108,6 +107,7 @@ extern lean_object* l_Lean_Elab_Term_termElabAttribute;
static lean_object* l___regBuiltin_Lean_Elab_Term_elabBinRel___closed__11;
lean_object* l_Lean_Elab_Term_elabForIn_throwFailure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__4;
lean_object* l_Lean_Elab_withMacroExpansionInfo___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn_throwFailure___closed__1;
lean_object* l_Lean_Elab_Term_elabBinOp_match__2(lean_object*);
static lean_object* l_Lean_Elab_Term_elabForIn___closed__8;
@ -2938,7 +2938,7 @@ x_35 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabBinOp___lambda__1), 10, 3
lean_closure_set(x_35, 0, x_1);
lean_closure_set(x_35, 1, x_33);
lean_closure_set(x_35, 2, x_34);
x_36 = l_Lean_Elab_withMacroExpansionInfo___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__2(x_1, x_33, x_35, x_3, x_4, x_5, x_6, x_7, x_8, x_24);
x_36 = l_Lean_Elab_withMacroExpansionInfo___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__7(x_1, x_33, x_35, x_3, x_4, x_5, x_6, x_7, x_8, x_24);
return x_36;
}
else

View file

@ -17,13 +17,13 @@ lean_object* l_Lean_registerTraceClass(lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_List_head_x21___at_Lean_Elab_Command_instMonadOptionsCommandElabM___spec__1(lean_object*);
lean_object* l_Lean_Elab_Frontend_runCommandElabM_match__1___rarg(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2;
static lean_object* l_Lean_Elab_process___closed__2;
lean_object* l_Lean_Elab_IO_processCommands_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_elabCommandAtFrontend___lambda__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_State_commands___default;
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2;
lean_object* l_Lean_Elab_IO_processCommands(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_processCommand_match__1___rarg(lean_object*, lean_object*);
lean_object* lean_run_frontend(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -31,7 +31,6 @@ static lean_object* l_Lean_Elab_process___closed__1;
lean_object* lean_environment_set_main_module(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_setCommandState___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_checkTraceOption(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__1;
lean_object* l_Lean_Elab_Frontend_getCommandState___rarg___boxed(lean_object*, lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_elabCommandAtFrontend___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -39,18 +38,18 @@ lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Frontend_runCommandElabM(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__4;
lean_object* l_Lean_Elab_Frontend_processCommand_match__1(lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__4;
lean_object* lean_profileit(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_enableInfoTree___at_Lean_Elab_Frontend_elabCommandAtFrontend___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__1;
lean_object* l_Lean_Elab_processHeader(lean_object*, lean_object*, lean_object*, lean_object*, uint32_t, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__3;
lean_object* l_Lean_Elab_runFrontend_match__1___rarg(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__5;
lean_object* l_List_forIn_loop___at_Lean_Elab_runFrontend___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageLog_toList(lean_object*);
lean_object* l_Lean_Elab_runFrontend_match__1(lean_object*);
lean_object* l_Lean_Elab_Frontend_processCommand___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__3;
static lean_object* l_Lean_Elab_process___closed__4;
lean_object* l_Lean_MessageData_toString(lean_object*, lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
@ -58,6 +57,7 @@ lean_object* l_Lean_Elab_Frontend_getInputContext___boxed(lean_object*, lean_obj
uint8_t l_Lean_KVMap_getBool(lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_Elab_Frontend_setParserState___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_print___at_IO_println___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__5;
lean_object* l_Lean_Elab_Command_mkState(lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at_Lean_Elab_runFrontend___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_st_mk_ref(lean_object*, lean_object*);
@ -65,7 +65,7 @@ lean_object* l_Lean_Elab_Frontend_elabCommandAtFrontend(lean_object*, lean_objec
lean_object* l_Lean_Elab_getPrintMessageEndPos___boxed(lean_object*);
static lean_object* l_Lean_Elab_Frontend_runCommandElabM___rarg___closed__1;
static lean_object* l_Lean_Elab_Frontend_processCommand___closed__1;
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747_(lean_object*);
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753_(lean_object*);
lean_object* l_Lean_Elab_Frontend_updateCmdPos(lean_object*);
extern lean_object* l_Lean_firstFrontendMacroScope;
lean_object* l_Lean_Elab_Command_elabCommand(lean_object*, lean_object*, lean_object*, lean_object*);
@ -2450,7 +2450,7 @@ return x_47;
}
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__1() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__1() {
_start:
{
lean_object* x_1;
@ -2458,17 +2458,17 @@ x_1 = lean_mk_string("printMessageEndPos");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__1;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__3() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__3() {
_start:
{
uint8_t x_1; lean_object* x_2;
@ -2478,7 +2478,7 @@ lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__4() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__4() {
_start:
{
lean_object* x_1;
@ -2486,13 +2486,13 @@ x_1 = lean_mk_string("print end position of each message in addition to start po
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__5() {
static lean_object* _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__3;
x_1 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__3;
x_2 = l_Lean_Elab_Frontend_runCommandElabM___rarg___closed__2;
x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__4;
x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__4;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
@ -2500,12 +2500,12 @@ lean_ctor_set(x_4, 2, x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747_(lean_object* x_1) {
lean_object* l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2;
x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__5;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2;
x_3 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__5;
x_4 = lean_register_option(x_2, x_3, x_1);
if (lean_obj_tag(x_4) == 0)
{
@ -2545,7 +2545,7 @@ uint8_t l_Lean_Elab_getPrintMessageEndPos(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; uint8_t x_4;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2;
x_2 = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2;
x_3 = 0;
x_4 = l_Lean_KVMap_getBool(x_1, x_2, x_3);
return x_4;
@ -3109,17 +3109,17 @@ l_Lean_Elab_process___closed__4 = _init_l_Lean_Elab_process___closed__4();
lean_mark_persistent(l_Lean_Elab_process___closed__4);
l_Lean_Elab_process___closed__5 = _init_l_Lean_Elab_process___closed__5();
lean_mark_persistent(l_Lean_Elab_process___closed__5);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__3);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__4 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__4();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__5 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__5();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747____closed__5);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_747_(lean_io_mk_world());
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__1 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__1();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__1);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__2);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__3 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__3();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__3);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__4 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__4();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__4);
l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__5 = _init_l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__5();
lean_mark_persistent(l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753____closed__5);
res = l_Lean_Elab_initFn____x40_Lean_Elab_Frontend___hyg_753_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

View file

@ -31,6 +31,7 @@ lean_object* l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(lean_object*, lean_obj
lean_object* l_Lean_resolveGlobalName___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__2;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__4;
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_resolveGlobalConstNoOverload___spec__1(lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__9;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__8;
@ -50,7 +51,6 @@ lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenI
lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1___closed__3;
lean_object* l_Lean_resolveGlobalConst___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_resolveGlobalConstNoOverload___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__1___closed__1;
static lean_object* l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheorems___spec__4___closed__3;
static lean_object* l___regBuiltin_Lean_Elab_Command_elabGenInjectiveTheorems___closed__10;
@ -176,7 +176,7 @@ x_10 = l_Lean_throwUnknownConstant___at_Lean_Elab_Command_elabGenInjectiveTheore
x_11 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_11, x_2, x_3, x_4);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_11, x_2, x_3, x_4);
return x_12;
}
}

View file

@ -37,6 +37,7 @@ lean_object* l_Lean_Elab_withInfoContext_x27(lean_object*);
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_TacticInfo_format(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__1(lean_object*);
static lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_TermInfo_format___lambda__1___closed__2;
@ -56,11 +57,11 @@ lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_modifyInfoTrees___rarg(
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos(lean_object*, lean_object*, lean_object*);
size_t l_USize_sub(size_t, size_t);
lean_object* l_Lean_Elab_InfoTree_format_match__1(lean_object*);
lean_object* l_Lean_Elab_instInhabitedElabInfo;
lean_object* l_Lean_Meta_ppExpr(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_findInfo_x3f_match__1(lean_object*);
lean_object* l_Lean_Elab_TermInfo_runMetaM(lean_object*);
static lean_object* l_Lean_Elab_TermInfo_format___lambda__1___closed__5;
static lean_object* l_Lean_Elab_instInhabitedContextInfo___closed__5;
lean_object* l_Lean_Elab_withInfoContext_x27_match__1(lean_object*);
lean_object* lean_st_ref_get(lean_object*, lean_object*);
@ -201,6 +202,7 @@ lean_object* lean_st_mk_ref(lean_object*, lean_object*);
lean_object* l_Lean_Core_getMaxHeartbeats(lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__4;
static lean_object* l_Lean_Elab_instInhabitedContextInfo___closed__1;
lean_object* l_Lean_Elab_Info_toElabInfo_x3f___boxed(lean_object*);
lean_object* l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_object*, lean_object*);
lean_object* l_Lean_Elab_ContextInfo_toPPContext(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__9;
@ -222,6 +224,7 @@ lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__5(lean_object*, le
static uint64_t l_Lean_Elab_instInhabitedTermInfo___closed__5;
lean_object* l_Lean_Elab_withInfoContext_x27___rarg___lambda__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Elab_assignInfoHoleId___spec__3(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instInhabitedElabInfo___closed__1;
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos_match__1(lean_object*);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_InfoTree_substitute_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -236,6 +239,7 @@ extern lean_object* l_Lean_firstFrontendMacroScope;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_CompletionInfo_stx___boxed(lean_object*);
lean_object* l_Lean_Elab_ContextInfo_ppGoals___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Info_toElabInfo_x3f(lean_object*);
lean_object* l_Lean_Elab_Info_updateContext_x3f_match__1(lean_object*);
size_t l_USize_mul(size_t, size_t);
static lean_object* l_Lean_Elab_ContextInfo_ppGoals___closed__2;
@ -293,6 +297,7 @@ lean_object* l_Std_PersistentArray_findSomeMAux___at_Lean_Elab_InfoTree_findInfo
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_InfoTree_findInfo_x3f___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instInhabitedInfo___closed__1;
lean_object* l_Lean_Elab_CommandInfo_format(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Name_isAnonymous(lean_object*);
lean_object* l_Lean_Elab_assignInfoHoleId(lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_MacroExpansionInfo_format___closed__1;
@ -324,7 +329,6 @@ lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instInhabitedTermInfo___closed__3;
lean_object* l_Lean_ppTerm(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__9;
static lean_object* l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
lean_object* l_Lean_Elab_withInfoTreeContext___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_enableInfoTree___rarg___lambda__1___boxed(lean_object*, lean_object*);
@ -347,7 +351,9 @@ static lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_f
lean_object* l_Lean_Elab_TermInfo_runMetaM___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailPos_x3f(lean_object*, uint8_t);
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1;
static lean_object* l_Lean_Elab_ContextInfo_mctx___default___closed__2;
lean_object* l_List_mapM___at_Lean_Elab_ContextInfo_ppGoals___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__5;
@ -392,6 +398,7 @@ lean_object* l_Lean_Elab_withInfoHole___rarg___lambda__4(lean_object*, lean_obje
lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_CompletionInfo_stx_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_ContextInfo_runMetaM___rarg___closed__3;
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Elab_withInfoTreeContext___rarg___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_mkEmptyEntries(lean_object*, lean_object*);
@ -614,6 +621,26 @@ x_1 = l_Lean_Elab_instInhabitedContextInfo___closed__9;
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instInhabitedElabInfo___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = lean_box(0);
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;
}
}
static lean_object* _init_l_Lean_Elab_instInhabitedElabInfo() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instInhabitedElabInfo___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instInhabitedTermInfo___closed__1() {
_start:
{
@ -688,13 +715,13 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_instInhabitedTermInfo___closed__4;
x_3 = l_Lean_Elab_instInhabitedTermInfo___closed__6;
x_4 = lean_box(0);
x_2 = l_Lean_Elab_instInhabitedElabInfo___closed__1;
x_3 = l_Lean_Elab_instInhabitedTermInfo___closed__4;
x_4 = l_Lean_Elab_instInhabitedTermInfo___closed__6;
x_5 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_5, 0, x_2);
lean_ctor_set(x_5, 1, x_1);
lean_ctor_set(x_5, 2, x_3);
lean_ctor_set(x_5, 1, x_3);
lean_ctor_set(x_5, 2, x_1);
lean_ctor_set(x_5, 3, x_4);
return x_5;
}
@ -711,7 +738,7 @@ static lean_object* _init_l_Lean_Elab_instInhabitedCommandInfo() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
x_1 = l_Lean_Elab_instInhabitedElabInfo___closed__1;
return x_1;
}
}
@ -835,18 +862,19 @@ _start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_2; lean_object* x_3;
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 3);
lean_inc(x_3);
return x_3;
x_3 = lean_ctor_get(x_2, 0);
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
return x_4;
}
else
{
lean_object* x_4;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
return x_4;
lean_object* x_5;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
return x_5;
}
}
}
@ -888,13 +916,13 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_box(0);
x_2 = l_Lean_Elab_ContextInfo_mctx___default___closed__4;
x_3 = lean_box(0);
x_2 = l_Lean_Elab_instInhabitedElabInfo___closed__1;
x_3 = l_Lean_Elab_ContextInfo_mctx___default___closed__4;
x_4 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_1);
lean_ctor_set(x_4, 2, x_3);
lean_ctor_set(x_4, 3, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set(x_4, 2, x_1);
lean_ctor_set(x_4, 3, x_3);
lean_ctor_set(x_4, 4, x_1);
return x_4;
}
@ -3110,11 +3138,83 @@ lean_dec(x_1);
return x_3;
}
}
static lean_object* _init_l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" @ ");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = l_Lean_Name_isAnonymous(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_dec(x_2);
x_6 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_5);
lean_dec(x_5);
x_7 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__7;
x_8 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_10 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = l_Std_fmt___at_Lean_Level_PP_Result_format___spec__1(x_3);
x_12 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
x_13 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_7);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15;
lean_dec(x_3);
x_14 = lean_ctor_get(x_2, 1);
lean_inc(x_14);
lean_dec(x_2);
x_15 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_14);
lean_dec(x_14);
return x_15;
}
}
}
lean_object* l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_1, x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Elab_TermInfo_runMetaM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_1, 0);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = l_Lean_Elab_ContextInfo_runMetaM___rarg(x_2, x_5, x_3, x_4);
@ -3174,24 +3274,6 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string(" @ ");
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_TermInfo_format___lambda__1___closed__5;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_TermInfo_format___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -3245,12 +3327,14 @@ lean_ctor_set(x_49, 1, x_48);
x_50 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_50, 0, x_49);
lean_ctor_set(x_50, 1, x_45);
x_51 = l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
x_51 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_52 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
x_53 = lean_ctor_get(x_2, 3);
x_54 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_3, x_53);
x_53 = lean_ctor_get(x_2, 0);
lean_inc(x_53);
lean_dec(x_2);
x_54 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_3, x_53);
x_55 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_55, 0, x_52);
lean_ctor_set(x_55, 1, x_54);
@ -3279,12 +3363,14 @@ lean_ctor_set(x_62, 1, x_61);
x_63 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_63, 0, x_62);
lean_ctor_set(x_63, 1, x_57);
x_64 = l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
x_64 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_65 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_65, 0, x_63);
lean_ctor_set(x_65, 1, x_64);
x_66 = lean_ctor_get(x_2, 3);
x_67 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_3, x_66);
x_66 = lean_ctor_get(x_2, 0);
lean_inc(x_66);
lean_dec(x_2);
x_67 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_3, x_66);
x_68 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_68, 0, x_65);
lean_ctor_set(x_68, 1, x_67);
@ -3352,8 +3438,10 @@ x_15 = l_Lean_Elab_TermInfo_format___lambda__1___closed__2;
x_16 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_16, 0, x_14);
lean_ctor_set(x_16, 1, x_15);
x_17 = lean_ctor_get(x_2, 3);
x_18 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_3, x_17);
x_17 = lean_ctor_get(x_2, 0);
lean_inc(x_17);
lean_dec(x_2);
x_18 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_3, x_17);
x_19 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_19, 0, x_16);
lean_ctor_set(x_19, 1, x_18);
@ -3379,8 +3467,10 @@ x_25 = l_Lean_Elab_TermInfo_format___lambda__1___closed__2;
x_26 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
x_27 = lean_ctor_get(x_2, 3);
x_28 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_3, x_27);
x_27 = lean_ctor_get(x_2, 0);
lean_inc(x_27);
lean_dec(x_2);
x_28 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_3, x_27);
x_29 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_29, 0, x_26);
lean_ctor_set(x_29, 1, x_28);
@ -3396,6 +3486,7 @@ return x_31;
else
{
uint8_t x_32;
lean_dec(x_2);
x_32 = !lean_is_exclusive(x_10);
if (x_32 == 0)
{
@ -3422,7 +3513,7 @@ lean_object* l_Lean_Elab_TermInfo_format(lean_object* x_1, lean_object* x_2, lea
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_2, 2);
x_4 = lean_ctor_get(x_2, 3);
lean_inc(x_4);
lean_inc(x_1);
lean_inc(x_2);
@ -3441,7 +3532,6 @@ _start:
lean_object* x_9;
x_9 = l_Lean_Elab_TermInfo_format___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8);
lean_dec(x_3);
lean_dec(x_2);
return x_9;
}
}
@ -3718,7 +3808,7 @@ lean_dec(x_34);
x_41 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
x_42 = l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
x_42 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_43 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
@ -3750,7 +3840,7 @@ x_53 = l_Lean_Elab_CompletionInfo_format___closed__2;
x_54 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_52);
x_55 = l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
x_55 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
@ -3815,7 +3905,7 @@ lean_object* l_Lean_Elab_CommandInfo_format(lean_object* x_1, lean_object* x_2,
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_4 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_2);
x_4 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_1, x_2);
x_5 = l_Lean_Elab_CommandInfo_format___closed__2;
x_6 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_6, 0, x_5);
@ -3835,7 +3925,6 @@ _start:
{
lean_object* x_4;
x_4 = l_Lean_Elab_CommandInfo_format(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
@ -3919,7 +4008,7 @@ lean_ctor_set(x_26, 1, x_25);
x_27 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_17);
x_28 = l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
x_28 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_29 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
@ -3966,7 +4055,7 @@ lean_ctor_set(x_44, 1, x_43);
x_45 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_34);
x_46 = l_Lean_Elab_TermInfo_format___lambda__1___closed__6;
x_46 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2;
x_47 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
@ -4573,7 +4662,7 @@ x_5 = lean_ctor_get(x_1, 1);
x_6 = lean_ctor_get(x_1, 3);
x_7 = lean_ctor_get(x_1, 4);
x_8 = lean_ctor_get(x_1, 5);
x_9 = lean_ctor_get(x_2, 0);
x_9 = lean_ctor_get(x_2, 1);
lean_inc(x_9);
lean_inc(x_8);
lean_inc(x_7);
@ -4601,7 +4690,7 @@ lean_ctor_set(x_12, 2, x_11);
lean_ctor_set(x_12, 3, x_6);
lean_ctor_set(x_12, 4, x_7);
lean_ctor_set(x_12, 5, x_8);
x_13 = lean_ctor_get(x_2, 1);
x_13 = lean_ctor_get(x_2, 2);
lean_inc(x_13);
x_14 = l_Lean_Elab_ContextInfo_ppGoals(x_10, x_13, x_3);
lean_dec(x_10);
@ -4623,12 +4712,13 @@ uint8_t x_19;
x_19 = !lean_is_exclusive(x_18);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37;
x_20 = lean_ctor_get(x_18, 0);
x_21 = lean_ctor_get(x_2, 2);
x_21 = lean_ctor_get(x_2, 0);
lean_inc(x_21);
lean_dec(x_2);
x_22 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_21);
lean_inc(x_21);
x_22 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_1, x_21);
x_23 = l_Lean_Elab_TacticInfo_format___closed__2;
x_24 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_24, 0, x_23);
@ -4637,126 +4727,133 @@ x_25 = l_Lean_Elab_ContextInfo_ppGoals___lambda__1___closed__2;
x_26 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
x_27 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__2(x_21);
x_28 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
x_29 = l_Lean_Elab_TacticInfo_format___closed__4;
x_30 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
x_27 = lean_ctor_get(x_21, 1);
lean_inc(x_27);
lean_dec(x_21);
x_28 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__2(x_27);
x_29 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_29, 0, x_26);
lean_ctor_set(x_29, 1, x_28);
x_30 = l_Lean_Elab_TacticInfo_format___closed__4;
x_31 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_15);
x_32 = l_Lean_Elab_TacticInfo_format___closed__6;
x_33 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
lean_ctor_set(x_31, 0, x_29);
lean_ctor_set(x_31, 1, x_30);
x_32 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_15);
x_33 = l_Lean_Elab_TacticInfo_format___closed__6;
x_34 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_20);
x_35 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__7;
x_36 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
lean_ctor_set(x_18, 0, x_36);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
x_35 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_20);
x_36 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__7;
x_37 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
lean_ctor_set(x_18, 0, x_37);
return x_18;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55;
x_37 = lean_ctor_get(x_18, 0);
x_38 = lean_ctor_get(x_18, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_18);
x_39 = lean_ctor_get(x_2, 2);
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57;
x_38 = lean_ctor_get(x_18, 0);
x_39 = lean_ctor_get(x_18, 1);
lean_inc(x_39);
lean_inc(x_38);
lean_dec(x_18);
x_40 = lean_ctor_get(x_2, 0);
lean_inc(x_40);
lean_dec(x_2);
x_40 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_39);
x_41 = l_Lean_Elab_TacticInfo_format___closed__2;
x_42 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_40);
x_43 = l_Lean_Elab_ContextInfo_ppGoals___lambda__1___closed__2;
x_44 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
x_45 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__2(x_39);
x_46 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_46, 0, x_44);
lean_ctor_set(x_46, 1, x_45);
x_47 = l_Lean_Elab_TacticInfo_format___closed__4;
lean_inc(x_40);
x_41 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo(x_1, x_40);
x_42 = l_Lean_Elab_TacticInfo_format___closed__2;
x_43 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_41);
x_44 = l_Lean_Elab_ContextInfo_ppGoals___lambda__1___closed__2;
x_45 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
x_46 = lean_ctor_get(x_40, 1);
lean_inc(x_46);
lean_dec(x_40);
x_47 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__2(x_46);
x_48 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_48, 0, x_46);
lean_ctor_set(x_48, 0, x_45);
lean_ctor_set(x_48, 1, x_47);
x_49 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_49, 0, x_48);
lean_ctor_set(x_49, 1, x_15);
x_50 = l_Lean_Elab_TacticInfo_format___closed__6;
x_49 = l_Lean_Elab_TacticInfo_format___closed__4;
x_50 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_50, 0, x_48);
lean_ctor_set(x_50, 1, x_49);
x_51 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
x_52 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_37);
x_53 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__7;
lean_ctor_set(x_51, 0, x_50);
lean_ctor_set(x_51, 1, x_15);
x_52 = l_Lean_Elab_TacticInfo_format___closed__6;
x_53 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_53, 0, x_51);
lean_ctor_set(x_53, 1, x_52);
x_54 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
x_55 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_55, 0, x_54);
lean_ctor_set(x_55, 1, x_38);
return x_55;
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_38);
x_55 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange_fmtPos___closed__7;
x_56 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
x_57 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_57, 0, x_56);
lean_ctor_set(x_57, 1, x_39);
return x_57;
}
}
else
{
uint8_t x_56;
uint8_t x_58;
lean_dec(x_15);
lean_dec(x_2);
x_56 = !lean_is_exclusive(x_18);
if (x_56 == 0)
x_58 = !lean_is_exclusive(x_18);
if (x_58 == 0)
{
return x_18;
}
else
{
lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_57 = lean_ctor_get(x_18, 0);
x_58 = lean_ctor_get(x_18, 1);
lean_inc(x_58);
lean_inc(x_57);
lean_object* x_59; lean_object* x_60; lean_object* x_61;
x_59 = lean_ctor_get(x_18, 0);
x_60 = lean_ctor_get(x_18, 1);
lean_inc(x_60);
lean_inc(x_59);
lean_dec(x_18);
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
return x_59;
x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_59);
lean_ctor_set(x_61, 1, x_60);
return x_61;
}
}
}
else
{
uint8_t x_60;
uint8_t x_62;
lean_dec(x_12);
lean_dec(x_2);
x_60 = !lean_is_exclusive(x_14);
if (x_60 == 0)
x_62 = !lean_is_exclusive(x_14);
if (x_62 == 0)
{
return x_14;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_61 = lean_ctor_get(x_14, 0);
x_62 = lean_ctor_get(x_14, 1);
lean_inc(x_62);
lean_inc(x_61);
lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_63 = lean_ctor_get(x_14, 0);
x_64 = lean_ctor_get(x_14, 1);
lean_inc(x_64);
lean_inc(x_63);
lean_dec(x_14);
x_63 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_63, 0, x_61);
lean_ctor_set(x_63, 1, x_62);
return x_63;
x_65 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_65, 0, x_63);
lean_ctor_set(x_65, 1, x_64);
return x_65;
}
}
}
@ -5071,7 +5168,6 @@ x_8 = lean_ctor_get(x_2, 0);
lean_inc(x_8);
lean_dec(x_2);
x_9 = l_Lean_Elab_CommandInfo_format(x_1, x_8, x_3);
lean_dec(x_8);
lean_dec(x_1);
return x_9;
}
@ -5106,6 +5202,57 @@ return x_15;
}
}
}
lean_object* l_Lean_Elab_Info_toElabInfo_x3f(lean_object* x_1) {
_start:
{
switch (lean_obj_tag(x_1)) {
case 0:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_2, 0);
lean_inc(x_3);
x_4 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_4, 0, x_3);
return x_4;
}
case 1:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_1, 0);
x_6 = lean_ctor_get(x_5, 0);
lean_inc(x_6);
x_7 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_7, 0, x_6);
return x_7;
}
case 2:
{
lean_object* x_8; lean_object* x_9;
x_8 = lean_ctor_get(x_1, 0);
lean_inc(x_8);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_8);
return x_9;
}
default:
{
lean_object* x_10;
x_10 = lean_box(0);
return x_10;
}
}
}
}
lean_object* l_Lean_Elab_Info_toElabInfo_x3f___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Elab_Info_toElabInfo_x3f(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Info_updateContext_x3f_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -6261,18 +6408,22 @@ return x_2;
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_8 = l_Lean_LocalContext_empty;
x_9 = lean_alloc_ctor(0, 4, 0);
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_1);
lean_ctor_set(x_9, 2, x_7);
lean_ctor_set(x_9, 3, x_2);
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l_Lean_Elab_pushInfoLeaf___rarg(x_3, x_4, x_10);
x_12 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_11, x_5);
return x_12;
x_10 = l_Lean_LocalContext_empty;
x_11 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
lean_ctor_set(x_11, 2, x_2);
lean_ctor_set(x_11, 3, x_7);
x_12 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_12, 0, x_11);
x_13 = l_Lean_Elab_pushInfoLeaf___rarg(x_3, x_4, x_12);
x_14 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_13, x_5);
return x_14;
}
}
lean_object* l_Lean_Elab_resolveGlobalConstNoOverloadWithInfo___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
@ -6360,8 +6511,8 @@ lean_closure_set(x_11, 1, x_1);
lean_closure_set(x_11, 2, x_9);
lean_closure_set(x_11, 3, x_4);
lean_closure_set(x_11, 4, x_5);
lean_closure_set(x_11, 5, x_8);
lean_closure_set(x_11, 6, x_6);
lean_closure_set(x_11, 5, x_6);
lean_closure_set(x_11, 6, x_8);
x_12 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_10, x_11);
return x_12;
}
@ -6411,21 +6562,25 @@ return x_6;
lean_object* l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_7 = l_Lean_LocalContext_empty;
x_8 = lean_alloc_ctor(0, 4, 0);
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_7 = lean_box(0);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_1);
lean_ctor_set(x_8, 2, x_6);
lean_ctor_set(x_8, 3, x_2);
x_9 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_9 = l_Lean_LocalContext_empty;
x_10 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
lean_ctor_set(x_10, 2, x_2);
lean_ctor_set(x_10, 3, x_6);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
lean_inc(x_3);
x_10 = l_Lean_Elab_pushInfoLeaf___rarg(x_3, x_4, x_9);
x_11 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__1___boxed), 2, 1);
lean_closure_set(x_11, 0, x_3);
x_12 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_10, x_11);
return x_12;
x_12 = l_Lean_Elab_pushInfoLeaf___rarg(x_3, x_4, x_11);
x_13 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__1___boxed), 2, 1);
lean_closure_set(x_13, 0, x_3);
x_14 = lean_apply_4(x_5, lean_box(0), lean_box(0), x_12, x_13);
return x_14;
}
}
lean_object* l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
@ -6503,11 +6658,11 @@ x_16 = l_Lean_mkConstWithLevelParams___rarg(x_1, x_3, x_4, x_13);
lean_inc(x_7);
lean_inc(x_2);
lean_inc(x_1);
lean_inc(x_5);
lean_inc(x_6);
lean_inc(x_5);
x_17 = lean_alloc_closure((void*)(l_List_forIn_loop___at_Lean_Elab_resolveGlobalConstWithInfos___spec__1___rarg___lambda__2), 6, 5);
lean_closure_set(x_17, 0, x_6);
lean_closure_set(x_17, 1, x_5);
lean_closure_set(x_17, 0, x_5);
lean_closure_set(x_17, 1, x_6);
lean_closure_set(x_17, 2, x_1);
lean_closure_set(x_17, 3, x_2);
lean_closure_set(x_17, 4, x_7);
@ -8031,7 +8186,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__4;
x_2 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__5;
x_3 = lean_unsigned_to_nat(304u);
x_3 = lean_unsigned_to_nat(322u);
x_4 = lean_unsigned_to_nat(2u);
x_5 = l_Lean_Elab_assignInfoHoleId___rarg___lambda__2___closed__3;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -8659,6 +8814,10 @@ l_Lean_Elab_instInhabitedContextInfo___closed__9 = _init_l_Lean_Elab_instInhabit
lean_mark_persistent(l_Lean_Elab_instInhabitedContextInfo___closed__9);
l_Lean_Elab_instInhabitedContextInfo = _init_l_Lean_Elab_instInhabitedContextInfo();
lean_mark_persistent(l_Lean_Elab_instInhabitedContextInfo);
l_Lean_Elab_instInhabitedElabInfo___closed__1 = _init_l_Lean_Elab_instInhabitedElabInfo___closed__1();
lean_mark_persistent(l_Lean_Elab_instInhabitedElabInfo___closed__1);
l_Lean_Elab_instInhabitedElabInfo = _init_l_Lean_Elab_instInhabitedElabInfo();
lean_mark_persistent(l_Lean_Elab_instInhabitedElabInfo);
l_Lean_Elab_instInhabitedTermInfo___closed__1 = _init_l_Lean_Elab_instInhabitedTermInfo___closed__1();
lean_mark_persistent(l_Lean_Elab_instInhabitedTermInfo___closed__1);
l_Lean_Elab_instInhabitedTermInfo___closed__2 = _init_l_Lean_Elab_instInhabitedTermInfo___closed__2();
@ -8762,6 +8921,10 @@ l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___closed__1 = _init_l
lean_mark_persistent(l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___closed__1);
l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___closed__2 = _init_l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___closed__2();
lean_mark_persistent(l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange___closed__2);
l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1 = _init_l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1();
lean_mark_persistent(l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__1);
l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2 = _init_l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2();
lean_mark_persistent(l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatElabInfo___closed__2);
l_Lean_Elab_TermInfo_format___lambda__1___closed__1 = _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Elab_TermInfo_format___lambda__1___closed__1);
l_Lean_Elab_TermInfo_format___lambda__1___closed__2 = _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__2();
@ -8770,10 +8933,6 @@ l_Lean_Elab_TermInfo_format___lambda__1___closed__3 = _init_l_Lean_Elab_TermInfo
lean_mark_persistent(l_Lean_Elab_TermInfo_format___lambda__1___closed__3);
l_Lean_Elab_TermInfo_format___lambda__1___closed__4 = _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__4();
lean_mark_persistent(l_Lean_Elab_TermInfo_format___lambda__1___closed__4);
l_Lean_Elab_TermInfo_format___lambda__1___closed__5 = _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__5();
lean_mark_persistent(l_Lean_Elab_TermInfo_format___lambda__1___closed__5);
l_Lean_Elab_TermInfo_format___lambda__1___closed__6 = _init_l_Lean_Elab_TermInfo_format___lambda__1___closed__6();
lean_mark_persistent(l_Lean_Elab_TermInfo_format___lambda__1___closed__6);
l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1___closed__1 = _init_l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1___closed__1();
lean_mark_persistent(l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1___closed__1);
l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1___closed__2 = _init_l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1___closed__2();

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -426,7 +426,7 @@ lean_object* l_Lean_Meta_forallBoundedTelescope___at_Lean_Meta_addPPExplicitToEx
lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_Structural_addSmartUnfoldingDefAux_visit___spec__5___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_getFixedPrefix___lambda__2(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_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadIndexDep_x3f_match__1(lean_object*);
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_6367_(lean_object*);
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_6385_(lean_object*);
static lean_object* l___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_elimRecursion___lambda__3___closed__3;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_PreDefinition_Structural_0__Lean_Elab_Structural_hasBadParamDep_x3f___spec__2(lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_ofSubarray___rarg(lean_object*);
@ -19839,7 +19839,7 @@ lean_dec(x_1);
return x_14;
}
}
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_6367_(lean_object* x_1) {
lean_object* l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_6385_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -20181,7 +20181,7 @@ l_Lean_Elab_Structural_structuralRecursion___closed__3 = _init_l_Lean_Elab_Struc
lean_mark_persistent(l_Lean_Elab_Structural_structuralRecursion___closed__3);
l_Lean_Elab_Structural_structuralRecursion___closed__4 = _init_l_Lean_Elab_Structural_structuralRecursion___closed__4();
lean_mark_persistent(l_Lean_Elab_Structural_structuralRecursion___closed__4);
res = l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_6367_(lean_io_mk_world());
res = l_Lean_Elab_Structural_initFn____x40_Lean_Elab_PreDefinition_Structural___hyg_6385_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));

View file

@ -82,6 +82,7 @@ lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_levelParamsToMessa
static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrint___closed__5;
lean_object* l_List_forM___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printId___spec__7(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_printIdCore___closed__2;
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__1;
extern lean_object* l_Lean_LocalContext_empty;
@ -192,7 +193,6 @@ lean_object* l_List_forIn_loop___at___private_Lean_Elab_Print_0__Lean_Elab_Comma
lean_object* l_Lean_Elab_Command_getRef(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_mkHeader___closed__10;
static lean_object* l___private_Lean_Elab_Print_0__Lean_Elab_Command_levelParamsToMessageData___closed__6;
lean_object* l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Command_elabPrintAxioms___closed__3;
lean_object* l_Lean_Elab_Command_elabPrintAxioms(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_TagDeclarationExtension_isTagged(lean_object*, lean_object*, lean_object*);
@ -2427,7 +2427,7 @@ x_10 = l___private_Lean_Elab_Print_0__Lean_Elab_Command_throwUnknownId___closed_
x_11 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__14(x_11, x_2, x_3, x_4);
x_12 = l_Lean_throwError___at_Lean_Elab_Command_elabCommand___spec__13(x_11, x_2, x_3, x_4);
return x_12;
}
}
@ -2582,56 +2582,60 @@ lean_inc(x_5);
x_11 = l_Lean_mkConstWithLevelParams___at___private_Lean_Elab_Print_0__Lean_Elab_Command_printId___spec__5(x_9, x_5, x_6, x_7);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_LocalContext_empty;
x_14 = lean_box(0);
lean_inc(x_1);
lean_inc(x_2);
x_15 = lean_alloc_ctor(0, 4, 0);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_2);
lean_ctor_set(x_15, 2, x_12);
lean_ctor_set(x_15, 3, x_1);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_15);
x_17 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Command_elabEnd___spec__3(x_16, x_5, x_6, x_13);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = lean_box(0);
lean_ctor_set(x_15, 1, x_1);
x_16 = l_Lean_LocalContext_empty;
lean_inc(x_2);
x_17 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
lean_ctor_set(x_17, 2, x_2);
lean_ctor_set(x_17, 3, x_12);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
x_19 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Command_elabEnd___spec__3(x_18, x_5, x_6, x_13);
x_20 = lean_ctor_get(x_19, 1);
lean_inc(x_20);
lean_dec(x_19);
x_21 = lean_box(0);
x_3 = x_10;
x_4 = x_19;
x_7 = x_18;
x_4 = x_21;
x_7 = x_20;
goto _start;
}
else
{
uint8_t x_21;
uint8_t x_23;
lean_dec(x_10);
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_21 = !lean_is_exclusive(x_11);
if (x_21 == 0)
x_23 = !lean_is_exclusive(x_11);
if (x_23 == 0)
{
return x_11;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_22 = lean_ctor_get(x_11, 0);
x_23 = lean_ctor_get(x_11, 1);
lean_inc(x_23);
lean_inc(x_22);
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_11, 0);
x_25 = lean_ctor_get(x_11, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_11);
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_22);
lean_ctor_set(x_24, 1, x_23);
return x_24;
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
}

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -45,6 +45,7 @@ extern lean_object* l_Lean_maxRecDepthErrorMessage;
lean_object* l_Lean_Meta_occursCheck(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances___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_Std_Range_forIn_loop___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__1(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_Lean_Elab_Tactic_evalTacticAux(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_SyntheticMVars_0__Lean_Elab_Term_synthesizePendingCoeInstMVar___lambda__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*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkMVar(lean_object*);
static lean_object* l_Lean_commitWhenSome_x3f___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__2___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__3___closed__9;
@ -58,7 +59,6 @@ lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUs
lean_object* l_List_append___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_commitWhenSome_x3f___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__2___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__3___closed__4;
lean_object* l_Lean_Elab_Tactic_evalTactic(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_commitWhenSome_x3f___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__2___at___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstance___spec__3___closed__2;
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_synthesizeUsingDefaultPrio(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_SyntheticMVars_0__Lean_Elab_Term_tryToSynthesizeUsingDefaultInstances(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -9422,7 +9422,8 @@ lean_inc(x_8);
lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
x_32 = l_Lean_Elab_Tactic_evalTactic(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_31);
x_32 = l_Lean_Elab_Tactic_evalTacticAux(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_31);
lean_dec(x_3);
x_12 = x_32;
goto block_21;
}
@ -9445,8 +9446,7 @@ lean_inc(x_7);
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_37 = l_Lean_Elab_Tactic_evalTactic(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_36);
x_37 = l_Lean_Elab_Tactic_evalTacticAux(x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_36);
if (lean_obj_tag(x_37) == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47;

File diff suppressed because it is too large Load diff

View file

@ -56,13 +56,13 @@ lean_object* l___regBuiltin_Lean_Elab_Tactic_evalDecide(lean_object*);
lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefine_x27(lean_object*);
lean_object* l_Lean_Elab_Tactic_elabTermEnsuringType_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_closeMainGoalUsing(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_Elab_Tactic_evalTacticAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalRefine___closed__3;
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___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_Tactic_elabTermForApply___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_elabTermForApply___closed__1;
lean_object* l___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_preprocessPropToDecide___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalDecide___boxed(lean_object*);
lean_object* l_Lean_Elab_Tactic_evalTactic(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_throwAbortTactic___at___private_Lean_Elab_Tactic_ElabTerm_0__Lean_Elab_Tactic_logUnassignedAndAbort___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalRename(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_Tactic_evalConstructor___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -3619,7 +3619,7 @@ if (x_15 == 0)
uint8_t x_16; lean_object* x_17;
x_16 = 2;
lean_ctor_set_uint8(x_14, 5, x_16);
x_17 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_17 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_17) == 0)
{
uint8_t x_18;
@ -3691,7 +3691,7 @@ lean_ctor_set_uint8(x_36, 7, x_32);
lean_ctor_set_uint8(x_36, 8, x_33);
lean_ctor_set_uint8(x_36, 9, x_34);
lean_ctor_set(x_6, 0, x_36);
x_37 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_37 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_37) == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
@ -3790,7 +3790,7 @@ lean_ctor_set(x_62, 0, x_61);
lean_ctor_set(x_62, 1, x_47);
lean_ctor_set(x_62, 2, x_48);
lean_ctor_set(x_62, 3, x_49);
x_63 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_62, x_7, x_8, x_9, x_10);
x_63 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_62, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_63) == 0)
{
lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67;
@ -3847,6 +3847,7 @@ _start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalWithReducible(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}
@ -3924,7 +3925,7 @@ if (x_15 == 0)
uint8_t x_16; lean_object* x_17;
x_16 = 3;
lean_ctor_set_uint8(x_14, 5, x_16);
x_17 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_17 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_17) == 0)
{
uint8_t x_18;
@ -3996,7 +3997,7 @@ lean_ctor_set_uint8(x_36, 7, x_32);
lean_ctor_set_uint8(x_36, 8, x_33);
lean_ctor_set_uint8(x_36, 9, x_34);
lean_ctor_set(x_6, 0, x_36);
x_37 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_37 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_37) == 0)
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
@ -4095,7 +4096,7 @@ lean_ctor_set(x_62, 0, x_61);
lean_ctor_set(x_62, 1, x_47);
lean_ctor_set(x_62, 2, x_48);
lean_ctor_set(x_62, 3, x_49);
x_63 = l_Lean_Elab_Tactic_evalTactic(x_12, x_2, x_3, x_4, x_5, x_62, x_7, x_8, x_9, x_10);
x_63 = l_Lean_Elab_Tactic_evalTacticAux(x_12, x_2, x_3, x_4, x_5, x_62, x_7, x_8, x_9, x_10);
if (lean_obj_tag(x_63) == 0)
{
lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67;
@ -4152,6 +4153,7 @@ _start:
{
lean_object* x_11;
x_11 = l_Lean_Elab_Tactic_evalWithReducibleAndInstances(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_2);
lean_dec(x_1);
return x_11;
}

View file

@ -56,6 +56,7 @@ lean_object* l_Lean_Elab_Tactic_evalInduction_checkTargets___boxed(lean_object*,
lean_object* l_Lean_Meta_whnfForall(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalAlt___lambda__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* l_Lean_throwError___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_elabTaggedTerm___spec__1(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_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, 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_Tactic_ElimApp_evalAlts_applyPreTac___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_checkAltNames___spec__3___closed__2;
@ -97,7 +98,6 @@ lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_
lean_object* lean_st_ref_get(lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___lambda__2___closed__4;
lean_object* l_Lean_Elab_Tactic_evalTactic(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_Tactic_ElimApp_setMotiveArg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg___closed__6;
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getAltVarNames(lean_object*);
@ -107,7 +107,6 @@ static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Ind
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___spec__1___lambda__1(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_local_ctx_find_from_user_name(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_ElimApp_setMotiveArg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_resolveGlobalConstNoOverload___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___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* l_Lean_Elab_Tactic_evalAlt(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_expr_instantiate1(lean_object*, lean_object*);
@ -240,6 +239,7 @@ lean_object* l_Lean_Elab_Tactic_ElimApp_mkElimApp_loop_match__1(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec__5___boxed(lean_object**);
static lean_object* l_Lean_Elab_Tactic_ElimApp_State_alts___default___closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Tactic_evalInduction_checkTargets___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__3(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___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___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*);
lean_object* l_Lean_Elab_Tactic_evalInduction_match__1(lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_ElimApp_getFType___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -295,6 +295,7 @@ lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_
lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
extern lean_object* l_Lean_instInhabitedSyntax;
lean_object* l_Lean_mkConstWithLevelParams___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___spec__7(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_Tactic_evalTactic___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_Meta_introNCore(lean_object*, lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_generalizeVars___lambda__1(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_ResolveName_resolveGlobalName(lean_object*, lean_object*, lean_object*, lean_object*);
@ -433,7 +434,6 @@ lean_object* l_Lean_throwError___at_Lean_Elab_Tactic_ElimApp_evalAlts_go___spec_
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___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_Elab_Tactic_ElimApp_Result_alts___default;
uint8_t l_Lean_NameSet_contains(lean_object*, lean_object*);
lean_object* l_Lean_addTrace___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___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* l___regBuiltin_Lean_Elab_Tactic_evalCases(lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_checkAltsOfOptInductionAlts___spec__1___lambda__1___closed__1;
lean_object* l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -853,7 +853,7 @@ x_14 = l_Lean_Elab_Tactic_setGoals(x_1, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_1
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
x_16 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic), 10, 1);
x_16 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalTactic___boxed), 10, 1);
lean_closure_set(x_16, 0, x_2);
x_17 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_withTacticInfoContext___rarg), 11, 2);
lean_closure_set(x_17, 0, x_3);
@ -4296,7 +4296,6 @@ lean_dec(x_7);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_17, 0, x_2);
@ -4313,6 +4312,7 @@ _start:
{
lean_object* x_12;
x_12 = l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_3);
lean_dec(x_1);
return x_12;
}
@ -4803,7 +4803,6 @@ lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
x_68 = l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(x_11, x_66, x_16, x_17, x_18, x_19, x_20, x_21, x_22, x_23, x_67);
if (lean_obj_tag(x_68) == 0)
{
@ -5217,7 +5216,6 @@ lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
x_140 = l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(x_11, x_138, x_16, x_17, x_18, x_19, x_20, x_21, x_22, x_23, x_139);
if (lean_obj_tag(x_140) == 0)
{
@ -5680,7 +5678,6 @@ lean_inc(x_20);
lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
x_220 = l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(x_11, x_218, x_16, x_17, x_18, x_19, x_20, x_21, x_22, x_23, x_219);
if (lean_obj_tag(x_220) == 0)
{
@ -6280,7 +6277,6 @@ lean_inc(x_19);
lean_inc(x_18);
lean_inc(x_17);
lean_inc(x_16);
lean_inc(x_15);
x_60 = l_Lean_Elab_Tactic_ElimApp_evalAlts_applyPreTac(x_6, x_58, x_15, x_16, x_17, x_18, x_19, x_20, x_21, x_22, x_59);
if (lean_obj_tag(x_60) == 0)
{
@ -9053,7 +9049,7 @@ x_26 = lean_ctor_get(x_17, 1);
lean_inc(x_26);
lean_dec(x_17);
x_27 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__3;
x_28 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_26);
x_28 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__2(x_27, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_26);
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
x_30 = lean_unbox(x_29);
@ -9088,7 +9084,7 @@ lean_ctor_set(x_39, 1, x_37);
x_40 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = l_Lean_addTrace___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__2(x_27, x_40, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_36);
x_41 = l_Lean_addTrace___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__3(x_27, x_40, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_36);
x_42 = lean_ctor_get(x_41, 1);
lean_inc(x_42);
lean_dec(x_41);
@ -9162,7 +9158,7 @@ x_66 = lean_ctor_get(x_57, 1);
lean_inc(x_66);
lean_dec(x_57);
x_67 = l___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getUserGeneralizingFVarIds___closed__3;
x_68 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__1(x_67, x_2, x_3, x_4, x_5, x_6, x_7, x_56, x_9, x_66);
x_68 = l___private_Lean_Util_Trace_0__Lean_checkTraceOptionM___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__2(x_67, x_2, x_3, x_4, x_5, x_6, x_7, x_56, x_9, x_66);
x_69 = lean_ctor_get(x_68, 0);
lean_inc(x_69);
x_70 = lean_unbox(x_69);
@ -9197,7 +9193,7 @@ lean_ctor_set(x_79, 1, x_77);
x_80 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_80, 0, x_79);
lean_ctor_set(x_80, 1, x_78);
x_81 = l_Lean_addTrace___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__2(x_67, x_80, x_2, x_3, x_4, x_5, x_6, x_7, x_56, x_9, x_76);
x_81 = l_Lean_addTrace___at_Lean_Elab_Tactic_expandTacticMacroFns_loop___spec__3(x_67, x_80, x_2, x_3, x_4, x_5, x_6, x_7, x_56, x_9, x_76);
x_82 = lean_ctor_get(x_81, 1);
lean_inc(x_82);
lean_dec(x_81);
@ -11582,94 +11578,98 @@ lean_inc(x_14);
x_27 = l_Lean_mkConstWithLevelParams___at___private_Lean_Elab_Tactic_Induction_0__Lean_Elab_Tactic_getElimNameInfo___spec__7(x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_26);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34;
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l_Lean_LocalContext_empty;
x_31 = lean_alloc_ctor(0, 4, 0);
x_30 = lean_box(0);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_3);
lean_ctor_set(x_31, 2, x_28);
lean_ctor_set(x_31, 3, x_1);
x_32 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_32, 0, x_31);
x_33 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3(x_32, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_29);
lean_ctor_set(x_31, 1, x_1);
x_32 = l_Lean_LocalContext_empty;
x_33 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
lean_ctor_set(x_33, 2, x_3);
lean_ctor_set(x_33, 3, x_28);
x_34 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_34, 0, x_33);
x_35 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3(x_34, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_29);
lean_dec(x_10);
x_34 = !lean_is_exclusive(x_33);
if (x_34 == 0)
x_36 = !lean_is_exclusive(x_35);
if (x_36 == 0)
{
lean_object* x_35;
x_35 = lean_ctor_get(x_33, 0);
lean_object* x_37;
x_37 = lean_ctor_get(x_35, 0);
lean_dec(x_37);
lean_ctor_set(x_35, 0, x_14);
return x_35;
}
else
{
lean_object* x_38; lean_object* x_39;
x_38 = lean_ctor_get(x_35, 1);
lean_inc(x_38);
lean_dec(x_35);
lean_ctor_set(x_33, 0, x_14);
return x_33;
}
else
{
lean_object* x_36; lean_object* x_37;
x_36 = lean_ctor_get(x_33, 1);
lean_inc(x_36);
lean_dec(x_33);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_14);
lean_ctor_set(x_37, 1, x_36);
return x_37;
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_14);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
else
{
uint8_t x_38;
uint8_t x_40;
lean_dec(x_14);
lean_dec(x_10);
lean_dec(x_3);
lean_dec(x_1);
x_38 = !lean_is_exclusive(x_27);
if (x_38 == 0)
x_40 = !lean_is_exclusive(x_27);
if (x_40 == 0)
{
return x_27;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_27, 0);
x_40 = lean_ctor_get(x_27, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_27, 0);
x_42 = lean_ctor_get(x_27, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_27);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
}
else
{
uint8_t x_42;
uint8_t x_44;
lean_dec(x_10);
lean_dec(x_3);
lean_dec(x_1);
x_42 = !lean_is_exclusive(x_13);
if (x_42 == 0)
x_44 = !lean_is_exclusive(x_13);
if (x_44 == 0)
{
return x_13;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_13, 0);
x_44 = lean_ctor_get(x_13, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_13, 0);
x_46 = lean_ctor_get(x_13, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_13);
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}

File diff suppressed because it is too large Load diff

View file

@ -2540,94 +2540,98 @@ lean_inc(x_14);
x_27 = l_Lean_mkConstWithLevelParams___at___private_Lean_Elab_Tactic_Simp_0__Lean_Elab_Tactic_elabSimpLemmas___spec__7(x_14, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_26);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; uint8_t x_34;
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l_Lean_LocalContext_empty;
x_31 = lean_alloc_ctor(0, 4, 0);
x_30 = lean_box(0);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_3);
lean_ctor_set(x_31, 2, x_28);
lean_ctor_set(x_31, 3, x_1);
x_32 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_32, 0, x_31);
x_33 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3(x_32, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_29);
lean_ctor_set(x_31, 1, x_1);
x_32 = l_Lean_LocalContext_empty;
x_33 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
lean_ctor_set(x_33, 2, x_3);
lean_ctor_set(x_33, 3, x_28);
x_34 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_34, 0, x_33);
x_35 = l_Lean_Elab_pushInfoLeaf___at_Lean_Elab_Tactic_elabSetOption___spec__3(x_34, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_29);
lean_dec(x_10);
x_34 = !lean_is_exclusive(x_33);
if (x_34 == 0)
x_36 = !lean_is_exclusive(x_35);
if (x_36 == 0)
{
lean_object* x_35;
x_35 = lean_ctor_get(x_33, 0);
lean_object* x_37;
x_37 = lean_ctor_get(x_35, 0);
lean_dec(x_37);
lean_ctor_set(x_35, 0, x_14);
return x_35;
}
else
{
lean_object* x_38; lean_object* x_39;
x_38 = lean_ctor_get(x_35, 1);
lean_inc(x_38);
lean_dec(x_35);
lean_ctor_set(x_33, 0, x_14);
return x_33;
}
else
{
lean_object* x_36; lean_object* x_37;
x_36 = lean_ctor_get(x_33, 1);
lean_inc(x_36);
lean_dec(x_33);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_14);
lean_ctor_set(x_37, 1, x_36);
return x_37;
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_14);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
else
{
uint8_t x_38;
uint8_t x_40;
lean_dec(x_14);
lean_dec(x_10);
lean_dec(x_3);
lean_dec(x_1);
x_38 = !lean_is_exclusive(x_27);
if (x_38 == 0)
x_40 = !lean_is_exclusive(x_27);
if (x_40 == 0)
{
return x_27;
}
else
{
lean_object* x_39; lean_object* x_40; lean_object* x_41;
x_39 = lean_ctor_get(x_27, 0);
x_40 = lean_ctor_get(x_27, 1);
lean_inc(x_40);
lean_inc(x_39);
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_27, 0);
x_42 = lean_ctor_get(x_27, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_27);
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
return x_41;
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
}
else
{
uint8_t x_42;
uint8_t x_44;
lean_dec(x_10);
lean_dec(x_3);
lean_dec(x_1);
x_42 = !lean_is_exclusive(x_13);
if (x_42 == 0)
x_44 = !lean_is_exclusive(x_13);
if (x_44 == 0)
{
return x_13;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45;
x_43 = lean_ctor_get(x_13, 0);
x_44 = lean_ctor_get(x_13, 1);
lean_inc(x_44);
lean_inc(x_43);
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_13, 0);
x_46 = lean_ctor_get(x_13, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_13);
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -12187,23 +12187,26 @@ _start:
{
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_11; uint8_t x_12;
x_11 = lean_ctor_get(x_1, 3);
lean_object* x_11; lean_object* x_12; uint8_t x_13;
x_11 = lean_ctor_get(x_1, 0);
lean_inc(x_11);
lean_dec(x_1);
x_12 = l_Lean_Syntax_isIdent(x_11);
if (x_12 == 0)
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
lean_inc(x_11);
x_13 = l_Lean_Syntax_getKind(x_11);
x_14 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCompletion___lambda__2___closed__8;
x_15 = lean_name_eq(x_13, x_14);
lean_dec(x_13);
if (x_15 == 0)
{
lean_object* x_16; lean_object* x_17;
x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = l_Lean_Syntax_isIdent(x_12);
if (x_13 == 0)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16;
lean_inc(x_12);
x_14 = l_Lean_Syntax_getKind(x_12);
x_15 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCompletion___lambda__2___closed__8;
x_16 = lean_name_eq(x_14, x_15);
lean_dec(x_14);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
lean_dec(x_12);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -12211,23 +12214,23 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_16 = lean_box(0);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_10);
return x_17;
x_17 = lean_box(0);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_10);
return x_18;
}
else
{
lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_18 = lean_unsigned_to_nat(0u);
x_19 = l_Lean_Syntax_getArg(x_11, x_18);
lean_dec(x_11);
x_20 = l_Lean_Syntax_isIdent(x_19);
if (x_20 == 0)
lean_object* x_19; lean_object* x_20; uint8_t x_21;
x_19 = lean_unsigned_to_nat(0u);
x_20 = l_Lean_Syntax_getArg(x_12, x_19);
lean_dec(x_12);
x_21 = l_Lean_Syntax_isIdent(x_20);
if (x_21 == 0)
{
lean_object* x_21; lean_object* x_22;
lean_dec(x_19);
lean_object* x_22; lean_object* x_23;
lean_dec(x_20);
lean_dec(x_9);
lean_dec(x_8);
lean_dec(x_7);
@ -12235,56 +12238,56 @@ lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
x_21 = lean_box(0);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_10);
return x_22;
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_10);
return x_23;
}
else
{
lean_object* x_23; uint8_t x_24; lean_object* x_25;
x_23 = l_Lean_Syntax_getId(x_19);
lean_dec(x_19);
x_24 = 1;
x_25 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore(x_2, x_23, x_24, x_3, x_5, x_6, x_7, x_8, x_9, x_10);
return x_25;
lean_object* x_24; uint8_t x_25; lean_object* x_26;
x_24 = l_Lean_Syntax_getId(x_20);
lean_dec(x_20);
x_25 = 1;
x_26 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore(x_2, x_24, x_25, x_3, x_5, x_6, x_7, x_8, x_9, x_10);
return x_26;
}
}
}
else
{
lean_object* x_26; uint8_t x_27; lean_object* x_28;
x_26 = l_Lean_Syntax_getId(x_11);
lean_dec(x_11);
x_27 = 0;
x_28 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore(x_2, x_26, x_27, x_3, x_5, x_6, x_7, x_8, x_9, x_10);
return x_28;
lean_object* x_27; uint8_t x_28; lean_object* x_29;
x_27 = l_Lean_Syntax_getId(x_12);
lean_dec(x_12);
x_28 = 0;
x_29 = l___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore(x_2, x_27, x_28, x_3, x_5, x_6, x_7, x_8, x_9, x_10);
return x_29;
}
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_dec(x_2);
lean_dec(x_1);
x_29 = lean_st_ref_get(x_9, x_10);
x_30 = lean_ctor_get(x_29, 0);
lean_inc(x_30);
x_31 = lean_ctor_get(x_29, 1);
x_30 = lean_st_ref_get(x_9, x_10);
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
lean_dec(x_29);
x_32 = lean_ctor_get(x_30, 0);
x_32 = lean_ctor_get(x_30, 1);
lean_inc(x_32);
lean_dec(x_30);
x_33 = lean_ctor_get(x_32, 1);
x_33 = lean_ctor_get(x_31, 0);
lean_inc(x_33);
lean_dec(x_32);
x_34 = lean_alloc_closure((void*)(l___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCompletion___lambda__1___boxed), 10, 2);
lean_closure_set(x_34, 0, x_4);
lean_closure_set(x_34, 1, x_3);
x_35 = l_Lean_SMap_forM___at___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore___spec__2(x_33, x_34, x_5, x_6, x_7, x_8, x_9, x_31);
lean_dec(x_31);
x_34 = lean_ctor_get(x_33, 1);
lean_inc(x_34);
lean_dec(x_33);
return x_35;
x_35 = lean_alloc_closure((void*)(l___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCompletion___lambda__1___boxed), 10, 2);
lean_closure_set(x_35, 0, x_4);
lean_closure_set(x_35, 1, x_3);
x_36 = l_Lean_SMap_forM___at___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore___spec__2(x_34, x_35, x_5, x_6, x_7, x_8, x_9, x_32);
lean_dec(x_34);
return x_36;
}
}
}
@ -12484,7 +12487,7 @@ lean_object* l___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCom
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_5 = lean_ctor_get(x_2, 0);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_inc(x_1);
lean_inc(x_2);
@ -12492,7 +12495,7 @@ x_6 = lean_alloc_closure((void*)(l___private_Lean_Server_Completion_0__Lean_Serv
lean_closure_set(x_6, 0, x_2);
lean_closure_set(x_6, 1, x_1);
lean_closure_set(x_6, 2, x_3);
x_7 = lean_ctor_get(x_2, 2);
x_7 = lean_ctor_get(x_2, 3);
lean_inc(x_7);
lean_dec(x_2);
x_8 = lean_alloc_closure((void*)(l___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCompletion___lambda__3___boxed), 7, 1);

File diff suppressed because it is too large Load diff

File diff suppressed because it is too large Load diff

View file

@ -24,7 +24,6 @@ lean_object* lean_io_error_to_string(lean_object*);
lean_object* l_Lean_Server_Requests_RequestError_methodNotFound(lean_object*);
lean_object* l_Lean_Server_Requests_RequestM_bindTask(lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_Requests_0__Lean_Server_Requests_parseParams___rarg___closed__2;
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__3;
lean_object* l_Std_PersistentHashMap_insertAux_traverse___at_Lean_Server_Requests_registerLspRequestHandler___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_RequestError_toLspResponseError(lean_object*, lean_object*);
size_t l_USize_sub(size_t, size_t);
@ -39,16 +38,15 @@ static lean_object* l_IO_AsyncList_waitFind_x3f___at_Lean_Server_Requests_Reques
lean_object* l_Std_PersistentHashMap_getCollisionNodeSize___rarg(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_routeLspRequest_match__1(lean_object*);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__5;
size_t l_USize_shiftRight(size_t, size_t);
lean_object* l_Lean_Server_Requests_handleLspRequest(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__3;
lean_object* l_Lean_Server_Requests_RequestM_bindTask___rarg___lambda__1(lean_object*);
uint8_t l_Std_PersistentHashMap_containsAtAux___at_Lean_Server_Requests_registerLspRequestHandler___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_io_map_task(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_requestHandlers;
lean_object* l_Lean_Server_Requests_RequestError_methodNotFound___boxed(lean_object*);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__1;
lean_object* lean_io_bind_task(lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_UInt64_toUSize(uint64_t);
static lean_object* l_Lean_Server_Requests_RequestError_methodNotFound___closed__2;
@ -61,6 +59,7 @@ lean_object* l_Lean_Json_compress(lean_object*);
lean_object* lean_st_ref_take(lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_RequestError_fileChanged___closed__1;
static lean_object* l_Lean_Server_Requests_registerLspRequestHandler___lambda__4___closed__1;
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__4;
lean_object* l_Lean_Server_Requests_RequestError_instCoeErrorRequestError(lean_object*);
lean_object* l_Lean_Server_Requests_RequestM_mapTask(lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_RequestM_bindTask___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
@ -74,7 +73,7 @@ lean_object* lean_array_fset(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_handleLspRequest___closed__1;
lean_object* l_Lean_Server_Requests_handleLspRequest___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_contains___at_Lean_Server_Requests_registerLspRequestHandler___spec__5___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492_(lean_object*);
lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498_(lean_object*);
lean_object* lean_task_map(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_registerLspRequestHandler___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_registerLspRequestHandler___lambda__4___closed__2;
@ -93,12 +92,13 @@ size_t l_USize_mul(size_t, size_t);
lean_object* l___private_Lean_Server_AsyncList_0__IO_AsyncList_coeErr___at_Lean_Server_Requests_RequestM_withWaitFindSnap___spec__2___lambda__1(lean_object*);
lean_object* l_Lean_Server_Requests_routeLspRequest(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_registerLspRequestHandler(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__2;
extern lean_object* l_Task_Priority_default;
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__1;
lean_object* l_Std_PersistentHashMap_containsAtAux___at_Lean_Server_Requests_registerLspRequestHandler___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_String_decEq___boxed(lean_object*, lean_object*);
static lean_object* l_Std_PersistentHashMap_insertAux___at_Lean_Server_Requests_registerLspRequestHandler___spec__2___closed__3;
size_t l_USize_land(size_t, size_t);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__2;
lean_object* l_Lean_Server_Requests_registerLspRequestHandler___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_registerLspRequestHandler___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Server_Requests_0__Lean_Server_Requests_parseParams(lean_object*);
@ -113,7 +113,6 @@ static lean_object* l_Lean_Server_Requests_registerLspRequestHandler___closed__1
lean_object* l_Lean_Server_Requests_registerLspRequestHandler___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Server_AsyncList_0__IO_AsyncList_coeErr___at_Lean_Server_Requests_RequestM_withWaitFindSnap___spec__2___closed__1;
lean_object* l_Std_PersistentHashMap_findAtAux___at___private_Lean_Server_Requests_0__Lean_Server_Requests_lookupLspRequestHandler___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__4;
lean_object* l_Lean_Server_Requests_RequestM_asTask_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_find_x3f___at___private_Lean_Server_Requests_0__Lean_Server_Requests_lookupLspRequestHandler___spec__1(lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_insertAtCollisionNodeAux___at_Lean_Server_Requests_registerLspRequestHandler___spec__4(lean_object*, lean_object*, lean_object*, lean_object*);
@ -133,6 +132,7 @@ lean_object* l_IO_mkRef___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_RequestM_mapTask___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_AsyncList_waitFind_x3f___at_Lean_Server_Requests_RequestM_withWaitFindSnap___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Requests_RequestM_withWaitFindSnap___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__5;
lean_object* lean_usize_to_nat(size_t);
lean_object* l_Lean_Server_Requests_RequestM_withWaitFindSnap_match__1(lean_object*);
lean_object* l___private_Lean_Server_Requests_0__Lean_Server_Requests_lookupLspRequestHandler___boxed(lean_object*, lean_object*);
@ -1298,7 +1298,7 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Server_Requests_RequestM_withWaitFindSna
return x_2;
}
}
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__1() {
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__1() {
_start:
{
lean_object* x_1;
@ -1306,17 +1306,17 @@ x_1 = lean_alloc_closure((void*)(l_String_decEq___boxed), 2, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__2() {
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__1;
x_1 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__1;
x_2 = lean_alloc_closure((void*)(l_instBEq___rarg), 3, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__3() {
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__3() {
_start:
{
lean_object* x_1;
@ -1324,21 +1324,21 @@ x_1 = l_Std_PersistentHashMap_mkEmptyEntriesArray(lean_box(0), lean_box(0));
return x_1;
}
}
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__4() {
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__3;
x_1 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__3;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__5() {
static lean_object* _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__4;
x_1 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__4;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
@ -1346,11 +1346,11 @@ lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492_(lean_object* x_1) {
lean_object* l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__5;
x_2 = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__5;
x_3 = l_IO_mkRef___rarg(x_2, x_1);
return x_3;
}
@ -3167,17 +3167,17 @@ l_IO_AsyncList_waitFind_x3f___at_Lean_Server_Requests_RequestM_withWaitFindSnap_
lean_mark_persistent(l_IO_AsyncList_waitFind_x3f___at_Lean_Server_Requests_RequestM_withWaitFindSnap___spec__1___closed__2);
l_Lean_Server_Requests_RequestM_withWaitFindSnap___rarg___lambda__1___closed__1 = _init_l_Lean_Server_Requests_RequestM_withWaitFindSnap___rarg___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Server_Requests_RequestM_withWaitFindSnap___rarg___lambda__1___closed__1);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__1 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__1();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__1);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__2 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__2();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__2);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__3 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__3();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__3);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__4 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__4();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__4);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__5 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__5();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492____closed__5);
res = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_492_(lean_io_mk_world());
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__1 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__1();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__1);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__2 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__2();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__2);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__3 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__3();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__3);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__4 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__4();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__4);
l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__5 = _init_l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__5();
lean_mark_persistent(l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498____closed__5);
res = l_Lean_Server_Requests_initFn____x40_Lean_Server_Requests___hyg_498_(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
l_Lean_Server_Requests_requestHandlers = lean_io_result_get_value(res);
lean_mark_persistent(l_Lean_Server_Requests_requestHandlers);

View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Server.Utils
// Imports: Init Lean.Data.Position Lean.Data.Lsp Init.System.FilePath
// Imports: Init Lean.Data.Position Lean.Data.Lsp Lean.Server.InfoUtils Init.System.FilePath
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -28,6 +28,7 @@ lean_object* l_Lean_Server_publishProgressAtPos___boxed(lean_object*, lean_objec
lean_object* l_Lean_Server_publishProgress(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_foldDocumentChanges_match__1(lean_object*);
extern uint8_t l_System_FilePath_isCaseInsensitive;
lean_object* l_String_Range_toLspRange___boxed(lean_object*, lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_IO_FS_Stream_withPrefix___elambda__4(lean_object*, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_publishMessages___spec__3(lean_object*, size_t, size_t, lean_object*, lean_object*);
@ -69,6 +70,7 @@ lean_object* l_Lean_Server_maybeTee___boxed(lean_object*, lean_object*, lean_obj
static lean_object* l_Lean_Server_maybeTee___closed__1;
lean_object* l_Lean_Server_foldDocumentChanges_match__2(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_publishMessages___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_String_Range_toLspRange(lean_object*, lean_object*);
static lean_object* l_Lean_Server_toFileUri___closed__2;
static lean_object* l_Lean_Server_publishProgressAtPos___closed__1;
lean_object* l_IO_FS_Stream_chainLeft(lean_object*, lean_object*, uint8_t);
@ -1825,7 +1827,7 @@ _start:
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Server_foldDocumentChanges___closed__2;
x_2 = l_Lean_Server_foldDocumentChanges___closed__3;
x_3 = lean_unsigned_to_nat(110u);
x_3 = lean_unsigned_to_nat(111u);
x_4 = lean_unsigned_to_nat(26u);
x_5 = l_Lean_Server_foldDocumentChanges___closed__4;
x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);
@ -3087,9 +3089,34 @@ x_2 = lean_alloc_closure((void*)(l_List_takeWhile___rarg), 2, 0);
return x_2;
}
}
lean_object* l_String_Range_toLspRange(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_ctor_get(x_2, 0);
x_4 = l_Lean_FileMap_utf8PosToLspPos(x_1, x_3);
x_5 = lean_ctor_get(x_2, 1);
x_6 = l_Lean_FileMap_utf8PosToLspPos(x_1, x_5);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_6);
return x_7;
}
}
lean_object* l_String_Range_toLspRange___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_String_Range_toLspRange(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Data_Position(lean_object*);
lean_object* initialize_Lean_Data_Lsp(lean_object*);
lean_object* initialize_Lean_Server_InfoUtils(lean_object*);
lean_object* initialize_Init_System_FilePath(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Server_Utils(lean_object* w) {
@ -3105,6 +3132,9 @@ lean_dec_ref(res);
res = initialize_Lean_Data_Lsp(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Server_InfoUtils(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_System_FilePath(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

View file

@ -83,6 +83,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Std_RBMap_max_x21___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBMap_instReprRBMap___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Std_RBMap_find_x21___rarg___closed__3;
lean_object* l_Std_RBMap_max_x21_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_balRight_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_balance2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_revFold___rarg(lean_object*, lean_object*, lean_object*);
@ -278,6 +279,7 @@ lean_object* l_Std_RBMap_foldM(lean_object*, lean_object*, lean_object*, lean_ob
lean_object* l_Std_RBNode_fold___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBMap_isEmpty(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_lowerBound_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBMap_max_x21_match__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_fold(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBMap_max___rarg(lean_object*);
lean_object* l_Std_RBNode_foldM___at_Std_RBMap_forM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -21876,6 +21878,37 @@ lean_dec(x_3);
return x_4;
}
}
lean_object* l_Std_RBMap_max_x21_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_1) == 0)
{
lean_object* x_4; lean_object* x_5;
lean_dec(x_2);
x_4 = lean_box(0);
x_5 = lean_apply_1(x_3, x_4);
return x_5;
}
else
{
lean_object* x_6; lean_object* x_7;
lean_dec(x_3);
x_6 = lean_ctor_get(x_1, 0);
lean_inc(x_6);
lean_dec(x_1);
x_7 = lean_apply_1(x_2, x_6);
return x_7;
}
}
}
lean_object* l_Std_RBMap_max_x21_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Std_RBMap_max_x21_match__1___rarg), 3, 0);
return x_4;
}
}
static lean_object* _init_l_Std_RBMap_max_x21___rarg___closed__1() {
_start:
{