diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cemitcodes.ml | 4 | ||||
| -rw-r--r-- | kernel/mod_subst.ml | 224 | ||||
| -rw-r--r-- | kernel/mod_subst.mli | 38 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 7 | ||||
| -rw-r--r-- | kernel/mod_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 53 | ||||
| -rw-r--r-- | kernel/modops.mli | 3 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 4 |
8 files changed, 260 insertions, 75 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 8e31f59761..cccb184433 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -255,7 +255,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -267,7 +267,7 @@ type body_code = let subst_body_code s = function | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) - | BCallias kn -> BCallias (subst_con s kn) + | BCallias kn -> BCallias (fst (subst_con s kn)) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 48bb9933ce..e0d16d4995 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -13,6 +13,20 @@ open Util open Names open Term +(* WARNING: not every constant in the associative list domain used to exist + in the environment. This allows a simple implementation of the join + operation. However, iterating over the associative list becomes a non-sense +*) +type resolver = (constant * constr option) list + +let make_resolver resolve = resolve + +let apply_opt_resolver resolve kn = + match resolve with + None -> None + | Some resolve -> + try List.assoc kn resolve with Not_found -> assert false + type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id let string_of_subst_domain = function @@ -24,21 +38,21 @@ module Umap = Map.Make(struct let compare = Pervasives.compare end) -(* this is correct under the condition that bound and struct - identifiers can never be identical (i.e. get the same stamp)! *) - -type substitution = module_path Umap.t +type substitution = (module_path * resolver option) Umap.t let empty_subst = Umap.empty -let add_msid sid = Umap.add (MSI sid) -let add_mbid bid = Umap.add (MBI bid) +let add_msid msid mp = + Umap.add (MSI msid) (mp,None) +let add_mbid mbid mp resolve = + let mp' = MBI mbid in + Umap.add (MBI mbid) (mp,resolve) let map_msid msid mp = add_msid msid mp empty_subst -let map_mbid mbid mp = add_mbid mbid mp empty_subst +let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst let list_contents sub = - let one_pair uid mp l = + let one_pair uid (mp,_) l = (string_of_subst_domain uid, string_of_mp mp)::l in Umap.fold one_pair sub [] @@ -53,22 +67,155 @@ let debug_pr_subst sub = in str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" -let rec subst_mp sub mp = (* 's like subst *) +let subst_mp0 sub mp = (* 's like subst *) + let rec aux mp = match mp with | MPself sid -> - (try Umap.find (MSI sid) sub with Not_found -> mp) + let mp',resolve = Umap.find (MSI sid) sub in + mp',resolve | MPbound bid -> - (try Umap.find (MBI bid) sub with Not_found -> mp) + let mp',resolve = Umap.find (MBI bid) sub in + mp',resolve + | MPdot (mp1,l) -> + let mp1',resolve = aux mp1 in + MPdot (mp1',l),resolve + | _ -> raise Not_found + in + try Some (aux mp) with Not_found -> None + +let subst_mp sub mp = + match subst_mp0 sub mp with + None -> mp + | Some (mp',_) -> mp' + + +let subst_kn0 sub kn = + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',_) -> + Some (make_kn mp' dir l) + | None -> None + +let subst_kn sub kn = + match subst_kn0 sub kn with + None -> kn + | Some kn' -> kn' + +let subst_con sub con = + let mp,dir,l = repr_con con in + match subst_mp0 sub mp with + None -> con,mkConst con + | Some (mp',resolve) -> + let con' = make_con mp' dir l in + match apply_opt_resolver resolve con with + None -> con',mkConst con' + | Some t -> con',t + +(* Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) +let subst_evaluable_reference subst = function + | EvalVarRef id -> EvalVarRef id + | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn)) + +(* +This should be rewritten to prevent duplication of constr's when not +necessary. +For now, it uses map_constr and is rather ineffective +*) + +let rec map_kn f f' c = + let func = map_kn f f' in + match kind_of_term c with + | Const kn -> f' kn + | Ind (kn,i) -> + (match f kn with + None -> c + | Some kn' -> + mkInd (kn',i)) + | Construct ((kn,i),j) -> + (match f kn with + None -> c + | Some kn' -> + mkConstruct ((kn',i),j)) + | Case (ci,p,c,l) -> + let ci' = + { ci with + ci_ind = + let (kn,i) = ci.ci_ind in + match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in + mkCase (ci', func p, func c, array_smartmap func l) + | _ -> map_constr func c + +let subst_mps sub = + map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con)) + +let rec replace_mp_in_mp mpfrom mpto mp = + match mp with + | _ when mp = mpfrom -> mpto | MPdot (mp1,l) -> - let mp1' = subst_mp sub mp1 in - if mp1==mp1' then - mp - else - MPdot (mp1',l) + let mp1' = replace_mp_in_mp mpfrom mpto mp1 in + if mp1==mp1' then mp + else MPdot (mp1',l) | _ -> mp -let join subst1 subst2 = - let subst = Umap.map (subst_mp subst2) subst1 in +let replace_mp_in_con mpfrom mpto kn = + let mp,dir,l = repr_con kn in + let mp'' = replace_mp_in_mp mpfrom mpto mp in + if mp==mp'' then kn + else make_con mp'' dir l + +exception BothSubstitutionsAreIdentitySubstitutions +exception ChangeDomain of resolver + +let join (subst1 : substitution) (subst2 : substitution) = + let apply_subst (sub : substitution) key (mp,resolve) = + let mp',resolve' = + match subst_mp0 sub mp with + None -> mp, None + | Some (mp',resolve') -> mp',resolve' in + let resolve'' : resolver option = + try + let res = + match resolve with + Some res -> res + | None -> + match resolve' with + None -> raise BothSubstitutionsAreIdentitySubstitutions + | Some res -> raise (ChangeDomain res) + in + Some + (List.map + (fun (kn,topt) -> + kn, + match topt with + None -> + (match key with + MSI msid -> + let kn' = replace_mp_in_con (MPself msid) mp kn in + apply_opt_resolver resolve' kn' + | MBI mbid -> + let kn' = replace_mp_in_con (MPbound mbid) mp kn in + apply_opt_resolver resolve' kn') + | Some t -> Some (subst_mps sub t)) res) + with + BothSubstitutionsAreIdentitySubstitutions -> None + | ChangeDomain res -> + Some + ((List.map + (fun (kn,topt) -> + let key' = + match key with + MSI msid -> MPself msid + | MBI mbid -> MPbound mbid in + (* let's replace mp with key in kn *) + let kn' = replace_mp_in_con mp key' kn in + kn',topt)) res) + in + mp',resolve'' in + let subst = Umap.mapi (apply_subst subst2) subst1 in Umap.fold Umap.add subst2 subst let rec occur_in_path uid path = @@ -79,7 +226,7 @@ let rec occur_in_path uid path = | _ -> false let occur_uid uid sub = - let check_one uid' mp = + let check_one uid' (mp,_) = if uid = uid' || occur_in_path uid mp then raise Exit in try @@ -112,42 +259,3 @@ let subst_substituted s r = | LSlazy(s',a) -> let s'' = join s' s in ref (LSlazy(s'',a)) - -let subst_kn sub kn = - let mp,dir,l = repr_kn kn in - let mp' = subst_mp sub mp in - if mp==mp' then kn else make_kn mp' dir l - -let subst_con sub con = - let mp,dir,l = repr_con con in - let mp' = subst_mp sub mp in - if mp==mp' then con else make_con mp' dir l - -let subst_evaluable_reference subst = function - | EvalVarRef id -> EvalVarRef id - | EvalConstRef kn -> EvalConstRef (subst_con subst kn) - -(* -map_kn : (kernel_name -> kernel_name) -> constr -> constr - -This should be rewritten to prevent duplication of constr's when not -necessary. -For now, it uses map_constr and is rather ineffective -*) - -let rec map_kn f f_con c = - let func = map_kn f f_con in - match kind_of_term c with - | Const kn -> - mkConst (f_con kn) - | Ind (kn,i) -> - mkInd (f kn,i) - | Construct ((kn,i),j) -> - mkConstruct ((f kn,i),j) - | Case (ci,p,c,l) -> - let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in - mkCase (ci', func p, func c, array_smartmap func l) - | _ -> map_constr func c - -let subst_mps sub = - map_kn (subst_kn sub) (subst_con sub) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index f4003c7f95..89491e2f91 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -8,22 +8,27 @@ (*i $Id$ i*) +(*s Mod_subst *) + open Names open Term -(*s Substitutions *) - +type resolver type substitution +val make_resolver : (constant * constr option) list -> resolver + val empty_subst : substitution val add_msid : mod_self_id -> module_path -> substitution -> substitution val add_mbid : - mod_bound_id -> module_path -> substitution -> substitution + mod_bound_id -> module_path -> resolver option -> substitution -> substitution -val map_msid : mod_self_id -> module_path -> substitution -val map_mbid : mod_bound_id -> module_path -> substitution +val map_msid : + mod_self_id -> module_path -> substitution +val map_mbid : + mod_bound_id -> module_path -> resolver option -> substitution (* sequential composition: [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] @@ -47,18 +52,29 @@ val debug_pr_subst : substitution -> Pp.std_ppcmds val subst_mp : substitution -> module_path -> module_path -(* [occur_*id id sub] returns true iff [id] occurs in [sub] - on either side *) +val subst_kn : + substitution -> kernel_name -> kernel_name -val occur_msid : mod_self_id -> substitution -> bool -val occur_mbid : mod_bound_id -> substitution -> bool +val subst_con : + substitution -> constant -> constant * constr -val subst_kn : substitution -> kernel_name -> kernel_name -val subst_con : substitution -> constant -> constant +(* Here the semantics is completely unclear. + What does "Hint Unfold t" means when "t" is a parameter? + Does the user mean "Unfold X.t" or does she mean "Unfold y" + where X.t is later on instantiated with y? I choose the first + interpretation (i.e. an evaluable reference is never expanded). *) val subst_evaluable_reference : substitution -> evaluable_global_reference -> evaluable_global_reference +(* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *) +val replace_mp_in_con : module_path -> module_path -> constant -> constant (* [subst_mps sub c] performs the substitution [sub] on all kernel names appearing in [c] *) val subst_mps : substitution -> constr -> constr + +(* [occur_*id id sub] returns true iff [id] occurs in [sub] + on either side *) + +val occur_msid : mod_self_id -> substitution -> bool +val occur_mbid : mod_bound_id -> substitution -> bool diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 0001a6c5ed..1d63486ba1 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -259,8 +259,13 @@ and translate_mexpr env mexpr = match mexpr with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) in + let resolve = Modops.resolver_of_environment farg_id farg_b mp env in MEBapply(feb,meb,cst), - subst_modtype (map_mbid farg_id mp) fbody_b + (* This is the place where the functor formal parameter is + substituted by the given argument to compute the type of the + functor application. *) + subst_modtype + (map_mbid farg_id mp (Some resolve)) fbody_b | MEstruct (msid,structure) -> let structure,signature = translate_entry_list env msid true structure in MEBstruct (msid,structure), diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 73dc914819..cfcc7bd585 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -19,6 +19,8 @@ val translate_modtype : env -> module_type_entry -> module_type_body val translate_module : env -> module_entry -> module_body +val translate_mexpr : env -> module_expr -> module_expr_body * module_type_body + val add_modtype_constraints : env -> module_type_body -> env val add_module_constraints : env -> module_body -> env diff --git a/kernel/modops.ml b/kernel/modops.ml index 0a18978327..2808973fa6 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -124,6 +124,9 @@ let rec check_modpath_equiv env mp1 mp2 = 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 failwith "capture"; @@ -149,16 +152,62 @@ and subst_signature sub sign = and subst_module sub mb = let mtb' = subst_modtype sub mb.msb_modtype 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 subst_signature_msid msid mp = subst_signature (map_msid msid mp) +let rec constants_of_specification env mp sign = + let aux res (l,elem) = + match elem with + | SPBconst cb -> (make_con mp empty_dirpath l)::res + | SPBmind _ -> res + | SPBmodule mb -> + (constants_of_modtype env (MPdot (mp,l)) + (module_body_of_spec mb).mod_type) @ res + | SPBmodtype mtb -> res (* ???? *) + in + List.fold_left aux [] 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 and then delta-expands + the obtained constants according to env *) +let resolver_of_environment mbid modtype mp env = + let constants = constants_of_modtype env (MPbound mbid) modtype in + let resolve = + List.map + (fun con -> + let con' = replace_mp_in_con (MPbound mbid) mp con in + let constr = + try + let constant = lookup_constant con' env in + if constant.Declarations.const_opaque then + None + else + option_app Declarations.force + constant.Declarations.const_body + with Not_found -> assert false + in + con,constr + ) constants + in + Mod_subst.make_resolver resolve + (* we assume that the substitution of "mp" into "msid" is already done (or unnecessary) *) let rec add_signature mp sign env = @@ -182,7 +231,6 @@ and add_module mp mb env = | MTBident _ -> anomaly "scrape_modtype does not work!" | MTBsig (msid,sign) -> add_signature mp (subst_signature_msid msid mp sign) env - | MTBfunsig _ -> env @@ -247,3 +295,4 @@ and strengthen_sig env msid sign mp = match sign with item::rest' let strengthen env mtb mp = strengthen_mtb env mp mtb + diff --git a/kernel/modops.mli b/kernel/modops.mli index 0e1d9cd34a..e770edc93e 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -95,3 +95,6 @@ val error_with_incorrect : label -> 'a val error_local_context : label option -> 'a val error_circular_with_module : identifier -> 'a + +val resolver_of_environment : + mod_bound_id -> module_type_body -> module_path -> env -> resolver diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 383f7c2c95..9f03b57c5d 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -249,8 +249,10 @@ and check_modtypes cst env mtb1 mtb2 equiv = add_module (MPbound arg_id2) (module_body_of_type arg_t2) env in let body_t1' = + (* since we are just checking well-typedness we do not need + to expand any constant. Hence the identity resolver. *) subst_modtype - (map_mbid arg_id1 (MPbound arg_id2)) + (map_mbid arg_id1 (MPbound arg_id2) None) body_t1 in check_modtypes cst env' body_t1' body_t2 equiv |