summaryrefslogtreecommitdiff
path: root/kernel/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/modops.ml')
-rw-r--r--kernel/modops.ml786
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