diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /kernel/mod_typing.ml | |
parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'kernel/mod_typing.ml')
-rw-r--r-- | kernel/mod_typing.ml | 67 |
1 files changed, 52 insertions, 15 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 5e8c7001..a8aff184 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.ml,v 1.11.2.1 2004/07/16 19:30:26 herbelin Exp $ i*) +(*i $Id: mod_typing.ml 7639 2005-12-02 10:01:15Z gregoire $ i*) open Util open Names @@ -17,6 +17,7 @@ open Environ open Term_typing open Modops open Subtyping +open Mod_subst exception Not_path @@ -65,8 +66,9 @@ and merge_with env mtb with_decl = | MTBsig(msid,sig_b) -> msid,sig_b | _ -> error_signature_expected mtb in - let id = match with_decl with - | With_Definition (id,_) | With_Module (id,_) -> id + let id,idl = match with_decl with + | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl + | With_Definition ([],_) | With_Module ([],_) -> assert false in let l = label_of_id id in try @@ -74,7 +76,9 @@ and merge_with env mtb with_decl = let before = List.rev rev_before in let env' = Modops.add_signature (MPself msid) before env in let new_spec = match with_decl with - | With_Definition (id,c) -> + | With_Definition ([],_) + | With_Module ([],_) -> assert false + | With_Definition ([id],c) -> let cb = match spec with SPBconst cb -> cb | _ -> error_not_a_constant l @@ -88,21 +92,25 @@ and merge_with env mtb with_decl = let cst = Constraint.union (Constraint.union cb.const_constraints cst1) - cst2 - in + cst2 in + let body = Some (Declarations.from_val j.uj_val) in SPBconst {cb with - const_body = - Some (Declarations.from_val j.uj_val); - const_constraints = cst} + const_body = body; + const_body_code = Cemitcodes.from_val + (compile_constant_body env' body false false); + const_constraints = cst} | Some b -> let cst1 = Reduction.conv env' c (Declarations.force b) in let cst = Constraint.union cb.const_constraints cst1 in + let body = Some (Declarations.from_val c) in SPBconst {cb with - const_body = Some (Declarations.from_val c); - const_constraints = cst} + const_body = body; + const_body_code = Cemitcodes.from_val + (compile_constant_body env' body false false); + const_constraints = cst} end (* and what about msid's ????? Don't they clash ? *) - | With_Module (id, mp) -> + | With_Module ([id], mp) -> let old = match spec with SPBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) @@ -133,6 +141,29 @@ and merge_with env mtb with_decl = msb_constraints = Constraint.union old.msb_constraints cst } in SPBmodule msb + | With_Definition (_::_,_) + | With_Module (_::_,_) -> + let old = match spec with + SPBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) + in + begin + match old.msb_equiv with + None -> + let new_with_decl = match with_decl with + With_Definition (_,c) -> With_Definition (idl,c) + | With_Module (_,c) -> With_Module (idl,c) in + let modtype = + merge_with env' old.msb_modtype new_with_decl in + let msb = + {msb_modtype = modtype; + msb_equiv = None; + msb_constraints = old.msb_constraints } + in + SPBmodule msb + | Some mp -> + error_a_generative_module_expected l + end in MTBsig(msid, before@(l,new_spec)::after) with @@ -143,13 +174,14 @@ and translate_entry_list env msid is_definition sig_e = let mp = MPself msid in let do_entry env (l,e) = let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in match e with | SPEconst ce -> - let cb = translate_constant env ce in + let cb = translate_constant env con ce in begin match cb.const_hyps with | (_::_) -> error_local_context (Some l) | [] -> - add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb) + add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb) end | SPEmind mie -> let mib = translate_mind env mie in @@ -253,8 +285,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), |