aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/modops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/modops.mli')
-rw-r--r--kernel/modops.mli54
1 files changed, 35 insertions, 19 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e148f9628..6aed95988 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -16,30 +16,43 @@ open Mod_subst
(** {6 Various operations on modules and module types } *)
-val module_body_of_type : module_path -> module_type_body -> module_body
+(** Functors *)
-val module_type_of_module :
- module_path option -> module_body -> module_type_body
+val is_functor : ('ty,'a) functorize -> bool
-val destr_functor :
- struct_expr_body -> MBId.t * module_type_body * struct_expr_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 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
-(** {6 Substitutions } *)
+val implem_smartmap :
+ (module_signature -> module_signature) ->
+ (module_expression -> module_expression) ->
+ (module_implementation -> module_implementation)
-val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body
+(** {6 Substitutions } *)
-val subst_signature : substitution -> structure_body -> structure_body
+val subst_signature : substitution -> module_signature -> module_signature
+val subst_structure : substitution -> structure_body -> structure_body
(** {6 Adding to an environment } *)
-val add_signature :
+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
+
+(** 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
@@ -53,17 +66,22 @@ 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
-(** {6 Cleaning a bound module expression } *)
+(** {6 Cleaning a module expression from bounded parts }
-val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
+ 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 : join and prune } *)
-val join_module_body : module_body -> unit
-val join_structure_body : structure_body -> unit
-val join_struct_expr_body : struct_expr_body -> unit
+val join_module : module_body -> unit
+val join_structure : structure_body -> unit
-val prune_structure_body : structure_body -> structure_body
+val prune_structure : structure_body -> structure_body
(** {6 Errors } *)
@@ -91,12 +109,12 @@ type module_typing_error =
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.t
| IncompatibleLabels of Label.t * Label.t
- | SignatureExpected of struct_expr_body
| NotAModule of string
| NotAModuleType of string
| NotAConstant of Label.t
@@ -121,8 +139,6 @@ val error_incompatible_labels : Label.t -> Label.t -> 'a
val error_no_such_label : Label.t -> 'a
-val error_signature_expected : struct_expr_body -> 'a
-
val error_not_a_module : string -> 'a
val error_not_a_constant : Label.t -> 'a