factorisation et generalisation des clauses

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

7 files changed, 62 insertions, 40 deletions

diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index ec4282fa2..e0756ca5b 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -209,6 +209,6 @@ let normalize_evaluables=
   onAllClauses
     (function 
 	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some id-> 
+       | Some (id,_,_)-> 
 	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (id,(Tacexpr.InHypTypeOnly,ref None)))
+	   (id,[],(Tacexpr.InHypTypeOnly,ref None)))
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 947ead355..1f9fec6d5 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -29,6 +29,8 @@ and ct_BOOL =
   | CT_true
 and ct_CASE =
     CT_case of string
+and ct_CLAUSE =
+    CT_clause of ct_HYP_LOCATION_LIST_OPT * ct_BOOL
 and ct_COERCION_OPT =
     CT_coerce_NONE_to_COERCION_OPT of ct_NONE
   | CT_coercion_atm
@@ -260,6 +262,14 @@ and ct_HINT_EXPRESSION =
   | CT_immediate of ct_FORMULA
   | CT_resolve of ct_FORMULA
   | CT_unfold_hint of ct_ID
+and ct_HYP_LOCATION =
+    CT_coerce_ID_to_HYP_LOCATION of ct_ID
+  | CT_intype of ct_ID
+  | CT_invalue of ct_ID
+and ct_HYP_LOCATION_LIST =
+    CT_hyp_location_list of ct_HYP_LOCATION list
+and ct_HYP_LOCATION_LIST_OPT =
+    CT_hyp_location_list_opt of ct_HYP_LOCATION_LIST option
 and ct_ID =
     CT_ident of string
   | CT_metac of ct_INT
@@ -287,11 +297,6 @@ and ct_ID_OPT_OR_ALL =
 and ct_ID_OR_INT =
     CT_coerce_ID_to_ID_OR_INT of ct_ID
   | CT_coerce_INT_to_ID_OR_INT of ct_INT
-and ct_ID_OR_INTYPE =
-    CT_coerce_ID_to_ID_OR_INTYPE of ct_ID
-  | CT_intype of ct_ID
-and ct_ID_OR_INTYPE_LIST =
-    CT_id_or_intype_list of ct_ID_OR_INTYPE list
 and ct_ID_OR_INT_OPT =
     CT_coerce_ID_OPT_to_ID_OR_INT_OPT of ct_ID_OPT
   | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT of ct_ID_OR_INT
@@ -473,8 +478,8 @@ and ct_TACTIC_COM =
   | CT_case_type of ct_FORMULA
   | CT_casetac of ct_FORMULA * ct_SPEC_LIST
   | CT_cdhyp of ct_ID
-  | CT_change of ct_FORMULA * ct_ID_OR_INTYPE_LIST
-  | CT_change_local of ct_PATTERN * ct_FORMULA * ct_ID_OR_INTYPE_LIST
+  | CT_change of ct_FORMULA * ct_CLAUSE
+  | CT_change_local of ct_PATTERN * ct_FORMULA * ct_CLAUSE
   | CT_clear of ct_ID_NE_LIST
   | CT_clear_body of ct_ID_NE_LIST
   | CT_cofixtactic of ct_ID_OPT * ct_COFIX_TAC_LIST
@@ -521,7 +526,7 @@ and ct_TACTIC_COM =
   | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
   | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE
-  | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_LIST
+  | CT_lettac of ct_ID * ct_FORMULA * ct_CLAUSE
   | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
@@ -535,7 +540,7 @@ and ct_TACTIC_COM =
   | CT_progress of ct_TACTIC_COM
   | CT_prolog of ct_FORMULA_LIST * ct_INT
   | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
-  | CT_reduce of ct_RED_COM * ct_ID_OR_INTYPE_LIST
+  | CT_reduce of ct_RED_COM * ct_CLAUSE
   | CT_reflexivity
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 7d3ed8dd8..a7e98b69d 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -516,7 +516,7 @@ let blast_auto = (free_try default_full_auto)
 			  (free_try (my_full_eauto 2)))
 *)
 ;;
-let blast_simpl = (free_try (reduce (Simpl None) []))
+let blast_simpl = (free_try (reduce (Simpl None) onConcl))
 ;;
 let blast_induction1 = 
     (free_try (tclTHEN (tclTRY intro)
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index eb7c6a205..3c4602856 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -169,7 +169,7 @@ let make_pbp_atomic_tactic = function
       TacAtom (zz, TacGeneralize [make_app (make_var h) l])
   | PbpLeft -> TacAtom (zz, TacLeft NoBindings)
   | PbpRight -> TacAtom (zz, TacRight NoBindings)
-  | PbpReduce -> TacAtom (zz, TacReduce (Red false, []))
+  | PbpReduce -> TacAtom (zz, TacReduce (Red false, onConcl))
   | PbpIntros l -> 
       let l = List.map (fun id -> IntroIdentifier id) l in
       TacAtom (zz, TacIntroPattern l)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ecc9d1bab..2d63e6339 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1699,7 +1699,7 @@ and natural_fix ig lh g gs narg ltree =
    | _ -> assert false
 and natural_reduce ig lh g gs ge mode la ltree =
   match la with
-    [] -> 
+    {onhyps=Some[];onconcl=true} -> 
       spv
         [  (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
@@ -1707,7 +1707,7 @@ and natural_reduce ig lh g gs ge mode la ltree =
 		  {ihsg=All_subgoals_hyp;isgintro="simpl"})
              ltree)
         ]
-  | [hyp] ->
+  | {onhyps=Some[hyp]; onconcl=false} ->
       spv
         [  (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 760c2286a..5d7cff4cf 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -73,6 +73,11 @@ and fCASE = function
    print_string "\n"and fCOERCION_OPT = function
 | CT_coerce_NONE_to_COERCION_OPT x -> fNONE x
 | CT_coercion_atm -> fNODE "coercion_atm" 0
+and fCLAUSE = function
+| CT_clause(x1,x2) ->
+   fHYP_LOCATION_LIST_OPT x1;
+   fBOOL x2;
+   fNODE "clause" 2
 and fCOFIXTAC = function
 | CT_cofixtac(x1, x2) ->
    fID x1;
@@ -671,6 +676,24 @@ and fHINT_EXPRESSION = function
 | CT_unfold_hint(x1) ->
    fID x1;
    fNODE "unfold_hint" 1
+and fHYP_LOCATION = function
+| CT_coerce_ID_to_HYP_LOCATION x -> fID x
+| CT_intype(x1) ->
+   fID x1;
+   fNODE "intype" 1
+| CT_invalue(x1) ->
+   fID x1;
+   fNODE "invalue" 1
+and fHYP_LOCATION_LIST = function
+| CT_hyp_location_list l ->
+   (List.iter fHYP_LOCATION l);
+   fNODE "hyp_location_list" (List.length l)
+and fHYP_LOCATION_LIST_OPT = function
+| CT_hyp_location_list_opt (Some l) ->
+   fHYP_LOCATION_LIST l;
+   fNODE "hyp_location_list_opt_some" 1
+| CT_hyp_location_list_opt None ->
+   fNODE "hyp_location_list_opt_none" 0
 and fID = function
 | CT_ident x -> fATOM "ident";
    (f_atom_string x);
@@ -712,15 +735,6 @@ and fID_OPT_OR_ALL = function
 and fID_OR_INT = function
 | CT_coerce_ID_to_ID_OR_INT x -> fID x
 | CT_coerce_INT_to_ID_OR_INT x -> fINT x
-and fID_OR_INTYPE = function
-| CT_coerce_ID_to_ID_OR_INTYPE x -> fID x
-| CT_intype(x1) ->
-   fID x1;
-   fNODE "intype" 1
-and fID_OR_INTYPE_LIST = function
-| CT_id_or_intype_list l ->
-   (List.iter fID_OR_INTYPE l);
-   fNODE "id_or_intype_list" (List.length l)
 and fID_OR_INT_OPT = function
 | CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x
 | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x
@@ -1061,12 +1075,12 @@ and fTACTIC_COM = function
    fNODE "cdhyp" 1
 | CT_change(x1, x2) ->
    fFORMULA x1;
-   fID_OR_INTYPE_LIST x2;
+   fCLAUSE x2;
    fNODE "change" 2
 | CT_change_local(x1, x2, x3) ->
    fPATTERN x1;
    fFORMULA x2;
-   fID_OR_INTYPE_LIST x3;
+   fCLAUSE x3;
    fNODE "change_local" 3
 | CT_clear(x1) ->
    fID_NE_LIST x1;
@@ -1232,7 +1246,7 @@ and fTACTIC_COM = function
 | CT_lettac(x1, x2, x3) ->
    fID x1;
    fFORMULA x2;
-   fUNFOLD_LIST x3;
+   fCLAUSE x3;
    fNODE "lettac" 3
 | CT_match_context(x,l) ->
    fCONTEXT_RULE x;
@@ -1286,7 +1300,7 @@ and fTACTIC_COM = function
    fNODE "rec_tactic_in" 2
 | CT_reduce(x1, x2) ->
    fRED_COM x1;
-   fID_OR_INTYPE_LIST x2;
+   fCLAUSE x2;
    fNODE "reduce" 2
 | CT_reflexivity -> fNODE "reflexivity" 0
 | CT_rename(x1, x2) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 41de42b72..6b4b82e39 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -401,15 +401,21 @@ let xlate_hyp = function
 
 let xlate_hyp_location =
  function
-  | AI (_,id), (InHypTypeOnly,_) -> CT_intype(xlate_ident id)
-  | AI (_,id), (InHyp,_) when !Options.v7 ->
-      CT_coerce_ID_to_ID_OR_INTYPE (xlate_ident id)
-  | AI (_,id), ((InHypValueOnly|InHyp),_) ->
+  | AI (_,id), _, (InHypTypeOnly,_) -> CT_intype(xlate_ident id)
+  | AI (_,id), _, (InHyp,_) when !Options.v7 ->
+      CT_coerce_ID_to_HYP_LOCATION (xlate_ident id)
+  | AI (_,id), _, ((InHypValueOnly|InHyp),_) ->
       xlate_error "TODO in v8: InHyp now means InHyp if variable but InHypValueOnly if a local definition"
-  | MetaId _, _ -> 
+  | MetaId _, _,_ -> 
       xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)"
 
-let xlate_clause l = CT_id_or_intype_list (List.map xlate_hyp_location l)
+let xlate_clause cls =
+  CT_clause
+    (CT_hyp_location_list_opt
+      (option_app
+        (fun l -> CT_hyp_location_list(List.map xlate_hyp_location l))
+        cls.onhyps),
+      if cls.onconcl then CT_true else CT_false)
 
 (** Tactics
    *)
@@ -889,8 +895,7 @@ and xlate_tac =
       if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
       else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
     | TacReflexivity -> CT_reflexivity
-    | TacSymmetry None -> CT_symmetry
-    | TacSymmetry (Some _) -> xlate_error "TODO: Symmetry in"
+    | TacSymmetry _ -> xlate_error "TODO: Symmetry <clause>"
     | TacTransitivity c -> CT_transitivity (xlate_formula c)
     | TacAssumption -> CT_assumption
     | TacExact c -> CT_exact (xlate_formula c)
@@ -1014,16 +1019,14 @@ and xlate_tac =
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
 	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
-    | TacInstantiate (a, b, None) -> 
-	CT_instantiate(CT_int a, xlate_formula b)
     | TacInstantiate (a, b, _) -> 
-	xlate_error "TODO: Instantiate ... in"
+	xlate_error "TODO: Instantiate ... <clause>"
 
     | TacLetTac (id, c, cl) ->
         CT_lettac(xlate_ident id, xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
-		  xlate_lettac_clauses cl)
+		  xlate_clause cl)
     | TacForward (true, name, c) -> 
 (* TODO LATER : avoid adding a location that will be ignored *)
                CT_pose(xlate_id_opt ((0,0), name), xlate_formula c)