diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/mod_typing.mli | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 53 |
1 files changed, 24 insertions, 29 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index e868aec2..b39e8212 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* 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 *) @@ -12,40 +12,35 @@ open Entries open Mod_subst open Names +(** Main functions for translating module entries *) val translate_module : env -> module_path -> inline -> module_entry -> module_body -val translate_module_type : - env -> module_path -> inline -> module_struct_entry -> module_type_body +val translate_modtype : + env -> module_path -> inline -> module_type_entry -> module_type_body -val translate_struct_module_entry : - env -> module_path -> inline -> module_struct_entry -> - struct_expr_body (* Signature *) - * struct_expr_body option (* Algebraic expr, in fact never None *) - * delta_resolver - * Univ.constraints - -val translate_struct_type_entry : - env -> inline -> module_struct_entry -> - struct_expr_body - * struct_expr_body option - * delta_resolver - * Univ.constraints - -val translate_struct_include_module_entry : - env -> module_path -> inline -> module_struct_entry -> - struct_expr_body - * struct_expr_body option (* Algebraic expr, always None *) - * delta_resolver - * Univ.constraints +(** Low-level function for translating a module struct entry : + - We translate to a module when a [module_path] is given, + otherwise to a module type. + - The first output is the expanded signature + - The second output is the algebraic expression, kept for the extraction. + It is never None when translating to a module, but for module type + it could not be contain applications or functors. +*) -val add_modtype_constraints : env -> module_type_body -> env +type 'alg translation = + module_signature * 'alg option * delta_resolver * Univ.constraints -val add_module_constraints : env -> module_body -> env +val translate_mse : + env -> module_path option -> inline -> module_struct_entry -> + module_alg_expr translation -val add_struct_expr_constraints : env -> struct_expr_body -> env - -val struct_expr_constraints : struct_expr_body -> Univ.constraints +val translate_mse_incl : + env -> module_path -> inline -> module_struct_entry -> + module_alg_expr translation -val module_constraints : module_body -> Univ.constraints +val finalize_module : + env -> module_path -> module_expression translation -> + (module_type_entry * inline) option -> + module_body |