summaryrefslogtreecommitdiff
path: root/clib
diff options
context:
space:
mode:
authorGaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2023-11-06 13:39:11 (GMT)
committerGaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2023-11-08 15:16:30 (GMT)
commit55505ed0df04e1d701d13e0861a3b0f6ff58a4ab (patch)
tree099451c461e0fc73af17e30ffa574587010c84c4 /clib
parentfb3a67760b373ab20fd3624c5de8cf3acb522fc3 (diff)
downloadcoq-55505ed0df04e1d701d13e0861a3b0f6ff58a4ab.zip
coq-55505ed0df04e1d701d13e0861a3b0f6ff58a4ab.tar.gz
coq-55505ed0df04e1d701d13e0861a3b0f6ff58a4ab.tar.bz2
Restore tailrecness of CList.filterrefs/pull/18262/head
filter2 and filter_with are also nontailrec but let's validate the idea first. Alternatives: - drop preservation of physical equality ("smartness") - continuation passing instead of mutation - drop tailrec explicitly (and stop using mutation since it's then useless AFAICT)
Diffstat (limited to 'clib')
-rw-r--r--clib/cList.ml29
1 files changed, 20 insertions, 9 deletions
diff --git a/clib/cList.ml b/clib/cList.ml
index ebf501b..eda1892 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -160,20 +160,31 @@ let assign l n e =
(** {6 Filtering} *)
-let rec filter_loop f p = function
- | [] -> ()
- | x :: l' as l ->
- let b = f x in
- filter_loop f p l';
- if b then if p.tail == l' then p.tail <- l else p.tail <- x :: p.tail
+(* [filter_loop f (Some (c0,l0)) c l] will do c0.tail <- l0 if [for_all f l] *)
+let rec filter_loop f reset p = function
+ | [] -> begin match reset with
+ | None -> ()
+ | Some (c,orig) -> c.tail <- orig
+ end
+ | x :: l as orig ->
+ if f x then
+ let c = { head = x; tail = [] } in
+ let () = p.tail <- cast c in
+ let reset = match reset with
+ | Some _ -> reset
+ | None -> Some (p,orig)
+ in
+ filter_loop f reset c l
+ else
+ filter_loop f None p l
let rec filter f = function
| [] -> []
- | x :: l' as l ->
+ | x :: l' as orig ->
if f x then
let c = { head = x; tail = [] } in
- filter_loop f c l';
- if c.tail == l' then l else cast c
+ filter_loop f None c l';
+ if c.tail == l' then orig else cast c
else
filter f l'