aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorletouzey2013-08-20 08:22:55 +0000
committerletouzey2013-08-20 08:22:55 +0000
commitc5b699f8feb54b7ada2cb6c6754a1909ebedcd3f (patch)
tree7d8867a46ab2960d323e3307ee1c73ec32c58785 /kernel
parentec2948e7848265dbf547d97f0866ebd8f5cb6c97 (diff)
Declarations.mli: reorganization of modular structures
The earlier type [struct_expr_body] was far too broad, leading to code with unclear invariants, many "assert false", etc etc. Its replacement [module_alg_expr] has only three constructors: * MEident * MEapply : note the module_path as 2nd arg, no more constraints here * MEwith : no more constant_body inside, constr is just fine But no more SEBfunctor or SEBstruct constructor here (see below). This way, this datatype corresponds to algebraic expressions, i.e. anything that can appear in non-interactive modules. In fact, it even coincides now with [Entries.module_struct_entry]. - Functor constructors are now necessarily on top of other structures thanks to a generic [functorize] datatype. - Structures are now separated from algebraic expressions by design : the [mod_type] and [typ_expr] fields now only contain structures (or functorized structures), while [mod_type_alg] and [typ_expr_alg] are restricted to algebraic expressions only. - Only the implementation field [mod_expr] could be either algebraic or structural. We handle this via a specialized datatype [module_implementation] with four constructors: * Abstract : no implementation (cf. for instance Declare Module) * Algebraic(_) : for non-interactive modules, e.g. Module M := N. * Struct(_) : for interactive module, e.g. Module M : T. ... End M. * FullStruct : for interactive module with no type restriction. The [FullStruct] is a particular case of [Struct] where the implementation need not be stored at all, since it is exactly equal to its expanded type present in [mod_type]. This is less fragile than hoping as earlier that pointer equality between [mod_type] and [mod_expr] will be preserved... - We clearly emphasize that only [mod_type] and [typ_expr] are relevant for the kernel, while [mod_type_alg] and [typ_expr_alg] are there only for a nicer extraction and shorter module printing. [mod_expr] is also not accessed by the kernel, but it is important for Print Assumptions later. - A few implicit invariants remain, for instance "no MEwith in mod_expr", see the final comment in Declarations - Heavy refactoring of module-related files : modops, mod_typing, safe_typing, declaremods, extraction/extract_env.ml ... - Coqchk has been adapted accordingly. The code concerning MEwith in Mod_checking is now gone, since we cannot have any in mod_expr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.mli105
-rw-r--r--kernel/entries.mli24
-rw-r--r--kernel/mod_typing.ml468
-rw-r--r--kernel/mod_typing.mli56
-rw-r--r--kernel/modops.ml712
-rw-r--r--kernel/modops.mli54
-rw-r--r--kernel/names.ml1
-rw-r--r--kernel/names.mli1
-rw-r--r--kernel/nativelibrary.ml20
-rw-r--r--kernel/nativelibrary.mli2
-rw-r--r--kernel/safe_typing.ml118
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/subtyping.ml114
13 files changed, 773 insertions, 906 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5cb406ffa2..6a5b0dbb20 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -155,8 +155,30 @@ type mutual_inductive_body = {
}
-(** {6 Modules: signature component specifications, module types, and
- module declarations } *)
+(** {6 Module declarations } *)
+
+(** Functor expressions are forced to be on top of other expressions *)
+
+type ('ty,'a) functorize =
+ | NoFunctor of 'a
+ | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize
+
+(** The fully-algebraic module expressions : names, applications, 'with ...'.
+ They correspond to the user entries of non-interactive modules.
+ They will be later expanded into module structures in [Mod_typing],
+ and won't play any role into the kernel after that : they are kept
+ only for short module printing and for extraction. *)
+
+type with_declaration =
+ | WithMod of Id.t list * module_path
+ | WithDef of Id.t list * constr
+
+type module_alg_expr =
+ | MEident of module_path
+ | MEapply of module_alg_expr * module_path
+ | MEwith of module_alg_expr * with_declaration
+
+(** A component of a module structure *)
type structure_field_body =
| SFBconst of constant_body
@@ -164,47 +186,58 @@ type structure_field_body =
| SFBmodule of module_body
| SFBmodtype of module_type_body
-(** NB: we may encounter now (at most) twice the same label in
+(** A module structure is a list of labeled components.
+
+ Note : we may encounter now (at most) twice the same label in
a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
and once for an object ([SFBconst] or [SFBmind]) *)
and structure_body = (Label.t * structure_field_body) list
-and struct_expr_body =
- | SEBident of module_path
- | SEBfunctor of MBId.t * module_type_body * struct_expr_body
- | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
- | SEBstruct of structure_body
- | SEBwith of struct_expr_body * with_declaration_body
+(** A module signature is a structure, with possibly functors on top of it *)
+
+and module_signature = (module_type_body,structure_body) functorize
+
+(** A module expression is an algebraic expression, possibly functorized. *)
-and with_declaration_body =
- With_module_body of Id.t list * module_path
- | With_definition_body of Id.t list * constant_body
+and module_expression = (module_type_body,module_alg_expr) functorize
+
+and module_implementation =
+ | Abstract (** no accessible implementation *)
+ | Algebraic of module_expression (** non-interactive algebraic expression *)
+ | Struct of module_signature (** interactive body *)
+ | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
and module_body =
- { (** absolute path of the module *)
- mod_mp : module_path;
- (** Implementation *)
- mod_expr : struct_expr_body option;
- (** Signature *)
- mod_type : struct_expr_body;
- (** algebraic structure expression is kept
- if it's relevant for extraction *)
- mod_type_alg : struct_expr_body option;
- (** set of all constraint in the module *)
- mod_constraints : Univ.constraints;
- (** quotiented set of equivalent constant and inductive name *)
- mod_delta : Mod_subst.delta_resolver;
- mod_retroknowledge : Retroknowledge.action list}
+ { mod_mp : module_path; (** absolute path of the module *)
+ mod_expr : module_implementation; (** implementation *)
+ mod_type : module_signature; (** expanded type *)
+ (** algebraic type, kept if it's relevant for extraction *)
+ mod_type_alg : module_expression option;
+ (** set of all constraints in the module *)
+ mod_constraints : Univ.constraints;
+ (** quotiented set of equivalent constants and inductive names *)
+ mod_delta : Mod_subst.delta_resolver;
+ mod_retroknowledge : Retroknowledge.action list }
+
+(** A [module_type_body] is similar to a [module_body], with
+ no implementation and retroknowledge fields *)
and module_type_body =
- {
- (** Path of the module type *)
- typ_mp : module_path;
- typ_expr : struct_expr_body;
- (** algebraic structure expression is kept
- if it's relevant for extraction *)
- typ_expr_alg : struct_expr_body option ;
- typ_constraints : Univ.constraints;
- (** quotiented set of equivalent constant and inductive name *)
- typ_delta : Mod_subst.delta_resolver}
+ { typ_mp : module_path; (** path of the module type *)
+ typ_expr : module_signature; (** expanded type *)
+ (** algebraic expression, kept if it's relevant for extraction *)
+ typ_expr_alg : module_expression option;
+ typ_constraints : Univ.constraints;
+ (** quotiented set of equivalent constants and inductive names *)
+ typ_delta : Mod_subst.delta_resolver}
+
+(** Extra invariants :
+
+ - No [MEwith] inside a [mod_expr] implementation : the 'with' syntax
+ is only supported for module types
+
+ - A module application is atomic, for instance ((M N) P) :
+ * the head of [MEapply] can only be another [MEapply] or a [MEident]
+ * the argument of [MEapply] is now directly forced to be a [module_path].
+*)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 3b7a2fd19f..b78372c0ea 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -67,16 +67,14 @@ type constant_entry =
(** {6 Modules } *)
-type module_struct_entry =
- MSEident of module_path
- | MSEfunctor of MBId.t * module_struct_entry * module_struct_entry
- | MSEwith of module_struct_entry * with_declaration
- | MSEapply of module_struct_entry * module_struct_entry
-
-and with_declaration =
- With_Module of Id.t list * module_path
- | With_Definition of Id.t list * constr
-
-and module_entry =
- { mod_entry_type : module_struct_entry option;
- mod_entry_expr : module_struct_entry option}
+type module_struct_entry = Declarations.module_alg_expr
+
+type module_params_entry =
+ (MBId.t * module_struct_entry) list (** older first *)
+
+type module_type_entry = module_params_entry * module_struct_entry
+
+type module_entry =
+ | MType of module_params_entry * module_struct_entry
+ | MExpr of
+ module_params_entry * module_struct_entry * module_struct_entry option
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d5555c624e..7794f19be0 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -20,17 +20,13 @@ open Environ
open Modops
open Mod_subst
-exception Not_path
-
-let path_of_mexpr = function
- | MSEident mp -> mp
- | _ -> raise Not_path
+type 'alg translation =
+ module_signature * 'alg option * delta_resolver * Univ.constraints
let rec mp_from_mexpr = function
- | MSEident mp -> mp
- | MSEapply (expr,_) -> mp_from_mexpr expr
- | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
- | MSEwith (expr,_) -> mp_from_mexpr expr
+ | MEident mp -> mp
+ | MEapply (expr,_) -> mp_from_mexpr expr
+ | MEwith (expr,_) -> mp_from_mexpr expr
let is_modular = function
| SFBmodule _ | SFBmodtype _ -> true
@@ -39,7 +35,7 @@ let is_modular = function
(** Split a [structure_body] at some label corresponding to
a modular definition or not. *)
-let split_sign k m struc =
+let split_struc k m struc =
let rec split rev_before = function
| [] -> raise Not_found
| (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) ->
@@ -48,8 +44,8 @@ let split_sign k m struc =
in split [] struc
let discr_resolver mtb = match mtb.typ_expr with
- | SEBstruct _ -> mtb.typ_delta
- | _ -> empty_delta_resolver (* when mp is a functor *)
+ | NoFunctor _ -> mtb.typ_delta
+ | MoreFunctor _ -> empty_delta_resolver
let rec rebuild_mp mp l =
match l with
@@ -58,19 +54,15 @@ let rec rebuild_mp mp l =
let (+++) = Univ.union_constraints
-let rec check_with_def env sign (idl,c) mp equiv =
- let sig_b = match sign with
- | SEBstruct(sig_b) -> sig_b
- | _ -> error_signature_expected sign
- in
+let rec check_with_def env struc (idl,c) mp equiv =
let lab,idl = match idl with
| [] -> assert false
| id::idl -> Label.of_id id, idl
in
try
let modular = not (List.is_empty idl) in
- let before,spec,after = split_sign lab modular sig_b in
- let env' = Modops.add_signature mp before equiv env in
+ let before,spec,after = split_struc lab modular struc in
+ let env' = Modops.add_structure mp before equiv env in
if List.is_empty idl then
(* Toplevel definition *)
let cb = match spec with
@@ -80,27 +72,26 @@ let rec check_with_def env sign (idl,c) mp equiv =
(* In the spirit of subtyping.check_constant, we accept
any implementations of parameters and opaques terms,
as long as they have the right type *)
- let def,cst = match cb.const_body with
+ let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j,cst1 = Typeops.infer env' c in
let typ = Typeops.type_of_constant_type env' cb.const_type in
let cst2 = Reduction.conv_leq env' j.uj_type typ in
let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in
- let def = Def (Lazyconstr.from_val j.uj_val) in
- def,cst
+ j.uj_val,cst
| Def cs ->
let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
let cst = Future.force cb.const_constraints +++ cst1 in
- let def = Def (Lazyconstr.from_val c) in
- def,cst
+ c, cst
in
+ let def = Def (Lazyconstr.from_val c') in
let cb' =
{ cb with
const_body = def;
const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
const_constraints = Future.from_val cst }
in
- SEBstruct(before@(lab,SFBconst(cb'))::after),cb',cst
+ before@(lab,SFBconst(cb'))::after, c', cst
else
(* Definition inside a sub-module *)
let mb = match spec with
@@ -108,33 +99,30 @@ let rec check_with_def env sign (idl,c) mp equiv =
| _ -> error_not_a_module (Label.to_string lab)
in
begin match mb.mod_expr with
- | Some _ -> error_generative_module_expected lab
- | None ->
- let sign,cb,cst =
- check_with_def env' mb.mod_type (idl,c) (MPdot(mp,lab)) mb.mod_delta
+ | Abstract ->
+ let struc = Modops.destr_nofunctor mb.mod_type in
+ let struc',c',cst =
+ check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
in
let mb' = { mb with
- mod_type = sign;
+ mod_type = NoFunctor struc';
mod_type_alg = None }
in
- SEBstruct(before@(lab,SFBmodule mb')::after),cb,cst
+ before@(lab,SFBmodule mb')::after, c', cst
+ | _ -> error_generative_module_expected lab
end
with
| Not_found -> error_no_such_label lab
| Reduction.NotConvertible -> error_incorrect_with_constraint lab
-let rec check_with_mod env sign (idl,mp1) mp equiv =
- let sig_b = match sign with
- | SEBstruct(sig_b) -> sig_b
- | _ -> error_signature_expected sign
- in
+let rec check_with_mod env struc (idl,mp1) mp equiv =
let lab,idl = match idl with
| [] -> assert false
| id::idl -> Label.of_id id, idl
in
try
- let before,spec,after = split_sign lab true sig_b in
- let env' = Modops.add_signature mp before equiv env in
+ let before,spec,after = split_struc lab true struc in
+ let env' = Modops.add_structure mp before equiv env in
let old = match spec with
| SFBmodule mb -> mb
| _ -> error_not_a_module (Label.to_string lab)
@@ -142,33 +130,35 @@ let rec check_with_mod env sign (idl,mp1) mp equiv =
if List.is_empty idl then
(* Toplevel module definition *)
let mb_mp1 = lookup_module mp1 env in
- let mtb_mp1 = module_type_of_module None mb_mp1 in
+ let mtb_mp1 = module_type_of_module mb_mp1 in
let cst = match old.mod_expr with
- | None ->
+ | Abstract ->
begin
try
- let mtb_old = module_type_of_module None old in
+ let mtb_old = module_type_of_module old in
Subtyping.check_subtypes env' mtb_mp1 mtb_old
+++ old.mod_constraints
with Failure _ -> error_incorrect_with_constraint lab
end
- | Some (SEBident(mp')) ->
+ | Algebraic (NoFunctor (MEident(mp'))) ->
check_modpath_equiv env' mp1 mp';
old.mod_constraints
- | _ -> error_generative_module_expected lab
+ | _ -> error_generative_module_expected lab
in
let mp' = MPdot (mp,lab) in
let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
- let new_mb' = {new_mb with
- mod_mp = mp';
- mod_expr = Some (SEBident mp1);
- mod_constraints = cst }
+ let new_mb' =
+ { new_mb with
+ mod_mp = mp';
+ mod_expr = Algebraic (NoFunctor (MEident mp1));
+ mod_constraints = cst }
in
+ let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
(* we propagate the new equality in the rest of the signature
with the identity substitution accompagned by the new resolver*)
let id_subst = map_mp mp' mp' new_mb.mod_delta in
- SEBstruct(before@(lab,SFBmodule new_mb')::subst_signature id_subst after),
- add_delta_resolver equiv new_mb.mod_delta,cst
+ let new_after = subst_structure id_subst after in
+ before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
else
(* Module definition of a sub-module *)
let mp' = MPdot (mp,lab) in
@@ -177,255 +167,163 @@ let rec check_with_mod env sign (idl,mp1) mp equiv =
| _ -> error_not_a_module (Label.to_string lab)
in
begin match old.mod_expr with
- | None ->
- let sign,equiv',cst =
- check_with_mod env' old.mod_type (idl,mp1) mp' old.mod_delta in
+ | Abstract ->
+ let struc = destr_nofunctor old.mod_type in
+ let struc',equiv',cst =
+ check_with_mod env' struc (idl,mp1) mp' old.mod_delta
+ in
+ let new_mb =
+ { old with
+ mod_type = NoFunctor struc';
+ mod_type_alg = None;
+ mod_delta = equiv' }
+ in
let new_equiv = add_delta_resolver equiv equiv' in
- let new_mb = { old with
- mod_type = sign;
- mod_type_alg = None;
- mod_delta = equiv'}
- in
let id_subst = map_mp mp' mp' equiv' in
- SEBstruct(before@(lab,SFBmodule new_mb)::subst_signature id_subst after),
- new_equiv,cst
- | Some (SEBident mp0) ->
+ let new_after = subst_structure id_subst after in
+ before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
+ | Algebraic (NoFunctor (MEident mp0)) ->
let mpnew = rebuild_mp mp0 idl in
check_modpath_equiv env' mpnew mp;
- SEBstruct(before@(lab,spec)::after),equiv,Univ.empty_constraint
+ before@(lab,spec)::after, equiv, Univ.empty_constraint
| _ -> error_generative_module_expected lab
end
with
| Not_found -> error_no_such_label lab
| Reduction.NotConvertible -> error_incorrect_with_constraint lab
-let check_with env sign with_decl alg_sign mp equiv =
- let sign,wd,equiv,cst= match with_decl with
- | With_Definition (idl,c) ->
- let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
- sign,With_definition_body(idl,cb),equiv,cst
- | With_Module (idl,mp1) ->
- let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
- sign,With_module_body(idl,mp1),equiv,cst
- in
- match alg_sign with
- | None -> sign, None, equiv, cst
- | Some s -> sign, Some (SEBwith(s, wd)), equiv, cst
-
-let rec translate_module env mp inl me =
- match me.mod_entry_expr, me.mod_entry_type with
- | None, None ->
- Errors.anomaly ~label:"Mod_typing.translate_module"
- (Pp.str "empty type and expr in module entry")
- | None, Some mte ->
- let mtb = translate_module_type env mp inl mte in
- { mod_mp = mp;
- mod_expr = None;
- mod_type = mtb.typ_expr;
- mod_type_alg = mtb.typ_expr_alg;
- mod_delta = mtb.typ_delta;
- mod_constraints = mtb.typ_constraints;
- mod_retroknowledge = []}
- | Some mexpr, _ ->
- let sign,alg_implem,resolver,cst1 =
- translate_struct_module_entry env mp inl mexpr in
- let sign,alg1,resolver,cst2 =
- match me.mod_entry_type with
- | None ->
- sign,None,resolver,Univ.empty_constraint
- | Some mte ->
- let mtb = translate_module_type env mp inl mte in
- let cst = Subtyping.check_subtypes env
- {typ_mp = mp;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = Univ.empty_constraint;
- typ_delta = resolver;}
- mtb
- in
- mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst
- in
- { mod_mp = mp;
- mod_type = sign;
- mod_expr = alg_implem;
- mod_type_alg = alg1;
- mod_constraints = cst1 +++ cst2;
- mod_delta = resolver;
- mod_retroknowledge = []}
- (* spiwack: not so sure about that. It may
- cause a bug when closing nested modules.
- If it does, I don't really know how to
- fix the bug.*)
-
-and translate_apply env inl ftrans mexpr mkalg =
- let sign,alg,resolver,cst1 = ftrans in
+let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
+
+let check_with env mp (sign,alg,reso,cst) = function
+ |WithDef(idl,c) ->
+ let struc = destr_nofunctor sign in
+ let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
+ let alg' = mk_alg_with alg (WithDef (idl,c')) in
+ (NoFunctor struc'),alg',reso, cst+++cst'
+ |WithMod(idl,mp1) as wd ->
+ let struc = destr_nofunctor sign in
+ let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
+ let alg' = mk_alg_with alg wd in
+ (NoFunctor struc'),alg',reso', cst+++cst'
+
+let mk_alg_app mpo alg arg = match mpo, alg with
+ | Some _, Some alg -> Some (MEapply (alg,arg))
+ | _ -> None
+
+(** Translation of 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 [SEBapply] or [SEBfunctor].
+*)
+
+let rec translate_mse env mpo inl = function
+ |MEident mp1 ->
+ let sign,reso = match mpo with
+ |Some mp ->
+ let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
+ mb.mod_type, mb.mod_delta
+ |None ->
+ let mtb = lookup_modtype mp1 env in
+ mtb.typ_expr, mtb.typ_delta
+ in
+ sign,Some (MEident mp1),reso,Univ.empty_constraint
+ |MEapply (fe,mp1) ->
+ translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+ |MEwith(me, with_decl) ->
+ assert (mpo == None); (* No 'with' syntax for modules *)
+ let mp = mp_from_mexpr me in
+ check_with env mp (translate_mse env None inl me) with_decl
+
+and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
let farg_id, farg_b, fbody_b = destr_functor sign in
- let mp1 =
- try path_of_mexpr mexpr
- with Not_path -> error_application_to_not_path mexpr
- in
- let mtb = module_type_of_module None (lookup_module mp1 env) in
+ let mtb = module_type_of_module (lookup_module mp1 env) in
let cst2 = Subtyping.check_subtypes env mtb farg_b in
let mp_delta = discr_resolver mtb in
let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
let subst = map_mbid farg_id mp1 mp_delta in
- subst_struct_expr subst fbody_b,
- mkalg alg mp1 cst2,
- subst_codom_delta_resolver subst resolver,
- cst1 +++ cst2
-
-and translate_functor env inl arg_id arg_e trans mkalg =
- let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
- let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
- let sign,alg,resolver,cst = trans env'
+ let body = subst_signature subst fbody_b in
+ let alg' = mkalg alg mp1 in
+ let reso' = subst_codom_delta_resolver subst reso in
+ body,alg',reso', cst1 +++ cst2
+
+let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
+ | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
+ | _ -> None
+
+let rec translate_mse_funct env mpo inl mse = function
+ |[] ->
+ let sign,alg,reso,cst = translate_mse env mpo inl mse in
+ sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+ |(mbid, ty) :: params ->
+ let mp_id = MPbound mbid in
+ let mtb = translate_modtype env mp_id inl ([],ty) in
+ let env' = add_module_type mp_id mtb env in
+ let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
+ let alg' = mk_alg_funct mpo mbid mtb alg in
+ MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.typ_constraints
+
+and translate_modtype env mp inl (params,mte) =
+ let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
+ let mtb =
+ { typ_mp = mp_from_mexpr mte;
+ typ_expr = sign;
+ typ_expr_alg = None;
+ typ_constraints = cst;
+ typ_delta = reso }
in
- SEBfunctor (arg_id, mtb, sign),
- mkalg alg arg_id mtb,
- resolver,
- cst +++ mtb.typ_constraints
-
-and translate_struct_module_entry env mp inl = function
- | MSEident mp1 ->
- let mb = lookup_module mp1 env in
- let mb' = strengthen_and_subst_mb mb mp false in
- mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
- | MSEfunctor (arg_id, arg_e, body_expr) ->
- let trans env' = translate_struct_module_entry env' mp inl body_expr in
- let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in
- translate_functor env inl arg_id arg_e trans mkalg
- | MSEapply (fexpr,mexpr) ->
- let trans = translate_struct_module_entry env mp inl fexpr in
- let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in
- translate_apply env inl trans mexpr mkalg
- | MSEwith(mte, with_decl) ->
- let sign,alg,resolve,cst1 =
- translate_struct_module_entry env mp inl mte in
- let sign,alg,resolve,cst2 =
- check_with env sign with_decl alg mp resolve in
- sign,alg,resolve, cst1 +++ cst2
-
-and translate_struct_type_entry env inl = function
- | MSEident mp1 ->
- let mtb = lookup_modtype mp1 env in
- mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint
- | MSEfunctor (arg_id, arg_e, body_expr) ->
- let trans env' = translate_struct_type_entry env' inl body_expr in
- translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None)
- | MSEapply (fexpr,mexpr) ->
- let trans = translate_struct_type_entry env inl fexpr in
- translate_apply env inl trans mexpr (fun _ _ _ -> None)
- | MSEwith(mte, with_decl) ->
- let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in
- let sign,alg,resolve,cst2 =
- check_with env sign with_decl alg (mp_from_mexpr mte) resolve
- in
- sign,alg,resolve, cst1 +++ cst2
-
-and translate_module_type env mp inl mte =
- let mp_from = mp_from_mexpr mte in
- let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in
- let mtb = subst_modtype_and_resolver
- {typ_mp = mp_from;
- typ_expr = sign;
- typ_expr_alg = None;
- typ_constraints = cst;
- typ_delta = resolve} mp
- in {mtb with typ_expr_alg = alg}
-
-let rec translate_struct_include_module_entry env mp inl = function
- | MSEident mp1 ->
- let mb = lookup_module mp1 env in
- let mb' = strengthen_and_subst_mb mb mp true in
- let mb_typ = clean_bounded_mod_expr mb'.mod_type in
- mb_typ,None,mb'.mod_delta,Univ.empty_constraint
- | MSEapply (fexpr,mexpr) ->
- let ftrans = translate_struct_include_module_entry env mp inl fexpr in
- translate_apply env inl ftrans mexpr (fun _ _ _ -> None)
- | _ -> Modops.error_higher_order_include ()
-
-let rec add_struct_expr_constraints env = function
- | SEBident _ -> env
-
- | SEBfunctor (_,mtb,meb) ->
- add_struct_expr_constraints
- (add_modtype_constraints env mtb) meb
-
- | SEBstruct (structure_body) ->
- List.fold_left
- (fun env (_,item) -> add_struct_elem_constraints env item)
- env
- structure_body
-
- | SEBapply (meb1,meb2,cst) ->
- Environ.add_constraints cst
- (add_struct_expr_constraints
- (add_struct_expr_constraints env meb1)
- meb2)
- | SEBwith(meb,With_definition_body(_,cb))->
- Environ.add_constraints (Future.force cb.const_constraints)
- (add_struct_expr_constraints env meb)
- | SEBwith(meb,With_module_body(_,_))->
- add_struct_expr_constraints env meb
-
-and add_struct_elem_constraints env = function
- | SFBconst cb ->
- Environ.add_constraints (Future.force cb.const_constraints) env
- | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
- | SFBmodule mb -> add_module_constraints env mb
- | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb =
- let env = match mb.mod_expr with
- | None -> env
- | Some meb -> add_struct_expr_constraints env meb
- in
- let env =
- add_struct_expr_constraints env mb.mod_type
- in
- Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb =
- Environ.add_constraints mtb.typ_constraints
- (add_struct_expr_constraints env mtb.typ_expr)
-
-
-let rec struct_expr_constraints cst = function
- | SEBident _ -> cst
-
- | SEBfunctor (_,mtb,meb) ->
- struct_expr_constraints
- (modtype_constraints cst mtb) meb
-
- | SEBstruct (structure_body) ->
- List.fold_left
- (fun cst (_,item) -> struct_elem_constraints cst item)
- cst
- structure_body
-
- | SEBapply (meb1,meb2,cst1) ->
- struct_expr_constraints (struct_expr_constraints (cst1 +++ cst) meb1)
- meb2
- | SEBwith(meb,With_definition_body(_,cb))->
- struct_expr_constraints ((Future.force cb.const_constraints) +++ cst) meb
- | SEBwith(meb,With_module_body(_,_))->
- struct_expr_constraints cst meb
-
-and struct_elem_constraints cst = function
- | SFBconst cb -> cst
- | SFBmind mib -> cst
- | SFBmodule mb -> module_constraints cst mb
- | SFBmodtype mtb -> modtype_constraints cst mtb
-
-and module_constraints cst mb =
- let cst = match mb.mod_expr with
- | None -> cst
- | Some meb -> struct_expr_constraints cst meb in
- let cst = struct_expr_constraints cst mb.mod_type in
- mb.mod_constraints +++ cst
-
-and modtype_constraints cst mtb =
- struct_expr_constraints (mtb.typ_constraints +++ cst) mtb.typ_expr
-
-
-let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
-let module_constraints = module_constraints Univ.empty_constraint
+ let mtb' = subst_modtype_and_resolver mtb mp in
+ { mtb' with typ_expr_alg = alg }
+
+(** [finalize_module] :
+ from an already-translated (or interactive) implementation
+ and a signature entry, produce a final [module_expr] *)
+
+let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
+ |None ->
+ let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
+ { mod_mp = mp;
+ mod_expr = impl;
+ mod_type = sign;
+ mod_type_alg = None;
+ mod_constraints = cst;
+ mod_delta = reso;
+ mod_retroknowledge = [] }
+ |Some (params_mte,inl) ->
+ let res_mtb = translate_modtype env mp inl params_mte in
+ let auto_mtb = {
+ typ_mp = mp;
+ typ_expr = sign;
+ typ_expr_alg = None;
+ typ_constraints = Univ.empty_constraint;
+ typ_delta = reso } in
+ let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
+ let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
+ { mod_mp = mp;
+ mod_expr = impl;
+ mod_type = res_mtb.typ_expr;
+ mod_type_alg = res_mtb.typ_expr_alg;
+ mod_constraints = cst +++ cst';
+ mod_delta = res_mtb.typ_delta;
+ mod_retroknowledge = [] }
+
+let translate_module env mp inl = function
+ |MType (params,ty) ->
+ let mtb = translate_modtype env mp inl (params,ty) in
+ module_body_of_type mp mtb
+ |MExpr (params,mse,oty) ->
+ let t = translate_mse_funct env (Some mp) inl mse params in
+ let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
+ finalize_module env mp t restype
+
+let rec translate_mse_incl env mp inl = function
+ |MEident mp1 ->
+ let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
+ let sign = clean_bounded_mod_expr mb.mod_type in
+ sign,None,mb.mod_delta,Univ.empty_constraint
+ |MEapply (fe,arg) ->
+ let ftrans = translate_mse_incl env mp inl fe in
+ translate_apply env inl ftrans arg (fun _ _ -> None)
+ |_ -> Modops.error_higher_order_include ()
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0990e36c10..21171705de 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -12,40 +12,40 @@ open Entries
open Mod_subst
open Names
+(** Main functions for translating module entries
+
+ Note : [module_body] and [module_type_body] obtained this way
+ won't have any [MEstruct] in their algebraic fields.
+*)
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.
+ Moreover algebraic expressions obtained here cannot contain [MEstruct].
+*)
-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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index deff291eca..76feb8498d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -51,12 +51,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
@@ -73,8 +73,11 @@ let error_existing_label l =
let error_application_to_not_path mexpr =
raise (ModuleTypingError (ApplicationToNotPath mexpr))
-let error_not_a_functor mtb =
- raise (ModuleTypingError (NotAFunctor mtb))
+let error_not_a_functor () =
+ raise (ModuleTypingError NotAFunctor)
+
+let error_is_a_functor () =
+ raise (ModuleTypingError IsAFunctor)
let error_incompatible_modtypes mexpr1 mexpr2 =
raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2)))
@@ -91,9 +94,6 @@ let error_no_such_label l =
let error_incompatible_labels l l' =
raise (ModuleTypingError (IncompatibleLabels (l,l')))
-let error_signature_expected mtb =
- raise (ModuleTypingError (SignatureExpected mtb))
-
let error_not_a_module s =
raise (ModuleTypingError (NotAModule s))
@@ -112,24 +112,49 @@ let error_no_such_label_sub l l1 =
let error_higher_order_include () =
raise (ModuleTypingError HigherOrderInclude)
-(** {6 Misc operations } *)
+(** {6 Operations on functors } *)
+
+let is_functor = function
+ |NoFunctor _ -> false
+ |MoreFunctor _ -> true
let destr_functor = function
- | SEBfunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
- | mtb -> error_not_a_functor mtb
+ |NoFunctor _ -> error_not_a_functor ()
+ |MoreFunctor (mbid,ty,x) -> (mbid,ty,x)
-let is_functor = function
- | SEBfunctor _ -> true
- | _ -> false
+let destr_nofunctor = function
+ |NoFunctor a -> a
+ |MoreFunctor _ -> error_is_a_functor ()
+
+let rec functor_smartmap fty f0 funct = match funct with
+ |MoreFunctor (mbid,ty,e) ->
+ let ty' = fty ty in
+ let e' = functor_smartmap fty f0 e in
+ if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e')
+ |NoFunctor a ->
+ let a' = f0 a in if a==a' then funct else NoFunctor a'
+
+let rec functor_iter fty f0 = function
+ |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e
+ |NoFunctor a -> f0 a
+
+(** {6 Misc operations } *)
+
+let module_type_of_module mb =
+ { typ_mp = mb.mod_mp;
+ typ_expr = mb.mod_type;
+ typ_expr_alg = None;
+ typ_constraints = mb.mod_constraints;
+ typ_delta = mb.mod_delta }
let module_body_of_type mp mtb =
{ mod_mp = mp;
mod_type = mtb.typ_expr;
mod_type_alg = mtb.typ_expr_alg;
- mod_expr = None;
+ mod_expr = Abstract;
mod_constraints = mtb.typ_constraints;
mod_delta = mtb.typ_delta;
- mod_retroknowledge = []}
+ mod_retroknowledge = [] }
let check_modpath_equiv env mp1 mp2 =
if ModPath.equal mp1 mp2 then ()
@@ -139,17 +164,27 @@ let check_modpath_equiv env mp1 mp2 =
if ModPath.equal mp1' mp2' then ()
else error_not_equal_modpaths mp1 mp2
+let implem_smartmap fs fa impl = match impl with
+ |Struct e -> let e' = fs e in if e==e' then impl else Struct e'
+ |Algebraic a -> let a' = fa a in if a==a' then impl else Algebraic a'
+ |Abstract|FullStruct -> impl
+
+let implem_iter fs fa impl = match impl with
+ |Struct e -> fs e
+ |Algebraic a -> fa a
+ |Abstract|FullStruct -> ()
+
(** {6 Substitutions of modular structures } *)
let id_delta x y = x
let rec subst_with_body sub = function
- |With_module_body(id,mp) as orig ->
+ |WithMod(id,mp) as orig ->
let mp' = subst_mp sub mp in
- if mp==mp' then orig else With_module_body(id,mp')
- |With_definition_body(id,cb) as orig ->
- let cb' = subst_const_body sub cb in
- if cb==cb' then orig else With_definition_body(id,cb')
+ if mp==mp' then orig else WithMod(id,mp')
+ |WithDef(id,c) as orig ->
+ let c' = subst_mps sub c in
+ if c==c' then orig else WithDef(id,c')
and subst_modtype sub do_delta mtb=
let { typ_mp = mp; typ_expr = ty; typ_expr_alg = aty } = mtb in
@@ -158,8 +193,8 @@ and subst_modtype sub do_delta mtb=
if ModPath.equal mp mp' then sub
else add_mp mp mp' empty_delta_resolver sub
in
- let ty' = subst_struct_expr sub do_delta ty in
- let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in
+ let ty' = subst_signature sub do_delta ty in
+ let aty' = Option.smartmap (subst_expression sub id_delta) aty in
let delta' = do_delta mtb.typ_delta sub in
if mp==mp' && ty==ty' && aty==aty' && delta'==mtb.typ_delta
then mtb
@@ -172,16 +207,16 @@ and subst_modtype sub do_delta mtb=
and subst_structure sub do_delta sign =
let subst_body ((l,body) as orig) = match body with
- | SFBconst cb ->
+ |SFBconst cb ->
let cb' = subst_const_body sub cb in
if cb==cb' then orig else (l,SFBconst cb')
- | SFBmind mib ->
+ |SFBmind mib ->
let mib' = subst_mind sub mib in
if mib==mib' then orig else (l,SFBmind mib')
- | SFBmodule mb ->
+ |SFBmodule mb ->
let mb' = subst_module sub do_delta mb in
if mb==mb' then orig else (l,SFBmodule mb')
- | SFBmodtype mtb ->
+ |SFBmodtype mtb ->
let mtb' = subst_modtype sub do_delta mtb in
if mtb==mtb' then orig else (l,SFBmodtype mtb')
in
@@ -194,13 +229,12 @@ and subst_module sub do_delta mb =
if not (is_functor ty) || ModPath.equal mp mp' then sub
else add_mp mp mp' empty_delta_resolver sub
in
- let ty' = subst_struct_expr sub do_delta ty in
- (* Special optim : maintain sharing between [mod_expr] and [mod_type] *)
- let me' = match me with
- | Some m when m == ty -> if ty == ty' then me else Some ty'
- | _ -> Option.smartmap (subst_struct_expr sub id_delta) me
+ let ty' = subst_signature sub do_delta ty in
+ let me' =
+ implem_smartmap
+ (subst_signature sub id_delta) (subst_expression sub id_delta) me
in
- let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in
+ let aty' = Option.smartmap (subst_expression sub id_delta) aty in
let delta' = do_delta mb.mod_delta sub in
if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
then mb
@@ -212,34 +246,35 @@ and subst_module sub do_delta mb =
mod_type_alg = aty';
mod_delta = delta' }
-and subst_struct_expr sub do_delta seb = match seb with
- |SEBident mp ->
+and subst_expr sub do_delta seb = match seb with
+ |MEident mp ->
let mp' = subst_mp sub mp in
- if mp==mp' then seb else SEBident mp'
- |SEBfunctor (mbid, mtb, meb) ->
- let mtb' = subst_modtype sub do_delta mtb in
- let meb' = subst_struct_expr sub do_delta meb in
- if mtb==mtb' && meb==meb' then seb
- else SEBfunctor(mbid,mtb',meb')
- |SEBstruct str ->
- let str' = subst_structure sub do_delta str in
- if str==str' then seb else SEBstruct str'
- |SEBapply (meb1,meb2,cst) ->
- let meb1' = subst_struct_expr sub do_delta meb1 in
- let meb2' = subst_struct_expr sub do_delta meb2 in
- if meb1==meb1' && meb2==meb2' then seb else SEBapply(meb1',meb2',cst)
- |SEBwith (meb,wdb) ->
- let meb' = subst_struct_expr sub do_delta meb in
+ if mp==mp' then seb else MEident mp'
+ |MEapply (meb1,mp2) ->
+ let meb1' = subst_expr sub do_delta meb1 in
+ let mp2' = subst_mp sub mp2 in
+ if meb1==meb1' && mp2==mp2' then seb else MEapply(meb1',mp2')
+ |MEwith (meb,wdb) ->
+ let meb' = subst_expr sub do_delta meb in
let wdb' = subst_with_body sub wdb in
- if meb==meb' && wdb==wdb' then seb else SEBwith(meb',wdb')
+ if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb')
+
+and subst_expression sub do_delta =
+ functor_smartmap
+ (subst_modtype sub do_delta)
+ (subst_expr sub do_delta)
+
+and subst_signature sub do_delta =
+ functor_smartmap
+ (subst_modtype sub do_delta)
+ (subst_structure sub do_delta)
-let subst_signature subst =
- subst_structure subst
- (fun resolver subst-> subst_codom_delta_resolver subst resolver)
+let do_delta_dom reso sub = subst_dom_delta_resolver sub reso
+let do_delta_codom reso sub = subst_codom_delta_resolver sub reso
+let do_delta_dom_codom reso sub = subst_dom_codom_delta_resolver sub reso
-let subst_struct_expr subst =
- subst_struct_expr subst
- (fun resolver subst-> subst_codom_delta_resolver subst resolver)
+let subst_signature subst = subst_signature subst do_delta_codom
+let subst_structure subst = subst_structure subst do_delta_codom
(** {6 Retroknowledge } *)
@@ -247,16 +282,12 @@ let subst_struct_expr subst =
the retroknowledge declared in the library *)
(* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
let add_retroknowledge mp =
- let perform rkaction env =
- match rkaction with
- | Retroknowledge.RKRegister (f, e) ->
- Environ.register env f
- (match e with
- | Const kn -> kind_of_term (mkConst kn)
- | Ind ind -> kind_of_term (mkInd ind)
- | _ ->
- anomaly ~label:"Modops.add_retroknowledge"
- (Pp.str "had to import an unsupported kind of term"))
+ let perform rkaction env = match rkaction with
+ |Retroknowledge.RKRegister (f, (Const _ | Ind _ as e)) ->
+ Environ.register env f e
+ |_ ->
+ Errors.anomaly ~label:"Modops.add_retroknowledge"
+ (Pp.str "had to import an unsupported kind of term")
in
fun lclrk env ->
(* The order of the declaration matters, for instance (and it's at the
@@ -271,7 +302,7 @@ let add_retroknowledge mp =
(** {6 Adding a module in the environment } *)
-let rec add_signature mp sign resolver env =
+let rec add_structure mp sign resolver env =
let add_one env (l,elem) = match elem with
|SFBconst cb ->
let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
@@ -288,105 +319,71 @@ and add_module mb env =
let mp = mb.mod_mp in
let env = Environ.shallow_add_module mb env in
match mb.mod_type with
- | SEBstruct (sign) ->
+ |NoFunctor struc ->
add_retroknowledge mp mb.mod_retroknowledge
- (add_signature mp sign mb.mod_delta env)
- | SEBfunctor _ -> env
- | _ ->
- anomaly ~label:"Modops"
- (Pp.str "the evaluation of the structure failed ")
+ (add_structure mp struc mb.mod_delta env)
+ |MoreFunctor _ -> env
+
+let add_module_type mp mtb env =
+ add_module (module_body_of_type mp mtb) env
(** {6 Strengtening } *)
let strengthen_const mp_from l cb resolver =
match cb.const_body with
- | Def _ -> cb
- | _ ->
- let kn = KerName.make2 mp_from l in
- let con = constant_of_delta_kn resolver kn in
- { cb with
- const_body = Def (Lazyconstr.from_val (mkConst con));
- const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
- }
+ |Def _ -> cb
+ |_ ->
+ let kn = KerName.make2 mp_from l in
+ let con = constant_of_delta_kn resolver kn in
+ { cb with
+ const_body = Def (Lazyconstr.from_val (mkConst con));
+ const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
let rec strengthen_mod mp_from mp_to mb =
- if mp_in_delta mb.mod_mp mb.mod_delta then
- mb
- else
- match mb.mod_type with
- | SEBstruct (sign) ->
- let resolve_out,sign_out =
- strengthen_sig mp_from sign mp_to mb.mod_delta
- in
- { mb with
- mod_expr = Some (SEBident mp_to);
- mod_type = SEBstruct(sign_out);
- mod_type_alg = mb.mod_type_alg;
- mod_constraints = mb.mod_constraints;
- mod_delta = add_mp_delta_resolver mp_from mp_to
- (add_delta_resolver mb.mod_delta resolve_out);
- mod_retroknowledge = mb.mod_retroknowledge }
- | SEBfunctor _ -> mb
- | _ ->
- anomaly ~label:"Modops"
- (Pp.str "the evaluation of the structure failed ")
-
-and strengthen_sig mp_from sign mp_to resolver =
- match sign with
- | [] -> empty_delta_resolver,[]
- | (l,SFBconst cb) :: rest ->
- let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out,item'::rest'
- | (_,SFBmind _ as item):: rest ->
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out,item::rest'
- | (l,SFBmodule mb) :: rest ->
- let mp_from' = MPdot (mp_from,l) in
- let mp_to' = MPdot(mp_to,l) in
- let mb_out = strengthen_mod mp_from' mp_to' mb in
- let item' = l,SFBmodule (mb_out) in
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- add_delta_resolver resolve_out mb.mod_delta, item':: rest'
- | (l,SFBmodtype mty as item) :: rest ->
- let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
- resolve_out,item::rest'
+ if mp_in_delta mb.mod_mp mb.mod_delta then mb
+ else match mb.mod_type with
+ |NoFunctor struc ->
+ let reso,struc' = strengthen_sig mp_from struc mp_to mb.mod_delta in
+ { mb with
+ mod_expr = Algebraic (NoFunctor (MEident mp_to));
+ mod_type = NoFunctor struc';
+ mod_delta =
+ add_mp_delta_resolver mp_from mp_to
+ (add_delta_resolver mb.mod_delta reso) }
+ |MoreFunctor _ -> mb
+
+and strengthen_sig mp_from struc mp_to reso = match struc with
+ |[] -> empty_delta_resolver,[]
+ |(l,SFBconst cb) :: rest ->
+ let item' = l,SFBconst (strengthen_const mp_from l cb reso) in
+ let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+ reso',item'::rest'
+ |(_,SFBmind _ as item):: rest ->
+ let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+ reso',item::rest'
+ |(l,SFBmodule mb) :: rest ->
+ let mp_from' = MPdot (mp_from,l) in
+ let mp_to' = MPdot(mp_to,l) in
+ let mb' = strengthen_mod mp_from' mp_to' mb in
+ let item' = l,SFBmodule mb' in
+ let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+ add_delta_resolver reso' mb.mod_delta, item':: rest'
+ |(l,SFBmodtype mty as item) :: rest ->
+ let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+ reso',item::rest'
let strengthen mtb mp =
- if mp_in_delta mtb.typ_mp mtb.typ_delta then
- (* in this case mtb has already been strengthened*)
- mtb
- else
- match mtb.typ_expr with
- | SEBstruct (sign) ->
- let resolve_out,sign_out =
- strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
- in
- {mtb with
- typ_expr = SEBstruct(sign_out);
- typ_delta = add_delta_resolver mtb.typ_delta
- (add_mp_delta_resolver mtb.typ_mp mp resolve_out)}
- | SEBfunctor _ -> mtb
- | _ ->
- anomaly ~label:"Modops"
- (Pp.str "the evaluation of the structure failed ")
-
-let module_type_of_module mp mb =
- match mp with
- Some mp ->
- strengthen {
- typ_mp = mp;
- typ_expr = mb.mod_type;
- typ_expr_alg = None;
- typ_constraints = mb.mod_constraints;
- typ_delta = mb.mod_delta} mp
-
- | None ->
- {typ_mp = mb.mod_mp;
- typ_expr = mb.mod_type;
- typ_expr_alg = None;
- typ_constraints = mb.mod_constraints;
- typ_delta = mb.mod_delta}
+ (* Has mtb already been strengthened ? *)
+ if mp_in_delta mtb.typ_mp mtb.typ_delta then mtb
+ else match mtb.typ_expr with
+ |NoFunctor struc ->
+ let reso',struc' = strengthen_sig mtb.typ_mp struc mp mtb.typ_delta in
+ { mtb with
+ typ_expr = NoFunctor struc';
+ typ_delta =
+ add_delta_resolver mtb.typ_delta
+ (add_mp_delta_resolver mtb.typ_mp mp reso') }
+ |MoreFunctor _ -> mtb
let inline_delta_resolver env inl mp mbid mtb delta =
let constants = inline_of_delta inl mtb.typ_delta in
@@ -409,109 +406,97 @@ let inline_delta_resolver env inl mp mbid mtb delta =
in
make_inline delta constants
-let rec strengthen_and_subst_mod mb subst mp_from mp_to resolver =
+let rec strengthen_and_subst_mod mb subst mp_from mp_to =
match mb.mod_type with
- | SEBstruct str ->
- let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
- if mb_is_an_alias then
- subst_module subst
- (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb
- else
- let resolver,new_sig =
- strengthen_and_subst_struct str subst
- mp_from mp_from mp_to false false mb.mod_delta
- in
- {mb with
- mod_mp = mp_to;
- mod_expr = Some (SEBident mp_from);
- mod_type = SEBstruct(new_sig);
- mod_delta = add_mp_delta_resolver mp_to mp_from resolver}
- | SEBfunctor(arg_id,arg_b,body) ->
- let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
- subst_module subst
- (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb
- | _ ->
- anomaly ~label:"Modops"
- (Pp.str "the evaluation of the structure failed ")
-
-and strengthen_and_subst_struct
- str subst mp_alias mp_from mp_to alias incl resolver =
+ |NoFunctor struc ->
+ let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
+ if mb_is_an_alias then subst_module subst do_delta_dom mb
+ else
+ let reso',struc' =
+ strengthen_and_subst_struct struc subst
+ mp_from mp_to false false mb.mod_delta
+ in
+ { mb with
+ mod_mp = mp_to;
+ mod_expr = Algebraic (NoFunctor (MEident mp_from));
+ mod_type = NoFunctor struc';
+ mod_delta = add_mp_delta_resolver mp_to mp_from reso' }
+ |MoreFunctor _ ->
+ let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
+ subst_module subst do_delta_dom mb
+
+and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
match str with
| [] -> empty_delta_resolver,[]
| (l,SFBconst cb) :: rest ->
- let item' = if alias then
- (* case alias no strengthening needed*)
- l,SFBconst (subst_const_body subst cb)
- else
- l,SFBconst (strengthen_const mp_from l
- (subst_const_body subst cb) resolver)
- in
- let resolve_out,rest' =
- strengthen_and_subst_struct rest subst
- mp_alias mp_from mp_to alias incl resolver in
+ let cb' = subst_const_body subst cb in
+ let cb'' =
+ if alias then cb'
+ else strengthen_const mp_from l cb' reso
+ in
+ let item' = l, SFBconst cb'' in
+ let reso',rest' =
+ strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+ in
if incl then
- (* If we are performing an inclusion we need to add
- the fact that the constant mp_to.l is \Delta-equivalent
- to resolver(mp_from.l) *)
- let kn_from = KerName.make2 mp_from l in
- let kn_to = KerName.make2 mp_to l in
- let old_name = kn_of_delta resolver kn_from in
- (add_kn_delta_resolver kn_to old_name resolve_out),
- item'::rest'
+ (* If we are performing an inclusion we need to add
+ the fact that the constant mp_to.l is \Delta-equivalent
+ to reso(mp_from.l) *)
+ let kn_from = KerName.make2 mp_from l in
+ let kn_to = KerName.make2 mp_to l in
+ let old_name = kn_of_delta reso kn_from in
+ add_kn_delta_resolver kn_to old_name reso', item'::rest'
else
- (*In this case the fact that the constant mp_to.l is
- \Delta-equivalent to resolver(mp_from.l) is already known
- because resolve_out contains mp_to maps to resolver(mp_from)*)
- resolve_out,item'::rest'
+ (* In this case the fact that the constant mp_to.l is
+ \Delta-equivalent to resolver(mp_from.l) is already known
+ because reso' contains mp_to maps to reso(mp_from) *)
+ reso', item'::rest'
| (l,SFBmind mib) :: rest ->
- (*Same as constant*)
let item' = l,SFBmind (subst_mind subst mib) in
- let resolve_out,rest' =
- strengthen_and_subst_struct rest subst
- mp_alias mp_from mp_to alias incl resolver in
+ let reso',rest' =
+ strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+ in
+ (* Same as constant *)
if incl then
let kn_from = KerName.make2 mp_from l in
let kn_to = KerName.make2 mp_to l in
- let old_name = kn_of_delta resolver kn_from in
- (add_kn_delta_resolver kn_to old_name resolve_out),
- item'::rest'
+ let old_name = kn_of_delta reso kn_from in
+ add_kn_delta_resolver kn_to old_name reso', item'::rest'
else
- resolve_out,item'::rest'
+ reso', item'::rest'
| (l,SFBmodule mb) :: rest ->
let mp_from' = MPdot (mp_from,l) in
- let mp_to' = MPdot(mp_to,l) in
- let mb_out = if alias then
- subst_module subst
- (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb
+ let mp_to' = MPdot (mp_to,l) in
+ let mb' = if alias then
+ subst_module subst do_delta_dom mb
else
- strengthen_and_subst_mod
- mb subst mp_from' mp_to' resolver
+ strengthen_and_subst_mod mb subst mp_from' mp_to'
in
- let item' = l,SFBmodule (mb_out) in
- let resolve_out,rest' =
- strengthen_and_subst_struct rest subst
- mp_alias mp_from mp_to alias incl resolver in
- (* if mb is a functor we should not derive new equivalences
- on names, hence we add the fact that the functor can only
- be equivalent to itself. If we adopt an applicative
- semantic for functor this should be changed.*)
- if is_functor mb_out.mod_type then
- (add_mp_delta_resolver
- mp_to' mp_to' resolve_out),item':: rest'
- else
- add_delta_resolver resolve_out mb_out.mod_delta,
- item':: rest'
- | (l,SFBmodtype mty) :: rest ->
+ let item' = l,SFBmodule mb' in
+ let reso',rest' =
+ strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+ in
+ (* if mb is a functor we should not derive new equivalences
+ on names, hence we add the fact that the functor can only
+ be equivalent to itself. If we adopt an applicative
+ semantic for functor this should be changed.*)
+ if is_functor mb'.mod_type then
+ add_mp_delta_resolver mp_to' mp_to' reso', item':: rest'
+ else
+ add_delta_resolver reso' mb'.mod_delta, item':: rest'
+ | (l,SFBmodtype mty) :: rest ->
let mp_from' = MPdot (mp_from,l) in
let mp_to' = MPdot(mp_to,l) in
let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
- let mty = subst_modtype subst'
- (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
- let resolve_out,rest' = strengthen_and_subst_struct rest subst
- mp_alias mp_from mp_to alias incl resolver
+ let mty = subst_modtype subst'
+ (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver)
+ mty
in
- (add_mp_delta_resolver mp_to' mp_to' resolve_out),
- (l,SFBmodtype mty)::rest'
+ let item' = l,SFBmodtype mty in
+ let reso',rest' =
+ strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+ in
+ add_mp_delta_resolver mp_to' mp_to' reso', item'::rest'
(** Let P be a module path when we write:
@@ -521,7 +506,7 @@ and strengthen_and_subst_struct
- The second one is strenghtening. *)
let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
- |SEBstruct str ->
+ |NoFunctor struc ->
let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
(* if mb.mod_mp is an alias then the strengthening is useless
(i.e. it is already done)*)
@@ -529,168 +514,125 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
let new_resolver =
add_mp_delta_resolver mp mp_alias
- (subst_dom_delta_resolver subst_resolver mb.mod_delta) in
+ (subst_dom_delta_resolver subst_resolver mb.mod_delta)
+ in
let subst = map_mp mb.mod_mp mp new_resolver in
- let resolver_out,new_sig =
- strengthen_and_subst_struct str subst
- mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
+ let reso',struc' =
+ strengthen_and_subst_struct struc subst
+ mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
in
{ mb with
mod_mp = mp;
- mod_type = SEBstruct(new_sig);
- mod_expr = Some (SEBident mb.mod_mp);
+ mod_type = NoFunctor struc';
+ mod_expr = Algebraic (NoFunctor (MEident mb.mod_mp));
mod_delta =
- if include_b then resolver_out
- else add_delta_resolver new_resolver resolver_out }
- |SEBfunctor(arg_id,argb,body) ->
+ if include_b then reso'
+ else add_delta_resolver new_resolver reso' }
+ |MoreFunctor _ ->
let subst = map_mp mb.mod_mp mp empty_delta_resolver in
- subst_module subst
- (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb
- | _ ->
- anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-
+ subst_module subst do_delta_dom_codom mb
let subst_modtype_and_resolver mtb mp =
- let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in
+ let subst = map_mp mtb.typ_mp mp empty_delta_resolver in
let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
- let full_subst = (map_mp mtb.typ_mp mp new_delta) in
- subst_modtype full_subst
- (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb
+ let full_subst = map_mp mtb.typ_mp mp new_delta in
+ subst_modtype full_subst do_delta_dom_codom mtb
+
+(** {6 Cleaning a module expression from bounded parts }
-(** {6 Cleaning a bounded module expression } *)
+ For instance:
+ functor(X:T)->struct module M:=X end)
+ becomes:
+ functor(X:T)->struct module M:=<content of T> end)
+*)
let rec is_bounded_expr l = function
- | SEBident mp -> List.mem mp l
- | SEBapply (fexpr,mexpr,_) ->
- is_bounded_expr l mexpr || is_bounded_expr l fexpr
+ | MEident (MPbound mbid) -> MBIset.mem mbid l
+ | MEapply (fexpr,mp) ->
+ is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr
| _ -> false
-let rec clean_struct l = function
- | (lab,SFBmodule mb) as field ->
- let clean_typ = clean_expr l mb.mod_type in
- let clean_impl =
- begin try
- if (is_bounded_expr l (Option.get mb.mod_expr)) then
- Some clean_typ
- else Some (clean_expr l (Option.get mb.mod_expr))
- with
- Option.IsNone -> None
- end in
- if clean_typ==mb.mod_type && clean_impl==mb.mod_expr then
- field
- else
- (lab,SFBmodule {mb with
- mod_type=clean_typ;
- mod_expr=clean_impl})
- | field -> field
-
-and clean_expr l = function
- | SEBfunctor (mbid,sigt,str) as s->
- let str_clean = clean_expr l str in
- let sig_clean = clean_expr l sigt.typ_expr in
- if str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **)
- s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
- | SEBstruct str as s->
- let str_clean = List.smartmap (clean_struct l) str in
- if str_clean == str then s else SEBstruct(str_clean)
- | str -> str
-
-let rec collect_mbid l = function
- | SEBfunctor (mbid,sigt,str) as s->
- let str_clean = collect_mbid ((MPbound mbid)::l) str in
- if str_clean == str then s else
- SEBfunctor (mbid,sigt,str_clean)
- | SEBstruct str as s->
- let str_clean = List.smartmap (clean_struct l) str in
- if str_clean == str then s else SEBstruct(str_clean)
- | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-
-
-let clean_bounded_mod_expr = function
- | SEBfunctor _ as str ->
- let str_clean = collect_mbid [] str in
- if str_clean == str then str else str_clean
- | str -> str
+let rec clean_module l mb =
+ let impl, typ = mb.mod_expr, mb.mod_type in
+ let typ' = clean_signature l typ in
+ let impl' = match impl with
+ | Algebraic (NoFunctor m) when is_bounded_expr l m -> FullStruct
+ | _ -> implem_smartmap (clean_signature l) (clean_expression l) impl
+ in
+ if typ==typ' && impl==impl' then mb
+ else { mb with mod_type=typ'; mod_expr=impl' }
+
+and clean_modtype l mt =
+ let ty = mt.typ_expr in
+ let ty' = clean_signature l ty in
+ if ty==ty' then mt else { mt with typ_expr=ty' }
+
+and clean_field l field = match field with
+ |(lab,SFBmodule mb) ->
+ let mb' = clean_module l mb in
+ if mb==mb' then field else (lab,SFBmodule mb')
+ |_ -> field
+
+and clean_structure l = List.smartmap (clean_field l)
+
+and clean_signature l =
+ functor_smartmap (clean_modtype l) (clean_structure l)
+
+and clean_expression l =
+ functor_smartmap (clean_modtype l) (fun me -> me)
+
+let rec collect_mbid l sign = match sign with
+ |MoreFunctor (mbid,ty,m) ->
+ let m' = collect_mbid (MBIset.add mbid l) m in
+ if m==m' then sign else MoreFunctor (mbid,ty,m')
+ |NoFunctor struc ->
+ let struc' = clean_structure l struc in
+ if struc==struc' then sign else NoFunctor struc'
+
+let clean_bounded_mod_expr sign =
+ if is_functor sign then collect_mbid MBIset.empty sign else sign
(** {6 Stm machinery : join and prune } *)
-let rec join_module_body mb =
- Option.iter join_struct_expr_body mb.mod_expr;
- Option.iter join_struct_expr_body mb.mod_type_alg;
- join_struct_expr_body mb.mod_type
-and join_structure_body struc =
- let join_body (l,body) = match body with
- | SFBconst sb -> join_constant_body sb
- | SFBmind _ -> ()
- | SFBmodule m -> join_module_body m
- | SFBmodtype m ->
- join_struct_expr_body m.typ_expr;
- Option.iter join_struct_expr_body m.typ_expr_alg in
- List.iter join_body struc;
-and join_struct_expr_body = function
- | SEBfunctor (_,t,e) ->
- join_struct_expr_body t.typ_expr;
- Option.iter join_struct_expr_body t.typ_expr_alg;
- join_struct_expr_body e
- | SEBident mp -> ()
- | SEBstruct s -> join_structure_body s
- | SEBapply (mexpr,marg,u) ->
- join_struct_expr_body mexpr;
- join_struct_expr_body marg
- | SEBwith (seb,wdcl) ->
- join_struct_expr_body seb;
- match wdcl with
- | With_module_body _ -> ()
- | With_definition_body (_, sb) -> join_constant_body sb
-
-let rec prune_module_body mb =
+let rec join_module mb =
+ implem_iter join_signature join_expression mb.mod_expr;
+ Option.iter join_expression mb.mod_type_alg;
+ join_signature mb.mod_type
+and join_modtype mt =
+ Option.iter join_expression mt.typ_expr_alg;
+ join_signature mt.typ_expr
+and join_field (l,body) = match body with
+ |SFBconst sb -> join_constant_body sb
+ |SFBmind _ -> ()
+ |SFBmodule m -> join_module m
+ |SFBmodtype m -> join_modtype m
+and join_structure struc = List.iter join_field struc
+and join_signature sign = functor_iter join_modtype join_structure sign
+and join_expression me = functor_iter join_modtype (fun _ -> ()) me
+
+let rec prune_module mb =
let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in
- let me' = Option.smartmap prune_struct_expr_body me in
- let mta' = Option.smartmap prune_struct_expr_body mta in
- let mt' = prune_struct_expr_body mt in
+ let mt' = prune_signature mt in
+ let me' = implem_smartmap prune_signature prune_expression me in
+ let mta' = Option.smartmap prune_expression mta in
if me' == me && mta' == mta && mt' == mt then mb
else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'}
-and prune_structure_body struc =
- let prune_body (l,body as orig) = match body with
- | SFBconst sb ->
- let sb' = prune_constant_body sb in
- if sb == sb' then orig else (l, SFBconst sb')
- | SFBmind _ -> orig
- | SFBmodule m ->
- let m' = prune_module_body m in
- if m == m' then orig else (l, SFBmodule m')
- | SFBmodtype m ->
- let te, te_alg = m.typ_expr, m.typ_expr_alg in
- let te' = prune_struct_expr_body te in
- let te_alg' =
- Option.smartmap prune_struct_expr_body te_alg in
- if te' == te && te_alg' == te_alg then orig
- else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'})
- in
- List.smartmap prune_body struc
-and prune_struct_expr_body orig = match orig with
- | SEBfunctor (id,t,e) ->
- let te, ta = t.typ_expr, t.typ_expr_alg in
- let te' = prune_struct_expr_body te in
- let ta' = Option.smartmap prune_struct_expr_body ta in
- let e' = prune_struct_expr_body e in
- if te' == te && ta' == ta && e' == e then orig
- else SEBfunctor(id, {t with typ_expr = te'; typ_expr_alg = ta'}, e')
- | SEBident _ -> orig
- | SEBstruct s ->
- let s' = prune_structure_body s in
- if s' == s then orig else SEBstruct s'
- | SEBapply (mexpr,marg,u) ->
- let mexpr' = prune_struct_expr_body mexpr in
- let marg' = prune_struct_expr_body marg in
- if mexpr' == mexpr && marg' == marg then orig
- else SEBapply (mexpr', marg', u)
- | SEBwith (seb,wdcl) ->
- let seb' = prune_struct_expr_body seb in
- let wdcl' = match wdcl with
- | With_module_body _ -> wdcl
- | With_definition_body (id, sb) ->
- let sb' = prune_constant_body sb in
- if sb' == sb then wdcl else With_definition_body (id, sb') in
- if seb' == seb && wdcl' == wdcl then orig
- else SEBwith (seb', wdcl')
+and prune_modtype mt =
+ let te, ta = mt.typ_expr, mt.typ_expr_alg in
+ let te' = prune_signature te in
+ let ta' = Option.smartmap prune_expression ta in
+ if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' }
+and prune_field (l,body as orig) = match body with
+ |SFBconst sb ->
+ let sb' = prune_constant_body sb in
+ if sb == sb' then orig else (l, SFBconst sb')
+ |SFBmind _ -> orig
+ |SFBmodule m ->
+ let m' = prune_module m in
+ if m == m' then orig else (l, SFBmodule m')
+ |SFBmodtype m ->
+ let m' = prune_modtype m in
+ if m == m' then orig else (l, SFBmodtype m')
+and prune_structure struc = List.smartmap prune_field struc
+and prune_signature sign = functor_smartmap prune_modtype prune_structure sign
+and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e148f96282..6aed95988c 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
diff --git a/kernel/names.ml b/kernel/names.ml
index fbd26ca3d8..0da8fc5d42 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -234,6 +234,7 @@ struct
end
module MBImap = Map.Make(MBId)
+module MBIset = Set.Make(MBId)
(** {6 Names of structure elements } *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 8022cb199e..c05e30b9b5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -169,6 +169,7 @@ sig
end
+module MBIset : Set.S with type elt = MBId.t
module MBImap : Map.S with type key = MBId.t
(** {6 The module part of the kernel name } *)
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index acb740cd0e..55d3485503 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -19,13 +19,11 @@ compiler *)
let rec translate_mod prefix mp env mod_expr acc =
match mod_expr with
- | SEBident mp' -> assert false
- | SEBstruct msb ->
- let env' = add_signature mp msb empty_delta_resolver env in
- List.fold_left (translate_field prefix mp env') acc msb
- | SEBfunctor (mbid,mtb,meb) -> acc
- | SEBapply (f,x,_) -> assert false
- | SEBwith _ -> assert false
+ | NoFunctor struc ->
+ let env' = add_structure mp struc empty_delta_resolver env in
+ List.fold_left (translate_field prefix mp env') acc struc
+ | MoreFunctor _ -> acc
+
and translate_field prefix mp env (code, upds as acc) (l,x) =
match x with
| SFBconst cb ->
@@ -41,14 +39,14 @@ and translate_field prefix mp env (code, upds as acc) (l,x) =
let dump_library mp dp env mod_expr =
if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
match mod_expr with
- | SEBstruct msb ->
- let env = add_signature mp msb empty_delta_resolver env in
+ | NoFunctor struc ->
+ let env = add_structure mp struc empty_delta_resolver env in
let prefix = mod_uid_of_dirpath dp ^ "." in
- let t0 = Sys.time () in
+ let t0 = Sys.time () in
clear_global_tbl ();
clear_symb_tbl ();
let mlcode, upds =
- List.fold_left (translate_field prefix mp env) ([],empty_updates) msb
+ List.fold_left (translate_field prefix mp env) ([],empty_updates) struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 7b74b00c52..3f413631c1 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -13,7 +13,7 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-val dump_library : module_path -> dir_path -> env -> struct_expr_body ->
+val dump_library : module_path -> dir_path -> env -> module_signature ->
global list * symbol array * code_location_updates
val compile_library :
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c7711b137d..5ff619ce15 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,8 +194,8 @@ let is_curmod_library senv =
match senv.modvariant with LIBRARY -> true | _ -> false
let join_safe_environment e =
- Modops.join_structure_body e.revstruct;
- List.fold_left
+ Modops.join_structure e.revstruct;
+ List.fold_left
(fun e fc -> add_constraints (Now (Future.join fc)) e)
{e with future_cst = []} e.future_cst
@@ -213,7 +213,7 @@ let prune_env env =
let prune_safe_environment e =
{ e with
modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE);
- revstruct = Modops.prune_structure_body e.revstruct;
+ revstruct = Modops.prune_structure e.revstruct;
future_cst = [];
env = prune_env e.env }
@@ -433,9 +433,9 @@ let add_mind dir l mie senv =
(** Insertion of module types *)
-let add_modtype l mte inl senv =
+let add_modtype l params_mte inl senv =
let mp = MPdot(senv.modpath, l) in
- let mtb = Mod_typing.translate_module_type senv.env mp inl mte in
+ let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in
let senv' = add_field (l,SFBmodtype mtb) MT senv in
mp, senv'
@@ -445,16 +445,19 @@ let full_add_module mb senv =
let senv = add_constraints (Now mb.mod_constraints) senv in
{ senv with env = Modops.add_module mb senv.env }
+let full_add_module_type mp mt senv =
+ let senv = add_constraints (Now mt.typ_constraints) senv in
+ { senv with env = Modops.add_module_type mp mt senv.env }
+
(** Insertion of modules *)
let add_module l me inl senv =
let mp = MPdot(senv.modpath, l) in
let mb = Mod_typing.translate_module senv.env mp inl me in
let senv' = add_field (l,SFBmodule mb) M senv in
- let senv'' = match mb.mod_type with
- | SEBstruct _ ->
- update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv'
- | _ -> senv'
+ let senv'' =
+ if Modops.is_functor mb.mod_type then senv'
+ else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv'
in
(mp,mb.mod_delta),senv''
@@ -489,27 +492,24 @@ let start_modtype l senv =
let add_module_parameter mbid mte inl senv =
let () = check_empty_struct senv in
let mp = MPbound mbid in
- let mtb = Mod_typing.translate_module_type senv.env mp inl mte in
- let senv = full_add_module (Modops.module_body_of_type mp mtb) senv in
+ let mtb = Mod_typing.translate_modtype senv.env mp inl ([],mte) in
+ let senv = full_add_module_type mp mtb senv in
let new_variant = match senv.modvariant with
| STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv)
| SIG (params,oldenv) -> SIG ((mbid,mtb) :: params, oldenv)
| _ -> assert false
in
- let new_paramresolver = match mtb.typ_expr with
- | SEBstruct _ ->
- Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver
- | _ -> senv.paramresolver
+ let new_paramresolver =
+ if Modops.is_functor mtb.typ_expr then senv.paramresolver
+ else Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver
in
mtb.typ_delta,
{ senv with
modvariant = new_variant;
paramresolver = new_paramresolver }
-let functorize_struct params seb0 =
- List.fold_left
- (fun seb (arg_id,arg_b) -> SEBfunctor(arg_id,arg_b,seb))
- seb0 params
+let functorize params init =
+ List.fold_left (fun e (mbid,mt) -> MoreFunctor(mbid,mt,e)) init params
let propagate_loads senv =
List.fold_left
@@ -520,36 +520,22 @@ let propagate_loads senv =
(** Build the module body of the current module, taking in account
a possible return type (_:T) *)
+let functorize_module params mb =
+ let f x = functorize params x in
+ { mb with
+ mod_expr = Modops.implem_smartmap f f mb.mod_expr;
+ mod_type = f mb.mod_type;
+ mod_type_alg = Option.map f mb.mod_type_alg }
+
let build_module_body params restype senv =
- let mp = senv.modpath in
- let mexpr = SEBstruct (List.rev senv.revstruct) in
- let mexpr' = functorize_struct params mexpr in
- match restype with
- | None ->
- { mod_mp = mp;
- mod_expr = Some mexpr';
- mod_type = mexpr';
- mod_type_alg = None;
- mod_constraints = senv.univ;
- mod_delta = senv.modresolver;
- mod_retroknowledge = senv.local_retroknowledge }
- | Some (res,inl) ->
- let res_mtb = Mod_typing.translate_module_type senv.env mp inl res in
- let auto_mtb = {
- typ_mp = mp;
- typ_expr = mexpr;
- typ_expr_alg = None;
- typ_constraints = Univ.empty_constraint;
- typ_delta = Mod_subst.empty_delta_resolver} in
- let cst = Subtyping.check_subtypes senv.env auto_mtb res_mtb in
- { mod_mp = mp;
- mod_expr = Some mexpr';
- mod_type = functorize_struct params res_mtb.typ_expr;
- mod_type_alg =
- Option.map (functorize_struct params) res_mtb.typ_expr_alg;
- mod_constraints = Univ.union_constraints cst senv.univ;
- mod_delta = res_mtb.typ_delta;
- mod_retroknowledge = senv.local_retroknowledge }
+ let struc = NoFunctor (List.rev senv.revstruct) in
+ let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) restype in
+ let mb =
+ Mod_typing.finalize_module senv.env senv.modpath
+ (struc,None,senv.modresolver,senv.univ) restype'
+ in
+ let mb' = functorize_module params mb in
+ { mb' with mod_retroknowledge = senv.local_retroknowledge }
(** Returning back to the old pre-interactive-module environment,
with one extra component and some updated fields
@@ -582,10 +568,9 @@ let end_module l restype senv =
let senv'= propagate_loads {senv with env=newenv} in
let newenv = Environ.add_constraints mb.mod_constraints senv'.env in
let newenv = Modops.add_module mb newenv in
- let newresolver = match mb.mod_type with
- | SEBstruct _ ->
- Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver
- | _ -> oldsenv.modresolver
+ let newresolver =
+ if Modops.is_functor mb.mod_type then oldsenv.modresolver
+ else Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver
in
(mp,mbids,mb.mod_delta),
propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv
@@ -596,14 +581,14 @@ let end_modtype l senv =
let () = check_current_label l mp in
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
- let auto_tb = SEBstruct (List.rev senv.revstruct) in
+ let auto_tb = NoFunctor (List.rev senv.revstruct) in
let newenv = oldsenv.env in
let newenv = Environ.add_constraints senv.univ newenv in
let newenv = set_engagement_opt newenv senv.engagement in
let senv' = propagate_loads {senv with env=newenv} in
let mtb =
{ typ_mp = mp;
- typ_expr = functorize_struct params auto_tb;
+ typ_expr = functorize params auto_tb;
typ_expr_alg = None;
typ_constraints = senv'.univ;
typ_delta = senv.modresolver }
@@ -616,22 +601,21 @@ let end_modtype l senv =
(** {6 Inclusion of module or module type } *)
let add_include me is_module inl senv =
+ let open Mod_typing in
let mp_sup = senv.modpath in
let sign,cst,resolver =
if is_module then
- let sign,_,resolver,cst =
- Mod_typing.translate_struct_include_module_entry senv.env mp_sup inl me
- in
- sign,cst,resolver
+ let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in
+ sign,cst,reso
else
- let mtb = Mod_typing.translate_module_type senv.env mp_sup inl me in
+ let mtb = translate_modtype senv.env mp_sup inl ([],me) in
mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
in
let senv = add_constraints (Now cst) senv in
(* Include Self support *)
let rec compute_sign sign mb resolver senv =
match sign with
- | SEBfunctor(mbid,mtb,str) ->
+ | MoreFunctor(mbid,mtb,str) ->
let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
let senv = add_constraints (Now cst_sub) senv in
let mpsup_delta =
@@ -639,21 +623,21 @@ let add_include me is_module inl senv =
in
let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
- compute_sign (Modops.subst_struct_expr subst str) mb resolver senv
+ compute_sign (Modops.subst_signature subst str) mb resolver senv
| str -> resolver,str,senv
in
let resolver,sign,senv =
let mtb =
{ typ_mp = mp_sup;
- typ_expr = SEBstruct (List.rev senv.revstruct);
+ typ_expr = NoFunctor (List.rev senv.revstruct);
typ_expr_alg = None;
typ_constraints = Univ.empty_constraint;
typ_delta = senv.modresolver } in
compute_sign sign mtb resolver senv
in
let str = match sign with
- | SEBstruct str_l -> str_l
- | _ -> Modops.error_higher_order_include ()
+ | NoFunctor struc -> struc
+ | MoreFunctor _ -> Modops.error_higher_order_include ()
in
let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv
in
@@ -682,7 +666,7 @@ type compiled_library = {
type native_library = Nativecode.global list
-let join_compiled_library l = Modops.join_module_body l.comp_mod
+let join_compiled_library l = Modops.join_module l.comp_mod
let start_library dir senv =
check_initial senv;
@@ -702,10 +686,10 @@ let export senv dir =
in
let () = check_current_library dir senv in
let mp = senv.modpath in
- let str = SEBstruct (List.rev senv.revstruct) in
+ let str = NoFunctor (List.rev senv.revstruct) in
let mb =
{ mod_mp = mp;
- mod_expr = Some str;
+ mod_expr = FullStruct;
mod_type = str;
mod_type_alg = None;
mod_constraints = senv.univ;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 3d67f6c073..5d1c98de53 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,7 +73,7 @@ val add_module :
Label.t -> Entries.module_entry -> Declarations.inline ->
(module_path * Mod_subst.delta_resolver) safe_transformer
val add_modtype :
- Label.t -> Entries.module_struct_entry -> Declarations.inline ->
+ Label.t -> Entries.module_type_entry -> Declarations.inline ->
module_path safe_transformer
(** Adding universe constraints *)
@@ -94,6 +94,8 @@ val add_module_parameter :
MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
Mod_subst.delta_resolver safe_transformer
+(** The optional result type is given without its functorial part *)
+
val end_module :
Label.t -> (Entries.module_struct_entry * Declarations.inline) option ->
(module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 99c1b8483e..6cedb6ad23 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -319,10 +319,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
check_conv error cst conv env ty1 ty2
let rec check_modules cst env msb1 msb2 subst1 subst2 =
- let mty1 = module_type_of_module None msb1 in
- let mty2 = module_type_of_module None msb2 in
- let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
- cst
+ let mty1 = module_type_of_module msb1 in
+ let mty2 = module_type_of_module msb2 in
+ check_modtypes cst env mty1 mty2 subst1 subst2 false
and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
let map1 = make_labmap mp1 sig1 in
@@ -344,67 +343,62 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
| Modtype mtb -> mtb
| _ -> 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
- check_modtypes cst env mtb1 mtb2 subst1 subst2 true
+ let env =
+ add_module_type mtb2.typ_mp mtb2
+ (add_module_type mtb1.typ_mp mtb1 env)
+ in
+ check_modtypes cst env mtb1 mtb2 subst1 subst2 true
in
List.fold_left check_one_body cst sig2
-and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
- if mtb1==mtb2 then cst else
- let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
- let rec check_structure cst env str1 str2 equiv subst1 subst2 =
- match str1,str2 with
- | SEBstruct (list1),
- SEBstruct (list2) ->
- if equiv then
- let subst2 =
- add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
- Univ.union_constraints
- (check_signatures cst env
- mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
- mtb1.typ_delta mtb2.typ_delta)
- (check_signatures cst env
- mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
- mtb2.typ_delta mtb1.typ_delta)
- else
- check_signatures cst env
- mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
- mtb1.typ_delta mtb2.typ_delta
- | SEBfunctor (arg_id1,arg_t1,body_t1),
- SEBfunctor (arg_id2,arg_t2,body_t2) ->
- let subst1 =
- (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in
- let cst = check_modtypes cst env
- arg_t2 arg_t1 subst2 subst1
- equiv in
- (* contravariant *)
- let env = add_module
- (module_body_of_type (MPbound arg_id2) arg_t2) env
- in
- let env = match body_t1 with
- SEBstruct str ->
- add_module {mod_mp = mtb1.typ_mp;
- mod_expr = None;
- mod_type = subst_struct_expr subst1 body_t1;
- mod_type_alg= None;
- mod_constraints=mtb1.typ_constraints;
- mod_retroknowledge = [];
- mod_delta = mtb1.typ_delta} env
- | _ -> env
- in
- check_structure cst env body_t1 body_t2 equiv
- subst1
- subst2
- | _ , _ -> error_incompatible_modtypes mtb1 mtb2
- in
- if mtb1'== mtb2' then cst
- else check_structure cst env mtb1' mtb2' equiv subst1 subst2
+and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
+ if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then cst
+ else
+ let rec check_structure cst env str1 str2 equiv subst1 subst2 =
+ match str1,str2 with
+ |NoFunctor list1,
+ NoFunctor list2 ->
+ if equiv then
+ let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
+ let cst1 = check_signatures cst env
+ mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+ mtb1.typ_delta mtb2.typ_delta
+ in
+ let cst2 = check_signatures cst env
+ mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
+ mtb2.typ_delta mtb1.typ_delta
+ in
+ Univ.union_constraints cst1 cst2
+ else
+ check_signatures cst env
+ mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+ mtb1.typ_delta mtb2.typ_delta
+ |MoreFunctor (arg_id1,arg_t1,body_t1),
+ MoreFunctor (arg_id2,arg_t2,body_t2) ->
+ let mp2 = MPbound arg_id2 in
+ let subst1 = join (map_mbid arg_id1 mp2 arg_t2.typ_delta) subst1 in
+ let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in
+ (* contravariant *)
+ let env = add_module_type mp2 arg_t2 env in
+ let env =
+ if Modops.is_functor body_t1 then env
+ else add_module
+ {mod_mp = mtb1.typ_mp;
+ mod_expr = Abstract;
+ mod_type = subst_signature subst1 body_t1;
+ mod_type_alg = None;
+ mod_constraints = mtb1.typ_constraints;
+ mod_retroknowledge = [];
+ mod_delta = mtb1.typ_delta} env
+ in
+ check_structure cst env body_t1 body_t2 equiv subst1 subst2
+ | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+ in
+ check_structure cst env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
let check_subtypes env sup super =
- let env = add_module
- (module_body_of_type sup.typ_mp sup) env in
- check_modtypes empty_constraint env
+ let env = add_module_type sup.typ_mp sup env in
+ check_modtypes empty_constraint env
(strengthen sup sup.typ_mp) super empty_subst
(map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:01:05 +0000