* The ML tactic is now also aware of rewriting directions.

* Code clean-up.
* Preparation for the last implementation phase.

The last implementation phase will consist in the algorithm that, performing
backtracking, chooses the right combination of morphisms in the syntactic
representation of the goal.


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

1 files changed, 253 insertions, 140 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 9ce587a7cb..7b6ebd7143 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -124,6 +124,7 @@ let coq_variance = lazy(constant ["Setoid"] "variance")
 let coq_Covariant = lazy(constant ["Setoid"] "Covariant")
 let coq_Contravariant = lazy(constant ["Setoid"] "Contravariant")
 let coq_Left2Right = lazy(constant ["Setoid"] "Left2Right")
+let coq_Right2Left = lazy(constant ["Setoid"] "Right2Left")
 let coq_MSNone = lazy(constant ["Setoid"] "MSNone")
 let coq_MSCovariant = lazy(constant ["Setoid"] "MSCovariant")
 let coq_MSContravariant = lazy(constant ["Setoid"] "MSContravariant")
@@ -148,6 +149,7 @@ let coq_fcl_singl = lazy(constant ["Setoid"] "fcl_singl")
 let coq_fcl_cons = lazy(constant ["Setoid"] "fcl_cons")
 
 let coq_setoid_rewrite = lazy(constant ["Setoid"] "setoid_rewrite")
+let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1")
 let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
 let coq_unit = lazy(gen_constant ["Init"; "Datatypes"] "unit")
 let coq_tt = lazy(gen_constant ["Init"; "Datatypes"] "tt")
@@ -176,6 +178,15 @@ let coq_prop_relation =
      rel_sym = Some (gen_constant ["Init"; "Logic"] "iff_sym")
    })
 
+let coq_prop_relation2 =
+ lazy (
+  Relation {
+     rel_a = mkProp ;
+     rel_aeq = Lazy.force coq_impl ;
+     rel_refl = None;
+     rel_sym = None
+   })
+
 
 (************************* Table of declared relations **********************)
 
@@ -723,6 +734,7 @@ let add_setoid a aeq th =
       Relation
        {rel_a = a ; rel_aeq = aeq ; rel_refl = Some refl ; rel_sym = Some sym}
     in
+     (*CSC: coq_prop_relation used here *)
      add_morphism None mor_name
       (aeq,[aeq_rel;aeq_rel],Lazy.force coq_prop_relation)
    end
@@ -732,10 +744,14 @@ let add_setoid a aeq th =
 
 (****************************** The tactic itself *******************************)
 
+type direction =
+   Left2Right
+ | Right2Left
+
 type constr_with_marks =
-  | MApp of constr * morphism_class * constr_with_marks array 
+  | MApp of constr * morphism_class * constr_with_marks array * direction
   | ToReplace
-  | ToKeep of constr
+  | ToKeep of constr * direction
 
 let is_to_replace = function
  | ToKeep _ -> false
@@ -745,6 +761,22 @@ let is_to_replace = function
 let get_mark a = 
   Array.fold_left (||) false (Array.map is_to_replace a)
 
+let cic_direction_of_direction =
+ function
+    Left2Right -> Lazy.force coq_Left2Right
+  | Right2Left -> Lazy.force coq_Right2Left
+
+let opposite_direction =
+ function
+    Left2Right -> Right2Left
+  | Right2Left -> Left2Right
+
+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
+
 type argument =
    Toapply of constr         (* apply the function to the argument *)
  | Toexpand of name * types  (* beta-expand the function w.r.t. an argument
@@ -781,130 +813,168 @@ let relation_of_hypothesis_and_term_to_rewrite gl (_,h) t =
    errorlabstrm "Setoid_rewrite"
     (prterm aeq ++ str " is not a setoid equality.")
 
-let mark_occur t in_c =
- let rec aux in_c =
+exception BackTrack
+
+let mark_occur t in_c input_direction direction =
+ let rec aux direction in_c =
   if eq_constr t in_c then
+(*CSC: The following if should be enabled as soon as backtracking is activated.
+  CSC: Right now it would reject also cases of right-to-left rewriting in
+  CSC: symmetric arguments
+*)
+   if input_direction = direction then
     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 " ++
+      str " in a covariant position. You can replace only occurrences that " ++
+      str " are in a contravariant position.")
+*)
   else
     match kind_of_term in_c with
       | App (c,al) -> 
-          let a = Array.map aux al in
-           if not (get_mark a) then ToKeep in_c
+         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.") ;
+                  Some (relation_morphism_of_constr_morphism morphism)
+             end
+            with Not_found -> None
+         in
+          let a =
+           match mor with
+              None ->
+               (try
+                 Array.map (aux Left2Right) al
+                with BackTrack ->
+                 Array.map (aux Right2Left) al)
+            | Some mor ->
+               let variances = Array.of_list (List.map fst mor.args) in
+               let apply_variance_to_direction default_dir =
+                function
+                   None -> default_dir
+                 | Some true -> direction
+                 | Some false -> opposite_direction direction
+               in
+                Util.array_map2
+                 (fun a variance ->
+                   try
+                    aux (apply_variance_to_direction Left2Right variance) a
+                   with BackTrack ->
+                    aux (apply_variance_to_direction Right2Left variance) a
+                 ) al variances
+          in
+           if not (get_mark a) then ToKeep (in_c,direction)
            else
-            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.") ;
-                     Some
-                      (ACMorphism
-                       (relation_morphism_of_constr_morphism morphism))
-                end
-               with Not_found -> None
-            in
-             (match mor with
-                 Some mor -> MApp (c,mor,a)
-               | 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 env = Global.env() in
-                 let typeofc = (Typing.type_of env Evd.empty 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
-                     [] ->
-                      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))
-                   | (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
-                          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 env c [] typ [] []
-                   (Array.to_list a))
+            (match mor with
+                Some mor -> MApp (c,ACMorphism mor,a,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 env = Global.env() in
+                let typeofc = (Typing.type_of env Evd.empty 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
+                    [] ->
+                     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),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
+                         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 env c [] typ [] []
+                  (Array.to_list a))
       | Prod (_, c1, c2) -> 
           if (dependent (mkRel 1) c2)
-          then ToKeep in_c
+          then ToKeep (in_c,direction)
           else 
-            let c1m = aux c1 in
-            let c2m = aux c2 in
+            let c1m = aux (opposite_direction direction) c1 in
+            let c2m = aux 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 (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
-              else ToKeep in_c
-      | _ -> ToKeep in_c
- in aux in_c
+               aux direction (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
+              else ToKeep (in_c,direction)
+      | _ -> ToKeep (in_c,direction)
+ in
+  aux direction in_c 
 
-let cic_morphism_context_list_of_list hole_relation =
+let cic_morphism_context_list_of_list hole_relation hole_direction out_direction
+=
  let check =
   function
-     None -> 
-      mkApp ((Lazy.force coq_MSNone),
-       [| Lazy.force coq_Left2Right ; Lazy.force coq_Left2Right |])
-   | Some true ->
-      mkApp ((Lazy.force coq_MSCovariant),
-       [| Lazy.force coq_Left2Right |])
-   | Some false ->
-      mkApp ((Lazy.force coq_MSContravariant),
-       [| Lazy.force coq_Left2Right |]) in
+     (None,dir,dir') -> 
+      mkApp ((Lazy.force coq_MSNone), [| dir ; dir' |])
+   | (Some true,dir,dir') ->
+      assert (dir = dir');
+      mkApp ((Lazy.force coq_MSCovariant), [| dir |])
+   | (Some false,dir,dir') ->
+      assert (dir <> dir');
+      mkApp ((Lazy.force coq_MSContravariant), [| dir |]) in
  let rec aux =
   function
      [] -> assert false
-   | [(variance,out),value] ->
+   | [(variance,out),(value,direction)] ->
       mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Argument_Class ; out |]),
       mkApp ((Lazy.force coq_fcl_singl),
-       [| hole_relation; Lazy.force coq_Left2Right ; out ;
-          Lazy.force coq_Left2Right ; Lazy.force coq_Left2Right ;
-          check variance ; value |])
-   | ((variance,out),value)::tl ->
+       [| hole_relation; hole_direction ; out ;
+          direction ; out_direction ;
+          check (variance,direction,out_direction) ; value |])
+   | ((variance,out),(value,direction))::tl ->
       let outtl, valuetl = aux tl in
        mkApp ((Lazy.force coq_cons),
         [| Lazy.force coq_Argument_Class ; out ; outtl |]),
        mkApp ((Lazy.force coq_fcl_cons),
-        [| hole_relation ; Lazy.force coq_Left2Right ; out ; outtl ;
-           Lazy.force coq_Left2Right ; Lazy.force coq_Left2Right ;
-           check variance ; value ; valuetl |])
+        [| hole_relation ; hole_direction ; out ; outtl ;
+           direction ; out_direction ;
+           check (variance,direction,out_direction) ;
+           value ; valuetl |])
  in aux
 
 let rec cic_type_nelist_of_list =
@@ -916,15 +986,17 @@ let rec cic_type_nelist_of_list =
      mkApp ((Lazy.force coq_cons),
       [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |])
 
-let syntactic_but_representation_of_marked_but hole_relation =
+let syntactic_but_representation_of_marked_but hole_relation hole_direction =
  let rec aux out (rel_out,precise_out,is_reflexive) =
   function
-     MApp (f, m, args) ->
+     MApp (f, m, args, direction) ->
+      let direction = cic_direction_of_direction direction in
       let morphism_theory, relations =
        match m with
           ACMorphism { args = args ; lem = lem } -> lem,args
         | ACFunction { f_args = f_args ; f_output = f_output } ->
            let mt =
+            (*CSC: coq_prop_relation used here *)
             if eq_constr out (cic_relation_class_of_relation_class
               (Lazy.force coq_prop_relation))
             then
@@ -944,46 +1016,46 @@ let syntactic_but_representation_of_marked_but hole_relation =
           cic_precise_relation_class_of_relation_class r
         ) relations in
       let cic_args_relations,argst =
-       cic_morphism_context_list_of_list hole_relation
+       cic_morphism_context_list_of_list hole_relation hole_direction direction
         (List.map2
          (fun (variance,trel,t,precise_t) v ->
            (variance,cic_argument_class_of_argument_class (variance,trel)),
-             aux t precise_t v
+             (aux t precise_t v,
+               direction_of_constr_with_marks hole_direction v)
          ) cic_relations (Array.to_list args))
       in
        mkApp ((Lazy.force coq_App),
-        [|hole_relation ; Lazy.force coq_Left2Right ;
-          cic_args_relations ; out ; Lazy.force coq_Left2Right ;
+        [|hole_relation ; hole_direction ;
+          cic_args_relations ; out ; direction ;
           morphism_theory ; argst|])
    | ToReplace ->
-      mkApp ((Lazy.force coq_ToReplace),
-       [| hole_relation ; Lazy.force coq_Left2Right |])
-   | ToKeep c ->
+      mkApp ((Lazy.force coq_ToReplace), [| hole_relation ; hole_direction |])
+   | ToKeep (c,direction) ->
+      let direction = cic_direction_of_direction direction in
        if is_reflexive then
         mkApp ((Lazy.force coq_ToKeep),
-         [| hole_relation ; Lazy.force coq_Left2Right ; precise_out ;
-            Lazy.force coq_Left2Right ; c |])
+         [| hole_relation ; hole_direction ; precise_out ; direction ; c |])
        else
         let c_is_proper =
          let typ = mkApp (rel_out, [| c ; c |]) in
           mkCast (Evarutil.mk_new_meta (),typ)
         in
          mkApp ((Lazy.force coq_ProperElementToKeep),
-          [| hole_relation ; Lazy.force coq_Left2Right; precise_out ;
-             Lazy.force coq_Left2Right; c ; c_is_proper |])
+          [| hole_relation ; hole_direction; precise_out ;
+             direction; c ; c_is_proper |])
  in aux
 
-let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
+let apply_coq_setoid_rewrite hole_relation prop_relation c1 c2 (direction,h)
+ prop_direction m
+=
  let {rel_aeq=hole_equality; rel_sym=hole_symmetry} = hole_relation in
  let hole_relation =
   cic_relation_class_of_relation_class (Relation hole_relation) in
- let prop_relation =
-  cic_relation_class_of_relation_class (Lazy.force coq_prop_relation) in
- let precise_prop_relation =
-  cic_precise_relation_class_of_relation_class
-   (Lazy.force coq_prop_relation) in
- let hyp =
-  if lft2rgt then h else
+ let hyp,hole_direction = h,cic_direction_of_direction direction in
+(*CSC: this old code seems interesting and allows to rewrite in one direction
+   both arguments in covariant and contravariant position. However, this
+   would mean extending a bit also the Coq part of the tactic and I do not
+   know if it is worth the effort.
    match hole_symmetry with
       Some sym ->
        mkApp (sym, [| c2 ; c1 ; h |])
@@ -993,35 +1065,76 @@ let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
          str "relation " ++ prterm hole_equality ++ str " is not known " ++
          str "to be symmetric. Either declare it as a symmetric " ++
          str "relation or use setoid_replace or (setoid_)rewrite from " ++
-         str "left to right only.")
+         str "left to right only.") in
+*)
+ let cic_prop_relation = cic_relation_class_of_relation_class prop_relation in
+ let precise_prop_relation =
+  cic_precise_relation_class_of_relation_class prop_relation
  in
   mkApp ((Lazy.force coq_setoid_rewrite),
-   [| hole_relation ; Lazy.force coq_Left2Right ; prop_relation ;
-      Lazy.force coq_Left2Right ; c1 ; c2 ;
-      syntactic_but_representation_of_marked_but hole_relation
-       prop_relation precise_prop_relation m ; hyp |])
+   [| hole_relation ; hole_direction ; cic_prop_relation ;
+      prop_direction ; c1 ; c2 ;
+      syntactic_but_representation_of_marked_but hole_relation hole_direction
+       cic_prop_relation precise_prop_relation m ; hyp |])
 
-let relation_rewrite c1 c2 (lft2rgt,cl) gl =
+let relation_rewrite c1 c2 (input_direction,cl) gl =
  let but = pf_concl gl in
  let (hyp,c1,c2) =
    let cl' =
      {cl with env = fst (w_unify_to_subterm (pf_env gl) (c1,but) cl.env)} in
    let c1 = Clenv.clenv_nf_meta cl' c1 in
    let c2 = Clenv.clenv_nf_meta cl' c2 in
-   (lft2rgt,Clenv.clenv_value cl'), c1, c2
+   (input_direction,Clenv.clenv_value cl'), c1, c2
  in
   let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in
-  let marked_but = mark_occur c1 but in
-  let th = apply_coq_setoid_rewrite input_relation c1 c2 hyp marked_but in
-   let hyp1 = Termops.replace_term c1 c2 but in
-   let hyp2 = but in
-   let impl1 = mkProd (Anonymous, hyp2, lift 1 hyp1) in
-   let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
-    let th' = mkApp ((Lazy.force coq_proj2), [|impl1; impl2; th|]) in
+  let output_direction,marked_but =
+   (*CSC: this code must be moved into mark_occur, as well as the choice of
+          the output relation *)
+   try
+    Right2Left, mark_occur c1 but input_direction Right2Left
+   with BackTrack -> try
+    Left2Right, mark_occur c1 but input_direction Left2Right
+   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 prop_relation gl =
+   let th =
+    apply_coq_setoid_rewrite input_relation prop_relation c1 c2 hyp
+     cic_output_direction marked_but
+   in
+    let new_but = Termops.replace_term c1 c2 but in
+    let hyp1,hyp2,proj =
+     match output_direction with
+        Right2Left -> new_but, but, Lazy.force coq_proj1
+      | Left2Right -> but, new_but, Lazy.force coq_proj2
+    in
+    let impl1 = mkProd (Anonymous, hyp2, lift 1 hyp1) in
+    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 prop_relation gl =
+   let th =
+    apply_coq_setoid_rewrite input_relation prop_relation c1 c2 hyp
+     cic_output_direction marked_but
+   in
+    let new_but = Termops.replace_term c1 c2 but in
      Tactics.refine
-      (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), hyp1) |])) gl
+      (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
+in
+ (*CSC: the prop_relation will be returned by mark_occur *)
+ Tacticals.tclORELSE (temporary_solution (Lazy.force coq_prop_relation))
+  (temporary_solution2 (Lazy.force coq_prop_relation2)) gl
 
 let general_s_rewrite lft2rgt c gl =
+ let direction = if lft2rgt then Left2Right else Right2Left in
  let ctype = pf_type_of gl c in
  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
@@ -1030,9 +1143,9 @@ let general_s_rewrite lft2rgt c gl =
    | x::y::z -> get_last_two (y::z)
    | _ -> error "The term provided is not an equivalence" in
  let (c1,c2) = get_last_two args in
-   if lft2rgt
-   then relation_rewrite c1 c2 (lft2rgt,eqclause) gl
-   else relation_rewrite c2 c1 (lft2rgt,eqclause) gl
+  match direction with
+     Left2Right -> relation_rewrite c1 c2 (direction,eqclause) gl
+   | Right2Left -> relation_rewrite c2 c1 (direction,eqclause) gl
 
 exception Use_replace