diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2023-11-06 13:39:11 (GMT) |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2023-11-08 15:16:30 (GMT) |
commit | 55505ed0df04e1d701d13e0861a3b0f6ff58a4ab (patch) | |
tree | 099451c461e0fc73af17e30ffa574587010c84c4 /clib | |
parent | fb3a67760b373ab20fd3624c5de8cf3acb522fc3 (diff) | |
download | coq-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.ml | 29 |
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' |