diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-20 08:22:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-20 08:22:51 +0000 |
commit | ec2948e7848265dbf547d97f0866ebd8f5cb6c97 (patch) | |
tree | 15c8ca8918a8a633c7664d564b14efb8f987385a | |
parent | 5275368649a254835a5277dfa185506713506618 (diff) |
Declareops + Modops : more clever substitutions
We try harder to preserve pointer equality when substituting.
This will probably have little effect (for instance the
constr_substituted are anyway _never_ substituted in place),
but it cannot harm.
Two particular cases:
- we try to share (and maintain shared) mind_user_lc and mind_nf_lc
- we try to share (and maintain shared) mod_expr and mod_type
TODO: check that native compiler is still ok, since we might have
less (ref NotLinked) now. Having references in constant_body and co
is anyway a Very Bad Idea (TM).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/declareops.ml | 188 | ||||
-rw-r--r-- | kernel/declareops.mli | 1 | ||||
-rw-r--r-- | kernel/modops.ml | 327 | ||||
-rw-r--r-- | kernel/modops.mli | 26 |
4 files changed, 310 insertions, 232 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 76d9876c4..da945b67b 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -14,7 +14,7 @@ open Util (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) -(** Constants *) +(** {6 Constants } *) let body_of_constant cb = match cb.const_body with | Undef _ -> None @@ -29,40 +29,54 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Undef _ | Def _ -> false -(** Constant substitutions *) +(** {7 Constant substitutions } *) let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in - if copt == copt' & t == t' then x else (id,copt',t') + if copt == copt' && t == t' then x else (id,copt',t') let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -(* TODO: these substitution functions could avoid duplicating things - when the substitution have preserved all the fields *) +let subst_const_type sub arity = match arity with + | NonPolymorphicType s -> + let s' = subst_mps sub s in + if s==s' then arity else NonPolymorphicType s' + | PolymorphicArity (ctx,s) -> + let ctx' = subst_rel_context sub ctx in + if ctx==ctx' then arity else PolymorphicArity (ctx',s) -let subst_const_type sub arity = - if is_empty_subst sub then arity - else match arity with - | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) - | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) +(** No need here to check for physical equality after substitution, + at least for Def due to the delayed substitution [subst_constr_subst]. *) -let subst_const_def sub = function - | Undef inl -> Undef inl +let subst_const_def sub def = match def with + | Undef _ -> def | Def c -> Def (subst_constr_subst sub c) | OpaqueDef lc -> - OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub)) - -let subst_const_body sub cb = { - const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false); - const_body = subst_const_def sub cb.const_body; - const_type = subst_const_type sub cb.const_type; - const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; - const_constraints = cb.const_constraints; - const_native_name = ref NotLinked; - const_inline_code = cb.const_inline_code } - -(** Hash-consing of constants *) + OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub)) + +let subst_const_body sub cb = + assert (List.is_empty cb.const_hyps); (* we're outside sections *) + if is_empty_subst sub then cb + else + let body' = subst_const_def sub cb.const_body in + let type' = subst_const_type sub cb.const_type in + if body' == cb.const_body && type' == cb.const_type then cb + else + { const_hyps = []; + const_body = body'; + const_type = type'; + const_body_code = + Cemitcodes.subst_to_patch_subst sub cb.const_body_code; + const_constraints = cb.const_constraints; + const_native_name = ref NotLinked; + const_inline_code = cb.const_inline_code } + +(** {7 Hash-consing of constants } *) + +(** This hash-consing is currently quite partial : we only + share internal fields (e.g. constr), and not the records + themselves. But would it really bring substantial gains ? *) let hcons_rel_decl ((n,oc,t) as d) = let n' = Names.Name.hcons n @@ -103,7 +117,7 @@ let hcons_const_body cb = (Univ.hcons_constraints (Future.force cb.const_constraints)) else cb.const_constraints } -(** Inductive types *) +(** {6 Inductive types } *) let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true @@ -113,10 +127,12 @@ let eq_recarg r1 r2 = match r1, r2 with let subst_recarg sub r = match r with | Norec -> r - | Mrec (kn,i) -> let kn' = subst_ind sub kn in - if kn==kn' then r else Mrec (kn',i) - | Imbr (kn,i) -> let kn' = subst_ind sub kn in - if kn==kn' then r else Imbr (kn',i) + | Mrec (kn,i) -> + let kn' = subst_ind sub kn in + if kn==kn' then r else Mrec (kn',i) + | Imbr (kn,i) -> + let kn' = subst_ind sub kn in + if kn==kn' then r else Imbr (kn',i) let mk_norec = Rtree.mk_node Norec [||] @@ -142,61 +158,79 @@ let recarg_length p j = let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p -(** Substitution of inductive declarations *) - -let subst_indarity sub = function -| Monomorphic s -> - Monomorphic { - mind_user_arity = subst_mps sub s.mind_user_arity; - mind_sort = s.mind_sort; - } -| Polymorphic s as x -> x - -let subst_mind_packet sub mbp = - { mind_consnames = mbp.mind_consnames; - mind_consnrealdecls = mbp.mind_consnrealdecls; - mind_typename = mbp.mind_typename; - mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; - mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; - mind_arity = subst_indarity sub mbp.mind_arity; - mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; - mind_nrealargs = mbp.mind_nrealargs; - mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; - mind_kelim = mbp.mind_kelim; - mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); - mind_nb_constant = mbp.mind_nb_constant; - mind_nb_args = mbp.mind_nb_args; - mind_reloc_tbl = mbp.mind_reloc_tbl } +(** {7 Substitution of inductive declarations } *) + +let subst_indarity sub ar = match ar with + | Monomorphic s -> + let uar' = subst_mps sub s.mind_user_arity in + if uar' == s.mind_user_arity then ar + else Monomorphic { mind_user_arity = uar'; mind_sort = s.mind_sort } + | Polymorphic _ -> ar + +let subst_mind_packet sub mip = + let { mind_nf_lc = nf; + mind_user_lc = user; + mind_arity_ctxt = ctxt; + mind_arity = ar; + mind_recargs = ra } = mip + in + let nf' = Array.smartmap (subst_mps sub) nf in + let user' = + (* maintain sharing of [mind_user_lc] and [mind_nf_lc] *) + if user==nf then nf' + else Array.smartmap (subst_mps sub) user + in + let ctxt' = subst_rel_context sub ctxt in + let ar' = subst_indarity sub ar in + let ra' = subst_wf_paths sub ra in + if nf==nf' && user==user' && ctxt==ctxt' && ar==ar' && ra==ra' + then mip + else + { mip with + mind_nf_lc = nf'; + mind_user_lc = user'; + mind_arity_ctxt = ctxt'; + mind_arity = ar'; + mind_recargs = ra' } let subst_mind sub mib = - { mind_record = mib.mind_record ; - mind_finite = mib.mind_finite ; - mind_ntypes = mib.mind_ntypes ; - mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); - mind_nparams = mib.mind_nparams; - mind_nparams_rec = mib.mind_nparams_rec; - mind_params_ctxt = - Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints; - mind_native_name = ref NotLinked } - -(** Hash-consing of inductive declarations *) + assert (List.is_empty mib.mind_hyps); (* we're outside sections *) + if is_empty_subst sub then mib + else + let params = mib.mind_params_ctxt in + let params' = Context.map_rel_context (subst_mps sub) params in + let packets = mib.mind_packets in + let packets' = Array.smartmap (subst_mind_packet sub) packets in + if params==params' && packets==packets' then mib + else + { mib with + mind_params_ctxt = params'; + mind_packets = packets'; + mind_native_name = ref NotLinked } + +(** {6 Hash-consing of inductive declarations } *) + +(** Just as for constants, this hash-consing is quite partial *) let hcons_indarity = function | Monomorphic a -> - Monomorphic { mind_user_arity = Term.hcons_constr a.mind_user_arity; - mind_sort = Term.hcons_sorts a.mind_sort } + Monomorphic + { mind_user_arity = Term.hcons_constr a.mind_user_arity; + mind_sort = Term.hcons_sorts a.mind_sort } | Polymorphic a -> Polymorphic (hcons_polyarity a) let hcons_mind_packet oib = - { oib with - mind_typename = Names.Id.hcons oib.mind_typename; - mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; - mind_arity = hcons_indarity oib.mind_arity; - mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; - mind_user_lc = Array.smartmap Term.hcons_types oib.mind_user_lc; - mind_nf_lc = Array.smartmap Term.hcons_types oib.mind_nf_lc } + let user = Array.smartmap Term.hcons_types oib.mind_user_lc in + let nf = Array.smartmap Term.hcons_types oib.mind_nf_lc in + (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *) + let nf = if Array.equal (==) user nf then user else nf in + { oib with + mind_typename = Names.Id.hcons oib.mind_typename; + mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; + mind_arity = hcons_indarity oib.mind_arity; + mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames; + mind_user_lc = user; + mind_nf_lc = nf } let hcons_mind mib = { mib with @@ -204,6 +238,8 @@ let hcons_mind mib = mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_constraints = Univ.hcons_constraints mib.mind_constraints } +(** {6 Stm machinery } *) + let join_constant_body cb = ignore(Future.join cb.const_constraints); match cb.const_body with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0da7c85c7..54eed5ea6 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -14,7 +14,6 @@ open Mod_subst (** {6 Constants} *) -val subst_const_def : substitution -> constant_def -> constant_def val subst_const_body : substitution -> constant_body -> constant_body (** Is there a actual body in const_body ? *) diff --git a/kernel/modops.ml b/kernel/modops.ml index d431fdfdd..deff291ec 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -25,6 +25,8 @@ open Environ open Entries open Mod_subst +(** {6 Errors } *) + type signature_mismatch_error = | InductiveFieldExpected of mutual_inductive_body | DefinitionFieldExpected @@ -45,7 +47,8 @@ type signature_mismatch_error = | NoTypeConstraintExpected type module_typing_error = - | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error + | SignatureMismatch of + Label.t * structure_field_body * signature_mismatch_error | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry | NotAFunctor of struct_expr_body @@ -109,17 +112,17 @@ let error_no_such_label_sub l l1 = let error_higher_order_include () = raise (ModuleTypingError HigherOrderInclude) -let destr_functor mtb = - match mtb with - | SEBfunctor (arg_id,arg_t,body_t) -> - (arg_id,arg_t,body_t) - | _ -> error_not_a_functor mtb +(** {6 Misc operations } *) + +let destr_functor = function + | SEBfunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) + | mtb -> error_not_a_functor mtb let is_functor = function - | SEBfunctor (arg_id,arg_t,body_t) -> true - | _ -> false + | SEBfunctor _ -> true + | _ -> false -let module_body_of_type mp mtb = +let module_body_of_type mp mtb = { mod_mp = mp; mod_type = mtb.typ_expr; mod_type_alg = mtb.typ_expr_alg; @@ -128,103 +131,119 @@ let module_body_of_type mp mtb = mod_delta = mtb.typ_delta; mod_retroknowledge = []} -let check_modpath_equiv env mp1 mp2 = - if mp_eq mp1 mp2 then () else - let mb1=lookup_module mp1 env in - let mb2=lookup_module mp2 env in - if mp_eq (mp_of_delta mb1.mod_delta mp1) (mp_of_delta mb2.mod_delta mp2) - then () - else error_not_equal_modpaths mp1 mp2 - +let check_modpath_equiv env mp1 mp2 = + if ModPath.equal mp1 mp2 then () + else + let mp1' = mp_of_delta (lookup_module mp1 env).mod_delta mp1 in + let mp2' = mp_of_delta (lookup_module mp2 env).mod_delta mp2 in + if ModPath.equal mp1' mp2' then () + else error_not_equal_modpaths mp1 mp2 + +(** {6 Substitutions of modular structures } *) + +let id_delta x y = x + let rec subst_with_body sub = function - | With_module_body(id,mp) -> - With_module_body(id,subst_mp sub mp) - | With_definition_body(id,cb) -> - With_definition_body( id,subst_const_body sub cb) + |With_module_body(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') and subst_modtype sub do_delta mtb= - let mp = subst_mp sub mtb.typ_mp in - let sub = add_mp mtb.typ_mp mp empty_delta_resolver sub in - let typ_expr' = subst_struct_expr sub do_delta mtb.typ_expr in - let typ_alg' = - Option.smartmap - (subst_struct_expr sub (fun x y-> x)) mtb.typ_expr_alg in - let mtb_delta = do_delta mtb.typ_delta sub in - if typ_expr'==mtb.typ_expr && - typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then - mtb - else - {mtb with - typ_mp = mp; - typ_expr = typ_expr'; - typ_expr_alg = typ_alg'; - typ_delta = mtb_delta} - -and subst_structure sub do_delta sign = - let subst_body = function - SFBconst cb -> - SFBconst (subst_const_body sub cb) - | SFBmind mib -> - SFBmind (subst_mind sub mib) - | SFBmodule mb -> - SFBmodule (subst_module sub do_delta mb) - | SFBmodtype mtb -> - SFBmodtype (subst_modtype sub do_delta mtb) + let { typ_mp = mp; typ_expr = ty; typ_expr_alg = aty } = mtb in + let mp' = subst_mp sub mp in + let sub = + if ModPath.equal mp mp' then sub + else add_mp mp mp' empty_delta_resolver sub in - List.map (fun (l,b) -> (l,subst_body b)) sign + let ty' = subst_struct_expr sub do_delta ty in + let aty' = Option.smartmap (subst_struct_expr 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 + else + { mtb with + typ_mp = mp'; + typ_expr = ty'; + typ_expr_alg = aty'; + typ_delta = delta' } + +and subst_structure sub do_delta sign = + let subst_body ((l,body) as orig) = match body with + | SFBconst cb -> + let cb' = subst_const_body sub cb in + if cb==cb' then orig else (l,SFBconst cb') + | SFBmind mib -> + let mib' = subst_mind sub mib in + if mib==mib' then orig else (l,SFBmind mib') + | SFBmodule mb -> + let mb' = subst_module sub do_delta mb in + if mb==mb' then orig else (l,SFBmodule mb') + | SFBmodtype mtb -> + let mtb' = subst_modtype sub do_delta mtb in + if mtb==mtb' then orig else (l,SFBmodtype mtb') + in + List.smartmap subst_body sign and subst_module sub do_delta mb = - let mp = subst_mp sub mb.mod_mp in - let sub = if is_functor mb.mod_type && not (mp_eq mp mb.mod_mp) then - add_mp mb.mod_mp mp - empty_delta_resolver sub else sub in - let id_delta = (fun x y-> x) in - let mtb',me' = - let mtb = subst_struct_expr sub do_delta mb.mod_type in - match mb.mod_expr with - None -> mtb,None - | Some me -> if me==mb.mod_type then - mtb,Some mtb - else mtb,Option.smartmap - (subst_struct_expr sub id_delta) mb.mod_expr + let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in + let mp' = subst_mp sub mp in + let sub = + 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 in - let typ_alg' = Option.smartmap - (subst_struct_expr sub id_delta) mb.mod_type_alg in - let mb_delta = do_delta mb.mod_delta sub in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mb_delta == mb.mod_delta && mp == mb.mod_mp - then mb else - { mb with - mod_mp = mp; - mod_expr = me'; - mod_type_alg = typ_alg'; - mod_type=mtb'; - mod_delta = mb_delta} - -and subst_struct_expr sub do_delta = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (mbid, mtb, meb') -> - SEBfunctor(mbid,subst_modtype sub do_delta mtb - ,subst_struct_expr sub do_delta meb') - | SEBstruct (str)-> - SEBstruct( subst_structure sub do_delta str) - | SEBapply (meb1,meb2,cst)-> - SEBapply(subst_struct_expr sub do_delta meb1, - subst_struct_expr sub do_delta meb2, - cst) - | SEBwith (meb,wdb)-> - SEBwith(subst_struct_expr sub do_delta meb, - subst_with_body sub wdb) + let aty' = Option.smartmap (subst_struct_expr 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 + else + { mb with + mod_mp = mp'; + mod_expr = me'; + mod_type = ty'; + mod_type_alg = aty'; + mod_delta = delta' } + +and subst_struct_expr sub do_delta seb = match seb with + |SEBident 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 + let wdb' = subst_with_body sub wdb in + if meb==meb' && wdb==wdb' then seb else SEBwith(meb',wdb') let subst_signature subst = - subst_structure subst + subst_structure subst (fun resolver subst-> subst_codom_delta_resolver subst resolver) -let subst_struct_expr subst = +let subst_struct_expr subst = subst_struct_expr subst (fun resolver subst-> subst_codom_delta_resolver subst resolver) -(* spiwack: here comes the function which takes care of importing +(** {6 Retroknowledge } *) + +(* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge mp = @@ -235,7 +254,9 @@ let add_retroknowledge mp = (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")) + | _ -> + 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 @@ -243,23 +264,25 @@ let add_retroknowledge mp = int31 type registration absolutely needs int31 bits to be registered. Since the local_retroknowledge is stored in reverse order (each new registration is added at the top of the list) we need a fold_right - for things to go right (the pun is not intented). So we lose + for things to go right (the pun is not intented). So we lose tail recursivity, but the world will have exploded before any module imports 10 000 retroknowledge registration.*) List.fold_right perform lclrk env -let rec add_signature mp sign resolver env = - let add_one env (l,elem) = - let kn = KerName.make2 mp l in - match elem with - | SFBconst cb -> - Environ.add_constant (constant_of_delta_kn resolver kn) cb env - | SFBmind mib -> - Environ.add_mind (mind_of_delta_kn resolver kn) mib env - | SFBmodule mb -> add_module mb env (* adds components as well *) - | SFBmodtype mtb -> Environ.add_modtype mtb env +(** {6 Adding a module in the environment } *) + +let rec add_signature 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 + Environ.add_constant c cb env + |SFBmind mib -> + let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in + Environ.add_mind mind mib env + |SFBmodule mb -> add_module mb env (* adds components as well *) + |SFBmodtype mtb -> Environ.add_modtype mtb env in - List.fold_left add_one env sign + List.fold_left add_one env sign and add_module mb env = let mp = mb.mod_mp in @@ -273,6 +296,8 @@ and add_module mb env = anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ") +(** {6 Strengtening } *) + let strengthen_const mp_from l cb resolver = match cb.const_body with | Def _ -> cb @@ -489,48 +514,54 @@ and strengthen_and_subst_struct (l,SFBmodtype mty)::rest' -(* Let P be a module path when we write "Module M:=P." or "Module M. Include P. End M." - we need to perform two operations to compute the body of M. The first one is applying - the substitution {P <- M} on the type of P and the second one is strenghtening. *) -let strengthen_and_subst_mb mb mp include_b = - match mb.mod_type with - SEBstruct str -> - 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)*) - let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in - 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 - 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 - in - {mb with - mod_mp = mp; - mod_type = SEBstruct(new_sig); - mod_expr = Some (SEBident mb.mod_mp); - mod_delta = if include_b then resolver_out - else add_delta_resolver new_resolver resolver_out} - | SEBfunctor(arg_id,argb,body) -> - 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 ") +(** Let P be a module path when we write: + "Module M:=P." or "Module M. Include P. End M." + We need to perform two operations to compute the body of M. + - The first one is applying the substitution {P <- M} on the type of P + - The second one is strenghtening. *) + +let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with + |SEBstruct str -> + 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)*) + let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in + 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 + 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 + in + { mb with + mod_mp = mp; + mod_type = SEBstruct(new_sig); + mod_expr = Some (SEBident mb.mod_mp); + mod_delta = + if include_b then resolver_out + else add_delta_resolver new_resolver resolver_out } + |SEBfunctor(arg_id,argb,body) -> + 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 ") let subst_modtype_and_resolver mtb mp = 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 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 + subst_modtype full_subst + (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb + +(** {6 Cleaning a bounded module expression } *) let rec is_bounded_expr l = function | SEBident mp -> List.mem mp l - | SEBapply (fexpr,mexpr,_) -> + | SEBapply (fexpr,mexpr,_) -> is_bounded_expr l mexpr || is_bounded_expr l fexpr | _ -> false @@ -560,9 +591,9 @@ and clean_expr l = function 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 = Util.List.smartmap (clean_struct l) str in - if str_clean == str then s else SEBstruct(str_clean) - | str -> str + 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-> @@ -570,8 +601,8 @@ let rec collect_mbid l = function if str_clean == str then s else SEBfunctor (mbid,sigt,str_clean) | SEBstruct str as s-> - let str_clean = Util.List.smartmap (clean_struct l) str in - if str_clean == str then s else SEBstruct(str_clean) + 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 ") @@ -581,6 +612,8 @@ let clean_bounded_mod_expr = function if str_clean == str then str else str_clean | str -> str +(** {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; @@ -632,8 +665,9 @@ and prune_structure_body struc = 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 - CList.smartmap prune_body struc + 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 @@ -660,4 +694,3 @@ and prune_struct_expr_body orig = match orig with if sb' == sb then wdcl else With_definition_body (id, sb') in if seb' == seb && wdcl' == wdcl then orig else SEBwith (seb', wdcl') - diff --git a/kernel/modops.mli b/kernel/modops.mli index ea92c45ea..e148f9628 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -14,28 +14,33 @@ open Declarations open Entries open Mod_subst -(** Various operations on modules and module types *) +(** {6 Various operations on modules and module types } *) +val module_body_of_type : module_path -> module_type_body -> module_body -val module_body_of_type : module_path -> module_type_body -> module_body - -val module_type_of_module : module_path option -> module_body -> - module_type_body +val module_type_of_module : + module_path option -> module_body -> module_type_body val destr_functor : struct_expr_body -> MBId.t * module_type_body * struct_expr_body +val check_modpath_equiv : env -> module_path -> module_path -> unit + +(** {6 Substitutions } *) + val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body val subst_signature : substitution -> structure_body -> structure_body +(** {6 Adding to an environment } *) + val add_signature : module_path -> structure_body -> delta_resolver -> env -> env (** adds a module and its components, but not the constraints *) val add_module : module_body -> env -> env -val check_modpath_equiv : env -> module_path -> module_path -> unit +(** {6 Strengthening } *) val strengthen : module_type_body -> module_path -> module_type_body @@ -48,15 +53,19 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body val subst_modtype_and_resolver : module_type_body -> module_path -> module_type_body +(** {6 Cleaning a bound module expression } *) + val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body +(** {6 Stm machinery : join and prune } *) + val join_module_body : module_body -> unit val join_structure_body : structure_body -> unit val join_struct_expr_body : struct_expr_body -> unit val prune_structure_body : structure_body -> structure_body -(** Errors *) +(** {6 Errors } *) type signature_mismatch_error = | InductiveFieldExpected of mutual_inductive_body @@ -78,7 +87,8 @@ type signature_mismatch_error = | NoTypeConstraintExpected type module_typing_error = - | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error + | SignatureMismatch of + Label.t * structure_field_body * signature_mismatch_error | LabelAlreadyDeclared of Label.t | ApplicationToNotPath of module_struct_entry | NotAFunctor of struct_expr_body |