diff --git a/CHANGES.md b/CHANGES.md index ff9f61f9..26d8af6f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -56,6 +56,8 @@ #550) - [petanque] Allow memoization control on `petanque/run` via a new parameter `memo` (@ejgallego, #780) + - [lsp] [petanque] Allow acces to `petanque` protocol from the lsp + server (@ejgallego, #778) # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_... ---------------------------------------------------- diff --git a/controller/dune b/controller/dune index 5a9170ed..2a470ba3 100644 --- a/controller/dune +++ b/controller/dune @@ -1,7 +1,7 @@ (library (name controller) (modules :standard \ coq_lsp) - (libraries coq fleche lsp dune-build-info)) + (libraries coq fleche petanque petanque_json lsp dune-build-info)) (executable (name coq_lsp) diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 627e6768..3ebe9b0f 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -427,6 +427,43 @@ let do_changeConfiguration ~io params = Rq_init.do_settings settings; () +(* EJGA: Note that our current configuration allow petanque calls to be + interrupted, this can become an issue with LSP. For now, clients must choose + a trade-off (we could disable interruption on petanque call, but that brings + other downsides) + + The only real solution is to wait for OCaml 5.x support, so we can server + read-only queries without interrupting the main Coq thread. *) +let petanque_handle ~token (module R : Petanque_json.Protocol.Request.S) ~params + = + let open Petanque_json in + match Interp.do_request (module R) ~params with + | Interp.Action.Now handler -> Rq.Action.now (handler ~token) + | Interp.Action.Doc { uri; handler } -> + (* Request document execution if not ready *) + let postpone = true in + Rq.Action.(Data (DocRequest { uri; postpone; handler })) + +let do_petanque ~token method_ params = + (* For now we do a manual brigde *) + let open Petanque_json.Protocol in + match method_ with + | s when String.equal Start.method_ s -> + petanque_handle ~token (module Start) ~params + | s when String.equal RunTac.method_ s -> + petanque_handle ~token (module RunTac) ~params + | s when String.equal Goals.method_ s -> + petanque_handle ~token (module Goals) ~params + | s when String.equal Premises.method_ s -> + petanque_handle ~token (module Premises) ~params + | _ -> + (* EJGA: should we allow this system to compose better with other LSP + extensions? *) + (* JSON-RPC method not found *) + let code = -32601 in + let message = "method not found" in + Rq.Action.error (code, message) + (***********************************************************************) (** LSP Init routine *) @@ -529,7 +566,7 @@ let dispatch_state_notification ~io ~ofn ~token ~state ~method_ ~params : dispatch_notification ~io ~ofn ~token ~state ~method_ ~params; state -let dispatch_request ~method_ ~params : Rq.Action.t = +let dispatch_request ~token ~method_ ~params : Rq.Action.t = match method_ with (* Lifecyle *) | "initialize" -> @@ -552,15 +589,14 @@ let dispatch_request ~method_ ~params : Rq.Action.t = | "coq/getDocument" -> do_document ~params (* Petanque embedding *) | msg when Coq.Compat.Ocaml_413.String.starts_with ~prefix:"petanque/" msg -> - L.trace "delegating to petanque [wip]" "%s" msg; - Rq.Action.error (-32601, "method not found") + do_petanque msg ~token params (* Generic handler *) | msg -> L.trace "no_handler" "%s" msg; Rq.Action.error (-32601, "method not found") let dispatch_request ~ofn_rq ~token ~id ~method_ ~params = - dispatch_request ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id + dispatch_request ~token ~method_ ~params |> Rq.serve ~ofn_rq ~token ~id let dispatch_message ~io ~ofn ~token ~state (com : LSP.Message.t) : State.t = let ofn_rq r = Lsp.Base.Message.response r |> ofn in diff --git a/editor/code/lib/types.ts b/editor/code/lib/types.ts index 1e196f07..76c98ac7 100644 --- a/editor/code/lib/types.ts +++ b/editor/code/lib/types.ts @@ -208,3 +208,15 @@ export interface CoqStoppedStatus { } export type CoqServerStatus = CoqBusyStatus | CoqIdleStatus | CoqStoppedStatus; + +// Petanque types, canonical source agent.mli +export interface PetStartParams { + uri: string; + pre_commands: string | null; + thm: string; +} + +export interface PetRunParams { + st: number; + tac: string; +} diff --git a/editor/code/package.json b/editor/code/package.json index d4ccf71e..a5278d66 100644 --- a/editor/code/package.json +++ b/editor/code/package.json @@ -132,6 +132,14 @@ { "command": "coq-lsp.heatmap.toggle", "title": "Coq LSP: Toggle heatmap" + }, + { + "command": "coq-lsp.petanque.start", + "title": "Coq LSP: Start a petanque session for theorem (Coq developer-only command)" + }, + { + "command": "coq-lsp.petanque.run", + "title": "Coq LSP: Run a tactic over a petanque session (Coq developer-only command)" } ], "keybindings": [ diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts index abc3f27e..d8dbf352 100644 --- a/editor/code/src/client.ts +++ b/editor/code/src/client.ts @@ -15,6 +15,7 @@ import { languages, Uri, TextEditorVisibleRangesChangeEvent, + InputBoxOptions, } from "vscode"; import * as vscode from "vscode"; @@ -54,6 +55,7 @@ import { FileProgressManager } from "./progress"; import { coqPerfData, PerfDataView } from "./perf"; import { sentenceNext, sentencePrevious } from "./edit"; import { HeatMap, HeatMapConfig } from "./heatmap"; +import { petanqueStart, petanqueRun, petSetClient } from "./petanque"; import { debounce, throttle } from "throttle-debounce"; // Convert perf data to VSCode format @@ -154,6 +156,7 @@ export function activateCoqLSP( ); context.subscriptions.push(disposable); } + function checkForVSCoq() { let vscoq = extensions.getExtension("maximedenes.vscoq") || @@ -216,6 +219,7 @@ export function activateCoqLSP( let cP = new Promise((resolve) => { client = clientFactory(context, clientOptions, wsConfig); + petSetClient(client); fileProgress = new FileProgressManager(client); perfDataHook = client.onNotification(coqPerfData, (data) => { perfDataView.update(data); @@ -519,6 +523,9 @@ export function activateCoqLSP( coqEditorCommand("heatmap.toggle", heatMapToggle); + coqEditorCommand("petanque.start", petanqueStart); + coqEditorCommand("petanque.run", petanqueRun); + createEnableButton(); // Fix for bug #750 diff --git a/editor/code/src/petanque.ts b/editor/code/src/petanque.ts new file mode 100644 index 00000000..87d5b1a1 --- /dev/null +++ b/editor/code/src/petanque.ts @@ -0,0 +1,60 @@ +import { window, InputBoxOptions, TextEditor } from "vscode"; +import { BaseLanguageClient, RequestType } from "vscode-languageclient"; +import { PetRunParams, PetStartParams } from "../lib/types"; + +const petStartReq = new RequestType( + "petanque/start" +); +let client: BaseLanguageClient; + +export function petSetClient(newClient: BaseLanguageClient) { + client = newClient; +} + +export const petanqueStart = (editor: TextEditor) => { + let uri = editor.document.uri.toString(); + let pre_commands = null; + + // Imput theorem name + let inputOptions: InputBoxOptions = { + title: "Petanque Start", + prompt: "Name of the theorem to start a session ", + }; + window + .showInputBox(inputOptions) + .then((thm_user) => { + let thm = thm_user ?? "petanque_debug"; + let params: PetStartParams = { uri, pre_commands, thm }; + return Promise.resolve(params); + }) + .then((params: PetStartParams) => { + client + .sendRequest(petStartReq, params) + .then((id) => + window.setStatusBarMessage(`petanque/start succeed ${id}`, 5000) + ) + .catch((error) => { + let err_message = error.toString(); + console.log(`error in save: ${err_message}`); + window.showErrorMessage(err_message); + }); + }); +}; + +const petRunReq = new RequestType("petanque/run"); + +export const petanqueRun = (editor: TextEditor) => { + // XXX Read from user + let params: PetRunParams = { st: 1, tac: "idtac." }; + client + .sendRequest(petRunReq, params) + .then((answer: any) => { + let res = JSON.stringify(answer); + window.setStatusBarMessage(`petanque/run succeed ${res}`, 5000); + }) + .catch((error) => { + let err_message = error.toString(); + console.log(`error in save: ${err_message}`); + window.showErrorMessage(err_message); + }); +}; diff --git a/examples/petanque.v b/examples/petanque.v new file mode 100644 index 00000000..8616a823 --- /dev/null +++ b/examples/petanque.v @@ -0,0 +1,2 @@ +Theorem petanque_debug : True. +Proof. now auto. Qed. diff --git a/fleche/theory.ml b/fleche/theory.ml index d4234974..6f573eaf 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -405,3 +405,7 @@ module Request = struct | FullDoc -> Handle.remove_cp_request ~uri ~id | PosInDoc { point; _ } -> Handle.remove_pt_request ~uri ~id ~point end + +(* xxx to remove *) +let find_doc ~uri = + Handle._find_opt ~uri |> Option.map (fun { Handle.doc; _ } -> doc) diff --git a/fleche/theory.mli b/fleche/theory.mli index e20c2cf7..2c037158 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -93,3 +93,6 @@ module Register : sig val add : t -> unit end end + +(* XXX this is temporal for petanque, will fix before merge *) +val find_doc : uri:Lang.LUri.File.t -> Doc.t option diff --git a/petanque/README.md b/petanque/README.md index 43d149e1..cdb47056 100644 --- a/petanque/README.md +++ b/petanque/README.md @@ -50,11 +50,18 @@ See the contributing guide for instructions on how to do the last. ## Running `petanque` JSON shell -You can use `petanque` in 2 different ways: +You can use `petanque` in 3 different ways: -- call the API directly from your OCaml program +- call the API using JSON-RPC directly in `coq-lsp`, over the LSP + protocol - use the provided `pet` and `pet-server` JSON-RPC shells, usually - with a library such as Pytanque. + with a library such as Pytanque +- call the API directly from your OCaml program + +See `agent.mli` for an overview of the API. The +`petanque/setWorkspace` method is only available in the `pet` and +`pet-server` shells; when `petanque` is used from LSP, the workspace +needs to be set using LSP in the usual way. To execute the `pet` JSON-RPC shell do: ``` diff --git a/petanque/agent.ml b/petanque/agent.ml index a8378a35..d531396e 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -101,17 +101,12 @@ let protect_to_result (r : _ Coq.Protect.E.t) : (_, _) Result.t = Error (Error.Anomaly (Pp.string_of_ppcmds msg)) | { r = Completed (Ok r); feedback = _ } -> Ok r -let fn = ref (fun ~token:_ _uri -> Error (Error.System "No handler for fn")) - -let start ~token ~uri ?pre_commands ~thm () = - match !fn ~token uri with - | Ok doc -> - let open Coq.Compat.Result.O in - let* node = find_thm ~doc ~thm in - (* Usually single shot, so we don't memoize *) - let memo = false in - execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result - | Error err -> Error err +let start ~token ~doc ?pre_commands ~thm () = + let open Coq.Compat.Result.O in + let* node = find_thm ~doc ~thm in + (* Usually single shot, so we don't memoize *) + let memo = false in + execute_precommands ~token ~memo ~pre_commands ~node |> protect_to_result let proof_finished { Coq.Goals.goals; stack; shelf; given_up; _ } = List.for_all CList.is_empty [ goals; shelf; given_up ] && CList.is_empty stack diff --git a/petanque/agent.mli b/petanque/agent.mli index 21b7902a..d0a908e3 100644 --- a/petanque/agent.mli +++ b/petanque/agent.mli @@ -40,16 +40,34 @@ module Run_result : sig | Current_state of 'a end -val fn : (token:Coq.Limits.Token.t -> Lang.LUri.File.t -> Fleche.Doc.t R.t) ref +(** Protocol notes: -(** [start ~token ~fn ~uri ~pre_commands ~thm] start a new proof for theorem - [thm] in file [uri] under [fn]. [token] can be used to interrupt the - computation. Returns the proof state or error otherwise. [pre_commands] is a - string of dot-separated Coq commands that will be executed before the proof - starts. *) + The idea is that the types of the functions here have a direct translation + to the JSON-RPC (or any other) protocol. + + Thus, types here correspond to types in the wire, except for cases where the + protocol layer performs an implicit mapping on types. + + So far, the mappings are: + + - [uri] <-> [Doc.t] + - [int] <-> [State.t] + + The [State.t] mapping is easy to do at the protocol level with a simple + mapping, however [uri -> Doc.t] may need to yield to the document manager to + build the corresponding [doc]. This is very convenient for users, but + introduces a little bit more machinery. + + We could imagine a future where [State.t] need to be managed asynchronously, + then the same approach that we use for [Doc.t] could happen. *) + +(** [start ~token ~doc ~pre_commands ~thm] start a new proof for theorem [thm] + in file [uri] under [fn]. [token] can be used to interrupt the computation. + Returns the proof state or error otherwise. [pre_commands] is a string of + dot-separated Coq commands that will be executed before the proof starts. *) val start : token:Coq.Limits.Token.t - -> uri:Lang.LUri.File.t + -> doc:Fleche.Doc.t -> ?pre_commands:string -> thm:string -> unit diff --git a/petanque/json_shell/interp.ml b/petanque/json_shell/interp.ml index cc6517a3..623f2ca1 100644 --- a/petanque/json_shell/interp.ml +++ b/petanque/json_shell/interp.ml @@ -2,44 +2,83 @@ open Protocol open Protocol_shell module A = Petanque.Agent -let do_request ~token (module R : Request.S) ~id ~params = +(* These types ares basically duplicated with controller/request.ml; move to a + common lib (lsp?) *) +type r = (Yojson.Safe.t, int * string) Result.t + +module Action = struct + type 'a t = + | Now of (token:Coq.Limits.Token.t -> r) + | Doc of + { uri : Lang.LUri.File.t + ; handler : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> r + } +end +(* End of controller/request.ml *) + +let of_pet_err res = + Result.map_error + (fun err -> + let message = Petanque.Agent.Error.to_string err in + let code = Petanque.Agent.Error.to_code err in + (code, message)) + res + +(* Basically a functor from R.Handler.t to Action.t, but closing over params *) +let do_request (module R : Protocol.Request.S) ~params = + let of_pet res = Result.map R.Handler.Response.to_yojson res |> of_pet_err in + let handler params = + match R.Handler.handler with + | Immediate handler -> + Action.Now (fun ~token -> handler ~token params |> of_pet) + | FullDoc { uri_fn; handler } -> + let uri = uri_fn params in + let handler ~token ~doc = handler ~token ~doc params |> of_pet in + Action.Doc { uri; handler } + in match R.Handler.Params.of_yojson (`Assoc params) with - | Ok params -> ( - match R.Handler.handler ~token params with - | Ok result -> - let result = R.Handler.Response.to_yojson result in - Lsp.Base.Response.mk_ok ~id ~result - | Error err -> - let message = A.Error.to_string err in - let code = A.Error.to_code err in - Lsp.Base.Response.mk_error ~id ~code ~message) + | Ok params -> handler params | Error message -> (* JSON-RPC Parse error *) let code = -32700 in - Lsp.Base.Response.mk_error ~id ~code ~message + Action.Now (fun ~token:_ -> Error (code, message)) -let handle_request ~token ~id ~method_ ~params = +let do_handle ~fn ~token (module R : Protocol.Request.S) ~params = + match do_request (module R) ~params with + | Action.Now handler -> handler ~token + | Action.Doc { uri; handler } -> + let open Coq.Compat.Result.O in + let* doc = fn ~token ~uri |> of_pet_err in + handler ~token ~doc + +let handle_request ~token ~method_ ~params = match method_ with | s when String.equal SetWorkspace.method_ s -> - do_request ~token (module SetWorkspace) ~id ~params + do_handle ~token (module SetWorkspace) ~params | s when String.equal Start.method_ s -> - do_request ~token (module Start) ~id ~params + do_handle ~token (module Start) ~params | s when String.equal RunTac.method_ s -> - do_request ~token (module RunTac) ~id ~params + do_handle ~token (module RunTac) ~params | s when String.equal Goals.method_ s -> - do_request ~token (module Goals) ~id ~params + do_handle ~token (module Goals) ~params | s when String.equal Premises.method_ s -> - do_request ~token (module Premises) ~id ~params + do_handle ~token (module Premises) ~params | _ -> - (* JSON-RPC method not found *) - let code = -32601 in - let message = "method not found" in - Lsp.Base.Response.mk_error ~id ~code ~message + fun ~fn:_ -> + (* JSON-RPC method not found *) + let code = -32601 in + let message = "method not found" in + Error (code, message) + +let request ~fn ~token ~id ~method_ ~params = + match handle_request ~fn ~token ~method_ ~params with + | Ok result -> Lsp.Base.Response.mk_ok ~id ~result + | Error (code, message) -> Lsp.Base.Response.mk_error ~id ~code ~message -let interp ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option = +let interp ~fn ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option = match r with | Request { id; method_; params } -> - let response = handle_request ~token ~id ~method_ ~params in + let response = request ~fn ~token ~id ~method_ ~params in Some (Lsp.Base.Message.response response) | Notification { method_; params = _ } -> let message = "unhandled notification: " ^ method_ in diff --git a/petanque/json_shell/pet.ml b/petanque/json_shell/pet.ml index 2ac03546..ab1e1216 100644 --- a/petanque/json_shell/pet.ml +++ b/petanque/json_shell/pet.ml @@ -28,8 +28,10 @@ let send_message msg = (* Format.fprintf Format.std_formatter "@[%a@]@\n%!" Yojson.Safe.pretty_print msg *) +let fn = Petanque.Shell.build_doc + let interp ~token request = - match Interp.interp ~token request with + match Interp.interp ~fn ~token request with | None -> () | Some message -> send_message message diff --git a/petanque/json_shell/protocol.ml b/petanque/json_shell/protocol.ml index 69223560..42a743e8 100644 --- a/petanque/json_shell/protocol.ml +++ b/petanque/json_shell/protocol.ml @@ -1,3 +1,4 @@ +open Lang open Petanque (* Serialization for agent types *) @@ -5,6 +6,15 @@ open JAgent (* RPC-side server mappings, internal; we could split this in a different module eventually as to make this clearer. *) +module HType = struct + type ('p, 'r) t = + | Immediate of (token:Coq.Limits.Token.t -> 'p -> 'r R.t) + | FullDoc of + { uri_fn : 'p -> LUri.File.t + ; handler : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> 'p -> 'r R.t + } +end + module type Handler = sig (* Server-side RPC specification *) module Params : sig @@ -16,7 +26,7 @@ module type Handler = sig type t [@@deriving to_yojson] end - val handler : token:Coq.Limits.Token.t -> Params.t -> Response.t R.t + val handler : (Params.t, Response.t) HType.t end (* Note that here we follow JSON-RPC / LSP capitalization conventions *) @@ -69,8 +79,13 @@ module Start = struct type t = State.t [@@deriving yojson] end - let handler ~token { Params.uri; pre_commands; thm } = - Agent.start ~token ~uri ?pre_commands ~thm () + let handler = + HType.FullDoc + { uri_fn = (fun { Params.uri; _ } -> uri) + ; handler = + (fun ~token ~doc { Params.uri = _; pre_commands; thm } -> + Agent.start ~token ~doc ?pre_commands ~thm ()) + } end end @@ -107,8 +122,10 @@ module RunTac = struct type t = State.t Run_result.t [@@deriving yojson] end - let handler ~token { Params.memo; st; tac } = - Agent.run ~token ?memo ~st ~tac () + let handler = + HType.Immediate + (fun ~token { Params.memo; st; tac } -> + Agent.run ~token ?memo ~st ~tac ()) end end @@ -131,7 +148,8 @@ module Goals = struct module Response = Response - let handler ~token { Params.st } = Agent.goals ~token ~st + let handler = + HType.Immediate (fun ~token { Params.st } -> Agent.goals ~token ~st) end end @@ -154,6 +172,7 @@ module Premises = struct module Response = Response - let handler ~token { Params.st } = Agent.premises ~token ~st + let handler = + HType.Immediate (fun ~token { Params.st } -> Agent.premises ~token ~st) end end diff --git a/petanque/json_shell/protocol_shell.ml b/petanque/json_shell/protocol_shell.ml index 55d2be3d..918d482b 100644 --- a/petanque/json_shell/protocol_shell.ml +++ b/petanque/json_shell/protocol_shell.ml @@ -21,7 +21,9 @@ module SetWorkspace = struct type t = unit [@@deriving yojson] end - let handler ~token { Params.debug; root } = - Petanque.Shell.set_workspace ~token ~debug ~root + let handler = + Protocol.HType.Immediate + (fun ~token { Params.debug; root } -> + Petanque.Shell.set_workspace ~token ~debug ~root) end end diff --git a/petanque/json_shell/server.ml b/petanque/json_shell/server.ml index 2a35cb7b..de1b11f9 100644 --- a/petanque/json_shell/server.ml +++ b/petanque/json_shell/server.ml @@ -9,6 +9,8 @@ let rq_info (r : Lsp.Base.Message.t) = | Response (Ok { id; _ } | Error { id; _ }) -> Format.asprintf "response for: %d" id +let fn = Petanque.Shell.build_doc + let rec handle_connection ~token ic oc () = try let* request = Lwt_io.read_line ic in @@ -23,7 +25,7 @@ let rec handle_connection ~token ic oc () = let* () = Logs_lwt.info (fun m -> m "Received: %s" (rq_info request)) in (* request could be a notification, so maybe we don't have to do a reply! *) - match Interp.interp ~token request with + match Interp.interp ~fn ~token request with | None -> handle_connection ~token ic oc () | Some reply -> let* () = Logs_lwt.info (fun m -> m "Sent reply") in diff --git a/petanque/shell.ml b/petanque/shell.ml index 490c5012..524e2ed5 100644 --- a/petanque/shell.ml +++ b/petanque/shell.ml @@ -79,9 +79,7 @@ let setup_doc ~token env uri = Ok (Fleche.Doc.check ~io ~token ~target ~doc ()) | Error err -> Error err -let fn ~token uri = - let env = Option.get !env in - setup_doc ~token env uri +let build_doc ~token ~uri = setup_doc ~token (Option.get !env) uri (* Flèche LSP backend handles the conversion at the protocol level *) let to_uri uri = Lang.LUri.of_string uri |> Lang.LUri.File.of_uri @@ -97,5 +95,4 @@ let set_roots ~token ~debug ~roots = let init_agent ~token ~debug ~roots = init_st := Some (init_coq ~debug); Fleche.Io.CallBack.set io; - Agent.fn := fn; set_roots ~token ~debug ~roots diff --git a/petanque/shell.mli b/petanque/shell.mli index 2b57dc76..a4409062 100644 --- a/petanque/shell.mli +++ b/petanque/shell.mli @@ -18,3 +18,8 @@ val set_workspace : -> debug:bool -> root:Lang.LUri.File.t -> unit Agent.R.t + +val build_doc : + token:Coq.Limits.Token.t + -> uri:Lang.LUri.File.t + -> (Fleche.Doc.t, Agent.Error.t) Result.t diff --git a/petanque/test/basic_api.ml b/petanque/test/basic_api.ml index ae4dbc8b..42707098 100644 --- a/petanque/test/basic_api.ml +++ b/petanque/test/basic_api.ml @@ -27,7 +27,10 @@ let start ~token = let root, uri = prepare_paths () in let* () = Petanque.Shell.set_workspace ~token ~debug ~root in let* () = Petanque.Shell.set_workspace ~token ~debug ~root in - Agent.start ~token ~uri ~thm:"rev_snoc_cons" () + (* Careful to call [build_doc] before we have set an environment! [pet] and + [pet-server] are careful to always set a default one *) + let* doc = Petanque.Shell.build_doc ~token ~uri in + Agent.start ~token ~doc ~thm:"rev_snoc_cons" () let extract_st (st : _ Agent.Run_result.t) = match st with