diff options
| -rw-r--r-- | kernel/indtypes.ml | 23 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 25 |
3 files changed, 32 insertions, 18 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7374f1808b..691992dec9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -39,7 +39,7 @@ let is_constructor_head t = type inductive_error = | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr - | NotConstructor of env * constr * constr + | NotConstructor of env * identifier * constr * constr * int * int | NonPar of env * constr * int * constr * constr | SameNamesTypes of identifier | SameNamesConstructors of identifier @@ -128,7 +128,7 @@ let rec infos_and_sort env t = let small = Term.is_small varj.utj_type in (logic,small) :: (infos_and_sort env1 c2) | _ when is_constructor_head t -> [] - | _ -> anomaly "infos_and_sort: not a positive constructor" + | _ -> (* don't fail if not positive, it is tested later *) [] let small_unit constrsinfos = let issmall = List.for_all is_small constrsinfos @@ -290,7 +290,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum -let explain_ind_err ntyp env0 nbpar c err = +let explain_ind_err id ntyp env0 nbpar c nargs err = let (lpar,c') = mind_extract_params nbpar c in let env = push_rel_context lpar env0 in match err with @@ -301,7 +301,7 @@ let explain_ind_err ntyp env0 nbpar c err = (NotEnoughArgs (env,c',mkRel (kt+nbpar)))) | LocalNotConstructor -> raise (InductiveError - (NotConstructor (env,c',mkRel (ntyp+nbpar)))) + (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs))) | LocalNonPar (n,l) -> raise (InductiveError (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar)))) @@ -397,7 +397,7 @@ let array_min nmr a = if nmr = 0 then 0 else (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = +let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc = let lparams = rel_context_length hyps in let nmr = rel_context_nhyps hyps in (* check the inductive types occur positively in [c] *) @@ -495,14 +495,14 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = in check_constr_rec ienv nmr [] c in let irecargs_nmr = - Array.map - (fun c -> + array_map2 + (fun id c -> let _,rawc = mind_extract_params lparams c in try check_constructors ienv true nmr rawc with IllFormedInd err -> - explain_ind_err (ntypes-i) env lparams c err) - indlc + explain_ind_err id (ntypes-i) env lparams c nargs err) + (Array.of_list lcnames) indlc in let irecargs = Array.map snd irecargs_nmr and nmr' = array_min nmr irecargs_nmr @@ -514,11 +514,12 @@ let check_positivity env_ar params inds = List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in let lparams = rel_context_length params in let nmr = rel_context_nhyps params in - let check_one i (_,_,lc,_) = + let check_one i (_,lcnames,lc,(sign,_)) = let ra_env = list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in - check_positivity_one ienv params i lc + let nargs = rel_context_nhyps sign - nmr in + check_positivity_one ienv params i nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 620cbf5805..5a583bcb13 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -26,7 +26,7 @@ open Typeops type inductive_error = | NonPos of env * constr * constr | NotEnoughArgs of env * constr * constr - | NotConstructor of env * constr * constr + | NotConstructor of env * identifier * constr * constr * int * int | NonPar of env * constr * int * constr * constr | SameNamesTypes of identifier | SameNamesConstructors of identifier diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 128091f44d..784346b244 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -534,12 +534,24 @@ let error_ill_formed_inductive env c v = str "Not enough arguments applied to the " ++ pv ++ str " in" ++ brk(1,1) ++ pc ++ str "." -let error_ill_formed_constructor env c v = - let pc = pr_lconstr_env env c in +let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env v in - str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ - str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ - pv ++ str "." + let atomic = (nb_prod c = 0) in + str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ + str "is not valid;" ++ brk(1,1) ++ + strbrk (if atomic then "it must be " else "its conclusion must be ") ++ + pv ++ + (* warning: because of implicit arguments it is difficult to say which + parameters must be explicitly given *) + (if nparams<>0 then + strbrk " applied to its " ++ str (plural nparams "parameter") + else + mt()) ++ + (if nargs<>0 then + str (if nparams<>0 then " and" else " applied") ++ + strbrk " to some " ++ str (plural nargs "argument") + else + mt()) ++ str "." let error_bad_ind_parameters env c n v1 v2 = let pc = pr_lconstr_env_at_top env c in @@ -593,7 +605,8 @@ let error_not_mutual_in_scheme ind ind' = let explain_inductive_error = function | NonPos (env,c,v) -> error_non_strictly_positive env c v | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v - | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v + | NotConstructor (env,id,c,v,n,m) -> + error_ill_formed_constructor env id c v n m | NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2 | SameNamesTypes id -> error_same_names_types id | SameNamesConstructors id -> error_same_names_constructors id |