diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 18:16:41 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 18:16:41 +0000 |
commit | 6eaff635db797d1f9225b22196832c1bb76c0d94 (patch) | |
tree | 0694fde7fb76446aec8ecc38d0ea7b6367a62857 | |
parent | 428d0f649f565137b1851389f8e26ad410ba7052 (diff) |
Added some tricky tail-rec versions of List functions to CList
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15803 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | lib/cList.ml | 145 | ||||
-rw-r--r-- | lib/util.ml | 2 | ||||
-rw-r--r-- | lib/util.mli | 2 |
3 files changed, 141 insertions, 8 deletions
diff --git a/lib/cList.ml b/lib/cList.ml index e3f35dcac..bc2109167 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -185,7 +185,143 @@ end include List -(* Lists *) +(** Tail-rec implementation of usual functions. This is a well-known trick used + in, for instance, ExtLib and Batteries. *) + +type 'a cell = { + head : 'a; + mutable tail : 'a list; +} + +external cast : 'a cell -> 'a list = "%identity" + +let map f = function +| [] -> [] +| x :: l -> + let rec loop p = function + | [] -> () + | x :: l -> + let c = { head = f x; tail = [] } in + p.tail <- cast c; + loop c l + in + let c = { head = f x; tail = [] } in + loop c l; + cast c + +let map2 f l1 l2 = match l1, l2 with +| [], [] -> [] +| x :: l1, y :: l2 -> + let rec loop p l1 l2 = match l1, l2 with + | [], [] -> () + | x :: l1, y :: l2 -> + let c = { head = f x y; tail = [] } in + p.tail <- cast c; + loop c l1 l2 + | _ -> invalid_arg "List.map2" + in + let c = { head = f x y; tail = [] } in + loop c l1 l2; + cast c +| _ -> invalid_arg "List.map2" + +let append l1 l2 = match l1 with +| [] -> l2 +| x :: l -> + let rec loop p = function + | [] -> p.tail <- l2 + | x :: l -> + let c = { head = x; tail = [] } in + p.tail <- cast c; + loop c l + in + let c = { head = x; tail = [] } in + loop c l; + cast c + +let concat l = + let rec copy p = function + | [] -> p + | x :: l -> + let c = { head = x; tail = [] } in + p.tail <- cast c; + copy c l + in + let rec loop p = function + | [] -> () + | x :: l -> loop (copy p x) l + in + let dummy = { head = Obj.magic 0; tail = [] } in + loop dummy l; + dummy.tail + +let flatten = concat + +let split = function +| [] -> [], [] +| (x, y) :: l -> + let rec loop p q = function + | [] -> () + | (x, y) :: l -> + let cl = { head = x; tail = [] } in + let cr = { head = y; tail = [] } in + p.tail <- cast cl; + q.tail <- cast cr; + loop cl cr l + in + let cl = { head = x; tail = [] } in + let cr = { head = y; tail = [] } in + loop cl cr l; + (cast cl, cast cr) + +let combine l1 l2 = match l1, l2 with +| [], [] -> [] +| x :: l1, y :: l2 -> + let rec loop p l1 l2 = match l1, l2 with + | [], [] -> () + | x :: l1, y :: l2 -> + let c = { head = (x, y); tail = [] } in + p.tail <- cast c; + loop c l1 l2 + | _ -> invalid_arg "List.combine" + in + let c = { head = (x, y); tail = [] } in + loop c l1 l2; + cast c +| _ -> invalid_arg "List.combine" + +let filter f l = + let rec loop p = function + | [] -> () + | x :: l -> + if f x then + let c = { head = x; tail = [] } in + let () = p.tail <- cast c in + loop c l + else + loop p l + in + let c = { head = Obj.magic 0; tail = [] } in + loop c l; + c.tail + +(** FIXME: Already present in OCaml 4.00 *) + +let map_i f i = function +| [] -> [] +| x :: l -> + let rec loop i p = function + | [] -> () + | x :: l -> + let c = { head = f i x; tail = [] } in + p.tail <- cast c; + loop (succ i) c l + in + let c = { head = f i x; tail = [] } in + loop (succ i) c l; + cast c + +(** Extensions of OCaml Stdlib *) let rec compare cmp l1 l2 = if l1 == l2 then 0 else @@ -267,13 +403,6 @@ let map_left f = (* ensures the order in case of side-effects *) in map_rec -let map_i f = - let rec map_i_rec i = function - | [] -> [] - | x::l -> let v = f i x in v :: map_i_rec (i+1) l - in - map_i_rec - let map2_i f i l1 l2 = let rec map_i i = function | ([], []) -> [] diff --git a/lib/util.ml b/lib/util.ml index 8916400ac..523579d1f 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -365,6 +365,8 @@ let ascii_of_ident s = module List : CList.ExtS = CList +let (@) = CList.append + (* Arrays *) let array_compare item_cmp v1 v2 = diff --git a/lib/util.mli b/lib/util.mli index a8ea6854c..58de91d37 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -73,6 +73,8 @@ val ascii_of_ident : string -> string module List : CList.ExtS +val (@) : 'a list -> 'a list -> 'a list + (** {6 Arrays. } *) val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int |