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

9 files changed, 213 insertions, 89 deletions

diff --git a/CHANGES b/CHANGES
index 1cf857df9..cecbae3d3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,10 @@ Specification language and notations
 - Structure/Record printing can be disable by "Unset Printing Records".
   In addition, it can be controlled on type by type basis using
   "Add Printing Record" or "Add Printing Constructor".
+- In a pattern containing a "match", a final "| _ => _" branch could be used
+  now instead of enumerating all remaining constructors. Moreover, the pattern
+  "match _ with _ => _ end" now allows to match any "match". A "in" annotation
+  can also be added to restrict to a precise inductive type.
 
 Tactics
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 8469d6db5..193b38ddb 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -911,6 +911,10 @@ let extern_sort s = extern_glob_sort (detype_sort s)
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
+let any_any_branch =
+  (* | _ => _ *)
+  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evd.InternalHole))
+
 let rec glob_of_pat env = function
   | PRef ref -> GRef (loc,ref)
   | PVar id -> GVar (loc,id)
@@ -938,22 +942,25 @@ let rec glob_of_pat env = function
   | PIf (c,b1,b2) ->
       GIf (loc, glob_of_pat env c, (Anonymous,None),
            glob_of_pat env b1, glob_of_pat env b2)
-  | PCase ((LetStyle,[|n|],ind,None),PMeta None,tm,[|b|]) ->
+  | PCase ({cip_style=LetStyle; cip_ind_args=None},PMeta None,tm,[(0,n,b)]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env b) in
       GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env tm,b)
-  | PCase (_,PMeta None,tm,[||]) ->
-      GCases (loc,RegularStyle,None,[glob_of_pat env tm,(Anonymous,None)],[])
-  | PCase ((_,cstr_nargs,indo,ind_nargs),p,tm,bv) ->
-      let brs = Array.to_list (Array.map (glob_of_pat env) bv) in
-      let brns = Array.to_list cstr_nargs in
-        (* ind is None only if no branch and no return type *)
-      let ind = Option.get indo in
-      let mat = simple_cases_matrix_of_branches ind brns brs in
-      let indnames,rtn =
-	if p = PMeta None then (Anonymous,None),None
-	else
-	  let nparams,n = Option.get ind_nargs in
-	  return_type_of_predicate ind nparams n (glob_of_pat env p) in
+  | PCase (info,p,tm,bl) ->
+      let mat = match bl, info.cip_ind with
+	| [], _ -> []
+	| _, Some ind ->
+	  let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env c)) bl in
+	  simple_cases_matrix_of_branches ind bl'
+	| _, None -> anomaly "PCase with some branches but unknown inductive"
+      in
+      let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
+      in
+      let indnames,rtn = match p, info.cip_ind, info.cip_ind_args with
+	| PMeta None, _, _ -> (Anonymous,None),None
+	| _, Some ind, Some (nparams,nargs) ->
+	  return_type_of_predicate ind nparams nargs (glob_of_pat env p)
+	| _ -> anomaly "PCase with non-trivial predicate but unknown inductive"
+      in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env tm,indnames],mat)
   | PFix f -> Detyping.detype false [] env (mkFix f)
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 72634b08e..c9e135edc 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -170,9 +170,10 @@ let rec interp_xml_constr = function
       let ind = get_xml_inductive al in
       let p = interp_xml_patternsType x in
       let tm = interp_xml_inductiveTerm y in
-      let brs = List.map interp_xml_pattern yl in
-      let brns = Array.to_list (compute_branches_lengths ind) in
-      let mat = simple_cases_matrix_of_branches ind brns brs in
+      let vars = compute_branches_lengths ind in
+      let brs = list_map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
+      in
+      let mat = simple_cases_matrix_of_branches ind brs in
       let nparams,n = compute_inductive_nargs ind in
       let nal,rtn = return_type_of_predicate ind nparams n p in
       GCases (loc,RegularStyle,rtn,[tm,nal],mat)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb1ced154..35aedd2c6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -672,14 +672,14 @@ let rec subst_glob_constr subst raw =
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
 
-let simple_cases_matrix_of_branches ind brns brs =
-  list_map2_i (fun i n b ->
+let simple_cases_matrix_of_branches ind brs =
+  List.map (fun (i,n,b) ->
       let nal,c = it_destRLambda_or_LetIn_names n b in
       let mkPatVar na = PatVar (dummy_loc,na) in
       let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in
       let ids = map_succeed Nameops.out_name nal in
       (dummy_loc,ids,[p],c))
-    0 brns brs
+    brs
 
 let return_type_of_predicate ind nparams nrealargs_ctxt pred =
   let nal,p = it_destRLambda_or_LetIn_names (nrealargs_ctxt+1) pred in
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index a423a471f..40e3d0f82 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -51,7 +51,7 @@ val synthetize_type : unit -> bool
 
 val it_destRLambda_or_LetIn_names : int -> glob_constr -> name list * glob_constr
 val simple_cases_matrix_of_branches :
-  inductive -> int list -> glob_constr list -> cases_clauses
+  inductive -> (int * int * glob_constr) list -> cases_clauses
 val return_type_of_predicate :
   inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr option
 
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 1facb7c7a..6e0ef5af1 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
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index ae86f3142..585de58fb 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -26,6 +26,12 @@ type extended_patvar_map = (patvar * constr_under_binders) list
 
 (* 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
@@ -39,8 +45,8 @@ 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 (** constructor index, nb of args *)
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
@@ -55,7 +61,8 @@ let rec occur_meta_pattern = function
       (occur_meta_pattern c1) or (occur_meta_pattern c2)
   | PCase(_,p,c,br) ->
       (occur_meta_pattern p) or
-      (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
+      (occur_meta_pattern c) or
+      (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
 
@@ -122,11 +129,17 @@ let pattern_of_constr sigma t =
           | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
-	let cip = ci.ci_pp_info in
-	let no = Some (ci.ci_npar,cip.ind_nargs) in
-	PCase ((cip.style,ci.ci_cstr_ndecls,Some ci.ci_ind,no),
-	       pattern_of_constr p,pattern_of_constr a,
-	       Array.map pattern_of_constr br)
+        let cip =
+	  { cip_style = ci.ci_pp_info.style;
+	    cip_ind = Some ci.ci_ind;
+	    cip_ind_args = Some (ci.ci_npar, ci.ci_pp_info.ind_nargs);
+	    cip_extensible = false }
+	in
+	let branch_of_constr i c =
+	  (i, ci.ci_cstr_ndecls.(i), pattern_of_constr c)
+	in
+	PCase (cip, pattern_of_constr p, pattern_of_constr a,
+	       Array.to_list (Array.mapi branch_of_constr br))
     | Fix f -> PFix f
     | CoFix f -> PCoFix f in
   let p = pattern_of_constr t in
@@ -143,7 +156,8 @@ let map_pattern_with_binders g f l = function
   | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
   | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
-  | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p,Array.map (f l) pl)
+  | PCase (ci,po,p,pl) ->
+    PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
   (* Non recursive *)
   | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
   (* Bound to terms *)
@@ -225,14 +239,20 @@ let rec subst_pattern subst pat =
       let c2' = subst_pattern subst c2 in
 	if c' == c && c1' == c1 && c2' == c2 then pat else
 	  PIf (c',c1',c2')
-  | PCase ((a,b,ind,n as cs),typ,c,branches) ->
+  | PCase (cip,typ,c,branches) ->
+      let ind = cip.cip_ind in
       let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in
+      let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
       let typ' = subst_pattern subst typ in
       let c' = subst_pattern subst c in
-      let branches' = array_smartmap (subst_pattern subst) branches in
-      let cs' = if ind == ind' then cs else (a,b,ind',n) in
-	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(cs',typ', c', branches')
+      let subst_branch ((i,n,c) as br) =
+	let c' = subst_pattern subst c in
+	if c' == c then br else (i,n,c')
+      in
+      let branches' = list_smartmap subst_branch branches in
+      if cip' == cip && typ' == typ && c' == c && branches' == branches
+      then pat
+      else PCase(cip', typ', c', branches')
   | PFix fixpoint ->
       let cstr = mkFix fixpoint in
       let fixpoint' = destFix (subst_mps subst cstr) in
@@ -247,6 +267,8 @@ let rec subst_pattern subst pat =
 let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
+let err loc pp = user_err_loc (loc,"pattern_of_glob_constr", pp)
+
 let rec pat_of_raw metas vars = function
   | GVar (_,id) ->
       (try PRel (list_index (Name id) vars)
@@ -287,52 +309,65 @@ let rec pat_of_raw metas vars = function
   | GLetTuple (loc,nal,(_,None),b,c) ->
       let mkGLambda c na = GLambda (loc,na,Explicit,GHole (loc,Evd.InternalHole),c) in
       let c = List.fold_left mkGLambda c nal in
-      PCase ((LetStyle,[|1|],None,None),PMeta None,pat_of_raw metas vars b,
-             [|pat_of_raw metas vars c|])
+      let cip =
+	{ cip_style = LetStyle;
+	  cip_ind = None;
+	  cip_ind_args = None;
+	  cip_extensible = false }
+      in
+      PCase (cip, PMeta None, pat_of_raw metas vars b,
+             [0,1,pat_of_raw metas vars c])
   | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
-      let pred,ind_nargs, ind = match p,indnames with
-	| Some p, Some (_,ind,n,nal) ->
-	    rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p)),
-	    Some (n,List.length nal),Some ind
-	| _ -> PMeta None, None, None in
-      let ind = match ind with Some _ -> ind | None ->
-	match brs with
-	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
-	  | _ -> None in
-      let cbrs =
-	Array.init (List.length brs) (pat_of_glob_branch loc metas vars ind brs)
+      let get_ind = function
+	| (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
+	| _ -> None
+      in
+      let ind_nargs,ind = match indnames with
+	| Some (_,ind,n,nal) -> Some (n,List.length nal), Some ind
+	| None -> None, get_ind brs
+      in
+      let ext,brs = pats_of_glob_branches loc metas vars ind brs
+      in
+      let pred = match p,indnames with
+	| Some p, Some (_,_,_,nal) ->
+	  rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas vars p))
+	| _ -> PMeta None
+      in
+      let info =
+	{ cip_style = sty;
+	  cip_ind = ind;
+	  cip_ind_args = ind_nargs;
+	  cip_extensible = ext }
       in
-      let cstr_nargs,brs = (Array.map fst cbrs, Array.map snd cbrs) in
-      PCase ((sty,cstr_nargs,ind,ind_nargs), pred,
-             pat_of_raw metas vars c, brs)
+      (* Nota : when we have a non-trivial predicate,
+	 the inductive type is known. Same when we have at least
+	 one non-trivial branch. These facts are used in [Constrextern]. *)
+      PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r ->
-      let loc = loc_of_glob_constr r in
-      user_err_loc (loc,"pattern_of_glob_constr", Pp.str"Non supported pattern.")
+  | r -> err (loc_of_glob_constr r) (Pp.str "Non supported pattern.")
 
-and pat_of_glob_branch loc metas vars ind brs i =
-  let bri = List.filter
-    (function
-        (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
-      | (loc,_,_,_) ->
-          user_err_loc (loc,"pattern_of_glob_constr",
-                        Pp.str "Non supported pattern.")) brs in
-  match bri with
-    | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
-	if ind <> None & ind <> Some indsp then
-          user_err_loc (loc,"pattern_of_glob_constr",
-            Pp.str "All constructors must be in the same inductive type.");
-        let lna =
-          List.map
-            (function PatVar(_,na) -> na
-              | PatCstr(loc,_,_,_) ->
-                  user_err_loc (loc,"pattern_of_glob_constr",
-                                Pp.str "Non supported pattern.")) lv in
-        let vars' = List.rev lna @ vars in
-	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
-    | _ -> user_err_loc (loc,"pattern_of_glob_constr",
-                         str "No unique branch for " ++ int (i+1) ++
-                         str"-th constructor.")
+and pats_of_glob_branches loc metas vars ind brs =
+  let get_arg = function
+    | PatVar(_,na) -> na
+    | PatCstr(loc,_,_,_) -> err loc (Pp.str "Non supported pattern.")
+  in
+  let rec get_pat indexes = function
+    | [] -> false, []
+    | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
+    | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs ->
+      if ind <> None && ind <> Some indsp then
+        err loc (Pp.str "All constructors must be in the same inductive type.");
+      if Intset.mem (j-1) indexes then
+	err loc
+          (str "No unique branch for " ++ int j ++ str"-th constructor.");
+      let lna = List.map get_arg lv in
+      let vars' = List.rev lna @ vars in
+      let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
+      let ext,pats = get_pat (Intset.add (j-1) indexes) brs in
+      ext, ((j-1, List.length lv, pat) :: pats)
+    | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.")
+  in
+  get_pat Intset.empty brs
 
 let pattern_of_glob_constr c =
   let metas = ref [] in
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 23de67598..cde6d4dc9 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
diff --git a/test-suite/success/PCase.v b/test-suite/success/PCase.v
new file mode 100644
index 000000000..67d680ba8
--- /dev/null
+++ b/test-suite/success/PCase.v
@@ -0,0 +1,66 @@
+
+(** Some tests of patterns containing matchs ending with joker branches.
+    Cf. the new form of the [constr_pattern] constructor [PCase]
+    in [pretyping/pattern.ml] *)
+
+(* A universal match matcher *)
+
+Ltac kill_match :=
+ match goal with
+   |- context [ match ?x with _ => _ end ] => destruct x
+ end.
+
+(* A match matcher restricted to a given type : nat *)
+
+Ltac kill_match_nat :=
+ match goal with
+   |- context [ match ?x in nat with _ => _ end ] => destruct x
+ end.
+
+(* Another way to restrict to a given type : give a branch *)
+
+Ltac kill_match_nat2 :=
+ match goal with
+   |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x
+ end.
+
+(* This should act only on empty match *)
+
+Ltac kill_match_empty :=
+ match goal with
+   |- context [ match ?x with end ] => destruct x
+ end.
+
+Lemma test1 (b:bool) : if b then True else O=O.
+Proof.
+ Fail kill_match_nat.
+ Fail kill_match_nat2.
+ Fail kill_match_empty.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ Fail kill_match_empty.
+ kill_match_nat. exact I. exact eq_refl.
+Qed.
+
+Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match_nat2. exact I. exact eq_refl.
+Qed.
+
+Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test3a (f:False) : match f return Prop with end.
+Proof.
+ kill_match_empty.
+Qed.
+
+Lemma test3b (f:False) : match f return Prop with end.
+Proof.
+ kill_match.
+Qed.