From 8741623408e100097167504bc35c4cbb7982aedd Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 17 Jul 2013 15:31:55 +0000 Subject: Modops.destr_functor without useless env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16629 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_typing.ml | 15 +++----- kernel/modops.ml | 101 ++++++++++++++++++++++++++----------------------- kernel/modops.mli | 2 +- library/declaremods.ml | 4 +- 4 files changed, 63 insertions(+), 59 deletions(-) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index b24deb0dc..f7f3c2b77 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -44,13 +44,10 @@ let rec list_split_assoc ((k,m) as km) rev_before = function | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> rev_before,b,after | h::tail -> list_split_assoc km (h::rev_before) tail -let discr_resolver env mtb = - match mtb.typ_expr with - SEBstruct _ -> - mtb.typ_delta - | _ -> (*case mp is a functor *) - empty_delta_resolver - +let discr_resolver mtb = match mtb.typ_expr with + | SEBstruct _ -> mtb.typ_delta + | _ -> empty_delta_resolver (* when mp is a functor *) + let rec rebuild_mp mp l = match l with []-> mp @@ -272,14 +269,14 @@ and translate_module env mp inl me = and translate_apply env inl ftrans mexpr mkalg = let sign,alg,resolver,cst1 = ftrans in - let farg_id, farg_b, fbody_b = destr_functor env sign in + let farg_id, farg_b, fbody_b = destr_functor sign in let mp1 = try path_of_mexpr mexpr with Not_path -> error_application_to_not_path mexpr in let mtb = module_type_of_module None (lookup_module mp1 env) in let cst2 = check_subtypes env mtb farg_b in - let mp_delta = discr_resolver env mtb in + let mp_delta = discr_resolver mtb in let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in let subst = map_mbid farg_id mp1 mp_delta in diff --git a/kernel/modops.ml b/kernel/modops.ml index 6c46ad510..3b789016b 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -119,7 +119,7 @@ let error_no_such_label_sub l l1 = (************************) -let destr_functor env mtb = +let destr_functor mtb = match mtb with | SEBfunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) @@ -299,17 +299,20 @@ let rec strengthen_mod mp_from mp_to mb = match mb.mod_type with | SEBstruct (sign) -> let resolve_out,sign_out = - strengthen_sig 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} + strengthen_sig 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 ~label:"Modops" (Pp.str "the evaluation of the structure failed ") + | _ -> + anomaly ~label:"Modops" + (Pp.str "the evaluation of the structure failed ") and strengthen_sig mp_from sign mp_to resolver = match sign with @@ -340,13 +343,16 @@ let strengthen mtb mp = match mtb.typ_expr with | SEBstruct (sign) -> let resolve_out,sign_out = - strengthen_sig 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)} + strengthen_sig 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 ~label:"Modops" (Pp.str "the evaluation of the structure failed ") + | _ -> + anomaly ~label:"Modops" + (Pp.str "the evaluation of the structure failed ") let module_type_of_module mp mb = match mp with @@ -386,32 +392,32 @@ let inline_delta_resolver env inl mp mbid mtb delta = in make_inline delta constants -let rec strengthen_and_subst_mod - mb subst mp_from mp_to 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 - 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 ~label:"Modops" (Pp.str "the evaluation of the structure failed ") - -and strengthen_and_subst_struct +let rec strengthen_and_subst_mod mb subst mp_from mp_to 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 + 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 ~label:"Modops" + (Pp.str "the evaluation of the structure failed ") + +and strengthen_and_subst_struct str subst mp_alias mp_from mp_to alias incl resolver = match str with | [] -> empty_delta_resolver,[] @@ -485,10 +491,11 @@ and strengthen_and_subst_struct let mty = subst_modtype subst' (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in let resolve_out,rest' = strengthen_and_subst_struct rest subst - mp_alias mp_from mp_to alias incl resolver in - (add_mp_delta_resolver - mp_to' mp_to' resolve_out),(l,SFBmodtype mty)::rest' - + 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 P be a module path when we write "Module M:=P." or "Module M. Include P. End M." we need to perform two operations to compute the body of M. The first one is applying diff --git a/kernel/modops.mli b/kernel/modops.mli index 66aadd124..c4d8ab349 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -23,7 +23,7 @@ val module_type_of_module : module_path option -> module_body -> module_type_body val destr_functor : - env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body + struct_expr_body -> MBId.t * module_type_body * struct_expr_body val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body diff --git a/library/declaremods.ml b/library/declaremods.ml index 0a5b61656..468f7229b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -388,7 +388,7 @@ let rec compute_subst env mbids sign mp_l inl = | _,[] -> mbids,empty_subst | [],r -> error "Application of a functor with too few arguments." | mbid::mbids,mp::mp_l -> - let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mb = Environ.lookup_module mp env in let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in let resolver = match discr_resolver mb with @@ -791,7 +791,7 @@ let rec include_subst env mp reso mbids sign inline = match mbids with | [] -> empty_subst | mbid::mbids -> - let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in + let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let subst = include_subst env mp reso mbids fbody_b inline in let mp_delta = Modops.inline_delta_resolver env inline mp farg_id farg_b reso -- cgit v1.2.3