diff options
-rw-r--r-- | kernel/indtypes.ml | 9 | ||||
-rw-r--r-- | kernel/indtypes.mli | 7 | ||||
-rw-r--r-- | kernel/type_errors.ml | 2 | ||||
-rw-r--r-- | kernel/type_errors.mli | 4 | ||||
-rw-r--r-- | toplevel/himsg.ml | 24 |
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 () |