diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 285 |
1 files changed, 230 insertions, 55 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 62d19bea..1bd68014 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Flags @@ -28,7 +26,7 @@ open Reduction open Cases open Logic open Printer -open Rawterm +open Glob_term open Evd let pr_lconstr c = quote (pr_lconstr c) @@ -52,7 +50,8 @@ let explain_unbound_var env v = let var = pr_id v in str "No such section variable or assumption: " ++ var ++ str "." -let explain_not_type env j = +let explain_not_type env sigma j = + let j = j_nf_evar sigma j in let pe = pr_ne_context_of (str "In environment") env in let pc,pt = pr_ljudge_env env j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -111,7 +110,8 @@ let explain_elim_arity env ind sorts c pj okinds = str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++ fnl () ++ msg -let explain_case_not_inductive env cj = +let explain_case_not_inductive env sigma cj = + let cj = j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -123,7 +123,8 @@ let explain_case_not_inductive env cj = str "has type" ++ brk(1,1) ++ pct ++ spc () ++ str "which is not a (co-)inductive type." -let explain_number_branches env cj expn = +let explain_number_branches env sigma cj expn = + let cj = j_nf_evar sigma cj in let env = make_all_name_different env in let pc = pr_lconstr_env env cj.uj_val in let pct = pr_lconstr_env env cj.uj_type in @@ -131,14 +132,17 @@ let explain_number_branches env cj expn = str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches." -let explain_ill_formed_branch env c i actty expty = +let explain_ill_formed_branch env sigma c ci actty expty = + let simp t = Reduction.nf_betaiota (nf_evar sigma t) in + let c = nf_evar sigma c in let env = make_all_name_different env in let pc = pr_lconstr_env env c in - let pa = pr_lconstr_env env actty in - let pe = pr_lconstr_env env expty in - str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++ - brk(1,1) ++ pa ++ spc () ++ + let pa = pr_lconstr_env env (simp actty) in + let pe = pr_lconstr_env env (simp expty) in + strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ + spc () ++ strbrk "the branch for constructor" ++ spc () ++ + quote (pr_constructor env ci) ++ + spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." let explain_generalization env (name,var) j = @@ -150,7 +154,9 @@ let explain_generalization env (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_actual_type env j pt = +let explain_actual_type env sigma j pt = + let j = j_nf_betaiotaevar sigma j in + let pt = Reductionops.nf_betaiota sigma pt in let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in let pt = pr_lconstr_env env pt in @@ -159,7 +165,11 @@ let explain_actual_type env j pt = str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." -let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = +let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = + let randl = jv_nf_betaiotaevar sigma randl in + let exptyp = nf_evar sigma exptyp in + let actualtyp = Reductionops.nf_betaiota sigma actualtyp in + let rator = j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -181,7 +191,9 @@ let explain_cant_apply_bad_type env (n,exptyp,actualtyp) rator randl = str "which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env env exptyp ++ str "." -let explain_cant_apply_not_functional env rator randl = +let explain_cant_apply_not_functional env sigma rator randl = + let randl = jv_nf_evar sigma randl in + let rator = j_nf_evar sigma rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env in*) @@ -200,14 +212,16 @@ let explain_cant_apply_not_functional env rator randl = str "cannot be applied to the " ++ str (plural nargs "term") ++ fnl () ++ str " " ++ v 0 appl -let explain_unexpected_type env actual_type expected_type = +let explain_unexpected_type env sigma actual_type expected_type = + let actual_type = nf_evar sigma actual_type in + let expected_type = nf_evar sigma expected_type in let pract = pr_lconstr_env env actual_type in let prexp = pr_lconstr_env env expected_type in - str "This type is" ++ spc () ++ pract ++ spc () ++ - str "but is expected to be" ++ - spc () ++ prexp ++ str "." + str "Found type" ++ spc () ++ pract ++ spc () ++ + str "where" ++ spc () ++ prexp ++ str " was expected." -let explain_not_product env c = +let explain_not_product env sigma c = + let c = nf_evar sigma c in let pr = pr_lconstr_env env c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ @@ -229,7 +243,8 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be an inductive type" - | RecursionOnIllegalTerm(j,arg,le,lt) -> + | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> + let arg_env = make_all_name_different arg_env in let called = match names.(j) with Name id -> pr_id id @@ -247,7 +262,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = prlist_with_sep pr_spc pr_db lt in str "Recursive call to " ++ called ++ spc () ++ strbrk "has principal argument equal to" ++ spc () ++ - pr_lconstr_env env arg ++ strbrk " instead of " ++ vars + pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = @@ -274,12 +289,12 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = str "Recursive call forbidden in the type of a recursive definition" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseFun c -> - str "Recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c + str "Invalid recursive call in a branch of" ++ spc () ++ pr_lconstr_env env c | RecCallInCaseArg c -> - str "Recursive call in the argument of cases in" ++ spc () ++ + str "Invalid recursive call in the argument of \"match\" in" ++ spc () ++ pr_lconstr_env env c | RecCallInCasePred c -> - str "Recursive call in the type of cases in" ++ spc () ++ + str "Invalid recursive call in the \"return\" clause of \"match\" in" ++ spc () ++ pr_lconstr_env env c | NotGuardedForm c -> str "Sub-expression " ++ pr_lconstr_env env c ++ @@ -295,7 +310,9 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = str"Recursive definition is:" ++ spc () ++ pvd ++ str "." with _ -> mt ()) -let explain_ill_typed_rec_body env i names vdefj vargs = +let explain_ill_typed_rec_body env sigma i names vdefj vargs = + let vdefj = jv_nf_evar sigma vdefj in + let vargs = Array.map (nf_evar sigma) vargs in let env = make_all_name_different env in let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in let pv = pr_lconstr_env env vargs.(i) in @@ -305,12 +322,14 @@ let explain_ill_typed_rec_body env i names vdefj vargs = str "has type" ++ spc () ++ pvdt ++ spc () ++ str "while it should be" ++ spc () ++ pv ++ str "." -let explain_cant_find_case_type env c = +let explain_cant_find_case_type env sigma c = + let c = nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env c in str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." -let explain_occur_check env ev rhs = +let explain_occur_check env sigma ev rhs = + let rhs = nf_evar sigma rhs in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let pt = pr_lconstr_env env rhs in @@ -354,7 +373,8 @@ let explain_hole_kind env evi = function | MatchingVar _ -> assert false -let explain_not_clean env ev t k = +let explain_not_clean env sigma ev t k = + let t = nf_evar sigma t in let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in @@ -401,13 +421,15 @@ let explain_wrong_case_info env ind ci = str "was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc ++ str "." -let explain_cannot_unify env m n = +let explain_cannot_unify env sigma m n = + let m = nf_evar sigma m in + let n = nf_evar sigma n in let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str "with" ++ brk(1,1) ++ pn ++ str "." -let explain_cannot_unify_local env m n subn = +let explain_cannot_unify_local env sigma m n subn = let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in let psubn = pr_lconstr_env env subn in @@ -449,7 +471,7 @@ let explain_non_linear_unification env m t = strbrk " which would require to abstract twice on " ++ pr_lconstr_env env t ++ str "." -let explain_type_error env err = +let explain_type_error env sigma err = let env = make_all_name_different env in match err with | UnboundRel n -> @@ -457,7 +479,7 @@ let explain_type_error env err = | UnboundVar v -> explain_unbound_var env v | NotAType j -> - explain_not_type env j + explain_not_type env sigma j | BadAssumption c -> explain_bad_assumption env c | ReferenceVariables id -> @@ -465,38 +487,39 @@ let explain_type_error env err = | ElimArity (ind, aritylst, c, pj, okinds) -> explain_elim_arity env ind aritylst c pj okinds | CaseNotInductive cj -> - explain_case_not_inductive env cj + explain_case_not_inductive env sigma cj | NumberBranches (cj, n) -> - explain_number_branches env cj n + explain_number_branches env sigma cj n | IllFormedBranch (c, i, actty, expty) -> - explain_ill_formed_branch env c i actty expty + explain_ill_formed_branch env sigma c i actty expty | Generalization (nvar, c) -> explain_generalization env nvar c | ActualType (j, pt) -> - explain_actual_type env j pt + explain_actual_type env sigma j pt | CantApplyBadType (t, rator, randl) -> - explain_cant_apply_bad_type env t rator randl + explain_cant_apply_bad_type env sigma t rator randl | CantApplyNonFunctional (rator, randl) -> - explain_cant_apply_not_functional env rator randl + explain_cant_apply_not_functional env sigma rator randl | IllFormedRecBody (err, lna, i, fixenv, vdefj) -> explain_ill_formed_rec_body env err lna i fixenv vdefj | IllTypedRecBody (i, lna, vdefj, vargs) -> - explain_ill_typed_rec_body env i lna vdefj vargs + explain_ill_typed_rec_body env sigma i lna vdefj vargs | WrongCaseInfo (ind,ci) -> explain_wrong_case_info env ind ci -let explain_pretype_error env err = +let explain_pretype_error env sigma err = + let env = env_nf_betaiotaevar sigma env in let env = make_all_name_different env in match err with - | CantFindCaseType c -> explain_cant_find_case_type env c - | OccurCheck (n,c) -> explain_occur_check env n c - | NotClean (n,c,k) -> explain_not_clean env n c k + | CantFindCaseType c -> explain_cant_find_case_type env sigma c + | OccurCheck (n,c) -> explain_occur_check env sigma n c + | NotClean (n,c,k) -> explain_not_clean env sigma n c k | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp | VarNotFound id -> explain_var_not_found env id - | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect - | NotProduct c -> explain_not_product env c - | CannotUnify (m,n) -> explain_cannot_unify env m n - | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn + | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect + | NotProduct c -> explain_not_product env sigma c + | CannotUnify (m,n) -> explain_cannot_unify env sigma m n + | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n @@ -504,6 +527,155 @@ let explain_pretype_error env err = explain_cannot_find_well_typed_abstraction env p l | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n | NonLinearUnification (m,c) -> explain_non_linear_unification env m c + | TypingError t -> explain_type_error env sigma t + +(* Module errors *) + +open Modops + +let explain_not_match_error = function + | InductiveFieldExpected _ -> + strbrk "an inductive definition is expected" + | DefinitionFieldExpected -> + strbrk "a definition is expected" + | ModuleFieldExpected -> + strbrk "a module is expected" + | ModuleTypeFieldExpected -> + strbrk "a module type is expected" + | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> + str "types given to " ++ str (string_of_id id) ++ str " differ" + | NotConvertibleBodyField -> + str "the body of definitions differs" + | NotConvertibleTypeField -> + str "types differ" + | NotSameConstructorNamesField -> + str "constructor names differ" + | NotSameInductiveNameInBlockField -> + str "inductive types names differ" + | FiniteInductiveFieldExpected isfinite -> + str "type is expected to be " ++ + str (if isfinite then "coinductive" else "inductive") + | InductiveNumbersFieldExpected n -> + str "number of inductive types differs" + | InductiveParamsNumberField n -> + str "inductive type has not the right number of parameters" + | RecordFieldExpected isrecord -> + str "type is expected " ++ str (if isrecord then "" else "not ") ++ + str "to be a record" + | RecordProjectionsExpected nal -> + (if List.length nal >= 2 then str "expected projection names are " + else str "expected projection name is ") ++ + pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal + | NotEqualInductiveAliases -> + str "Aliases to inductive types do not match" + | NoTypeConstraintExpected -> + strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained" + +let explain_signature_mismatch l spec why = + str "Signature components for label " ++ str (string_of_label l) ++ + str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." + +let explain_label_already_declared l = + str ("The label "^string_of_label l^" is already declared.") + +let explain_application_to_not_path _ = + str "Application of modules is restricted to paths." + +let explain_not_a_functor mtb = + str "Application of not a functor." + +let explain_incompatible_module_types mexpr1 mexpr2 = + str "Incompatible module types." + +let explain_not_equal_module_paths mp1 mp2 = + str "Non equal modules." + +let explain_no_such_label l = + str "No such label " ++ str (string_of_label l) ++ str "." + +let explain_incompatible_labels l l' = + str "Opening and closing labels are not the same: " ++ + str (string_of_label l) ++ str " <> " ++ str (string_of_label l') ++ str "!" + +let explain_signature_expected mtb = + str "Signature expected." + +let explain_no_module_to_end () = + str "No open module to end." + +let explain_no_module_type_to_end () = + str "No open module type to end." + +let explain_not_a_module s = + quote (str s) ++ str " is not a module." + +let explain_not_a_module_type s = + quote (str s) ++ str " is not a module type." + +let explain_not_a_constant l = + quote (pr_label l) ++ str " is not a constant." + +let explain_incorrect_label_constraint l = + str "Incorrect constraint for label " ++ + quote (pr_label l) ++ str "." + +let explain_generative_module_expected l = + str "The module " ++ str (string_of_label l) ++ + strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct." + +let explain_non_empty_local_context = function + | None -> str "The local context is not empty." + | Some l -> + str "The local context of the component " ++ + str (string_of_label l) ++ str " is not empty." + +let explain_label_missing l s = + str "The field " ++ str (string_of_label l) ++ str " is missing in " + ++ str s ++ str "." + +let explain_module_error = function + | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err + | LabelAlreadyDeclared l -> explain_label_already_declared l + | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr + | NotAFunctor mtb -> explain_not_a_functor mtb + | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2 + | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2 + | NoSuchLabel l -> explain_no_such_label l + | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2 + | SignatureExpected mtb -> explain_signature_expected mtb + | NoModuleToEnd -> explain_no_module_to_end () + | NoModuleTypeToEnd -> explain_no_module_type_to_end () + | NotAModule s -> explain_not_a_module s + | NotAModuleType s -> explain_not_a_module_type s + | NotAConstant l -> explain_not_a_constant l + | IncorrectWithConstraint l -> explain_incorrect_label_constraint l + | GenerativeModuleExpected l -> explain_generative_module_expected l + | NonEmptyLocalContect lopt -> explain_non_empty_local_context lopt + | LabelMissing (l,s) -> explain_label_missing l s + +(* Module internalization errors *) + +(* +let explain_declaration_not_path _ = + str "Declaration is not a path." + +*) + +let explain_not_module_nor_modtype s = + quote (str s) ++ str " is not a module or module type." + +let explain_incorrect_with_in_module () = + str "The syntax \"with\" is not allowed for modules." + +let explain_incorrect_module_application () = + str "Illegal application to a module type." + +open Modintern + +let explain_module_internalization_error = function + | NotAModuleNorModtype s -> explain_not_module_nor_modtype s + | IncorrectWithInModule -> explain_incorrect_with_in_module () + | IncorrectModuleApplication -> explain_incorrect_module_application () (* Typeclass errors *) @@ -525,6 +697,7 @@ let explain_no_instance env (_,id) l = prlist_with_sep pr_spc (pr_lconstr_env env) l let pr_constraints printenv env evm = + let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in let l = Evd.to_list evm in let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> @@ -534,12 +707,14 @@ let pr_constraints printenv env evm = (reset_with_named_context evi.evar_hyps env) in (if printenv then pe ++ fnl () else mt ()) ++ prlist_with_sep (fun () -> fnl ()) - (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l + (fun (ev, evi) -> str(string_of_existential ev) ++ + str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++ + pr_evar_map_constraints evm else - pr_evar_map evm + pr_evar_map None evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evarutil.nf_evars evd in + let evm = Evarutil.nf_evar_map evd in let undef = Evd.undefined_evars evm in match constr with | None -> @@ -684,7 +859,7 @@ let error_not_allowed_case_analysis isrec kind i = let error_not_mutual_in_scheme ind ind' = if ind = ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ - str "occurs twice." + str " occurs twice." else str "The inductive types " ++ pr_inductive (Global.env()) ind ++ spc () ++ str "and" ++ spc () ++ pr_inductive (Global.env()) ind' ++ spc () ++ @@ -805,7 +980,7 @@ let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,c,(env',e)) -> str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ spc () ++ str "is not well typed." ++ fnl () ++ - explain_type_error env' e + explain_type_error env' Evd.empty e let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = @@ -831,7 +1006,7 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = let filter = function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in let unboundvars = list_map_filter filter unboundvars in - quote (pr_rawconstr_env (Global.env()) c) ++ + quote (pr_glob_constr_env (Global.env()) c) ++ (if unboundvars <> [] or vars <> [] then strbrk " (with " ++ prlist_with_sep pr_comma |