From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- kernel/modops.ml | 90 ++++++++++++++++++++++++++++++++------------------------ 1 file changed, 51 insertions(+), 39 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index 0f0056ed..ab187dba 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = + fun is_mod sub subst_impl do_delta mb -> let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in let mp' = subst_mp sub mp in let sub = @@ -204,10 +208,7 @@ and subst_body is_mod sub do_delta mb = else add_mp mp mp' empty_delta_resolver sub in let ty' = subst_signature sub do_delta ty in - let me' = - implem_smartmap - (subst_signature sub id_delta) (subst_expression sub id_delta) me - in + let me' = subst_impl sub me in let aty' = Option.smartmap (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta @@ -220,9 +221,14 @@ and subst_body is_mod sub do_delta mb = mod_type_alg = aty'; mod_delta = delta' } -and subst_module sub do_delta mb = subst_body true sub do_delta mb +and subst_module sub do_delta mb = + subst_body true sub subst_impl do_delta mb + +and subst_impl sub me = + implem_smartmap + (subst_signature sub id_delta) (subst_expression sub id_delta) me -and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb +and subst_modtype sub do_delta mtb = subst_body false sub (fun _ () -> ()) do_delta mtb and subst_expr sub do_delta seb = match seb with |MEident mp -> @@ -261,13 +267,13 @@ let subst_structure subst = subst_structure subst do_delta_codom (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge mp = let perform rkaction env = match rkaction with - |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> + | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e - |_ -> + | _ -> CErrors.anomaly ~label:"Modops.add_retroknowledge" - (Pp.str "had to import an unsupported kind of term") + (Pp.str "had to import an unsupported kind of term.") in - fun lclrk env -> + fun (ModBodyRK 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. @@ -327,12 +333,10 @@ let strengthen_const mp_from l cb resolver = |_ -> let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in - let u = - if cb.const_polymorphic then - let u = Univ.UContext.instance cb.const_universes in - let s = Univ.make_instance_subst u in - Univ.subst_univs_level_instance s u - else Univ.Instance.empty + let u = + match cb.const_universes with + | Monomorphic_const _ -> Univ.Instance.empty + | Polymorphic_const ctx -> Univ.make_abstract_instance ctx in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); @@ -398,10 +402,10 @@ let inline_delta_resolver env inl mp mbid mtb delta = | Undef _ | OpaqueDef _ -> l | Def body -> let constr = Mod_subst.force_constr body in - add_inline_delta_resolver kn (lev, Some constr) l + add_inline_delta_resolver kn (lev, Some constr) l with Not_found -> - error_no_such_label_sub (con_label con) - (string_of_mp (con_modpath con)) + error_no_such_label_sub (Constant.label con) + (ModPath.to_string (Constant.modpath con)) in make_inline delta constants @@ -568,7 +572,7 @@ let rec is_bounded_expr l = function is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr | _ -> false -let rec clean_module l mb = +let rec clean_module_body l mb = let impl, typ = mb.mod_expr, mb.mod_type in let typ' = clean_signature l typ in let impl' = match impl with @@ -578,19 +582,25 @@ let rec clean_module l mb = if typ==typ' && impl==impl' then mb else { mb with mod_type=typ'; mod_expr=impl' } +and clean_module_type l mb = + let (), typ = mb.mod_expr, mb.mod_type in + let typ' = clean_signature l typ in + if typ==typ' then mb + else { mb with mod_type=typ' } + and clean_field l field = match field with |(lab,SFBmodule mb) -> - let mb' = clean_module l mb in + let mb' = clean_module_body l mb in if mb==mb' then field else (lab,SFBmodule mb') |_ -> field and clean_structure l = List.smartmap (clean_field l) and clean_signature l = - functor_smartmap (clean_module l) (clean_structure l) + functor_smartmap (clean_module_type l) (clean_structure l) and clean_expression l = - functor_smartmap (clean_module l) (fun me -> me) + functor_smartmap (clean_module_type l) (fun me -> me) let rec collect_mbid l sign = match sign with |MoreFunctor (mbid,ty,m) -> @@ -614,14 +624,16 @@ let join_constant_body except otab cb = | _ -> () let join_structure except otab s = - let rec join_module mb = - implem_iter join_signature join_expression mb.mod_expr; + let rec join_module : 'a. 'a generic_module_body -> unit = fun mb -> Option.iter join_expression mb.mod_type_alg; join_signature mb.mod_type and join_field (l,body) = match body with |SFBconst sb -> join_constant_body except otab sb |SFBmind _ -> () - |SFBmodule m |SFBmodtype m -> join_module m + |SFBmodule m -> + implem_iter join_signature join_expression m.mod_expr; + join_module m + |SFBmodtype m -> join_module m and join_structure struc = List.iter join_field struc and join_signature sign = functor_iter join_module join_structure sign -- cgit v1.2.3