large update of CCList.Zipper. Breaking semantics of CCList.Zipper.is_empty

src/core/CCList.ml

@@ -815,14 +815,17 @@ module Zipper = struct
   let empty = [], []
 
   let is_empty = function
-    | _, [] -> true
+    | [], [] -> true
-    | _, _::_ -> false
+    | _ -> false
 
-  let to_list (l,r) =
+  let to_list (l,r) = List.rev_append l r
-    let rec append l acc = match l with
+
-      | [] -> acc
+  let to_rev_list (l,r) = List.rev_append r l
-      | x::l' -> append l' (x::acc)
+
-    in append l r
+  (*$Q
+    Q.(pair (list small_int)(list small_int)) (fun z -> \
+      Zipper.to_list z = List.rev (Zipper.to_rev_list z))
+  *)
 
   let make l = [], l
 
@@ -846,6 +849,10 @@ module Zipper = struct
         | Some _ -> l, x::r
         end
 
+  let is_focused = function
+    | _, [] -> true
+    | _ -> false
+
   let focused = function
     | _, x::_ -> Some x
     | _, [] -> None
@@ -853,6 +860,21 @@ module Zipper = struct
   let focused_exn = function
     | _, x::_ -> x
     | _, [] -> raise Not_found
+
+  let insert x (l,r) = l, x::r
+
+  let remove (l,r) = match r with
+    | [] -> l, []
+    | _ :: r' -> l, r'
+
+  (*$Q
+    Q.(triple int (list small_int)(list small_int)) (fun (x,l,r) -> \
+      Zipper.insert x (l,r) |> Zipper.remove = (l,r))
+  *)
+
+  let drop_before (_, r) = [], r
+
+  let drop_after (l, _) = l, []
 end
 
 (** {2 References on Lists} *)

src/core/CCList.mli

@@ -302,15 +302,28 @@ end
 
 module Zipper : sig
   type 'a t = 'a list * 'a list
+  (** The pair [l, r] represents the list [List.rev_append l r], but
+      with the focus on [r]. *)
 
   val empty : 'a t
   (** Empty zipper *)
 
   val is_empty : _ t -> bool
-  (** Empty zipper, or at the end of the zipper? *)
+  (** Empty zipper? Returns true iff the two lists are empty. *)
+
+  (*$T
+    Zipper.(is_empty empty)
+    not ([42] |> Zipper.make |> Zipper.right |> Zipper.is_empty)
+  *)
 
   val to_list : 'a t -> 'a list
-  (** Convert the zipper back to a list *)
+  (** Convert the zipper back to a list.
+      [to_list (l,r)] is [List.rev_append l r] *)
+
+  val to_rev_list : 'a t -> 'a list
+  (** Convert the zipper back to a {i reversed} list.
+      In other words, [to_list (l,r)] is [List.rev_append r l]
+      @since NEXT_RELEASE *)
 
   val make : 'a list -> 'a t
   (** Create a zipper pointing at the first element of the list *)
@@ -325,6 +338,20 @@ module Zipper : sig
   (** Modify the current element, if any, by returning a new element, or
       returning [None] if the element is to be deleted *)
 
+  val insert : 'a -> 'a t -> 'a t
+  (** Insert an element at the current position. If an element was focused,
+      [insert x l] adds [x] just before it, and focuses on [x]
+      @since NEXT_RELEASE *)
+
+  val remove : 'a t -> 'a t
+  (** [remove l] removes the current element, if any.
+      @since NEXT_RELEASE *)
+
+  val is_focused : _ t -> bool
+  (** Is the zipper focused on some element? That is, will {!focused}
+      return a [Some v]?
+      @since NEXT_RELEASE *)
+
   val focused : 'a t -> 'a option
   (** Returns the focused element, if any. [focused zip = Some _] iff
       [empty zip = false] *)
@@ -332,6 +359,14 @@ module Zipper : sig
   val focused_exn : 'a t -> 'a
   (** Returns the focused element, or
       @raise Not_found if the zipper is at an end *)
+
+  val drop_before : 'a t -> 'a t
+  (** Drop every element on the "left" (calling {!left} then will do nothing).
+      @since NEXT_RELEASE *)
+
+  val drop_after : 'a t -> 'a t
+  (** Drop every element on the "right" (calling {!right} then will do nothing).
+      @since NEXT_RELEASE *)
 end
 
 (** {2 References on Lists}