The quoting function is now almost complete (in the sense that it can find

multiple solutions).

Since several solutions are observationally equal (i.e. they open the same
new set of goals), they are identified by the tactic. In case of multiple
non observationally equal solutions, the list of them is presented to the
user and the first one is randomically chosen. The user should be given
a possibility to choose.

Still todo: making the quoting function completely complete.

Note: the wf_unifty_to_subterm is now called twice. The first time is not
modulus delta conversion (the reasonable choice). The second time is modulus
delta conversion and the call is made iff the first call failed.
This is required by Ring that exploits the delta conversion ;-(


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

1 files changed, 241 insertions, 145 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 1c0798ee67..93a0e29458 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -763,10 +763,26 @@ type direction =
    Left2Right
  | Right2Left
 
+let prdirection =
+ function
+    Left2Right -> str "->"
+  | Right2Left -> str "<-"
+
 type constr_with_marks =
   | MApp of constr * morphism_class * constr_with_marks array * direction
   | ToReplace
-  | ToKeep of constr * direction
+  | 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
@@ -790,7 +806,7 @@ let direction_of_constr_with_marks hole_direction =
  function
     MApp (_,_,_,dir) -> cic_direction_of_direction dir
   | ToReplace -> hole_direction
-  | ToKeep (_,dir) -> cic_direction_of_direction dir
+  | ToKeep (_,_,dir) -> cic_direction_of_direction dir
 
 type argument =
    Toapply of constr         (* apply the function to the argument *)
@@ -828,8 +844,6 @@ let relation_of_hypothesis_and_term_to_rewrite gl (_,h) t =
    errorlabstrm "Setoid_rewrite"
     (prterm aeq ++ str " is not a setoid equality.")
 
-exception BackTrack
-
 (* rel1 is a subrelation of rel2 whenever 
     forall x1 x2, rel1 x1 x2 -> rel2 x1 x2
    The Coq part of the tactic, however, needs rel1 == rel2.
@@ -850,16 +864,76 @@ let subrelation rel1 rel2 =
 *)
   | _,_ -> false
 
-let mark_occur gl t in_c input_relation input_direction
-     output_relation output_direction
-=
+(* 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 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
+   let rec equal_sets =
+    function
+       [],[] -> true
+     | [],_
+     | _,[] -> false
+     | he::tl,l ->
+        equal_sets
+         ((List.filter (fun e -> not (eq_constr e he)) tl),
+          (List.filter (fun e -> not (eq_constr e he)) l))
+   in
+    equal_sets (glc1,glc2)
+;;
+
+(* given a list of constr_with_marks, it returns the list without duplicates
+   up to marked_constr_equiv *)
+let elim_duplicates to_marked_constr =
+ let rec aux =
+  function
+     [] -> []
+   | he:: tl ->
+      if List.exists (marked_constr_equiv to_marked_constr he) tl then
+       (*CSC: here we choose to get rid of he. But this may not be the
+              best choice. See the comment about marked_constr_equiv.*)
+       aux tl
+      else he::aux tl
+ in
+  aux
+
+(* given the array of lists [| l1 ; ... ; ln |] it returns the list of arrays
+   [ c1 ; ... ; cn ] that is the cartesian product of the sets l1, ..., ln *)
+let cartesian_product a =
+ let rec aux =
+  function
+     [] -> assert false
+   | [he] -> List.map (fun e -> [e]) he
+   | he::tl ->
+      let tl' = aux tl in
+       List.flatten
+        (List.map (function e -> List.map (function l -> e :: l) tl') he)
+ in
+  List.map Array.of_list
+   (aux (List.map (elim_duplicates identity) (Array.to_list a)))
+
+exception BackTrack
+
+let mark_occur gl t in_c input_relation input_direction =
  let rec aux output_relation output_direction in_c =
   if eq_constr t in_c then
    if input_direction = output_direction
    && subrelation (Relation input_relation) output_relation then
-    ToReplace
+    [ToReplace]
    else
-    raise BackTrack
+    []
 (*CSC: nice error message, incompatible with backtracking
     errorlabstrm "Setoid_rewrite"
      (str "The term " ++ prterm in_c ++ str " that must be rewritten occurs " ++
@@ -869,29 +943,20 @@ let mark_occur gl t in_c input_relation input_direction
   else
     match kind_of_term in_c with
       | App (c,al) -> 
-         let mor =
-           try
-             begin
-              match morphism_table_find c with
-                 [] -> assert false
-               | morphism::tl ->
-                  if tl <> [] then
-                   msg_warning
-                    (str "There are several morphisms declared for " ++
-                      prterm c ++
-                      str ". The morphism " ++ prmorphism c morphism ++
-                      str " is randomly chosen.") ;
-                  let relation_morphism =
-                   relation_morphism_of_constr_morphism morphism in
-                  if subrelation relation_morphism.output output_relation then
-                   Some relation_morphism
-                  else
-                   raise BackTrack
-             end
-            with Not_found -> None
+         let mors =
+          try
+           let morphisms =
+            List.map relation_morphism_of_constr_morphism
+             (morphism_table_find c)
+           in
+            List.filter
+             (fun mor -> subrelation mor.output output_relation) morphisms
+          with Not_found -> []
          in
-          (match mor with
-             Some mor ->
+          (* First we look for well typed morphisms *)
+          let res_mors =
+           List.fold_left
+            (fun res mor ->
               let a =
                let arguments = Array.of_list mor.args in
                let apply_variance_to_direction default_dir =
@@ -902,83 +967,97 @@ let mark_occur gl t in_c input_relation input_direction
                in
                 Util.array_map2
                  (fun a (variance,relation) ->
-                   try
-                    aux relation
-                     (apply_variance_to_direction Left2Right variance) a
-                   with BackTrack ->
-try
-                    aux relation
-                     (apply_variance_to_direction Right2Left variance) a
-(*CSC: an horrible hack. This should be no longer useful once that every possibility is tried. *)
-with BackTrack -> ToKeep (a,apply_variance_to_direction Left2Right variance)
+                   (aux relation
+                     (apply_variance_to_direction Left2Right variance) a) @
+                   (aux relation
+                     (apply_variance_to_direction Right2Left variance) a)
                  ) al arguments
               in
-               if not (get_mark a) then ToKeep (in_c,output_direction)
-               else
-                MApp (c,ACMorphism mor,a,output_direction)
-           | None ->
-             (* the tactic works only if the function type is
-                made of non-dependent products only. However, here we
-                can cheat a bit by partially istantiating c to match
-                the requirement when the arguments to be replaced are
-                bound by non-dependent products only. *)
-             let typeofc = Tacmach.pf_type_of gl c in
-             let typ = nf_betaiota typeofc in
-             let rec find_non_dependent_function env c c_args_rev typ
-                      f_args_rev a_rev
-             =
-              function
-                 [] ->
-                  if not (get_mark (Array.of_list a_rev)) then
-                   ToKeep (in_c,output_direction)
-                  else
-                   let mor =
-                    ACFunction {f_args=List.rev f_args_rev ; f_output=typ} in
-                   let func = beta_expand c c_args_rev in
-                    MApp
-                     (func,mor,Array.of_list (List.rev a_rev),
-                      output_direction)
-               | (he::tl) as a->
-                  let typnf = Reduction.whd_betadeltaiota env typ in
-                   match kind_of_term typnf with
-                     Cast (typ,_) ->
-                      find_non_dependent_function env c c_args_rev typ
-                       f_args_rev a_rev a
-                   | Prod (name,s,t) ->
-                      let env' = push_rel (name,None,s) env in
-                      let he =
-                       try
-                         aux (Leibniz s) Left2Right he
-                       with BackTrack ->
-                         aux (Leibniz s) Right2Left he in
-                      begin
-                       match noccurn 1 t, he with
-                          _, ToKeep (arg,_) ->
-                           (* generic product, to keep *)
-                           find_non_dependent_function
-                            env' c ((Toapply arg)::c_args_rev)
-                            (subst1 arg t) f_args_rev a_rev tl
-                        | true, _ ->
-                           (* non-dependent product, to replace *)
-                           find_non_dependent_function
-                            env' c ((Toexpand (name,s))::c_args_rev)
-                             (lift 1 t) (s::f_args_rev) (he::a_rev) tl
-                        | false, _ ->
-                           (* dependent product, to replace *)
-                           (*CSC: this limitation is due to the reflexive
-                             implementation and it is hard to lift *)
-                           errorlabstrm "Setoid_replace"
-                            (str "Cannot rewrite in the argument of a " ++
-                             str "dependent product. If you need this " ++
-                             str "feature, please report to the authors.")
-                      end
-                   | _ -> assert false
-             in
-              find_non_dependent_function (Tacmach.pf_env gl) c [] typ [] []
-               (Array.to_list al))
+               let a' = cartesian_product a in
+                (List.map
+                  (function a ->
+                    if not (get_mark a) then
+                     ToKeep (in_c,output_relation,output_direction)
+                    else
+                     MApp (c,ACMorphism mor,a,output_direction)) a') @ res
+            ) [] mors in
+          (* Then we look for well typed functions *)
+          let res_functions =
+           (* the tactic works only if the function type is
+               made of non-dependent products only. However, here we
+               can cheat a bit by partially istantiating c to match
+               the requirement when the arguments to be replaced are
+               bound by non-dependent products only. *)
+            let typeofc = Tacmach.pf_type_of gl c in
+            let typ = nf_betaiota typeofc in
+            let rec find_non_dependent_function env c c_args_rev typ f_args_rev
+                     a_rev
+            =
+             function
+                [] ->
+                 if not (get_mark (Array.of_list a_rev)) then
+                  [ToKeep (in_c,output_relation,output_direction)]
+                 else
+                  let err =
+                   match output_relation with
+                      Leibniz typ' when eq_constr typ typ' -> false
+                    | _ when output_relation = (Lazy.force coq_prop_relation) ->
+                       false
+                    | _ -> true
+                  in
+                   if err then []
+                   else
+                    let mor =
+                     ACFunction {f_args=List.rev f_args_rev; f_output=typ} in
+                    let func = beta_expand c c_args_rev in
+                     [MApp
+                       (func,mor,Array.of_list (List.rev a_rev),
+                        output_direction)]
+              | (he::tl) as a->
+                 let typnf = Reduction.whd_betadeltaiota env typ in
+                  match kind_of_term typnf with
+                    Cast (typ,_) ->
+                     find_non_dependent_function env c c_args_rev typ
+                      f_args_rev a_rev a
+                  | Prod (name,s,t) ->
+                     let env' = push_rel (name,None,s) env in
+                     let he =
+                      (aux (Leibniz s) Left2Right he) @
+                      (aux (Leibniz s) Right2Left he) in
+(*CSC: let's make it simple at first *)
+let he = match he with [] -> raise BackTrack | he::_ -> (*ppnl (str "!!!!!! THE TACTIC IS STILL INCOMPLETE HERE !!!!!");*) he in
+                     begin
+                      match noccurn 1 t, he with
+                         _, ToKeep (arg,_,_) ->
+                          (* generic product, to keep *)
+                          find_non_dependent_function
+                           env' c ((Toapply arg)::c_args_rev)
+                           (subst1 arg t) f_args_rev a_rev tl
+                       | true, _ ->
+                          (* non-dependent product, to replace *)
+                          find_non_dependent_function
+                           env' c ((Toexpand (name,s))::c_args_rev)
+                            (lift 1 t) (s::f_args_rev) (he::a_rev) tl
+                       | false, _ ->
+                          (* dependent product, to replace *)
+                          (*CSC: this limitation is due to the reflexive
+                            implementation and it is hard to lift *)
+                          errorlabstrm "Setoid_replace"
+                           (str "Cannot rewrite in the argument of a " ++
+                            str "dependent product. If you need this " ++
+                            str "feature, please report to the author.")
+                     end
+                  | _ -> assert false
+            in
+try
+             find_non_dependent_function (Tacmach.pf_env gl) c [] typ [] []
+              (Array.to_list al)
+with BackTrack -> []
+          in
+           elim_duplicates identity (res_functions @ res_mors)
       | Prod (_, c1, c2) -> 
           if (dependent (mkRel 1) c2)
-          then ToKeep (in_c,output_direction)
+          then [ToKeep (in_c,output_relation,output_direction)]
           else 
            (*CSC: output_relation in the two lines below is a bug.
              I should use the two arguments of the relation associated to
@@ -988,16 +1067,46 @@ with BackTrack -> ToKeep (a,apply_variance_to_direction Left2Right variance)
            let c2m =
             aux output_relation output_direction c2
            in
-             if ((is_to_replace c1m)||(is_to_replace c2m))
-             then
-              (* this can be optimized since c1 and c2 will be *)
-              (* processed again                               *)
-              aux output_relation output_direction
-               (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
-             else ToKeep (in_c,output_direction)
-      | _ -> ToKeep (in_c,output_direction)
+            let a = cartesian_product [| c1m ; c2m |] in
+             List.fold_left
+              (fun res a ->
+                if get_mark a
+                then
+                 (* this can be optimized since c1 and c2 will be *)
+                 (* processed again                               *)
+                 (aux output_relation output_direction
+                  (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))) @ res
+                else (ToKeep (in_c,output_relation,output_direction))::res) [] a
+      | _ -> [ToKeep (in_c,output_relation,output_direction)]
  in
-  aux output_relation output_direction in_c 
+  let aux2 output_relation output_direction =
+   List.map
+    (fun res -> output_relation,output_direction,res)
+     (aux output_relation output_direction in_c) in
+  let res =
+   (aux2 (Lazy.force coq_prop_relation) Right2Left) @
+   (* This is the case of a proposition of signature A ++> iff or B --> iff *)
+   (aux2 (Lazy.force coq_prop_relation) Left2Right) @
+   (aux2 (Lazy.force coq_prop_relation2) Right2Left) in
+  let res = elim_duplicates (function (_,_,t) -> t) res in
+  match res with
+     [] ->
+      errorlabstrm "Setoid_rewrite"
+       (str "Either the term " ++ prterm in_c ++ str " that must be " ++
+        str "rewritten occurs in a covariant position or the goal is not " ++
+        str "made of morphism applications only. You can replace only " ++
+        str "occurrences that are in a contravariant position and such that " ++
+        str "the context obtained by abstracting them is made of morphism " ++
+        str "applications only.")
+   | [he] -> he
+   | he::_ ->
+      msg_warning
+       (str "There are several possible ways to perform this rewriting:" ++
+         pr_fnl () ++
+         prlist_with_sep pr_fnl
+          (function (_,_,mc) -> prconstr_with_marks mc) res ++ pr_fnl () ++
+         str " The first one is randomly chosen.") ;
+      he
 
 let cic_morphism_context_list_of_list hole_relation hole_direction out_direction
 =
@@ -1084,7 +1193,7 @@ let syntactic_but_representation_of_marked_but hole_relation hole_direction =
           morphism_theory ; argst|])
    | ToReplace ->
       mkApp ((Lazy.force coq_ToReplace), [| hole_relation ; hole_direction |])
-   | ToKeep (c,direction) ->
+   | ToKeep (c,_,direction) ->
       let direction = cic_direction_of_direction direction in
        if is_reflexive then
         mkApp ((Lazy.force coq_ToKeep),
@@ -1134,39 +1243,24 @@ let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h)
 let relation_rewrite c1 c2 (input_direction,cl) gl =
  let but = pf_concl gl in
  let (hyp,c1,c2) =
+let oldc1 = c1 in
    let (env',c1) =
-    w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env in
+    try
+     w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
+    with
+     Pretype_errors.PretypeError _ ->
+      (*CSC: not very nice; to make Ring work *)
+      w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
+   in
    let cl' = {cl with env = env' } in
    let c2 = Clenv.clenv_nf_meta cl' c2 in
    (input_direction,Clenv.clenv_value cl'), c1, c2
  in
   let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in
   let output_relation,output_direction,marked_but =
-   (*CSC: this code must be moved into mark_occur, as well as the choice of
-          the output relation *)
-   try
-    Lazy.force coq_prop_relation, Right2Left,
-     mark_occur gl c1 but input_relation input_direction
-      (Lazy.force coq_prop_relation) Right2Left
-   with BackTrack -> try
-    (* This is the case of a proposition of signature A ++> iff or B --> iff *)
-    Lazy.force coq_prop_relation, Left2Right,
-     mark_occur gl c1 but input_relation input_direction
-      (Lazy.force coq_prop_relation) Left2Right
-   with BackTrack -> try
-    Lazy.force coq_prop_relation2, Right2Left,
-     mark_occur gl c1 but input_relation input_direction
-      (Lazy.force coq_prop_relation2) Right2Left
-   with BackTrack ->
-    (*CSC: the error is too detailed. The tactic can now fail also for other
-      CSC: more stupid reasons (i.e. randomly not choosing the right morphism *)
-    errorlabstrm "Setoid_rewrite"
-     (str "The term " ++ prterm c1 ++ str " that must be rewritten occurs " ++
-      str "in a covariant position. You can replace only occurrences that " ++
-        str "are in a contravariant position.")
-  in
-   let cic_output_direction = cic_direction_of_direction output_direction in
-let temporary_solution gl =
+   mark_occur gl c1 but input_relation input_direction in
+  let cic_output_direction = cic_direction_of_direction output_direction in
+  let if_output_relation_is_iff gl =
    let th =
     apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
      cic_output_direction marked_but
@@ -1181,9 +1275,8 @@ let temporary_solution gl =
     let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
      let th' = mkApp (proj, [|impl2; impl1; th|]) in
       Tactics.refine
-       (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
-in
-let temporary_solution2 gl =
+       (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in
+  let if_output_relation_is_if gl =
    let th =
     apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
      cic_output_direction marked_but
@@ -1191,8 +1284,11 @@ let temporary_solution2 gl =
     let new_but = Termops.replace_term c1 c2 but in
      Tactics.refine
       (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
-in
- Tacticals.tclFIRST [temporary_solution ; temporary_solution2] gl
+  in
+   if output_relation = (Lazy.force coq_prop_relation) then
+    if_output_relation_is_iff gl
+   else
+    if_output_relation_is_if gl
 
 let general_s_rewrite lft2rgt c gl =
  let direction = if lft2rgt then Left2Right else Right2Left in