diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 786 |
1 files changed, 412 insertions, 374 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 34d9e930..b49d34b3 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 12234 2009-07-09 09:14:09Z soubiran $ i*) +(*i $Id$ i*) (*i*) open Util @@ -21,6 +21,7 @@ open Mod_subst (*i*) + let error_existing_label l = error ("The label "^string_of_label l^" is already declared.") @@ -60,6 +61,9 @@ let error_not_a_modtype_loc loc s = let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) +let error_not_a_module_or_modtype_loc loc s = + user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type.")) + let error_not_a_module s = error_not_a_module_loc dummy_loc s let error_not_a_constant l = @@ -82,20 +86,12 @@ let error_local_context lo = (string_of_label l)^" is not empty.") -let error_no_such_label_sub l l1 l2 = - error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".") - +let error_no_such_label_sub l l1 = + error ("The field "^(string_of_label l)^" is missing in "^l1^".") +let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules." -let rec list_split_assoc k rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail - -let path_of_seb = function - | SEBident mp -> mp - | _ -> anomaly "Modops: evaluation failed." - +let error_application_to_module_type _ = error "Module application to a module type." let destr_functor env mtb = match mtb with @@ -103,123 +99,126 @@ let destr_functor env mtb = (arg_id,arg_t,body_t) | _ -> error_not_a_functor mtb -(* the constraints are not important here *) +let is_functor = function + | SEBfunctor (arg_id,arg_t,body_t) -> true + | _ -> false -let module_body_of_type mtb = - { mod_type = Some mtb.typ_expr; +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 = Constraint.empty; - mod_alias = mtb.typ_alias; + mod_constraints = mtb.typ_constraints; + mod_delta = mtb.typ_delta; mod_retroknowledge = []} -let module_type_of_module mp mb = - let mp1,expr = - (match mb.mod_type with - | Some expr -> mp,expr - | None -> (match mb.mod_expr with - | Some (SEBident mp') ->(Some mp'),(SEBident mp') - | Some expr -> mp,expr - | None -> - anomaly "Modops: empty expr and type")) in - {typ_expr = expr; - typ_alias = mb.mod_alias; - typ_strength = mp1 - } - -let rec check_modpath_equiv env mp1 mp2 = +let check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else - let mp1 = scrape_alias mp1 env in - let mp2 = scrape_alias mp2 env in - if mp1=mp2 then () - else - error_not_equal mp1 mp2 + let mb1=lookup_module mp1 env in + let mb2=lookup_module mp2 env in + if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2) + then () + else error_not_equal mp1 mp2 let rec subst_with_body sub = function - | With_module_body(id,mp,typ_opt,cst) -> - With_module_body(id,subst_mp sub mp,Option.smartmap - (subst_struct_expr sub) typ_opt,cst) + | 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 mtb = - let typ_expr' = subst_struct_expr sub mtb.typ_expr in - let sub_mtb = join_alias mtb.typ_alias sub in - if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then - mtb +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_expr = typ_expr'; - typ_alias = sub_mtb} + {mtb with + typ_mp = mp; + typ_expr = typ_expr'; + typ_expr_alg = typ_alg'; + typ_delta = mtb_delta} -and subst_structure sub sign = - let subst_body = function +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 mb) + SFBmodule (subst_module sub do_delta mb) | SFBmodtype mtb -> - SFBmodtype (subst_modtype sub mtb) - | SFBalias (mp,typ_opt,cst) -> - SFBalias (subst_mp sub mp,Option.smartmap - (subst_struct_expr sub) typ_opt,cst) + SFBmodtype (subst_modtype sub do_delta mtb) in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub mb = - let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in - (* This is similar to the previous case. In this case we have - a module M in a signature that is knows to be equivalent to a module M' - (because the signature is "K with Module M := M'") and we are substituting - M' with some M''. *) - let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in - let mb_alias = update_subst sub mb.mod_alias in - let mb_alias = if mb_alias = empty_subst then - join_alias mb.mod_alias sub - else - join mb_alias (join_alias mb.mod_alias sub) - in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mb_alias == mb.mod_alias +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 + 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 - { mod_expr = me'; - mod_type=mtb'; - mod_constraints=mb.mod_constraints; - mod_alias = mb_alias; - mod_retroknowledge=mb.mod_retroknowledge} - - -and subst_struct_expr sub = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (msid, mtb, meb') -> - SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') - | SEBstruct (msid,str)-> - SEBstruct(msid, subst_structure sub str) + { 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 meb1, - subst_struct_expr sub meb2, + SEBapply(subst_struct_expr sub do_delta meb1, + subst_struct_expr sub do_delta meb2, cst) | SEBwith (meb,wdb)-> - SEBwith(subst_struct_expr sub meb, + SEBwith(subst_struct_expr sub do_delta meb, subst_with_body sub wdb) - -let subst_signature_msid msid mp = - subst_structure (map_msid msid mp) +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 the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) -let add_retroknowledge msid mp = - let subst = add_msid msid mp empty_subst in - let subst_and_perform rkaction env = +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 (subst_mps subst (mkConst kn)) - | Ind ind -> kind_of_term (subst_mps subst (mkInd ind)) + | 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") in fun lclrk env -> @@ -231,302 +230,341 @@ let add_retroknowledge msid mp = 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 subst_and_perform lclrk env - - + List.fold_right perform lclrk env -let strengthen_const env mp l cb = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> - let const = mkConst (make_con mp empty_dirpath l) in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false; - const_body_code = Cemitcodes.from_val - (compile_constant_body env const_subs false false) - } - -let strengthen_mind env mp l mib = match mib.mind_equiv with - | Some _ -> mib - | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} - - -let rec eval_struct env = function - | SEBident mp -> - begin - let mtb =lookup_modtype mp env in - match mtb.typ_expr,mtb.typ_strength with - mtb,None -> eval_struct env mtb - | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb) - end - | SEBapply (seb1,seb2,_) -> - let svb1 = eval_struct env seb1 in - let farg_id, farg_b, fbody_b = destr_functor env svb1 in - let mp = path_of_seb seb2 in - let mp = scrape_alias mp env in - let sub_alias = (lookup_modtype mp env).typ_alias in - let sub_alias = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> - join_alias - (subst_key (map_msid msid mp) sub_alias) - (map_msid msid mp) - | _ -> sub_alias in - let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in - let sub_alias1 = update_subst sub_alias - (map_mbid farg_id mp (Some resolve)) in - eval_struct env (subst_struct_expr - (join sub_alias1 - (map_mbid farg_id mp (Some resolve))) fbody_b) - | SEBwith (mtb,(With_definition_body _ as wdb)) -> - let mtb',_ = merge_with env mtb wdb empty_subst in - mtb' - | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) -> - let alias_in_mp = - (lookup_modtype mp env).typ_alias in - let alias_in_mp = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) alias_in_mp - | _ -> alias_in_mp in - let mtb',_ = merge_with env mtb wdb alias_in_mp in - mtb' -(* | SEBfunctor(mbid,mtb,body) -> - let env = add_module (MPbound mbid) (module_body_of_type mtb) env in - SEBfunctor(mbid,mtb,eval_struct env body) *) - | mtb -> mtb - -and type_of_mb env mb = - match mb.mod_type,mb.mod_expr with - None,Some b -> eval_struct env b - | Some t, _ -> eval_struct env t - | _,_ -> anomaly - "Modops: empty type and empty expr" - -and merge_with env mtb with_decl alias= - let msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) -> msid,sig_b - | _ -> error_signature_expected mtb - in - let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false - in - let l = label_of_id id in - try - let rev_before,spec,after = list_split_assoc l [] sig_b in - let before = List.rev rev_before in - let rec mp_rec = function - | [] -> MPself msid - | i::r -> MPdot(mp_rec r,label_of_id i) - in - let env' = add_signature (MPself msid) before env in - let new_spec,subst = match with_decl with - | With_definition_body ([],_) - | With_module_body ([],_,_,_) -> assert false - | With_definition_body ([id],c) -> - SFBconst c,None - | With_module_body ([id], mp,typ_opt,cst) -> - let mp' = scrape_alias mp env' in - let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in - SFBalias (mp,typ_opt,Some cst), - Some(join (map_mp (mp_rec [id]) mp') new_alias) - | With_definition_body (_::_,_) - | With_module_body (_::_,_,_,_) -> - let old,aliasold = match spec with - SFBmodule msb -> Some msb, None - | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst) - | _ -> error_not_a_module (string_of_label l) - in - if aliasold = None then - let old = Option.get old in - let new_with_decl,subst1 = - match with_decl with - With_definition_body (_,c) -> With_definition_body (idl,c),None - | With_module_body (idc,mp,typ_opt,cst) -> - let mp' = scrape_alias mp env' in - With_module_body (idl,mp,typ_opt,cst), - Some(map_mp (mp_rec (List.rev idc)) mp') - in - let subst = match subst1 with - | None -> None - | Some s -> Some (join s (update_subst alias s)) in - let modtype,subst_msb = - merge_with env' (type_of_mb env' old) new_with_decl alias in - let msb = - { mod_expr = None; - mod_type = Some modtype; - mod_constraints = old.mod_constraints; - mod_alias = begin - match subst_msb with - |None -> empty_subst - |Some s -> s - end; - mod_retroknowledge = old.mod_retroknowledge} - in - (SFBmodule msb),subst - else - let mpold,typ_opt,cst = Option.get aliasold in - SFBalias (mpold,typ_opt,cst),None - in - SEBstruct(msid, before@(l,new_spec):: - (Option.fold_right subst_structure subst after)),subst - with - Not_found -> error_no_such_label l - -and add_signature mp sign env = +let rec add_signature mp sign resolver env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in - let con = make_con mp empty_dirpath l in + let con = constant_of_kn kn in + let mind = mind_of_kn kn in match elem with - | SFBconst cb -> Environ.add_constant con cb env - | SFBmind mib -> Environ.add_mind kn mib env - | SFBmodule mb -> - add_module (MPdot (mp,l)) mb env + | SFBconst cb -> + let con = constant_of_delta resolver con in + Environ.add_constant con cb env + | SFBmind mib -> + let mind = mind_of_delta resolver mind in + Environ.add_mind mind mib env + | SFBmodule mb -> add_module mb env (* adds components as well *) - | SFBalias (mp1,_,cst) -> - Environ.register_alias (MPdot(mp,l)) mp1 env - | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) - mtb env + | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env in List.fold_left add_one env sign -and add_module mp mb env = +and add_module mb env = + let mp = mb.mod_mp in let env = Environ.shallow_add_module mp mb env in - let env = - Environ.add_modtype mp (module_type_of_module (Some mp) mb) env - in - let mod_typ = type_of_mb env mb in - match mod_typ with - | SEBstruct (msid,sign) -> - add_retroknowledge msid mp (mb.mod_retroknowledge) - (add_signature mp (subst_signature_msid msid mp sign) env) + 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 " - - -and constants_of_specification env mp sign = - let aux (env,res) (l,elem) = - match elem with - | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res - | SFBmind _ -> env,res - | SFBmodule mb -> - let new_env = add_module (MPdot (mp,l)) mb env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (type_of_mb env mb)) @ res - | SFBalias (mp1,typ_opt,cst) -> - let new_env = register_alias (MPdot (mp,l)) mp1 env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (eval_struct env (SEBident mp1))) @ res - | SFBmodtype mtb -> - (* module type dans un module type. - Il faut au moins mettre mtb dans l'environnement (avec le bon - kn pour pouvoir continuer aller deplier les modules utilisant ce - mtb - ex: - Module Type T1. - Module Type T2. - .... - End T2. - ..... - Declare Module M : T2. - End T2 - si on ne rajoute pas T2 dans l'environement de typage - on va exploser au moment du Declare Module - *) - let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in - new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res - in - snd (List.fold_left aux (env,[]) sign) - -and constants_of_modtype env mp modtype = - match (eval_struct env modtype) with - SEBstruct (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | SEBfunctor _ -> [] - | _ -> anomaly "Modops:the evaluation of the structure failed " - -(* returns a resolver for kn that maps mbid to mp. We only keep - constants that have the inline flag *) -and resolver_of_environment mbid modtype mp alias env = - let constants = constants_of_modtype env (MPbound mbid) modtype.typ_expr in - let constants = List.map (fun (l,cb) -> (l,subst_const_body alias cb)) constants in - let rec make_resolve = function - | [] -> [] - | (con,expecteddef)::r -> - let con' = replace_mp_in_con (MPbound mbid) mp con in - let con',_ = subst_con alias con' in - (* let con' = replace_mp_in_con (MPbound mbid) mp con' in *) - try - if expecteddef.Declarations.const_inline then - let constant = lookup_constant con' env in - if (not constant.Declarations.const_opaque) then - let constr = Option.map Declarations.force - constant.Declarations.const_body in - (con,constr)::(make_resolve r) - else make_resolve r - else make_resolve r - with Not_found -> error_no_such_label (con_label con') - in - let resolve = make_resolve constants in - Mod_subst.make_resolver resolve +let strengthen_const env mp_from l cb resolver = + match cb.const_opaque, cb.const_body with + | false, Some _ -> cb + | true, Some _ + | _, None -> + let con = make_con mp_from empty_dirpath l in + let con = constant_of_delta resolver con in + let const = mkConst con in + let const_subs = Some (Declarations.from_val const) in + {cb with + const_body = const_subs; + const_opaque = false; + const_body_code = Cemitcodes.from_val + (compile_constant_body env const_subs false false) + } + +let rec strengthen_mod env 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 env 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 env mp_from sign mp_to resolver = + match sign with + | [] -> empty_delta_resolver,[] + | (l,SFBconst cb) :: rest -> + let item' = + l,SFBconst (strengthen_const env mp_from l cb resolver) in + let resolve_out,rest' = + strengthen_sig env mp_from rest mp_to resolver in + resolve_out,item'::rest' + | (_,SFBmind _ as item):: rest -> + let resolve_out,rest' = + strengthen_sig env 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 env mp_from' mp_to' mb in + let item' = l,SFBmodule (mb_out) in + let env' = add_module mb_out env in + let resolve_out,rest' = + strengthen_sig env' mp_from rest mp_to resolver in + add_delta_resolver resolve_out mb.mod_delta, + item':: rest' + | (l,SFBmodtype mty as item) :: rest -> + let env' = add_modtype + (MPdot(mp_from,l)) mty env + in + let resolve_out,rest' = + strengthen_sig env' mp_from rest mp_to resolver in + resolve_out,item::rest' -and strengthen_mtb env mp mtb = - let mtb1 = eval_struct env mtb in - match mtb1 with - | SEBfunctor _ -> mtb1 - | SEBstruct (msid,sign) -> - SEBstruct (msid,strengthen_sig env msid sign mp) - | _ -> anomaly "Modops:the evaluation of the structure failed " - -and strengthen_mod env mp mb = - let mod_typ = type_of_mb env mb in - { mod_expr = mb.mod_expr; - mod_type = Some (strengthen_mtb env mp mod_typ); - mod_constraints = mb.mod_constraints; - mod_alias = mb.mod_alias; - mod_retroknowledge = mb.mod_retroknowledge} - -and strengthen_sig env msid sign mp = match sign with - | [] -> [] - | (l,SFBconst cb) :: rest -> - let item' = l,SFBconst (strengthen_const env mp l cb) in - let rest' = strengthen_sig env msid rest mp in +let strengthen env 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 env 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 env mp mb = + match mp with + Some mp -> + strengthen env { + 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} + +let complete_inline_delta_resolver env mp mbid mtb delta = + let constants = inline_of_delta mtb.typ_delta in + let rec make_inline delta = function + | [] -> delta + | kn::r -> + let kn = replace_mp_in_kn (MPbound mbid) mp kn in + let con = constant_of_kn kn in + let con' = constant_of_delta delta con in + try + let constant = lookup_constant con' env in + if (not constant.Declarations.const_opaque) then + let constr = Option.map Declarations.force + constant.Declarations.const_body in + if constr = None then + (make_inline delta r) + else + add_inline_constr_delta_resolver con (Option.get constr) + (make_inline delta r) + else + (make_inline delta r) + with + Not_found -> error_no_such_label_sub (con_label con) + (string_of_mp (con_modpath con)) + in + make_inline delta constants + +let rec strengthen_and_subst_mod + mb subst env mp_from mp_to env 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 env + 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 env mp_alias mp_from mp_to alias incl resolver = + match str with + | [] -> empty_delta_resolver,[] + | (l,SFBconst cb) :: rest -> + let item' = if alias then + l,SFBconst (subst_const_body subst cb) + else + l,SFBconst (strengthen_const env mp_from l + (subst_const_body subst cb) resolver) + in + let con = make_con mp_from empty_dirpath l in + let resolve_out,rest' = + strengthen_and_subst_struct rest subst env + mp_alias mp_from mp_to alias incl resolver in + if incl then + let old_name = constant_of_delta resolver con in + (add_constant_delta_resolver + (constant_of_kn_equiv (make_kn mp_to empty_dirpath l) + (canonical_con old_name)) + resolve_out), item'::rest' - | (l,SFBmind mib) :: rest -> - let item' = l,SFBmind (strengthen_mind env mp l mib) in - let rest' = strengthen_sig env msid rest mp in + else + resolve_out,item'::rest' + | (l,SFBmind mib) :: rest -> + let item' = l,SFBmind (subst_mind subst mib) in + let mind = make_mind mp_from empty_dirpath l in + let resolve_out,rest' = + strengthen_and_subst_struct rest subst env + mp_alias mp_from mp_to alias incl resolver in + if incl then + let old_name = mind_of_delta resolver mind in + (add_mind_delta_resolver + (mind_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_mind old_name)) resolve_out), item'::rest' - | (l,SFBmodule mb) :: rest -> - let mp' = MPdot (mp,l) in - let item' = l,SFBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) mb env in - let rest' = strengthen_sig env' msid rest mp in + else + 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 = if alias then + subst_module subst + (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb + else + strengthen_and_subst_mod + mb subst env mp_from' mp_to' env resolver + in + let item' = l,SFBmodule (mb_out) in + let env' = add_module mb_out env in + let resolve_out,rest' = + strengthen_and_subst_struct rest subst env' + mp_alias mp_from mp_to alias incl resolver in + 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,SFBalias (mp1,_,cst)) as item) :: rest -> - let env' = register_alias (MPdot(MPself msid,l)) mp1 env in - let rest' = strengthen_sig env' msid rest mp in - item::rest' - | (l,SFBmodtype mty as item) :: rest -> - let env' = add_modtype - (MPdot((MPself msid),l)) - mty - env - in - let rest' = strengthen_sig env' msid rest mp in - 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 env' = add_modtype mp_from' mty env in + let resolve_out,rest' = strengthen_and_subst_struct rest subst env' + 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 strengthen env mtb mp = strengthen_mtb env mp mtb +let strengthen_and_subst_mb mb mp env 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 is an alias then the strengthening is useless + (i.e. it is already done)*) + let mp_alias = delta_of_mp 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 env + 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 update_subst env mb mp = - match type_of_mb env mb with - | SEBstruct(msid,str) -> false, join_alias - (subst_key (map_msid msid mp) mb.mod_alias) - (map_msid msid mp) - | _ -> true, mb.mod_alias +let subst_modtype_and_resolver mtb mp env = + 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 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 + | _ -> 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 |