diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.mli | 105 | ||||
| -rw-r--r-- | kernel/entries.mli | 24 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 468 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 56 | ||||
| -rw-r--r-- | kernel/modops.ml | 712 | ||||
| -rw-r--r-- | kernel/modops.mli | 54 | ||||
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | kernel/nativelibrary.ml | 20 | ||||
| -rw-r--r-- | kernel/nativelibrary.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 118 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 114 |
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 |