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, 12 insertions, 10 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 1facb7c7ab..6e0ef5af14 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -85,11 +85,6 @@ let build_lambda toabstract stk (m : constr) =
   in
   buildrec m 1 stk
 
-let same_case_structure (_,cs1,ind,_) ci2 br1 br2 =
-  match ind with
-  | Some ind -> ind = ci2.ci_ind
-  | None -> cs1 = ci2.ci_cstr_ndecls
-
 let rec list_insert f a = function
   | [] -> [a]
   | b::l when f a b -> a::b::l
@@ -223,11 +218,18 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
             raise PatternMatchingFailure
 
       | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) ->
-	  if same_case_structure ci1 ci2 br1 br2 then
-  	    array_fold_left2 (sorec stk)
-	      (sorec stk (sorec stk subst a1 a2) p1 p2) br1 br2
-          else
-            raise PatternMatchingFailure
+	  let n2 = Array.length br2 in
+	  if (ci1.cip_ind <> None && ci1.cip_ind <> Some ci2.ci_ind) ||
+	     (not ci1.cip_extensible && List.length br1 <> n2)
+	  then raise PatternMatchingFailure;
+	  let chk_branch subst (j,n,c) =
+	    (* (ind,j+1) is normally known to be a correct constructor
+	       and br2 a correct match over the same inductive *)
+	    assert (j < n2);
+	    sorec stk subst c br2.(j)
+	  in
+	  let chk_head = sorec stk (sorec stk subst a1 a2) p1 p2 in
+	  List.fold_left chk_branch chk_head br1
 
       |	PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
       |	PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst