max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-01-19 13:25:26 -08:00
parent 445420315e
commit 79bb2f2d5a
25 changed files with 17802 additions and 6872 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/Lean/Data/Lsp/Capabilities.lean generated
View file

@ -31,6 +31,9 @@ structure ServerCapabilities where
textDocumentSync? : Option TextDocumentSyncOptions := none
hoverProvider : Bool := false
documentSymbolProvider : Bool := false
definitionProvider : Bool := false
declarationProvider : Bool := false
typeDefinitionProvider : Bool := false
deriving ToJson, FromJson
end Lsp

26
stage0/src/Lean/Data/Lsp/LanguageFeatures.lean generated
View file

@ -28,6 +28,32 @@ instance : FromJson HoverParams := ⟨fun j => do
instance : ToJson HoverParams :=
⟨fun o => toJson o.toTextDocumentPositionParams⟩
structure DeclarationParams extends TextDocumentPositionParams
instance : FromJson DeclarationParams := ⟨fun j => do
let tdpp ← @fromJson? TextDocumentPositionParams _ j
pure ⟨tdpp⟩⟩
instance : ToJson DeclarationParams :=
⟨fun o => toJson o.toTextDocumentPositionParams⟩
structure DefinitionParams extends TextDocumentPositionParams
instance : FromJson DefinitionParams := ⟨fun j => do
let tdpp ← @fromJson? TextDocumentPositionParams _ j
pure ⟨tdpp⟩⟩
instance : ToJson DefinitionParams :=
⟨fun o => toJson o.toTextDocumentPositionParams⟩
structure TypeDefinitionParams extends TextDocumentPositionParams
instance : FromJson TypeDefinitionParams := ⟨fun j => do
let tdpp ← @fromJson? TextDocumentPositionParams _ j
pure ⟨tdpp⟩⟩
instance : ToJson TypeDefinitionParams :=
⟨fun o => toJson o.toTextDocumentPositionParams⟩
structure DocumentSymbolParams where
textDocument : TextDocumentIdentifier

11
stage0/src/Lean/DeclarationRange.lean generated
View file

@ -9,8 +9,15 @@ import Lean.AuxRecursor
namespace Lean
structure DeclarationRange where
pos : Position
endPos : Position
pos : Position
/-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
file, which is IO-heavy. -/
charUtf16 : Nat
endPos : Position
/-- See `charUtf16`. -/
endCharUtf16 : Nat
deriving Inhabited, DecidableEq, Repr
structure DeclarationRanges where

13
stage0/src/Lean/Elab/DeclarationRange.lean generated
View file

@ -5,14 +5,21 @@ Authors: Leonardo de Moura
-/
import Lean.DeclarationRange
import Lean.Elab.Log
import Lean.Data.Lsp.Utf16
namespace Lean.Elab
def getDeclarationRange [Monad m] [MonadFileMap m] (stx : Syntax) : m DeclarationRange := do
let pos := stx.getPos.getD 0
let endPos := stx.getTailPos.getD pos
let fileMap ← getFileMap
return { pos := fileMap.toPosition pos, endPos := fileMap.toPosition endPos }
let pos := stx.getPos.getD 0
let endPos := stx.getTailPos.getD pos |> fileMap.toPosition
let pos := pos |> fileMap.toPosition
return {
pos := pos
charUtf16 := fileMap.leanPosToLspPos pos |>.character
endPos := endPos
endCharUtf16 := fileMap.leanPosToLspPos endPos |>.character
}
/--
For most builtin declarations, the selection range is just its name, which is stored in the second position.

9
stage0/src/Lean/Server/FileSource.lean generated
View file

@ -43,6 +43,15 @@ instance DidCloseTextDocumentParams.hasFileSource : FileSource DidCloseTextDocum
instance HoverParams.hasFileSource : FileSource HoverParams :=
⟨fun h => fileSource h.toTextDocumentPositionParams⟩
instance DeclarationParams.hasFileSource : FileSource DeclarationParams :=
⟨fun h => fileSource h.toTextDocumentPositionParams⟩
instance DefinitionParams.hasFileSource : FileSource DefinitionParams :=
⟨fun h => fileSource h.toTextDocumentPositionParams⟩
instance TypeDefinitionParams.hasFileSource : FileSource TypeDefinitionParams :=
⟨fun h => fileSource h.toTextDocumentPositionParams⟩
instance WaitForDiagnosticsParam.hasFileSource : FileSource WaitForDiagnosticsParam :=
⟨fun p => p.uri⟩

253
stage0/src/Lean/Server/FileWorker.lean generated
View file

@ -9,6 +9,7 @@ import Std.Data.RBMap
import Lean.Environment
import Lean.PrettyPrinter
import Lean.DeclarationRange
import Lean.Data.Lsp
import Lean.Data.Json.FromToJson
@ -46,6 +47,8 @@ open Lsp
open IO
open Snapshots
open Lean.Parser.Command
open Std (RBMap RBMap.empty)
open JsonRpc
section Utils
private def logSnapContent (s : Snapshot) (text : FileMap) : IO Unit :=
@ -88,36 +91,18 @@ section Utils
deriving Inhabited
end Utils
open IO
open Std (RBMap RBMap.empty)
open JsonRpc
section ServerM
-- Pending requests are tracked so they can be cancelled
abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b))
structure ServerContext where
hIn : FS.Stream
hOut : FS.Stream
hLog : FS.Stream
docRef : IO.Ref EditableDocument
pendingRequestsRef : IO.Ref PendingRequestMap
abbrev ServerM := ReaderT ServerContext IO
def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : ServerM Unit := do
(←read).pendingRequestsRef.modify map
/-- Elaborates the next command after `parentSnap` and emits diagnostics. -/
private def nextCmdSnap (m : DocumentMeta) (parentSnap : Snapshot) (cancelTk : CancelToken) : ExceptT ElabTaskError ServerM Snapshot := do
/- Asynchronous snapshot elaboration. -/
section Elab
/-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
private def nextCmdSnap (m : DocumentMeta) (parentSnap : Snapshot) (cancelTk : CancelToken) (hOut : FS.Stream)
: ExceptT ElabTaskError IO Snapshot := do
cancelTk.check
let st ← read
let maybeSnap ← compileNextCmd m.text.source parentSnap
-- TODO(MH): check for interrupt with increased precision
cancelTk.check
let sendDiagnostics (msgLog : MessageLog) : IO Unit := do
let diagnostics ← msgLog.msgs.mapM (msgToDiagnostic m.text)
st.hOut.writeLspNotification {
hOut.writeLspNotification {
method := "textDocument/publishDiagnostics"
param := {
uri := m.uri
@ -148,12 +133,31 @@ section ServerM
sendDiagnostics msgLog
throw ElabTaskError.eof
/-- Elaborates all commands after `initSnap`, emitting the diagnostics. -/
def unfoldCmdSnaps (m : DocumentMeta) (initSnap : Snapshot) (cancelTk : CancelToken) : ServerM (AsyncList ElabTaskError Snapshot) := do
AsyncList.unfoldAsync (nextCmdSnap m . cancelTk (←read)) initSnap
/-- Elaborates all commands after `initSnap`, emitting the diagnostics into `hOut`. -/
def unfoldCmdSnaps (m : DocumentMeta) (initSnap : Snapshot) (cancelTk : CancelToken) (hOut : FS.Stream)
: IO (AsyncList ElabTaskError Snapshot) := do
AsyncList.unfoldAsync (nextCmdSnap m . cancelTk hOut) initSnap
end Elab
/-- Use `leanpkg print-paths` to compile dependencies on the fly and add them to LEAN_PATH. -/
partial def leanpkgSetupSearchPath (leanpkgPath : String) (m : DocumentMeta) (imports : Array Import) : ServerM Unit := do
-- Pending requests are tracked so they can be cancelled
abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b))
structure ServerContext where
hIn : FS.Stream
hOut : FS.Stream
hLog : FS.Stream
srcSearchPath : SearchPath
docRef : IO.Ref EditableDocument
pendingRequestsRef : IO.Ref PendingRequestMap
abbrev ServerM := ReaderT ServerContext IO
/- Worker initialization sequence. -/
section Initialization
/-- Use `leanpkg print-paths` to compile dependencies on the fly and add them to `LEAN_PATH`.
Compilation progress is reported to `hOut` via LSP notifications. Return the search path for
source files. -/
partial def leanpkgSetupSearchPath (leanpkgPath : String) (m : DocumentMeta) (imports : Array Import) (hOut : FS.Stream) : IO SearchPath := do
let leanpkgProc ← Process.spawn {
stdin := Process.Stdio.null
stdout := Process.Stdio.piped
@ -161,7 +165,6 @@ section ServerM
cmd := leanpkgPath
args := #["print-paths"] ++ imports.map (toString ·.module)
}
let hOut := (← read).hOut
-- progress notification: report latest stderr line
let rec processStderr (acc : String) : IO String := do
let line ← leanpkgProc.stderr.getLine
@ -183,23 +186,31 @@ section ServerM
let stderr ← IO.ofExcept stderr.get
if (← leanpkgProc.wait) == 0 then
match stdout.split (· == '\n') with
| [""] => pure () -- e.g. no leanpkg.toml
| [leanPath, leanSrcPath] => searchPathRef.set (← parseSearchPath leanPath (← getBuiltinSearchPath))
| _ => throw <| IO.userError s!"unexpected output from `leanpkg src-paths`:\n{stdout}\nstderr:{stderr}"
| [""] => pure [] -- e.g. no leanpkg.toml
| [leanPath, leanSrcPath] => let sp ← getBuiltinSearchPath
let sp ← addSearchPathFromEnv sp
let sp ← parseSearchPath leanPath sp
searchPathRef.set sp
let srcPath := parseSearchPath leanSrcPath
srcPath.mapM realPathNormalized
| _ => throw <| IO.userError s!"unexpected output from `leanpkg print-paths`:\n{stdout}\nstderr:\n{stderr}"
else
throw <| IO.userError stderr
throw <| IO.userError s!"`leanpkg print-paths` failed:\n{stdout}\nstderr:\n{stderr}"
/-- Compiles the contents of a Lean file. -/
def compileDocument (m : DocumentMeta) : ServerM Unit := do
def compileHeader (m : DocumentMeta) (hOut : FS.Stream) : IO (Snapshot × SearchPath) := do
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
| some path => s!"{path}/bin/leanpkg{System.FilePath.exeSuffix}"
| _ => s!"{← appDir}/leanpkg{System.FilePath.exeSuffix}"
let mut srcSearchPath := match (← IO.getEnv "LEAN_SRC_PATH") with
| some p => parseSearchPath p
| none => []
-- NOTE: leanpkg does not exist in stage 0 (yet?)
if (← fileExists leanpkgPath) then
leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray
let pkgSearchPath ← leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray hOut
srcSearchPath := srcSearchPath ++ pkgSearchPath
let (headerEnv, msgLog) ← Elab.processHeader headerStx opts msgLog inputCtx
let cmdState := Elab.Command.mkState headerEnv msgLog opts
let opts := opts.setBool `interpreter.prefer_native false
@ -210,9 +221,34 @@ section ServerM
mpState := headerParserState
data := SnapshotData.headerData cmdState
}
return (headerSnap, srcSearchPath)
def initializeWorker (p : DidOpenTextDocumentParams) (i o e : FS.Stream)
: IO ServerContext := do
let doc := p.textDocument
/- NOTE(WN): `toFileMap` marks line beginnings as immediately following
"\n", which should be enough to handle both LF and CRLF correctly.
This is because LSP always refers to characters by (line, column),
so if we get the line number correct it shouldn't matter that there
is a CR there. -/
let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
let (headerSnap, srcSearchPath) ← compileHeader meta o
let cancelTk ← CancelToken.new
let cmdSnaps ← unfoldCmdSnaps m headerSnap cancelTk
(←read).docRef.set ⟨m, headerSnap, cmdSnaps, cancelTk⟩
let cmdSnaps ← unfoldCmdSnaps meta headerSnap cancelTk o
let doc : EditableDocument := ⟨meta, headerSnap, cmdSnaps, cancelTk⟩
return {
hIn := i
hOut := o
hLog := e
srcSearchPath := srcSearchPath
docRef := ←IO.mkRef doc
pendingRequestsRef := ←IO.mkRef RBMap.empty
}
end Initialization
section Updates
def updatePendingRequests (map : PendingRequestMap → PendingRequestMap) : ServerM Unit := do
(←read).pendingRequestsRef.modify map
/-- Given the new document and `changePos`, the UTF-8 offset of a change into the pre-change source,
updates editable doc state. -/
@ -239,7 +275,7 @@ section ServerM
let mut validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos)
if validSnaps.length = 0 then
let cancelTk ← CancelToken.new
let newCmdSnaps ← unfoldCmdSnaps newMeta newHeaderSnap cancelTk
let newCmdSnaps ← unfoldCmdSnaps newMeta newHeaderSnap cancelTk st.hOut
st.docRef.set ⟨newMeta, newHeaderSnap, newCmdSnaps, cancelTk⟩
else
/- When at least one valid non-header snap exists, it may happen that a change does not fall
@ -257,23 +293,14 @@ section ServerM
validSnaps ← validSnaps.dropLast
lastSnap ← preLastSnap
let cancelTk ← CancelToken.new
let newSnaps ← unfoldCmdSnaps newMeta lastSnap cancelTk
let newSnaps ← unfoldCmdSnaps newMeta lastSnap cancelTk st.hOut
let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps
st.docRef.set ⟨newMeta, newHeaderSnap, newCmdSnaps, cancelTk⟩
end ServerM
end Updates
/- Notifications are handled in the main thread. They may change global worker state
such as the current file contents. -/
section NotificationHandling
def handleDidOpen (p : DidOpenTextDocumentParams) : ServerM Unit :=
let doc := p.textDocument
/- NOTE(WN): `toFileMap` marks line beginnings as immediately following
"\n", which should be enough to handle both LF and CRLF correctly.
This is because LSP always refers to characters by (line, column),
so if we get the line number correct it shouldn't matter that there
is a CR there. -/
compileDocument ⟨doc.uri, doc.version, doc.text.toFileMap⟩
def handleDidChange (p : DidChangeTextDocumentParams) : ServerM Unit := do
let docId := p.textDocument
let changes := p.contentChanges
@ -313,6 +340,23 @@ section RequestHandling
def mapTask (t : Task α) (f : α → ExceptT RequestError ServerM β) : RequestM β := fun st =>
(IO.mapTask · t) fun a => f a st
/-- Create a task which waits for a snapshot matching `p`, handles various errors,
and if a matching snapshot was found executes `x` with it. If not found, the task
executes `notFoundX`. -/
def withWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
(notFoundX : ExceptT RequestError ServerM β)
(x : Snapshot → ExceptT RequestError ServerM β)
: ServerM (Task (Except IO.Error (Except RequestError β))) := do
let findTask ← doc.cmdSnaps.waitFind? p
mapTask findTask fun
| Except.error ElabTaskError.aborted =>
throwThe RequestError RequestError.fileChanged
| Except.error (ElabTaskError.ioError e) =>
throwThe IO.Error e
| Except.error ElabTaskError.eof => notFoundX
| Except.ok none => notFoundX
| Except.ok (some snap) => x snap
/- Requests that need data from a certain command should traverse the snapshots
by successively getting the next task, meaning that we might need to wait for elaboration.
When that happens, the request should send a "content changed" error to the user
@ -325,55 +369,23 @@ section RequestHandling
let st ← read
let doc ← st.docRef.get
let text := doc.meta.text
let hoverPos := text.lspPosToUtf8Pos p.position
let findTask ← doc.cmdSnaps.waitFind? (fun s => s.endPos > hoverPos)
let mkHover (s : String) (f : String.Pos) (t : String.Pos) : Hover :=
{ contents := { kind := MarkupKind.markdown
value := s }
range? := some { start := text.utf8PosToLspPos f
«end» := text.utf8PosToLspPos t } }
mapTask findTask fun
| Except.error ElabTaskError.aborted =>
throwThe RequestError RequestError.fileChanged
| Except.error (ElabTaskError.ioError e) =>
throwThe IO.Error e
| Except.error ElabTaskError.eof =>
return none
| Except.ok (some snap) => do
for t in snap.toCmdState.infoState.trees do
let ts := t.smallestNodes fun
| Info.ofTermInfo i =>
match i.pos?, i.tailPos? with
| some pos, some tailPos =>
/- TODO(WN): when we have a way to do so,
check for synthetic syntax and allow arbitrary syntax kinds. -/
if pos ≤ hoverPos ∧ hoverPos < tailPos then
#[identKind,
strLitKind,
charLitKind,
numLitKind,
scientificLitKind,
nameLitKind,
fieldIdxKind,
interpolatedStrLitKind,
interpolatedStrKind
].contains i.stx.getKind
else false
| _, _ => false
| _ => false
let mut nds : Array (Nat × ContextInfo × TermInfo) := #[]
for t in ts do
if let InfoTree.context ci (InfoTree.node (Info.ofTermInfo i) _) := t then
let diff := i.tailPos?.get! - i.pos?.get!
nds := nds.push (diff, ci, i)
if let some (_, ci, i) := nds.getMax? (fun a b => a.1 > b.1) then
let hoverPos := text.lspPosToUtf8Pos p.position
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure none) fun snap => do
for t in snap.toCmdState.infoState.trees do
if let some (ci, i) := t.hoverableTermAt? hoverPos then
let tFmt ← ci.runMetaM i.lctx do
return f!"{← Meta.ppExpr i.expr} : {← Meta.ppExpr (← Meta.inferType i.expr)}"
let mut hoverFmt := f!"```lean
{tFmt}
```"
if let Expr.const n .. := i.expr then
if let some n := i.expr.constName? then
if let some doc ← ci.runMetaM i.lctx <| findDocString? n then
hoverFmt := f!"{hoverFmt}\n***\n{doc}"
@ -381,14 +393,42 @@ section RequestHandling
pure ()
return none
| Except.ok none => return none
def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam)
: ServerM (Task (Except IO.Error (Except RequestError WaitForDiagnostics))) := do
open Elab in
partial def handleDefinition (goToType? : Bool) (id : RequestID) (p : TextDocumentPositionParams)
: ServerM (Task (Except IO.Error (Except RequestError (Array LocationLink)))) := do
let st ← read
let doc ← st.docRef.get
let t ← doc.cmdSnaps.waitAll
t.map fun _ => Except.ok $ Except.ok WaitForDiagnostics.mk
let text := doc.meta.text
let hoverPos := text.lspPosToUtf8Pos p.position
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure #[]) fun snap => do
for t in snap.toCmdState.infoState.trees do
if let some (ci, i) := t.hoverableTermAt? hoverPos then
let expr := if goToType? then ← ci.runMetaM i.lctx <| Meta.inferType i.expr
else i.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? ← st.srcSearchPath.findWithExt ".lean" modName
pure <| modFname?.map ("file://" ++ ·)
| 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.pos?.get!, text.utf8PosToLspPos i.tailPos?.get!⟩
targetUri := modUri
targetRange := declRangeToLspRange ranges.range
targetSelectionRange := declRangeToLspRange ranges.selectionRange
}
return #[ll]
return #[]
def rangeOfSyntax (text : FileMap) (stx : Syntax) : Range :=
⟨text.utf8PosToLspPos <| stx.getHeadInfo.get!.pos.get!,
@ -449,6 +489,13 @@ section RequestHandling
children? := syms.toArray
} :: syms', stxs'')
def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam)
: ServerM (Task (Except IO.Error (Except RequestError WaitForDiagnostics))) := do
let st ← read
let doc ← st.docRef.get
let t ← doc.cmdSnaps.waitAll
t.map fun _ => Except.ok $ Except.ok WaitForDiagnostics.mk
end RequestHandling
section MessageHandling
@ -487,6 +534,9 @@ section MessageHandling
match method with
| "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam WaitForDiagnostics handleWaitForDiagnostics
| "textDocument/hover" => handle HoverParams (Option Hover) handleHover
| "textDocument/declaration" => handle TextDocumentPositionParams (Array LocationLink) <| handleDefinition (goToType? := false)
| "textDocument/definition" => handle TextDocumentPositionParams (Array LocationLink) <| handleDefinition (goToType? := false)
| "textDocument/typeDefinition" => handle TextDocumentPositionParams (Array LocationLink) <| handleDefinition (goToType? := true)
| "textDocument/documentSymbol" => handle DocumentSymbolParams DocumentSymbolResult handleDocumentSymbol
| _ => throwServerError s!"Got unsupported request: {method}"
end MessageHandling
@ -529,17 +579,9 @@ def initAndRunWorker (i o e : FS.Stream) : IO UInt32 := do
let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
let e ← e.withPrefix s!"[{param.textDocument.uri}] "
let _ ← IO.setStderr e
let ctx : ServerContext := {
hIn := i
hOut := o
hLog := e
-- `openDocument` will not access `docRef`, but set it
docRef := ←IO.mkRef arbitrary
pendingRequestsRef := ←IO.mkRef (RBMap.empty : PendingRequestMap)
}
ReaderT.run (r := ctx) try
handleDidOpen param
mainLoop
try
let ctx ← initializeWorker param i o e
ReaderT.run (r := ctx) mainLoop
return 0
catch e =>
o.writeLspNotification {
@ -565,4 +607,3 @@ def workerMain : IO UInt32 := do
return (1 : UInt32)
end Lean.Server.FileWorker

32
stage0/src/Lean/Server/InfoUtils.lean generated
View file

@ -45,4 +45,36 @@ def TacticInfo.pos? (i : TacticInfo) : Option String.Pos :=
def TacticInfo.tailPos? (i : TacticInfo) : Option String.Pos :=
i.stx.getTailPos
/-- Find a `TermInfo`, if any, which should be shown on hover/cursor at position `hoverPos`. -/
partial def InfoTree.hoverableTermAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × TermInfo) :=
let ts := t.smallestNodes fun
| Info.ofTermInfo i =>
match i.pos?, i.tailPos? with
| some pos, some tailPos =>
/- TODO(WN): when we have a way to do so,
check for synthetic syntax and allow arbitrary syntax kinds. -/
if pos ≤ hoverPos ∧ hoverPos < tailPos then
#[identKind,
strLitKind,
charLitKind,
numLitKind,
scientificLitKind,
nameLitKind,
fieldIdxKind,
interpolatedStrLitKind,
interpolatedStrKind
].contains i.stx.getKind
else false
| _, _ => false
| _ => false
let terms : List (Nat × ContextInfo × TermInfo) := ts.filterMap (fun
| context ci (node (Info.ofTermInfo i) _) =>
let diff := i.tailPos?.get! - i.pos?.get!
some (diff, ci, i)
| _ => none
)
terms.toArray.getMax? (fun a b => a.1 > b.1) |>.map fun (_, ci, i) => (ci, i)
end Lean.Elab

6
stage0/src/Lean/Server/Watchdog.lean generated
View file

@ -355,6 +355,9 @@ section MessageHandling
match method with
| "textDocument/waitForDiagnostics" => handle WaitForDiagnosticsParam
| "textDocument/hover" => handle HoverParams
| "textDocument/declaration" => handle DeclarationParams
| "textDocument/definition" => handle DefinitionParams
| "textDocument/typeDefinition" => handle TypeDefinitionParams
| "textDocument/documentSymbol" => handle DocumentSymbolParams
| _ =>
(←read).hOut.writeLspResponseError
@ -437,6 +440,9 @@ def mkLeanServerCapabilities : ServerCapabilities := {
save? := none
}
hoverProvider := true
declarationProvider := true
definitionProvider := true
typeDefinitionProvider := true
documentSymbolProvider := true
}

37
stage0/src/Lean/Util/Path.lean generated
View file

@ -18,15 +18,32 @@ def realPathNormalized (fname : String) : IO String := do
let fname ← IO.realPath fname
pure (System.FilePath.normalizePath fname)
def modPathToFilePath : Name → String
| Name.str p h _ => modPathToFilePath p ++ pathSep ++ h
| Name.anonymous => ""
| Name.num p _ _ => panic! "ill-formed import"
abbrev SearchPath := List String
namespace SearchPath
/-- If the package of `mod` can be found in `sp`, return the path with extension
`ext` (`.lean` or `.olean`) corresponding to `mod`. Otherwise, return `none.` -/
def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option String) := do
let pkg := mod.getRoot.toString
let root? ← sp.findM? (fun path =>
IO.isDir s!"{path}{pathSep}{pkg}" <||> IO.fileExists s!"{path}{pathSep}{pkg}{ext}")
return root?.map (· ++ modPathToFilePath mod ++ ext)
end SearchPath
builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {}
def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath :=
pure $ System.FilePath.splitSearchPath path ++ sp
def parseSearchPath (path : String) (sp : SearchPath := ∅) : SearchPath :=
System.FilePath.splitSearchPath path ++ sp
@[extern c inline "LEAN_IS_STAGE0"]
constant isStage0 (u : Unit) : Bool
private constant isStage0 (u : Unit) : Bool
def getBuiltinSearchPath : IO SearchPath := do
let appDir ← IO.appDir
@ -42,23 +59,17 @@ def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
@[export lean_init_search_path]
def initSearchPath (path : Option String := none) : IO Unit :=
match path with
| some path => parseSearchPath path >>= searchPathRef.set
| some path => searchPathRef.set <| parseSearchPath path
| none => do
let sp ← getBuiltinSearchPath
let sp ← addSearchPathFromEnv sp
searchPathRef.set sp
def modPathToFilePath : Name → String
| Name.str p h _ => modPathToFilePath p ++ pathSep ++ h
| Name.anonymous => ""
| Name.num p _ _ => panic! "ill-formed import"
def findOLean (mod : Name) : IO String := do
let sp ← searchPathRef.get
let pkg := mod.getRoot.toString
let some root ← sp.findM? (fun path => IO.isDir s!"{path}{pathSep}{pkg}" <||> IO.fileExists s!"{path}{pathSep}{pkg}.olean")
| throw $ IO.userError $ "unknown package '" ++ pkg ++ "'"
pure $ root ++ modPathToFilePath mod ++ ".olean"
let some fname ← sp.findWithExt ".olean" mod
| throw $ IO.userError $ "unknown package '" ++ mod.getRoot.toString ++ "'"
return fname
/-- Infer module name of source file name. -/
@[export lean_module_name_of_file]

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

343
stage0/stdlib/Lean/Data/Lsp/Capabilities.c generated
View file

@ -13,37 +13,43 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3;
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_instFromJsonOption___rarg___closed__1;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____boxed(lean_object*);
uint8_t l_Lean_Lsp_ServerCapabilities_declarationProvider___default;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5;
uint8_t l_Lean_Lsp_ServerCapabilities_documentSymbolProvider___default;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3;
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities;
lean_object* l_Lean_Lsp_ClientCapabilities_hasToJson(lean_object*);
uint8_t l_Lean_Lsp_ServerCapabilities_hoverProvider___default;
lean_object* l_List_join___rarg(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____spec__1___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Lsp_ServerCapabilities_typeDefinitionProvider___default;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_381____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_478_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____boxed(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_ClientCapabilities_hasToJson___closed__1;
lean_object* l_Lean_Lsp_ClientCapabilities_hasToJson___boxed(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonClientCapabilities(lean_object*);
lean_object* l_Lean_Lsp_instToJsonServerCapabilities;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108_(lean_object*);
lean_object* l_Lean_Lsp_instToJsonServerCapabilities___closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____spec__1(lean_object*, lean_object*);
uint8_t l_Lean_Lsp_ServerCapabilities_definitionProvider___default;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4;
lean_object* l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default;
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities___closed__1;
lean_object* l_Lean_Json_getObjValD(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2;
lean_object* l_Lean_Json_mkObj(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37_(lean_object*);
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_534_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonClientCapabilities___closed__1;
lean_object* l_Lean_Lsp_instFromJsonClientCapabilities___boxed(lean_object*);
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6;
static lean_object* _init_l_Lean_Lsp_instFromJsonClientCapabilities___closed__1() {
_start:
{
@ -121,7 +127,31 @@ x_1 = 0;
return x_1;
}
}
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____spec__1(lean_object* x_1, lean_object* x_2) {
static uint8_t _init_l_Lean_Lsp_ServerCapabilities_definitionProvider___default() {
_start:
{
uint8_t x_1;
x_1 = 0;
return x_1;
}
}
static uint8_t _init_l_Lean_Lsp_ServerCapabilities_declarationProvider___default() {
_start:
{
uint8_t x_1;
x_1 = 0;
return x_1;
}
}
static uint8_t _init_l_Lean_Lsp_ServerCapabilities_typeDefinitionProvider___default() {
_start:
{
uint8_t x_1;
x_1 = 0;
return x_1;
}
}
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
@ -147,7 +177,7 @@ return x_8;
}
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1() {
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1() {
_start:
{
lean_object* x_1;
@ -155,7 +185,7 @@ x_1 = lean_mk_string("textDocumentSync");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2() {
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2() {
_start:
{
lean_object* x_1;
@ -163,7 +193,7 @@ x_1 = lean_mk_string("hoverProvider");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3() {
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3() {
_start:
{
lean_object* x_1;
@ -171,17 +201,41 @@ x_1 = lean_mk_string("documentSymbolProvider");
return x_1;
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37_(lean_object* x_1) {
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4() {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; 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_1;
x_1 = lean_mk_string("definitionProvider");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("declarationProvider");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("typeDefinitionProvider");
return x_1;
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; uint8_t 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_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; lean_object* x_38;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1;
x_4 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____spec__1(x_3, x_2);
x_3 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1;
x_4 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____spec__1(x_3, x_2);
x_5 = lean_ctor_get_uint8(x_1, sizeof(void*)*1);
x_6 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_6, 0, x_5);
x_7 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2;
x_7 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
@ -192,41 +246,80 @@ lean_ctor_set(x_10, 1, x_9);
x_11 = lean_ctor_get_uint8(x_1, sizeof(void*)*1 + 1);
x_12 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_12, 0, x_11);
x_13 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3;
x_13 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3;
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_12);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_9);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_9);
x_17 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_17, 0, x_10);
lean_ctor_set(x_17, 1, x_16);
x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_4);
lean_ctor_set(x_18, 1, x_17);
x_19 = l_List_join___rarg(x_18);
x_20 = l_Lean_Json_mkObj(x_19);
return x_20;
x_16 = lean_ctor_get_uint8(x_1, sizeof(void*)*1 + 2);
x_17 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_17, 0, x_16);
x_18 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4;
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_17);
x_20 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_9);
x_21 = lean_ctor_get_uint8(x_1, sizeof(void*)*1 + 3);
x_22 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_22, 0, x_21);
x_23 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5;
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_24);
lean_ctor_set(x_25, 1, x_9);
x_26 = lean_ctor_get_uint8(x_1, sizeof(void*)*1 + 4);
x_27 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_27, 0, x_26);
x_28 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6;
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_28);
lean_ctor_set(x_29, 1, x_27);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_9);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_9);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_25);
lean_ctor_set(x_32, 1, x_31);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_20);
lean_ctor_set(x_33, 1, x_32);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_15);
lean_ctor_set(x_34, 1, x_33);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_10);
lean_ctor_set(x_35, 1, x_34);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_4);
lean_ctor_set(x_36, 1, x_35);
x_37 = l_List_join___rarg(x_36);
x_38 = l_Lean_Json_mkObj(x_37);
return x_38;
}
}
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____spec__1(x_1, x_2);
x_3 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____spec__1(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____boxed(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37_(x_1);
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43_(x_1);
lean_dec(x_1);
return x_2;
}
@ -235,7 +328,7 @@ static lean_object* _init_l_Lean_Lsp_instToJsonServerCapabilities___closed__1()
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____boxed), 1, 0);
return x_1;
}
}
@ -247,7 +340,7 @@ x_1 = l_Lean_Lsp_instToJsonServerCapabilities___closed__1;
return x_1;
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____spec__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
@ -296,12 +389,12 @@ return x_11;
}
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75_(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____spec__1(x_1, x_2);
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
@ -314,7 +407,7 @@ lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_3, 0);
lean_inc(x_5);
lean_dec(x_3);
x_6 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2;
x_6 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2;
x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_381____spec__1(x_1, x_6);
if (lean_obj_tag(x_7) == 0)
{
@ -329,7 +422,7 @@ lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_7, 0);
lean_inc(x_9);
lean_dec(x_7);
x_10 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3;
x_10 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3;
x_11 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_381____spec__1(x_1, x_10);
if (lean_obj_tag(x_11) == 0)
{
@ -341,61 +434,136 @@ return x_12;
}
else
{
uint8_t x_13;
x_13 = !lean_is_exclusive(x_11);
if (x_13 == 0)
lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_13 = lean_ctor_get(x_11, 0);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4;
x_15 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_381____spec__1(x_1, x_14);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_14; lean_object* x_15; uint8_t x_16; uint8_t x_17;
x_14 = lean_ctor_get(x_11, 0);
x_15 = lean_alloc_ctor(0, 1, 2);
lean_ctor_set(x_15, 0, x_5);
x_16 = lean_unbox(x_9);
lean_object* x_16;
lean_dec(x_13);
lean_dec(x_9);
lean_ctor_set_uint8(x_15, sizeof(void*)*1, x_16);
x_17 = lean_unbox(x_14);
lean_dec(x_14);
lean_ctor_set_uint8(x_15, sizeof(void*)*1 + 1, x_17);
lean_ctor_set(x_11, 0, x_15);
return x_11;
lean_dec(x_5);
x_16 = lean_box(0);
return x_16;
}
else
{
lean_object* x_18; lean_object* x_19; uint8_t x_20; uint8_t x_21; lean_object* x_22;
x_18 = lean_ctor_get(x_11, 0);
lean_inc(x_18);
lean_dec(x_11);
x_19 = lean_alloc_ctor(0, 1, 2);
lean_ctor_set(x_19, 0, x_5);
x_20 = lean_unbox(x_9);
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5;
x_19 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_381____spec__1(x_1, x_18);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20;
lean_dec(x_17);
lean_dec(x_13);
lean_dec(x_9);
lean_ctor_set_uint8(x_19, sizeof(void*)*1, x_20);
x_21 = lean_unbox(x_18);
lean_dec(x_18);
lean_ctor_set_uint8(x_19, sizeof(void*)*1 + 1, x_21);
x_22 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_22, 0, x_19);
return x_22;
lean_dec(x_5);
x_20 = lean_box(0);
return x_20;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_19, 0);
lean_inc(x_21);
lean_dec(x_19);
x_22 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6;
x_23 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_381____spec__1(x_1, x_22);
if (lean_obj_tag(x_23) == 0)
{
lean_object* x_24;
lean_dec(x_21);
lean_dec(x_17);
lean_dec(x_13);
lean_dec(x_9);
lean_dec(x_5);
x_24 = lean_box(0);
return x_24;
}
else
{
uint8_t x_25;
x_25 = !lean_is_exclusive(x_23);
if (x_25 == 0)
{
lean_object* x_26; lean_object* x_27; uint8_t x_28; uint8_t x_29; uint8_t x_30; uint8_t x_31; uint8_t x_32;
x_26 = lean_ctor_get(x_23, 0);
x_27 = lean_alloc_ctor(0, 1, 5);
lean_ctor_set(x_27, 0, x_5);
x_28 = lean_unbox(x_9);
lean_dec(x_9);
lean_ctor_set_uint8(x_27, sizeof(void*)*1, x_28);
x_29 = lean_unbox(x_13);
lean_dec(x_13);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 1, x_29);
x_30 = lean_unbox(x_17);
lean_dec(x_17);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 2, x_30);
x_31 = lean_unbox(x_21);
lean_dec(x_21);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 3, x_31);
x_32 = lean_unbox(x_26);
lean_dec(x_26);
lean_ctor_set_uint8(x_27, sizeof(void*)*1 + 4, x_32);
lean_ctor_set(x_23, 0, x_27);
return x_23;
}
else
{
lean_object* x_33; lean_object* x_34; uint8_t x_35; uint8_t x_36; uint8_t x_37; uint8_t x_38; uint8_t x_39; lean_object* x_40;
x_33 = lean_ctor_get(x_23, 0);
lean_inc(x_33);
lean_dec(x_23);
x_34 = lean_alloc_ctor(0, 1, 5);
lean_ctor_set(x_34, 0, x_5);
x_35 = lean_unbox(x_9);
lean_dec(x_9);
lean_ctor_set_uint8(x_34, sizeof(void*)*1, x_35);
x_36 = lean_unbox(x_13);
lean_dec(x_13);
lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 1, x_36);
x_37 = lean_unbox(x_17);
lean_dec(x_17);
lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 2, x_37);
x_38 = lean_unbox(x_21);
lean_dec(x_21);
lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 3, x_38);
x_39 = lean_unbox(x_33);
lean_dec(x_33);
lean_ctor_set_uint8(x_34, sizeof(void*)*1 + 4, x_39);
x_40 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_40, 0, x_34);
return x_40;
}
}
}
}
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
}
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____spec__1(x_1, x_2);
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____boxed(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75_(x_1);
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108_(x_1);
lean_dec(x_1);
return x_2;
}
@ -404,7 +572,7 @@ static lean_object* _init_l_Lean_Lsp_instFromJsonServerCapabilities___closed__1(
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75____boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108____boxed), 1, 0);
return x_1;
}
}
@ -441,12 +609,21 @@ l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default = _init_l_Lean_Lsp_
lean_mark_persistent(l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default);
l_Lean_Lsp_ServerCapabilities_hoverProvider___default = _init_l_Lean_Lsp_ServerCapabilities_hoverProvider___default();
l_Lean_Lsp_ServerCapabilities_documentSymbolProvider___default = _init_l_Lean_Lsp_ServerCapabilities_documentSymbolProvider___default();
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__1);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__2);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37____closed__3);
l_Lean_Lsp_ServerCapabilities_definitionProvider___default = _init_l_Lean_Lsp_ServerCapabilities_definitionProvider___default();
l_Lean_Lsp_ServerCapabilities_declarationProvider___default = _init_l_Lean_Lsp_ServerCapabilities_declarationProvider___default();
l_Lean_Lsp_ServerCapabilities_typeDefinitionProvider___default = _init_l_Lean_Lsp_ServerCapabilities_typeDefinitionProvider___default();
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__1);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__2);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__3);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__4);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__5);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43____closed__6);
l_Lean_Lsp_instToJsonServerCapabilities___closed__1 = _init_l_Lean_Lsp_instToJsonServerCapabilities___closed__1();
lean_mark_persistent(l_Lean_Lsp_instToJsonServerCapabilities___closed__1);
l_Lean_Lsp_instToJsonServerCapabilities = _init_l_Lean_Lsp_instToJsonServerCapabilities();

8
stage0/stdlib/Lean/Data/Lsp/InitShutdown.c generated
View file

@ -88,7 +88,7 @@ lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonInitializePar
lean_object* l_Lean_Lsp_instToJsonInitializedParams(lean_object*);
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instFromJsonInitializeResult;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____closed__14;
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonServerInfo____x40_Lean_Data_Lsp_InitShutdown___hyg_316_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____closed__5;
@ -121,7 +121,7 @@ lean_object* l_Lean_Lsp_instToJsonInitializeParams___closed__1;
lean_object* l_Lean_Lsp_instFromJsonServerInfo;
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____closed__1;
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____spec__2___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43_(lean_object*);
lean_object* l_Lean_Lsp_InitializeParams_rootUri_x3f___default;
lean_object* l_Lean_Lsp_InitializeParams_initializationOptions_x3f___default;
lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____closed__2;
@ -1650,7 +1650,7 @@ _start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_37_(x_2);
x_3 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_43_(x_2);
x_4 = l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_165____closed__5;
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_4);
@ -1712,7 +1712,7 @@ _start:
{
lean_object* x_3; lean_object* x_4;
x_3 = l_Lean_Json_getObjValD(x_1, x_2);
x_4 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_75_(x_3);
x_4 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_108_(x_3);
lean_dec(x_3);
return x_4;
}

272
stage0/stdlib/Lean/Data/Lsp/LanguageFeatures.c generated
View file

@ -20,15 +20,16 @@ lean_object* l_Lean_Lsp_instToJsonHoverParams(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__61;
lean_object* l_Lean_Lsp_instFromJsonDefinitionParams___boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__75;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__26;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__58;
lean_object* l_Lean_Lsp_instFromJsonHoverParams___boxed(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299____spec__1(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1626____closed__2;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_125____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4;
lean_object* l_Lean_Lsp_DocumentSymbolAux_children_x3f___default(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocationLink____x40_Lean_Data_Lsp_Basic___hyg_631____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux___rarg(lean_object*);
@ -36,6 +37,9 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__12;
lean_object* l_Lean_Lsp_instToJsonDocumentSymbol;
lean_object* l_Lean_Lsp_instToJsonSymbolKind_match__1(lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonDeclarationParams(lean_object*);
lean_object* l_Lean_Lsp_instToJsonDefinitionParams(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonDefinitionParams(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__71;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__7;
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__2(lean_object*, lean_object*);
@ -43,15 +47,17 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__42;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__53;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__37;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__55;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind_match__1___rarg___boxed(lean_object**);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__3;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_join___rarg(lean_object*);
uint8_t l_USize_decLt(size_t, size_t);
lean_object* l_Lean_Lsp_instToJsonHover___closed__1;
lean_object* l_Lean_Lsp_instToJsonDocumentSymbolParams;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__14;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__28;
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__5;
extern lean_object* l_Int_Int_pow___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_11____closed__1;
@ -77,51 +83,51 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind_match__1___rarg(uint8_t, lean_objec
lean_object* l_Array_mapMUnsafe_map___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__49;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__50;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2;
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__6;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__34;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__48;
lean_object* l_Lean_Lsp_instToJsonSymbolKind(uint8_t);
lean_object* l_Lean_Lsp_instFromJsonDocumentSymbolParams;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__72;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__23;
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocationLink____x40_Lean_Data_Lsp_Basic___hyg_584____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go_match__1(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__13;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__41;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259_(lean_object*);
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__1(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373_(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_125_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__38;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__21;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_40____boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonDeclarationParams(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__22;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1;
size_t lean_usize_of_nat(lean_object*);
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_499____closed__2;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__62;
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentEdit____x40_Lean_Data_Lsp_Basic___hyg_1053____closed__1;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__54;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2;
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentIdentifier____x40_Lean_Data_Lsp_Basic___hyg_915_(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__33;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__25;
lean_object* l_Lean_Lsp_instFromJsonDeclarationParams___boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__29;
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1660_(lean_object*);
lean_object* l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__52;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__46;
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__1(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValD(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instFromJsonHoverParams(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__65;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__70;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__35;
lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams___boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonHover;
lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__36;
@ -139,6 +145,7 @@ lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__74;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__60;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__47;
extern lean_object* l_Lean_JsonNumber_toString___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239____boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__44;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_LanguageFeatures___hyg_40____spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__1;
@ -147,21 +154,23 @@ lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonHove
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__57;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__17;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__8;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_155_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonHover;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__45;
lean_object* l_Lean_Lsp_instFromJsonHover___closed__1;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__67;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__9;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__40;
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__27;
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__4;
lean_object* l_Lean_Lsp_instToJsonDocumentSymbolParams___closed__1;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2(lean_object*);
lean_object* l_Lean_Lsp_instToJsonSymbolKind___closed__68;
lean_object* l_Lean_Lsp_instToJsonDocumentSymbolResult(lean_object*);
lean_object* l_Lean_Lsp_instToJsonTypeDefinitionParams(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1;
lean_object* lean_nat_to_int(lean_object*);
lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go_match__1___rarg(lean_object*, lean_object*);
@ -382,7 +391,154 @@ x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionPara
return x_2;
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_125_(lean_object* x_1) {
lean_object* l_Lean_Lsp_instFromJsonDeclarationParams(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
else
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_2);
if (x_4 == 0)
{
return x_2;
}
else
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
lean_dec(x_2);
x_6 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
}
}
}
lean_object* l_Lean_Lsp_instFromJsonDeclarationParams___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonDeclarationParams(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instToJsonDeclarationParams(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instFromJsonDefinitionParams(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
else
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_2);
if (x_4 == 0)
{
return x_2;
}
else
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
lean_dec(x_2);
x_6 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
}
}
}
lean_object* l_Lean_Lsp_instFromJsonDefinitionParams___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonDefinitionParams(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instToJsonDefinitionParams(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1299_(x_1);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
x_3 = lean_box(0);
return x_3;
}
else
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_2);
if (x_4 == 0)
{
return x_2;
}
else
{
lean_object* x_5; lean_object* x_6;
x_5 = lean_ctor_get(x_2, 0);
lean_inc(x_5);
lean_dec(x_2);
x_6 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_6, 0, x_5);
return x_6;
}
}
}
}
lean_object* l_Lean_Lsp_instFromJsonTypeDefinitionParams___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonTypeDefinitionParams(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instToJsonTypeDefinitionParams(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1265_(x_1);
return x_2;
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
@ -415,11 +571,11 @@ return x_7;
}
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_125____boxed(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_125_(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(x_1);
lean_dec(x_1);
return x_2;
}
@ -428,7 +584,7 @@ static lean_object* _init_l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_125____boxed), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239____boxed), 1, 0);
return x_1;
}
}
@ -440,7 +596,7 @@ x_1 = l_Lean_Lsp_instFromJsonDocumentSymbolParams___closed__1;
return x_1;
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_155_(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
@ -465,7 +621,7 @@ static lean_object* _init_l_Lean_Lsp_instToJsonDocumentSymbolParams___closed__1(
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_155_), 1, 0);
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_269_), 1, 0);
return x_1;
}
}
@ -2338,7 +2494,7 @@ x_2 = lean_box(0);
return x_2;
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg(lean_object* x_1, size_t x_2, size_t x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
@ -2369,15 +2525,15 @@ goto _start;
}
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2(lean_object* x_1) {
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg___boxed), 4, 0);
x_2 = lean_alloc_closure((void*)(l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg___boxed), 4, 0);
return x_2;
}
}
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
if (lean_obj_tag(x_3) == 0)
@ -2399,7 +2555,7 @@ x_7 = lean_usize_of_nat(x_6);
lean_dec(x_6);
x_8 = 0;
x_9 = x_5;
x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg(x_1, x_7, x_8, x_9);
x_10 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg(x_1, x_7, x_8, x_9);
x_11 = x_10;
x_12 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_12, 0, x_11);
@ -2414,15 +2570,15 @@ return x_15;
}
}
}
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__1(lean_object* x_1) {
lean_object* l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__1___rarg), 3, 0);
x_2 = lean_alloc_closure((void*)(l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__1___rarg), 3, 0);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1() {
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1() {
_start:
{
lean_object* x_1;
@ -2430,7 +2586,7 @@ x_1 = lean_mk_string("name");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2() {
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2() {
_start:
{
lean_object* x_1;
@ -2438,7 +2594,7 @@ x_1 = lean_mk_string("detail");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3() {
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3() {
_start:
{
lean_object* x_1;
@ -2446,7 +2602,7 @@ x_1 = lean_mk_string("selectionRange");
return x_1;
}
}
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4() {
static lean_object* _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4() {
_start:
{
lean_object* x_1;
@ -2454,7 +2610,7 @@ x_1 = lean_mk_string("children");
return x_1;
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg(lean_object* x_1, lean_object* x_2) {
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint8_t 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; 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; 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;
@ -2472,7 +2628,7 @@ lean_inc(x_8);
lean_dec(x_2);
x_9 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_9, 0, x_3);
x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1;
x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1;
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
@ -2480,7 +2636,7 @@ x_12 = lean_box(0);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
x_14 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2;
x_14 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2;
x_15 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1354____spec__1(x_14, x_4);
lean_dec(x_4);
x_16 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_6);
@ -2492,15 +2648,15 @@ x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_12);
x_20 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_7);
x_21 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3;
x_21 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3;
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_20);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_12);
x_24 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4;
x_25 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__1___rarg(x_1, x_24, x_8);
x_24 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4;
x_25 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__1___rarg(x_1, x_24, x_8);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_12);
@ -2719,15 +2875,15 @@ return x_37;
}
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259_(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373_(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg), 2, 0);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg), 2, 0);
return x_2;
}
}
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
@ -2735,7 +2891,7 @@ x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = lean_unbox_usize(x_3);
lean_dec(x_3);
x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____spec__2___rarg(x_1, x_5, x_6, x_4);
x_7 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____spec__2___rarg(x_1, x_5, x_6, x_4);
return x_7;
}
}
@ -2743,7 +2899,7 @@ lean_object* l_Lean_Lsp_instToJsonDocumentSymbolAux___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg), 2, 1);
x_2 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
@ -2790,7 +2946,7 @@ x_6 = lean_array_uget(x_3, x_2);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_array_uset(x_3, x_2, x_7);
x_9 = x_6;
x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_9);
x_10 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_9);
x_11 = 1;
x_12 = x_2 + x_11;
x_13 = x_10;
@ -2837,7 +2993,7 @@ return x_14;
}
}
}
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; uint8_t x_4; lean_object* x_5; lean_object* x_6; 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; 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; 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;
@ -2855,7 +3011,7 @@ lean_inc(x_7);
lean_dec(x_1);
x_8 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_8, 0, x_2);
x_9 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1;
x_9 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1;
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_8);
@ -2863,7 +3019,7 @@ x_11 = lean_box(0);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
x_13 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2;
x_13 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2;
x_14 = l_Lean_Json_opt___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonDocumentFilter____x40_Lean_Data_Lsp_Basic___hyg_1354____spec__1(x_13, x_3);
lean_dec(x_3);
x_15 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_5);
@ -2875,14 +3031,14 @@ x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_11);
x_19 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353_(x_6);
x_20 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3;
x_20 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3;
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
x_22 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_11);
x_23 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4;
x_23 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4;
x_24 = l_Lean_Json_opt___at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__2(x_23, x_7);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_24);
@ -3106,7 +3262,7 @@ lean_object* l_Lean_Lsp_instToJsonDocumentSymbol_go(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_1);
x_2 = l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____at_Lean_Lsp_instToJsonDocumentSymbol_go___spec__1(x_1);
return x_2;
}
}
@ -3345,14 +3501,14 @@ l_Lean_Lsp_instToJsonSymbolKind___closed__76 = _init_l_Lean_Lsp_instToJsonSymbol
lean_mark_persistent(l_Lean_Lsp_instToJsonSymbolKind___closed__76);
l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default = _init_l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default();
lean_mark_persistent(l_Lean_Lsp_DocumentSymbolAux_detail_x3f___default);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__1);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__2);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__3);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_259____rarg___closed__4);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__1);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__2);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__3);
l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4 = _init_l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4();
lean_mark_persistent(l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_toJsonDocumentSymbolAux____x40_Lean_Data_Lsp_LanguageFeatures___hyg_373____rarg___closed__4);
l_Lean_Lsp_instToJsonDocumentSymbol___closed__1 = _init_l_Lean_Lsp_instToJsonDocumentSymbol___closed__1();
lean_mark_persistent(l_Lean_Lsp_instToJsonDocumentSymbol___closed__1);
l_Lean_Lsp_instToJsonDocumentSymbol = _init_l_Lean_Lsp_instToJsonDocumentSymbol();

504
stage0/stdlib/Lean/DeclarationRange.c generated
View file

File diff suppressed because it is too large Load diff

190
stage0/stdlib/Lean/Elab/Declaration.c generated
View file

@ -54,6 +54,7 @@ lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Declaration_0__Lean
lean_object* l___regBuiltin_Lean_Elab_Command_expandInitialize___closed__1;
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1142____closed__5;
lean_object* l_Lean_Elab_Command_elabDeclaration___closed__4;
lean_object* l_Lean_Syntax_getIdAt(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_commandElabAttribute;
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -180,6 +181,7 @@ lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1(lean_object*, lean_object
extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__2;
lean_object* l___regBuiltin_Lean_Elab_Command_expandMutualPreamble(lean_object*);
lean_object* l_Lean_Elab_Command_expandInitCmd___closed__10;
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
lean_object* l_Lean_Elab_Command_expandDeclNamespace_x3f_match__1(lean_object*);
extern lean_object* l_Lean_Elab_Command_checkValidCtorModifier___rarg___lambda__1___closed__3;
lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView_match__2___rarg(lean_object*, lean_object*);
@ -244,7 +246,6 @@ lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_Declar
lean_object* l_Lean_Elab_addAuxDeclarationRanges___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_expandInitCmd(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Command_expandMutualNamespace___spec__1___closed__1;
extern lean_object* l_Lean_Parser_Command_end___elambda__1___closed__2;
lean_object* l_Lean_Elab_Command_expandInitCmd___closed__4;
lean_object* l_Lean_Elab_Command_expandInitCmd___closed__11;
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_3377____closed__18;
@ -253,7 +254,6 @@ extern lean_object* l_Lean_Elab_macroAttribute;
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_3377____closed__30;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1142____closed__7;
extern lean_object* l_Lean_Parser_Command_end___elambda__1___closed__1;
lean_object* l_Lean_Elab_Command_elabMutual(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_initFn____x40_Lean_Compiler_InitAttr___hyg_551____closed__2;
lean_object* l___private_Lean_Elab_Declaration_0__Lean_Elab_Command_elabMutualInductive(lean_object*, lean_object*, lean_object*, lean_object*);
@ -333,6 +333,7 @@ lean_object* l_Lean_Elab_Command_elabDeclaration___closed__2;
extern lean_object* l_Lean_mkOptionalNode___closed__2;
lean_object* l_Lean_Elab_Command_elabAxiom___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*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_checkValidCtorModifier___at___private_Lean_Elab_Declaration_0__Lean_Elab_Command_inductiveSyntaxToView___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_leanPosToLspPos(lean_object*, lean_object*);
extern lean_object* l_Lean_expandExplicitBindersAux_loop___closed__4;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_12864____closed__5;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
@ -1718,83 +1719,112 @@ return x_2;
lean_object* l_Lean_Elab_getDeclarationRange___at_Lean_Elab_Command_elabAxiom___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6;
x_5 = l_Lean_Syntax_getPos(x_1);
x_6 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_ctor_get(x_2, 1);
x_6 = l_Lean_Syntax_getPos(x_1);
x_7 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_7 = lean_ctor_get(x_2, 1);
lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_8 = lean_unsigned_to_nat(0u);
x_9 = l_Lean_FileMap_toPosition(x_7, x_8);
x_9 = l_Lean_FileMap_toPosition(x_5, x_8);
lean_inc(x_9);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_4);
return x_11;
x_10 = l_Lean_FileMap_leanPosToLspPos(x_5, x_9);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
lean_inc(x_11);
lean_inc(x_9);
x_12 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_12, 0, x_9);
lean_ctor_set(x_12, 1, x_11);
lean_ctor_set(x_12, 2, x_9);
lean_ctor_set(x_12, 3, x_11);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_4);
return x_13;
}
else
{
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;
x_12 = lean_ctor_get(x_6, 0);
lean_inc(x_12);
lean_dec(x_6);
x_13 = lean_ctor_get(x_2, 1);
x_14 = lean_unsigned_to_nat(0u);
x_15 = l_Lean_FileMap_toPosition(x_13, x_14);
x_16 = l_Lean_FileMap_toPosition(x_13, x_12);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_15);
lean_ctor_set(x_17, 1, x_16);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_4);
return x_18;
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;
x_14 = lean_ctor_get(x_10, 1);
lean_inc(x_14);
lean_dec(x_10);
x_15 = lean_ctor_get(x_7, 0);
lean_inc(x_15);
lean_dec(x_7);
x_16 = l_Lean_FileMap_toPosition(x_5, x_15);
lean_inc(x_16);
x_17 = l_Lean_FileMap_leanPosToLspPos(x_5, x_16);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_19, 0, x_9);
lean_ctor_set(x_19, 1, x_14);
lean_ctor_set(x_19, 2, x_16);
lean_ctor_set(x_19, 3, x_18);
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_4);
return x_20;
}
}
else
{
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_19 = lean_ctor_get(x_5, 0);
lean_inc(x_19);
lean_dec(x_5);
x_20 = lean_ctor_get(x_2, 1);
x_21 = l_Lean_FileMap_toPosition(x_20, x_19);
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_6, 0);
lean_inc(x_21);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_21);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_4);
return x_23;
lean_dec(x_6);
x_22 = l_Lean_FileMap_toPosition(x_5, x_21);
lean_inc(x_22);
x_23 = l_Lean_FileMap_leanPosToLspPos(x_5, x_22);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_23, 1);
lean_inc(x_24);
lean_dec(x_23);
lean_inc(x_24);
lean_inc(x_22);
x_25 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_25, 0, x_22);
lean_ctor_set(x_25, 1, x_24);
lean_ctor_set(x_25, 2, x_22);
lean_ctor_set(x_25, 3, x_24);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_4);
return x_26;
}
else
{
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;
x_24 = lean_ctor_get(x_5, 0);
lean_inc(x_24);
lean_dec(x_5);
x_25 = lean_ctor_get(x_6, 0);
lean_inc(x_25);
lean_dec(x_6);
x_26 = lean_ctor_get(x_2, 1);
x_27 = l_Lean_FileMap_toPosition(x_26, x_24);
x_28 = l_Lean_FileMap_toPosition(x_26, x_25);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_4);
return x_30;
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;
x_27 = lean_ctor_get(x_23, 1);
lean_inc(x_27);
lean_dec(x_23);
x_28 = lean_ctor_get(x_7, 0);
lean_inc(x_28);
lean_dec(x_7);
x_29 = l_Lean_FileMap_toPosition(x_5, x_28);
lean_inc(x_29);
x_30 = l_Lean_FileMap_leanPosToLspPos(x_5, x_29);
x_31 = lean_ctor_get(x_30, 1);
lean_inc(x_31);
lean_dec(x_30);
x_32 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_32, 0, x_22);
lean_ctor_set(x_32, 1, x_27);
lean_ctor_set(x_32, 2, x_29);
lean_ctor_set(x_32, 3, x_31);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_4);
return x_33;
}
}
}
@ -4793,6 +4823,16 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Command_elabDeclaration___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_myMacro____x40_Init_NotationExtra___hyg_1142____closed__3;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Command_elabDeclaration(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -4964,7 +5004,7 @@ lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_51);
x_54 = lean_array_push(x_49, x_53);
x_55 = lean_array_push(x_54, x_38);
x_56 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_56 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
x_57 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_57, 0, x_41);
lean_ctor_set(x_57, 1, x_56);
@ -4975,7 +5015,7 @@ x_61 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_61, 0, x_60);
lean_ctor_set(x_61, 1, x_59);
x_62 = lean_array_push(x_58, x_61);
x_63 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_63 = l_Lean_Elab_Command_elabDeclaration___closed__4;
x_64 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_64, 0, x_63);
lean_ctor_set(x_64, 1, x_62);
@ -6269,7 +6309,7 @@ lean_ctor_set(x_36, 0, x_35);
lean_ctor_set(x_36, 1, x_34);
x_37 = lean_array_push(x_32, x_36);
x_38 = lean_array_push(x_37, x_26);
x_39 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_39 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
x_40 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_40, 0, x_29);
lean_ctor_set(x_40, 1, x_39);
@ -6280,7 +6320,7 @@ x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_43);
lean_ctor_set(x_44, 1, x_42);
x_45 = lean_array_push(x_41, x_44);
x_46 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_46 = l_Lean_Elab_Command_elabDeclaration___closed__4;
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_45);
@ -6314,7 +6354,7 @@ lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_56);
x_59 = lean_array_push(x_54, x_58);
x_60 = lean_array_push(x_59, x_26);
x_61 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_61 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
x_62 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_62, 0, x_50);
lean_ctor_set(x_62, 1, x_61);
@ -6325,7 +6365,7 @@ x_66 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_66, 0, x_65);
lean_ctor_set(x_66, 1, x_64);
x_67 = lean_array_push(x_63, x_66);
x_68 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_68 = l_Lean_Elab_Command_elabDeclaration___closed__4;
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_68);
lean_ctor_set(x_69, 1, x_67);
@ -6918,13 +6958,13 @@ if (x_29 == 0)
{
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; 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;
x_30 = lean_ctor_get(x_28, 0);
x_31 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_31 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
x_32 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
x_33 = lean_array_push(x_19, x_32);
x_34 = lean_array_push(x_33, x_21);
x_35 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_35 = l_Lean_Elab_Command_elabDeclaration___closed__4;
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_35);
lean_ctor_set(x_36, 1, x_34);
@ -6952,13 +6992,13 @@ x_46 = lean_ctor_get(x_28, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_28);
x_47 = l_Lean_Parser_Command_end___elambda__1___closed__1;
x_47 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_353____closed__1;
x_48 = lean_alloc_ctor(2, 2, 0);
lean_ctor_set(x_48, 0, x_45);
lean_ctor_set(x_48, 1, x_47);
x_49 = lean_array_push(x_19, x_48);
x_50 = lean_array_push(x_49, x_21);
x_51 = l_Lean_Parser_Command_end___elambda__1___closed__2;
x_51 = l_Lean_Elab_Command_elabDeclaration___closed__4;
x_52 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_50);
@ -8505,6 +8545,8 @@ l_Lean_Elab_Command_elabDeclaration___closed__2 = _init_l_Lean_Elab_Command_elab
lean_mark_persistent(l_Lean_Elab_Command_elabDeclaration___closed__2);
l_Lean_Elab_Command_elabDeclaration___closed__3 = _init_l_Lean_Elab_Command_elabDeclaration___closed__3();
lean_mark_persistent(l_Lean_Elab_Command_elabDeclaration___closed__3);
l_Lean_Elab_Command_elabDeclaration___closed__4 = _init_l_Lean_Elab_Command_elabDeclaration___closed__4();
lean_mark_persistent(l_Lean_Elab_Command_elabDeclaration___closed__4);
l___regBuiltin_Lean_Elab_Command_elabDeclaration___closed__1 = _init_l___regBuiltin_Lean_Elab_Command_elabDeclaration___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Elab_Command_elabDeclaration___closed__1);
res = l___regBuiltin_Lean_Elab_Command_elabDeclaration(lean_io_mk_world());

297
stage0/stdlib/Lean/Elab/DeclarationRange.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.DeclarationRange
// Imports: Init Lean.DeclarationRange Lean.Elab.Log
// Imports: Init Lean.DeclarationRange Lean.Elab.Log Lean.Data.Lsp.Utf16
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -16,178 +16,154 @@ extern "C" {
lean_object* l_Lean_addDeclarationRanges___rarg(lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Elab_addDeclarationRanges___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__3(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Command_example___elambda__1___closed__2;
lean_object* l_Lean_Elab_addDeclarationRanges___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange(lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_addAuxDeclarationRanges___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l_Lean_Elab_addAuxDeclarationRanges(lean_object*);
lean_object* l_Lean_Elab_addDeclarationRanges___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_NotationExtra___hyg_3377____closed__28;
lean_object* l_Lean_Elab_addDeclarationRanges(lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getKind(lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getPos(lean_object*);
extern lean_object* l_Lean_mkOptionalNode___closed__1;
lean_object* l_Lean_Elab_addAuxDeclarationRanges___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailPos(lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_leanPosToLspPos(lean_object*, lean_object*);
lean_object* l_Lean_Elab_getDeclarationSelectionRef(lean_object*);
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1(lean_object* x_1, lean_object* x_2) {
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_3 = lean_ctor_get(x_1, 0);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_ctor_get(x_3, 1);
lean_inc(x_4);
lean_dec(x_3);
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_FileMap_toPosition(x_2, x_5);
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Syntax_getPos(x_1);
x_5 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_4) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = lean_ctor_get(x_2, 0);
lean_inc(x_6);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_6);
x_8 = lean_apply_2(x_4, lean_box(0), x_7);
return x_8;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
lean_dec(x_2);
x_7 = lean_ctor_get(x_6, 1);
lean_inc(x_7);
lean_dec(x_6);
x_8 = lean_unsigned_to_nat(0u);
x_9 = l_Lean_FileMap_toPosition(x_3, x_8);
lean_inc(x_9);
x_10 = l_Lean_FileMap_leanPosToLspPos(x_3, x_9);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
lean_dec(x_4);
x_6 = lean_unsigned_to_nat(0u);
x_7 = l_Lean_FileMap_toPosition(x_3, x_6);
x_8 = l_Lean_FileMap_toPosition(x_3, x_2);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_apply_2(x_5, lean_box(0), x_9);
return x_10;
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_10, 1);
lean_inc(x_11);
lean_dec(x_10);
lean_inc(x_11);
lean_inc(x_9);
x_12 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_12, 0, x_9);
lean_ctor_set(x_12, 1, x_11);
lean_ctor_set(x_12, 2, x_9);
lean_ctor_set(x_12, 3, x_11);
x_13 = lean_apply_2(x_7, lean_box(0), x_12);
return x_13;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
else
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_4 = lean_ctor_get(x_1, 0);
lean_inc(x_4);
lean_dec(x_1);
x_5 = lean_ctor_get(x_4, 1);
lean_inc(x_5);
lean_dec(x_4);
x_6 = l_Lean_FileMap_toPosition(x_3, x_2);
lean_inc(x_6);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_6);
x_8 = lean_apply_2(x_5, lean_box(0), x_7);
return x_8;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_5 = lean_ctor_get(x_1, 0);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_ctor_get(x_5, 1);
lean_inc(x_6);
lean_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;
x_14 = lean_ctor_get(x_10, 1);
lean_inc(x_14);
lean_dec(x_10);
x_15 = lean_ctor_get(x_5, 0);
lean_inc(x_15);
lean_dec(x_5);
x_7 = l_Lean_FileMap_toPosition(x_4, x_2);
x_8 = l_Lean_FileMap_toPosition(x_4, x_3);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_apply_2(x_6, lean_box(0), x_9);
return x_10;
x_16 = l_Lean_FileMap_toPosition(x_3, x_15);
lean_inc(x_16);
x_17 = l_Lean_FileMap_leanPosToLspPos(x_3, x_16);
x_18 = lean_ctor_get(x_17, 1);
lean_inc(x_18);
lean_dec(x_17);
x_19 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_19, 0, x_9);
lean_ctor_set(x_19, 1, x_14);
lean_ctor_set(x_19, 2, x_16);
lean_ctor_set(x_19, 3, x_18);
x_20 = lean_apply_2(x_7, lean_box(0), x_19);
return x_20;
}
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_21 = lean_ctor_get(x_2, 0);
lean_inc(x_21);
lean_dec(x_2);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_ctor_get(x_4, 0);
lean_inc(x_23);
lean_dec(x_4);
x_24 = l_Lean_FileMap_toPosition(x_3, x_23);
lean_inc(x_24);
x_25 = l_Lean_FileMap_leanPosToLspPos(x_3, x_24);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_25, 1);
lean_inc(x_26);
lean_dec(x_25);
lean_inc(x_26);
lean_inc(x_24);
x_27 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_27, 0, x_24);
lean_ctor_set(x_27, 1, x_26);
lean_ctor_set(x_27, 2, x_24);
lean_ctor_set(x_27, 3, x_26);
x_28 = lean_apply_2(x_22, lean_box(0), x_27);
return x_28;
}
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;
x_29 = lean_ctor_get(x_25, 1);
lean_inc(x_29);
lean_dec(x_25);
x_30 = lean_ctor_get(x_5, 0);
lean_inc(x_30);
lean_dec(x_5);
x_31 = l_Lean_FileMap_toPosition(x_3, x_30);
lean_inc(x_31);
x_32 = l_Lean_FileMap_leanPosToLspPos(x_3, x_31);
x_33 = lean_ctor_get(x_32, 1);
lean_inc(x_33);
lean_dec(x_32);
x_34 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_34, 0, x_24);
lean_ctor_set(x_34, 1, x_29);
lean_ctor_set(x_34, 2, x_31);
lean_ctor_set(x_34, 3, x_33);
x_35 = lean_apply_2(x_22, lean_box(0), x_34);
return x_35;
}
}
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Syntax_getPos(x_3);
x_5 = l_Lean_Syntax_getTailPos(x_3);
if (lean_obj_tag(x_4) == 0)
{
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
x_7 = lean_alloc_closure((void*)(l_Lean_Elab_getDeclarationRange___rarg___lambda__1___boxed), 2, 1);
lean_closure_set(x_7, 0, x_1);
x_8 = lean_apply_4(x_6, lean_box(0), lean_box(0), x_2, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_1, 1);
lean_inc(x_9);
x_10 = lean_ctor_get(x_5, 0);
lean_inc(x_10);
lean_dec(x_5);
x_11 = lean_alloc_closure((void*)(l_Lean_Elab_getDeclarationRange___rarg___lambda__2___boxed), 3, 2);
lean_closure_set(x_11, 0, x_1);
lean_closure_set(x_11, 1, x_10);
x_12 = lean_apply_4(x_9, lean_box(0), lean_box(0), x_2, x_11);
return x_12;
}
}
else
{
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
x_13 = lean_ctor_get(x_1, 1);
lean_inc(x_13);
x_14 = lean_ctor_get(x_4, 0);
lean_inc(x_14);
lean_dec(x_4);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_getDeclarationRange___rarg___lambda__3___boxed), 3, 2);
lean_closure_set(x_15, 0, x_1);
lean_closure_set(x_15, 1, x_14);
x_16 = lean_apply_4(x_13, lean_box(0), lean_box(0), x_2, x_15);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_17 = lean_ctor_get(x_1, 1);
lean_inc(x_17);
x_18 = lean_ctor_get(x_4, 0);
lean_inc(x_18);
lean_dec(x_4);
x_19 = lean_ctor_get(x_5, 0);
lean_inc(x_19);
lean_dec(x_5);
x_20 = lean_alloc_closure((void*)(l_Lean_Elab_getDeclarationRange___rarg___lambda__4___boxed), 4, 3);
lean_closure_set(x_20, 0, x_1);
lean_closure_set(x_20, 1, x_18);
lean_closure_set(x_20, 2, x_19);
x_21 = lean_apply_4(x_17, lean_box(0), lean_box(0), x_2, x_20);
return x_21;
}
}
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
x_5 = lean_alloc_closure((void*)(l_Lean_Elab_getDeclarationRange___rarg___lambda__1___boxed), 3, 2);
lean_closure_set(x_5, 0, x_3);
lean_closure_set(x_5, 1, x_1);
x_6 = lean_apply_4(x_4, lean_box(0), lean_box(0), x_2, x_5);
return x_6;
}
}
lean_object* l_Lean_Elab_getDeclarationRange(lean_object* x_1) {
@ -198,42 +174,15 @@ x_2 = lean_alloc_closure((void*)(l_Lean_Elab_getDeclarationRange___rarg), 3, 0);
return x_2;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Elab_getDeclarationRange___rarg___lambda__1(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Elab_getDeclarationRange___rarg___lambda__2(x_1, x_2, x_3);
x_4 = l_Lean_Elab_getDeclarationRange___rarg___lambda__1(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Elab_getDeclarationRange___rarg___lambda__3(x_1, x_2, x_3);
lean_dec(x_3);
return x_4;
}
}
lean_object* l_Lean_Elab_getDeclarationRange___rarg___lambda__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Elab_getDeclarationRange___rarg___lambda__4(x_1, x_2, x_3, x_4);
lean_dec(x_4);
return x_5;
}
}
lean_object* l_Lean_Elab_getDeclarationSelectionRef(lean_object* x_1) {
_start:
{
@ -387,6 +336,7 @@ return x_2;
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_DeclarationRange(lean_object*);
lean_object* initialize_Lean_Elab_Log(lean_object*);
lean_object* initialize_Lean_Data_Lsp_Utf16(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_DeclarationRange(lean_object* w) {
lean_object * res;
@ -401,6 +351,9 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Log(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Data_Lsp_Utf16(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));
}
#ifdef __cplusplus

154
stage0/stdlib/Lean/Elab/LetRec.c generated
View file

@ -198,6 +198,7 @@ lean_object* l_Lean_Elab_Term_elabBinders___rarg(lean_object*, lean_object*, uin
lean_object* l_Lean_Syntax_getTailPos(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_registerLetRecsToLift___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_leanPosToLspPos(lean_object*, lean_object*);
extern lean_object* l_Lean_Meta_CheckAssignment_checkFVar___closed__2;
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*);
lean_object* l_List_foldr___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_registerLetRecsToLift___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -773,83 +774,112 @@ return x_13;
lean_object* l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_LetRec_0__Lean_Elab_Term_mkLetRecDeclView___spec__8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_Syntax_getPos(x_1);
x_10 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_2, 1);
x_10 = l_Lean_Syntax_getPos(x_1);
x_11 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_ctor_get(x_2, 1);
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(0u);
x_13 = l_Lean_FileMap_toPosition(x_11, x_12);
x_13 = l_Lean_FileMap_toPosition(x_9, x_12);
lean_inc(x_13);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
return x_15;
x_14 = l_Lean_FileMap_leanPosToLspPos(x_9, x_13);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
lean_inc(x_15);
lean_inc(x_13);
x_16 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_16, 0, x_13);
lean_ctor_set(x_16, 1, x_15);
lean_ctor_set(x_16, 2, x_13);
lean_ctor_set(x_16, 3, x_15);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_8);
return x_17;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_16 = lean_ctor_get(x_10, 0);
lean_inc(x_16);
lean_dec(x_10);
x_17 = lean_ctor_get(x_2, 1);
x_18 = lean_unsigned_to_nat(0u);
x_19 = l_Lean_FileMap_toPosition(x_17, x_18);
x_20 = l_Lean_FileMap_toPosition(x_17, x_16);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_8);
return x_22;
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_18 = lean_ctor_get(x_14, 1);
lean_inc(x_18);
lean_dec(x_14);
x_19 = lean_ctor_get(x_11, 0);
lean_inc(x_19);
lean_dec(x_11);
x_20 = l_Lean_FileMap_toPosition(x_9, x_19);
lean_inc(x_20);
x_21 = l_Lean_FileMap_leanPosToLspPos(x_9, x_20);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_23, 0, x_13);
lean_ctor_set(x_23, 1, x_18);
lean_ctor_set(x_23, 2, x_20);
lean_ctor_set(x_23, 3, x_22);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_8);
return x_24;
}
}
else
{
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = lean_ctor_get(x_9, 0);
lean_inc(x_23);
lean_dec(x_9);
x_24 = lean_ctor_get(x_2, 1);
x_25 = l_Lean_FileMap_toPosition(x_24, x_23);
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_10, 0);
lean_inc(x_25);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_25);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_8);
return x_27;
lean_dec(x_10);
x_26 = l_Lean_FileMap_toPosition(x_9, x_25);
lean_inc(x_26);
x_27 = l_Lean_FileMap_leanPosToLspPos(x_9, x_26);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
lean_dec(x_27);
lean_inc(x_28);
lean_inc(x_26);
x_29 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_29, 0, x_26);
lean_ctor_set(x_29, 1, x_28);
lean_ctor_set(x_29, 2, x_26);
lean_ctor_set(x_29, 3, x_28);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_8);
return x_30;
}
else
{
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;
x_28 = lean_ctor_get(x_9, 0);
lean_inc(x_28);
lean_dec(x_9);
x_29 = lean_ctor_get(x_10, 0);
lean_inc(x_29);
lean_dec(x_10);
x_30 = lean_ctor_get(x_2, 1);
x_31 = l_Lean_FileMap_toPosition(x_30, x_28);
x_32 = l_Lean_FileMap_toPosition(x_30, x_29);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_8);
return x_34;
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_31 = lean_ctor_get(x_27, 1);
lean_inc(x_31);
lean_dec(x_27);
x_32 = lean_ctor_get(x_11, 0);
lean_inc(x_32);
lean_dec(x_11);
x_33 = l_Lean_FileMap_toPosition(x_9, x_32);
lean_inc(x_33);
x_34 = l_Lean_FileMap_leanPosToLspPos(x_9, x_33);
x_35 = lean_ctor_get(x_34, 1);
lean_inc(x_35);
lean_dec(x_34);
x_36 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_36, 0, x_26);
lean_ctor_set(x_36, 1, x_31);
lean_ctor_set(x_36, 2, x_33);
lean_ctor_set(x_36, 3, x_35);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_8);
return x_37;
}
}
}

154
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -654,6 +654,7 @@ lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_Fix
lean_object* l_Lean_throwError___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__9___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_withUsed___rarg___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_Meta_withLCtx___at_Lean_Elab_Term_MutualClosure_main___spec__2(lean_object*);
lean_object* l_Lean_FileMap_leanPosToLspPos(lean_object*, lean_object*);
lean_object* l_Lean_Elab_instInhabitedDefViewElabHeader;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_expandWhereDeclsAsStructInst___spec__2___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalContextImp___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -4194,83 +4195,112 @@ return x_47;
lean_object* l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__12(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_Syntax_getPos(x_1);
x_10 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_2, 1);
x_10 = l_Lean_Syntax_getPos(x_1);
x_11 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_ctor_get(x_2, 1);
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(0u);
x_13 = l_Lean_FileMap_toPosition(x_11, x_12);
x_13 = l_Lean_FileMap_toPosition(x_9, x_12);
lean_inc(x_13);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
return x_15;
x_14 = l_Lean_FileMap_leanPosToLspPos(x_9, x_13);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
lean_inc(x_15);
lean_inc(x_13);
x_16 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_16, 0, x_13);
lean_ctor_set(x_16, 1, x_15);
lean_ctor_set(x_16, 2, x_13);
lean_ctor_set(x_16, 3, x_15);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_8);
return x_17;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_16 = lean_ctor_get(x_10, 0);
lean_inc(x_16);
lean_dec(x_10);
x_17 = lean_ctor_get(x_2, 1);
x_18 = lean_unsigned_to_nat(0u);
x_19 = l_Lean_FileMap_toPosition(x_17, x_18);
x_20 = l_Lean_FileMap_toPosition(x_17, x_16);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_8);
return x_22;
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_18 = lean_ctor_get(x_14, 1);
lean_inc(x_18);
lean_dec(x_14);
x_19 = lean_ctor_get(x_11, 0);
lean_inc(x_19);
lean_dec(x_11);
x_20 = l_Lean_FileMap_toPosition(x_9, x_19);
lean_inc(x_20);
x_21 = l_Lean_FileMap_leanPosToLspPos(x_9, x_20);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_23, 0, x_13);
lean_ctor_set(x_23, 1, x_18);
lean_ctor_set(x_23, 2, x_20);
lean_ctor_set(x_23, 3, x_22);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_8);
return x_24;
}
}
else
{
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = lean_ctor_get(x_9, 0);
lean_inc(x_23);
lean_dec(x_9);
x_24 = lean_ctor_get(x_2, 1);
x_25 = l_Lean_FileMap_toPosition(x_24, x_23);
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_10, 0);
lean_inc(x_25);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_25);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_8);
return x_27;
lean_dec(x_10);
x_26 = l_Lean_FileMap_toPosition(x_9, x_25);
lean_inc(x_26);
x_27 = l_Lean_FileMap_leanPosToLspPos(x_9, x_26);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
lean_dec(x_27);
lean_inc(x_28);
lean_inc(x_26);
x_29 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_29, 0, x_26);
lean_ctor_set(x_29, 1, x_28);
lean_ctor_set(x_29, 2, x_26);
lean_ctor_set(x_29, 3, x_28);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_8);
return x_30;
}
else
{
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;
x_28 = lean_ctor_get(x_9, 0);
lean_inc(x_28);
lean_dec(x_9);
x_29 = lean_ctor_get(x_10, 0);
lean_inc(x_29);
lean_dec(x_10);
x_30 = lean_ctor_get(x_2, 1);
x_31 = l_Lean_FileMap_toPosition(x_30, x_28);
x_32 = l_Lean_FileMap_toPosition(x_30, x_29);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_8);
return x_34;
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_31 = lean_ctor_get(x_27, 1);
lean_inc(x_31);
lean_dec(x_27);
x_32 = lean_ctor_get(x_11, 0);
lean_inc(x_32);
lean_dec(x_11);
x_33 = l_Lean_FileMap_toPosition(x_9, x_32);
lean_inc(x_33);
x_34 = l_Lean_FileMap_leanPosToLspPos(x_9, x_33);
x_35 = lean_ctor_get(x_34, 1);
lean_inc(x_35);
lean_dec(x_34);
x_36 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_36, 0, x_26);
lean_ctor_set(x_36, 1, x_31);
lean_ctor_set(x_36, 2, x_33);
lean_ctor_set(x_36, 3, x_35);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_8);
return x_37;
}
}
}

154
stage0/stdlib/Lean/Elab/Structure.c generated
View file

@ -600,6 +600,7 @@ lean_object* l_Array_foldlMUnsafe_fold___at___private_Lean_Elab_Structure_0__Lea
lean_object* l_Lean_throwError___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_withFields___spec__5___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn(lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandFields_match__2(lean_object*);
lean_object* l_Lean_FileMap_leanPosToLspPos(lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_levelMVarToParamFVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___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* l_Lean_throwErrorAt___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -2925,83 +2926,112 @@ return x_13;
lean_object* l_Lean_Elab_getDeclarationRange___at___private_Lean_Elab_Structure_0__Lean_Elab_Command_expandCtor___spec__18(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_Syntax_getPos(x_1);
x_10 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_2, 1);
x_10 = l_Lean_Syntax_getPos(x_1);
x_11 = l_Lean_Syntax_getTailPos(x_1);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_11 = lean_ctor_get(x_2, 1);
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(0u);
x_13 = l_Lean_FileMap_toPosition(x_11, x_12);
x_13 = l_Lean_FileMap_toPosition(x_9, x_12);
lean_inc(x_13);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
return x_15;
x_14 = l_Lean_FileMap_leanPosToLspPos(x_9, x_13);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_14, 1);
lean_inc(x_15);
lean_dec(x_14);
lean_inc(x_15);
lean_inc(x_13);
x_16 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_16, 0, x_13);
lean_ctor_set(x_16, 1, x_15);
lean_ctor_set(x_16, 2, x_13);
lean_ctor_set(x_16, 3, x_15);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_8);
return x_17;
}
else
{
lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_16 = lean_ctor_get(x_10, 0);
lean_inc(x_16);
lean_dec(x_10);
x_17 = lean_ctor_get(x_2, 1);
x_18 = lean_unsigned_to_nat(0u);
x_19 = l_Lean_FileMap_toPosition(x_17, x_18);
x_20 = l_Lean_FileMap_toPosition(x_17, x_16);
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_21);
lean_ctor_set(x_22, 1, x_8);
return x_22;
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
x_18 = lean_ctor_get(x_14, 1);
lean_inc(x_18);
lean_dec(x_14);
x_19 = lean_ctor_get(x_11, 0);
lean_inc(x_19);
lean_dec(x_11);
x_20 = l_Lean_FileMap_toPosition(x_9, x_19);
lean_inc(x_20);
x_21 = l_Lean_FileMap_leanPosToLspPos(x_9, x_20);
x_22 = lean_ctor_get(x_21, 1);
lean_inc(x_22);
lean_dec(x_21);
x_23 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_23, 0, x_13);
lean_ctor_set(x_23, 1, x_18);
lean_ctor_set(x_23, 2, x_20);
lean_ctor_set(x_23, 3, x_22);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_8);
return x_24;
}
}
else
{
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_23 = lean_ctor_get(x_9, 0);
lean_inc(x_23);
lean_dec(x_9);
x_24 = lean_ctor_get(x_2, 1);
x_25 = l_Lean_FileMap_toPosition(x_24, x_23);
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_10, 0);
lean_inc(x_25);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_25);
x_27 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_8);
return x_27;
lean_dec(x_10);
x_26 = l_Lean_FileMap_toPosition(x_9, x_25);
lean_inc(x_26);
x_27 = l_Lean_FileMap_leanPosToLspPos(x_9, x_26);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
lean_dec(x_27);
lean_inc(x_28);
lean_inc(x_26);
x_29 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_29, 0, x_26);
lean_ctor_set(x_29, 1, x_28);
lean_ctor_set(x_29, 2, x_26);
lean_ctor_set(x_29, 3, x_28);
x_30 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_30, 0, x_29);
lean_ctor_set(x_30, 1, x_8);
return x_30;
}
else
{
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;
x_28 = lean_ctor_get(x_9, 0);
lean_inc(x_28);
lean_dec(x_9);
x_29 = lean_ctor_get(x_10, 0);
lean_inc(x_29);
lean_dec(x_10);
x_30 = lean_ctor_get(x_2, 1);
x_31 = l_Lean_FileMap_toPosition(x_30, x_28);
x_32 = l_Lean_FileMap_toPosition(x_30, x_29);
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_31);
lean_ctor_set(x_33, 1, x_32);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_8);
return x_34;
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_31 = lean_ctor_get(x_27, 1);
lean_inc(x_31);
lean_dec(x_27);
x_32 = lean_ctor_get(x_11, 0);
lean_inc(x_32);
lean_dec(x_11);
x_33 = l_Lean_FileMap_toPosition(x_9, x_32);
lean_inc(x_33);
x_34 = l_Lean_FileMap_leanPosToLspPos(x_9, x_33);
x_35 = lean_ctor_get(x_34, 1);
lean_inc(x_35);
lean_dec(x_34);
x_36 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_36, 0, x_26);
lean_ctor_set(x_36, 1, x_31);
lean_ctor_set(x_36, 2, x_33);
lean_ctor_set(x_36, 3, x_35);
x_37 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_8);
return x_37;
}
}
}

1586
stage0/stdlib/Lean/Parser/Transform.c generated Normal file
View file

File diff suppressed because it is too large Load diff

60
stage0/stdlib/Lean/Server/FileSource.c generated
View file

@ -13,11 +13,16 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Lsp_DefinitionParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_DocumentSymbolParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_TextDocumentIdentifier_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_TypeDefinitionParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_DidCloseTextDocumentParams_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_DidChangeTextDocumentParams_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_DeclarationParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_DeclarationParams_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_WaitForDiagnosticsParam_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_TypeDefinitionParams_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_TextDocumentItem_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_DidOpenTextDocumentParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_HoverParams_hasFileSource___boxed(lean_object*);
@ -28,6 +33,7 @@ lean_object* l_Lean_Lsp_Location_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_TextDocumentEdit_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_TextDocumentPositionParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_WaitForDiagnosticsParam_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_DefinitionParams_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_DidChangeTextDocumentParams_hasFileSource___boxed(lean_object*);
lean_object* l_Lean_Lsp_HoverParams_hasFileSource(lean_object*);
lean_object* l_Lean_Lsp_TextDocumentIdentifier_hasFileSource(lean_object*);
@ -215,6 +221,60 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_DeclarationParams_hasFileSource(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
return x_2;
}
}
lean_object* l_Lean_Lsp_DeclarationParams_hasFileSource___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_DeclarationParams_hasFileSource(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_DefinitionParams_hasFileSource(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
return x_2;
}
}
lean_object* l_Lean_Lsp_DefinitionParams_hasFileSource___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_DefinitionParams_hasFileSource(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_TypeDefinitionParams_hasFileSource(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
return x_2;
}
}
lean_object* l_Lean_Lsp_TypeDefinitionParams_hasFileSource___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_TypeDefinitionParams_hasFileSource(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_WaitForDiagnosticsParam_hasFileSource(lean_object* x_1) {
_start:
{

15450
stage0/stdlib/Lean/Server/FileWorker.c generated
View file

File diff suppressed because it is too large Load diff

989
stage0/stdlib/Lean/Server/InfoUtils.c generated
View file

File diff suppressed because it is too large Load diff

2889
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

File diff suppressed because it is too large Load diff

1232
stage0/stdlib/Lean/Util/Path.c generated
View file

File diff suppressed because it is too large Load diff