nouveau Subst:

- marche lorsqu'il n'y rien a reecrire
- marche avec les hypotheses definies (Subst inclut l'Unfold partout)


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

3 files changed, 72 insertions, 38 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index bfa1baf83..4fc8c04e1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -30,6 +30,7 @@ open Evar_refiner
 open Wcclausenv
 open Pattern
 open Hipattern
+open Tacexpr
 open Tacticals
 open Tactics
 open Tacinterp
@@ -103,9 +104,6 @@ let general_rewrite_in lft2rgt id (c,l) gl =
         let hdcncls = string_of_inductive hdcncl in 
 	let suffix =
           Indrec.elimination_suffix (elimination_sort_of_hyp id gl) in
-        let hdcncls = string_of_inductive hdcncl in 
-	let suffix =
-          Indrec.elimination_suffix (elimination_sort_of_hyp id gl) in
         let rwr_thm =
           if lft2rgt then hdcncls^suffix else hdcncls^suffix^"_r" in
         let elim =
@@ -1142,45 +1140,79 @@ let substHypInConcl_RL = substHypInConcl false
 
 (* Substitutions tactics (JCF) *)
 
-exception FoundHyp of identifier
+let unfold_body x gl =
+  let hyps = pf_hyps gl in
+  let xval =
+    match Sign.lookup_named x hyps with
+        (_,Some xval,_) -> xval
+      | _ -> errorlabstrm "unfold_body"
+          (pr_id x ++ str" is not a defined hypothesis") in
+  let aft = afterHyp x gl in
+  let hl = List.fold_right
+    (fun (y,yval,_) cl ->
+      if yval=None then InHypType y :: cl
+      else InHyp y :: InHypType y :: cl) aft [] in
+  let xvar = mkVar x in
+  let rfun _ _ c = replace_term xvar xval c in
+  tclTHENLIST
+    [tclMAP (fun h -> reduct_in_hyp rfun h) hl;
+     reduct_in_concl rfun] gl
+
+
+
+
+exception FoundHyp of named_declaration
 
 let is_eq_x x c =
   let eqpat = build_coq_eq_pattern () in
   (is_matching eqpat c) &&
-  (let (_,y,_) = match_eq eqpat c in
-   match kind_of_term y with Var y -> x = y | _ -> false)
+  let (_,lhs,rhs) = match_eq eqpat c in
+  (x = lhs) && not (occur_term x rhs)
+
+let eq_rhs eq =
+  (snd (destApplication eq)).(2)
 
 let subst_one x gl = 
+  let hyps = pf_hyps gl in
+  let (_,xval,_) = Sign.lookup_named x hyps in
+  if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
   let varx = mkVar x in
-  let hyps = pf_hyps_types gl in
-  let hyp = 
+  let (hyp,rhs) = 
     try
-      let test (id,c) = if is_eq_x x c then raise (FoundHyp id) in
-      List.iter test hyps;
-      errorlabstrm "subst" (str "cannot find any equality over " ++ pr_id x)
-    with FoundHyp id ->
-      id
-  in
-  let dephyps = 
-    let test (id,c) = 
-      if id <> hyp && occur_term varx c then id else failwith "caught" 
-    in
-    map_succeed test hyps
-  in
-  let clear_x = let (_,d,_) = Sign.lookup_named x (pf_hyps gl) in d = None in
-  let dephyps = List.rev dephyps in
-  tclTHENLIST [
-    generalize (List.map mkVar dephyps);
-    thin dephyps;
-    rewriteLR (mkVar hyp);
-    intros_using dephyps;
-    clear [hyp];
-    if clear_x then tclTRY (clear [x]) else tclIDTAC
-  ] gl
-
-let rec subst = function
-  | [] -> tclIDTAC
-  | x :: r -> tclTHEN (subst_one x) (subst r)
+      let test (_,_,c as d) _ = if is_eq_x varx c then raise (FoundHyp d) in
+      Sign.fold_named_context test ~init:() hyps;
+      errorlabstrm "Subst"
+        (str "cannot find any non-recursive equality over " ++ pr_id x)
+    with FoundHyp (id,_,c) -> (id, eq_rhs c) in
+  let depdecls = 
+    let test (id,_,c as dcl) = 
+      if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl
+      else failwith "caught" in
+    List.rev (map_succeed test hyps) in
+  let dephyps = List.map (fun (id,_,_) -> id) depdecls in
+  let abshyps =
+    map_succeed
+      (fun (id,v,_) -> if v=None then mkVar id else failwith "caught")
+      depdecls in
+  let introtac = function
+      (id,None,_) -> intro_using id
+    | (id,Some hval,htyp) ->
+        forward true (Name id) (mkCast(replace_term varx rhs hval,
+                                       replace_term varx rhs htyp)) in
+  tclTHENLIST 
+    ((if depdecls <> [] then
+        if abshyps <> [] then
+          [generalize abshyps;
+           rewriteLR (mkVar hyp);
+           thin dephyps;
+           tclMAP introtac depdecls]
+        else
+          [thin dephyps;
+           tclMAP introtac depdecls]
+      else []) @
+     [tclTRY (clear [x;hyp])]) gl
+
+let subst = tclMAP subst_one
 
 let subst_all gl =
   let eqpat = build_coq_eq_pattern () in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 871444c21..e37e2d29b 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -91,6 +91,8 @@ val discriminable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
 
+val unfold_body : identifier -> tactic
+
 val subst : identifier list -> tactic
 val subst_all : tactic
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 4617ba354..7ea582692 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -220,11 +220,11 @@ let split_dep_and_nodep hyps gl =
     hyps ([],[])
 
 
-let dest_eq gls t =
+let dest_nf_eq gls t =
   match dest_match_eq gls t with
     | [(1,x);(2,y);(3,z)] ->
         (x,pf_whd_betadeltaiota gls y, pf_whd_betadeltaiota gls z)
-    | _ -> error "dest_eq: should be an equality"
+    | _ -> error "dest_nf_eq: should be an equality"
 
 let generalizeRewriteIntros tac depids id gls = 
   let dids = dependent_hyps id depids (pf_env gls) in
@@ -246,7 +246,7 @@ let projectAndApply thin id depids gls =
   let subst_hyp_RL id = tclTRY(hypSubst_RL id None) in
   let subst_hyp gls = 
     let orient_rule id = 
-      let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id) in
+      let (t,t1,t2) = dest_nf_eq gls (pf_get_hyp_typ gls id) in
       match (kind_of_term t1, kind_of_term t2) with
         | Var id1, _ ->
             generalizeRewriteIntros (subst_hyp_LR id) depids id1
@@ -256,7 +256,7 @@ let projectAndApply thin id depids gls =
     in 
     onLastHyp orient_rule gls 
   in
-  let (t,t1,t2) = dest_eq gls (pf_get_hyp_typ gls id)  in
+  let (t,t1,t2) = dest_nf_eq gls (pf_get_hyp_typ gls id)  in
   match (thin, kind_of_term t1, kind_of_term t2) with
     | (true, Var id1,  _) ->
         generalizeRewriteIntros