format pairs of items for pr_depth to get alternating separators

eval thunks once in prlist_sep_lastsep, make code clearer
add typeclass debug output test

5 files changed, 58 insertions, 28 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index 6d28ed13b..1902f79cb 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -220,23 +220,25 @@ let prlist pr l = Ppcmd_glue (List.map pr l)
    if a strict behavior is needed, use [prlist_strict] instead.
    evaluation is done from left to right. *)
 
-let prlist_sep_lastsep no_empty sep lastsep elem =
-  let rec start = function
-    |[] -> mt ()
-    |[e] -> elem e
-    |h::t -> let e = elem h in
-        if no_empty && ismt e then start t else
-          let rec aux = function
-            |[] -> mt ()
-            |h::t ->
-               let e = elem h and r = aux t in
-                 if no_empty && ismt e then r else
-                   if ismt r
-                   then let s = lastsep () in s ++ e
-                   else let s = sep () in s ++ e ++ r
-          in let r = aux t in e ++ r
-  in start
-
+let prlist_sep_lastsep no_empty sep_thunk lastsep_thunk elem l =
+  let sep = sep_thunk () in
+  let lastsep = lastsep_thunk () in
+  let elems = List.map elem l in
+  let filtered_elems =
+    if no_empty then
+      List.filter (fun e -> not (ismt e)) elems
+    else
+      elems
+  in
+  let rec insert_seps es =
+    match es with
+    | []     -> mt ()
+    | [e]    -> e
+    | h::[e] -> h ++ lastsep ++ e
+    | h::t   -> h ++ sep ++ insert_seps t
+  in
+  insert_seps filtered_elems
+  
 let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l
 (* [prlist_with_sep sep pr [a ; ... ; c]] outputs
    [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
diff --git a/lib/pp.mli b/lib/pp.mli
index be255a74f..96656c8b6 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -145,7 +145,10 @@ val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prlist_with_sep :
    (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 (** [prlist_with_sep sep pr [a ; ... ; c]] outputs
-    [pr a ++ sep() ++ ... ++ sep() ++ pr c]. *)
+    [pr a ++ sep () ++ ... ++ sep () ++ pr c]. 
+    where the thunk sep is memoized, rather than being called each place 
+     its result is used.
+*)
 
 val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
 (** As [prlist], but on arrays. *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7a8595653..d44e64b83 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -494,16 +494,15 @@ let catchable = function
   | Refiner.FailError _ -> true
   | e -> Logic.catchable_exception e
 
-(* alternate separators in debug search path output *)
-let debug_seps = [| "." ; "-" |]
-let next_sep seps = 
-  let num_seps = Array.length seps in
-  let sep_index = ref 0 in
-  fun () ->
-    let sep = seps.(!sep_index) in
-    sep_index := (!sep_index + 1) mod num_seps;
-    str sep
-let pr_depth l = prlist_with_sep (next_sep debug_seps) int (List.rev l)
+let pr_depth l = 
+  let rec fmt elts =
+    match elts with
+    | [] -> []
+    | [n] -> [string_of_int n]
+    | n1::n2::rest ->
+       (string_of_int n1 ^ "." ^ string_of_int n2) :: fmt rest
+  in
+  prlist_with_sep (fun () -> str "-") str (fmt (List.rev l))
 
 let is_Prop env sigma concl =
   let ty = Retyping.get_type_of env sigma concl in
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
new file mode 100644
index 000000000..73369ab71
--- /dev/null
+++ b/test-suite/output/TypeclassDebug.out
@@ -0,0 +1,18 @@
+Debug: 1: looking for foo without backtracking
+Debug: 1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2 : foo
+Debug: 1.1-2: looking for foo without backtracking
+Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2 : foo
+Debug: 1.1-2.1-2: looking for foo without backtracking
+Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2.1-2 : foo
+Debug: 1.1-2.1-2.1-2: looking for foo without backtracking
+Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2.1-2.1-2 : foo
+Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking
+Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo
+The command has indeed failed with message:
+Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
+Tactic failure: Proof search reached its limit.
diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v
new file mode 100644
index 000000000..d38e2a50e
--- /dev/null
+++ b/test-suite/output/TypeclassDebug.v
@@ -0,0 +1,8 @@
+(* show alternating separators in typeclass debug output; see discussion in PR #868 *)
+
+Parameter foo : Prop.
+Axiom H : foo -> foo.
+Hint Resolve H : foo.
+Goal foo.
+Typeclasses eauto := debug.
+Fail typeclasses eauto 5 with foo.