Ajouts des causes d'erreur de Indrec

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

5 files changed, 39 insertions, 7 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e48e9dc97..9335a63b7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -5,6 +5,7 @@ open Util
 open Names
 open Generic
 open Term
+open Constant
 open Inductive
 open Sign
 open Environ
@@ -25,6 +26,7 @@ open Typeops
 (* Various well-formedness check for inductive declarations            *)
 
 type inductive_error =
+  (* These are errors related to inductive constructions in this module *)
   | NonPos of name list * constr * constr
   | NotEnoughArgs of name list * constr * constr
   | NotConstructor of name list * constr * constr
@@ -33,6 +35,10 @@ type inductive_error =
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
   | BadEntry
+  (* These are errors related to recursors building in Indrec *)
+  | NotAllowedCaseAnalysis of bool * sorts * inductive
+  | BadInduction of bool * identifier * sorts
+  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
@@ -225,7 +231,7 @@ let listrec_mconstr env ntypes nparams i indlc =
       (* when substituted *) 
       Array.map 
 	(function c -> 
-	   let c' = hnf_prod_appvect env Evd.empty "is_imbr_pos" c 
+	   let c' = hnf_prod_appvect env Evd.empty c 
 		      (Array.map (lift auxntyp) lpar) in 
 	   check_construct false newidx c') 
 	auxlcvect
@@ -312,6 +318,7 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       mind_lc = lc;
       mind_nrealargs = List.length ar_sign - nparams;
       mind_arity  = ar;
+      mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_listrec = recargs;
       mind_finite = finite }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index e955f6009..505ea1d95 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -5,7 +5,7 @@
 open Names
 open Univ
 open Term
-open Inductive
+open Constant
 open Environ
 (*i*)
 
@@ -14,6 +14,7 @@ open Environ
   definition. *)
 
 type inductive_error =
+  (* These are errors related to inductive constructions in this module *)
   | NonPos of name list * constr * constr
   | NotEnoughArgs of name list * constr * constr
   | NotConstructor of name list * constr * constr
@@ -22,6 +23,10 @@ type inductive_error =
   | SameNamesConstructors of identifier * identifier
   | NotAnArity of identifier
   | BadEntry
+  (* These are errors related to recursors building in Indrec *)
+  | NotAllowedCaseAnalysis of bool * sorts * inductive
+  | BadInduction of bool * identifier * sorts
+  | NotMutualInScheme
 
 exception InductiveError of inductive_error
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 3cca1c694..8ca7135aa 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -15,7 +15,7 @@ type type_error =
   | NotAType of constr
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of constr * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * constr * constr
       * (constr * constr * string) option
   | CaseNotInductive of constr * constr
   | NumberBranches of constr * constr * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 66242b7cf..7ffbd312e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -17,7 +17,7 @@ type type_error =
   | NotAType of constr
   | BadAssumption of constr
   | ReferenceVariables of identifier
-  | ElimArity of constr * constr list * constr * constr * constr
+  | ElimArity of inductive * constr list * constr * constr * constr
       * (constr * constr * string) option
   | CaseNotInductive of constr * constr
   | NumberBranches of constr * constr * int
@@ -53,7 +53,7 @@ val error_assumption : path_kind -> env -> constr -> 'b
 val error_reference_variables : path_kind -> env -> identifier -> 'b
 
 val error_elim_arity : 
-  path_kind -> env -> constr -> constr list -> constr 
+  path_kind -> env -> inductive -> constr list -> constr 
     -> constr -> constr -> (constr * constr * string) option -> 'b
 
 val error_case_not_inductive : 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 079ad7ed1..2dfd35a0e 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -57,7 +57,7 @@ let msg_bad_elimination ctx k = function
       [<>]
 
 let explain_elim_arity k ctx ind aritylst c p pt okinds = 
-  let pi = prterm_env ctx ind in
+  let pi = pr_inductive 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 p in
@@ -325,7 +325,7 @@ let explain_refiner_error = function
   | OccurMeta t -> explain_refiner_occur_meta t
   | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg
   | CannotUnify (m,n) -> explain_refiner_cannot_unify m n
-  | CannotGeneralize (_,ty) -> explain_refiner_cannot_generalize ty
+  | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l
 
@@ -381,7 +381,23 @@ let error_not_an_arity id =
 let error_bad_entry () =
   [< 'sTR "Bad inductive definition." >]
 
+let error_not_allowed_case_analysis dep kind i =
+  [< 'sTR (if dep then "Dependent" else "Non Dependent");
+     'sTR " case analysis on sort: "; print_sort kind; 'fNL;
+     'sTR "is not allowed for inductive definition: ";
+     pr_inductive i >]
+
+let error_bad_induction dep indid kind =
+  [<'sTR (if dep then "Dependent" else "Non dependend");
+    'sTR " induction for type "; print_id indid;
+    'sTR " and sort "; print_sort kind; 
+    'sTR "is not allowed">]
+
+let error_not_mutual_in_scheme () =
+ [< 'sTR "Induction schemes is concerned only with mutually inductive types" >]
+
 let explain_inductive_error = function
+  (* These are errors related to inductive constructions *)
   | NonPos (lna,c,v) -> error_non_strictly_positive CCI lna c v
   | NotEnoughArgs (lna,c,v) -> error_ill_formed_inductive CCI lna c v
   | NotConstructor (lna,c,v) -> error_ill_formed_constructor CCI lna c v
@@ -390,3 +406,7 @@ let explain_inductive_error = function
   | SameNamesConstructors (id,cid) -> error_same_names_constructors id cid
   | NotAnArity id -> error_not_an_arity id
   | BadEntry -> error_bad_entry ()
+  (* These are errors related to recursors *)
+  | NotAllowedCaseAnalysis (dep,k,i) -> error_not_allowed_case_analysis dep k i
+  | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
+  | NotMutualInScheme -> error_not_mutual_in_scheme ()