From 40ca986dd292d0f3b78240c3049d1b4c98c81940 Mon Sep 17 00:00:00 2001
From: Arthur Carcano <arthur.carcano@ocamlpro.com>
Date: Tue, 6 Aug 2024 11:02:03 +0200
Subject: [PATCH] Document and rename API in wq.ml

---
 src/cmd/cmd_sym.ml              |  2 +-
 src/data_structures/wq.ml       |  2 +-
 src/data_structures/wq.mli      | 14 +++++++++++++-
 src/symbolic/symbolic_choice.ml |  2 +-
 4 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml
index de0305963..00b869aca 100644
--- a/src/cmd/cmd_sym.ml
+++ b/src/cmd/cmd_sym.ml
@@ -53,7 +53,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let pc = Choice.return (Ok ()) in
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
   let thread = Thread_with_memory.init () in
-  let res_queue = Wq.init () in
+  let res_queue = Wq.make () in
   let callback v =
     let open Symbolic_choice_intf in
     match (fail_mode, v) with
diff --git a/src/data_structures/wq.ml b/src/data_structures/wq.ml
index f602a293c..842ec824c 100644
--- a/src/data_structures/wq.ml
+++ b/src/data_structures/wq.ml
@@ -24,7 +24,7 @@ let work_while f q = Synchronizer.work_while f q
 
 let fail = Synchronizer.fail
 
-let init () =
+let make () =
   let q = Queue.create () in
   let writter v condvar =
     let was_empty = Queue.is_empty q in
diff --git a/src/data_structures/wq.mli b/src/data_structures/wq.mli
index 67f81f0f0..24720b1cb 100644
--- a/src/data_structures/wq.mli
+++ b/src/data_structures/wq.mli
@@ -2,20 +2,32 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
+(** Synchronized FIFO queues *)
+
 type !'a t
 
-val init : unit -> 'a t
+(** Create a new queue *)
+val make : unit -> 'a t
 
+(** Add a new element to the queue *)
 val push : 'a -> 'a t -> unit
 
+(** Get an element from the queue. The boolean shall be true to atomically start
+    a new pledge (cf make_pledge) while popping. *)
 val pop : 'a t -> bool -> 'a option
 
+(** Make a new pledge, ie indicate that new elements may be pushed to the queue
+    and that calls to pop should block waitting for them. *)
 val make_pledge : 'a t -> unit
 
+(** End one pledge. *)
 val end_pledge : 'a t -> unit
 
+(** Mark the queue as failed: all threads trying to pop from it will get no
+    element. *)
 val fail : 'a t -> unit
 
+(** Pop all elements from the queue in a lazy Seq.t, *)
 val read_as_seq : 'a t -> finalizer:(unit -> unit) -> 'a Seq.t
 
 val work_while : ('a -> ('a -> unit) -> unit) -> 'a t -> unit
diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml
index d522c642e..894f80820 100644
--- a/src/symbolic/symbolic_choice.ml
+++ b/src/symbolic/symbolic_choice.ml
@@ -82,7 +82,7 @@ module CoreImpl = struct
     type ('a, 'wls) t = { work_queue : ('a, 'wls) work_queue } [@@unboxed]
 
     let init_scheduler () =
-      let work_queue = Wq.init () in
+      let work_queue = Wq.make () in
       { work_queue }
 
     let add_init_task sched task = Wq.push task sched.work_queue