diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 124 |
1 files changed, 77 insertions, 47 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index 1519df4d..6fbcd81d 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,47 +1,66 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names -open Univ open Term open Environ open Declarations open Entries open Mod_subst -(** Various operations on modules and module types *) +(** {6 Various operations on modules and module types } *) +(** Functors *) -val module_body_of_type : module_path -> module_type_body -> module_body +val is_functor : ('ty,'a) functorize -> bool -val module_type_of_module : module_path option -> module_body -> - module_type_body +val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize + +val destr_nofunctor : ('ty,'a) functorize -> 'a + +(** Conversions between [module_body] and [module_type_body] *) -val destr_functor : - env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body +val module_type_of_module : module_body -> module_type_body +val module_body_of_type : module_path -> module_type_body -> module_body + +val check_modpath_equiv : env -> module_path -> module_path -> unit -val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body +val implem_smartmap : + (module_signature -> module_signature) -> + (module_expression -> module_expression) -> + (module_implementation -> module_implementation) -val subst_signature : substitution -> structure_body -> structure_body +(** {6 Substitutions } *) -val add_signature : +val subst_signature : substitution -> module_signature -> module_signature +val subst_structure : substitution -> structure_body -> structure_body + +(** {6 Adding to an environment } *) + +val add_structure : module_path -> structure_body -> delta_resolver -> env -> env (** adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env -val check_modpath_equiv : env -> module_path -> module_path -> unit +(** same as add_module, but for a module whose native code has been linked by +the native compiler. The linking information is updated. *) +val add_linked_module : module_body -> Pre_env.link_info -> env -> env + +(** same, for a module type *) +val add_module_type : module_path -> module_type_body -> env -> env + +(** {6 Strengthening } *) val strengthen : module_type_body -> module_path -> module_type_body val inline_delta_resolver : - env -> inline -> module_path -> mod_bound_id -> module_type_body -> + env -> inline -> module_path -> MBId.t -> module_type_body -> delta_resolver -> delta_resolver val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body @@ -49,52 +68,69 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body val subst_modtype_and_resolver : module_type_body -> module_path -> module_type_body -val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body +(** {6 Cleaning a module expression from bounded parts } + + For instance: + functor(X:T)->struct module M:=X end) + becomes: + functor(X:T)->struct module M:=<content of T> end) +*) + +val clean_bounded_mod_expr : module_signature -> module_signature + +(** {6 Stm machinery } *) -(** Errors *) +val join_structure : + Future.UUIDSet.t -> Opaqueproof.opaquetab -> structure_body -> unit + +(** {6 Errors } *) type signature_mismatch_error = | InductiveFieldExpected of mutual_inductive_body | DefinitionFieldExpected | ModuleFieldExpected | ModuleTypeFieldExpected - | NotConvertibleInductiveField of identifier - | NotConvertibleConstructorField of identifier + | NotConvertibleInductiveField of Id.t + | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool | InductiveNumbersFieldExpected of int | InductiveParamsNumberField of int | RecordFieldExpected of bool - | RecordProjectionsExpected of name list + | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases | NoTypeConstraintExpected + | IncompatibleInstances + | IncompatibleUniverses of Univ.univ_inconsistency + | IncompatiblePolymorphism of env * types * types + | IncompatibleConstraints of Univ.constraints type module_typing_error = - | SignatureMismatch of label * structure_field_body * signature_mismatch_error - | LabelAlreadyDeclared of label + | SignatureMismatch of + Label.t * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry - | NotAFunctor of struct_expr_body + | NotAFunctor + | IsAFunctor | 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 + | NoSuchLabel of Label.t + | IncompatibleLabels of Label.t * Label.t | NotAModule of string | NotAModuleType of string - | NotAConstant of label - | IncorrectWithConstraint of label - | GenerativeModuleExpected of label - | NonEmptyLocalContect of label option - | LabelMissing of label * string + | NotAConstant of Label.t + | IncorrectWithConstraint of Label.t + | GenerativeModuleExpected of Label.t + | LabelMissing of Label.t * string + | HigherOrderInclude exception ModuleTypingError of module_typing_error -val error_existing_label : label -> 'a +val error_existing_label : Label.t -> 'a val error_application_to_not_path : module_struct_entry -> 'a @@ -102,26 +138,20 @@ val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a 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_signature_expected : struct_expr_body -> 'a + Label.t -> structure_field_body -> signature_mismatch_error -> 'a -val error_no_module_to_end : unit -> 'a +val error_incompatible_labels : Label.t -> Label.t -> 'a -val error_no_modtype_to_end : unit -> 'a +val error_no_such_label : Label.t -> 'a val error_not_a_module : string -> 'a -val error_not_a_constant : label -> 'a +val error_not_a_constant : Label.t -> 'a -val error_incorrect_with_constraint : label -> 'a +val error_incorrect_with_constraint : Label.t -> 'a -val error_generative_module_expected : label -> 'a +val error_generative_module_expected : Label.t -> 'a -val error_non_empty_local_context : label option -> 'a +val error_no_such_label_sub : Label.t->string->'a -val error_no_such_label_sub : label->string->'a +val error_higher_order_include : unit -> 'a |