diff --git a/src/core/CCList.ml b/src/core/CCList.ml index 4be891a6..5833d17d 100644 --- a/src/core/CCList.ml +++ b/src/core/CCList.ml @@ -815,14 +815,17 @@ module Zipper = struct let empty = [], [] let is_empty = function - | _, [] -> true - | _, _::_ -> false + | [], [] -> true + | _ -> false - let to_list (l,r) = - let rec append l acc = match l with - | [] -> acc - | x::l' -> append l' (x::acc) - in append l r + let to_list (l,r) = List.rev_append l r + + let to_rev_list (l,r) = List.rev_append r l + + (*$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} *) diff --git a/src/core/CCList.mli b/src/core/CCList.mli index 06144586..f470396e 100644 --- a/src/core/CCList.mli +++ b/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}