From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- kernel/modops.ml | 529 ++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 365 insertions(+), 164 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index fb00cfcd..9242a757 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 9980 2007-07-12 13:32:37Z soubiran $ i*) +(*i $Id: modops.ml 11142 2008-06-18 15:37:31Z soubiran $ i*) (*i*) open Util @@ -20,7 +20,6 @@ open Entries open Mod_subst (*i*) -exception Circularity of string let error_existing_label l = error ("The label "^string_of_label l^" is already declared") @@ -33,11 +32,10 @@ let error_not_a_functor _ = error "Application of not a functor" let error_incompatible_modtypes _ _ = error "Incompatible module types" -let error_not_equal p1 p2 = error ((string_of_mp p1)^" and "^(string_of_mp p2)^" are not equal modules") +let error_not_equal _ _ = error "Not equal modules" + +let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match") -let error_not_match l l1 l2 = error (l1^" is not a subtype of "^l2^": "^ - "Signature components for label "^(string_of_label l)^" do not match.") - let error_no_such_label l = error ("No such label "^string_of_label l) let error_incompatible_labels l l' = @@ -83,140 +81,332 @@ let error_local_context lo = error ("The local context of the component "^ (string_of_label l)^" is not empty") -let error_circular_with_module l = - error ("The construction \"with Module "^(string_of_id l)^":=...\" is about to create\na circular module type. Their resolution is not implemented yet.\nIf you really need that feature, please report.") - -let error_circularity_in_subtyping l l1 l2 = - error ("An occurrence of "^l^" creates a circularity\n during the subtyping verification between "^l1^" and "^l2^".") let error_no_such_label_sub l l1 l2 = - error (l1^" is not a subtype of "^l2^":"^"The field "^(string_of_label l)^" is missing in "^l1^".") + error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".") -let rec scrape_modtype env = function - | MTBident kn -> scrape_modtype env (lookup_modtype kn env) - | mtb -> mtb -(* the constraints are not important here *) -let module_body_of_spec msb = - { mod_type = msb.msb_modtype; - mod_equiv = msb.msb_equiv; - mod_expr = None; - mod_user_type = None; - mod_constraints = Constraint.empty} - -let module_body_of_type mtb = - { mod_type = mtb; - mod_equiv = None; - mod_expr = None; - mod_user_type = None; - mod_constraints = Constraint.empty} +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." -(* the constraints are not important here *) -let module_spec_of_body mb = - { msb_modtype = mb.mod_type; - msb_equiv = mb.mod_equiv; - msb_constraints = Constraint.empty} +let destr_functor env mtb = + match mtb with + | SEBfunctor (arg_id,arg_t,body_t) -> + (arg_id,arg_t,body_t) + | _ -> error_not_a_functor mtb +(* the constraints are not important here *) -let destr_functor = function - | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) - | mtb -> error_not_a_functor mtb - -exception Not_equiv_path +let module_body_of_type mtb = + { mod_type = Some mtb.typ_expr; + mod_expr = None; + mod_constraints = Constraint.empty; + mod_alias = mtb.typ_alias; + mod_retroknowledge = []} + +let module_type_of_module mp mb = + {typ_expr = + (match mb.mod_type with + | Some expr -> expr + | None -> (match mb.mod_expr with + | Some expr -> expr + | None -> + anomaly "Modops: empty expr and type")); + typ_alias = mb.mod_alias; + typ_strength = mp + } let rec check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else - let mb1 = lookup_module mp1 env in - match mb1.mod_equiv with - | None -> - let mb2 = lookup_module mp2 env in - (match mb2.mod_equiv with - | None -> raise Not_equiv_path - | Some mp2' -> check_modpath_equiv env mp2' mp1) - | Some mp1' -> check_modpath_equiv env mp2 mp1' - - -let rec subst_modtype sub = function - (* This is the case in which I am substituting a whole module. - For instance "Module M(X). Module N := X. End M". When I apply - M to M' I must substitute M' for X in "Module N := X". *) - | MTBident ln -> MTBident (subst_kn sub ln) - | MTBfunsig (arg_id, arg_b, body_b) -> - if occur_mbid arg_id sub then raise (Circularity (string_of_mbid arg_id)); - MTBfunsig (arg_id, - subst_modtype sub arg_b, - subst_modtype sub body_b) - | MTBsig (sid1, msb) -> - if occur_msid sid1 sub then raise (Circularity (string_of_msid sid1)); - MTBsig (sid1, subst_signature sub msb) - -and subst_signature sub sign = - let subst_body = function - SPBconst cb -> - SPBconst (subst_const_body sub cb) - | SPBmind mib -> - SPBmind (subst_mind sub mib) - | SPBmodule mb -> - SPBmodule (subst_module sub mb) - | SPBmodtype mtb -> - SPBmodtype (subst_modtype sub mtb) + 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 subst_with_body sub = function + | With_module_body(id,mp,cst) -> + With_module_body(id,subst_mp sub mp,cst) + | With_definition_body(id,cb) -> + With_definition_body( id,subst_const_body sub cb) + +let rec subst_modtype sub mtb = + let typ_expr' = subst_struct_expr sub mtb.typ_expr in + if typ_expr'==mtb.typ_expr then + mtb + else + { mtb with + typ_expr = typ_expr'} + +and subst_structure sub 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) + | SFBmodtype mtb -> + SFBmodtype (subst_modtype sub mtb) + | SFBalias (mp,cst) -> + SFBalias (subst_mp sub mp,cst) in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub mb = - let mtb' = subst_modtype sub mb.msb_modtype in +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 mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in - if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else - { msb_modtype=mtb'; - msb_equiv=mpo'; - msb_constraints=mb.msb_constraints} + 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 + 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) + | SEBapply (meb1,meb2,cst)-> + SEBapply(subst_struct_expr sub meb1, + subst_struct_expr sub meb2, + cst) + | SEBwith (meb,wdb)-> + SEBwith(subst_struct_expr sub meb, + subst_with_body sub wdb) + let subst_signature_msid msid mp = - subst_signature (map_msid msid mp) + subst_structure (map_msid msid mp) + +(* 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 = + 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)) + | _ -> anomaly "Modops.add_retroknowledge: 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 + time this comment is being written, the only relevent instance) the + 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 + tail recursivity, but the world will have exploded before any module + imports 10 000 retroknowledge registration.*) + List.fold_right subst_and_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)} -(* we assume that the substitution of "mp" into "msid" is already done -(or unnecessary) *) -let rec add_signature mp sign env = + +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 sub_alias1 = update_subst sub_alias + (map_mbid farg_id mp (None)) in + let resolve = resolver_of_environment farg_id farg_b mp sub_alias env 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 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,cst) -> + let mp' = scrape_alias mp env in + let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in + SFBalias (mp,Some cst), + Some(join (map_mp (mp_rec [id]) mp') new_alias) + | With_definition_body (_::_,_) + | With_module_body (_::_,_,_) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) + 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,cst) -> + let mp' = scrape_alias mp env in + With_module_body (idl,mp,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 + 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 add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in let con = make_con mp empty_dirpath l in match elem with - | SPBconst cb -> Environ.add_constant con cb env - | SPBmind mib -> Environ.add_mind kn mib env - | SPBmodule mb -> - add_module (MPdot (mp,l)) (module_body_of_spec mb) env - (* adds components as well *) - | SPBmodtype mtb -> Environ.add_modtype kn mtb env + | 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 + (* 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 in List.fold_left add_one env sign - and add_module mp mb env = let env = Environ.shallow_add_module mp mb env in - match scrape_modtype env mb.mod_type with - | MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> - add_signature mp (subst_signature_msid msid mp sign) env - | MTBfunsig _ -> env + 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) + | SEBfunctor _ -> env + | _ -> anomaly "Modops:the evaluation of the structure failed " + -let rec constants_of_specification env mp sign = +and constants_of_specification env mp sign = let aux (env,res) (l,elem) = match elem with - | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res - | SPBmind _ -> env,res - | SPBmodule mb -> - let new_env = add_module (MPdot (mp,l)) (module_body_of_spec mb) env in + | 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,cst) -> + let new_env = register_alias (MPdot (mp,l)) mp1 env in new_env,(constants_of_modtype env (MPdot (mp,l)) - (module_body_of_spec mb).mod_type) @ res - | SPBmodtype mtb -> + (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 @@ -232,87 +422,98 @@ let rec constants_of_specification env mp sign = 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 (make_kn mp empty_dirpath l) mtb env in - new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res + 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 scrape_modtype env modtype with - MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | MTBfunsig _ -> [] - -(* returns a resolver for kn that maps mbid to mp *) -(* Desactivated until v8.2, waiting for the integration -of "Parameter Inline". *) -let resolver_of_environment mbid modtype mp env = - let constants = constants_of_modtype env (MPbound mbid) modtype in - let _ = List.map (fun (con,_) -> con,None) constants in - Mod_subst.make_resolver [] - - -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) - } + 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_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 strengthen_mtb env mp mtb = match scrape_modtype env mtb with - | MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBfunsig _ -> mtb - | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp) - -and strengthen_mod env mp msb = - { msb_modtype = strengthen_mtb env mp msb.msb_modtype; - msb_equiv = begin match msb.msb_equiv with - | Some _ -> msb.msb_equiv - | None -> Some mp - end ; - msb_constraints = msb.msb_constraints; } - +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,SPBconst cb) :: rest -> - let item' = l,SPBconst (strengthen_const env mp l cb) in + | (l,SFBconst cb) :: rest -> + let item' = l,SFBconst (strengthen_const env mp l cb) in let rest' = strengthen_sig env msid rest mp in item'::rest' - | (l,SPBmind mib) :: rest -> - let item' = l,SPBmind (strengthen_mind env mp l mib) in + | (l,SFBmind mib) :: rest -> + let item' = l,SFBmind (strengthen_mind env mp l mib) in let rest' = strengthen_sig env msid rest mp in item'::rest' - | (l,SPBmodule mb) :: rest -> + | (l,SFBmodule mb) :: rest -> let mp' = MPdot (mp,l) in - let item' = l,SPBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) - (module_body_of_spec mb) - env - 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 + 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,SPBmodtype mty as item) :: rest -> + item::rest' + | (l,SFBmodtype mty as item) :: rest -> let env' = add_modtype - (make_kn (MPself msid) empty_dirpath l) + (MPdot((MPself msid),l)) mty env in let rest' = strengthen_sig env' msid rest mp in item::rest' + let strengthen env mtb mp = strengthen_mtb env mp mtb + +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 -- cgit v1.2.3