diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 90 |
1 files changed, 51 insertions, 39 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of @@ -17,7 +19,7 @@ open Util open Names -open Term +open Constr open Declarations open Declareops open Environ @@ -35,6 +37,7 @@ type signature_mismatch_error = | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField | NotConvertibleTypeField of env * types * types + | CumulativeStatusExpected of bool | PolymorphicStatusExpected of bool | NotSameConstructorNamesField | NotSameInductiveNameInBlockField @@ -44,11 +47,10 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | NoTypeConstraintExpected | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.constraints + | IncompatibleConstraints of Univ.AUContext.t type module_typing_error = | SignatureMismatch of @@ -58,7 +60,7 @@ type module_typing_error = | NotAFunctor | IsAFunctor | IncompatibleModuleTypes of module_type_body * module_type_body - | NotEqualModulePaths of module_path * module_path + | NotEqualModulePaths of ModPath.t * ModPath.t | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | NotAModule of string @@ -67,7 +69,7 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | IncludeRestrictedFunctor of module_path + | IncludeRestrictedFunctor of ModPath.t exception ModuleTypingError of module_typing_error @@ -142,11 +144,12 @@ let rec functor_iter fty f0 = function (** {6 Misc operations } *) let module_type_of_module mb = - { mb with mod_expr = Abstract; mod_type_alg = None } + { mb with mod_expr = (); mod_type_alg = None; + mod_retroknowledge = ModTypeRK; } let module_body_of_type mp mtb = - assert (mtb.mod_expr == Abstract); - { mtb with mod_mp = mp } + { mtb with mod_expr = Abstract; mod_mp = mp; + mod_retroknowledge = ModBodyRK []; } let check_modpath_equiv env mp1 mp2 = if ModPath.equal mp1 mp2 then () @@ -195,7 +198,8 @@ let rec subst_structure sub do_delta sign = in List.smartmap subst_body sign -and subst_body is_mod sub do_delta mb = +and subst_body : 'a. _ -> _ -> (_ -> '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 |