From 378a22c8abfbe63ac1266ec6ea588028bf11198b Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 4 May 2015 12:33:44 +0200 Subject: [PATCH] `containers.misc.RAL`: more efficient in memory (unfold list) --- src/misc/RAL.ml | 103 +++++++++++++++++++++++++++--------------------- 1 file changed, 57 insertions(+), 46 deletions(-) diff --git a/src/misc/RAL.ml b/src/misc/RAL.ml index f1b3f7ca..fb60a965 100644 --- a/src/misc/RAL.ml +++ b/src/misc/RAL.ml @@ -30,13 +30,11 @@ type +'a tree = | Leaf of 'a | Node of 'a * 'a tree * 'a tree -and +'a t = (int * 'a tree) list +and +'a t = + | Nil + | Cons of int * 'a tree * 'a t (** Functional array of complete trees *) -(* TODO: inline list's nodes - TODO: encode "complete binary tree" into types *) - - (** {2 Functions on trees} *) (* lookup [i]-th element in the tree [t], which has size [size] *) @@ -63,56 +61,67 @@ let rec tree_update size t i v =match t, i with (** {2 Functions on lists of trees} *) -let empty = [] +let empty = Nil -let return x = [1, Leaf x] +let return x = Cons (1, Leaf x, Nil) let is_empty = function - | [] -> true - | _ -> false + | Nil -> true + | Cons _ -> false let rec get l i = match l with - | [] -> raise (Invalid_argument "RAL.get: wrong index") - | (size,t) :: _ when i < size -> tree_lookup size t i - | (size,_) :: l' -> get l' (i - size) + | Nil -> raise (Invalid_argument "RAL.get: wrong index") + | Cons (size,t, _) when i < size -> tree_lookup size t i + | Cons (size,_, l') -> get l' (i - size) let rec set l i v = match l with - | [] -> raise (Invalid_argument "RAL.set: wrong index") - | (size,t) :: l' when i < size -> (size, tree_update size t i v) :: l' - | (size,t) :: l' -> (size, t) :: set l' (i - size) v + | Nil -> raise (Invalid_argument "RAL.set: wrong index") + | Cons (size,t, l') when i < size -> Cons (size, tree_update size t i v, l') + | Cons (size,t, l') -> Cons (size, t, set l' (i - size) v) + +(*$Q + Q.(pair (pair int int) (list int)) (fun ((i,v),l) -> \ + let ral = of_list l in let ral = set ral i v in \ + get ral i = v) +*) let cons x l = match l with - | (size1, t1) :: (size2, t2) :: l' -> + | Cons (size1, t1, Cons (size2, t2, l')) -> if size1 = size2 - then (1 + size1 + size2, Node (x, t1, t2)) :: l' - else (1, Leaf x) :: l - | _ -> (1, Leaf x) :: l + then Cons (1 + size1 + size2, Node (x, t1, t2), l') + else Cons (1, Leaf x, l) + | _ -> Cons (1, Leaf x, l) let hd l = match l with - | [] -> raise (Invalid_argument "RAL.hd: empty list") - | (_, Leaf x) :: _ -> x - | (_, Node (x, _, _)) :: _ -> x + | Nil -> raise (Invalid_argument "RAL.hd: empty list") + | Cons (_, Leaf x, _) -> x + | Cons (_, Node (x, _, _), _) -> x let tl l = match l with - | [] -> raise (Invalid_argument "RAL.tl: empty list") - | (_, Leaf _) :: l' -> l' - | (size, Node (_, t1, t2)) :: l' -> + | Nil -> raise (Invalid_argument "RAL.tl: empty list") + | Cons (_, Leaf _, l') -> l' + | Cons (size, Node (_, t1, t2), l') -> let size' = size / 2 in - (size', t1) :: (size', t2) :: l' + Cons (size', t1, Cons (size', t2, l')) + +(*$T + let l = of_list[1;2;3] in hd l = 1 + let l = of_list[1;2;3] in tl l |> to_list = [2;3] +*) let front l = match l with - | [] -> None - | (_, Leaf x) :: tl -> Some (x, tl) - | (size, Node (x, t1, t2)) :: l' -> + | Nil -> None + | Cons (_, Leaf x, tl) -> Some (x, tl) + | Cons (size, Node (x, t1, t2), l') -> let size' = size / 2 in - Some (x, (size', t1) :: (size', t2) :: l') + Some (x, Cons (size', t1, Cons (size', t2, l'))) let front_exn l = match l with - | [] -> raise (Invalid_argument "RAL.front") - | (_, Leaf x) :: tl -> x, tl - | (size, Node (x, t1, t2)) :: l' -> + | Nil -> raise (Invalid_argument "RAL.front") + | Cons (_, Leaf x, tl) -> x, tl + | Cons (size, Node (x, t1, t2), l') -> let size' = size / 2 in - x, (size', t1) :: (size', t2) :: l' + x, Cons (size', t1, Cons (size', t2, l')) let rec _remove prefix l i = let x, l' = front_exn l in @@ -126,24 +135,26 @@ let rec _map_tree f t = match t with | Leaf x -> Leaf (f x) | Node (x, l, r) -> Node (f x, _map_tree f l, _map_tree f r) -let map f l = List.map (fun (i,t) -> i, _map_tree f t) l +let rec map f l = match l with + | Nil -> Nil + | Cons (i, t, tl) -> Cons (i, _map_tree f t, map f tl) let rec length l = match l with - | [] -> 0 - | (size,_) :: l' -> size + length l' + | Nil -> 0 + | Cons (size,_, l') -> size + length l' let rec iter f l = match l with - | [] -> () - | (_, Leaf x) :: l' -> f x; iter f l' - | (_, t) :: l' -> iter_tree t f; iter f l' + | Nil -> () + | Cons (_, Leaf x, l') -> f x; iter f l' + | Cons (_, t, l') -> iter_tree t f; iter f l' and iter_tree t f = match t with | Leaf x -> f x | Node (x, t1, t2) -> f x; iter_tree t1 f; iter_tree t2 f let rec fold f acc l = match l with - | [] -> acc - | (_, Leaf x) :: l' -> fold f (f acc x) l' - | (_, t) :: l' -> + | Nil -> acc + | Cons (_, Leaf x, l') -> fold f (f acc x) l' + | Cons (_, t, l') -> let acc' = fold_tree t acc f in fold f acc' l' and fold_tree t acc f = match t with @@ -154,9 +165,9 @@ and fold_tree t acc f = match t with fold_tree t2 acc f let rec fold_rev f acc l = match l with - | [] -> acc - | (_, Leaf x) :: l' -> f (fold f acc l') x - | (_, t) :: l' -> + | Nil -> acc + | Cons (_, Leaf x, l') -> f (fold f acc l') x + | Cons (_, t, l') -> let acc = fold_rev f acc l' in fold_tree_rev t acc f and fold_tree_rev t acc f = match t with