Lean.Data.JsonRpc

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

source

instance Lean.JsonRpc.instCoeStringRequestID :

Coe String Lean.JsonRpc.RequestID

Equations

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

source

instance Lean.JsonRpc.instCoeJsonNumberRequestID :

Coe Lean.JsonNumber Lean.JsonRpc.RequestID

Equations

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

source

instance Lean.JsonRpc.instLTRequestID :

LT Lean.JsonRpc.RequestID

Equations

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

source

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))

source

instance Lean.JsonRpc.instFromJsonRequestID :

Lean.FromJson Lean.JsonRpc.RequestID

Equations

Lean.JsonRpc.instFromJsonRequestID = { fromJson? := fun j => match j with | Lean.Json.str s => pure (Lean.JsonRpc.RequestID.str s) | Lean.Json.num n => pure (Lean.JsonRpc.RequestID.num n) | x => throw "a request id needs to be a number or a string" }

source

instance Lean.JsonRpc.instToJsonRequestID :

Lean.ToJson Lean.JsonRpc.RequestID

Equations

Lean.JsonRpc.instToJsonRequestID = { toJson := fun rid => match rid with | Lean.JsonRpc.RequestID.str s => Lean.Json.str s | Lean.JsonRpc.RequestID.num n => Lean.Json.num n | Lean.JsonRpc.RequestID.null => Lean.Json.null }

source

instance Lean.JsonRpc.instToJsonMessage :

Lean.ToJson Lean.JsonRpc.Message

Equations

Lean.JsonRpc.instToJsonMessage = { toJson := fun m => Lean.Json.mkObj (("jsonrpc", Lean.Json.str "2.0") :: match m with | Lean.JsonRpc.Message.request id method params? => [("id", Lean.toJson id), ("method", Lean.Json.str method)] ++ Lean.Json.opt "params" params? | Lean.JsonRpc.Message.notification method params? => ("method", Lean.Json.str method) :: Lean.Json.opt "params" params? | Lean.JsonRpc.Message.response id result => [("id", Lean.toJson id), ("result", result)] | Lean.JsonRpc.Message.responseError id code message data? => [("id", Lean.toJson id), ("error", Lean.Json.mkObj ([("code", Lean.toJson code), ("message", Lean.Json.str message)] ++ Lean.Json.opt "data" data?))]) }

source

instance Lean.JsonRpc.instFromJsonMessage :

Lean.FromJson Lean.JsonRpc.Message

Equations

Lean.JsonRpc.instFromJsonMessage = { fromJson? := fun j => do let discr ← Lean.Json.getObjVal? j "jsonrpc" match discr with | Lean.Json.str "2.0" => HOrElse.hOrElse (do let id ← Lean.Json.getObjValAs? j Lean.JsonRpc.RequestID "id" let method ← Lean.Json.getObjValAs? j String "method" let params? : Except String Lean.Json.Structured := Lean.Json.getObjValAs? j Lean.Json.Structured "params" pure (Lean.JsonRpc.Message.request id method (Except.toOption params?))) fun x => HOrElse.hOrElse (do let method ← Lean.Json.getObjValAs? j String "method" let params? : Except String Lean.Json.Structured := Lean.Json.getObjValAs? j Lean.Json.Structured "params" pure (Lean.JsonRpc.Message.notification method (Except.toOption params?))) fun x => HOrElse.hOrElse (do let id ← Lean.Json.getObjValAs? j Lean.JsonRpc.RequestID "id" let result ← Lean.Json.getObjVal? j "result" pure (Lean.JsonRpc.Message.response id result)) fun x => do let id ← Lean.Json.getObjValAs? j Lean.JsonRpc.RequestID "id" let err ← Lean.Json.getObjVal? j "error" let code ← Lean.Json.getObjValAs? err Lean.JsonRpc.ErrorCode "code" let message ← Lean.Json.getObjValAs? err String "message" let data? : Except String Lean.Json := Lean.Json.getObjVal? err "data" pure (Lean.JsonRpc.Message.responseError id code message (Except.toOption data?)) | x => throw "only version 2.0 of JSON RPC is supported" }

source

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

Lean.FromJson (Lean.JsonRpc.Notification α)

Equations

Lean.JsonRpc.instFromJsonNotification = { fromJson? := fun j => do let msg ← Lean.fromJson? j match msg with | Lean.JsonRpc.Message.notification method params? => do let params ← pure params? let param ← Lean.fromJson? (Lean.toJson params) pure { method := method, param := param } | x => throw "not a notfication" }

source

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

IO Lean.JsonRpc.Message

Equations

IO.FS.Stream.readMessage h nBytes = do let j ← IO.FS.Stream.readJson h nBytes match Lean.fromJson? j with | Except.ok m => pure m | Except.error inner => throw (IO.userError (toString "JSON '" ++ toString (Lean.Json.compress j) ++ toString "' did not have the format of a JSON-RPC message.\n" ++ toString inner ++ toString ""))

source

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

IO (Lean.JsonRpc.Request α)

Equations

IO.FS.Stream.readRequestAs h nBytes expectedMethod α = do let m ← IO.FS.Stream.readMessage h nBytes match m with | Lean.JsonRpc.Message.request id method params? => if method = expectedMethod then let j := Lean.toJson params?; match Lean.fromJson? j with | Except.ok v => pure { id := id, method := expectedMethod, param := v } | Except.error inner => throw (IO.userError (toString "Unexpected param '" ++ toString (Lean.Json.compress j) ++ toString "' for method '" ++ toString expectedMethod ++ toString "'\n" ++ toString inner ++ toString "")) else throw (IO.userError (toString "Expected method '" ++ toString expectedMethod ++ toString "', got method '" ++ toString method ++ toString "'")) | x => throw (IO.userError (toString "Expected JSON-RPC request, got: '" ++ toString (Lean.Json.compress (Lean.toJson m)) ++ toString "'"))

source

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

IO (Lean.JsonRpc.Notification α)

Equations

IO.FS.Stream.readNotificationAs h nBytes expectedMethod α = do let m ← IO.FS.Stream.readMessage h nBytes match m with | Lean.JsonRpc.Message.notification method params? => if method = expectedMethod then let j := Lean.toJson params?; match Lean.fromJson? j with | Except.ok v => pure { method := expectedMethod, param := v } | Except.error inner => throw (IO.userError (toString "Unexpected param '" ++ toString (Lean.Json.compress j) ++ toString "' for method '" ++ toString expectedMethod ++ toString "'\n" ++ toString inner ++ toString "")) else throw (IO.userError (toString "Expected method '" ++ toString expectedMethod ++ toString "', got method '" ++ toString method ++ toString "'")) | x => throw (IO.userError (toString "Expected JSON-RPC notification, got: '" ++ toString (Lean.Json.compress (Lean.toJson m)) ++ toString "'"))

source

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

IO (Lean.JsonRpc.Response α)

source

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

IO Unit

Equations

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

source

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

IO Unit

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)))

source

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

IO Unit

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)))

source

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

IO Unit

Equations

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

source

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

IO Unit

Equations

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

source

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

IO Unit

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?))