Merge pull request #194 from tlaplus/fix-lsp-obl-state-aggr

LSP: Use maximum obligation status instead of latest.

Author: kape1395

Diff for: lsp/lib/docs/obl.ml

@@ -8,6 +8,7 @@ module Role = struct
     | Unknown  (** Initially all the obligations are of unknown role. *)
     | Unexpected
         (** Was not received from the parser, but got later from the prover. *)
+  [@@deriving show]
 
   let as_string = function
     | Main -> "main"
@@ -16,9 +17,26 @@ module Role = struct
     | Unexpected -> "unexpected"
 end
 
+(** We define obligation's map explicitly to have ability to print it. *)
+module ObligationByProverMap = struct
+  include StrMap
+
+  type t = Toolbox.Obligation.t StrMap.t
+
+  let pp ppf (m : t) =
+    let it =
+      iter
+        (fun k v ->
+          Format.fprintf ppf "@[%s -> %a;@]" k Toolbox.Obligation.pp v)
+        m
+    in
+    it
+end
+
 type t = {
   role : Role.t;
   parsed : Tlapm_lib.Proof.T.obligation option;
+      [@printer fun _ fmt -> Printf.ifprintf fmt "...skipped..."]
       (** The obligation as received from the parser. *)
   parsed_text_plain : string option Lazy.t;  (** Works as a cache. *)
   parsed_text_normalized : string option Lazy.t;  (** Works as a cache. *)
@@ -27,11 +45,12 @@ type t = {
           reset all the prover results. *)
   p_obl_id : int option;  (** Obligation ID, as assigned by the prover. *)
   checking : bool;  (** Is obligation checking currently running? *)
-  by_prover : Toolbox.Obligation.t StrMap.t;
+  by_prover : ObligationByProverMap.t;
   prover_names : string list option;
   latest_prover : string option;
   status : Proof_status.t;
 }
+[@@deriving show]
 
 let obl_to_str obl =
   let buf = Buffer.create 100 in
@@ -43,7 +62,7 @@ let obl_to_str obl =
 let obl_to_normalized_str obl =
   obl_to_str (Tlapm_lib.Backend.Toolbox.normalize true obl)
 
-let of_parsed_obligation (parsed : Tlapm_lib.Proof.T.obligation) status =
+let of_parsed_obligation (parsed : Tlapm_lib.Proof.T.obligation) =
   let parsed_text_plain = lazy (Some (obl_to_str parsed)) in
   let parsed_text_normalized = lazy (Some (obl_to_normalized_str parsed)) in
   {
@@ -54,10 +73,10 @@ let of_parsed_obligation (parsed : Tlapm_lib.Proof.T.obligation) status =
     p_ref = 0;
     p_obl_id = None;
     checking = false;
-    by_prover = StrMap.empty;
+    by_prover = ObligationByProverMap.empty;
     prover_names = None;
     latest_prover = None;
-    status;
+    status = Pending;
   }
 
 let reset obl p_ref =
@@ -66,7 +85,7 @@ let reset obl p_ref =
     p_ref;
     p_obl_id = None;
     checking = false;
-    by_prover = StrMap.empty;
+    by_prover = ObligationByProverMap.empty;
     prover_names = None;
     latest_prover = None;
     status = Proof_status.Pending;
@@ -82,7 +101,7 @@ let loc obl =
       (match obl.latest_prover with
       | None ->
           assert false (* there should be either parsed info or prover result *)
-      | Some prover -> StrMap.find prover obl.by_prover)
+      | Some prover -> ObligationByProverMap.find prover obl.by_prover)
         .loc
   | Some parsed -> Range.of_locus_must (Tlapm_lib.Util.get_locus parsed.obl)
 
@@ -105,7 +124,9 @@ let is_final obl =
       match obl.prover_names with
       | None -> false
       | Some prover_names ->
-          let have_prover_result pn = StrMap.mem pn obl.by_prover in
+          let have_prover_result pn =
+            ObligationByProverMap.mem pn obl.by_prover
+          in
           List.for_all have_prover_result prover_names)
 
 let status obl = if obl.checking then Proof_status.Progress else obl.status
@@ -119,12 +140,12 @@ let latest_status_msg obl =
   | None -> Proof_status.to_message obl.status
   | Some prover ->
       Toolbox.tlapm_obl_state_to_string
-        (StrMap.find prover obl.by_prover).status
+        (ObligationByProverMap.find prover obl.by_prover).status
 
 let latest_obl_text obl =
   match obl.latest_prover with
   | None -> text_normalized obl
-  | Some prover -> (StrMap.find prover obl.by_prover).obl
+  | Some prover -> (ObligationByProverMap.find prover obl.by_prover).obl
 
 let with_prover_terminated p_ref (obl : t) =
   if obl.p_ref <= p_ref then { obl with checking = false } else obl
@@ -144,7 +165,7 @@ let with_prover_obligation p_ref (tlapm_obl : Toolbox.Obligation.t)
           (* To have it reset bellow. *)
           p_obl_id = None;
           checking = false;
-          by_prover = StrMap.empty;
+          by_prover = ObligationByProverMap.empty;
           prover_names = None;
           latest_prover = None;
           status = Proof_status.Pending;
@@ -156,12 +177,17 @@ let with_prover_obligation p_ref (tlapm_obl : Toolbox.Obligation.t)
       match Toolbox.Obligation.(tlapm_obl.prover) with
       | None -> obl
       | Some prover ->
-          {
-            obl with
-            by_prover = StrMap.add prover tlapm_obl obl.by_prover;
-            latest_prover = Some prover;
-            status = Proof_status.of_tlapm_obl_state tlapm_obl.status;
-          }
+          let latest_prover = Some prover in
+          let by_prover =
+            ObligationByProverMap.add prover tlapm_obl obl.by_prover
+          in
+          let status =
+            ObligationByProverMap.fold
+              (fun _ (o : Toolbox.Obligation.t) acc ->
+                Proof_status.max (Proof_status.of_tlapm_obl_state o.status) acc)
+              by_prover Pending
+          in
+          { obl with by_prover; latest_prover; status }
     in
     { obl with p_obl_id = Some tlapm_obl.id; checking = not (is_final obl) }
   in
@@ -246,10 +272,12 @@ let as_lsp_tlaps_proof_obligation_state obl =
     let final = is_final obl in
     match obl.prover_names with
     | None ->
-        List.map (fun (_pn, o) -> make_result o) (StrMap.to_list obl.by_prover)
+        List.map
+          (fun (_pn, o) -> make_result o)
+          (ObligationByProverMap.to_list obl.by_prover)
     | Some prover_names ->
         let planned pn =
-          match StrMap.find_opt pn obl.by_prover with
+          match ObligationByProverMap.find_opt pn obl.by_prover with
           | None -> if final then None else Some (make_pending pn)
           | Some o -> Some (make_result o)
         in
@@ -258,7 +286,12 @@ let as_lsp_tlaps_proof_obligation_state obl =
         in
         List.append
           (List.filter_map planned prover_names)
-          (List.filter_map unplanned (StrMap.to_list obl.by_prover))
+          (List.filter_map unplanned
+             (ObligationByProverMap.to_list obl.by_prover))
   in
   Structs.TlapsProofObligationState.make ~role ~range ~status ~normalized
     ~results
+
+let%test_unit "Check Role.pp" =
+  Format.printf "%a" Role.pp Role.Unexpected;
+  assert ("Obl.Role.Unexpected" = Role.show Role.Unexpected)

Diff for: lsp/lib/docs/obl.mli

@@ -7,7 +7,7 @@ end
 
 type t
 
-val of_parsed_obligation : Tlapm_lib.Proof.T.obligation -> Proof_status.t -> t
+val of_parsed_obligation : Tlapm_lib.Proof.T.obligation -> t
 val with_role : Role.t -> t -> t
 val with_prover_terminated : int -> t -> t
 val with_prover_obligation : int -> Toolbox.Obligation.t -> t option -> t

Diff for: lsp/lib/docs/proof_status.ml

@@ -1,6 +1,7 @@
 open Prover
 
 type t = Proved | Failed | Omitted | Missing | Pending | Progress
+[@@deriving show]
 
 let of_tlapm_obl_state = function
   | Toolbox.ToBeProved -> Progress
@@ -28,25 +29,29 @@ let to_message = function
   | Pending -> "Proof pending."
   | Proved -> "Proof checked successfully."
 
+(** For a proof step, we will take the maximum of statuses returned by different
+    provers for each obligation and the minimum across the obligations. *)
 let to_order = function
-  | Failed -> 0
-  | Missing -> 1
-  | Omitted -> 2
-  | Progress -> 3
-  | Pending -> 4
+  | Pending -> 0
+  | Failed -> 1
+  | Missing -> 2
+  | Omitted -> 3
+  | Progress -> 4
   | Proved -> 5
 
 let of_order = function
-  | 0 -> Failed
-  | 1 -> Missing
-  | 2 -> Omitted
-  | 3 -> Progress
-  | 4 -> Pending
+  | 0 -> Pending
+  | 1 -> Failed
+  | 2 -> Missing
+  | 3 -> Omitted
+  | 4 -> Progress
   | 5 -> Proved
   | _ -> failwith "Impossible order"
 
+let bot = Pending
 let top = Proved
 let min a b = of_order (min (to_order a) (to_order b))
+let max a b = of_order (max (to_order a) (to_order b))
 let yojson_of_t t = `String (to_string t)
 
 let is_diagnostic = function

Diff for: lsp/lib/docs/proof_status.mli

@@ -1,14 +1,17 @@
 open Prover
 
 type t = Proved | Failed | Omitted | Missing | Pending | Progress
+[@@deriving show]
 
 val of_tlapm_obl_state : Toolbox.tlapm_obl_state -> t
 val to_string : t -> string
 val to_message : t -> string
 val to_order : t -> int
 val of_order : int -> t
+val bot : t
 val top : t
 val min : t -> t -> t
+val max : t -> t -> t
 val yojson_of_t : t -> Yojson.Safe.t
 
 val is_diagnostic : t -> bool

Diff for: lsp/lib/docs/proof_step.ml

@@ -395,7 +395,7 @@ let of_module (mule : Tlapm_lib.Module.T.mule) prev : t option =
           | None -> Tlapm_lib.Backend.Fingerprints.write_fingerprint o
           | Some _ -> o
         in
-        let o = Obl.of_parsed_obligation o Proof_status.Pending in
+        let o = Obl.of_parsed_obligation o in
         let o = Obl.with_proof_state_from o (Hashtbl.find_opt prev_obs) in
         Some (o_range, o)
       in

Diff for: lsp/lib/dune

@@ -9,6 +9,6 @@
   ; (flags -only-test docs/proof_step.ml -verbose)
   )
  (preprocess
-  (pps ppx_inline_test)))
+  (pps ppx_inline_test ppx_deriving.show)))
 
 (include_subdirs qualified)

Diff for: lsp/lib/prover/prover.mli

@@ -26,6 +26,7 @@ module Toolbox : sig
       already : bool option;
       obl : string option;
     }
+    [@@deriving show]
   end
 
   type tlapm_notif_severity = TlapmNotifError | TlapmNotifWarning

Diff for: lsp/lib/prover/toolbox.ml

@@ -7,6 +7,7 @@ type tlapm_obl_state =
   | Interrupted
   | Trivial
   | Unknown of string
+[@@deriving show]
 
 let tlapm_obl_state_of_string s =
   match s with
@@ -42,7 +43,9 @@ module Obligation = struct
     reason : string option;
     already : bool option;
     obl : string option;
+        [@printer fun _ fmt -> Printf.ifprintf fmt "...skipped..."]
   }
+  [@@deriving show]
 
   (** This is for testing only. *)
   module Test = struct

Diff for: lsp/lib/prover/toolbox.mli

@@ -9,6 +9,7 @@ type tlapm_obl_state =
   | Interrupted
   | Trivial
   | Unknown of string
+[@@deriving show]
 
 val tlapm_obl_state_to_string : tlapm_obl_state -> string
 
@@ -24,6 +25,7 @@ module Obligation : sig
     already : bool option;
     obl : string option;
   }
+  [@@deriving show]
 
   (** For testing only. *)
   module Test : sig

Diff for: lsp/lib/range.ml

@@ -3,7 +3,7 @@
 module LspT = Lsp.Types
 
 module Position : sig
-  type t
+  type t [@@deriving show]
 
   val make : int -> int -> t
   val of_pair : int * int -> t
@@ -16,7 +16,7 @@ module Position : sig
   val max : t -> t -> t
   val line : t -> int
 end = struct
-  type t = P of int * int
+  type t = P of int * int [@@deriving show]
 
   let make l c = P (l, c)
   let of_pair (l, c) = P (l, c)
@@ -43,7 +43,7 @@ end = struct
   let line (P (l, _)) = l
 end
 
-type t = R of (int * int) * (int * int)
+type t = R of (int * int) * (int * int) [@@deriving show]
 
 let line_from (R ((fl, _), _)) = fl
 let line_till (R (_, (tl, _))) = tl

Diff for: lsp/lib/range.mli

@@ -1,12 +1,12 @@
 module LspT := Lsp.Types
 
 module Position : sig
-  type t
+  type t [@@deriving show]
 
   val compare : t -> t -> int
 end
 
-type t
+type t [@@deriving show]
 
 val from : t -> Position.t
 val till : t -> Position.t