diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-20 08:22:51 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-20 08:22:51 +0000 |
| commit | ec2948e7848265dbf547d97f0866ebd8f5cb6c97 (patch) | |
| tree | 15c8ca8918a8a633c7664d564b14efb8f987385a /kernel/modops.mli | |
| parent | 5275368649a254835a5277dfa185506713506618 (diff) | |
Declareops + Modops : more clever substitutions
We try harder to preserve pointer equality when substituting.
This will probably have little effect (for instance the
constr_substituted are anyway _never_ substituted in place),
but it cannot harm.
Two particular cases:
- we try to share (and maintain shared) mind_user_lc and mind_nf_lc
- we try to share (and maintain shared) mod_expr and mod_type
TODO: check that native compiler is still ok, since we might have
less (ref NotLinked) now. Having references in constant_body and co
is anyway a Very Bad Idea (TM).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index ea92c45ea..e148f9628 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -14,28 +14,33 @@ open Declarations open Entries open Mod_subst -(** Various operations on modules and module types *) +(** {6 Various operations on modules and module types } *) +val module_body_of_type : module_path -> module_type_body -> module_body -val module_body_of_type : module_path -> module_type_body -> module_body - -val module_type_of_module : module_path option -> module_body -> - module_type_body +val module_type_of_module : + module_path option -> module_body -> module_type_body val destr_functor : struct_expr_body -> MBId.t * module_type_body * struct_expr_body +val check_modpath_equiv : env -> module_path -> module_path -> unit + +(** {6 Substitutions } *) + val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body val subst_signature : substitution -> structure_body -> structure_body +(** {6 Adding to an environment } *) + val add_signature : 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 +(** {6 Strengthening } *) val strengthen : module_type_body -> module_path -> module_type_body @@ -48,15 +53,19 @@ 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 } *) + val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body +(** {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 prune_structure_body : structure_body -> structure_body -(** Errors *) +(** {6 Errors } *) type signature_mismatch_error = | InductiveFieldExpected of mutual_inductive_body @@ -78,7 +87,8 @@ type signature_mismatch_error = | NoTypeConstraintExpected type module_typing_error = - | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error + | SignatureMismatch of + Label.t * structure_field_body * signature_mismatch_error | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry | NotAFunctor of struct_expr_body |