From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/modops.ml | 886 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 457 insertions(+), 429 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index 3a914477..392e667b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (arg_id,arg_t,body_t) - | _ -> error_not_a_functor mtb +(** {6 Operations on functors } *) let is_functor = function - | SEBfunctor (arg_id,arg_t,body_t) -> true - | _ -> false - -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_constraints = mtb.typ_constraints; - mod_delta = mtb.typ_delta; - mod_retroknowledge = []} - -let check_modpath_equiv env mp1 mp2 = - if mp1=mp2 then () else - let mb1=lookup_module mp1 env in - let mb2=lookup_module mp2 env in - if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2) - then () - else error_not_equal_modpaths mp1 mp2 - -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) - -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) + |NoFunctor _ -> false + |MoreFunctor _ -> true + +let destr_functor = function + |NoFunctor _ -> error_not_a_functor () + |MoreFunctor (mbid,ty,x) -> (mbid,ty,x) + +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 = + { mb with mod_expr = Abstract; mod_type_alg = None } + +let module_body_of_type mp mtb = + assert (mtb.mod_expr == Abstract); + { mtb with mod_mp = mp } + +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 + +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 subst_with_body sub = function + |WithMod(id,mp) as orig -> + let mp' = subst_mp sub mp in + 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') + +let rec 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_body 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.map (fun (l,b) -> (l,subst_body b)) 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=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 + List.smartmap subst_body sign + +and subst_body is_mod sub do_delta mb = + 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 ModPath.equal mp mp' then sub + else if is_mod && not (is_functor ty) then sub + else add_mp mp mp' empty_delta_resolver sub 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 subst_signature subst = - subst_structure subst - (fun resolver subst-> subst_codom_delta_resolver subst resolver) - -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 + 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_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 + else + { mb with + mod_mp = mp'; + mod_expr = me'; + mod_type = ty'; + mod_type_alg = aty'; + mod_delta = delta' } + +and subst_module sub do_delta mb = subst_body true sub do_delta mb + +and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb + +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 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 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 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_signature subst = subst_signature subst do_delta_codom +let subst_structure subst = subst_structure subst do_delta_codom + +(** {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 = - 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 "Modops.add_retroknowledge: had to import an unsupported kind of term") + let perform rkaction env = match rkaction with + |Retroknowledge.RKRegister (f, e) when (isConst e || isInd 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 @@ -256,120 +276,117 @@ 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 = make_kn mp empty_dirpath 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.typ_mp mtb env +(** {6 Adding a module in the environment } *) + +let rec add_structure mp sign resolver linkinfo 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_key c cb linkinfo env + |SFBmind mib -> + let mind = mind_of_delta_kn resolver (KerName.make2 mp l) in + let mib = + if mib.mind_private != None then + { mib with mind_private = Some true } + else mib + in + Environ.add_mind_key mind (mib,ref linkinfo) env + |SFBmodule mb -> add_module mb linkinfo 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 = +and add_module mb linkinfo env = let mp = mb.mod_mp in - let env = Environ.shallow_add_module mp mb env in - match mb.mod_type with - | SEBstruct (sign) -> - add_retroknowledge mp mb.mod_retroknowledge - (add_signature mp sign mb.mod_delta env) - | SEBfunctor _ -> env - | _ -> anomaly "Modops:the evaluation of the structure failed " + let env = Environ.shallow_add_module mb env in + match mb.mod_type with + |NoFunctor struc -> + add_retroknowledge mp mb.mod_retroknowledge + (add_structure mp struc mb.mod_delta linkinfo env) + |MoreFunctor _ -> env + +let add_linked_module mb linkinfo env = + add_module mb linkinfo env + +let add_structure mp sign resolver env = + add_structure mp sign resolver no_link_info env + +let add_module mb env = + add_module mb no_link_info 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 = make_kn mp_from empty_dirpath l in - let con = constant_of_delta_kn resolver kn in + |Def _ -> cb + |_ -> + let kn = KerName.make2 mp_from l in + let con = constant_of_delta_kn resolver kn in + let u = + if cb.const_polymorphic then + Univ.UContext.instance cb.const_universes + else Univ.Instance.empty + in { cb with - const_body = Def (Declarations.from_val (mkConst con)); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) - } + const_body = Def (Mod_subst.from_val (mkConstU (con,u))); + const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) } 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 "Modops: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 "Modops: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.mod_mp mtb.mod_delta then mtb + else match mtb.mod_type with + |NoFunctor struc -> + let reso',struc' = strengthen_sig mtb.mod_mp struc mp mtb.mod_delta in + { mtb with + mod_type = NoFunctor struc'; + mod_delta = + add_delta_resolver mtb.mod_delta + (add_mp_delta_resolver mtb.mod_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 + let constants = inline_of_delta inl mtb.mod_delta in let rec make_inline delta = function | [] -> delta | (lev,kn)::r -> @@ -381,7 +398,7 @@ let inline_delta_resolver env inl mp mbid mtb delta = match constant.const_body with | Undef _ | OpaqueDef _ -> l | Def body -> - let constr = Declarations.force body in + let constr = Mod_subst.force_constr body in add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> error_no_such_label_sub (con_label con) @@ -389,198 +406,209 @@ 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 = - 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 "Modops:the evaluation of the structure failed " - -and strengthen_and_subst_struct - str subst mp_alias mp_from mp_to alias incl resolver = +let rec strengthen_and_subst_mod mb subst mp_from mp_to = + match mb.mod_type with + |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 = make_kn mp_from empty_dirpath l in - let kn_to = make_kn mp_to empty_dirpath 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 item' = l,SFBmind (subst_mind_body subst mib) 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 = make_kn mp_from empty_dirpath l in - let kn_to = make_kn mp_to empty_dirpath 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 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 - 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 in - (add_mp_delta_resolver - mp_to' mp_to' resolve_out),(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 "Modops:the evaluation of the structure failed " - + let mty = subst_modtype subst' + (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver) + mty + in + 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: + "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 + |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)*) + 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 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 = NoFunctor struc'; + mod_expr = Algebraic (NoFunctor (MEident mb.mod_mp)); + mod_delta = + 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 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 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 subst = map_mp mtb.mod_mp mp empty_delta_resolver in + let new_delta = subst_dom_codom_delta_resolver subst mtb.mod_delta in + let full_subst = map_mp mtb.mod_mp mp new_delta in + subst_modtype full_subst do_delta_dom_codom mtb + +(** {6 Cleaning a module expression from bounded parts } + + For instance: + functor(X:T)->struct module M:=X end) + becomes: + functor(X:T)->struct module M:= 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 && sig_clean = sigt.typ_expr then - 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 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 = Util.list_smartmap (clean_struct l) str in - if str_clean == str then s else SEBstruct(str_clean) - | _ -> anomaly "Modops: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_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_module l) (clean_structure l) + +and clean_expression l = + functor_smartmap (clean_module 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 } *) +let join_constant_body except otab cb = + match cb.const_body with + | OpaqueDef o -> + (match Opaqueproof.uuid_opaque otab o with + | Some uuid when not(Future.UUIDSet.mem uuid except) -> + Opaqueproof.join_opaque otab o + | _ -> ()) + | _ -> () + +let join_structure except otab s = + 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_field (l,body) = match body with + |SFBconst sb -> join_constant_body except otab sb + |SFBmind _ -> () + |SFBmodule m |SFBmodtype m -> join_module m + and join_structure struc = List.iter join_field struc + and join_signature sign = + functor_iter join_module join_structure sign + and join_expression me = functor_iter join_module (fun _ -> ()) me in + join_structure s + -- cgit v1.2.3