Progress is now shown.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

lsp/lib/tlapm_lsp_docs.ml

@@ -241,7 +241,23 @@ end = struct
     TlapmRange.lines_covered_or_all input pss_locs
 end
 
-type proof_res = int * tlapm_obligation list * tlapm_notif list * PS.t list
+module ProofRes = struct
+  type t = {
+    p_ref : int;
+    obs : tlapm_obligation list;
+    nts : tlapm_notif list;
+    pss : PS.t list;
+  }
+
+  let empty = { p_ref = 0; obs = []; nts = []; pss = [] }
+
+  let obs_done t =
+    List.fold_left
+      (fun acc ob ->
+        if ToolboxProtocol.tlapm_obl_state_is_terminal ob.status then acc + 1
+        else acc)
+      0 t.obs
+end
 
 (** Versions that are collected after the last prover launch or client
     asks for diagnostics. We store some limited number of versions here,
@@ -274,10 +290,9 @@ module TA : sig
   val text : t -> string
   val merge_into : t -> TV.t -> t
   val try_parse : t -> LspT.DocumentUri.t -> t
-  val proof_res : t -> proof_res
+  val proof_res : t -> ProofRes.t
   val prepare_proof : t -> LspT.DocumentUri.t -> int -> t option
   val locate_proof_range : t -> TlapmRange.t -> TlapmRange.t
-  val obl_num : t -> int -> t option
   val add_obl : t -> int -> tlapm_obligation -> t option
   val add_notif : t -> int -> tlapm_notif -> t option
   val terminated : t -> int -> t option
@@ -342,9 +357,14 @@ end = struct
     | { mule = None; _ } -> try_parse_anyway uri act
     | { mule = Some _; _ } -> act
 
-  let proof_res (act : t) =
+  let proof_res (act : t) : ProofRes.t =
     let obs_list = List.map snd (OblMap.to_list act.obs) in
-    (act.p_ref, obs_list, act.nts, PS.flatten act.pss)
+    {
+      p_ref = act.p_ref;
+      obs = obs_list;
+      nts = act.nts;
+      pss = PS.flatten act.pss;
+    }
 
   let prepare_proof (act : t) uri next_p_ref =
     let act = try_parse act uri in
@@ -354,12 +374,6 @@ end = struct
 
   let locate_proof_range act range = PS.locate_proof_range act.pss range
 
-  let obl_num (act : t) p_ref =
-    if act.p_ref = p_ref then
-      (* TODO: Handle the work progress based on this. *)
-      Some act
-    else None
-
   let add_obl (act : t) (p_ref : int) (obl : tlapm_obligation) =
     if act.p_ref = p_ref then
       let drop_older_intersecting (o_pr, _o_id) (o : tlapm_obligation) =
@@ -478,7 +492,7 @@ let with_doc_vsn docs uri vsn f =
 
 (* Push specific version to the actual, increase the proof_rec and clear the notifications. *)
 let prepare_proof docs uri vsn range :
-    t * (int * string * TlapmRange.t * proof_res) option =
+    t * (int * string * TlapmRange.t * ProofRes.t) option =
   with_doc_vsn docs uri vsn @@ fun (doc : TD.t) (act : TA.t) ->
   let next_doc, next_p_ref = TD.next_p_ref doc in
   match TA.prepare_proof act uri next_p_ref with
@@ -497,12 +511,6 @@ let suggest_proof_range docs uri range : t * (int * TlapmRange.t) option =
       let p_range = TA.locate_proof_range act range in
       (doc, act, Some (vsn, p_range))
 
-let obl_num docs uri vsn p_ref =
-  with_doc_vsn docs uri vsn @@ fun (doc : TD.t) (act : TA.t) ->
-  match TA.obl_num act p_ref with
-  | None -> (doc, act, None)
-  | Some act -> (doc, act, Some (TA.proof_res act))
-
 let add_obl docs uri vsn p_ref (obl : tlapm_obligation) =
   with_doc_vsn docs uri vsn @@ fun (doc : TD.t) (act : TA.t) ->
   match TA.add_obl act p_ref obl with

lsp/lib/tlapm_lsp_docs.mli

@@ -15,8 +15,18 @@ type t
 type tk = Lsp.Types.DocumentUri.t
 (** Key type to identify documents. *)
 
-type proof_res = int * tlapm_obligation list * tlapm_notif list * PS.t list
 (** Result of an update, returns an actual list of obligations and errors. *)
+module ProofRes : sig
+  type t = {
+    p_ref : int;
+    obs : tlapm_obligation list;
+    nts : tlapm_notif list;
+    pss : PS.t list;
+  }
+
+  val empty : t
+  val obs_done : t -> int
+end
 
 val empty : t
 (** Create new empty document store. *)
@@ -32,27 +42,24 @@ val prepare_proof :
   tk ->
   int ->
   TlapmRange.t ->
-  t * (int * string * TlapmRange.t * proof_res) option
+  t * (int * string * TlapmRange.t * ProofRes.t) option
 (** Increment the prover ref for the specified doc/vsn. *)
 
 val suggest_proof_range :
   t -> tk -> TlapmRange.t -> t * (int * TlapmRange.t) option
 (** Suggest proof range based on the user selection. *)
 
-val obl_num : t -> tk -> int -> int -> t * proof_res option
-(** We got the obligation number for the current proof invocation. *)
-
-val add_obl : t -> tk -> int -> int -> tlapm_obligation -> t * proof_res option
+val add_obl : t -> tk -> int -> int -> tlapm_obligation -> t * ProofRes.t option
 (** Record obligation for the document, clear all the intersecting ones. *)
 
-val add_notif : t -> tk -> int -> int -> tlapm_notif -> t * proof_res option
+val add_notif : t -> tk -> int -> int -> tlapm_notif -> t * ProofRes.t option
 (** Record obligation for the document, clear all the intersecting ones. *)
 
-val terminated : t -> tk -> int -> int -> t * proof_res option
+val terminated : t -> tk -> int -> int -> t * ProofRes.t option
 (** Cleanup the incomplete proof states on termination of the prover. *)
 
-val get_proof_res : t -> tk -> int -> t * proof_res option
+val get_proof_res : t -> tk -> int -> t * ProofRes.t option
 (** Get the latest actual proof results. Cleanup them, if needed. *)
 
-val get_proof_res_latest : t -> tk -> t * int option * proof_res option
+val get_proof_res_latest : t -> tk -> t * int option * ProofRes.t option
 (** Get the latest actual proof results. Cleanup them, if needed. *)

lsp/lib/tlapm_lsp_progress.ml

@@ -1,5 +1,42 @@
 module LspT = Lsp.Types
 
+type t = {
+  p_ref : int;
+  token : LspT.ProgressToken.t;
+  started : bool;
+  ended : bool;
+  obl_count : int option; (* Total number of proof obligations. *)
+  obl_done : int; (* Number of obligations already checked. *)
+}
+
+let title = "Checking TLA+ proofs"
+
+let message pr =
+  match pr.obl_count with
+  | None -> "Obligation count unknown."
+  | Some total ->
+      Format.sprintf "%d of %d obligations checked" pr.obl_done total
+
+let percentage pr =
+  match pr.obl_count with
+  | None -> 0
+  | Some 0 -> 100
+  | Some obl_count -> pr.obl_done * 100 / obl_count
+
+let token p_ref = `String (Format.sprintf "tlapm_lsp-p_ref-%d" p_ref)
+
+let reset p_ref ended =
+  {
+    p_ref;
+    token = token p_ref;
+    started = ended;
+    ended;
+    obl_count = None;
+    obl_done = 0;
+  }
+
+let make () = reset 0 true
+
 module type Callbacks = sig
   type t
 
@@ -8,42 +45,6 @@ module type Callbacks = sig
 end
 
 module Make (CB : Callbacks) = struct
-  type t = {
-    p_ref : int;
-    token : LspT.ProgressToken.t;
-    started : bool;
-    ended : bool;
-    obl_count : int option; (* Total number of proof obligations. *)
-    obl_done : int; (* Number of obligations already checked. *)
-  }
-
-  let title = "Checking TLA+ proofs"
-
-  let message pr =
-    match pr.obl_count with
-    | None -> "Obligation count unknown."
-    | Some total ->
-        Format.sprintf "%d of %d obligations checked" total pr.obl_done
-
-  let percentage pr =
-    match pr.obl_count with
-    | None -> 0
-    | Some obl_count -> pr.obl_done * 100 / obl_count
-
-  let token p_ref = `String (Format.sprintf "tlapm_lsp-p_ref-%d" p_ref)
-
-  let reset p_ref ended =
-    {
-      p_ref;
-      token = token p_ref;
-      started = ended;
-      ended;
-      obl_count = None;
-      obl_done = 0;
-    }
-
-  let make () = reset 0 true
-
   (* --------------- Functions creating LSP packets. --------------- *)
 
   let lsp_req_create pr =
@@ -118,7 +119,7 @@ module Make (CB : Callbacks) = struct
       (pr, cb_state)
     else (pr, cb_state)
 
-  let obl_progress pr p_ref obl_done cb_state =
+  let obl_changed pr p_ref obl_done cb_state =
     if
       p_ref = pr.p_ref && pr.started && (not pr.ended)
       && obl_done <> pr.obl_done
@@ -154,12 +155,12 @@ let%test_module "progress reporting tests" =
 
     let%test_unit "basic" =
       let cb = TestCB.fresh in
-      let pr = TestPr.make () in
+      let pr = make () in
       let p_ref = 1 in
       let pr, cb = TestPr.proof_started pr p_ref cb in
       let pr, cb = TestPr.obl_num pr p_ref 10 cb in
-      let pr, cb = TestPr.obl_progress pr p_ref 5 cb in
-      let pr, cb = TestPr.obl_progress pr p_ref 10 cb in
+      let pr, cb = TestPr.obl_changed pr p_ref 5 cb in
+      let pr, cb = TestPr.obl_changed pr p_ref 10 cb in
       let _pr, cb = TestPr.proof_ended pr p_ref cb in
       match List.length cb.sent with
       | 5 -> ()

lsp/lib/tlapm_lsp_progress.mli

@@ -3,28 +3,27 @@
     VSCode don't support the client-initiated workDoneProgress
     with LSP. *)
 
+type t
+
+val make : unit -> t
+(** Create new instance of progress tracker. *)
+
 module type Callbacks = sig
   type t
 
   val next_req_id : t -> Jsonrpc.Id.t * t
   val lsp_send : t -> Jsonrpc.Packet.t -> t
 end
 
-(* TODO: Use it in the Docs. *)
 (* TODO: Handle the cancelation. *)
 module Make (CB : Callbacks) : sig
-  type t
-
-  val make : unit -> t
-  (** Create new instance of progress tracker. *)
-
   val proof_started : t -> int -> CB.t -> t * CB.t
   (** Called when new TLAPM run is initiated. *)
 
   val obl_num : t -> int -> int -> CB.t -> t * CB.t
   (** Called when a number of obligations is received from the TLAPM. *)
 
-  val obl_progress : t -> int -> int -> CB.t -> t * CB.t
+  val obl_changed : t -> int -> int -> CB.t -> t * CB.t
   (** Called when some proof obligation state change is received from TLAPM. *)
 
   val proof_ended : t -> int -> CB.t -> t * CB.t

lsp/lib/tlapm_lsp_prover.ml

@@ -186,6 +186,17 @@ module ToolboxProtocol = struct
     | Trivial -> "trivial"
     | Unknown s -> "unknown state: " ^ s
 
+  let tlapm_obl_state_is_terminal (s : tlapm_obl_state) : bool =
+    match s with
+    | ToBeProved -> false
+    | BeingProved -> false
+    | Normalized -> false
+    | Proved -> true
+    | Failed -> true
+    | Interrupted -> false
+    | Trivial -> true
+    | Unknown _ -> false
+
   type tlapm_obligation = {
     id : int;
     loc : TlapmRange.t;

lsp/lib/tlapm_lsp_prover.mli

@@ -41,6 +41,7 @@ module ToolboxProtocol : sig
     | Unknown of string
 
   val tlapm_obl_state_to_string : tlapm_obl_state -> string
+  val tlapm_obl_state_is_terminal : tlapm_obl_state -> bool
 
   type tlapm_obligation = {
     id : int;

lsp/lib/tlapm_lsp_server.mli

@@ -2,8 +2,7 @@ type transport = Stdio | Socket of int
 
 (**
 Here we serve the LSP RPC over TCP.
-This module contains only the generic server-related functions,
-the tlapm-specifics is moved to tlapm_lsp_packets.
+This module contains only the generic server-related functions.
 *)
 
 val run :