Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) for use in the LSP server.

inductive Lean.JsonRpc.RequestID : Type

In JSON-RPC, each request from the client editor to the language server comes with a request id so that the corresponding response can be identified or cancelled.

• str (s : String) : RequestID
• num (n : JsonNumber) : RequestID
• null : RequestID

def Lean.JsonRpc.instInhabitedRequestID.default : RequestID

Equations

• Lean.JsonRpc.instInhabitedRequestID.default = Lean.JsonRpc.RequestID.str default

instance Lean.JsonRpc.instInhabitedRequestID : Inhabited RequestID

Equations

• Lean.JsonRpc.instInhabitedRequestID = { default := Lean.JsonRpc.instInhabitedRequestID.default }

instance Lean.JsonRpc.instBEqRequestID : BEq RequestID

Equations

• Lean.JsonRpc.instBEqRequestID = { beq := Lean.JsonRpc.instBEqRequestID.beq }

def Lean.JsonRpc.instBEqRequestID.beq : RequestID → RequestID → Bool

Equations

• Lean.JsonRpc.instBEqRequestID.beq (Lean.JsonRpc.RequestID.str a) (Lean.JsonRpc.RequestID.str b) = (a == b)
• Lean.JsonRpc.instBEqRequestID.beq (Lean.JsonRpc.RequestID.num a) (Lean.JsonRpc.RequestID.num b) = (a == b)
• Lean.JsonRpc.instBEqRequestID.beq Lean.JsonRpc.RequestID.null Lean.JsonRpc.RequestID.null = true
• Lean.JsonRpc.instBEqRequestID.beq x✝¹ x✝ = false

instance Lean.JsonRpc.instOrdRequestID : Ord RequestID

Equations

• Lean.JsonRpc.instOrdRequestID = { compare := Lean.JsonRpc.instOrdRequestID.ord }

def Lean.JsonRpc.instOrdRequestID.ord : RequestID → RequestID → Ordering

Equations

• Lean.JsonRpc.instOrdRequestID.ord (Lean.JsonRpc.RequestID.str a) (Lean.JsonRpc.RequestID.str b) = (compare a b).then Ordering.eq
• Lean.JsonRpc.instOrdRequestID.ord (Lean.JsonRpc.RequestID.str a) x✝ = Ordering.lt
• Lean.JsonRpc.instOrdRequestID.ord x (Lean.JsonRpc.RequestID.str b) = Ordering.gt
• Lean.JsonRpc.instOrdRequestID.ord (Lean.JsonRpc.RequestID.num a) (Lean.JsonRpc.RequestID.num b) = (compare a b).then Ordering.eq
• Lean.JsonRpc.instOrdRequestID.ord (Lean.JsonRpc.RequestID.num a) x✝ = Ordering.lt
• Lean.JsonRpc.instOrdRequestID.ord x (Lean.JsonRpc.RequestID.num b) = Ordering.gt
• Lean.JsonRpc.instOrdRequestID.ord Lean.JsonRpc.RequestID.null Lean.JsonRpc.RequestID.null = Ordering.eq

instance Lean.JsonRpc.instOfNatRequestID {n : Nat} : OfNat RequestID n

Equations

• Lean.JsonRpc.instOfNatRequestID = { ofNat := Lean.JsonRpc.RequestID.num (Lean.JsonNumber.fromNat n) }

instance Lean.JsonRpc.instToStringRequestID : ToString RequestID

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.JsonRpc.ErrorCode : Type

Error codes defined by JSON-RPC and LSP.

• parseError : ErrorCode

  Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.

• invalidRequest : ErrorCode

  The JSON sent is not a valid Request object.

• methodNotFound : ErrorCode

  The method does not exist / is not available.

• invalidParams : ErrorCode

  Invalid method parameter(s).

• internalError : ErrorCode

  Internal JSON-RPC error.

• serverNotInitialized : ErrorCode

  Error code indicating that a server received a notification or request before the server has received the initialize request.

• unknownErrorCode : ErrorCode
• contentModified : ErrorCode

  The server detected that the content of a document got modified outside normal conditions. A server should NOT send this error code if it detects a content change in it unprocessed messages. The result even computed on an older state might still be useful for the client.

  If a client decides that a result is not of any use anymore the client should cancel the request.

• requestCancelled : ErrorCode

  The client has canceled a request and a server as detected the cancel.

• rpcNeedsReconnect : ErrorCode
• workerExited : ErrorCode
• workerCrashed : ErrorCode

instance Lean.JsonRpc.instInhabitedErrorCode : Inhabited ErrorCode

Equations

• Lean.JsonRpc.instInhabitedErrorCode = { default := Lean.JsonRpc.instInhabitedErrorCode.default }

def Lean.JsonRpc.instInhabitedErrorCode.default : ErrorCode

Equations

• Lean.JsonRpc.instInhabitedErrorCode.default = Lean.JsonRpc.ErrorCode.parseError

def Lean.JsonRpc.instBEqErrorCode.beq : ErrorCode → ErrorCode → Bool

Equations

• Lean.JsonRpc.instBEqErrorCode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Lean.JsonRpc.instBEqErrorCode : BEq ErrorCode

Equations

• Lean.JsonRpc.instBEqErrorCode = { beq := Lean.JsonRpc.instBEqErrorCode.beq }

instance Lean.JsonRpc.instFromJsonErrorCode : FromJson ErrorCode

Equations

• One or more equations did not get rendered due to their size.

instance Lean.JsonRpc.instToJsonErrorCode : ToJson ErrorCode

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.JsonRpc.Message : Type

A JSON-RPC message.

Uses separate constructors for notifications and errors because client and server behavior is expected to be wildly different for both.

• request (id : RequestID) (method : String) (params? : Option Json.Structured) : Message

  A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• notification (method : String) (params? : Option Json.Structured) : Message

  A notification message. A processed notification message must not send a response back. They work like events.

• response (id : RequestID) (result : Json) : Message

  A Response Message sent as a result of a request.

• responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) : Message

  A non-successful response.

instance Lean.JsonRpc.instInhabitedMessage : Inhabited Message

Equations

• Lean.JsonRpc.instInhabitedMessage = { default := Lean.JsonRpc.instInhabitedMessage.default }

def Lean.JsonRpc.instInhabitedMessage.default : Message

Equations

• Lean.JsonRpc.instInhabitedMessage.default = Lean.JsonRpc.Message.request default default default

def Lean.JsonRpc.Batch : Type

Equations

• Lean.JsonRpc.Batch = Array Lean.JsonRpc.Message

structure Lean.JsonRpc.Request (α : Type u) : Type u

Generic version of Message.request.

A request message to describe a request between the client and the server. Every processed request must send a response back to the sender of the request.

• LSP
• JSON-RPC

• id : RequestID
• method : String
• param : α

def Lean.JsonRpc.instInhabitedRequest.default {a✝ : Type u_1} [Inhabited a✝] : Request a✝

Equations

• Lean.JsonRpc.instInhabitedRequest.default = { id := default, method := default, param := default }

instance Lean.JsonRpc.instInhabitedRequest {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Request a✝)

Equations

• Lean.JsonRpc.instInhabitedRequest = { default := Lean.JsonRpc.instInhabitedRequest.default }

instance Lean.JsonRpc.instBEqRequest {α✝ : Type u_1} [BEq α✝] : BEq (Request α✝)

Equations

• Lean.JsonRpc.instBEqRequest = { beq := Lean.JsonRpc.instBEqRequest.beq }

def Lean.JsonRpc.instBEqRequest.beq {α✝ : Type u_1} [BEq α✝] : Request α✝ → Request α✝ → Bool

Equations

• Lean.JsonRpc.instBEqRequest.beq { id := a, method := a_1, param := a_2 } { id := b, method := b_1, param := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.JsonRpc.instBEqRequest.beq x✝¹ x✝ = false

instance Lean.JsonRpc.instCoeOutRequestMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Request α) Message

Equations

• Lean.JsonRpc.instCoeOutRequestMessageOfToJson = { coe := fun (r : Lean.JsonRpc.Request α) => Lean.JsonRpc.Message.request r.id r.method (Lean.Json.toStructured? r.param).toOption }

def Lean.JsonRpc.Request.ofMessage? : Message → Option (Request Json)

Equations

• Lean.JsonRpc.Request.ofMessage? (Lean.JsonRpc.Message.request id method params?) = some { id := id, method := method, param := Lean.toJson params? }
• Lean.JsonRpc.Request.ofMessage? x✝ = none

structure Lean.JsonRpc.Notification (α : Type u) : Type u

Generic version of Message.notification.

A notification message. A processed notification message must not send a response back. They work like events.

• JSON-RPC
• LSP.

• method : String
• param : α

instance Lean.JsonRpc.instInhabitedNotification {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Notification a✝)

Equations

• Lean.JsonRpc.instInhabitedNotification = { default := Lean.JsonRpc.instInhabitedNotification.default }

def Lean.JsonRpc.instInhabitedNotification.default {a✝ : Type u_1} [Inhabited a✝] : Notification a✝

Equations

• Lean.JsonRpc.instInhabitedNotification.default = { method := default, param := default }

instance Lean.JsonRpc.instBEqNotification {α✝ : Type u_1} [BEq α✝] : BEq (Notification α✝)

Equations

• Lean.JsonRpc.instBEqNotification = { beq := Lean.JsonRpc.instBEqNotification.beq }

def Lean.JsonRpc.instBEqNotification.beq {α✝ : Type u_1} [BEq α✝] : Notification α✝ → Notification α✝ → Bool

Equations

• Lean.JsonRpc.instBEqNotification.beq { method := a, param := a_1 } { method := b, param := b_1 } = (a == b && a_1 == b_1)
• Lean.JsonRpc.instBEqNotification.beq x✝¹ x✝ = false

instance Lean.JsonRpc.instCoeOutNotificationMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Notification α) Message

Equations

• One or more equations did not get rendered due to their size.

def Lean.JsonRpc.Notification.ofMessage? : Message → Option (Notification Json)

Equations

• Lean.JsonRpc.Notification.ofMessage? (Lean.JsonRpc.Message.notification method params?) = some { method := method, param := Lean.toJson params? }
• Lean.JsonRpc.Notification.ofMessage? x✝ = none

structure Lean.JsonRpc.Response (α : Type u) : Type u

Generic version of Message.response.

A Response Message sent as a result of a request. If a request doesn’t provide a result value the receiver of a request still needs to return a response message to conform to the JSON-RPC specification. The result property of the ResponseMessage should be set to null in this case to signal a successful request.

References:

• JSON-RPC
• LSP

• id : RequestID
• result : α

def Lean.JsonRpc.instInhabitedResponse.default {a✝ : Type u_1} [Inhabited a✝] : Response a✝

Equations

• Lean.JsonRpc.instInhabitedResponse.default = { id := default, result := default }

instance Lean.JsonRpc.instInhabitedResponse {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Response a✝)

Equations

• Lean.JsonRpc.instInhabitedResponse = { default := Lean.JsonRpc.instInhabitedResponse.default }

def Lean.JsonRpc.instBEqResponse.beq {α✝ : Type u_1} [BEq α✝] : Response α✝ → Response α✝ → Bool

Equations

• Lean.JsonRpc.instBEqResponse.beq { id := a, result := a_1 } { id := b, result := b_1 } = (a == b && a_1 == b_1)
• Lean.JsonRpc.instBEqResponse.beq x✝¹ x✝ = false

instance Lean.JsonRpc.instBEqResponse {α✝ : Type u_1} [BEq α✝] : BEq (Response α✝)

Equations

• Lean.JsonRpc.instBEqResponse = { beq := Lean.JsonRpc.instBEqResponse.beq }

instance Lean.JsonRpc.instCoeOutResponseMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (Response α) Message

Equations

• Lean.JsonRpc.instCoeOutResponseMessageOfToJson = { coe := fun (r : Lean.JsonRpc.Response α) => Lean.JsonRpc.Message.response r.id (Lean.toJson r.result) }

def Lean.JsonRpc.Response.ofMessage? : Message → Option (Response Json)

Equations

• Lean.JsonRpc.Response.ofMessage? (Lean.JsonRpc.Message.response id result) = some { id := id, result := result }
• Lean.JsonRpc.Response.ofMessage? x✝ = none

structure Lean.JsonRpc.ResponseError (α : Type u) : Type u

Generic version of Message.responseError.

References:

• JSON-RPC
• LSP.

• id : RequestID
• code : ErrorCode
• message : String

  A string providing a short description of the error.

• data? : Option α

  A primitive or structured value that contains additional information about the error. Can be omitted.

def Lean.JsonRpc.instInhabitedResponseError.default {a✝ : Type u_1} : ResponseError a✝

Equations

• Lean.JsonRpc.instInhabitedResponseError.default = { id := default, code := default, message := default, data? := default }

instance Lean.JsonRpc.instInhabitedResponseError {a✝ : Type u_1} : Inhabited (ResponseError a✝)

Equations

• Lean.JsonRpc.instInhabitedResponseError = { default := Lean.JsonRpc.instInhabitedResponseError.default }

def Lean.JsonRpc.instBEqResponseError.beq {α✝ : Type u_1} [BEq α✝] : ResponseError α✝ → ResponseError α✝ → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.JsonRpc.instBEqResponseError.beq x✝¹ x✝ = false

instance Lean.JsonRpc.instBEqResponseError {α✝ : Type u_1} [BEq α✝] : BEq (ResponseError α✝)

Equations

• Lean.JsonRpc.instBEqResponseError = { beq := Lean.JsonRpc.instBEqResponseError.beq }

instance Lean.JsonRpc.instCoeOutResponseErrorMessageOfToJson {α : Type u_1} [ToJson α] : CoeOut (ResponseError α) Message

Equations

• One or more equations did not get rendered due to their size.

instance Lean.JsonRpc.instCoeOutResponseErrorUnitMessage : CoeOut (ResponseError Unit) Message

Equations

• Lean.JsonRpc.instCoeOutResponseErrorUnitMessage = { coe := fun (r : Lean.JsonRpc.ResponseError Unit) => Lean.JsonRpc.Message.responseError r.id r.code r.message none }

def Lean.JsonRpc.ResponseError.ofMessage? : Message → Option (ResponseError Json)

Equations

• Lean.JsonRpc.ResponseError.ofMessage? (Lean.JsonRpc.Message.responseError id code message data?) = some { id := id, code := code, message := message, data? := data? }
• Lean.JsonRpc.ResponseError.ofMessage? x✝ = none

instance Lean.JsonRpc.instCoeStringRequestID : Coe String RequestID

Equations

• Lean.JsonRpc.instCoeStringRequestID = { coe := Lean.JsonRpc.RequestID.str }

instance Lean.JsonRpc.instCoeJsonNumberRequestID : Coe JsonNumber RequestID

Equations

• Lean.JsonRpc.instCoeJsonNumberRequestID = { coe := Lean.JsonRpc.RequestID.num }

def Lean.JsonRpc.RequestID.lt : RequestID → RequestID → Bool

Equations

• (Lean.JsonRpc.RequestID.str a).lt (Lean.JsonRpc.RequestID.str b) = decide (a < b)
• (Lean.JsonRpc.RequestID.num a).lt (Lean.JsonRpc.RequestID.num b) = decide (a < b)
• Lean.JsonRpc.RequestID.null.lt (Lean.JsonRpc.RequestID.num n) = true
• Lean.JsonRpc.RequestID.null.lt (Lean.JsonRpc.RequestID.str s) = true
• (Lean.JsonRpc.RequestID.num n).lt (Lean.JsonRpc.RequestID.str s) = true
• x✝¹.lt x✝ = false

def Lean.JsonRpc.RequestID.ltProp : LT RequestID

Equations

• Lean.JsonRpc.RequestID.ltProp = { lt := fun (a b : Lean.JsonRpc.RequestID) => a.lt b = true }

instance Lean.JsonRpc.instLTRequestID : LT RequestID

Equations

• Lean.JsonRpc.instLTRequestID = Lean.JsonRpc.RequestID.ltProp

instance Lean.JsonRpc.instDecidableLtRequestID (a b : RequestID) : Decidable (a < b)

Equations

• Lean.JsonRpc.instDecidableLtRequestID a b = inferInstanceAs (Decidable (a.lt b = true))

instance Lean.JsonRpc.instFromJsonRequestID : FromJson RequestID

Equations

• One or more equations did not get rendered due to their size.

instance Lean.JsonRpc.instToJsonRequestID : ToJson RequestID

Equations

• One or more equations did not get rendered due to their size.

instance Lean.JsonRpc.instToJsonMessage : ToJson Message

Equations

• One or more equations did not get rendered due to their size.

instance Lean.JsonRpc.instFromJsonMessage : FromJson Message

Equations

• One or more equations did not get rendered due to their size.

instance Lean.JsonRpc.instFromJsonNotification {α : Type} [FromJson α] : FromJson (Notification α)

Equations

• One or more equations did not get rendered due to their size.

inductive Lean.JsonRpc.MessageMetaData : Type

A variant of Message that has been parsed partially, without the payload. This is useful when we want to process the metadata of a Message without parsing and converting the whole thing.

• request (id : RequestID) (method : String) : MessageMetaData
• notification (method : String) : MessageMetaData
• response (id : RequestID) : MessageMetaData
• responseError (id : RequestID) (code : ErrorCode) (message : String) (data? : Option Json) : MessageMetaData

def Lean.JsonRpc.instInhabitedMessageMetaData.default : MessageMetaData

Equations

• Lean.JsonRpc.instInhabitedMessageMetaData.default = Lean.JsonRpc.MessageMetaData.request default default

instance Lean.JsonRpc.instInhabitedMessageMetaData : Inhabited MessageMetaData

Equations

• Lean.JsonRpc.instInhabitedMessageMetaData = { default := Lean.JsonRpc.instInhabitedMessageMetaData.default }

def Lean.JsonRpc.MessageMetaData.toMessage : MessageMetaData → Message

Equations

• (Lean.JsonRpc.MessageMetaData.request id method).toMessage = Lean.JsonRpc.Message.request id method none
• (Lean.JsonRpc.MessageMetaData.notification method).toMessage = Lean.JsonRpc.Message.notification method none
• (Lean.JsonRpc.MessageMetaData.response id).toMessage = Lean.JsonRpc.Message.response id Lean.Json.null
• (Lean.JsonRpc.MessageMetaData.responseError id code message data?).toMessage = Lean.JsonRpc.Message.responseError id code message data?

def Lean.JsonRpc.parseMessageMetaData (input : String) : Except String MessageMetaData

Danger: For performance reasons, this function makes a number of fragile assumptions about input. Namely:

• input is the output of (toJson (v : Message)).compress
• compress yields a lexicographic ordering of JSON object keys

Equations

• Lean.JsonRpc.parseMessageMetaData input = (Lean.JsonRpc.messageMetaDataParser✝ input).run input

def IO.FS.Stream.readMessage (h : Stream) (nBytes : Nat) : IO Lean.JsonRpc.Message

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.Stream.readRequestAs (h : Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Request α)

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.Stream.readNotificationAs (h : Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Notification α)

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.Stream.readResponseAs (h : Stream) (nBytes : Nat) (expectedID : Lean.JsonRpc.RequestID) (α : Type) [Lean.FromJson α] : IO (Lean.JsonRpc.Response α)

Equations

• One or more equations did not get rendered due to their size.

def IO.FS.Stream.writeMessage (h : Stream) (m : Lean.JsonRpc.Message) : IO Unit

Equations

• h.writeMessage m = h.writeJson (Lean.toJson m)

def IO.FS.Stream.writeRequest {α : Type u_1} [Lean.ToJson α] (h : Stream) (r : Lean.JsonRpc.Request α) : IO Unit

Equations

• h.writeRequest r = h.writeMessage (Lean.JsonRpc.Message.request r.id r.method (Lean.Json.toStructured? r.param).toOption)

def IO.FS.Stream.writeNotification {α : Type u_1} [Lean.ToJson α] (h : Stream) (n : Lean.JsonRpc.Notification α) : IO Unit

Equations

• h.writeNotification n = h.writeMessage (Lean.JsonRpc.Message.notification n.method (Lean.Json.toStructured? n.param).toOption)

def IO.FS.Stream.writeResponse {α : Type u_1} [Lean.ToJson α] (h : Stream) (r : Lean.JsonRpc.Response α) : IO Unit

Equations

• h.writeResponse r = h.writeMessage (Lean.JsonRpc.Message.response r.id (Lean.toJson r.result))

def IO.FS.Stream.writeResponseError (h : Stream) (e : Lean.JsonRpc.ResponseError Unit) : IO Unit

Equations

• h.writeResponseError e = h.writeMessage (Lean.JsonRpc.Message.responseError e.id e.code e.message none)

def IO.FS.Stream.writeResponseErrorWithData {α : Type u_1} [Lean.ToJson α] (h : Stream) (e : Lean.JsonRpc.ResponseError α) : IO Unit

Equations

• h.writeResponseErrorWithData e = h.writeMessage (Lean.JsonRpc.Message.responseError e.id e.code e.message (Option.map Lean.toJson e.data?))