Mise en place d'un test de clauses non utilisees

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

3 files changed, 23 insertions, 20 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 14a4a24f2d..221b0998d3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -33,7 +33,7 @@ type pattern_matching_error =
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
-  | RedundantClause of cases_pattern list
+  | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
 
 exception PatternMatchingError of env * pattern_matching_error
@@ -220,6 +220,7 @@ type equation =
       rhs          : rhs;
       alias_stack  : name list;
       eqn_loc      : loc;
+      used         : bool ref;
       tag          : pattern_source }
 
 type matrix = equation list
@@ -493,24 +494,19 @@ let check_all_variables typ mat =
 	   error_bad_pattern_loc loc (cstr_sp,ctxt_of_ids ids) typ)
     mat
 
-let check_number_of_regular_eqns pb eqns =
-  match List.filter is_regular eqns with
-    | [] -> (*warning "Found several default clauses, kept the first one"*) ()
-    | [_] -> ()
-    | _::eqn::_ ->
-	let tms = match pb.history with
-	  | Result tms -> tms 
-	  | _ -> assert false in
-	raise_pattern_matching_error
-	  (eqn.eqn_loc, pb.env, RedundantClause tms)
+let check_unused_pattern env eqn =
+  if not !(eqn.used) then 
+    raise_pattern_matching_error
+      (eqn.eqn_loc, env, UnusedClause eqn.patterns)
+
+let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with 
     | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
-    | (eqn::_::_ as eqns) ->
-	check_number_of_regular_eqns pb eqns;
+    | eqn::_ ->
+	set_used_pattern eqn;
 	eqn.tag, eqn.rhs
-    | [eqn] -> eqn.tag, eqn.rhs
 
 (**********************************************************************)
 (* Functions to deal with matrix factorization *)
@@ -1223,6 +1219,7 @@ let matx_of_eqns env tomatchl eqns =
       tag = RegularPat;
       alias_stack = [];
       eqn_loc = loc;
+      used = ref false;
       rhs = rhs }
   in List.map build_eqn eqns
 
@@ -1432,6 +1429,9 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
       typing_function = typing_fun } in
   
   let _, j = compile pb in
+
+  (* We check for unused patterns *)
+  List.iter (check_unused_pattern env) matx;
   
   match tycon with
     | Some p ->	Coercion.inh_conv_coerce_to loc env isevars j p
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index acd9f3089f..a7dddb5cb2 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -24,7 +24,7 @@ type pattern_matching_error =
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * constr * constr
   | NeedsInversion of constr * constr
-  | RedundantClause of cases_pattern list
+  | UnusedClause of cases_pattern list
   | NonExhaustive of cases_pattern list
 
 exception PatternMatchingError of env * pattern_matching_error
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index fb78b56d9b..34cb1a13b0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -502,10 +502,13 @@ let explain_needs_inversion ctx x t =
   [< 'sTR "Sorry, I need inversion to compile pattern matching of term ";
      px ; 'sTR " of type: "; pt>]
 
-let explain_redundant_clauses env pats =
+let explain_unused_clause env pats =
   let s = if List.length pats > 1 then "s" else "" in
-  [<'sTR ("Redundant clause for pattern"^s); 'sPC;
-    hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats) >]
+(* Without localisation
+  [<'sTR ("Unused clause with pattern"^s); 'sPC;
+    hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats); 'sTR ")" >]
+*)
+  [<'sTR "This clause is redundant" >]
 
 let explain_non_exhaustive env pats =
   let s = if List.length pats > 1 then "s" else "" in
@@ -523,7 +526,7 @@ let explain_pattern_matching_error env = function
       explain_wrong_predicate_arity env pred n dep
   | NeedsInversion (x,t) ->
       explain_needs_inversion env x t
-  | RedundantClause tms ->
-      explain_redundant_clauses env tms
+  | UnusedClause tms ->
+      explain_unused_clause env tms
   | NonExhaustive tms ->
       explain_non_exhaustive env tms