diff options
| -rw-r--r-- | interp/modintern.ml | 60 | ||||
| -rw-r--r-- | interp/modintern.mli | 11 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 12 | ||||
| -rw-r--r-- | kernel/modops.ml | 160 | ||||
| -rw-r--r-- | kernel/modops.mli | 49 | ||||
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 8 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 150 |
10 files changed, 316 insertions, 140 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index 5866073ccd..c127590923 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -14,6 +14,54 @@ open Libnames open Topconstr open Constrintern +type module_internalization_error = + | NotAModuleNorModtype of string + | IncorrectWithInModule + | IncorrectModuleApplication + +exception ModuleInternalizationError of module_internalization_error + +(* +val error_declaration_not_path : module_struct_entry -> 'a + +val error_not_a_functor : module_struct_entry -> 'a + +val error_not_equal : module_path -> module_path -> 'a + +val error_result_must_be_signature : unit -> 'a + +oval error_not_a_modtype_loc : loc -> string -> 'a + +val error_not_a_module_loc : loc -> string -> 'a + +val error_not_a_module_or_modtype_loc : loc -> string -> 'a + +val error_with_in_module : unit -> 'a + +val error_application_to_module_type : unit -> 'a +*) + +let error_result_must_be_signature () = + error "The result module type must be a signature." + +let error_not_a_modtype_loc loc s = + Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) + +let error_not_a_module_loc loc s = + Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s)) + +let error_not_a_module_nor_modtype_loc loc s = + Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s)) + +let error_incorrect_with_in_module () = + raise (ModuleInternalizationError IncorrectWithInModule) + +let error_application_to_module_type () = + raise (ModuleInternalizationError IncorrectModuleApplication) + + + + let rec make_mp mp = function [] -> mp | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl @@ -68,7 +116,7 @@ let lookup_module (loc,qid) = let mp = Nametab.locate_module qid in Dumpglob.dump_modref loc mp "modtype"; mp with - | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) + | Not_found -> error_not_a_module_loc loc (string_of_qualid qid) let lookup_modtype (loc,qid) = try @@ -76,7 +124,7 @@ let lookup_modtype (loc,qid) = Dumpglob.dump_modref loc mp "mod"; mp with | Not_found -> - Modops.error_not_a_modtype_loc loc (string_of_qualid qid) + error_not_a_modtype_loc loc (string_of_qualid qid) let lookup_module_or_modtype (loc,qid) = try @@ -86,7 +134,7 @@ let lookup_module_or_modtype (loc,qid) = let mp = Nametab.locate_modtype qid in Dumpglob.dump_modref loc mp "mod"; (mp,false) with Not_found -> - Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid) + error_not_a_module_nor_modtype_loc loc (string_of_qualid qid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> @@ -101,7 +149,7 @@ let rec interp_modexpr env = function let me1 = interp_modexpr env me1 in let me2 = interp_modexpr env me2 in MSEapply(me1,me2) - | CMwith _ -> Modops.error_with_in_module () + | CMwith _ -> error_incorrect_with_in_module () let rec interp_modtype env = function @@ -123,10 +171,10 @@ let rec interp_modexpr_or_modtype env = function | CMapply (me1,me2) -> let me1,ismod1 = interp_modexpr_or_modtype env me1 in let me2,ismod2 = interp_modexpr_or_modtype env me2 in - if not ismod2 then Modops.error_application_to_module_type (); + if not ismod2 then error_application_to_module_type (); (MSEapply (me1,me2), ismod1) | CMwith (me,decl) -> let me,ismod = interp_modexpr_or_modtype env me in let decl = transl_with_decl env decl in - if ismod then Modops.error_with_in_module (); + if ismod then error_incorrect_with_in_module (); (MSEwith(me,decl), ismod) diff --git a/interp/modintern.mli b/interp/modintern.mli index a294806635..71a00c2fef 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -14,8 +14,17 @@ open Libnames open Names open Topconstr +(** Module internalization errors *) + +type module_internalization_error = + | NotAModuleNorModtype of string + | IncorrectWithInModule + | IncorrectModuleApplication + +exception ModuleInternalizationError of module_internalization_error + (** Module expressions and module types are interpreted relatively to - eventual functor or funsig arguments. *) + possible functor or functor signature arguments. *) val interp_modtype : env -> module_ast -> module_struct_entry diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index bbcabd72a2..335c2a94ee 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -132,12 +132,12 @@ and check_with_aux_def env sign with_decl mp equiv = mod_type_alg = None}) in SEBstruct(before@((l,new_spec)::after)),cb,cst | Some msb -> - error_a_generative_module_expected l + error_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l + | Reduction.NotConvertible -> error_incorrect_with_constraint l and check_with_aux_mod env sign with_decl mp equiv = let sig_b = match sign with @@ -175,12 +175,12 @@ and check_with_aux_mod env sign with_decl mp equiv = (check_subtypes env' mtb_mp1 (module_type_of_module env' None old)) old.mod_constraints - with Failure _ -> error_with_incorrect (label_of_id id) + with Failure _ -> error_incorrect_with_constraint (label_of_id id) end | Some (SEBident(mp')) -> check_modpath_equiv env' mp1 mp'; old.mod_constraints - | _ -> error_a_generative_module_expected l + | _ -> error_generative_module_expected l in let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) env false in @@ -220,12 +220,12 @@ and check_with_aux_mod env sign with_decl mp equiv = SEBstruct(before@(l,spec)::after) ,equiv,empty_constraint | _ -> - error_a_generative_module_expected l + error_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l + | Reduction.NotConvertible -> error_incorrect_with_constraint l and translate_module env mp inl me = match me.mod_entry_expr, me.mod_entry_type with diff --git a/kernel/modops.ml b/kernel/modops.ml index 302d251949..6d4ebb989b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -25,19 +25,6 @@ open Environ open Entries open Mod_subst -let error_existing_label l = - error ("The label "^string_of_label l^" is already declared.") - -let error_declaration_not_path _ = error "Declaration is not a path." - -let error_application_to_not_path _ = error "Application to not path." - -let error_not_a_functor _ = error "Application of not a functor." - -let error_incompatible_modtypes _ _ = error "Incompatible module types." - -let error_not_equal _ _ = error "Non equal modules." - type signature_mismatch_error = | InductiveFieldExpected of mutual_inductive_body | DefinitionFieldExpected @@ -57,104 +44,83 @@ type signature_mismatch_error = | NotEqualInductiveAliases | NoTypeConstraintExpected -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 error_not_match l _ why = - errorlabstrm "" - (str "Signature components for label " ++ str (string_of_label l) ++ - str " do not match:" ++ spc () ++ explain_not_match_error why ++ str ".") - -let error_no_such_label l = error ("No such label "^string_of_label l^".") - -let error_incompatible_labels l l' = - error ("Opening and closing labels are not the same: " - ^string_of_label l^" <> "^string_of_label l'^" !") - -let error_result_must_be_signature () = - error "The result module type must be a signature." +type module_typing_error = + | SignatureMismatch of label * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of label + | ApplicationToNotPath of module_struct_entry + | NotAFunctor of struct_expr_body + | IncompatibleModuleTypes of module_type_body * module_type_body + | NotEqualModulePaths of module_path * module_path + | NoSuchLabel of label + | IncompatibleLabels of label * label + | SignatureExpected of struct_expr_body + | NoModuleToEnd + | NoModuleTypeToEnd + | NotAModule of string + | NotAModuleType of string + | NotAConstant of label + | IncorrectWithConstraint of label + | GenerativeModuleExpected of label + | NonEmptyLocalContect of label option + | LabelMissing of label * string -let error_signature_expected mtb = - error "Signature expected." +exception ModuleTypingError of module_typing_error -let error_no_module_to_end _ = - error "No open module to end." +let error_existing_label l = + raise (ModuleTypingError (LabelAlreadyDeclared l)) -let error_no_modtype_to_end _ = - error "No open module type to end." +let error_application_to_not_path mexpr = + raise (ModuleTypingError (ApplicationToNotPath mexpr)) -let error_not_a_modtype_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module type.")) +let error_not_a_functor mtb = + raise (ModuleTypingError (NotAFunctor mtb)) -let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) +let error_incompatible_modtypes mexpr1 mexpr2 = + raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2))) -let error_not_a_module_or_modtype_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type.")) +let error_not_equal_modpaths mp1 mp2 = + raise (ModuleTypingError (NotEqualModulePaths (mp1,mp2))) -let error_not_a_module s = error_not_a_module_loc dummy_loc s +let error_signature_mismatch l spec why = + raise (ModuleTypingError (SignatureMismatch (l,spec,why))) -let error_not_a_constant l = - error ("\""^(string_of_label l)^"\" is not a constant.") +let error_no_such_label l = + raise (ModuleTypingError (NoSuchLabel l)) -let error_with_incorrect l = - error ("Incorrect constraint for label \""^(string_of_label l)^"\".") +let error_incompatible_labels l l' = + raise (ModuleTypingError (IncompatibleLabels (l,l'))) -let error_a_generative_module_expected l = - error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ - "components of generative modules can be changed using the \"with\" " ^ - "construct.") +let error_signature_expected mtb = + raise (ModuleTypingError (SignatureExpected mtb)) -let error_local_context lo = - match lo with - None -> - error ("The local context is not empty.") - | (Some l) -> - error ("The local context of the component "^ - (string_of_label l)^" is not empty.") +let error_no_module_to_end _ = + raise (ModuleTypingError NoModuleToEnd) +let error_no_modtype_to_end _ = + raise (ModuleTypingError NoModuleTypeToEnd) -let error_no_such_label_sub l l1 = - error ("The field "^(string_of_label l)^" is missing in "^l1^".") +let error_not_a_modtype s = + raise (ModuleTypingError (NotAModuleType s)) + +let error_not_a_module s = + raise (ModuleTypingError (NotAModule s)) + +let error_not_a_constant l = + raise (ModuleTypingError (NotAConstant l)) -let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules." +let error_incorrect_with_constraint l = + raise (ModuleTypingError (IncorrectWithConstraint l)) + +let error_generative_module_expected l = + raise (ModuleTypingError (GenerativeModuleExpected l)) + +let error_non_empty_local_context lo = + raise (ModuleTypingError (NonEmptyLocalContect lo)) + +let error_no_such_label_sub l l1 = + raise (ModuleTypingError (LabelMissing (l,l1))) -let error_application_to_module_type _ = error "Module application to a module type." +(************************) let destr_functor env mtb = match mtb with @@ -181,7 +147,7 @@ let check_modpath_equiv env mp1 mp2 = let mb2=lookup_module mp2 env in if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2) then () - else error_not_equal mp1 mp2 + else error_not_equal_modpaths mp1 mp2 let rec subst_with_body sub = function | With_module_body(id,mp) -> diff --git a/kernel/modops.mli b/kernel/modops.mli index cf8d62043f..35be04665b 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -72,53 +72,56 @@ type signature_mismatch_error = | NotEqualInductiveAliases | NoTypeConstraintExpected -val error_existing_label : label -> 'a +type module_typing_error = + | SignatureMismatch of label * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of label + | ApplicationToNotPath of module_struct_entry + | NotAFunctor of struct_expr_body + | IncompatibleModuleTypes of module_type_body * module_type_body + | NotEqualModulePaths of module_path * module_path + | NoSuchLabel of label + | IncompatibleLabels of label * label + | SignatureExpected of struct_expr_body + | NoModuleToEnd + | NoModuleTypeToEnd + | NotAModule of string + | NotAModuleType of string + | NotAConstant of label + | IncorrectWithConstraint of label + | GenerativeModuleExpected of label + | NonEmptyLocalContect of label option + | LabelMissing of label * string + +exception ModuleTypingError of module_typing_error -val error_declaration_not_path : module_struct_entry -> 'a +val error_existing_label : label -> 'a val error_application_to_not_path : module_struct_entry -> 'a -val error_not_a_functor : module_struct_entry -> 'a - val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a -val error_not_equal : module_path -> module_path -> 'a - -val error_not_match : +val error_signature_mismatch : label -> structure_field_body -> signature_mismatch_error -> 'a val error_incompatible_labels : label -> label -> 'a val error_no_such_label : label -> 'a -val error_result_must_be_signature : unit -> 'a - val error_signature_expected : struct_expr_body -> 'a val error_no_module_to_end : unit -> 'a val error_no_modtype_to_end : unit -> 'a -val error_not_a_modtype_loc : loc -> string -> 'a - -val error_not_a_module_loc : loc -> string -> 'a - -val error_not_a_module_or_modtype_loc : loc -> string -> 'a - val error_not_a_module : string -> 'a val error_not_a_constant : label -> 'a -val error_with_incorrect : label -> 'a +val error_incorrect_with_constraint : label -> 'a -val error_a_generative_module_expected : label -> 'a +val error_generative_module_expected : label -> 'a -val error_local_context : label option -> 'a +val error_non_empty_local_context : label option -> 'a val error_no_such_label_sub : label->string->'a - -val error_with_in_module : unit -> 'a - -val error_application_to_module_type : unit -> 'a - diff --git a/kernel/names.ml b/kernel/names.ml index 6e39b35bb3..4466f558f9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -107,6 +107,7 @@ let label_of_mbid (_,s,_) = s let mk_label l = l let string_of_label = string_of_id +let pr_label l = str (string_of_label l) let id_of_label l = l let label_of_id id = id diff --git a/kernel/names.mli b/kernel/names.mli index 2d112b32ac..acc764028f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -47,6 +47,7 @@ type label val mk_label : string -> label val string_of_label : label -> string +val pr_label : label -> Pp.std_ppcmds val label_of_id : identifier -> label val id_of_label : label -> identifier diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 66c731a9de..8f4ec76f84 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -367,7 +367,7 @@ let end_module l restype senv = | STRUCT params -> params, (List.length params > 0) in if l <> modinfo.label then error_incompatible_labels l modinfo.label; - if not (empty_context senv.env) then error_local_context None; + if not (empty_context senv.env) then error_non_empty_local_context None; let functorize_struct tb = List.fold_left (fun mtb (arg_id,arg_b) -> @@ -574,7 +574,7 @@ let end_modtype l senv = | SIG params -> params in if l <> modinfo.label then error_incompatible_labels l modinfo.label; - if not (empty_context senv.env) then error_local_context None; + if not (empty_context senv.env) then error_non_empty_local_context None; let auto_tb = SEBstruct (List.rev senv.revstruct) in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8085575217..0c72995080 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -78,7 +78,7 @@ let check_conv_error error why cst f env a1 a2 = let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= let kn1 = make_mind mp1 empty_dirpath l in let kn2 = make_mind mp2 empty_dirpath l in - let error why = error_not_match l spec2 why in + let error why = error_signature_mismatch l spec2 why in let check_conv why cst f = check_conv_error error why cst f in let mib1 = match info1 with @@ -201,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = - let error why = error_not_match l spec2 why in + let error why = error_signature_mismatch l spec2 why in let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = @@ -353,13 +353,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= match info1 with | Module msb -> check_modules cst env msb msb2 subst1 subst2 - | _ -> error_not_match l spec2 ModuleFieldExpected + | _ -> error_signature_mismatch l spec2 ModuleFieldExpected end | SFBmodtype mtb2 -> let mtb1 = match info1 with | Modtype mtb -> mtb - | _ -> error_not_match l spec2 ModuleTypeFieldExpected + | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected in let env = add_module (module_body_of_type mtb2.typ_mp mtb2) (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 9443217f1b..6af1f9d56c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -155,7 +155,7 @@ let explain_generalization env (name,var) j = let explain_actual_type env sigma j pt = let j = j_nf_betaiotaevar sigma j in - let pt = nf_betaiota sigma pt 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 @@ -528,6 +528,154 @@ let explain_pretype_error env sigma err = | 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 to not path." + +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 env sigma = 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 "Module 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 *) let explain_not_a_class env c = |