Amélioration messages d'erreur arité incorrecte (notamment record)

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

2 files changed, 47 insertions, 20 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f683e7b443..fb702de0f1 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -59,30 +59,37 @@ let explain_reference_variables c =
   [< 'sTR "the constant"; 'sPC; pc; 'sPC; 
      'sTR "refers to variables which are not in the context" >]
 
-let msg_bad_elimination ctx = function
-  | Some(kp,ki,explanation) ->
-      let pki = prterm_env ctx ki in
-      let pkp = prterm_env ctx kp in
-      (hOV 0 
-         [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
-            pki; 'bRK(1,0);
-            'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
-            'sTR "because"; 'sPC; 'sTR explanation >])
-  | None -> 
-      [<>]
-
 let explain_elim_arity ctx ind aritylst c pj okinds = 
   let pi = pr_inductive ctx ind in
   let ppar = prlist_with_sep pr_coma (prterm_env ctx) aritylst in
   let pc = prterm_env ctx c in
   let pp = prterm_env ctx pj.uj_val in
   let ppt = prterm_env ctx pj.uj_type in
+  let msg = match okinds with
+  | Some(kp,ki,explanation) ->
+      let pki = prterm_env ctx ki in
+      let pkp = prterm_env ctx kp in
+      let explanation =	match explanation with
+	| NonInformativeToInformative ->
+	  "non-informative objects may not construct informative ones."
+	| StrongEliminationOnNonSmallType ->
+          "strong elimination on non-small inductive types leads to paradoxes."
+	| WrongArity ->
+	  "wrong arity" in
+	(hOV 0 
+           [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
+              pki; 'bRK(1,0);
+              'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
+              'sTR "because"; 'sPC; 'sTR explanation >])
+  | None -> 
+      [<>]
+  in
   [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
      'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
      'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
      'sTR "has type"; 'bRK(1,1); ppt; 'fNL;
      'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
-     msg_bad_elimination ctx okinds >]
+     msg >]
 
 let explain_case_not_inductive ctx cj =
   let pc = prterm_env ctx cj.uj_val in
@@ -537,6 +544,13 @@ let explain_non_exhaustive env pats =
   [<'sTR ("Non exhaustive pattern-matching: no clause found for pattern"^s);
     'sPC; hOV 0 (prlist_with_sep pr_spc pr_cases_pattern pats) >]
 
+let explain_cannot_infer_predicate env typs =
+  let pr_branch (cstr,typ) =
+    [< 'sTR "For "; prterm_env env cstr; 'sTR " : "; prterm_env env typ >]
+  in
+  [<'sTR "Unable to unify the types found in the branches:";
+    'sPC; hOV 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) >]
+
 let explain_pattern_matching_error env = function
   | BadPattern (c,t) -> 
       explain_bad_pattern env c t
@@ -552,3 +566,5 @@ let explain_pattern_matching_error env = function
       explain_unused_clause env tms
   | NonExhaustive tms ->
       explain_non_exhaustive env tms
+  | CannotInferPredicate typs ->
+      explain_cannot_infer_predicate env typs
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 896a008371..d113b94505 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -23,6 +23,7 @@ open Inductive
 open Safe_typing
 open Nametab
 open Indtypes
+open Type_errors
 
 (********** definition d'un record (structure) **************)
 
@@ -70,7 +71,7 @@ type record_error =
   | MissingProj of identifier * identifier list
   | BadTypedProj of identifier * env * Type_errors.type_error
 
-let warning_or_error coe err =
+let warning_or_error coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
 	let s,have = if List.length projs > 1 then "s","have" else "","has" in
@@ -78,12 +79,22 @@ let warning_or_error coe err =
 	   'sTR" cannot be defined because the projection"; 'sTR s; 'sPC;
            prlist_with_sep pr_coma pr_id projs; 'sPC; 'sTR have; 'sTR "n't." >]
     | BadTypedProj (fi,ctx,te) ->
-        [<'sTR (string_of_id fi); 
-          'sTR" cannot be defined for the following reason:";
-	  'fNL; 'sTR "  "; hOV 2 (Himsg.explain_type_error ctx te) >]
+	match te with
+	  | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
+              [<'sTR (string_of_id fi); 
+		'sTR" cannot be defined because it is informative and ";
+		Printer.pr_inductive (Global.env()) indsp;
+		'sTR " is not." >]   
+	  | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
+	      [<'sTR (string_of_id fi); 
+		'sTR" cannot be defined because it is large and ";
+		Printer.pr_inductive (Global.env()) indsp;
+		'sTR " is not." >]
+	  | _ -> 
+	      [<'sTR " cannot be defined because it is not typable" >]
   in
   if coe then errorlabstrm "structure" st;
-  pPNL (hOV 0 [< 'sTR"Warning: "; st >])
+  Options.if_verbose pPNL (hOV 0 [< 'sTR"Warning: "; st >])
 
 (* We build projections *)
 let declare_projections indsp coers fields =
@@ -106,7 +117,7 @@ let declare_projections indsp coers fields =
 	   | None -> global_vars env ti in
 	 let bad_projs = (list_intersect ids_not_ok fv_ti) in
 	 if bad_projs <> [] then begin
-	   warning_or_error coe (MissingProj (fi,bad_projs));
+	   warning_or_error coe indsp (MissingProj (fi,bad_projs));
            (None::sp_projs,fi::ids_not_ok,subst)
          end else
 	   let body = match optci with
@@ -128,7 +139,7 @@ let declare_projections indsp coers fields =
 		 declare_constant fi (ConstantEntry cie,NeverDischarge)
 	       in Some sp
              with Type_errors.TypeError (ctx,te) -> begin
-               warning_or_error coe (BadTypedProj (fi,ctx,te));
+               warning_or_error coe indsp (BadTypedProj (fi,ctx,te));
 	       None
 	     end in
 	   match name with