Proofview: move [list_goto] to the [CList] module.

It is, after all, a generic function about lists.

6 files changed, 37 insertions, 40 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index 3115826c6..0ac372d8d 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -70,6 +70,8 @@ sig
   val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
   val subset : 'a list -> 'a list -> bool
   val chop : int -> 'a list -> 'a list * 'a list
+  exception IndexOutOfRange
+  val goto : int -> 'a list -> 'a list * 'a list
   val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
   val firstn : int -> 'a list -> 'a list
@@ -596,17 +598,28 @@ let subset l1 l2 =
   in
   look l1
 
+(** [goto i l] splits [l] into two lists [(l1,l2)] such that
+    [(List.rev l1)++l2=l] and [l1] has length [i].  It raises
+    [IndexOutOfRange] when [i] is negative or greater than the
+    length of [l]. *)
+exception IndexOutOfRange
+let goto n l =
+  let rec goto i acc = function
+    | tl when Int.equal i 0 -> (acc, tl)
+    | h::t -> goto (pred i) (h::acc) t
+    | [] -> raise IndexOutOfRange
+  in
+  goto n [] l
+
 (* [chop i l] splits [l] into two lists [(l1,l2)] such that
    [l1++l2=l] and [l1] has length [i].
    It raises [Failure] when [i] is negative or greater than the length of [l]  *)
 
 let chop n l =
-  let rec chop_aux i acc = function
-    | tl when Int.equal i 0 -> (List.rev acc, tl)
-    | h::t -> chop_aux (pred i) (h::acc) t
-    | [] -> failwith "List.chop"
-  in
-  chop_aux n [] l
+  try let (h,t) = goto n l in (List.rev h,t)
+  with IndexOutOfRange -> failwith "List.chop"
+    (* spiwack: should raise [IndexOutOfRange] but I'm afraid of missing
+       a try/with when replacing the exception. *)
 
 (* [split_when p l] splits [l] into two lists [(l1,a::l2)] such that
     [l1++(a::l2)=l], [p a=true] and [p b = false] for every element [b] of [l1].
diff --git a/lib/cList.mli b/lib/cList.mli
index aa888679c..19eeb2509 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -142,7 +142,20 @@ sig
   (** Merge two sorted lists and preserves the uniqueness property. *)
 
   val subset : 'a list -> 'a list -> bool
+
   val chop : int -> 'a list -> 'a list * 'a list
+  (** [chop i l] splits [l] into two lists [(l1,l2)] such that
+      [l1++l2=l] and [l1] has length [i].  It raises [Failure] when [i]
+      is negative or greater than the length of [l] *)
+
+  exception IndexOutOfRange
+  val goto: int -> 'a list -> 'a list * 'a list
+  (** [goto i l] splits [l] into two lists [(l1,l2)] such that
+      [(List.rev l1)++l2=l] and [l1] has length [i].  It raises
+      [IndexOutOfRange] when [i] is negative or greater than the
+      length of [l]. *)
+
+
   val split_when : ('a -> bool) -> 'a list -> 'a list * 'a list
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
   val firstn : int -> 'a list -> 'a list
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb826bedc..b96a12c46 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -102,7 +102,7 @@ let solve ?with_end_tac gi tac pr =
     Proof.run_tactic (Global.env ()) tac pr
   with
     | Proof_global.NoCurrentProof  -> Errors.error "No focused proof"
-    | Proofview.IndexOutOfRange ->
+    | CList.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
 	                            Errors.errorlabstrm "" msg
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 15ce94011..24fdc41da 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -215,7 +215,7 @@ let _unfocus pr =
    a need for it? *)
 let focus cond inf i pr =
   try _focus cond (Obj.repr inf) i i pr
-  with Proofview.IndexOutOfRange -> raise (NoSuchGoals (i,i))
+  with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
 
 let rec unfocus kind pr () =
   let cond = cond_of_focus pr in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8272b17db..860e29fff 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -158,31 +158,6 @@ let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
 let partial_proof entry pv = List.map (return_constr pv) (List.map fst entry)
 
-(* spiwack: this function should probably go in the Util section,
-    but I'd rather have Util (or a separate module for lists)
-    raise proper exceptions before *)
-(* [IndexOutOfRange] occurs in case of malformed indices
-   with respect to list lengths. *)
-exception IndexOutOfRange
-(* no handler: should not be allowed to reach toplevel *)
-
-(* [list_goto i l] returns a pair of lists [c,t] where
-   [c] has length [i] and is the reversed of the [i] first
-   elements of [l], and [t] is the rest of the list.
-   The idea is to navigate through the list, [c] is then
-   seen as the context of the current position. 
-   Raises [IndexOutOfRange] if [i > length l]*)
-let list_goto = 
-  let rec aux acc index = function
-    | l when Int.equal index 0-> (acc,l)
-    | [] -> raise IndexOutOfRange
-    | a::q -> aux (a::acc) (index-1) q
-  in
-  fun i l ->
-    if i < 0 then
-      raise IndexOutOfRange
-    else
-      aux [] i l
 
 (* Type of the object which allow to unfocus a view.*)
 (* First component is a reverse list of what comes before
@@ -202,10 +177,10 @@ let focus_context f = f
    [focus_sublist i j l] raises [IndexOutOfRange] if
    [i > length l], or [j > length l] or [ j < i ].  *)
 let focus_sublist i j l =
-  let (left,sub_right) = list_goto (i-1) l in
+  let (left,sub_right) = CList.goto (i-1) l in
   let (sub, right) = 
     try List.chop (j-i+1) sub_right
-    with Failure _ -> raise IndexOutOfRange
+    with Failure _ -> raise CList.IndexOutOfRange
   in
   (sub, (left,right))
 
@@ -409,7 +384,7 @@ let tclFOCUS_gen nosuchgoal i j t =
     t >>= fun result ->
     Pv.modify (fun next -> unfocus context next) >>
     Proof.ret result
-  with IndexOutOfRange -> nosuchgoal
+  with CList.IndexOutOfRange -> nosuchgoal
 
 let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
 let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0d9c64a5c..b758d0aec 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -61,10 +61,6 @@ val initial_goals : entry -> (constr * types) list
 
 (*** Focusing operations ***)
 
-(* [IndexOutOfRange] occurs in case of malformed indices
-   with respect to list lengths. *)
-exception IndexOutOfRange
-
 (* Type of the object which allow to unfocus a view.*)
 type focus_context