Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle tactique primitive Cut basé sur un Let non dépendant; amélioration efficacité ancien Cut

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

5 files changed, 30 insertions, 2 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index a5fe2d5962..36c928094d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -379,6 +379,12 @@ let prim_refiner r sigma goal =
 	       if !check then error "Introduction needs a product"
 	       else anomaly "Intro_replacing: expects a product")
 	
+    | { name = Cut b; terms = [t]; newids = [id] } ->
+        if occur_meta t then error_use_instantiate();
+        let sg1 = mk_goal info sign t in
+        let sg2 = mk_goal info (add_named_decl (id,None,t) sign) cl in
+        if b then [sg1;sg2] else [sg2;sg1]  
+
     | { name = Fix; hypspecs = []; terms = []; 
 	newids = [f]; params = [Num(_,n)] } ->
      	let rec check_ind k cl = 
@@ -533,7 +539,11 @@ let prim_extractor subfun vl pft =
 	       let cty = subst_vars vl ty in
 	       mkLetIn (Name id, cb, cty, subfun (id::vl) spf)
 	   | _ -> error "incomplete proof!")
-	
+
+    | {ref=Some(Prim{name=Cut b;terms=[t];newids=[id]},[spf1;spf2]) } ->
+        let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+	mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2)
+
     | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> 
 	let cty = subst_vars vl cl in 
 	let na = Name f in 
@@ -604,6 +614,12 @@ let pr_prim_rule = function
   | {name=Intro_replacing;newids=[id]} -> 
       [< 'sTR"intro replacing " ; pr_id id >]
 	
+  | {name=Cut b;terms=[t];newids=[id]} ->
+      if b then
+        [< 'sTR"TrueCut "; prterm t >]
+      else
+        [< 'sTR"Cut "; prterm t; 'sTR ";[Intro "; pr_id id; 'sTR "|Idtac]" >]
+	
   | {name=Fix;newids=[f];params=[Num(_,n)]} -> 
       [< 'sTR"Fix "; pr_id f; 'sTR"/"; 'iNT n>]
       
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 363dd09645..2820f05f5e 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -36,6 +36,7 @@ type prim_rule_name =
   | Intro
   | Intro_after
   | Intro_replacing
+  | Cut of bool
   | Fix
   | Cofix
   | Refine 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5d415d5a08..16190b8eae 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -39,6 +39,7 @@ type prim_rule_name =
   | Intro
   | Intro_after
   | Intro_replacing
+  | Cut of bool
   | Fix
   | Cofix
   | Refine 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8768dfd315..69697c809f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -223,6 +223,14 @@ let intro_replacing whereid pf =
   refiner (Prim { name = Intro_replacing; newids = [];
                   hypspecs = [whereid]; terms = []; params = [] }) pf
 
+let internal_cut id t pf = 
+  refiner (Prim { name = Cut true; newids = [id];
+                  hypspecs = []; terms = [t]; params = [] }) pf
+
+let internal_cut_rev id t pf = 
+  refiner (Prim { name = Cut false; newids = [id];
+                  hypspecs = []; terms = [t]; params = [] }) pf
+
 let refine c pf = 
   refiner (Prim { name = Refine; terms = [c];
 		  hypspecs = []; newids = []; params = [] }) pf
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e7742f2ecd..721f847243 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -161,8 +161,10 @@ val context       : ctxtty -> tactic
 val refiner         : rule -> tactic
 val introduction    : identifier -> tactic
 val intro_replacing : identifier -> tactic
+val internal_cut    : identifier -> types -> tactic
+val internal_cut_rev : identifier -> types -> tactic
 val refine          : constr -> tactic
-val convert_concl   : constr -> tactic
+val convert_concl   : types -> tactic
 val convert_hyp     : identifier -> types -> tactic
 val convert_deftype : identifier -> types -> tactic
 val convert_defbody : identifier -> constr -> tactic