Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'ClearBody H' et 'Assert H := c'

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

5 files changed, 60 insertions, 0 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 40dce23495..38f2d1d0fc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -246,6 +246,19 @@ let apply_to_hyp sign id f =
   in
   if (not !check) || !found then sign' else error "No such assumption"
 
+let apply_to_hyp2 env id f =
+  let found = ref false in
+  let env' =
+    fold_named_context_both_sides
+      (fun env (idc,c,ct as d) tail ->
+	 if idc = id then begin
+	   found := true; f env d tail
+	 end else 
+	   push_named_decl d env)
+      (named_context env) (reset_context env)
+  in
+  if (not !check) || !found then env' else error "No such assumption"
+
 let global_vars_set_of_var = function
   | (_,None,t) -> global_vars_set (body_of_type t)
   | (_,Some c,t) ->
@@ -318,6 +331,36 @@ let remove_hyp env id =
        if !check then check_forward_dependencies id tail;
        env)
 
+let recheck_typability (what,id) env sigma t =
+  try let _ = type_of env sigma t in ()
+  with _ ->
+    let s = match what with
+      | None -> "the conclusion"
+      | Some id -> "hypothesis "^(string_of_id id) in
+    error
+      ("The correctness of "^s^" relies on the body of "^(string_of_id id))
+  
+let remove_hyp_body env sigma id =
+  apply_to_hyp2 env id
+    (fun env (_,c,t) tail ->
+       match c with
+         | None -> error ((string_of_id id)^" is not a local definition")
+         | Some c ->
+             let env' = push_named_decl (id,None,t) env in
+             if !check then 
+               ignore
+                 (Sign.fold_named_context 
+                    (fun (id',c,t as d) env'' ->
+                       (match c with
+                          | None -> 
+                              recheck_typability (Some id',id) env'' sigma t
+                          | Some b ->
+                              let b' = mkCast (b,t) in
+                              recheck_typability (Some id',id) env'' sigma b');
+                       push_named_decl d env'')
+                    tail env');
+             env')
+
 (* Primitive tactics are handled here *)
 
 let prim_refiner r sigma goal =
@@ -494,6 +537,16 @@ let prim_refiner r sigma goal =
      	let sg = mk_goal info sign' cl in
      	[sg]
 
+    | { name = ThinBody; hypspecs = ids } ->
+	let clear_aux env id =
+          let env' = remove_hyp_body env sigma id in
+          if !check then recheck_typability (None,id) env' sigma cl;
+          env'
+	in
+	let sign' = named_context (List.fold_left clear_aux env ids) in
+     	let sg = mk_goal info sign' cl in
+     	[sg]
+
     | { name = Move withdep; hypspecs = ids } ->
 	let (hfrom,hto) =
 	  match ids with [h1;h2] ->(h1,h2)| _ -> anomaly "prim_refiner:MOVE" in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2820f05f5e..f427ec1f56 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -45,6 +45,7 @@ type prim_rule_name =
   | Convert_defbody
   | Convert_deftype
   | Thin
+  | ThinBody
   | Move of bool
 
 type prim_rule = {
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 16190b8eae..eb31544cbc 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -48,6 +48,7 @@ type prim_rule_name =
   | Convert_defbody
   | Convert_deftype
   | Thin
+  | ThinBody
   | Move of bool
 
 type prim_rule = {
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d2f12d3523..5c1a2c8761 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -254,6 +254,10 @@ let thin ids gl =
   refiner (Prim { name = Thin; hypspecs = ids;
                   terms = []; newids = []; params = []}) gl
 
+let thin_body ids gl = 
+  refiner (Prim { name = ThinBody; hypspecs = ids;
+                  terms = []; newids = []; params = []}) gl
+
 let move_hyp with_dep id1 id2 gl = 
   refiner (Prim { name = Move with_dep;
                   hypspecs = [id1;id2]; terms = [];
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 930588fcb8..640e294394 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -167,6 +167,7 @@ val convert_hyp     : identifier -> types -> tactic
 val convert_deftype : identifier -> types -> tactic
 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 mutual_fix      : identifier list -> int list -> constr list -> tactic
 val mutual_cofix    : identifier list -> constr list -> tactic