Start documenting new [rewrite_strat] tactic that applies rewriting

according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.  


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

4 files changed, 51 insertions, 32 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 39e0c653c9..4ebe089e96 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -25,13 +25,13 @@ type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
 		  rew_l2r: bool;
-		  rew_tac: glob_tactic_expr }
+		  rew_tac: glob_tactic_expr option }
 
 let subst_hint subst hint =
   let cst' = subst_mps subst hint.rew_lemma in
   let typ' = subst_mps subst hint.rew_type in
   let pat' = subst_mps subst hint.rew_pat in
-  let t' = Tacsubst.subst_tactic subst hint.rew_tac in
+  let t' = Option.smartmap (Tacsubst.subst_tactic subst) hint.rew_tac in
     if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
 	rew_lemma = cst'; rew_type = typ';
@@ -82,16 +82,18 @@ let print_rewrite_hintdb bas =
 	   (fun h ->
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
 	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
-	       str " then use tactic " ++
-	       Pptactic.pr_glob_tactic (Global.env()) h.rew_tac)
+	       Option.cata (fun tac -> str " then use tactic " ++
+	       Pptactic.pr_glob_tactic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
 
-type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr
+type raw_rew_rule = Loc.t * constr * bool * raw_tactic_expr option
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
   let lrul = find_rewrites bas in
-  let lrul = List.map (fun h -> (h.rew_lemma,h.rew_l2r,Tacinterp.eval_tactic h.rew_tac)) lrul in
+  let lrul = List.map (fun h -> 
+  let tac = match h.rew_tac with None -> tclIDTAC | Some t -> Tacinterp.eval_tactic t in
+    (h.rew_lemma,h.rew_l2r,tac)) lrul in
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
         (tclREPEAT_MAIN
@@ -104,7 +106,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
     (List.fold_left (fun tac bas ->
        tclTHEN tac
         (one_base (fun dir c tac ->
-	  let tac = tac, conds in
+	  let tac = (tac, conds) in
 	    general_rewrite dir AllOccurrences true false ~tac c)
 	  tac_main bas))
       tclIDTAC lbas))
@@ -238,7 +240,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
     let eqclause =
       if metas then eqclause
-      else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+      else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
     in
     let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
     let rec split_last_two = function
@@ -286,7 +288,7 @@ let add_rew_rules base lrul =
 	let pat = if b then info.hyp_left else info.hyp_right in
 	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
 		    rew_pat = pat; rew_l2r = b;
-		    rew_tac = Tacintern.glob_tactic t}
+		    rew_tac = Option.map Tacintern.glob_tactic t}
 	in incr counter;
 	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 773e3694eb..9ddabc5846 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Tacmach
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr
+type raw_rew_rule = Loc.t * Term.constr * bool * Tacexpr.raw_tactic_expr option
 
 (** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -29,7 +29,7 @@ type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
 		  rew_l2r: bool;
-		  rew_tac: glob_tactic_expr }
+		  rew_tac: glob_tactic_expr option }
 
 val find_rewrites : string -> rew_rule list
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 75fedc5985..e14c234213 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -259,14 +259,14 @@ let add_rewrite_hint bases ort t lcsr =
 
 VERNAC COMMAND EXTEND HintRewrite
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
-  [ add_rewrite_hint bl o (Tacexpr.TacId []) l ]
+  [ add_rewrite_hint bl o None l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident_list(bl) ] ->
-  [ add_rewrite_hint bl o t l ]
+  [ add_rewrite_hint bl o (Some t) l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  [ add_rewrite_hint ["core"] o (Tacexpr.TacId []) l ]
+  [ add_rewrite_hint ["core"] o None l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  [ add_rewrite_hint ["core"] o t l ]
+  [ add_rewrite_hint ["core"] o (Some t) l ]
 END
 
 (**********************************************************************)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 0e6654545d..f7c13d01a5 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -348,7 +348,22 @@ let refresh_hypinfo env sigma hypinfo =
 	| _ -> hypinfo
   else hypinfo
 
-let unify_eqn env sigma hypinfo t =
+
+let solve_remaining_by by env prf =
+  match by with
+  | None -> env, prf
+  | Some tac ->
+    let indep = clenv_independent env in
+    let tac = eval_tactic tac in
+    let evd' = 
+      List.fold_right (fun mv evd ->
+        let ty = Clenv.clenv_nf_meta env (meta_type evd mv) in
+	let c = Pfedit.build_by_tactic env.env ty (tclCOMPLETE tac) in
+	  meta_assign mv (c, (Conv,TypeNotProcessed)) evd)
+      indep env.evd
+    in { env with evd = evd' }, prf
+
+let unify_eqn env sigma hypinfo by t =
   if isEvar t then None
   else try
     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
@@ -365,10 +380,11 @@ let unify_eqn env sigma hypinfo t =
 (* 	  let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
 	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
 	  let env' = { env' with evd = evd' } in
-	  let nf c = Evarutil.nf_evar evd' (Clenv.clenv_nf_meta env' c) in
+	  let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in	   
+	  let nf c = Evarutil.nf_evar env'.evd (Clenv.clenv_nf_meta env' c) in
 	  let c1 = nf c1 and c2 = nf c2
 	  and car = nf car and rel = nf rel
-	  and prf = nf (Clenv.clenv_value env') in
+	  and prf = nf prf in
 	  let ty1 = Typing.type_of env'.env env'.evd c1
 	  and ty2 = Typing.type_of env'.env env'.evd c2
 	  in
@@ -633,7 +649,7 @@ let apply_constraint env avoid car rel prf cstr res =
 
 let eq_env x y = x == y
 
-let apply_rule hypinfo loccs : strategy =
+let apply_rule hypinfo by loccs : strategy =
   let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
     if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
@@ -641,7 +657,7 @@ let apply_rule hypinfo loccs : strategy =
     fun env avoid t ty cstr evars ->
       if not (eq_env !hypinfo.cl.env env) then
 	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
-      let unif = unify_eqn env (goalevars evars) hypinfo t in
+      let unif = unify_eqn env (goalevars evars) hypinfo by t in
 	if not (Option.is_empty unif) then incr occ;
 	match unif with
 	| Some (evd', (prf, (car, rel, c1, c2))) when is_occ !occ ->
@@ -655,10 +671,10 @@ let apply_rule hypinfo loccs : strategy =
 	    end
 	| _ -> None
 
-let apply_lemma flags (evm,c) left2right loccs : strategy =
+let apply_lemma flags (evm,c) left2right by loccs : strategy =
   fun env avoid t ty cstr evars ->
     let hypinfo = ref (decompose_applied_relation env (goalevars evars) flags None c left2right) in
-      apply_rule hypinfo loccs env avoid t ty cstr evars
+      apply_rule hypinfo by loccs env avoid t ty cstr evars
 
 let make_leibniz_proof c ty r =
   let prf = 
@@ -1010,8 +1026,8 @@ module Strategies =
       fix (fun out -> choice s (one_subterm out))
 
     let lemmas flags cs : strategy =
-      List.fold_left (fun tac (l,l2r) ->
-	choice tac (apply_lemma flags l l2r AllOccurrences))
+      List.fold_left (fun tac (l,l2r,by) ->
+	choice tac (apply_lemma flags l l2r by AllOccurrences))
 	fail cs
 
     let inj_open c = (Evd.empty,c)
@@ -1019,12 +1035,13 @@ module Strategies =
     let old_hints (db : string) : strategy =
       let rules = Autorewrite.find_rewrites db in
 	lemmas rewrite_unif_flags
-	  (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules)
+	  (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r, hint.Autorewrite.rew_tac)) rules)
 
     let hints (db : string) : strategy =
       fun env avoid t ty cstr evars ->
       let rules = Autorewrite.find_matches db t in
-      let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r) in
+      let lemma hint = (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r,
+			hint.Autorewrite.rew_tac) in
       let lems = List.map lemma rules in
 	lemmas rewrite_unif_flags lems env avoid t ty cstr evars
 
@@ -1078,7 +1095,7 @@ end
 (** The strategy for a single rewrite, dealing with occurences. *)
 
 let rewrite_strat flags occs hyp =
-  let app = apply_rule hyp occs in
+  let app = apply_rule hyp None occs in
   let rec aux () =
     Strategies.choice app (subterm true flags (fun env -> aux () env))
   in aux ()
@@ -1359,22 +1376,22 @@ let occurrences_of = function
 let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
   let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
     apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) 
-      l2r occs env avoid t ty cstr (evd, cstrevars evars)
+      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
 let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
   let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
     apply_lemma (general_rewrite_unif_flags ()) (evd, (c, NoBindings)) 
-      l2r occs env avoid t ty cstr (evd, cstrevars evars)
+      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
 let interp_constr_list env sigma =
   List.map (fun c -> 
 	      let evd, c = Constrintern.interp_open_constr sigma env c in
-		(evd, (c, NoBindings)), true)
+		(evd, (c, NoBindings)), true, None)
 
 let interp_glob_constr_list env sigma =
   List.map (fun c -> 
 	      let evd, c = Pretyping.understand_tcc sigma env c in
-		(evd, (c, NoBindings)), true)
+		(evd, (c, NoBindings)), true, None)
 
 (* Syntax for rewriting with strategies *)
 
@@ -1945,7 +1962,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
 let apply_lemma gl (c,l) cl l2r occs =
   let sigma = project gl in
   let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in
-  let app = apply_rule hypinfo occs in
+  let app = apply_rule hypinfo None occs in
   let rec aux () =
     Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env))
   in !hypinfo, aux ()