aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/inductive.ml9
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/type_errors.ml7
-rw-r--r--kernel/type_errors.mli9
-rw-r--r--toplevel/himsg.ml42
-rw-r--r--toplevel/record.ml25
6 files changed, 65 insertions, 29 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d7181299e..c9399925b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -222,14 +222,13 @@ let is_info_arity env c =
let error_elim_expln env kp ki =
if is_info_arity env kp && not (is_info_arity env ki) then
- "non-informative objects may not construct informative ones."
+ NonInformativeToInformative
else
match (kind_of_term kp,kind_of_term ki) with
- | Sort (Type _), Sort (Prop _) ->
- "strong elimination on non-small inductive types leads to paradoxes."
- | _ -> "wrong arity"
+ | Sort (Type _), Sort (Prop _) -> StrongEliminationOnNonSmallType
+ | _ -> WrongArity
-exception Arity of (constr * constr * string) option
+exception Arity of (constr * constr * arity_error) option
let is_correct_arity env kelim (c,pj) indf t =
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 7e08a31c0..720ae3e4a 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -46,7 +46,7 @@ val type_of_constructor : env -> constructor -> types
val arities_of_constructors : env -> inductive -> types array
-exception Arity of (constr * constr * string) option
+exception Arity of (constr * constr * Type_errors.arity_error) option
(* [type_case_branches env (I,args) (p:A) c] computes useful types
about the following Cases expression:
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f1eb32b5b..fc98a2ef1 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -34,6 +34,11 @@ type guard_error =
| RecCallInCasePred of constr
| NotGuardedForm
+type arity_error =
+ | NonInformativeToInformative
+ | StrongEliminationOnNonSmallType
+ | WrongArity
+
type type_error =
| UnboundRel of int
| UnboundVar of variable
@@ -41,7 +46,7 @@ type type_error =
| BadAssumption of unsafe_judgment
| ReferenceVariables of constr
| ElimArity of inductive * types list * constr * unsafe_judgment
- * (constr * constr * string) option
+ * (constr * constr * arity_error) option
| CaseNotInductive of unsafe_judgment
| WrongCaseInfo of inductive * case_info
| NumberBranches of unsafe_judgment * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 99b46877a..a18ffd7e5 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -36,6 +36,11 @@ type guard_error =
| RecCallInCasePred of constr
| NotGuardedForm
+type arity_error =
+ | NonInformativeToInformative
+ | StrongEliminationOnNonSmallType
+ | WrongArity
+
type type_error =
| UnboundRel of int
| UnboundVar of variable
@@ -43,7 +48,7 @@ type type_error =
| BadAssumption of unsafe_judgment
| ReferenceVariables of constr
| ElimArity of inductive * types list * constr * unsafe_judgment
- * (constr * constr * string) option
+ * (constr * constr * arity_error) option
| CaseNotInductive of unsafe_judgment
| WrongCaseInfo of inductive * case_info
| NumberBranches of unsafe_judgment * int
@@ -71,7 +76,7 @@ val error_reference_variables : env -> constr -> 'a
val error_elim_arity :
env -> inductive -> types list -> constr
- -> unsafe_judgment -> (constr * constr * string) option -> 'a
+ -> unsafe_judgment -> (constr * constr * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f683e7b44..fb702de0f 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 896a00837..d113b9450 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:55:23 +0000