Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324/// JSON-RPC 2.0: the message layer both of this toolkit's protocols sit on.////// `framing` answers "where does a message end"; this module answers "what does/// it say". Both LSP and MCP are JSON-RPC 2.0 over their own framing, which is/// the whole reason the two layers are separate modules rather than one/// protocol-specific reader.////// THE ID IS KEPT AS THE NODE THE CLIENT SENT, never as a parsed number, and/// that is the one decision in this file that is load-bearing rather than/// stylistic. A client sends `"id": 1` and matches the response to its request BY/// THAT VALUE; a server that parsed the id into an `I64` and re-rendered it would/// eventually emit `1.0` (or `"1"`) for some id and the client would have a/// response it cannot place -- a hang with no error anywhere, since JSON-RPC has/// no way to complain about an unmatched id. Carrying the `Json` node and/// splicing it back out makes that impossible by construction: nothing in the/// encode path can change a value it never inspects.////// Nothing here is LSP-specific, and nothing here frames: `rpc_encode_*` returns/// a JSON BODY, and the caller wraps it with `framing`. That split is what lets/// the same module serve MCP's newline-delimited transport, and it is what makes/// every test below runnable without a socket.use json::json {Json}// `BTreeMap` IS NAMED, and the warning that costs is the right trade.//// `std/src/map.mo` has no `pub` decls at all, so naming `BTreeMap` here raises// `cross_mote_package_private` -- that part of this comment's earlier advice was// correct, and `lang/src/json.mo:7` carries the same warning for the same reason.// What changed is the other side: an EMPTY filter is now a hard ERROR, because a// `use` line is the complete dependency declaration and a brace item names a// top-level declaration exactly (`MONAD_USE_COMPLETENESS=error`, the enforced CI// step). A warning shared with main's own corpus beats an error that fails the// build, and `lang/src/json.mo:7`'s `{BTreeMap, BTreeMap.to_list, empty}` is the// spelling to match. The 21 such warnings in this corpus all predate these motes.use std::map {BTreeMap}// --- Error codes ---//// The five the specification reserves. They are the whole error vocabulary this// server needs: a method it does not implement is `method not found`, malformed// params are `invalid params`, and anything the server itself could not do is// `internal`, which is also the code for every failure with no better one.//// Written as `0 - n` rather than `-n` so the negative literal cannot be read as// subtraction by a reader or a reparse; these are the only negative constants in// this mote and they are worth the four extra characters./// The payload was not JSON at all. The one error whose id is necessarily/// unknown, since the request that would have carried it could not be read.pub def rpc_code_parse_error : I64 := 0 - 32700/// JSON, but not a JSON-RPC request object.pub def rpc_code_invalid_request : I64 := 0 - 32600/// Well-formed, but this server does not implement the method. The server MUST/// answer this rather than ignore an unknown request, and it is the code that/// makes a client able to tell a missing feature from a hung one.pub def rpc_code_method_not_found : I64 := 0 - 32601pub def rpc_code_invalid_params : I64 := 0 - 32602pub def rpc_code_internal : I64 := 0 - 32603/// The version string every message carries, in and out.pub def rpc_version : String := "2.0"/// An id, as an `Option`: a message that carries one is a request and MUST be/// answered; a message that does not is a notification and MUST NOT be. The/// `Option` is not a nicety -- answering a notification, or failing to answer a/// request, are both protocol violations, and this is the type that makes the/// distinction visible at every call site.////// `Option (Option Json)` would be the honest type for a RESPONSE (where an/// absent id is legal and means "the request could not be read"), which is why/// `RpcMessage.failure` below carries `Option Json` rather than reusing/// `RpcId`-style naming. That asymmetry is the specification's, not this/// module's.pub type RpcMessage { /// A request: it has an id and it must be answered. request (id : Json) (method : String) (params : Option Json), /// A notification: no id, and answering it is a protocol violation. notification (method : String) (params : Option Json), /// A response to something this server sent. It never sends requests, so /// this arrives only from a confused or hostile peer. response (id : Json) (result : Json), /// An error to send. Ids are absent when the request that would have carried /// one was unreadable. failure (id : Option Json) (code : I64) (message : String), /// Input this module could not turn into any of the above. Carries a reason /// for the log, and the server answers `rpc_code_parse_error` (or /// `rpc_code_invalid_request`) with a null id. unparseable (reason : String),}/// Does this message demand an answer?////// The single question the server loop must get right: it decides whether to/// write anything back. A notification treated as a request puts an unsolicited/// response on the stream, which clients report as an internal error; a request/// treated as a notification leaves the client waiting forever.pub def rpc_wants_reply (m : RpcMessage) : Bool := match m { RpcMessage.request _id _method _params => true, RpcMessage.notification _method _params => false, RpcMessage.response _id _result => false, RpcMessage.failure _id _code _message => false, RpcMessage.unparseable _reason => false, }/// The method name, or the empty string for a message that has none.pub def rpc_method (m : RpcMessage) : String := match m { RpcMessage.request _id method _params => method, RpcMessage.notification method _params => method, RpcMessage.response _id _result => "", RpcMessage.failure _id _code _message => "", RpcMessage.unparseable _reason => "", }/// The params node, or `Option.none` for a request that omitted it.////// A JSON-RPC request may legitimately omit `params` entirely, and an empty/// array is NOT the same as an absent one for methods that take none -- so this/// stays an `Option` all the way to the handler rather than being defaulted/// here.pub def rpc_params (m : RpcMessage) : Option Json := match m { RpcMessage.request _id _method params => params, RpcMessage.notification _method params => params, RpcMessage.response _id _result => Option.none, RpcMessage.failure _id _code _message => Option.none, RpcMessage.unparseable _reason => Option.none, }/// The id node of a message that has one, so a caller can echo it into an error/// without re-deriving which constructor it came from.pub def rpc_id (m : RpcMessage) : Option Json := match m { RpcMessage.request id _method _params => Option.some id, RpcMessage.notification _method _params => Option.none, RpcMessage.response id _result => Option.some id, RpcMessage.failure id _code _message => id, RpcMessage.unparseable _reason => Option.none, }// --- Object building ---/// Start an empty JSON object.////// THE `BTreeMap String Json` ANNOTATION IS LOAD-BEARING, and the reason is a/// trap worth recording. `Map`'s class declaration gives it a DEFAULT instance/// (`class Map (M := HashMap)`, `std/src/map.mo:18`), so an unannotated/// `Map.empty` resolves to a `HashMap` and NOT to the `BTreeMap` that/// `Json.make_object` requires. Inference does not catch it at the `Map.empty`/// site -- the expected type is not known there -- so the mistake surfaces much/// later, while the `Json` node is being built, as a constructor-arity error/// naming none of these types. One annotated binding, here, is what stops every/// call site in this mote from having to know it.def rpc_empty_object : BTreeMap String Json := Map.empty/// Build an object from its fields. Later pairs win, which cannot arise from the/// callers here -- each names its keys once -- so nothing depends on it.////// This exists so that no caller in another mote has to name `BTreeMap`: the/// signature is `List (Pair String Json) -> Json` and the map never appears.#[partial]pub def rpc_object (ps : List (Pair String Json)) : Json := rpc_object_go ps rpc_empty_object#[partial]def rpc_object_go (ps : List (Pair String Json)) (m : BTreeMap String Json) : Json := match ps { List.empty => Json.make_object m, List.cons p rest => match p { Pair.pair k v => rpc_object_go rest (Map.insert k v m), }, }/// One field of a JSON object, or `Option.none` when the value is not an object/// or the key is absent. Both are the same answer to every caller here: a/// request without `method` is malformed and a request without `params` is fine,/// and neither is worth a distinct error.#[partial]pub def rpc_field (key : String) (j : Json) : Option Json := match Json.get_object j { Result.err _e => Option.none, Result.ok o => Json.object_get key o, }/// Render a parse failure for the log.////// `Json.ParseError`'s own `to_string` is not `pub`, but its constructors are,/// so this matches them rather than asking for a promotion: the two-constructor/// type is the whole vocabulary and rendering it cannot drift from the type/// without a compile error.def rpc_parse_error_text (pe : Json.ParseError) : String := match pe { Json.ParseError.expected e f => String.concat "expected " (String.concat e (String.concat ", found " f)), Json.ParseError.generic s => s, }// --- Parsing ---/// Turn a message body into an outcome.////// Never fails: a body that cannot be read is `RpcMessage.unparseable` carrying/// why, because the server has to answer SOMETHING for a malformed frame and a/// function that returned an error would leave the caller to invent the reply.////// A message with a `method` is a request when it carries an id and a/// notification when it does not -- that is the specification's whole/// distinction, and `"id": null` is NOT the same as an absent id. This reads/// presence, not null-ness, and treats an explicit null id as present, which is/// what a strict reading of the spec says and the safe way round: answering a/// notification is a visible protocol error, while ignoring a request hangs the/// client.#[partial]pub def rpc_parse (text : String) : RpcMessage := match Json.parse text { Result.err pe => RpcMessage.unparseable (rpc_parse_error_text pe), Result.ok j => rpc_of_json j, }#[partial]def rpc_of_json (j : Json) : RpcMessage := match rpc_field "method" j { Option.none => rpc_of_json_without_method j, Option.some mj => match Json.get_str mj { Result.err _e => RpcMessage.unparseable "method is not a string", Result.ok method => match rpc_field "id" j { Option.none => RpcMessage.notification method (rpc_field "params" j), Option.some id => RpcMessage.request id method (rpc_field "params" j), }, }, }/// An object with no `method`. Either a response to a request this server never/// sent, or not a JSON-RPC message at all -- and it is `response` only when it/// carries both an id and a `result`, since guessing the other way would answer/// a message the peer considers a reply.#[partial]def rpc_of_json_without_method (j : Json) : RpcMessage := match rpc_field "id" j { Option.none => RpcMessage.unparseable "no method and no id", Option.some id => match rpc_field "result" j { Option.none => RpcMessage.unparseable "no method and no result", Option.some result => RpcMessage.response id result, }, }// --- Encoding ---//// Every encoder returns a JSON BODY, unframed. `framing` adds `Content-Length`// (or the newline), which is what keeps this module independent of which// protocol is asking./// A response: the same id node the request carried, spliced back in untouched.#[partial]pub def rpc_encode_result (id : Json) (result : Json) : String := Json.to_string (rpc_object [ Pair.pair "jsonrpc" (Json.make_str rpc_version), Pair.pair "id" id, Pair.pair "result" result, ])/// An error with a known id.#[partial]pub def rpc_encode_error (id : Json) (code : I64) (message : String) : String := Json.to_string (rpc_object [ Pair.pair "jsonrpc" (Json.make_str rpc_version), Pair.pair "id" id, Pair.pair "error" (rpc_error_node code message), ])/// An error with NO id, which is what a parse failure gets: the request that/// would have carried one could not be read, so the specification requires a/// null there rather than any guess.#[partial]pub def rpc_encode_error_no_id (code : I64) (message : String) : String := Json.to_string (rpc_object [ Pair.pair "jsonrpc" (Json.make_str rpc_version), Pair.pair "id" Json.make_null, Pair.pair "error" (rpc_error_node code message), ])def rpc_error_node (code : I64) (message : String) : Json := rpc_object [ Pair.pair "code" (Json.make_num_int code), Pair.pair "message" (Json.make_str message), ]/// A message the server initiates, which for this server means diagnostics and/// nothing else. A notification has no id by definition, so there is no id/// parameter to get wrong.#[partial]pub def rpc_encode_notification (method : String) (params : Json) : String := Json.to_string (rpc_object [ Pair.pair "jsonrpc" (Json.make_str rpc_version), Pair.pair "method" (Json.make_str method), Pair.pair "params" params, ])/// A request, which this server sends only in tests and in the session replay/// harness -- it is a client-side message, and having it here is what lets the/// replay script be the same code path as a real client.#[partial]pub def rpc_encode_request (id : Json) (method : String) (params : Json) : String := Json.to_string (rpc_object [ Pair.pair "jsonrpc" (Json.make_str rpc_version), Pair.pair "id" id, Pair.pair "method" (Json.make_str method), Pair.pair "params" params, ])