Code re-formatted under ./lsp.

No real changes are made, only changes done by `(cd lsp; dune fmt)`. This is to make other PRs less cluttered by the reformatted comments, etc. Signed-off-by: Karolis Petrauskas <[email protected]>
tlaplus · Jan 6, 2025 · c5e566b · c5e566b
1 parent 9df048d
commit c5e566b
Show file tree

Hide file tree

Showing 23 changed files with 111 additions and 112 deletions.
diff --git a/.ocamlformat b/.ocamlformat
@@ -1,2 +1,2 @@
-version=0.26.2
+version=0.27.0
 profile=default
diff --git a/lsp/lib/docs/doc.mli b/lsp/lib/docs/doc.mli
@@ -1,4 +1,5 @@
-(** Represents a document identified by its uri. It can contain multiple versions and all the related info. *)
+(** Represents a document identified by its uri. It can contain multiple
+    versions and all the related info. *)
 
 open Util
 

diff --git a/lsp/lib/docs/doc_actual.ml b/lsp/lib/docs/doc_actual.ml
@@ -8,9 +8,9 @@ module Parsed = struct
   type t = {
     nts : Toolbox.tlapm_notif list;
     ps : Proof_step.t option;
-        (** Parsed document structure, a tree of proof steps.
-          It is obtained by parsing the document and then updated
-          when obligation proof states are received from the prover. *)
+        (** Parsed document structure, a tree of proof steps. It is obtained by
+            parsing the document and then updated when obligation proof states
+            are received from the prover. *)
   }
 
   let make ~uri ~(doc_vsn : Doc_vsn.t) ~(ps_prev : Proof_step.t option) ~parser
@@ -42,9 +42,9 @@ type t = {
       (** Parsed document and information derived from it. *)
 }
 
-(** Create new actual document based on the document version [doc_vsn]
-    and port the current state from the previous actual document
-    [prev_act], if provided. *)
+(** Create new actual document based on the document version [doc_vsn] and port
+    the current state from the previous actual document [prev_act], if provided.
+*)
 let make uri doc_vsn prev_act parser =
   match prev_act with
   | None ->

diff --git a/lsp/lib/docs/doc_proof_res.mli b/lsp/lib/docs/doc_proof_res.mli
@@ -1,6 +1,5 @@
-(** Proof results of a document. Includes the errors returned from the prover
-    as well as all the proof steps with their current state.
-    *)
+(** Proof results of a document. Includes the errors returned from the prover as
+    well as all the proof steps with their current state. *)
 
 open Util
 open Prover

diff --git a/lsp/lib/docs/doc_vsn.mli b/lsp/lib/docs/doc_vsn.mli
@@ -1,7 +1,6 @@
-(** Versions that are collected after the last prover launch or client
-    asks for diagnostics. We store some limited number of versions here,
-    just to cope with async events from the client.
-    *)
+(** Versions that are collected after the last prover launch or client asks for
+    diagnostics. We store some limited number of versions here, just to cope
+    with async events from the client. *)
 
 type t
 

diff --git a/lsp/lib/docs/docs.mli b/lsp/lib/docs/docs.mli
@@ -17,7 +17,7 @@ type t
 (** A document store type. *)
 
 type parser_fun = Util.parser_fun
-(** Parser function to use to parse modules.  *)
+(** Parser function to use to parse modules. *)
 
 type tk = LspT.DocumentUri.t
 (** Key type to identify documents. *)
@@ -38,7 +38,8 @@ val with_parser : t -> parser_fun -> t
 (** Set parser function to use. *)
 
 val add : t -> tk -> int -> string -> t
-(** Either add document or its revision. Forgets all previous unused revisions. *)
+(** Either add document or its revision. Forgets all previous unused revisions.
+*)
 
 val rem : t -> tk -> t
 (** Remove a document with all its revisions. *)
@@ -71,7 +72,8 @@ val prover_terminated : t -> tk -> int -> int -> t * Doc_proof_res.t option
 (** Cleanup the incomplete proof states on termination of the prover. *)
 
 val get_proof_res : t -> tk -> int -> t * Doc_proof_res.t option
-(** Get the actual proof results for the specific version. Cleanup them, if needed. *)
+(** Get the actual proof results for the specific version. Cleanup them, if
+    needed. *)
 
 val get_proof_res_latest : t -> tk -> t * int option * Doc_proof_res.t option
 (** Get the latest actual proof results. Cleanup them, if needed. *)
@@ -86,4 +88,5 @@ val get_proof_step_details :
 
 val get_proof_step_details_latest :
   t -> tk -> Range.Position.t -> t * Structs.TlapsProofStepDetails.t option
-(** Get the current proof state for the specific obligation at the latest version of the document. *)
+(** Get the current proof state for the specific obligation at the latest
+    version of the document. *)
diff --git a/lsp/lib/docs/obl.ml b/lsp/lib/docs/obl.ml
@@ -23,8 +23,8 @@ type t = {
   parsed_text_plain : string option Lazy.t;  (** Works as a cache. *)
   parsed_text_normalized : string option Lazy.t;  (** Works as a cache. *)
   p_ref : int;
-      (** We collect proof info in a scope of p_ref only.
-          For each new p_ref we reset all the prover results. *)
+      (** We collect proof info in a scope of p_ref only. For each new p_ref we
+          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;
@@ -95,8 +95,8 @@ let is_for_obl_id obl p_ref obl_id =
     match obl.p_obl_id with None -> false | Some id -> id = obl_id
   else false
 
-(** Either there exist a success result (the latest one),
-    or we have outputs from all the provers. *)
+(** Either there exist a success result (the latest one), or we have outputs
+    from all the provers. *)
 let is_final obl =
   match obl.status with
   | Pending | Progress -> false
@@ -112,8 +112,8 @@ let status obl = if obl.checking then Proof_status.Progress else obl.status
 let text_plain obl = Lazy.force obl.parsed_text_plain
 let text_normalized obl = Lazy.force obl.parsed_text_normalized
 
-(** Try to get most detailed status message.
-    Take it from the prover result, if exist. *)
+(** Try to get most detailed status message. Take it from the prover result, if
+    exist. *)
 let latest_status_msg obl =
   match obl.latest_prover with
   | None -> Proof_status.to_message obl.status

diff --git a/lsp/lib/docs/proof_step.ml b/lsp/lib/docs/proof_step.ml
@@ -1,7 +1,8 @@
 open Util
 open Prover
 
-(** We categorize the proof steps just to make the presentation in the UI clearer. *)
+(** We categorize the proof steps just to make the presentation in the UI
+    clearer. *)
 module Kind = struct
   type t = Module | Struct | Leaf
 
@@ -13,31 +14,30 @@ end
 
 type t = {
   kind : Kind.t;
-      (** Kind/Type of this proof step.
-          We want to show the proof steps differently based in its type. *)
+      (** Kind/Type of this proof step. We want to show the proof steps
+          differently based in its type. *)
   status_parsed : Proof_status.t option;
-      (** Status derived at the parse time, if any.
-          This is for the omitted or error cases. *)
+      (** Status derived at the parse time, if any. This is for the omitted or
+          error cases. *)
   status_derived : Proof_status.t;
-      (** Derived status.
-          Here we sum-up the states from all the related obligations and sub-steps. *)
+      (** Derived status. Here we sum-up the states from all the related
+          obligations and sub-steps. *)
   step_loc : Range.t;
-      (** Location of the entire step.
-          It starts with a statement/sequent and ends with the BY keyword (inclusive),
-          not including the listed facts and definitions. In the case of a structured
-          proof, this ends with the BY keyword of the corresponding QED step. *)
+      (** Location of the entire step. It starts with a statement/sequent and
+          ends with the BY keyword (inclusive), not including the listed facts
+          and definitions. In the case of a structured proof, this ends with the
+          BY keyword of the corresponding QED step. *)
   head_loc : Range.t;
-      (** The location of the proof sequent.
-          It is always contained within the [step_loc].
-          This is shown as a step in the UI. *)
+      (** The location of the proof sequent. It is always contained within the
+          [step_loc]. This is shown as a step in the UI. *)
   full_loc : Range.t;
-      (** [step_loc] plus all the BY facts included.
-          If an obligation is in [full_loc] but not in the [step_loc],
-          we consider it supplementary (will be shown a bit more hidden). *)
+      (** [step_loc] plus all the BY facts included. If an obligation is in
+          [full_loc] but not in the [step_loc], we consider it supplementary
+          (will be shown a bit more hidden). *)
   obs : Obl.t RangeMap.t;
-      (** Obligations associated with this step.
-          Here we include all the obligations fitting into [full_loc],
-          but not covered by any of the [sub] steps. *)
+      (** Obligations associated with this step. Here we include all the
+          obligations fitting into [full_loc], but not covered by any of the
+          [sub] steps. *)
   sub : t list; (* Sub-steps, if any. *)
 }
 
@@ -290,13 +290,15 @@ and of_step (step : Tlapm_lib.Proof.T.step) acc : t option * Acc.t =
         (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)
   | Proof.T.TakeTuply tuply_bounds ->
       let suppl_locs =
-        List.concat (List.map (fun (tuply_name, _) ->
-          begin match tuply_name with
-          | Expr.T.Bound_name hint ->
-            List.filter_map Range.of_wrapped [ hint ]
-          | Expr.T.Bound_names hints ->
-            List.filter_map Range.of_wrapped hints
-          end) tuply_bounds)
+        List.concat
+          (List.map
+             (fun (tuply_name, _) ->
+               match tuply_name with
+               | Expr.T.Bound_name hint ->
+                   List.filter_map Range.of_wrapped [ hint ]
+               | Expr.T.Bound_names hints ->
+                   List.filter_map Range.of_wrapped hints)
+             tuply_bounds)
       in
       Acc.some
         (of_implicit_proof_step (Range.of_wrapped_must step) suppl_locs acc)

diff --git a/lsp/lib/docs/proof_step.mli b/lsp/lib/docs/proof_step.mli
@@ -1,8 +1,6 @@
-(** Proof step, as it is displayed in the editor.
-    The proof steps are obtained by parsing the TLAPS source file.
-    Later the proof obligation info is added to the tree as they are
-    obtained from the prover.
-    *)
+(** Proof step, as it is displayed in the editor. The proof steps are obtained
+    by parsing the TLAPS source file. Later the proof obligation info is added
+    to the tree as they are obtained from the prover. *)
 
 open Util
 open Prover

diff --git a/lsp/lib/docs/util.ml b/lsp/lib/docs/util.ml
@@ -1,7 +1,6 @@
-(** Obligation reference consists of the proof session reference (p_ref)
-    and the obligation id (obl_id) as assigned by the TLAPS. This reference
-    is unique across proof attempts.
-    *)
+(** Obligation reference consists of the proof session reference (p_ref) and the
+    obligation id (obl_id) as assigned by the TLAPS. This reference is unique
+    across proof attempts. *)
 module OblRef = struct
   type t = { p_ref : int; obl_id : int }
 

diff --git a/lsp/lib/parser/parser.ml b/lsp/lib/parser/parser.ml
@@ -4,4 +4,4 @@ let module_of_string ~content ~filename ~loader_paths =
       ~prefer_stdlib:true
   with
   | Ok (_mcx, mule) -> Ok mule
-  | Error err -> Error err
+  | Error err -> Error err
diff --git a/lsp/lib/parser/parser.mli b/lsp/lib/parser/parser.mli
@@ -1,6 +1,6 @@
 (** Responsible for parsing the TLA+ documents.
-    TODO: SANY integration should be added here as well.
-    *)
+
+    TODO: SANY integration should be added here as well. *)
 
 val module_of_string :
   content:string ->

diff --git a/lsp/lib/prover/progress.mli b/lsp/lib/prover/progress.mli
@@ -1,7 +1,6 @@
-(** Maintains the proof progress in the client app. Here we use the
-    server initiated progress and cancellation support, because the
-    VSCode don't support the client-initiated workDoneProgress
-    with LSP. *)
+(** Maintains the proof progress in the client app. Here we use the server
+    initiated progress and cancellation support, because the VSCode don't
+    support the client-initiated workDoneProgress with LSP. *)
 
 module LspT := Lsp.Types
 
@@ -21,7 +20,7 @@ module Make (CB : Callbacks) : sig
   (** Create new instance of progress tracker. *)
 
   val is_latest : t -> LspT.ProgressToken.t -> bool
-  (** Checks if the token is of the last progress.  *)
+  (** Checks if the token is of the last progress. *)
 
   val proof_started : p_ref:int -> CB.t -> CB.t
   (** Called when new TLAPM run is initiated. *)

diff --git a/lsp/lib/prover/prover.ml b/lsp/lib/prover/prover.ml
@@ -9,18 +9,19 @@ module Toolbox = Toolbox
 
 (* ***** Prover process management ****************************************** *)
 
-(**
-  Returns the tlapm executable path or error, if there is no such in known places.
-  If installed, both files are in the same dir:
+(** Returns the tlapm executable path or error, if there is no such in known
+    places. If installed, both files are in the same dir:
     - .../bin/tlapm
     - .../bin/tlapm_lsp
-  Otherwise, if that's development environment, the files are:
+
+    Otherwise, if that's development environment, the files are:
     - .../src/tlapm.exe
     - .../lsp/bin/tlapm_lsp.exe
-  And during the inline tests:
+
+    And during the inline tests:
     - .../src/tlapm.exe
     - .../lsp/lib/.tlapm_lsp_lib.inline-tests/inline_test_runner_tlapm_lsp_lib.exe
-  *)
+*)
 let tlapm_exe () =
   let open Filename in
   let this_exe = Sys.executable_name in

diff --git a/lsp/lib/prover/prover.mli b/lsp/lib/prover/prover.mli
@@ -66,7 +66,7 @@ module Progress : sig
     (** Create new instance of progress tracker. *)
 
     val is_latest : t -> LspT.ProgressToken.t -> bool
-    (** Checks if the token is of the last progress.  *)
+    (** Checks if the token is of the last progress. *)
 
     val proof_started : p_ref:int -> CB.t -> CB.t
     (** Called when new TLAPM run is initiated. *)
@@ -75,7 +75,8 @@ module Progress : sig
     (** Called when a number of obligations is received from the TLAPM. *)
 
     val obligation_done : p_ref:int -> obl_id:int -> CB.t -> CB.t
-    (** Called when some proof obligation state change is received from TLAPM. *)
+    (** Called when some proof obligation state change is received from TLAPM.
+    *)
 
     val proof_ended : p_ref:int -> CB.t -> CB.t
     (** Called when the TLAPM terminates. *)

diff --git a/lsp/lib/range.ml b/lsp/lib/range.ml
@@ -122,7 +122,8 @@ let lines_intersect a b =
   let ltb = line_till b in
   lfa <= ltb && lfb <= lta
 
-(** [line_covered r p] is true, if the line of position [p] intersects with the range [r] lines. *)
+(** [line_covered r p] is true, if the line of position [p] intersects with the
+    range [r] lines. *)
 let line_covered r p =
   let l = Position.line p in
   line_from r <= l && l <= line_till r

diff --git a/lsp/lib/server/codec.mli b/lsp/lib/server/codec.mli
@@ -1,7 +1,6 @@
-(**
-Here we construct a decoder/encoder for the LSP protocol on top of Eio flows.
-We use the lsp module from the ocaml-lsp server and configure it to run over Eio.
-*)
+(** Here we construct a decoder/encoder for the LSP protocol on top of Eio
+    flows. We use the lsp module from the ocaml-lsp server and configure it to
+    run over Eio. *)
 
 type trace_fun = string -> unit
 type input_chan = Eio.Buf_read.t * trace_fun

diff --git a/lsp/lib/server/handlers.ml b/lsp/lib/server/handlers.ml
@@ -129,16 +129,16 @@ module Make (CB : Callbacks) = struct
              ~workDoneProgress:true ())
         ~diagnosticProvider:
           (`DiagnosticOptions
-            (DiagnosticOptions.create ~identifier:CB.diagnostic_source
-               ~interFileDependencies:false ~workspaceDiagnostics:false
-               ~workDoneProgress:false ()))
+             (DiagnosticOptions.create ~identifier:CB.diagnostic_source
+                ~interFileDependencies:false ~workspaceDiagnostics:false
+                ~workDoneProgress:false ()))
         ~codeActionProvider:
           (`CodeActionOptions
-            (CodeActionOptions.create ~resolveProvider:false
-               ~workDoneProgress:false
-               ~codeActionKinds:
-                 [ CodeActionKind.Other "tlaplus.tlaps.check-step.ca" ]
-               ()))
+             (CodeActionOptions.create ~resolveProvider:false
+                ~workDoneProgress:false
+                ~codeActionKinds:
+                  [ CodeActionKind.Other "tlaplus.tlaps.check-step.ca" ]
+                ()))
         ~experimental:
           Structs.ServerCapabilitiesExperimental.(
             yojson_of_t
@@ -280,10 +280,8 @@ module Make (CB : Callbacks) = struct
           (Printf.sprintf "command unknown: %s" unknown)
           cb_state
 
-  (**
-    Provide code actions for a document.
-    - Code actions can be used for proof decomposition, probably.
-  *)
+  (** Provide code actions for a document.
+      - Code actions can be used for proof decomposition, probably. *)
   let handle_jsonrpc_req_code_action (jsonrpc_req : Jsonrpc.Request.t)
       (params : LspT.CodeActionParams.t) cb_state =
     let user_range = params.range in

diff --git a/lsp/lib/server/handlers.mli b/lsp/lib/server/handlers.mli
@@ -18,8 +18,8 @@ module type Callbacks = sig
 
   val track_obligation_proof_state :
     t -> LspT.DocumentUri.t -> LspT.Range.t -> t
-  (** User selected a position in a document, we have to provide the
-      obligation info for it. The information has to be re-sent on update. *)
+  (** User selected a position in a document, we have to provide the obligation
+      info for it. The information has to be re-sent on update. *)
 
   val latest_diagnostics :
     t -> LspT.DocumentUri.t -> t * (int * LspT.Diagnostic.t list)

diff --git a/lsp/lib/server/server.ml b/lsp/lib/server/server.ml
@@ -5,7 +5,8 @@ module Structs = Structs
 (** 50 MB should be enough. *)
 let max_size = 50 * 1024 * 1024
 
-(** The proof info updates are aggregated for 0.5s before sending them to IDE. *)
+(** The proof info updates are aggregated for 0.5s before sending them to IDE.
+*)
 let timer_tick_period = 0.5
 
 type transport = Stdio | Socket of int