[internal] [request] Refactor handling of Coq execution in requests

controller/request.ml

@@ -17,6 +17,27 @@
 
 module R = struct
   type t = (Yojson.Safe.t, int * string) Result.t
+
+  let err_code = -32803
+
+  (* We log feedback generated during requests, improve so clients can use this,
+     but it needs conversion of positions. *)
+  let do_feedback feedback = Fleche.Io.Log.feedback feedback
+
+  let print_err ~name e =
+    match e with
+    | Coq.Protect.Error.Anomaly (_loc, msg) | User (_loc, msg) ->
+      Format.asprintf "Error in %s request: %a" name Pp.pp_with msg
+
+  let of_execution ~name ~f x : t =
+    let Coq.Protect.E.{ r; feedback } = f x in
+    do_feedback feedback;
+    match r with
+    | Interrupted -> Error (err_code, name ^ " request interrupted")
+    | Completed (Error e) ->
+      let error_msg = print_err ~name e in
+      Error (err_code, error_msg)
+    | Completed (Ok r) -> r
 end
 
 type document = doc:Fleche.Doc.t -> R.t

controller/request.mli

@@ -17,6 +17,12 @@
 
 module R : sig
   type t = (Yojson.Safe.t, int * string) Result.t
+
+  (* We don't allow to pass the feedback to the [f] handler yet, that's not
+     hard, but I'd suggest waiting until the conversion of character points is
+     working better. *)
+  val of_execution :
+    name:string -> f:('a -> (t, Loc.t) Coq.Protect.E.t) -> 'a -> t
 end
 
 type document = doc:Fleche.Doc.t -> R.t
@@ -43,4 +49,5 @@ module Data : sig
   val serve : doc:Fleche.Doc.t -> t -> R.t
 end
 
+(** Returns an empty list of results for any position / document *)
 val empty : position

controller/rq_goals.ml

@@ -31,45 +31,39 @@ let pp ~pp_format pp =
   | Pp -> Lsp.JCoq.Pp.to_yojson pp
   | Str -> `String (Pp.string_of_ppcmds pp)
 
-(* XXX: Speculative execution here requires more thought, about errors,
-   location, we need to make the request fail if it is not good, etc... Moreover
-   we should tune whether we cache the results; we try this for now. *)
-let parse_and_execute_in tac st =
-  (* Parse tac, loc==FIXME *)
+let parse ~loc tac st =
   let str = Gramlib.Stream.of_string tac in
-  let str = Coq.Parsing.Parsable.make ?loc:None str in
-  match Coq.Parsing.parse ~st str with
-  | Coq.Protect.E.{ r = Interrupted; feedback = _ }
-  | Coq.Protect.E.{ r = Completed (Error _); feedback = _ }
-  | Coq.Protect.E.{ r = Completed (Ok None); feedback = _ } -> None
-  | Coq.Protect.E.{ r = Completed (Ok (Some ast)); feedback = _ } -> (
-    let open Fleche.Memo in
-    (* XXX use the bind in Coq.Protect.E *)
-    match (Interp.eval (st, ast)).res with
-    | Coq.Protect.E.{ r = Interrupted; feedback = _ }
-    | Coq.Protect.E.{ r = Completed (Error _); feedback = _ } -> None
-    | Coq.Protect.E.{ r = Completed (Ok st); feedback = _ } -> Some st)
+  let str = Coq.Parsing.Parsable.make ?loc str in
+  Coq.Parsing.parse ~st str
 
-let run_pretac ?pretac st =
+let parse_and_execute_in ~loc tac st =
+  let open Coq.Protect.E.O in
+  let* ast = parse ~loc tac st in
+  match ast with
+  | Some ast -> (Fleche.Memo.Interp.eval (st, ast)).res
+  (* On EOF we return the previous state, the command was the empty string or a
+     comment *)
+  | None -> Coq.Protect.E.ok st
+
+let run_pretac ~loc ~st pretac =
   match pretac with
-  | None ->
-    (* Debug option *)
-    (* Lsp.Io.trace "goals" "pretac empty"; *)
-    Some st
-  | Some tac -> Fleche.Info.in_state ~st ~f:(parse_and_execute_in tac) st
+  | None -> Coq.Protect.E.ok st
+  | Some tac -> Coq.State.in_stateM ~st ~f:(parse_and_execute_in ~loc tac) st
 
 let get_goal_info ~doc ~point ~mode ~pretac () =
   let open Fleche in
   let node = Info.LC.node ~doc ~point mode in
   match node with
-  | None -> (None, None)
-  | Some node -> (
-    match run_pretac ?pretac node.Doc.Node.state with
-    | None -> (None, None)
-    | Some st ->
-      let goals = Info.Goals.goals ~st in
-      let program = Info.Goals.program ~st in
-      (goals, Some program))
+  | None -> Coq.Protect.E.ok (None, None)
+  | Some node ->
+    let open Coq.Protect.E.O in
+    let st = Doc.Node.state node in
+    (* XXX: Get the location from node *)
+    let loc = None in
+    let* st = run_pretac ~loc ~st pretac in
+    let+ goals = Info.Goals.goals ~st in
+    let program = Info.Goals.program ~st in
+    (goals, Some program)
 
 let goals ~pp_format ~mode ~pretac () ~doc ~point =
   let open Fleche in
@@ -78,11 +72,16 @@ let goals ~pp_format ~mode ~pretac () ~doc ~point =
   let position =
     Lang.Point.{ line = fst point; character = snd point; offset = -1 }
   in
-  let goals, program = get_goal_info ~doc ~point ~mode ~pretac () in
+  let open Coq.Protect.E.O in
+  let+ goals, program = get_goal_info ~doc ~point ~mode ~pretac () in
   let node = Info.LC.node ~doc ~point Exact in
   let messages = mk_messages node in
   let error = Option.bind node mk_error in
   let pp = pp ~pp_format in
   Lsp.JFleche.GoalsAnswer.(
     to_yojson pp { textDocument; position; goals; program; messages; error })
   |> Result.ok
+
+let goals ~pp_format ~mode ~pretac () ~doc ~point =
+  let f () = goals ~pp_format ~mode ~pretac () ~doc ~point in
+  Request.R.of_execution ~name:"goals" ~f ()

controller/rq_hover.ml

@@ -108,7 +108,7 @@ let info_of_id ~st id =
 
 let info_of_id_at_point ~node id =
   let st = node.Fleche.Doc.Node.state in
-  Fleche.Info.in_state ~st ~f:(info_of_id ~st) id
+  Coq.State.in_state ~st ~f:(info_of_id ~st) id
 
 let pp_typ id = function
   | Def typ ->
@@ -122,7 +122,10 @@ let to_list x = Option.cata (fun x -> [ x ]) [] x
 
 let info_type ~contents ~point ~node : string option =
   Option.bind (Rq_common.get_id_at_point ~contents ~point) (fun id ->
-      Option.map (pp_typ id) (info_of_id_at_point ~node id))
+      match info_of_id_at_point ~node id with
+      | Coq.Protect.{ E.r = R.Completed (Ok (Some info)); feedback = _ } ->
+        Some (pp_typ id info)
+      | _ -> None)
 
 let extract_def ~point:_ (def : Vernacexpr.definition_expr) :
     Constrexpr.constr_expr list =

controller/rq_save.ml

@@ -1,19 +1,10 @@
 (** Several todos here in terms of usability *)
 
-let code = -32803
-
-let print_err ~uri e =
-  match e with
-  | Coq.Protect.Error.Anomaly (_loc, msg) | User (_loc, msg) ->
-    Format.asprintf "Error when saving %s: %a"
-      (Lang.LUri.File.to_string_file uri)
-      Pp.pp_with msg
-
 let request ~doc =
-  match Fleche.Doc.save ~doc with
-  | { Coq.Protect.E.r = Interrupted; _ } ->
-    Error (code, "save operation interrupted")
-  | { Coq.Protect.E.r = Completed (Error e); _ } ->
-    let error_msg = print_err ~uri:doc.uri e in
-    Error (code, error_msg)
-  | { Coq.Protect.E.r = Completed (Ok ()); _ } -> Ok `Null
+  let open Coq.Protect.E.O in
+  let f () =
+    (* XXX: What do do with feedback, return to user? *)
+    let+ () = Fleche.Doc.save ~doc in
+    Ok `Null
+  in
+  Request.R.of_execution ~name:"save" ~f ()

coq/protect.ml

@@ -84,6 +84,11 @@ module E = struct
       { r; feedback = feedback @ fb2 }
 
   let ok v = { r = Completed (Ok v); feedback = [] }
+
+  module O = struct
+    let ( let+ ) x f = map ~f x
+    let ( let* ) x f = bind ~f x
+  end
 end
 
 (* Eval with reified exceptions and feedback *)

coq/protect.mli

@@ -37,6 +37,11 @@ module E : sig
   val map_loc : f:('l -> 'm) -> ('a, 'l) t -> ('a, 'm) t
   val bind : f:('a -> ('b, 'l) t) -> ('a, 'l) t -> ('b, 'l) t
   val ok : 'a -> ('a, 'l) t
+
+  module O : sig
+    val ( let+ ) : ('a, 'l) t -> ('a -> 'b) -> ('b, 'l) t
+    val ( let* ) : ('a, 'l) t -> ('a -> ('b, 'l) t) -> ('b, 'l) t
+  end
 end
 
 (** Must be hooked to allow [Protect] to capture the feedback. *)

coq/state.ml

@@ -101,6 +101,11 @@ let in_state ~st ~f a =
   in
   Protect.eval ~f a
 
+let in_stateM ~st ~f a =
+  let open Protect.E.O in
+  let* () = Protect.eval ~f:Vernacstate.unfreeze_full_state st in
+  f a
+
 let admit ~st () =
   let () = Vernacstate.unfreeze_full_state st in
   match st.Vernacstate.interp.lemmas with

coq/state.mli

@@ -20,6 +20,10 @@ val program : st:t -> Declare.OblState.View.t Names.Id.Map.t
     Coq state setting is imperative, so we need to wrap it in protect. *)
 val in_state : st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.t
 
+(** Execute a monadic command in state [st]. *)
+val in_stateM :
+  st:t -> f:('a -> ('b, Loc.t) Protect.E.t) -> 'a -> ('b, Loc.t) Protect.E.t
+
 (** Drop the proofs from the state *)
 val drop_proofs : st:t -> t
 

fleche/info.ml

@@ -147,25 +147,15 @@ module O = Make (Offset)
    information from a document, and the other that further processes it, like
    for goals, possibly executing Coq code. *)
 
-(* XXX: This needs fixing by having a better monad *)
-let in_state ~st ~f node =
-  match Coq.State.in_state ~st ~f node with
-  | { r = Coq.Protect.R.Completed (Result.Ok res); feedback } ->
-    Io.Log.feedback feedback;
-    res
-  | { r = Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted
-    ; feedback
-    } ->
-    Io.Log.feedback feedback;
-    None
-
 (* Related to goal request *)
 module Goals = struct
   let pr_goal st =
     let ppx env sigma x =
       let { Coq.Protect.E.r; feedback } =
         Coq.Print.pr_letype_env ~goal_concl_style:true env sigma x
       in
+      (* XXX: We ideally want to thread this in the monad too, but it'd be
+         better if the printer was more functional *)
       Io.Log.feedback feedback;
       match r with
       | Coq.Protect.R.Completed (Ok pr) -> pr
@@ -177,7 +167,7 @@ module Goals = struct
 
   (* We need to use [in_state] here due to printing not being pure, but we want
      a better design here eventually *)
-  let goals ~st = in_state ~st ~f:pr_goal st
+  let goals ~st = Coq.State.in_state ~st ~f:pr_goal st
   let program ~st = Coq.State.program ~st
 end
 
@@ -194,7 +184,7 @@ module Completion = struct
 
   let candidates ~st prefix =
     let ( let* ) = Option.bind in
-    in_state ~st prefix ~f:(fun prefix ->
+    Coq.State.in_state ~st prefix ~f:(fun prefix ->
         let* p = to_qualid prefix in
         Nametab.completion_canditates p
         |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x))

fleche/info.mli

@@ -50,16 +50,15 @@ end
 module LC : S with module P := LineCol
 module O : S with module P := Offset
 
-(** Helper to absorb errors in state change to [None], needed due to the lack of
-    proper monad in Coq.Protect, to fix soon *)
-val in_state : st:Coq.State.t -> f:('a -> 'b option) -> 'a -> 'b option
-
 (** We move towards a more modular design here, for preprocessing *)
 module Goals : sig
-  val goals : st:Coq.State.t -> Pp.t Coq.Goals.reified_pp option
+  val goals :
+    st:Coq.State.t -> (Pp.t Coq.Goals.reified_pp option, Loc.t) Coq.Protect.E.t
+
   val program : st:Coq.State.t -> Declare.OblState.View.t Names.Id.Map.t
 end
 
 module Completion : sig
-  val candidates : st:Coq.State.t -> string -> string list option
+  val candidates :
+    st:Coq.State.t -> string -> (string list option, Loc.t) Coq.Protect.E.t
 end