From 56ca108e63191e90c3d4169c37a4c97017e3c6ae Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 14:19:34 +0200 Subject: TQueue: Expose the length of TQueues --- stm/tQueue.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'stm/tQueue.ml') diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 6fef895ae8..2a43cd7d13 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -15,6 +15,7 @@ module PriorityQueue : sig val pop : ?picky:('a -> bool) -> 'a t -> 'a val push : 'a t -> 'a -> unit val clear : 'a t -> unit + val length : 'a t -> int end = struct type 'a item = int * 'a type 'a rel = 'a item -> 'a item -> int @@ -38,6 +39,7 @@ end = struct let set_rel rel ({ contents = (xs, _) } as t) = let rel (_,x) (_,y) = rel x y in t := (List.sort rel xs, rel) + let length ({ contents = (l, _) }) = List.length l end type 'a t = { @@ -92,6 +94,12 @@ let push { queue = q; lock = m; cond = c; release } x = Condition.broadcast c; Mutex.unlock m +let length { queue = q; lock = m } = + Mutex.lock m; + let n = PriorityQueue.length q in + Mutex.unlock m; + n + let clear { queue = q; lock = m; cond = c } = Mutex.lock m; PriorityQueue.clear q; -- cgit v1.2.3 From f6b3704391de97ee544da9ae7316685cd2d9fae3 Mon Sep 17 00:00:00 2001 From: Alec Faithfull Date: Tue, 6 Oct 2015 14:20:22 +0200 Subject: TQueue: Allow some tasks to be saved when clearing a TQueue --- stm/tQueue.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'stm/tQueue.ml') diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 2a43cd7d13..2dad962bec 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -105,6 +105,18 @@ let clear { queue = q; lock = m; cond = c } = PriorityQueue.clear q; Mutex.unlock m +let clear_saving { queue = q; lock = m; cond = c } f = + Mutex.lock m; + let saved = ref [] in + while not (PriorityQueue.is_empty q) do + let elem = PriorityQueue.pop q in + match f elem with + | Some x -> saved := x :: !saved + | None -> () + done; + Mutex.unlock m; + List.rev !saved + let is_empty { queue = q } = PriorityQueue.is_empty q let destroy tq = -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- stm/tQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm/tQueue.ml') diff --git a/stm/tQueue.ml b/stm/tQueue.ml index 2dad962bec..ee121c46a2 100644 --- a/stm/tQueue.ml +++ b/stm/tQueue.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*