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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-26 17:49:32 -08:00
parent bbafd80322
commit 3e241b21da
23 changed files with 11302 additions and 10004 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

202
stage0/src/Lean/Data/Lsp/Basic.lean generated
View file

@ -20,16 +20,7 @@ open Json
structure CancelParams where
id : JsonRpc.RequestID
deriving Inhabited, BEq
instance CancelParams.hasFromJson : FromJson CancelParams :=
⟨fun j => do
let id ← j.getObjValAs? JsonRpc.RequestID "id"
pure ⟨id⟩⟩
instance CancelParams.hasToJson : ToJson CancelParams :=
⟨fun o => mkObj $
⟨"id", toJson o.id⟩ :: []⟩
deriving Inhabited, BEq, ToJson, FromJson
abbrev DocumentUri := String
@ -40,17 +31,7 @@ offsets. For diagnostics, one-based `Lean.Position`s are used internally.
structure Position where
line : Nat
character : Nat
deriving Inhabited, BEq
instance : FromJson Position := ⟨fun j => do
let line ← j.getObjValAs? Nat "line"
let character ← j.getObjValAs? Nat "character"
pure ⟨line, character⟩⟩
instance : ToJson Position := ⟨fun o =>
mkObj [
⟨"line", o.line⟩,
⟨"character", o.character⟩]⟩
deriving Inhabited, BEq, ToJson, FromJson
instance : ToString Position := ⟨fun p =>
"(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩
@ -58,51 +39,19 @@ instance : ToString Position := ⟨fun p =>
structure Range where
start : Position
«end» : Position
deriving Inhabited, BEq
instance : FromJson Range := ⟨fun j => do
let start ← j.getObjValAs? Position "start"
let «end» ← j.getObjValAs? Position "end"
pure ⟨start, «end»⟩⟩
instance : ToJson Range := ⟨fun o =>
mkObj [
⟨"start", toJson o.start⟩,
⟨"end", toJson o.«end»⟩]⟩
deriving Inhabited, BEq, ToJson, FromJson
structure Location where
uri : DocumentUri
range : Range
deriving Inhabited, BEq
instance : FromJson Location := ⟨fun j => do
let uri ← j.getObjValAs? DocumentUri "uri"
let range ← j.getObjValAs? Range "range"
pure ⟨uri, range⟩⟩
instance : ToJson Location := ⟨fun o =>
mkObj [
⟨"uri", toJson o.uri⟩,
⟨"range", toJson o.range⟩]⟩
deriving Inhabited, BEq, ToJson, FromJson
structure LocationLink where
originSelectionRange? : Option Range
targetUri : DocumentUri
targetRange : Range
targetSelectionRange : Range
instance : FromJson LocationLink := ⟨fun j => do
let originSelectionRange? := j.getObjValAs? Range "originSelectionRange"
let targetUri ← j.getObjValAs? DocumentUri "targetUri"
let targetRange ← j.getObjValAs? Range "targetRange"
let targetSelectionRange ← j.getObjValAs? Range "targetSelectionRange"
pure ⟨originSelectionRange?, targetUri, targetRange, targetSelectionRange⟩⟩
instance : ToJson LocationLink := ⟨fun o => mkObj $
opt "originSelectionRange" o.originSelectionRange? ++ [
⟨"targetUri", toJson o.targetUri⟩,
⟨"targetRange", toJson o.targetRange⟩,
⟨"targetSelectionRange", toJson o.targetSelectionRange⟩]⟩
deriving ToJson, FromJson
-- NOTE: Diagnostic defined in Diagnostics.lean
@ -112,31 +61,12 @@ structure Command where
title : String
command : String
arguments? : Option (Array Json) := none
instance : FromJson Command := ⟨fun j => do
let title ← j.getObjValAs? String "title"
let command ← j.getObjValAs? String "command"
let arguments? := j.getObjValAs? (Array Json) "arguments"
pure ⟨title, command, arguments?⟩⟩
instance : ToJson Command := ⟨fun o => mkObj $
opt "arguments" o.arguments? ++ [
⟨"title", o.title⟩,
⟨"command", o.command⟩]⟩
deriving ToJson, FromJson
structure TextEdit where
range : Range
newText : String
instance : FromJson TextEdit := ⟨fun j => do
let range ← j.getObjValAs? Range "range"
let newText ← j.getObjValAs? String "newText"
pure ⟨range, newText⟩⟩
instance : ToJson TextEdit := ⟨fun o =>
mkObj [
⟨"range", toJson o.range⟩,
⟨"newText", o.newText⟩]⟩
deriving ToJson, FromJson
def TextEditBatch := Array TextEdit
@ -148,39 +78,17 @@ instance : ToJson TextEditBatch :=
structure TextDocumentIdentifier where
uri : DocumentUri
instance : FromJson TextDocumentIdentifier := ⟨fun j =>
TextDocumentIdentifier.mk <$> j.getObjValAs? DocumentUri "uri"⟩
instance : ToJson TextDocumentIdentifier :=
⟨fun o => mkObj [⟨"uri", o.uri⟩]⟩
deriving ToJson, FromJson
structure VersionedTextDocumentIdentifier where
uri : DocumentUri
version? : Option Nat := none
instance : FromJson VersionedTextDocumentIdentifier := ⟨fun j => do
let uri ← j.getObjValAs? DocumentUri "uri"
let version? := j.getObjValAs? Nat "version"
pure ⟨uri, version?⟩⟩
instance : ToJson VersionedTextDocumentIdentifier := ⟨fun o => mkObj $
opt "version" o.version? ++
[⟨"uri", o.uri⟩]⟩
deriving ToJson, FromJson
structure TextDocumentEdit where
textDocument : VersionedTextDocumentIdentifier
edits : TextEditBatch
instance : FromJson TextDocumentEdit := ⟨fun j => do
let textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument"
let edits ← j.getObjValAs? TextEditBatch "edits"
pure ⟨textDocument, edits⟩⟩
instance : ToJson TextDocumentEdit := ⟨fun o =>
mkObj [
⟨"textDocument", toJson o.textDocument⟩,
⟨"edits", toJson o.edits⟩]⟩
deriving ToJson, FromJson
-- TODO(Marc): missing:
-- File Resource Changes, WorkspaceEdit
@ -192,50 +100,18 @@ structure TextDocumentItem where
languageId : String
version : Nat
text : String
instance : FromJson TextDocumentItem := ⟨fun j => do
let uri ← j.getObjValAs? DocumentUri "uri"
let languageId ← j.getObjValAs? String "languageId"
let version ← j.getObjValAs? Nat "version"
let text ← j.getObjValAs? String "text"
pure ⟨uri, languageId, version, text⟩⟩
instance : ToJson TextDocumentItem := ⟨fun o =>
mkObj [
⟨"uri", o.uri⟩,
⟨"languageId", o.languageId⟩,
⟨"version", o.version⟩,
⟨"text", o.text⟩]⟩
deriving ToJson, FromJson
structure TextDocumentPositionParams where
textDocument : TextDocumentIdentifier
position : Position
instance : FromJson TextDocumentPositionParams := ⟨fun j => do
let textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument"
let position ← j.getObjValAs? Position "position"
pure ⟨textDocument, position⟩⟩
instance : ToJson TextDocumentPositionParams := ⟨fun o =>
mkObj [
⟨"textDocument", toJson o.textDocument⟩,
⟨"position", toJson o.position⟩]⟩
deriving ToJson, FromJson
structure DocumentFilter where
language? : Option String := none
scheme? : Option String := none
pattern? : Option String := none
instance : FromJson DocumentFilter := ⟨fun j => do
let language? := j.getObjValAs? String "language"
let scheme? := j.getObjValAs? String "scheme"
let pattern? := j.getObjValAs? String "pattern"
pure ⟨language?, scheme?, pattern?⟩⟩
instance : ToJson DocumentFilter := ⟨fun o => mkObj $
opt "language" o.language? ++
opt "scheme" o.scheme? ++
opt "pattern" o.pattern?⟩
deriving ToJson, FromJson
def DocumentSelector := Array DocumentFilter
@ -247,21 +123,11 @@ instance : ToJson DocumentSelector :=
structure StaticRegistrationOptions where
id? : Option String := none
instance : FromJson StaticRegistrationOptions :=
⟨fun j => some ⟨j.getObjValAs? String "id"⟩⟩
instance : ToJson StaticRegistrationOptions :=
⟨fun o => mkObj $ opt "id" o.id?⟩
deriving ToJson, FromJson
structure TextDocumentRegistrationOptions where
documentSelector? : Option DocumentSelector := none
instance : FromJson TextDocumentRegistrationOptions :=
⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩
instance : ToJson TextDocumentRegistrationOptions :=
⟨fun o => mkObj $ opt "documentSelector" o.documentSelector?⟩
deriving ToJson, FromJson
inductive MarkupKind where
| plaintext | markdown
@ -278,57 +144,29 @@ instance : ToJson MarkupKind := ⟨fun
structure MarkupContent where
kind : MarkupKind
value : String
instance : FromJson MarkupContent := ⟨fun j => do
let kind ← j.getObjValAs? MarkupKind "kind"
let value ← j.getObjValAs? String "value"
pure ⟨kind, value⟩⟩
instance : ToJson MarkupContent := ⟨fun o =>
mkObj [
⟨"kind", toJson o.kind⟩,
⟨"value", o.value⟩]⟩
deriving ToJson, FromJson
structure ProgressParams (α : Type) where
token : String -- do we need `integer`?
value : α
instance [ToJson α] : ToJson (ProgressParams α) := ⟨fun o =>
mkObj [
⟨"token", o.token⟩,
⟨"value", toJson o.value⟩]⟩
deriving ToJson
structure WorkDoneProgressReport where
kind := "report"
message? : Option String := none
cancellable := false
percentage? : Option Nat := none
instance : ToJson WorkDoneProgressReport := ⟨fun o =>
mkObj [
⟨"kind", o.kind⟩,
⟨"message", toJson o.message?⟩,
⟨"cancellable", o.cancellable⟩,
⟨"percentage", toJson o.percentage?⟩]⟩
deriving ToJson
structure WorkDoneProgressBegin extends WorkDoneProgressReport where
kind := "begin"
title : String
instance : ToJson WorkDoneProgressBegin := ⟨fun o =>
mkObj [
⟨"kind", o.kind⟩,
⟨"title", o.title⟩,
⟨"message", toJson o.message?⟩]⟩
deriving ToJson
structure WorkDoneProgressEnd where
kind := "end"
message? : Option String := none
instance : ToJson WorkDoneProgressEnd := ⟨fun o =>
mkObj [
⟨"kind", o.kind⟩,
⟨"message", toJson o.message?⟩]⟩
deriving ToJson
-- TODO(Marc): missing:
-- WorkDoneProgressOptions, PartialResultParams

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

@ -30,16 +30,7 @@ instance ClientCapabilities.hasToJson : ToJson ClientCapabilities :=
structure ServerCapabilities where
textDocumentSync? : Option TextDocumentSyncOptions := none
hoverProvider : Bool := false
instance : FromJson ServerCapabilities :=
⟨fun j => do
let textDocumentSync? := j.getObjValAs? TextDocumentSyncOptions "textDocumentSync"
let hoverProvider ← j.getObjValAs? Bool "hoverProvider"
pure ⟨textDocumentSync?, hoverProvider⟩⟩
instance : ToJson ServerCapabilities := ⟨fun o => mkObj $
opt "textDocumentSync" o.textDocumentSync? ++
[⟨"hoverProvider", o.hoverProvider⟩]⟩
deriving ToJson, FromJson
end Lsp
end Lean

46
stage0/src/Lean/Data/Lsp/Diagnostics.lean generated
View file

@ -68,17 +68,7 @@ instance : ToJson DiagnosticTag := ⟨fun
structure DiagnosticRelatedInformation where
location : Location
message : String
deriving Inhabited, BEq
instance : FromJson DiagnosticRelatedInformation := ⟨fun j => do
let location ← j.getObjValAs? Location "location"
let message ← j.getObjValAs? String "message"
pure ⟨location, message⟩⟩
instance : ToJson DiagnosticRelatedInformation := ⟨fun o =>
mkObj [
⟨"location", toJson o.location⟩,
⟨"message", o.message⟩]⟩
deriving Inhabited, BEq, ToJson, FromJson
structure Diagnostic where
range : Range
@ -88,43 +78,13 @@ structure Diagnostic where
message : String
tags? : Option (Array DiagnosticTag) := none
relatedInformation? : Option (Array DiagnosticRelatedInformation) := none
deriving Inhabited, BEq
instance : FromJson Diagnostic := ⟨fun j => do
let range ← j.getObjValAs? Range "range"
let severity? := j.getObjValAs? DiagnosticSeverity "severity"
let code? := j.getObjValAs? DiagnosticCode "code"
let source? := j.getObjValAs? String "source"
let message ← j.getObjValAs? String "message"
let tags? := j.getObjValAs? (Array DiagnosticTag) "tags"
let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation"
pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩
instance : ToJson Diagnostic := ⟨fun o => mkObj $
opt "severity" o.severity? ++
opt "code" o.code? ++
opt "source" o.source? ++
opt "tags" o.tags? ++
opt "relatedInformation" o.relatedInformation? ++ [
⟨"range", toJson o.range⟩,
⟨"message", o.message⟩]⟩
deriving Inhabited, BEq, ToJson, FromJson
structure PublishDiagnosticsParams where
uri : DocumentUri
version? : Option Int := none
diagnostics: Array Diagnostic
deriving Inhabited, BEq
instance : FromJson PublishDiagnosticsParams := ⟨fun j => do
let uri ← j.getObjValAs? DocumentUri "uri"
let version? := j.getObjValAs? Int "version"
let diagnostics ← j.getObjValAs? (Array Diagnostic) "diagnostics"
pure ⟨uri, version?, diagnostics⟩⟩
instance : ToJson PublishDiagnosticsParams := ⟨fun o => mkObj $
opt "version" o.version? ++ [
⟨"uri", toJson o.uri⟩,
⟨"diagnostics", toJson o.diagnostics⟩]⟩
deriving Inhabited, BEq, ToJson, FromJson
/-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
def msgToDiagnostic (text : FileMap) (m : Message) : IO Diagnostic := do

11
stage0/src/Lean/Data/Lsp/Extra.lean generated
View file

@ -22,14 +22,7 @@ open Json
structure WaitForDiagnosticsParam where
uri : DocumentUri
instance : FromJson WaitForDiagnosticsParam :=
⟨fun j => do
let id ← j.getObjValAs? DocumentUri "uri"
pure ⟨id⟩⟩
instance : ToJson WaitForDiagnosticsParam :=
⟨fun o => mkObj [⟨"uri", toJson o.uri⟩]⟩
deriving ToJson, FromJson
structure WaitForDiagnostics
@ -39,4 +32,4 @@ instance : FromJson WaitForDiagnostics :=
instance : ToJson WaitForDiagnostics :=
⟨fun o => mkObj []⟩
end Lean.Lsp
end Lean.Lsp

10
stage0/src/Lean/Data/Lsp/Hover.lean generated
View file

@ -19,15 +19,7 @@ structure Hover where
but they are deprecated, so maybe can get away without. -/
contents : MarkupContent
range? : Option Range := none
instance : FromJson Hover := ⟨fun j => do
let contents ← j.getObjValAs? MarkupContent "contents"
let range? := j.getObjValAs? Range "range"
pure ⟨contents, range?⟩⟩
instance : ToJson Hover := ⟨fun o => mkObj $
⟨"contents", toJson o.contents⟩ ::
opt "range" o.range?⟩
deriving ToJson, FromJson
structure HoverParams extends TextDocumentPositionParams

43
stage0/src/Lean/Data/Lsp/InitShutdown.lean generated
View file

@ -19,14 +19,7 @@ open Json
structure ClientInfo where
name : String
version? : Option String := none
instance : FromJson ClientInfo := ⟨fun j => do
let name ← j.getObjValAs? String "name"
let version? := j.getObjValAs? String "version"
pure ⟨name, version?⟩⟩
instance ClientInfo.hasToJson : ToJson ClientInfo :=
⟨fun o => mkObj $ ⟨"name", o.name⟩ :: opt "version" o.version?⟩
deriving ToJson, FromJson
inductive Trace where
| off
@ -57,6 +50,7 @@ structure InitializeParams where
/- If omitted, we default to off. -/
trace : Trace := Trace.off
workspaceFolders? : Option (Array WorkspaceFolder) := none
deriving ToJson
instance : FromJson InitializeParams := ⟨fun j => do
/- Many of these params can be null instead of not present.
@ -75,16 +69,6 @@ instance : FromJson InitializeParams := ⟨fun j => do
let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
pure ⟨processId?, clientInfo?, rootUri?, initializationOptions?, capabilities, trace, workspaceFolders?⟩⟩
instance InitializeParams.hasToJson : ToJson InitializeParams :=
⟨fun o => mkObj $
opt "processId" o.processId? ++
opt "clientInfo" o.clientInfo? ++
opt "rootUri" o.rootUri? ++
opt "initializationOptions" o.initializationOptions? ++
[⟨"capabilities", toJson o.capabilities⟩] ++
[⟨"trace", toJson o.trace⟩] ++
opt "workspaceFolders" o.workspaceFolders?⟩
inductive InitializedParams where
| mk
@ -97,31 +81,12 @@ instance : ToJson InitializedParams :=
structure ServerInfo where
name : String
version? : Option String := none
instance : FromJson ServerInfo :=
⟨fun j => do
let name ← j.getObjValAs? String "name"
let version? := j.getObjValAs? String "version"
pure ⟨name, version?⟩⟩
instance : ToJson ServerInfo := ⟨fun o => mkObj $
⟨"name", o.name⟩ ::
opt "version" o.version?⟩
deriving ToJson, FromJson
structure InitializeResult where
capabilities : ServerCapabilities
serverInfo? : Option ServerInfo := none
instance : FromJson InitializeResult :=
⟨fun j => do
let capabilities ← j.getObjValAs? ServerCapabilities "capabilities"
let serverInfo? := j.getObjValAs? ServerInfo "serverInfo"
pure ⟨capabilities, serverInfo?⟩⟩
instance : ToJson InitializeResult := ⟨fun o =>
mkObj $
⟨"capabilities", toJson o.capabilities⟩ ::
opt "serverInfo" o.serverInfo?⟩
deriving ToJson, FromJson
end Lsp
end Lean

56
stage0/src/Lean/Data/Lsp/TextSync.lean generated
View file

@ -33,21 +33,12 @@ instance : ToJson TextDocumentSyncKind := ⟨fun
structure DidOpenTextDocumentParams where
textDocument : TextDocumentItem
instance : FromJson DidOpenTextDocumentParams := ⟨fun j =>
DidOpenTextDocumentParams.mk <$> j.getObjValAs? TextDocumentItem "textDocument"⟩
instance : ToJson DidOpenTextDocumentParams := ⟨fun o =>
mkObj $ [⟨"textDocument", toJson o.textDocument⟩]⟩
deriving ToJson, FromJson
structure TextDocumentChangeRegistrationOptions where
documentSelector? : Option DocumentSelector := none
syncKind : TextDocumentSyncKind
instance : FromJson TextDocumentChangeRegistrationOptions := ⟨fun j => do
let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector"
let syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind"
pure ⟨documentSelector?, syncKind⟩⟩
deriving FromJson
inductive TextDocumentContentChangeEvent where
-- omitted: deprecated rangeLength
@ -69,14 +60,7 @@ instance TextDocumentContentChangeEvent.hasToJson : ToJson TextDocumentContentCh
structure DidChangeTextDocumentParams where
textDocument : VersionedTextDocumentIdentifier
contentChanges : Array TextDocumentContentChangeEvent
instance : FromJson DidChangeTextDocumentParams := ⟨fun j => do
let textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument"
let contentChanges ← j.getObjValAs? (Array TextDocumentContentChangeEvent) "contentChanges"
pure ⟨textDocument, contentChanges⟩⟩
instance DidChangeTextDocumentParams.hasToJson : ToJson DidChangeTextDocumentParams :=
⟨fun o => mkObj $ [⟨"textDocument", toJson o.textDocument⟩, ⟨"contentChanges", toJson o.contentChanges⟩]⟩
deriving ToJson, FromJson
-- TODO: missing:
-- WillSaveTextDocumentParams, TextDocumentSaveReason,
@ -84,23 +68,11 @@ instance DidChangeTextDocumentParams.hasToJson : ToJson DidChangeTextDocumentPar
structure SaveOptions where
includeText : Bool
instance : FromJson SaveOptions :=
⟨fun j => do
let includeText ← j.getObjValAs? Bool "includeText"
pure ⟨includeText⟩⟩
instance : ToJson SaveOptions := ⟨fun o =>
mkObj $ [⟨"includeText", o.includeText⟩]⟩
deriving ToJson, FromJson
structure DidCloseTextDocumentParams where
textDocument : TextDocumentIdentifier
instance : FromJson DidCloseTextDocumentParams := ⟨fun j =>
DidCloseTextDocumentParams.mk <$> j.getObjValAs? TextDocumentIdentifier "textDocument"⟩
instance DidCloseTextDocumentParams.hasToJson : ToJson DidCloseTextDocumentParams :=
⟨fun o => mkObj $ [⟨"textDocument", toJson o.textDocument⟩]⟩
deriving ToJson, FromJson
-- TODO: TextDocumentSyncClientCapabilities
@ -111,23 +83,7 @@ structure TextDocumentSyncOptions where
willSave : Bool
willSaveWaitUntil : Bool
save? : Option SaveOptions := none
instance : FromJson TextDocumentSyncOptions :=
⟨fun j => do
let openClose ← j.getObjValAs? Bool "openClose"
let change ← j.getObjValAs? TextDocumentSyncKind "change"
let willSave ← j.getObjValAs? Bool "willSave"
let willSaveUntil ← j.getObjValAs? Bool "willSaveWaitUntil"
let save? := j.getObjValAs? SaveOptions "save"
pure ⟨openClose, change, willSave, willSaveUntil, save?⟩⟩
instance : ToJson TextDocumentSyncOptions := ⟨fun o =>
mkObj $
opt "save" o.save? ++ [
⟨"openClose", toJson o.openClose⟩,
⟨"change", toJson o.change⟩,
⟨"willSave", toJson o.willSave⟩,
⟨"willSaveWaitUntil", toJson o.willSaveWaitUntil⟩]⟩
deriving ToJson, FromJson
end Lsp
end Lean

10
stage0/src/Lean/Data/Lsp/Workspace.lean generated
View file

@ -15,16 +15,8 @@ open Json
structure WorkspaceFolder where
uri : DocumentUri
name : String
deriving ToJson, FromJson
instance : FromJson WorkspaceFolder := ⟨fun j => do
let uri ← j.getObjValAs? DocumentUri "uri"
let name ← j.getObjValAs? String "name"
pure ⟨uri, name⟩⟩
instance : ToJson WorkspaceFolder := ⟨fun o =>
mkObj [
⟨"uri", toJson o.uri⟩,
⟨"name", toJson o.name⟩]⟩
-- TODO(WN):
-- WorkspaceFoldersServerCapabilities,
-- DidChangeWorkspaceFoldersParams,

4
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -57,7 +57,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
getAntiquotTerm stx
else if isTokenAntiquot stx && !isEscapedAntiquot stx then
match stx[0] with
| Syntax.atom _ val => `(Syntax.atom $(getAntiquotTerm stx) $(quote val))
| Syntax.atom _ val => `(Syntax.atom (Option.getD (getHeadInfo $(getAntiquotTerm stx)) info) $(quote val))
| _ => throwErrorAt stx "expected token"
else if isAntiquotSuffixSplice stx && !isEscapedAntiquot stx then
-- splices must occur in a `many` node
@ -226,7 +226,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
-- We assume that atoms are uniquely determined by the node kind and never have to be checked
unconditionally pure
else if quoted.isTokenAntiquot then
unconditionally (`(let $(quoted.getAntiquotTerm) := discr.getHeadInfo.get!; $(·)))
unconditionally (`(let $(quoted.getAntiquotTerm) := discr; $(·)))
else if isAntiquot quoted && !isEscapedAntiquot quoted then
-- quotation contains a single antiquotation
let k := antiquotKind? quoted |>.get!

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

5285
stage0/stdlib/Lean/Data/Lsp/Basic.c generated
View file

File diff suppressed because it is too large Load diff

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

@ -13,39 +13,33 @@
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__3;
lean_object* l_List_append___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Tactic_change___closed__1;
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities(lean_object*);
extern lean_object* l_Lean_instFromJsonOption___rarg___closed__1;
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____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_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonServerCapabilities___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentSyncOptions___spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_419_(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*);
lean_object* l_Lean_Lsp_instToJsonServerCapabilities___boxed(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonServerCapabilities___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonServerCapabilities___spec__1___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__3;
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentChangeRegistrationOptions___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instToJsonServerCapabilities;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_335____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61_(lean_object*);
lean_object* l_Lean_Lsp_instToJsonServerCapabilities___closed__1;
lean_object* l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default;
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities___closed__1;
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities___boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__1;
lean_object* l_Lean_Json_getObjValD(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonSaveOptions___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonTextDocumentSyncOptions___spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2;
lean_object* l_Lean_Json_mkObj(lean_object*);
extern lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__2;
extern lean_object* l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__1;
extern lean_object* l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__1;
extern lean_object* l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__4;
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonServerCapabilities___spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__2;
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities___closed__2;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_463_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonClientCapabilities___closed__1;
lean_object* l_Lean_Lsp_instFromJsonClientCapabilities___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_61____spec__1___boxed(lean_object*, lean_object*);
static lean_object* _init_l_Lean_Lsp_instFromJsonClientCapabilities___closed__1() {
_start:
{
@ -115,141 +109,7 @@ x_1 = 0;
return x_1;
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonServerCapabilities___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = l_Lean_Json_getObjValD(x_1, x_2);
x_4 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__1;
x_5 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonSaveOptions___spec__1(x_3, x_4);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6;
lean_dec(x_3);
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_5, 0);
lean_inc(x_7);
lean_dec(x_5);
x_8 = l_Lean_Parser_Tactic_change___closed__1;
x_9 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentChangeRegistrationOptions___spec__1(x_3, x_8);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10;
lean_dec(x_7);
lean_dec(x_3);
x_10 = lean_box(0);
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_9, 0);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__2;
x_13 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonSaveOptions___spec__1(x_3, x_12);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14;
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_3);
x_14 = lean_box(0);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_15 = lean_ctor_get(x_13, 0);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__3;
x_17 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonSaveOptions___spec__1(x_3, x_16);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18;
lean_dec(x_15);
lean_dec(x_11);
lean_dec(x_7);
lean_dec(x_3);
x_18 = lean_box(0);
return x_18;
}
else
{
uint8_t x_19;
x_19 = !lean_is_exclusive(x_17);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24; uint8_t x_25; uint8_t x_26; uint8_t x_27;
x_20 = lean_ctor_get(x_17, 0);
x_21 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__4;
x_22 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentSyncOptions___spec__1(x_3, x_21);
lean_dec(x_3);
x_23 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_23, 0, x_22);
x_24 = lean_unbox(x_7);
lean_dec(x_7);
lean_ctor_set_uint8(x_23, sizeof(void*)*1, x_24);
x_25 = lean_unbox(x_11);
lean_dec(x_11);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 1, x_25);
x_26 = lean_unbox(x_15);
lean_dec(x_15);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 2, x_26);
x_27 = lean_unbox(x_20);
lean_dec(x_20);
lean_ctor_set_uint8(x_23, sizeof(void*)*1 + 3, x_27);
lean_ctor_set(x_17, 0, x_23);
return x_17;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; uint8_t x_32; uint8_t x_33; uint8_t x_34; uint8_t x_35; lean_object* x_36;
x_28 = lean_ctor_get(x_17, 0);
lean_inc(x_28);
lean_dec(x_17);
x_29 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__4;
x_30 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentSyncOptions___spec__1(x_3, x_29);
lean_dec(x_3);
x_31 = lean_alloc_ctor(0, 1, 4);
lean_ctor_set(x_31, 0, x_30);
x_32 = lean_unbox(x_7);
lean_dec(x_7);
lean_ctor_set_uint8(x_31, sizeof(void*)*1, x_32);
x_33 = lean_unbox(x_11);
lean_dec(x_11);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 1, x_33);
x_34 = lean_unbox(x_15);
lean_dec(x_15);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 2, x_34);
x_35 = lean_unbox(x_28);
lean_dec(x_28);
lean_ctor_set_uint8(x_31, sizeof(void*)*1 + 3, x_35);
x_36 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_36, 0, x_31);
return x_36;
}
}
}
}
}
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonServerCapabilities___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("textDocumentSync");
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonServerCapabilities___closed__2() {
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__1() {
_start:
{
lean_object* x_1;
@ -257,18 +117,113 @@ x_1 = lean_mk_string("hoverProvider");
return x_1;
}
}
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities(lean_object* x_1) {
static lean_object* _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2() {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Lsp_instFromJsonServerCapabilities___closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonServerCapabilities___spec__1(x_1, x_2);
x_4 = l_Lean_Lsp_instFromJsonServerCapabilities___closed__2;
x_5 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonSaveOptions___spec__1(x_1, x_4);
lean_object* x_1;
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_35____closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2;
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*1);
x_4 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_4, 0, x_3);
x_5 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
x_7 = lean_box(0);
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_6);
lean_ctor_set(x_8, 1, x_7);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__3;
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_8);
x_11 = l_Lean_Json_mkObj(x_10);
return x_11;
}
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;
x_12 = lean_ctor_get(x_2, 0);
x_13 = l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_419_(x_12);
x_14 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2;
x_15 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_8);
x_17 = l_Lean_Json_mkObj(x_16);
return x_17;
}
}
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____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_35_(x_1);
lean_dec(x_1);
return x_2;
}
}
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_35____boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonServerCapabilities() {
_start:
{
lean_object* x_1;
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_61____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_getObjValD(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
x_4 = l_Lean_instFromJsonOption___rarg___closed__1;
return x_4;
}
else
{
lean_object* x_5;
x_5 = l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonTextDocumentSyncOptions____x40_Lean_Data_Lsp_TextSync___hyg_463_(x_3);
lean_dec(x_3);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6;
lean_dec(x_3);
x_6 = lean_box(0);
return x_6;
}
@ -278,211 +233,124 @@ uint8_t x_7;
x_7 = !lean_is_exclusive(x_5);
if (x_7 == 0)
{
lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_8 = lean_ctor_get(x_5, 0);
x_9 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_9, 0, x_3);
x_10 = lean_unbox(x_8);
lean_dec(x_8);
lean_ctor_set_uint8(x_9, sizeof(void*)*1, x_10);
lean_ctor_set(x_5, 0, x_9);
return x_5;
lean_object* x_8;
x_8 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_8, 0, x_5);
return x_8;
}
else
{
lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_11 = lean_ctor_get(x_5, 0);
lean_inc(x_11);
lean_object* x_9; lean_object* x_10; lean_object* x_11;
x_9 = lean_ctor_get(x_5, 0);
lean_inc(x_9);
lean_dec(x_5);
x_12 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_12, 0, x_3);
x_13 = lean_unbox(x_11);
lean_dec(x_11);
lean_ctor_set_uint8(x_12, sizeof(void*)*1, x_13);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_12);
return x_14;
x_10 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
return x_11;
}
}
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonServerCapabilities___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
}
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61_(lean_object* x_1) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonServerCapabilities___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Lsp_instFromJsonServerCapabilities___boxed(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_35____closed__2;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonServerCapabilities(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonServerCapabilities___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_box(0);
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
lean_object* x_4;
x_4 = lean_box(0);
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_1);
lean_ctor_set(x_5, 1, x_4);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_3);
return x_6;
return x_4;
}
else
{
lean_object* x_7; uint8_t x_8; uint8_t x_9; uint8_t 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_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get_uint8(x_7, sizeof(void*)*1);
x_9 = lean_ctor_get_uint8(x_7, sizeof(void*)*1 + 1);
x_10 = lean_ctor_get_uint8(x_7, sizeof(void*)*1 + 2);
x_11 = lean_ctor_get_uint8(x_7, sizeof(void*)*1 + 3);
x_12 = lean_ctor_get(x_7, 0);
x_13 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__4;
x_14 = l_Lean_Json_opt___at_Lean_Lsp_instToJsonTextDocumentSyncOptions___spec__1(x_13, x_12);
x_15 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_15, 0, x_8);
x_16 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__1;
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_18, 0, x_10);
x_19 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__2;
x_20 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_20, 0, x_19);
lean_ctor_set(x_20, 1, x_18);
x_21 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_21, 0, x_11);
x_22 = l_Lean_Lsp_instFromJsonTextDocumentSyncOptions___closed__3;
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
x_24 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_3);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_20);
lean_ctor_set(x_25, 1, x_24);
switch (x_9) {
case 0:
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_35____closed__1;
x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonSaveOptions____x40_Lean_Data_Lsp_TextSync___hyg_335____spec__1(x_1, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_26 = l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__1;
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_25);
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_17);
lean_ctor_set(x_28, 1, x_27);
x_29 = l_List_append___rarg(x_14, x_28);
x_30 = l_Lean_Json_mkObj(x_29);
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_1);
lean_ctor_set(x_31, 1, x_30);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_3);
return x_32;
lean_object* x_8;
lean_dec(x_5);
x_8 = lean_box(0);
return x_8;
}
case 1:
else
{
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;
x_33 = l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__2;
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_25);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_17);
lean_ctor_set(x_35, 1, x_34);
x_36 = l_List_append___rarg(x_14, x_35);
x_37 = l_Lean_Json_mkObj(x_36);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_1);
lean_ctor_set(x_38, 1, x_37);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_3);
return x_39;
}
default:
uint8_t x_9;
x_9 = !lean_is_exclusive(x_7);
if (x_9 == 0)
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
x_40 = l_Lean_Lsp_instToJsonTextDocumentSyncOptions___closed__3;
x_41 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_25);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_17);
lean_ctor_set(x_42, 1, x_41);
x_43 = l_List_append___rarg(x_14, x_42);
x_44 = l_Lean_Json_mkObj(x_43);
x_45 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_45, 0, x_1);
lean_ctor_set(x_45, 1, x_44);
x_46 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_46, 0, x_45);
lean_ctor_set(x_46, 1, x_3);
return x_46;
lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_10 = lean_ctor_get(x_7, 0);
x_11 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_11, 0, x_5);
x_12 = lean_unbox(x_10);
lean_dec(x_10);
lean_ctor_set_uint8(x_11, sizeof(void*)*1, x_12);
lean_ctor_set(x_7, 0, x_11);
return x_7;
}
}
}
}
}
lean_object* l_Lean_Lsp_instToJsonServerCapabilities(lean_object* x_1) {
_start:
else
{
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; lean_object* x_11; lean_object* x_12;
x_2 = lean_ctor_get(x_1, 0);
x_3 = l_Lean_Lsp_instFromJsonServerCapabilities___closed__1;
x_4 = l_Lean_Json_opt___at_Lean_Lsp_instToJsonServerCapabilities___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_Lean_Lsp_instFromJsonServerCapabilities___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);
x_9 = lean_box(0);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = l_List_append___rarg(x_4, x_10);
x_12 = l_Lean_Json_mkObj(x_11);
return x_12;
lean_object* x_13; lean_object* x_14; uint8_t x_15; lean_object* x_16;
x_13 = lean_ctor_get(x_7, 0);
lean_inc(x_13);
lean_dec(x_7);
x_14 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_14, 0, x_5);
x_15 = lean_unbox(x_13);
lean_dec(x_13);
lean_ctor_set_uint8(x_14, sizeof(void*)*1, x_15);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_14);
return x_16;
}
}
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonServerCapabilities___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_61____spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_opt___at_Lean_Lsp_instToJsonServerCapabilities___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_61____spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_Lean_Lsp_instToJsonServerCapabilities___boxed(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instToJsonServerCapabilities(x_1);
x_2 = l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_fromJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_61_(x_1);
lean_dec(x_1);
return x_2;
}
}
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_61____boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonServerCapabilities() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Lsp_instFromJsonServerCapabilities___closed__1;
return x_1;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Data_JsonRpc(lean_object*);
lean_object* initialize_Lean_Data_Lsp_TextSync(lean_object*);
@ -507,10 +375,20 @@ lean_mark_persistent(l_Lean_Lsp_ClientCapabilities_hasToJson___closed__1);
l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default = _init_l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default();
lean_mark_persistent(l_Lean_Lsp_ServerCapabilities_textDocumentSync_x3f___default);
l_Lean_Lsp_ServerCapabilities_hoverProvider___default = _init_l_Lean_Lsp_ServerCapabilities_hoverProvider___default();
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__1 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__1);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__2);
l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__3 = _init_l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__3();
lean_mark_persistent(l___private_Lean_Data_Lsp_Capabilities_0__Lean_Lsp_toJsonServerCapabilities____x40_Lean_Data_Lsp_Capabilities___hyg_35____closed__3);
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();
lean_mark_persistent(l_Lean_Lsp_instToJsonServerCapabilities);
l_Lean_Lsp_instFromJsonServerCapabilities___closed__1 = _init_l_Lean_Lsp_instFromJsonServerCapabilities___closed__1();
lean_mark_persistent(l_Lean_Lsp_instFromJsonServerCapabilities___closed__1);
l_Lean_Lsp_instFromJsonServerCapabilities___closed__2 = _init_l_Lean_Lsp_instFromJsonServerCapabilities___closed__2();
lean_mark_persistent(l_Lean_Lsp_instFromJsonServerCapabilities___closed__2);
l_Lean_Lsp_instFromJsonServerCapabilities = _init_l_Lean_Lsp_instFromJsonServerCapabilities();
lean_mark_persistent(l_Lean_Lsp_instFromJsonServerCapabilities);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

2936
stage0/stdlib/Lean/Data/Lsp/Diagnostics.c generated
View file

File diff suppressed because it is too large Load diff

92
stage0/stdlib/Lean/Data/Lsp/Extra.c generated
View file

@ -13,24 +13,62 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__1(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__1;
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnosticsParam___closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_484____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnostics(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnosticsParam(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnosticsParam;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_27_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnostics___closed__1;
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam;
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnostics___boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnostics___closed__1;
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnostics(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_27____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_7_(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnostics___boxed(lean_object*);
lean_object* l_Lean_Json_mkObj(lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonLocation___closed__1;
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___boxed(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam(lean_object* x_1) {
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___closed__1;
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_7_(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;
x_2 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__1;
x_4 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
x_5 = lean_box(0);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);
x_7 = l_Lean_Json_mkObj(x_6);
return x_7;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonWaitForDiagnosticsParam___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_toJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_7_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonWaitForDiagnosticsParam() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Lsp_instToJsonWaitForDiagnosticsParam___closed__1;
return x_1;
}
}
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_27_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Lsp_instFromJsonLocation___closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__1(x_1, x_2);
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_484____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
@ -58,31 +96,29 @@ return x_7;
}
}
}
lean_object* l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___boxed(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_27____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam(x_1);
x_2 = l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_27_(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instToJsonWaitForDiagnosticsParam(lean_object* x_1) {
static lean_object* _init_l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___closed__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;
x_2 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_2, 0, x_1);
x_3 = l_Lean_Lsp_instFromJsonLocation___closed__1;
x_4 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
x_5 = lean_box(0);
x_6 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_6, 0, x_4);
lean_ctor_set(x_6, 1, x_5);
x_7 = l_Lean_Json_mkObj(x_6);
return x_7;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonWaitForDiagnosticsParam____x40_Lean_Data_Lsp_Extra___hyg_27____boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonWaitForDiagnostics___closed__1() {
@ -159,6 +195,14 @@ lean_dec_ref(res);
res = initialize_Lean_Data_Lsp_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Lsp_instToJsonWaitForDiagnosticsParam___closed__1 = _init_l_Lean_Lsp_instToJsonWaitForDiagnosticsParam___closed__1();
lean_mark_persistent(l_Lean_Lsp_instToJsonWaitForDiagnosticsParam___closed__1);
l_Lean_Lsp_instToJsonWaitForDiagnosticsParam = _init_l_Lean_Lsp_instToJsonWaitForDiagnosticsParam();
lean_mark_persistent(l_Lean_Lsp_instToJsonWaitForDiagnosticsParam);
l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___closed__1 = _init_l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___closed__1();
lean_mark_persistent(l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam___closed__1);
l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam = _init_l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam();
lean_mark_persistent(l_Lean_Lsp_instFromJsonWaitForDiagnosticsParam);
l_Lean_Lsp_instFromJsonWaitForDiagnostics___closed__1 = _init_l_Lean_Lsp_instFromJsonWaitForDiagnostics___closed__1();
lean_mark_persistent(l_Lean_Lsp_instFromJsonWaitForDiagnostics___closed__1);
l_Lean_Lsp_instToJsonWaitForDiagnostics___closed__1 = _init_l_Lean_Lsp_instToJsonWaitForDiagnostics___closed__1();

438
stage0/stdlib/Lean/Data/Lsp/Hover.c generated
View file

@ -14,34 +14,30 @@
extern "C" {
#endif
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_1109_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonHoverParams___boxed(lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonPosition___closed__2;
extern lean_object* l_Lean_Lsp_instFromJsonPosition___closed__1;
extern lean_object* l_Lean_Lsp_instToJsonMarkupContent___closed__2;
extern lean_object* l_Lean_Lsp_instToJsonMarkupContent___closed__1;
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1;
lean_object* l_Lean_Lsp_instToJsonHover___closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____spec__1___boxed(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__2;
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__2;
lean_object* l_Lean_Lsp_Hover_range_x3f___default;
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__2(lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonTextDocumentPositionParams___closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentPositionParams___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonHover___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonRange___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Json_opt___at_Lean_Lsp_instToJsonLocationLink___spec__1(lean_object*, lean_object*);
lean_object* l_Lean_JsonNumber_fromNat(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11_(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_565____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1083_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1438_(lean_object*);
lean_object* l_Lean_Json_getObjValD(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instFromJsonHoverParams(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonMarkupContent___spec__1(lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonMarkupContent___closed__1;
extern lean_object* l_Lean_Lsp_instFromJsonMarkupContent___closed__2;
lean_object* l_Lean_Lsp_instToJsonHover(lean_object*);
lean_object* l_Lean_Lsp_instToJsonHover;
lean_object* l_Lean_Json_mkObj(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonHover___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Lsp_instFromJsonHover(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1412_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__3;
lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_328_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonHover;
lean_object* l_Lean_Lsp_instFromJsonHover___closed__1;
extern lean_object* l_Lean_Lsp_instFromJsonLocation___closed__1;
extern lean_object* l_Lean_Lsp_instFromJsonLocation___closed__2;
lean_object* l_Lean_Lsp_instFromJsonHover___boxed(lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonTextDocumentEdit___closed__1;
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_JsonRpc_instFromJsonMessage___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____spec__1(lean_object*, lean_object*);
static lean_object* _init_l_Lean_Lsp_Hover_range_x3f___default() {
_start:
{
@ -50,72 +46,7 @@ x_1 = lean_box(0);
return x_1;
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonHover___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = l_Lean_Json_getObjValD(x_1, x_2);
x_4 = l_Lean_Lsp_instFromJsonMarkupContent___closed__1;
x_5 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonMarkupContent___spec__1(x_3, x_4);
if (lean_obj_tag(x_5) == 0)
{
lean_object* x_6;
lean_dec(x_3);
x_6 = lean_box(0);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_5, 0);
lean_inc(x_7);
lean_dec(x_5);
x_8 = l_Lean_Lsp_instFromJsonMarkupContent___closed__2;
x_9 = l_Lean_Json_getObjValAs_x3f___at_Lean_JsonRpc_instFromJsonMessage___spec__2(x_3, x_8);
lean_dec(x_3);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10;
lean_dec(x_7);
x_10 = lean_box(0);
return x_10;
}
else
{
uint8_t x_11;
x_11 = !lean_is_exclusive(x_9);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; uint8_t x_14;
x_12 = lean_ctor_get(x_9, 0);
x_13 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_13, 0, x_12);
x_14 = lean_unbox(x_7);
lean_dec(x_7);
lean_ctor_set_uint8(x_13, sizeof(void*)*1, x_14);
lean_ctor_set(x_9, 0, x_13);
return x_9;
}
else
{
lean_object* x_15; lean_object* x_16; uint8_t x_17; lean_object* x_18;
x_15 = lean_ctor_get(x_9, 0);
lean_inc(x_15);
lean_dec(x_9);
x_16 = lean_alloc_ctor(0, 1, 1);
lean_ctor_set(x_16, 0, x_15);
x_17 = lean_unbox(x_7);
lean_dec(x_7);
lean_ctor_set_uint8(x_16, sizeof(void*)*1, x_17);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_16);
return x_18;
}
}
}
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonHover___closed__1() {
static lean_object* _init_l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1() {
_start:
{
lean_object* x_1;
@ -123,140 +54,110 @@ x_1 = lean_mk_string("contents");
return x_1;
}
}
lean_object* l_Lean_Lsp_instFromJsonHover(lean_object* x_1) {
static lean_object* _init_l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__2() {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Lsp_instFromJsonHover___closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonHover___spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
x_4 = lean_box(0);
return x_4;
}
else
{
uint8_t x_5;
x_5 = !lean_is_exclusive(x_3);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_ctor_get(x_3, 0);
x_7 = l_Lean_Lsp_instFromJsonLocation___closed__2;
x_8 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__2(x_1, x_7);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_6);
lean_ctor_set(x_9, 1, x_8);
lean_ctor_set(x_3, 0, x_9);
return x_3;
}
else
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_10 = lean_ctor_get(x_3, 0);
lean_inc(x_10);
lean_dec(x_3);
x_11 = l_Lean_Lsp_instFromJsonLocation___closed__2;
x_12 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__2(x_1, x_11);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_10);
lean_ctor_set(x_13, 1, x_12);
x_14 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_14, 0, x_13);
return x_14;
}
}
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonHover___spec__1___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonHover___spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__2;
x_2 = lean_box(0);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* l_Lean_Lsp_instFromJsonHover___boxed(lean_object* x_1) {
static lean_object* _init_l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__3() {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonHover(x_1);
lean_dec(x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__2;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Lsp_instToJsonHover(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t 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_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get_uint8(x_2, sizeof(void*)*1);
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
x_3 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1412_(x_2);
lean_dec(x_2);
x_5 = lean_alloc_ctor(3, 1, 0);
x_4 = l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1;
x_5 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = l_Lean_Lsp_instFromJsonMarkupContent___closed__2;
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_ctor_get(x_1, 1);
lean_inc(x_10);
lean_ctor_set(x_5, 1, x_3);
x_6 = lean_ctor_get(x_1, 1);
lean_inc(x_6);
lean_dec(x_1);
x_11 = l_Lean_Lsp_instFromJsonLocation___closed__2;
x_12 = l_Lean_Json_opt___at_Lean_Lsp_instToJsonLocationLink___spec__1(x_11, x_10);
if (x_3 == 0)
if (lean_obj_tag(x_6) == 0)
{
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;
x_13 = l_Lean_Lsp_instToJsonMarkupContent___closed__1;
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_9);
x_15 = l_Lean_Json_mkObj(x_14);
x_16 = l_Lean_Lsp_instFromJsonHover___closed__1;
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_16);
lean_ctor_set(x_17, 1, x_15);
x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_12);
x_19 = l_Lean_Json_mkObj(x_18);
return x_19;
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__3;
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_5);
lean_ctor_set(x_8, 1, x_7);
x_9 = l_Lean_Json_mkObj(x_8);
return x_9;
}
else
{
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;
x_20 = l_Lean_Lsp_instToJsonMarkupContent___closed__2;
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_9);
x_22 = l_Lean_Json_mkObj(x_21);
x_23 = l_Lean_Lsp_instFromJsonHover___closed__1;
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_12);
x_26 = l_Lean_Json_mkObj(x_25);
return x_26;
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;
x_10 = lean_ctor_get(x_6, 0);
lean_inc(x_10);
lean_dec(x_6);
x_11 = lean_box(0);
x_12 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_328_(x_10);
x_13 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__2;
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_11);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_5);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_Lean_Json_mkObj(x_16);
return x_17;
}
}
}
lean_object* l_Lean_Lsp_instFromJsonHoverParams(lean_object* x_1) {
static lean_object* _init_l_Lean_Lsp_instToJsonHover___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonHover() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Lsp_instToJsonHover___closed__1;
return x_1;
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____spec__1(lean_object* x_1, lean_object* x_2) {
_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_Basic_0__Lean_Lsp_fromJsonMarkupContent____x40_Lean_Data_Lsp_Basic___hyg_1438_(x_3);
lean_dec(x_3);
return x_4;
}
}
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Lsp_instFromJsonTextDocumentEdit___closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonTextDocumentPositionParams___spec__1(x_1, x_2);
x_2 = l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
@ -269,8 +170,8 @@ 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_Lean_Lsp_instFromJsonTextDocumentPositionParams___closed__1;
x_7 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonRange___spec__1(x_1, x_6);
x_6 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__2;
x_7 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocationLink____x40_Lean_Data_Lsp_Basic___hyg_565____spec__1(x_1, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8;
@ -309,6 +210,73 @@ return x_14;
}
}
}
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____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_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____spec__1(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37_(x_1);
lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonHover___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_fromJsonHover____x40_Lean_Data_Lsp_Hover___hyg_37____boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instFromJsonHover() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Lsp_instFromJsonHover___closed__1;
return x_1;
}
}
lean_object* l_Lean_Lsp_instFromJsonHoverParams(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_1109_(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_instFromJsonHoverParams___boxed(lean_object* x_1) {
_start:
{
@ -321,65 +289,9 @@ return x_2;
lean_object* l_Lean_Lsp_instToJsonHoverParams(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; 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;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_4, 0, x_2);
x_5 = l_Lean_Lsp_instFromJsonLocation___closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
x_7 = lean_box(0);
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_6);
lean_ctor_set(x_8, 1, x_7);
x_9 = l_Lean_Json_mkObj(x_8);
x_10 = l_Lean_Lsp_instFromJsonTextDocumentEdit___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);
x_12 = lean_ctor_get(x_3, 0);
lean_inc(x_12);
x_13 = l_Lean_JsonNumber_fromNat(x_12);
x_14 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_14, 0, x_13);
x_15 = l_Lean_Lsp_instFromJsonPosition___closed__1;
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_14);
x_17 = lean_ctor_get(x_3, 1);
lean_inc(x_17);
lean_dec(x_3);
x_18 = l_Lean_JsonNumber_fromNat(x_17);
x_19 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_19, 0, x_18);
x_20 = l_Lean_Lsp_instFromJsonPosition___closed__2;
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_7);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_16);
lean_ctor_set(x_23, 1, x_22);
x_24 = l_Lean_Json_mkObj(x_23);
x_25 = l_Lean_Lsp_instFromJsonTextDocumentPositionParams___closed__1;
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_24);
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_26);
lean_ctor_set(x_27, 1, x_7);
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_11);
lean_ctor_set(x_28, 1, x_27);
x_29 = l_Lean_Json_mkObj(x_28);
return x_29;
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonTextDocumentPositionParams____x40_Lean_Data_Lsp_Basic___hyg_1083_(x_1);
return x_2;
}
}
lean_object* initialize_Init(lean_object*);
@ -401,8 +313,20 @@ if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Lsp_Hover_range_x3f___default = _init_l_Lean_Lsp_Hover_range_x3f___default();
lean_mark_persistent(l_Lean_Lsp_Hover_range_x3f___default);
l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1 = _init_l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__1);
l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__2 = _init_l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__2();
lean_mark_persistent(l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__2);
l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__3 = _init_l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__3();
lean_mark_persistent(l___private_Lean_Data_Lsp_Hover_0__Lean_Lsp_toJsonHover____x40_Lean_Data_Lsp_Hover___hyg_11____closed__3);
l_Lean_Lsp_instToJsonHover___closed__1 = _init_l_Lean_Lsp_instToJsonHover___closed__1();
lean_mark_persistent(l_Lean_Lsp_instToJsonHover___closed__1);
l_Lean_Lsp_instToJsonHover = _init_l_Lean_Lsp_instToJsonHover();
lean_mark_persistent(l_Lean_Lsp_instToJsonHover);
l_Lean_Lsp_instFromJsonHover___closed__1 = _init_l_Lean_Lsp_instFromJsonHover___closed__1();
lean_mark_persistent(l_Lean_Lsp_instFromJsonHover___closed__1);
l_Lean_Lsp_instFromJsonHover = _init_l_Lean_Lsp_instFromJsonHover();
lean_mark_persistent(l_Lean_Lsp_instFromJsonHover);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

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

File diff suppressed because it is too large Load diff

855
stage0/stdlib/Lean/Data/Lsp/Ipc.c generated
View file

File diff suppressed because it is too large Load diff

1849
stage0/stdlib/Lean/Data/Lsp/TextSync.c generated
View file

File diff suppressed because it is too large Load diff

134
stage0/stdlib/Lean/Data/Lsp/Workspace.c generated
View file

@ -13,16 +13,20 @@
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Lean_Lsp_instFromJsonWorkspaceFolder(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__1(lean_object*, lean_object*);
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__1;
lean_object* l_Lean_Lsp_instFromJsonWorkspaceFolder;
lean_object* l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_484____spec__1(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9_(lean_object*);
lean_object* l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1;
lean_object* l_Lean_Lsp_instFromJsonWorkspaceFolder___boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWorkspaceFolder___boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWorkspaceFolder___closed__1;
lean_object* l_Lean_Json_mkObj(lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonLocation___closed__1;
lean_object* l_Lean_Lsp_instToJsonWorkspaceFolder(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_fromJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_35____boxed(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1;
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_fromJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_35_(lean_object*);
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____boxed(lean_object*);
lean_object* l_Lean_Lsp_instToJsonWorkspaceFolder;
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_JsonRpc_instFromJsonMessage___spec__2(lean_object*, lean_object*);
static lean_object* _init_l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1() {
static lean_object* _init_l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1() {
_start:
{
lean_object* x_1;
@ -30,12 +34,68 @@ x_1 = lean_mk_string("name");
return x_1;
}
}
lean_object* l_Lean_Lsp_instFromJsonWorkspaceFolder(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9_(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; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_4 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_4, 0, x_2);
x_5 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
lean_inc(x_3);
x_7 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_7, 0, x_3);
x_8 = l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1;
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_7);
x_10 = lean_box(0);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_6);
lean_ctor_set(x_12, 1, x_11);
x_13 = l_Lean_Json_mkObj(x_12);
return x_13;
}
}
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9_(x_1);
lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonWorkspaceFolder___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____boxed), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Lsp_instToJsonWorkspaceFolder() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Lsp_instToJsonWorkspaceFolder___closed__1;
return x_1;
}
}
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_fromJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_35_(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Lean_Lsp_instFromJsonLocation___closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonLocation___spec__1(x_1, x_2);
x_2 = l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_458____closed__1;
x_3 = l_Lean_Json_getObjValAs_x3f___at___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_fromJsonLocation____x40_Lean_Data_Lsp_Basic___hyg_484____spec__1(x_1, x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4;
@ -48,7 +108,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_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1;
x_6 = l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1;
x_7 = l_Lean_Json_getObjValAs_x3f___at_Lean_JsonRpc_instFromJsonMessage___spec__2(x_1, x_6);
if (lean_obj_tag(x_7) == 0)
{
@ -88,53 +148,29 @@ return x_14;
}
}
}
lean_object* l_Lean_Lsp_instFromJsonWorkspaceFolder___boxed(lean_object* x_1) {
lean_object* l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_fromJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_35____boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instFromJsonWorkspaceFolder(x_1);
x_2 = l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_fromJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_35_(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Lean_Lsp_instToJsonWorkspaceFolder(lean_object* x_1) {
static lean_object* _init_l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__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; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_2 = lean_ctor_get(x_1, 0);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_2);
x_4 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_4, 0, x_2);
x_5 = l_Lean_Lsp_instFromJsonLocation___closed__1;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_5);
lean_ctor_set(x_6, 1, x_4);
lean_inc(x_3);
x_7 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_7, 0, x_3);
x_8 = l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1;
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_7);
x_10 = lean_box(0);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_6);
lean_ctor_set(x_12, 1, x_11);
x_13 = l_Lean_Json_mkObj(x_12);
return x_13;
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_fromJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_35____boxed), 1, 0);
return x_1;
}
}
lean_object* l_Lean_Lsp_instToJsonWorkspaceFolder___boxed(lean_object* x_1) {
static lean_object* _init_l_Lean_Lsp_instFromJsonWorkspaceFolder() {
_start:
{
lean_object* x_2;
x_2 = l_Lean_Lsp_instToJsonWorkspaceFolder(x_1);
lean_dec(x_1);
return x_2;
lean_object* x_1;
x_1 = l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1;
return x_1;
}
}
lean_object* initialize_Init(lean_object*);
@ -154,8 +190,16 @@ lean_dec_ref(res);
res = initialize_Lean_Data_Json(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1 = _init_l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1();
lean_mark_persistent(l___private_Lean_Data_Lsp_Workspace_0__Lean_Lsp_toJsonWorkspaceFolder____x40_Lean_Data_Lsp_Workspace___hyg_9____closed__1);
l_Lean_Lsp_instToJsonWorkspaceFolder___closed__1 = _init_l_Lean_Lsp_instToJsonWorkspaceFolder___closed__1();
lean_mark_persistent(l_Lean_Lsp_instToJsonWorkspaceFolder___closed__1);
l_Lean_Lsp_instToJsonWorkspaceFolder = _init_l_Lean_Lsp_instToJsonWorkspaceFolder();
lean_mark_persistent(l_Lean_Lsp_instToJsonWorkspaceFolder);
l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1 = _init_l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1();
lean_mark_persistent(l_Lean_Lsp_instFromJsonWorkspaceFolder___closed__1);
l_Lean_Lsp_instFromJsonWorkspaceFolder = _init_l_Lean_Lsp_instFromJsonWorkspaceFolder();
lean_mark_persistent(l_Lean_Lsp_instFromJsonWorkspaceFolder);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

3363
stage0/stdlib/Lean/Elab/Quotation.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff