factorisation et generalisation des clauses

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

6 files changed, 107 insertions, 79 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 491fd467f7..9c450101b0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -137,20 +137,6 @@ GEXTEND Gram
   pattern_occ:
     [ [ nl = LIST0 integer; c = constr -> (nl,c) ] ]
   ;
-  pattern_occ_hyp_tail_list:
-    [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ]
-  ;
-  pattern_occ_hyp_list:
-    [ [ nl = LIST1 natural; IDENT "Goal" -> (Some nl,[])
-      | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list
-        -> (g,(id,nl)::l)
-      | IDENT "Goal" -> (Some [],[])
-      | id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list -> (g,(id,[])::l)
-    ] ]
-  ;
-  clause_pattern:
-    [ [ "in"; p = pattern_occ_hyp_list -> p | -> None, [] ] ]
-  ;
   intropatterns:
     [ [ l = LIST0 simple_intropattern -> l ]]
   ;
@@ -217,18 +203,41 @@ GEXTEND Gram
       | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
   ;
   hypident:
-    [ [ id = id_or_meta -> id,(InHyp,ref None)
-      | "("; "Type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None)
+    [ [ id = id_or_meta -> id,[],(InHyp,ref None)
+      | "("; "Type"; "of"; id = id_or_meta; ")" ->
+          id,[],(InHypTypeOnly,ref None)
     ] ]
   ;
   clause:
-    [ [ "in"; idl = LIST1 hypident -> idl
-      | -> [] ] ]
+    [ [ "in"; idl = LIST1 hypident ->
+        {onhyps=Some idl;onconcl=false; concl_occs=[]}
+      | -> {onhyps=Some[];onconcl=true;concl_occs=[]} ] ]
   ;
   simple_clause:
     [ [ "in"; idl = LIST1 id_or_meta -> idl
       | -> [] ] ]
   ;
+  pattern_occ_hyp_tail_list:
+    [ [ pl = pattern_occ_hyp_list -> pl
+      | -> {onhyps=Some[];onconcl=false; concl_occs=[]} ] ]
+  ;
+  pattern_occ_hyp_list:
+    [ [ nl = LIST1 natural; IDENT "Goal" ->
+          {onhyps=Some[];onconcl=true;concl_occs=nl}
+      | nl = LIST1 natural; id = id_or_meta; cls = pattern_occ_hyp_tail_list
+        -> {cls with
+            onhyps=option_app(fun l -> (id,nl,(InHyp,ref None))::l)
+              cls.onhyps} 
+      | IDENT "Goal" -> {onhyps=Some[];onconcl=true;concl_occs=[]}
+      | id = id_or_meta; cls = pattern_occ_hyp_tail_list ->
+         {cls with
+          onhyps=option_app(fun l -> (id,[],(InHyp,ref None))::l)
+            cls.onhyps} ] ]
+  ;
+  clause_pattern:
+    [ [ "in"; p = pattern_occ_hyp_list -> p 
+      | -> {onhyps=None; onconcl=true; concl_occs=[] } ] ]
+  ;
   fixdecl:
     [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ]
   ;
@@ -293,9 +302,8 @@ GEXTEND Gram
       | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
       | IDENT "LetTac"; id = base_ident; ":="; c = constr; p = clause_pattern
         -> TacLetTac (id,c,p)
-      | IDENT "Instantiate"; n = natural; c = constr; 
-	  ido = OPT [ "in"; id = id_or_ltac_ref -> id ] -> 
-	    TacInstantiate (n,c,ido)
+      | IDENT "Instantiate"; n = natural; c = constr; cls = clause -> 
+	    TacInstantiate (n,c,cls)
       | IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
       | IDENT "LApply"; c = constr -> TacLApply c
@@ -346,8 +354,7 @@ GEXTEND Gram
 
       (* Equivalence relations *)
       | IDENT "Reflexivity" -> TacReflexivity
-      | IDENT "Symmetry"; ido = OPT [ "in"; id = id_or_ltac_ref -> id ] -> 
-	  TacSymmetry ido
+      | IDENT "Symmetry"; cls = clause -> TacSymmetry cls
       | IDENT "Transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 54af7a4f2f..77a5d919bf 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -181,27 +181,15 @@ GEXTEND Gram
       | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr ->
 	  (Some (nl,c1), c2) ] ]
   ;
+  occurrences:
+    [ [ "at"; nl = LIST1 integer -> nl
+      | -> [] ] ]
+  ;
   pattern_occ:
-    [ [ c = constr; "at"; nl = LIST0 integer -> (nl,c)
-      | c = constr -> ([],c) ] ]
+    [ [ c = constr; nl = occurrences -> (nl,c) ] ]
   ;
   unfold_occ:
-    [ [ c = global; "at"; nl = LIST0 integer -> (nl,c)
-      | c = global -> ([],c) ] ]
-  ;
-  pattern_occ_hyp_tail_list:
-    [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ]
-  ;
-  pattern_occ_hyp_list:
-    [ [ nl = LIST1 natural; IDENT "Goal" -> (Some nl,[])
-      | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list
-	  -> (g,(id,nl)::l)
-      | IDENT "Goal" -> (Some [],[])
-      | id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list -> (g,(id,[])::l)
-    ] ]
-  ;
-  clause_pattern:
-    [ [ "in"; p = pattern_occ_hyp_list -> p | -> None, [] ] ]
+    [ [ c = global; nl = occurrences -> (nl,c) ] ]
   ;
   intropatterns:
     [ [ l = LIST0 simple_intropattern -> l ]]
@@ -267,9 +255,23 @@ GEXTEND Gram
       | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id,(InHypValueOnly,ref None)
     ] ]
   ;
+  hypident_occ:
+    [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ]
+  ;
   clause:
-    [ [ "in"; idl = LIST1 hypident -> idl
-      | -> [] ] ]
+    [ [ "in"; "*"; occs=occurrences ->
+        {onhyps=None;onconcl=true;concl_occs=occs}
+      | "in"; "*"; "|-"; (b,occs)=concl_occ ->
+          {onhyps=None; onconcl=b; concl_occs=occs}
+      | "in"; hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ ->
+          {onhyps=Some hl; onconcl=b; concl_occs=occs}
+      | "in"; hl=LIST0 hypident_occ SEP"," ->
+          {onhyps=Some hl; onconcl=false; concl_occs=[]}
+      | -> {onhyps=Some[];onconcl=true; concl_occs=[]} ] ]
+  ;
+  concl_occ:
+    [ [ "*"; occs = occurrences -> (true,occs)
+      | -> (false, []) ] ]
   ;
   simple_clause:
     [ [ "in"; idl = LIST1 id_or_meta -> idl
@@ -339,10 +341,10 @@ GEXTEND Gram
       | IDENT "generalize"; IDENT "dependent"; c = constr ->
           TacGeneralizeDep c
       | IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")";
-          p = clause_pattern -> TacLetTac (id,c,p)
+          p = clause -> TacLetTac (id,c,p)
       | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")";
-	  ido = OPT [ "in"; id = id_or_meta -> id ] ->
-            TacInstantiate (n,c,ido)
+	  cls = clause ->
+            TacInstantiate (n,c,cls)
 	    
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
@@ -396,8 +398,7 @@ GEXTEND Gram
 
       (* Equivalence relations *)
       | IDENT "reflexivity" -> TacReflexivity
-      | IDENT "symmetry"; ido = OPT [ "in"; id = id_or_meta -> id ] -> 
-	  TacSymmetry ido
+      | IDENT "symmetry"; cls = clause -> TacSymmetry cls
       | IDENT "transitivity"; c = constr -> TacTransitivity c
 
       (* Equality and inversion *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ccda07549e..12e57e85f9 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -141,27 +141,35 @@ let pr_with_names = function
   | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids)
 
 let pr_hyp_location pr_id = function
-  | id, (InHyp,_) -> spc () ++ pr_id id
-  | id, (InHypTypeOnly,_) -> spc () ++ str "(Type of " ++ pr_id id ++ str ")"
-  | id, _ -> error "Unsupported hyp location in v7"
+  | id, _, (InHyp,_) -> spc () ++ pr_id id
+  | id, _, (InHypTypeOnly,_) ->
+      spc () ++ str "(Type of " ++ pr_id id ++ str ")"
+  | id, _, _ -> error "Unsupported hyp location in v7"
 
 let pr_clause pr_id = function
   | [] -> mt ()
   | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
 
+
+let pr_clauses pr_id cls =
+  match cls with
+      { onhyps = Some l; onconcl = false } ->
+        spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l)
+    | { onhyps = Some []; onconcl = true } -> mt()
+    | _ -> error "this clause has both hypothesis and conclusion"
+
 let pr_simple_clause pr_id = function
   | [] -> mt ()
   | l -> spc () ++
       hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l)
 
-let pr_clause_pattern pr_id = function
-  | (None, []) -> mt ()
-  | (glopt,l) ->
-      str " in" ++
-      prlist
-        (fun (id,nl) -> prlist (pr_arg int) nl 
-	  ++ spc () ++ pr_id id) l ++
-        pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt
+let pr_clause_pattern pr_id cls =
+  pr_opt
+    (prlist (fun (id,occs,_) ->
+      prlist (pr_arg int) occs ++ spc () ++ pr_id id)) cls.onhyps ++
+  if cls.onconcl then
+    prlist (pr_arg int) cls.concl_occs ++ spc() ++ str"Goal"
+  else mt()
 
 let pr_subterms pr occl =
   hov 0 (pr_occurrences pr occl ++ spc () ++ str "with")
@@ -400,7 +408,6 @@ let rec pr_atom0 = function
   | TacAutoTDB None -> str "AutoTDB"
   | TacDestructConcl -> str "DConcl"
   | TacReflexivity -> str "Reflexivity"
-  | TacSymmetry None -> str "Symmetry"
   | t -> str "(" ++ pr_atom1 t ++ str ")"
 
   (* Main tactic printer *)
@@ -459,12 +466,10 @@ and pr_atom1 = function
       pr_constr c)
   | TacLetTac (id,c,cl) ->
       hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++
-        pr_constr c ++ pr_clause_pattern pr_ident cl)
-  | TacInstantiate (n,c,None) ->
-      hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c)
-  | TacInstantiate (n,c,Some id) ->
+        pr_constr c ++ pr_clauses pr_ident cl)
+  | TacInstantiate (n,c,cls) ->
       hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ 
-	     spc () ++ str "in" ++ pr_arg pr_ident id)
+	     pr_clauses pr_ident cls)
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
@@ -538,14 +543,14 @@ and pr_atom1 = function
 
   (* Conversion *)  
   | TacReduce (r,h) ->
-      hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h)
+      hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clauses pr_ident h)
   | TacChange (occl,c,h) ->
       hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++ 
-        brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
+        brk (1,1) ++ pr_constr c ++ pr_clauses pr_ident h)
 
   (* Equivalence relations *)
-  | (TacReflexivity | TacSymmetry None) as x -> pr_atom0 x
-  | TacSymmetry (Some id) -> str "Symmetry " ++ pr_ident id
+  | TacReflexivity as x -> pr_atom0 x
+  | TacSymmetry cls -> str "Symmetry " ++ pr_clauses pr_ident cls
   | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c
 
   (* Equality and inversion *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index dfe341beb8..decb60923d 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -132,10 +132,6 @@ let mlexpr_of_reference = function
   | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >>
   | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >>
 
-let mlexpr_of_bool = function
-  | true -> <:expr< True >>
-  | false -> <:expr< False >>
-
 let mlexpr_of_intro_pattern = function
   | Tacexpr.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO"
   | Tacexpr.IntroWildcard -> <:expr< Tacexpr.IntroWildcard >>
@@ -158,10 +154,22 @@ let mlexpr_of_loc loc = <:expr< $dloc$ >>
 
 let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
 
+let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int
+
 let mlexpr_of_hyp_location = function
-  | id, (Tacexpr.InHyp,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHyp, ref None)) >>
-  | id, (Tacexpr.InHypTypeOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypTypeOnly, ref None)) >>
-  | id, (Tacexpr.InHypValueOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypValueOnly,ref None)) >>
+  | id, occs, (Tacexpr.InHyp,_) ->
+      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHyp, ref None)) >>
+  | id, occs, (Tacexpr.InHypTypeOnly,_) ->
+      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHypTypeOnly, ref None)) >>
+  | id, occs, (Tacexpr.InHypValueOnly,_) ->
+      <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHypValueOnly,ref None)) >>
+
+let mlexpr_of_clause cl =
+  <:expr< {Tacexpr.onhyps=
+             $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location)
+               cl.Tacexpr.onhyps$;
+           Tacexpr.onconcl= $mlexpr_of_bool cl.Tacexpr.onconcl$;
+           Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >>
 
 (*
 let mlexpr_of_red_mode = function
@@ -418,16 +426,16 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Conversion *)
   | Tacexpr.TacReduce (r,cl) ->
-      let l = mlexpr_of_list mlexpr_of_hyp_location cl in
+      let l = mlexpr_of_clause cl in
       <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >>
   | Tacexpr.TacChange (occl,c,cl) ->
-      let l = mlexpr_of_list mlexpr_of_hyp_location cl in
+      let l = mlexpr_of_clause cl in
       let g = mlexpr_of_option mlexpr_of_occ_constr in
       <:expr< Tacexpr.TacChange $g occl$ $mlexpr_of_constr c$ $l$ >>
 
   (* Equivalence relations *)
   | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>
-  | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_option mlexpr_of_hyp ido$ >>
+  | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 85259d6e4b..5dcb0686da 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -54,6 +54,11 @@ let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
 (* We don't give location for tactic quotation! *)
 let loc = dummy_loc
 
+
+let mlexpr_of_bool = function
+  | true -> <:expr< True >>
+  | false -> <:expr< False >>
+
 let mlexpr_of_int n = <:expr< $int:string_of_int n$ >>
 
 let mlexpr_of_string s = <:expr< $str:s$ >>
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 6be871a0af..c858f2c0e9 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -20,6 +20,8 @@ val mlexpr_of_triple :
   ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr)
     -> 'a * 'b * 'c -> MLast.expr
 
+val mlexpr_of_bool : bool -> MLast.expr
+
 val mlexpr_of_int : int -> MLast.expr
 
 val mlexpr_of_string : string -> MLast.expr