Ajout tactiques Rename et Pose; modifications pour Inversion

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

5 files changed, 55 insertions, 6 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index ea524791a..c6057367e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -235,19 +235,22 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   else 
     List.rev_append left (moverec [] [declfrom] right)
 
+(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
+   returns [tail::(f head (id,_,_) tail)] *)
 let apply_to_hyp sign id f =
   let found = ref false in
   let sign' =
     fold_named_context_both_sides
-      (fun sign (idc,c,ct as d) tail ->
+      (fun head (idc,c,ct as d) tail ->
 	 if idc = id then begin
-	   found := true; f sign d tail
+	   found := true; f head d tail
 	 end else 
-	   add_named_decl d sign)
+	   add_named_decl d head)
       sign ~init:empty_named_context
   in
   if (not !check) || !found then sign' else error "No such assumption"
 
+(* Same but with whole environment *)
 let apply_to_hyp2 env id f =
   let found = ref false in
   let env' =
@@ -261,6 +264,20 @@ let apply_to_hyp2 env id f =
   in
   if (not !check) || !found then env' else error "No such assumption"
 
+exception Found of int
+
+let apply_to_hyp_and_dependent_on sign id f g =
+  let found = ref false in
+  let sign =
+    Sign.fold_named_context
+      (fun (idc,_,_ as d) oldest ->
+         if idc = id then (found := true; add_named_decl (f d) oldest)
+         else if !found then add_named_decl (g d) oldest
+         else add_named_decl d oldest)
+      sign ~init:empty_named_context
+  in
+  if (not !check) || !found then sign else error "No such assumption"
+
 let global_vars_set_of_var = function
   | (_,None,t) -> global_vars_set (Global.env()) (body_of_type t)
   | (_,Some c,t) ->
@@ -280,7 +297,7 @@ let check_forward_dependencies id tail =
   List.iter
     (function (id',_,_ as decl) ->
        if occur_var_in_decl env id decl then
-	 error ((string_of_id id) ^ " is used in the hypothesis " 
+	 error ((string_of_id id) ^ " is used in hypothesis " 
 		^ (string_of_id id')))
     tail
 
@@ -316,6 +333,12 @@ let convert_def inbody sign sigma id c =
 		  (b,c)) in
 	     add_named_decl (idc,Some b,t) sign)
 
+
+let rename_hyp id1 id2 sign =
+  apply_to_hyp_and_dependent_on sign id1
+    (fun (_,b,t) -> (id2,b,t))
+    (map_named_declaration (replace_vars [id1,mkVar id2]))
+
 let replace_hyp sign id d =
   apply_to_hyp sign id
     (fun sign _ tail ->
@@ -559,9 +582,21 @@ let prim_refiner r sigma goal =
   	let hyps' = 
 	  move_after withdep toleft (left,declfrom,right) hto in
   	[mk_goal hyps' cl]
-	
+
+    | { name = Rename; hypspecs = [id1]; newids = [id2] } ->
+        if id1 <> id2 & List.mem id2 (ids_of_named_context sign) then
+          error ((string_of_id id2)^" is already used");
+        let sign' = rename_hyp id1 id2 sign in
+        let cl' = replace_vars [id1,mkVar id2] cl in
+        [mk_goal sign' cl']
+
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
+(* Util *)
+let rec rebind id1 id2 = function
+  | [] -> []
+  | id::l -> if id = id1 then id2::l else id::(rebind id1 id2 l)
+
 let prim_extractor subfun vl pft =
   let cl = pft.goal.evar_concl in
   match pft with
@@ -653,7 +688,10 @@ let prim_extractor subfun vl pft =
 	
     | {ref=Some(Prim{name=Move _;hypspecs=ids},[pf])} ->
 	subfun vl pf
-	  
+
+    | {ref=Some(Prim{name=Rename;hypspecs=[id1];newids=[id2];},[pf])} ->
+	subfun (rebind id1 id2 vl) pf
+
     | {ref=Some(Prim _,_)} ->
 	error "prim_extractor handed unrecognizable primitive proof"
 	  
@@ -729,5 +767,8 @@ let pr_prim_rule = function
   | {name=Move withdep;hypspecs=[id1;id2]} ->
       (str (if withdep then "Dependent " else "") ++
 	 str"Move "  ++ pr_id id1 ++ str " after " ++ pr_id id2)
+
+  | {name=Rename;hypspecs=[id1];newids=[id2]} ->
+      (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
       
   | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule"
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 9965488c9..f1df084b2 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -46,6 +46,7 @@ type prim_rule_name =
   | Thin
   | ThinBody
   | Move of bool
+  | Rename
 
 type prim_rule = {
   name : prim_rule_name;
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index aab94e4b4..dd6f0f05d 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -49,6 +49,7 @@ type prim_rule_name =
   | Thin
   | ThinBody
   | Move of bool
+  | Rename
 
 type prim_rule = {
   name : prim_rule_name;
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index adb4df3d5..362bac2a6 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -260,6 +260,11 @@ let move_hyp with_dep id1 id2 gl =
                   hypspecs = [id1;id2]; terms = [];
 		  newids = []; params = []}) gl
 
+let rename_hyp id1 id2 gl = 
+  refiner (Prim { name = Rename;
+                  hypspecs = [id1]; terms = [];
+		  newids = [id2]; params = []}) gl
+
 let mutual_fix lf ln lar pf = 
   refiner (Prim { name = FixRule; newids = lf;
                   hypspecs = []; terms = lar;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d520d200d..eba872a77 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -163,6 +163,7 @@ val convert_defbody : identifier -> constr -> tactic
 val thin            : identifier list -> tactic
 val thin_body       : identifier list -> tactic
 val move_hyp        : bool -> identifier -> identifier -> tactic
+val rename_hyp      : identifier -> identifier -> tactic
 val mutual_fix      : identifier list -> int list -> constr list -> tactic
 val mutual_cofix    : identifier list -> constr list -> tactic
 val rename_bound_var_goal : tactic