1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: himsg.ml 11986 2009-03-17 11:44:20Z herbelin $ *)
24
open Typeclasses_errors
33
let pr_lconstr c = quote (pr_lconstr c)
34
let pr_lconstr_env e c = quote (pr_lconstr_env e c)
35
let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
36
let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t)
40
match lookup_rel i env with
41
Name id, _, _ -> pr_id id
42
| Anonymous, _, _ -> str "<>"
43
with Not_found -> str "UNBOUND_REL_" ++ int i
45
let explain_unbound_rel env n =
46
let pe = pr_ne_context_of (str "In environment") env in
47
str "Unbound reference: " ++ pe ++
48
str "The reference " ++ int n ++ str " is free."
50
let explain_unbound_var env v =
52
str "No such section variable or assumption: " ++ var ++ str "."
54
let explain_not_type env j =
55
let pe = pr_ne_context_of (str "In environment") env in
56
let pc,pt = pr_ljudge_env env j in
57
pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
58
str "has type" ++ spc () ++ pt ++ spc () ++
59
str "which should be Set, Prop or Type."
61
let explain_bad_assumption env j =
62
let pe = pr_ne_context_of (str "In environment") env in
63
let pc,pt = pr_ljudge_env env j in
64
pe ++ str "Cannot declare a variable or hypothesis over the term" ++
65
brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
66
str "because this term is not a type."
68
let explain_reference_variables c =
69
let pc = pr_lconstr c in
70
str "The constant" ++ spc () ++ pc ++ spc () ++
71
str "refers to variables which are not in the context."
73
let rec pr_disjunction pr = function
75
| [a;b] -> pr a ++ str " or" ++ spc () ++ pr b
76
| a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
79
let explain_elim_arity env ind sorts c pj okinds =
80
let env = make_all_name_different env in
81
let pi = pr_inductive env ind in
82
let pc = pr_lconstr_env env c in
83
let msg = match okinds with
84
| Some(kp,ki,explanation) ->
85
let pki = pr_sort_family ki in
86
let pkp = pr_sort_family kp in
87
let explanation = match explanation with
88
| NonInformativeToInformative ->
89
"proofs can be eliminated only to build proofs"
90
| StrongEliminationOnNonSmallType ->
91
"strong elimination on non-small inductive types leads to paradoxes"
94
let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
95
let ppt = pr_lconstr_env env (snd (decompose_prod_assum pj.uj_type)) in
97
(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
98
str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
101
(str "Elimination of an inductive object of sort " ++
103
str "is not allowed on a predicate in sort " ++ pkp ++ fnl () ++
104
str "because" ++ spc () ++ str explanation ++ str ".")
106
str "ill-formed elimination predicate."
109
str "Incorrect elimination of" ++ spc () ++ pc ++ spc () ++
110
str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++
113
let explain_case_not_inductive env cj =
114
let env = make_all_name_different env in
115
let pc = pr_lconstr_env env cj.uj_val in
116
let pct = pr_lconstr_env env cj.uj_type in
117
match kind_of_term cj.uj_type with
119
str "Cannot infer a type for this expression."
121
str "The term" ++ brk(1,1) ++ pc ++ spc () ++
122
str "has type" ++ brk(1,1) ++ pct ++ spc () ++
123
str "which is not a (co-)inductive type."
125
let explain_number_branches env cj expn =
126
let env = make_all_name_different env in
127
let pc = pr_lconstr_env env cj.uj_val in
128
let pct = pr_lconstr_env env cj.uj_type in
129
str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
130
str "of type" ++ brk(1,1) ++ pct ++ spc () ++
131
str "expects " ++ int expn ++ str " branches."
133
let explain_ill_formed_branch env c i actty expty =
134
let env = make_all_name_different env in
135
let pc = pr_lconstr_env env c in
136
let pa = pr_lconstr_env env actty in
137
let pe = pr_lconstr_env env expty in
138
str "In pattern-matching on term" ++ brk(1,1) ++ pc ++
139
spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++
140
brk(1,1) ++ pa ++ spc () ++
141
str "which should be" ++ brk(1,1) ++ pe ++ str "."
143
let explain_generalization env (name,var) j =
144
let pe = pr_ne_context_of (str "In environment") env in
145
let pv = pr_ltype_env env var in
146
let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) j in
147
pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
148
str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
149
str "it has type" ++ spc () ++ pt ++
150
spc () ++ str "which should be Set, Prop or Type."
152
let explain_actual_type env j pt =
153
let pe = pr_ne_context_of (str "In environment") env in
154
let (pc,pct) = pr_ljudge_env env j in
155
let pt = pr_lconstr_env env pt in
157
str "The term" ++ brk(1,1) ++ pc ++ spc () ++
158
str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
159
str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "."
161
let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl =
162
let env = make_all_name_different env in
163
let nargs = Array.length randl in
164
(* let pe = pr_ne_context_of (str "in environment") env in*)
165
let pr,prt = pr_ljudge_env env rator in
166
let term_string1 = str (plural nargs "term") in
168
if nargs>1 then str "The " ++ nth n ++ str " term" else str "This term" in
169
let appl = prvect_with_sep pr_fnl
171
let pc,pct = pr_ljudge_env env c in
172
hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
174
str "Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
175
str "The term" ++ brk(1,1) ++ pr ++ spc () ++
176
str "of type" ++ brk(1,1) ++ prt ++ spc () ++
177
str "cannot be applied to the " ++ term_string1 ++ fnl () ++
178
str " " ++ v 0 appl ++ fnl () ++ term_string2 ++ str " has type" ++
179
brk(1,1) ++ pr_lconstr_env env actualtyp ++ spc () ++
180
str "which should be coercible to" ++ brk(1,1) ++
181
pr_lconstr_env env exptyp ++ str "."
183
let explain_cant_apply_not_functional env rator randl =
184
let env = make_all_name_different env in
185
let nargs = Array.length randl in
186
(* let pe = pr_ne_context_of (str "in environment") env in*)
187
let pr = pr_lconstr_env env rator.uj_val in
188
let prt = pr_lconstr_env env rator.uj_type in
189
let appl = prvect_with_sep pr_fnl
191
let pc = pr_lconstr_env env c.uj_val in
192
let pct = pr_lconstr_env env c.uj_type in
193
hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
195
str "Illegal application (Non-functional construction): " ++
196
(* pe ++ *) fnl () ++
197
str "The expression" ++ brk(1,1) ++ pr ++ spc () ++
198
str "of type" ++ brk(1,1) ++ prt ++ spc () ++
199
str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++
202
let explain_unexpected_type env actual_type expected_type =
203
let pract = pr_lconstr_env env actual_type in
204
let prexp = pr_lconstr_env env expected_type in
205
str "This type is" ++ spc () ++ pract ++ spc () ++
206
str "but is expected to be" ++
207
spc () ++ prexp ++ str "."
209
let explain_not_product env c =
210
let pr = pr_lconstr_env env c in
211
str "The type of this term is a product" ++ spc () ++
212
str "while it is expected to be" ++
213
(if is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
215
(* TODO: use the names *)
217
let explain_ill_formed_rec_body env err names i fixenv vdefj =
220
Name id -> str "Recursive definition of " ++ pr_id id
221
| Anonymous -> str "The " ++ nth i ++ str " definition" in
223
let st = match err with
225
(* Fixpoint guard errors *)
226
| NotEnoughAbstractionInFixBody ->
227
str "Not enough abstractions in the definition"
228
| RecursionNotOnInductiveType c ->
229
str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++
230
str "which should be an inductive type"
231
| RecursionOnIllegalTerm(j,arg,le,lt) ->
235
| Anonymous -> str "the " ++ nth i ++ str " definition" in
238
([],[]) -> assert false
240
str "a subterm of " ++ pr_db env x
242
str "a subterm of the following variables: " ++
243
prlist_with_sep pr_spc (pr_db env) le
244
| ([x],_) -> pr_db env x
246
str "one of the following variables: " ++
247
prlist_with_sep pr_spc (pr_db env) lt in
248
str "Recursive call to " ++ called ++ spc () ++
249
str "has principal argument equal to" ++ spc () ++
250
pr_lconstr_env env arg ++ fnl () ++ str "instead of " ++ vars
252
| NotEnoughArgumentsForFixCall j ->
256
| Anonymous -> str "the " ++ nth i ++ str " definition" in
257
str "Recursive call to " ++ called ++ str " has not enough arguments"
259
(* CoFixpoint guard errors *)
260
| CodomainNotInductiveType c ->
261
str "The codomain is" ++ spc () ++ pr_lconstr_env env c ++ spc () ++
262
str "which should be a coinductive type"
263
| NestedRecursiveOccurrences ->
264
str "Nested recursive occurrences"
265
| UnguardedRecursiveCall c ->
266
str "Unguarded recursive call in" ++ spc () ++ pr_lconstr_env env c
267
| RecCallInTypeOfAbstraction c ->
268
str "Recursive call forbidden in the domain of an abstraction:" ++
269
spc () ++ pr_lconstr_env env c
270
| RecCallInNonRecArgOfConstructor c ->
271
str "Recursive call on a non-recursive argument of constructor" ++
272
spc () ++ pr_lconstr_env env c
273
| RecCallInTypeOfDef c ->
274
str "Recursive call forbidden in the type of a recursive definition" ++
275
spc () ++ pr_lconstr_env env c
276
| RecCallInCaseFun c ->
277
str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c
278
| RecCallInCaseArg c ->
279
str "Recursive call in the argument of cases in" ++ spc () ++
281
| RecCallInCasePred c ->
282
str "Recursive call in the type of cases in" ++ spc () ++
284
| NotGuardedForm c ->
285
str "Sub-expression " ++ pr_lconstr_env env c ++
286
strbrk " not in guarded form (should be a constructor," ++
287
strbrk " an abstraction, a match, a cofix or a recursive call)"
289
prt_name i ++ str " is ill-formed." ++ fnl () ++
290
pr_ne_context_of (str "In environment") env ++
293
let explain_ill_typed_rec_body env i names vdefj vargs =
294
let env = make_all_name_different env in
295
let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in
296
let pv = pr_lconstr_env env vargs.(i) in
298
(if Array.length vdefj = 1 then mt () else nth (i+1) ++ spc ()) ++
299
str "recursive definition" ++ spc () ++ pvd ++ spc () ++
300
str "has type" ++ spc () ++ pvdt ++ spc () ++
301
str "while it should be" ++ spc () ++ pv ++ str "."
303
let explain_cant_find_case_type env c =
304
let env = make_all_name_different env in
305
let pe = pr_lconstr_env env c in
306
str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "."
308
let explain_occur_check env ev rhs =
309
let env = make_all_name_different env in
310
let id = Evd.string_of_existential ev in
311
let pt = pr_lconstr_env env rhs in
312
str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++
313
pt ++ spc () ++ str "that would depend on itself."
315
let pr_ne_context_of header footer env =
316
if Environ.rel_context env = empty_rel_context &
317
Environ.named_context env = empty_named_context
319
else pr_ne_context_of header env
321
let explain_hole_kind env evi = function
322
| QuestionMark _ -> str "this placeholder"
324
str "the type of this pattern-matching problem"
325
| BinderType (Name id) ->
326
str "the type of " ++ Nameops.pr_id id
327
| BinderType Anonymous ->
328
str "the type of this anonymous binder"
329
| ImplicitArg (c,(n,ido)) ->
330
let id = Option.get ido in
331
str "the implicit parameter " ++
332
pr_id id ++ spc () ++ str "of" ++
333
spc () ++ Nametab.pr_global_env Idset.empty c
335
str "an internal placeholder" ++
336
Option.cata (fun evi ->
337
let env = Evd.evar_env evi in
338
str " of type " ++ pr_lconstr_env env evi.evar_concl ++
339
pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env)
341
| TomatchTypeParameter (tyi,n) ->
342
str "the " ++ nth n ++
343
str " argument of the inductive type (" ++ pr_inductive env tyi ++
346
str "an existential variable"
348
str "the type of an impossible pattern-matching clause"
350
let explain_not_clean env ev t k =
351
let env = make_all_name_different env in
352
let id = Evd.string_of_existential ev in
353
let var = pr_lconstr_env env t in
354
str "Tried to instantiate " ++ explain_hole_kind env None k ++
355
str " (" ++ str id ++ str ")" ++ spc () ++
356
str "with a term using variable " ++ var ++ spc () ++
357
str "which is not in its scope."
359
let explain_unsolvability = function
361
| Some (SeveralInstancesFound n) ->
362
strbrk " (several distinct possible instances found)"
364
let explain_typeclass_resolution env evi k =
366
| GoalEvar | InternalHole | ImplicitArg _ ->
367
(match Typeclasses.class_of_constr evi.evar_concl with
369
let env = Evd.evar_env evi in
370
fnl () ++ str "Could not find an instance for " ++
371
pr_lconstr_env env evi.evar_concl ++
372
pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
376
let explain_unsolvable_implicit env evi k explain =
377
str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++
378
explain_unsolvability explain ++ str "." ++
379
explain_typeclass_resolution env evi k
381
let explain_var_not_found env id =
382
str "The variable" ++ spc () ++ pr_id id ++
383
spc () ++ str "was not found" ++
384
spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "."
386
let explain_wrong_case_info env ind ci =
387
let pi = pr_inductive (Global.env()) ind in
388
if ci.ci_ind = ind then
389
str "Pattern-matching expression on an object of inductive type" ++
390
spc () ++ pi ++ spc () ++ str "has invalid information."
392
let pc = pr_inductive (Global.env()) ci.ci_ind in
393
str "A term of inductive type" ++ spc () ++ pi ++ spc () ++
394
str "was given to a pattern-matching expression on the inductive type" ++
395
spc () ++ pc ++ str "."
397
let explain_cannot_unify env m n =
398
let pm = pr_lconstr_env env m in
399
let pn = pr_lconstr_env env n in
400
str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
401
str "with" ++ brk(1,1) ++ pn ++ str "."
403
let explain_cannot_unify_local env m n subn =
404
let pm = pr_lconstr_env env m in
405
let pn = pr_lconstr_env env n in
406
let psubn = pr_lconstr_env env subn in
407
str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
408
str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++
409
psubn ++ str " contains local variables."
411
let explain_refiner_cannot_generalize env ty =
412
str "Cannot find a well-typed generalisation of the goal with type: " ++
413
pr_lconstr_env env ty ++ str "."
415
let explain_no_occurrence_found env c id =
416
str "Found no subterm matching " ++ pr_lconstr_env env c ++
419
| Some id -> pr_id id
420
| None -> str"the current goal") ++ str "."
422
let explain_cannot_unify_binding_type env m n =
423
let pm = pr_lconstr_env env m in
424
let pn = pr_lconstr_env env n in
425
str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
426
str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "."
428
let explain_cannot_find_well_typed_abstraction env p l =
429
str "Abstracting over the " ++
430
str (plural (List.length l) "term") ++ spc () ++
431
hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++
432
str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
433
str "which is ill-typed."
435
let explain_type_error env err =
436
let env = make_all_name_different env in
439
explain_unbound_rel env n
441
explain_unbound_var env v
443
explain_not_type env j
445
explain_bad_assumption env c
446
| ReferenceVariables id ->
447
explain_reference_variables id
448
| ElimArity (ind, aritylst, c, pj, okinds) ->
449
explain_elim_arity env ind aritylst c pj okinds
450
| CaseNotInductive cj ->
451
explain_case_not_inductive env cj
452
| NumberBranches (cj, n) ->
453
explain_number_branches env cj n
454
| IllFormedBranch (c, i, actty, expty) ->
455
explain_ill_formed_branch env c i actty expty
456
| Generalization (nvar, c) ->
457
explain_generalization env nvar c
458
| ActualType (j, pt) ->
459
explain_actual_type env j pt
460
| CantApplyBadType (t, rator, randl) ->
461
explain_cant_apply_bad_type env t rator randl
462
| CantApplyNonFunctional (rator, randl) ->
463
explain_cant_apply_not_functional env rator randl
464
| IllFormedRecBody (err, lna, i, fixenv, vdefj) ->
465
explain_ill_formed_rec_body env err lna i fixenv vdefj
466
| IllTypedRecBody (i, lna, vdefj, vargs) ->
467
explain_ill_typed_rec_body env i lna vdefj vargs
468
| WrongCaseInfo (ind,ci) ->
469
explain_wrong_case_info env ind ci
471
let explain_pretype_error env err =
472
let env = make_all_name_different env in
474
| CantFindCaseType c -> explain_cant_find_case_type env c
475
| OccurCheck (n,c) -> explain_occur_check env n c
476
| NotClean (n,c,k) -> explain_not_clean env n c k
477
| UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp
478
| VarNotFound id -> explain_var_not_found env id
479
| UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect
480
| NotProduct c -> explain_not_product env c
481
| CannotUnify (m,n) -> explain_cannot_unify env m n
482
| CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn
483
| CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
484
| NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
485
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
486
| CannotFindWellTypedAbstraction (p,l) ->
487
explain_cannot_find_well_typed_abstraction env p l
490
(* Typeclass errors *)
492
let explain_not_a_class env c =
493
pr_constr_env env c ++ str" is not a declared type class."
495
let explain_unbound_method env cid id =
496
str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++
497
pr_global cid ++ str "."
499
let pr_constr_exprs exprs =
500
hv 0 (List.fold_right
501
(fun d pps -> ws 2 ++ Ppconstr.pr_constr_expr d ++ pps)
504
let explain_no_instance env (_,id) l =
505
str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++
506
str "applied to arguments" ++ spc () ++
507
prlist_with_sep pr_spc (pr_lconstr_env env) l
509
let pr_constraints printenv env evm =
510
let l = Evd.to_list evm in
511
let (ev, evi) = List.hd l in
512
if List.for_all (fun (ev', evi') ->
513
eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
515
let pe = pr_ne_context_of (str "In environment:") (mt ())
516
(reset_with_named_context evi.evar_hyps env) in
517
(if printenv then pe ++ fnl () else mt ()) ++
518
prlist_with_sep (fun () -> fnl ())
519
(fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l
523
let explain_unsatisfiable_constraints env evd constr =
524
let evm = Evd.evars_of evd in
527
str"Unable to satisfy the following constraints:" ++ fnl() ++
528
pr_constraints true env evm
530
explain_unsolvable_implicit env evi k None ++ fnl () ++
531
if List.length (Evd.to_list evm) > 1 then
532
str"With the following constraints:" ++ fnl() ++
533
pr_constraints false env evm
536
let explain_mismatched_contexts env c i j =
537
str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
538
hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++ fnl () ++ brk (1,1) ++
539
hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
541
let explain_typeclass_error env err =
543
| NotAClass c -> explain_not_a_class env c
544
| UnboundMethod (cid, id) -> explain_unbound_method env cid id
545
| NoInstance (id, l) -> explain_no_instance env id l
546
| UnsatisfiableConstraints (evd, c) -> explain_unsatisfiable_constraints env evd c
547
| MismatchedContextInstance (c, i, j) -> explain_mismatched_contexts env c i j
551
let explain_refiner_bad_type arg ty conclty =
552
str "Refiner was given an argument" ++ brk(1,1) ++
553
pr_lconstr arg ++ spc () ++
554
str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
555
str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "."
557
let explain_refiner_unresolved_bindings l =
558
str "Unable to find an instance for the " ++
559
str (plural (List.length l) "variable") ++ spc () ++
560
prlist_with_sep pr_coma pr_name l ++ str"."
562
let explain_refiner_cannot_apply t harg =
563
str "In refiner, a term of type" ++ brk(1,1) ++
564
pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
565
pr_lconstr harg ++ str "."
567
let explain_refiner_not_well_typed c =
568
str "The term " ++ pr_lconstr c ++ str " is not well-typed."
570
let explain_intro_needs_product () =
571
str "Introduction tactics needs products."
573
let explain_does_not_occur_in c hyp =
574
str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++
575
str "does not occur in" ++ spc () ++ pr_id hyp ++ str "."
577
let explain_non_linear_proof c =
578
str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
579
spc () ++ str "because a metavariable has several occurrences."
581
let explain_meta_in_type c =
582
str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++
583
str " of another meta"
585
let explain_refiner_error = function
586
| BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
587
| UnresolvedBindings t -> explain_refiner_unresolved_bindings t
588
| CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
589
| NotWellTyped c -> explain_refiner_not_well_typed c
590
| IntroNeedsProduct -> explain_intro_needs_product ()
591
| DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
592
| NonLinearProof c -> explain_non_linear_proof c
593
| MetaInType c -> explain_meta_in_type c
595
(* Inductive errors *)
597
let error_non_strictly_positive env c v =
598
let pc = pr_lconstr_env env c in
599
let pv = pr_lconstr_env env v in
600
str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
601
brk(1,1) ++ pc ++ str "."
603
let error_ill_formed_inductive env c v =
604
let pc = pr_lconstr_env env c in
605
let pv = pr_lconstr_env env v in
606
str "Not enough arguments applied to the " ++ pv ++
607
str " in" ++ brk(1,1) ++ pc ++ str "."
609
let error_ill_formed_constructor env id c v nparams nargs =
610
let pv = pr_lconstr_env env v in
611
let atomic = (nb_prod c = 0) in
612
str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++
613
str "is not valid;" ++ brk(1,1) ++
614
strbrk (if atomic then "it must be " else "its conclusion must be ") ++
616
(* warning: because of implicit arguments it is difficult to say which
617
parameters must be explicitly given *)
619
strbrk " applied to its " ++ str (plural nparams "parameter")
623
str (if nparams<>0 then " and" else " applied") ++
624
strbrk " to some " ++ str (plural nargs "argument")
628
let error_bad_ind_parameters env c n v1 v2 =
629
let pc = pr_lconstr_env_at_top env c in
630
let pv1 = pr_lconstr_env env v1 in
631
let pv2 = pr_lconstr_env env v2 in
632
str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
633
str " as " ++ nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
635
let error_same_names_types id =
636
str "The name" ++ spc () ++ pr_id id ++ spc () ++
637
str "is used more than once."
639
let error_same_names_constructors id =
640
str "The constructor name" ++ spc () ++ pr_id id ++ spc () ++
641
str "is used more than once."
643
let error_same_names_overlap idl =
644
strbrk "The following names are used both as type names and constructor " ++
645
str "names:" ++ spc () ++
646
prlist_with_sep pr_coma pr_id idl ++ str "."
648
let error_not_an_arity id =
649
str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity."
651
let error_bad_entry () =
652
str "Bad inductive definition."
654
let error_large_non_prop_inductive_not_in_type () =
655
str "Large non-propositional inductive types must be in Type."
657
(* Recursion schemes errors *)
659
let error_not_allowed_case_analysis isrec kind i =
660
str (if isrec then "Induction" else "Case analysis") ++
661
strbrk " on sort " ++ pr_sort kind ++
662
strbrk " is not allowed for inductive definition " ++
663
pr_inductive (Global.env()) i ++ str "."
665
let error_not_mutual_in_scheme ind ind' =
667
str "The inductive type " ++ pr_inductive (Global.env()) ind ++
670
str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++
671
str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++
672
str "are not mutually defined."
674
(* Inductive constructions errors *)
676
let explain_inductive_error = function
677
| NonPos (env,c,v) -> error_non_strictly_positive env c v
678
| NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v
679
| NotConstructor (env,id,c,v,n,m) ->
680
error_ill_formed_constructor env id c v n m
681
| NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters env c n v1 v2
682
| SameNamesTypes id -> error_same_names_types id
683
| SameNamesConstructors id -> error_same_names_constructors id
684
| SameNamesOverlap idl -> error_same_names_overlap idl
685
| NotAnArity id -> error_not_an_arity id
686
| BadEntry -> error_bad_entry ()
687
| LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type ()
689
(* Recursion schemes errors *)
691
let explain_recursion_scheme_error = function
692
| NotAllowedCaseAnalysis (isrec,k,i) ->
693
error_not_allowed_case_analysis isrec k i
694
| NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind'
696
(* Pattern-matching errors *)
698
let explain_bad_pattern env cstr ty =
699
let env = make_all_name_different env in
700
let pt = pr_lconstr_env env ty in
701
let pc = pr_constructor env cstr in
702
str "Found the constructor " ++ pc ++ brk(1,1) ++
703
str "while matching a term of type " ++ pt ++ brk(1,1) ++
704
str "which is not an inductive type."
706
let explain_bad_constructor env cstr ind =
707
let pi = pr_inductive env ind in
708
(* let pc = pr_constructor env cstr in*)
709
let pt = pr_inductive env (inductive_of_constructor cstr) in
710
str "Found a constructor of inductive type " ++ pt ++ brk(1,1) ++
711
str "while a constructor of " ++ pi ++ brk(1,1) ++
714
let decline_string n s =
715
if n = 0 then "no "^s^"s"
716
else if n = 1 then "1 "^s
717
else (string_of_int n^" "^s^"s")
719
let explain_wrong_numarg_constructor env cstr n =
720
str "The constructor " ++ pr_constructor env cstr ++
721
str " expects " ++ str (decline_string n "argument") ++ str "."
723
let explain_wrong_numarg_inductive env ind n =
724
str "The inductive type " ++ pr_inductive env ind ++
725
str " expects " ++ str (decline_string n "argument") ++ str "."
727
let explain_wrong_predicate_arity env pred nondep_arity dep_arity=
728
let env = make_all_name_different env in
729
let pp = pr_lconstr_env env pred in
730
str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++
731
str "should be of arity" ++ spc () ++
732
pr_lconstr_env env nondep_arity ++ spc () ++
733
str "(for non dependent case) or" ++
734
spc () ++ pr_lconstr_env env dep_arity ++ spc () ++ str "(for dependent case)."
736
let explain_needs_inversion env x t =
737
let env = make_all_name_different env in
738
let px = pr_lconstr_env env x in
739
let pt = pr_lconstr_env env t in
740
str "Sorry, I need inversion to compile pattern matching on term " ++
741
px ++ str " of type: " ++ pt ++ str "."
743
let explain_unused_clause env pats =
744
(* Without localisation
745
let s = if List.length pats > 1 then "s" else "" in
746
(str ("Unused clause with pattern"^s) ++ spc () ++
747
hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
749
str "This clause is redundant."
751
let explain_non_exhaustive env pats =
752
str "Non exhaustive pattern-matching: no clause found for " ++
753
str (plural (List.length pats) "pattern") ++
754
spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats)
756
let explain_cannot_infer_predicate env typs =
757
let env = make_all_name_different env in
758
let pr_branch (cstr,typ) =
759
let cstr,_ = decompose_app cstr in
760
str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ
762
str "Unable to unify the types found in the branches:" ++
763
spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
765
let explain_pattern_matching_error env = function
766
| BadPattern (c,t) ->
767
explain_bad_pattern env c t
768
| BadConstructor (c,ind) ->
769
explain_bad_constructor env c ind
770
| WrongNumargConstructor (c,n) ->
771
explain_wrong_numarg_constructor env c n
772
| WrongNumargInductive (c,n) ->
773
explain_wrong_numarg_inductive env c n
774
| WrongPredicateArity (pred,n,dep) ->
775
explain_wrong_predicate_arity env pred n dep
776
| NeedsInversion (x,t) ->
777
explain_needs_inversion env x t
778
| UnusedClause tms ->
779
explain_unused_clause env tms
780
| NonExhaustive tms ->
781
explain_non_exhaustive env tms
782
| CannotInferPredicate typs ->
783
explain_cannot_infer_predicate env typs
785
let explain_reduction_tactic_error = function
786
| Tacred.InvalidAbstraction (env,c,(env',e)) ->
787
str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++
788
spc () ++ str "is not well typed." ++ fnl () ++
789
explain_type_error env' e
791
let explain_ltac_call_trace (last,trace,loc) =
792
let calls = last :: List.rev (List.map snd trace) in
793
let pr_call = function
794
| Proof_type.LtacNotationCall s -> quote (str s)
795
| Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
796
| Proof_type.LtacVarCall (id,t) ->
797
quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
798
Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
799
| Proof_type.LtacAtomCall (te,otac) -> quote
800
(Pptactic.pr_glob_tactic (Global.env())
801
(Tacexpr.TacAtom (dummy_loc,te)))
803
| Some te' when (Obj.magic te' <> te) ->
804
strbrk " (expanded to " ++ quote
805
(Pptactic.pr_tactic (Global.env())
806
(Tacexpr.TacAtom (dummy_loc,te')))
809
| Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
811
function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in
812
let unboundvars = list_map_filter filter unboundvars in
813
quote (pr_rawconstr_env (Global.env()) c) ++
814
(if unboundvars <> [] or vars <> [] then
815
strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) ->
816
pr_id id ++ str ":=" ++ Printer.pr_lconstr c)
817
(List.rev vars @ unboundvars) ++ str ")"
820
let kind_of_last_call = match list_last calls with
821
| Proof_type.LtacConstrInterp _ -> ", last term evaluation failed."
822
| _ -> ", last call failed." in
823
hov 0 (str "In nested Ltac calls to " ++
824
pr_enum pr_call calls ++ strbrk kind_of_last_call)
added
removed
toplevel/himsg.ml
