Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructors

 For instance, consider this inductive type:

    Inductive Ind := A | B | C | D.

 For detecting "match" on this type, one was forced earlier to write code
 in Ltac using "match goal" and/or "context [...]" and long patterns such as:

    match _ with A => _ | B => _ | C => _ | D => _ end

 After this patch, this pattern can be shortened in many alternative ways:

    match _ with A => _ | _ => _ end
    match _ with B => _ | _ => _ end
    match _ in Ind with _ => _ end

 Indeed, if we want to detect a "match" of a given type, we can either
 leave at least one branch where a constructor is explicit, or use a "in"
 annotation.

 Now, we can also detect any "match" regardless of its type:

   match _ with _ => _ end

 Note : this will even detect "match" over empty inductive types.
 Compatibility should be preserved, since "match _ with end" will
 continue to correspond only to empty inductive types.

 Internally, the constr_pattern PCase has changed quite a lot, a few elements
 are now grouped into a case_info_pattern record, while branches are now
 lists of given sub-patterns.

 NB: writing "match" with missing last branches in a constr pattern was actually
 tolerated by Pattern.pattern_of_glob_constr earlier, since the number of
 constructor per inductive is unknown there. And this was triggering an uncaught
 exception in a array_fold_left_2 in Matching later. Oups. At least this patch
 fixes this issue...

 Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number
 of branch in a match pattern. I doubt this was really a problem, but having now
 linear code instead cannot harm ;-)

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

1 files changed, 11 insertions, 2 deletions

diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 23de675989..cde6d4dc98 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -60,6 +60,12 @@ type extended_patvar_map = (patvar * constr_under_binders) list
 
 (** {5 Patterns} *)
 
+type case_info_pattern =
+    { cip_style : case_style;
+      cip_ind : inductive option;
+      cip_ind_args : (int * int) option; (** number of params and args *)
+      cip_extensible : bool (** does this match end with _ => _ ? *) }
+
 type constr_pattern =
   | PRef of global_reference
   | PVar of identifier
@@ -73,11 +79,14 @@ type constr_pattern =
   | PSort of glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of (case_style * int array * inductive option * (int * int) option)
-      * constr_pattern * constr_pattern * constr_pattern array
+  | PCase of case_info_pattern * constr_pattern * constr_pattern *
+      (int * int * constr_pattern) list (** index of constructor, nb of args *)
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
+(** Nota : in a [PCase], the array of branches might be shorter than
+    expected, denoting the use of a final "_ => _" branch *)
+
 (** {5 Functions on patterns} *)
 
 val occur_meta_pattern : constr_pattern -> bool