1) bug fixed: new goals where compared according to the relation arguments

   only. Now the head of the relation is used to.
2) much nicer pretty-printing of the multiple set of side conditions that
   the tactic can now produce


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6152 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 32 insertions, 29 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index c8060931b..14a81311b 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -35,6 +35,18 @@ open Constrintern
 let replace = ref (fun _ _ -> assert false)
 let register_replace f = replace := f
 
+(* util function; it should be in util.mli *)
+let prlist_with_sepi sep elem =
+ let rec aux n =
+  function
+   | []   -> mt ()
+   | [h]  -> elem n h
+   | h::t ->
+      let e = elem n h and s = sep() and r = aux (n+1) t in
+      e ++ s ++ r
+ in
+  aux 1
+
 type relation =
    { rel_a: constr ;
      rel_aeq: constr;
@@ -775,17 +787,6 @@ type constr_with_marks =
   | ToReplace
   | ToKeep of constr * relation relation_class * direction
 
-let rec prconstr_with_marks =
- function
-    MApp (c,m,a,d) ->
-     str "(" ++ prterm c ++ str " " ++
-      prvect_with_sep (fun () -> str " ") prconstr_with_marks a ++ str ")"
-  | ToReplace -> str "*"
-  | ToKeep (c,Leibniz _,_)
-  | ToKeep (c,Relation {rel_refl=Some _},_) -> prterm c
-  | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) ->
-     str "(?:" ++ prterm (mkApp (aeq, [| c ; c|])) ++ str ")"
-
 let is_to_replace = function
  | ToKeep _ -> false
  | ToReplace -> true
@@ -866,25 +867,26 @@ let subrelation rel1 rel2 =
 *)
   | _,_ -> false
 
+(* this function returns the list of new goals opened by a constr_with_marks *)
+let rec collect_new_goals =
+ function
+   MApp (_,_,a,_) -> List.concat (List.map collect_new_goals (Array.to_list a))
+ | ToReplace
+ | ToKeep (_,Leibniz _,_)
+ | ToKeep (_,Relation {rel_refl=Some _},_) -> []
+ | ToKeep (c,Relation {rel_aeq=aeq; rel_refl=None},_) -> [mkApp(aeq,[|c ; c|])]
+
 (* two marked_constr are equivalent if they produce the same set of new goals *)
-(*CSC: Note: it would be better if the tactic got rid of the smaller multiset
-       of goals when the two multisets are equal sets. I.e.: the tactic that
-       open one new goal G should be preferred to the tactic that opens two
-       copies of the new goal G. Moreover, a smaller proof term should be
-       preferred to a bigger one when the size of the two multisets is equal. *)
 let marked_constr_equiv_or_more_complex to_marked_constr c1 c2 =
- let rec collect_new_goals =
-  function
-    MApp (_,_,a,_) -> List.concat (List.map collect_new_goals (Array.to_list a))
-  | ToReplace
-  | ToKeep (_,Leibniz _,_)
-  | ToKeep (_,Relation {rel_refl=Some _},_) -> []
-  | ToKeep (c,Relation {rel_refl=None},_) -> [c]
- in
   let glc1 = collect_new_goals (to_marked_constr c1) in
   let glc2 = collect_new_goals (to_marked_constr c2) in
    List.for_all (fun c -> List.exists (fun c' -> eq_constr c c') glc1) glc2
-;;
+
+let pr_new_goals i c =
+ let glc = collect_new_goals c in
+  str " " ++ int i ++ str ") side conditions:" ++ pr_fnl () ++ str "   " ++
+   prlist_with_sep (fun () -> str "\n   ")
+    (fun c -> str " ... |- " ++ prterm c) glc
 
 (* given a list of constr_with_marks, it returns the list where
    constr_with_marks than open more goals than simpler ones in the list
@@ -1095,11 +1097,12 @@ let mark_occur gl t in_c input_relation input_direction =
    | [he] -> he
    | he::_ ->
       msg_warning
-       (str "There are several possible ways to perform this rewriting:" ++
+       (str "The application of the tactic is subject to one of the \n" ++
+        str "following set of side conditions that the user needs to prove:" ++
          pr_fnl () ++
-         prlist_with_sep pr_fnl
-          (function (_,_,mc) -> prconstr_with_marks mc) res ++ pr_fnl () ++
-         str " The first one is randomly chosen.") ;
+         prlist_with_sepi pr_fnl
+          (fun i (_,_,mc) -> pr_new_goals i mc) res ++ pr_fnl () ++
+         str "The first set is randomly chosen.") ;
       he
 
 let cic_morphism_context_list_of_list hole_relation hole_direction out_direction