a try to make intro patterns better

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

3 files changed, 49 insertions, 30 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index e50d1a1f6f..7efed88d6c 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -365,10 +365,13 @@ and ct_INT =
     CT_int of int
 and ct_INTRO_PATT =
     CT_coerce_ID_to_INTRO_PATT of ct_ID
-  | CT_conj_pattern of ct_INTRO_PATT_LIST
-  | CT_disj_pattern of ct_INTRO_PATT_LIST
+  | CT_conj_pattern of ct_INTRO_PATT_LIST * ct_INTRO_PATT_LIST list
+  | CT_disj_pattern of ct_INTRO_PATT_LIST * ct_INTRO_PATT_LIST list
 and ct_INTRO_PATT_LIST =
     CT_intro_patt_list of ct_INTRO_PATT list
+and ct_INTRO_PATT_OPT =
+    CT_coerce_ID_OPT_to_INTRO_PATT_OPT of ct_ID_OPT
+  | CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT of ct_INTRO_PATT
 and ct_INT_LIST =
     CT_int_list of ct_INT list
 and ct_INT_NE_LIST =
@@ -575,7 +578,7 @@ and ct_TACTIC_COM =
   | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA
   | CT_decompose_record of ct_FORMULA
   | CT_decompose_sum of ct_FORMULA
-  | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_LIST * ct_FORMULA_OPT
+  | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_OPT * ct_FORMULA_OPT
   | CT_deprewrite_lr of ct_ID
   | CT_deprewrite_rl of ct_ID
   | CT_destruct of ct_ID_OR_INT
@@ -603,7 +606,7 @@ and ct_TACTIC_COM =
   | CT_intro_after of ct_ID_OPT * ct_ID
   | CT_intros of ct_INTRO_PATT_LIST
   | CT_intros_until of ct_ID_OR_INT
-  | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_LIST * ct_ID_LIST
+  | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_OPT * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
   | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE
   | CT_lettac of ct_ID_OPT * ct_FORMULA * ct_CLAUSE
@@ -611,8 +614,8 @@ and ct_TACTIC_COM =
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
-  | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST
-  | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST
+  | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT
+  | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
   | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index f39e210464..3a2c9b1cbb 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -917,16 +917,21 @@ and fINT = function
    (f_atom_int x);
    print_string "\n"and fINTRO_PATT = function
 | CT_coerce_ID_to_INTRO_PATT x -> fID x
-| CT_conj_pattern(x1) ->
-   fINTRO_PATT_LIST x1;
-   fNODE "conj_pattern" 1
-| CT_disj_pattern(x1) ->
-   fINTRO_PATT_LIST x1;
-   fNODE "disj_pattern" 1
+| CT_conj_pattern(x,l) ->
+   fINTRO_PATT_LIST x;
+   (List.iter fINTRO_PATT_LIST l);
+   fNODE "conj_pattern" (1 + (List.length l))
+| CT_disj_pattern(x,l) ->
+   fINTRO_PATT_LIST x;
+   (List.iter fINTRO_PATT_LIST l);
+   fNODE "disj_pattern" (1 + (List.length l))
 and fINTRO_PATT_LIST = function
 | CT_intro_patt_list l ->
    (List.iter fINTRO_PATT l);
    fNODE "intro_patt_list" (List.length l)
+and fINTRO_PATT_OPT = function
+| CT_coerce_ID_OPT_to_INTRO_PATT_OPT x -> fID_OPT x
+| CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT x -> fINTRO_PATT x
 and fINT_LIST = function
 | CT_int_list l ->
    (List.iter fINT l);
@@ -1366,7 +1371,7 @@ and fTACTIC_COM = function
 | CT_depinversion(x1, x2, x3, x4) ->
    fINV_TYPE x1;
    fID_OR_INT x2;
-   fINTRO_PATT_LIST x3;
+   fINTRO_PATT_OPT x3;
    fFORMULA_OPT x4;
    fNODE "depinversion" 4
 | CT_deprewrite_lr(x1) ->
@@ -1467,7 +1472,7 @@ and fTACTIC_COM = function
 | CT_inversion(x1, x2, x3, x4) ->
    fINV_TYPE x1;
    fID_OR_INT x2;
-   fINTRO_PATT_LIST x3;
+   fINTRO_PATT_OPT x3;
    fID_LIST x4;
    fNODE "inversion" 4
 | CT_left(x1) ->
@@ -1501,12 +1506,12 @@ and fTACTIC_COM = function
 | CT_new_destruct(x1, x2, x3) ->
    fFORMULA_OR_INT x1;
    fUSING x2;
-   fINTRO_PATT_LIST x3;
+   fINTRO_PATT_OPT x3;
    fNODE "new_destruct" 3
 | CT_new_induction(x1, x2, x3) ->
    fFORMULA_OR_INT x1;
    fUSING x2;
-   fINTRO_PATT_LIST x3;
+   fINTRO_PATT_OPT x3;
    fNODE "new_induction" 3
 | CT_omega -> fNODE "omega" 0
 | CT_orelse(x1, x2) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index dd7aa015f9..a3233c1dd6 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -601,14 +601,20 @@ let get_flag r =
   (* Rem: EVAR flag obsolète *)
   conv_flags, red_ids
 
-let rec xlate_intro_pattern =
+let ct_conj_pattern x y = CT_conj_pattern(x, y);;
+
+let ct_disj_pattern x y = CT_disj_pattern(x,y);;
+
+let rec xlate_intro_pattern b =
  function
-  | IntroOrAndPattern [l] ->
-      CT_conj_pattern(CT_intro_patt_list (List.map xlate_intro_pattern l))
-  | IntroOrAndPattern ll ->
-      let insert_conj l = CT_conj_pattern (CT_intro_patt_list
-        (List.map xlate_intro_pattern l))
-      in CT_disj_pattern(CT_intro_patt_list (List.map insert_conj ll))
+  | IntroOrAndPattern [] -> assert false
+  | IntroOrAndPattern (fp::ll) ->
+      (if b then ct_disj_pattern else ct_conj_pattern)
+      (CT_intro_patt_list(List.map (xlate_intro_pattern (not b)) fp))
+      (List.map 
+	 (fun l ->
+	    CT_intro_patt_list(List.map (xlate_intro_pattern (not b)) l))
+	 ll)
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
 
@@ -672,12 +678,16 @@ let xlate_lettac_clauses = function
 	      CT_unfold_list((CT_coerce_ID_to_UNFOLD(CT_ident "Goal"))::res)
 	  | None -> CT_unfold_list res;;
 
-let xlate_intro_patt_list c =
- CT_intro_patt_list
-   (List.map
-      (fun l -> 
-	 CT_conj_pattern (CT_intro_patt_list (List.map xlate_intro_pattern l)))
-      c);;
+let xlate_intro_patt_list = function
+    [] -> assert false
+  | (fp::ll) ->
+      CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT
+	(CT_disj_pattern
+    	   (CT_intro_patt_list(List.map (xlate_intro_pattern false) fp),
+	    List.map
+	      (fun l -> 
+		 CT_intro_patt_list(List.map (xlate_intro_pattern false) l))
+	      ll));;
 
 let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
   function
@@ -922,7 +932,8 @@ and xlate_tac =
 	CT_move_after(xlate_hyp id1, xlate_hyp id2)
     | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
     | TacIntroPattern patt_list ->
-	CT_intros (CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
+	CT_intros
+	  (CT_intro_patt_list (List.map (xlate_intro_pattern true) patt_list))
     | TacIntroMove (Some id, None) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
     | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)