Documentation

Lean.Data.JsonRpc

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

inductive Lean.JsonRpc.RequestID:

Type

str: String → Lean.JsonRpc.RequestID
num: Lean.JsonNumber → Lean.JsonRpc.RequestID
null: Lean.JsonRpc.RequestID

instance Lean.JsonRpc.instInhabitedRequestID:

Inhabited Lean.JsonRpc.RequestID

Equations

Lean.JsonRpc.instInhabitedRequestID = { default := Lean.JsonRpc.RequestID.str default }

instance Lean.JsonRpc.instBEqRequestID:

BEq Lean.JsonRpc.RequestID

Equations

Lean.JsonRpc.instBEqRequestID = { beq := [anonymous] }

instance Lean.JsonRpc.instOrdRequestID:

Ord Lean.JsonRpc.RequestID

Equations

Lean.JsonRpc.instOrdRequestID = { compare := [anonymous] }

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

OfNat Lean.JsonRpc.RequestID n

Equations

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

instance Lean.JsonRpc.instToStringRequestID:

ToString Lean.JsonRpc.RequestID

Equations

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

inductive Lean.JsonRpc.ErrorCode:

Type

parseError: Lean.JsonRpc.ErrorCode
invalidRequest: Lean.JsonRpc.ErrorCode
methodNotFound: Lean.JsonRpc.ErrorCode
invalidParams: Lean.JsonRpc.ErrorCode
internalError: Lean.JsonRpc.ErrorCode
serverNotInitialized: Lean.JsonRpc.ErrorCode
unknownErrorCode: Lean.JsonRpc.ErrorCode
contentModified: Lean.JsonRpc.ErrorCode
requestCancelled: Lean.JsonRpc.ErrorCode
rpcNeedsReconnect: Lean.JsonRpc.ErrorCode
workerExited: Lean.JsonRpc.ErrorCode
workerCrashed: Lean.JsonRpc.ErrorCode

Error codes defined by JSON-RPC and LSP.

instance Lean.JsonRpc.instInhabitedErrorCode:

Inhabited Lean.JsonRpc.ErrorCode

Equations

Lean.JsonRpc.instInhabitedErrorCode = { default := Lean.JsonRpc.ErrorCode.parseError }

instance Lean.JsonRpc.instBEqErrorCode:

BEq Lean.JsonRpc.ErrorCode

Equations

Lean.JsonRpc.instBEqErrorCode = { beq := [anonymous] }

instance Lean.JsonRpc.instFromJsonErrorCode:

Lean.FromJson Lean.JsonRpc.ErrorCode

Equations

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

instance Lean.JsonRpc.instToJsonErrorCode:

Lean.ToJson Lean.JsonRpc.ErrorCode

Equations

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

inductive Lean.JsonRpc.Message:

Type

request: Lean.JsonRpc.RequestID → String → Option Lean.Json.Structured → Lean.JsonRpc.Message
notification: String → Option Lean.Json.Structured → Lean.JsonRpc.Message
response: Lean.JsonRpc.RequestID → Lean.Json → Lean.JsonRpc.Message
responseError: Lean.JsonRpc.RequestID → Lean.JsonRpc.ErrorCode → String → Option Lean.Json → Lean.JsonRpc.Message

def Lean.JsonRpc.Batch:

Type

Equations

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

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

Type u

id : Lean.JsonRpc.RequestID
method : String
param : α

instance Lean.JsonRpc.instInhabitedRequest:

{a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.JsonRpc.Request a)

Equations

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

instance Lean.JsonRpc.instBEqRequest:

{α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Request α)

Equations

Lean.JsonRpc.instBEqRequest = { beq := [anonymous] }

instance Lean.JsonRpc.instCoeRequestMessage {α : Type u_1} [inst : Lean.ToJson α] :

Coe (Lean.JsonRpc.Request α) Lean.JsonRpc.Message

Equations

Lean.JsonRpc.instCoeRequestMessage = { coe := fun r => Lean.JsonRpc.Message.request r.id r.method (Except.toOption (Lean.Json.toStructured? r.param)) }

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

Type u

method : String
param : α

instance Lean.JsonRpc.instInhabitedNotification:

{a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.JsonRpc.Notification a)

Equations

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

instance Lean.JsonRpc.instBEqNotification:

{α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Notification α)

Equations

Lean.JsonRpc.instBEqNotification = { beq := [anonymous] }

instance Lean.JsonRpc.instCoeNotificationMessage {α : Type u_1} [inst : Lean.ToJson α] :

Coe (Lean.JsonRpc.Notification α) Lean.JsonRpc.Message

Equations

Lean.JsonRpc.instCoeNotificationMessage = { coe := fun r => Lean.JsonRpc.Message.notification r.method (Except.toOption (Lean.Json.toStructured? r.param)) }

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

Type u

id : Lean.JsonRpc.RequestID
result : α

instance Lean.JsonRpc.instInhabitedResponse:

{a : Type u_1} → [inst : Inhabited a] → Inhabited (Lean.JsonRpc.Response a)

Equations

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

instance Lean.JsonRpc.instBEqResponse:

{α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.Response α)

Equations

Lean.JsonRpc.instBEqResponse = { beq := [anonymous] }

instance Lean.JsonRpc.instCoeResponseMessage {α : Type u_1} [inst : Lean.ToJson α] :

Coe (Lean.JsonRpc.Response α) Lean.JsonRpc.Message

Equations

Lean.JsonRpc.instCoeResponseMessage = { coe := fun r => Lean.JsonRpc.Message.response r.id (Lean.toJson r.result) }

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

Type u

instance Lean.JsonRpc.instInhabitedResponseError:

{a : Type u_1} → Inhabited (Lean.JsonRpc.ResponseError a)

Equations

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

instance Lean.JsonRpc.instBEqResponseError:

{α : Type u_1} → [inst : BEq α] → BEq (Lean.JsonRpc.ResponseError α)

Equations

Lean.JsonRpc.instBEqResponseError = { beq := [anonymous] }

instance Lean.JsonRpc.instCoeResponseErrorMessage {α : Type u_1} [inst : Lean.ToJson α] :

Coe (Lean.JsonRpc.ResponseError α) Lean.JsonRpc.Message

Equations

Lean.JsonRpc.instCoeResponseErrorMessage = { coe := fun r => Lean.JsonRpc.Message.responseError r.id r.code r.message (Option.map Lean.toJson r.data?) }

instance Lean.JsonRpc.instCoeStringRequestID:

Coe String Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instCoeJsonNumberRequestID:

Coe Lean.JsonNumber Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instLTRequestID:

LT Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instDecidableLtRequestIDInstLTRequestID (a : Lean.JsonRpc.RequestID) (b : Lean.JsonRpc.RequestID) :

Decidable (a < b)

Equations

Lean.JsonRpc.instDecidableLtRequestIDInstLTRequestID a b = inferInstanceAs (Decidable (Lean.JsonRpc.RequestID.lt a b = true))

instance Lean.JsonRpc.instFromJsonRequestID:

Lean.FromJson Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instToJsonRequestID:

Lean.ToJson Lean.JsonRpc.RequestID

Equations

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

instance Lean.JsonRpc.instToJsonMessage:

Lean.ToJson Lean.JsonRpc.Message

Equations

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

instance Lean.JsonRpc.instFromJsonMessage:

Lean.FromJson Lean.JsonRpc.Message

Equations

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

instance Lean.JsonRpc.instFromJsonNotification {α : Type} [inst : Lean.FromJson α] :

Lean.FromJson (Lean.JsonRpc.Notification α)

Equations

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

def IO.FS.Stream.readMessage (h : IO.FS.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 : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [inst : 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 : IO.FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [inst : Lean.FromJson α] :

IO (Lean.JsonRpc.Notification α)

Equations

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

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

IO (Lean.JsonRpc.Response α)

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

Equations

IO.FS.Stream.writeMessage h m = IO.FS.Stream.writeJson h (Lean.toJson m)

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

Equations

IO.FS.Stream.writeRequest h r = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.request r.id r.method (Except.toOption (Lean.Json.toStructured? r.param)))

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

Equations

IO.FS.Stream.writeNotification h n = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.notification n.method (Except.toOption (Lean.Json.toStructured? n.param)))

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

Equations

IO.FS.Stream.writeResponse h r = IO.FS.Stream.writeMessage h (Lean.JsonRpc.Message.response r.id (Lean.toJson r.result))

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

Equations

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

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

Equations

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