diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 404 |
1 files changed, 210 insertions, 194 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index f0d579a4..0c2c6bd7 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,14 +1,20 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) +(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of + the Coq module system *) +(* Inlining and more liberal use of modules and module types by Claudio + Sacerdoti, Nov 2004 *) +(* New structure-based model of modules and miscellaneous bug fixes by + Élie Soubiran, from Feb 2008 *) + +(* This file provides with various operations on modules and module types *) -(*i*) open Util open Pp open Names @@ -18,80 +24,103 @@ open Declarations open Environ open Entries open Mod_subst -(*i*) - - - -let error_existing_label l = - error ("The label "^string_of_label l^" is already declared.") - -let error_declaration_not_path _ = error "Declaration is not a path." - -let error_application_to_not_path _ = error "Application to not path." - -let error_not_a_functor _ = error "Application of not a functor." - -let error_incompatible_modtypes _ _ = error "Incompatible module types." - -let error_not_equal _ _ = error "Non equal modules." -let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.") - -let error_no_such_label l = error ("No such label "^string_of_label l^".") - -let error_incompatible_labels l l' = - error ("Opening and closing labels are not the same: " - ^string_of_label l^" <> "^string_of_label l'^" !") - -let error_result_must_be_signature () = - error "The result module type must be a signature." +type signature_mismatch_error = + | InductiveFieldExpected of mutual_inductive_body + | DefinitionFieldExpected + | ModuleFieldExpected + | ModuleTypeFieldExpected + | NotConvertibleInductiveField of identifier + | NotConvertibleConstructorField of identifier + | NotConvertibleBodyField + | NotConvertibleTypeField + | NotSameConstructorNamesField + | NotSameInductiveNameInBlockField + | FiniteInductiveFieldExpected of bool + | InductiveNumbersFieldExpected of int + | InductiveParamsNumberField of int + | RecordFieldExpected of bool + | RecordProjectionsExpected of name list + | NotEqualInductiveAliases + | NoTypeConstraintExpected + +type module_typing_error = + | SignatureMismatch of label * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of label + | ApplicationToNotPath of module_struct_entry + | NotAFunctor of struct_expr_body + | IncompatibleModuleTypes of module_type_body * module_type_body + | NotEqualModulePaths of module_path * module_path + | NoSuchLabel of label + | IncompatibleLabels of label * label + | SignatureExpected of struct_expr_body + | NoModuleToEnd + | NoModuleTypeToEnd + | NotAModule of string + | NotAModuleType of string + | NotAConstant of label + | IncorrectWithConstraint of label + | GenerativeModuleExpected of label + | NonEmptyLocalContect of label option + | LabelMissing of label * string + +exception ModuleTypingError of module_typing_error + +let error_existing_label l = + raise (ModuleTypingError (LabelAlreadyDeclared l)) + +let error_application_to_not_path mexpr = + raise (ModuleTypingError (ApplicationToNotPath mexpr)) + +let error_not_a_functor mtb = + raise (ModuleTypingError (NotAFunctor mtb)) + +let error_incompatible_modtypes mexpr1 mexpr2 = + raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2))) + +let error_not_equal_modpaths mp1 mp2 = + raise (ModuleTypingError (NotEqualModulePaths (mp1,mp2))) + +let error_signature_mismatch l spec why = + raise (ModuleTypingError (SignatureMismatch (l,spec,why))) + +let error_no_such_label l = + raise (ModuleTypingError (NoSuchLabel l)) + +let error_incompatible_labels l l' = + raise (ModuleTypingError (IncompatibleLabels (l,l'))) let error_signature_expected mtb = - error "Signature expected." + raise (ModuleTypingError (SignatureExpected mtb)) -let error_no_module_to_end _ = - error "No open module to end." +let error_no_module_to_end _ = + raise (ModuleTypingError NoModuleToEnd) let error_no_modtype_to_end _ = - error "No open module type to end." - -let error_not_a_modtype_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module type.")) - -let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) + raise (ModuleTypingError NoModuleTypeToEnd) -let error_not_a_module_or_modtype_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type.")) +let error_not_a_modtype s = + raise (ModuleTypingError (NotAModuleType s)) -let error_not_a_module s = error_not_a_module_loc dummy_loc s +let error_not_a_module s = + raise (ModuleTypingError (NotAModule s)) -let error_not_a_constant l = - error ("\""^(string_of_label l)^"\" is not a constant.") +let error_not_a_constant l = + raise (ModuleTypingError (NotAConstant l)) -let error_with_incorrect l = - error ("Incorrect constraint for label \""^(string_of_label l)^"\".") +let error_incorrect_with_constraint l = + raise (ModuleTypingError (IncorrectWithConstraint l)) -let error_a_generative_module_expected l = - error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ - "component of generative modules can be changed using the \"with\" " ^ - "construct.") - -let error_local_context lo = - match lo with - None -> - error ("The local context is not empty.") - | (Some l) -> - error ("The local context of the component "^ - (string_of_label l)^" is not empty.") +let error_generative_module_expected l = + raise (ModuleTypingError (GenerativeModuleExpected l)) +let error_non_empty_local_context lo = + raise (ModuleTypingError (NonEmptyLocalContect lo)) let error_no_such_label_sub l l1 = - error ("The field "^(string_of_label l)^" is missing in "^l1^".") - -let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules." + raise (ModuleTypingError (LabelMissing (l,l1))) -let error_application_to_module_type _ = error "Module application to a module type." +(************************) let destr_functor env mtb = match mtb with @@ -116,9 +145,9 @@ let check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else let mb1=lookup_module mp1 env in let mb2=lookup_module mp2 env in - if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2) + if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2) then () - else error_not_equal mp1 mp2 + else error_not_equal_modpaths mp1 mp2 let rec subst_with_body sub = function | With_module_body(id,mp) -> @@ -235,18 +264,13 @@ let add_retroknowledge mp = let rec add_signature mp sign resolver env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in - let con = constant_of_kn kn in - let mind = mind_of_kn kn in - match elem with - | SFBconst cb -> - let con = constant_of_delta resolver con in - Environ.add_constant con cb env - | SFBmind mib -> - let mind = mind_of_delta resolver mind in - Environ.add_mind mind mib env - | SFBmodule mb -> add_module mb env - (* adds components as well *) - | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env + match elem with + | SFBconst cb -> + Environ.add_constant (constant_of_delta_kn resolver kn) cb env + | SFBmind mib -> + Environ.add_mind (mind_of_delta_kn resolver kn) mib env + | SFBmodule mb -> add_module mb env (* adds components as well *) + | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env in List.fold_left add_one env sign @@ -260,100 +284,83 @@ and add_module mb env = | SEBfunctor _ -> env | _ -> anomaly "Modops:the evaluation of the structure failed " -let strengthen_const env mp_from l cb resolver = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> - let con = make_con mp_from empty_dirpath l in - let con = constant_of_delta resolver con in - let const = mkConst con in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false; - const_body_code = Cemitcodes.from_val - (compile_constant_body env const_subs false false) - } - - -let rec strengthen_mod env mp_from mp_to mb = +let strengthen_const mp_from l cb resolver = + match cb.const_body with + | Def _ -> cb + | _ -> + let kn = make_kn mp_from empty_dirpath l in + let con = constant_of_delta_kn resolver kn in + { cb with + const_body = Def (Declarations.from_val (mkConst con)); + const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) + } + +let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then - mb + mb else match mb.mod_type with - | SEBstruct (sign) -> - let resolve_out,sign_out = - strengthen_sig env mp_from sign mp_to mb.mod_delta in + | 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 + 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 "Modops:the evaluation of the structure failed " - -and strengthen_sig env mp_from sign mp_to resolver = + +and strengthen_sig mp_from sign mp_to resolver = match sign with | [] -> empty_delta_resolver,[] | (l,SFBconst cb) :: rest -> - let item' = - l,SFBconst (strengthen_const env mp_from l cb resolver) in - let resolve_out,rest' = - strengthen_sig env mp_from rest mp_to resolver in - resolve_out,item'::rest' + let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out,item'::rest' | (_,SFBmind _ as item):: rest -> - let resolve_out,rest' = - strengthen_sig env mp_from rest mp_to resolver in - resolve_out,item::rest' + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out,item::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in - let mp_to' = MPdot(mp_to,l) in - let mb_out = - strengthen_mod env mp_from' mp_to' mb in + let mp_to' = MPdot(mp_to,l) in + let mb_out = strengthen_mod mp_from' mp_to' mb in let item' = l,SFBmodule (mb_out) in - let env' = add_module mb_out env in - let resolve_out,rest' = - strengthen_sig env' mp_from rest mp_to resolver in - add_delta_resolver resolve_out mb.mod_delta, - item':: rest' - | (l,SFBmodtype mty as item) :: rest -> - let env' = add_modtype - (MPdot(mp_from,l)) mty env - in - let resolve_out,rest' = - strengthen_sig env' mp_from rest mp_to resolver in - resolve_out,item::rest' - -let strengthen env mtb mp = + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + add_delta_resolver resolve_out mb.mod_delta, item':: rest' + | (l,SFBmodtype mty as item) :: rest -> + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out,item::rest' + +let strengthen mtb mp = if mp_in_delta mtb.typ_mp mtb.typ_delta then (* in this case mtb has already been strengthened*) - mtb + mtb else match mtb.typ_expr with - | SEBstruct (sign) -> + | SEBstruct (sign) -> let resolve_out,sign_out = - strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in + 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 "Modops:the evaluation of the structure failed " - -let module_type_of_module env mp mb = + +let module_type_of_module mp mb = match mp with Some mp -> - strengthen env { + strengthen { typ_mp = mp; typ_expr = mb.mod_type; typ_expr_alg = None; typ_constraints = mb.mod_constraints; typ_delta = mb.mod_delta} mp - + | None -> {typ_mp = mb.mod_mp; typ_expr = mb.mod_type; @@ -361,34 +368,29 @@ let module_type_of_module env mp mb = typ_constraints = mb.mod_constraints; typ_delta = mb.mod_delta} -let complete_inline_delta_resolver env mp mbid mtb delta = - let constants = inline_of_delta mtb.typ_delta in +let inline_delta_resolver env inl mp mbid mtb delta = + let constants = inline_of_delta inl mtb.typ_delta in let rec make_inline delta = function | [] -> delta - | kn::r -> + | (lev,kn)::r -> let kn = replace_mp_in_kn (MPbound mbid) mp kn in - let con = constant_of_kn kn in - let con' = constant_of_delta delta con in - try - let constant = lookup_constant con' env in - if (not constant.Declarations.const_opaque) then - let constr = Option.map Declarations.force - constant.Declarations.const_body in - if constr = None then - (make_inline delta r) - else - add_inline_constr_delta_resolver con (Option.get constr) - (make_inline delta r) - else - (make_inline delta r) - with - Not_found -> error_no_such_label_sub (con_label con) - (string_of_mp (con_modpath con)) + let con = constant_of_delta_kn delta kn in + try + let constant = lookup_constant con env in + let l = make_inline delta r in + match constant.const_body with + | Undef _ | OpaqueDef _ -> l + | Def body -> + let constr = Declarations.force body in + 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)) in - make_inline delta constants + make_inline delta constants let rec strengthen_and_subst_mod - mb subst env mp_from mp_to env resolver = + 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 @@ -397,7 +399,7 @@ let rec strengthen_and_subst_mod (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb else let resolver,new_sig = - strengthen_and_subst_struct str subst env + strengthen_and_subst_struct str subst mp_from mp_from mp_to false false mb.mod_delta in {mb with @@ -413,42 +415,48 @@ let rec strengthen_and_subst_mod | _ -> anomaly "Modops:the evaluation of the structure failed " and strengthen_and_subst_struct - str subst env mp_alias mp_from mp_to alias incl resolver = + str subst mp_alias mp_from mp_to alias incl resolver = match str with | [] -> empty_delta_resolver,[] | (l,SFBconst cb) :: rest -> - let item' = if alias then + let item' = if alias then + (* case alias no strengthening needed*) l,SFBconst (subst_const_body subst cb) else - l,SFBconst (strengthen_const env mp_from l + l,SFBconst (strengthen_const mp_from l (subst_const_body subst cb) resolver) in - let con = make_con mp_from empty_dirpath l in let resolve_out,rest' = - strengthen_and_subst_struct rest subst env + strengthen_and_subst_struct rest subst mp_alias mp_from mp_to alias incl resolver in - if incl then - let old_name = constant_of_delta resolver con in - (add_constant_delta_resolver - (constant_of_kn_equiv (make_kn mp_to empty_dirpath l) - (canonical_con old_name)) - resolve_out), - item'::rest' - else - resolve_out,item'::rest' + if incl then + (* If we are performing an inclusion we need to add + the fact that the constant mp_to.l is \Delta-equivalent + to resolver(mp_from.l) *) + let kn_from = make_kn mp_from empty_dirpath l in + let kn_to = make_kn mp_to empty_dirpath l in + let old_name = kn_of_delta resolver kn_from in + (add_kn_delta_resolver kn_to old_name resolve_out), + item'::rest' + else + (*In this case the fact that the constant mp_to.l is + \Delta-equivalent to resolver(mp_from.l) is already known + because resolve_out contains mp_to maps to resolver(mp_from)*) + resolve_out,item'::rest' | (l,SFBmind mib) :: rest -> + (*Same as constant*) let item' = l,SFBmind (subst_mind subst mib) in - let mind = make_mind mp_from empty_dirpath l in let resolve_out,rest' = - strengthen_and_subst_struct rest subst env + strengthen_and_subst_struct rest subst mp_alias mp_from mp_to alias incl resolver in - if incl then - let old_name = mind_of_delta resolver mind in - (add_mind_delta_resolver - (mind_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_mind old_name)) resolve_out), - item'::rest' - else - resolve_out,item'::rest' + if incl then + let kn_from = make_kn mp_from empty_dirpath l in + let kn_to = make_kn mp_to empty_dirpath l in + let old_name = kn_of_delta resolver kn_from in + (add_kn_delta_resolver kn_to old_name resolve_out), + item'::rest' + else + resolve_out,item'::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in @@ -457,15 +465,20 @@ and strengthen_and_subst_struct (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb else strengthen_and_subst_mod - mb subst env mp_from' mp_to' env resolver + mb subst mp_from' mp_to' resolver in let item' = l,SFBmodule (mb_out) in - let env' = add_module mb_out env in - let resolve_out,rest' = - strengthen_and_subst_struct rest subst env' + let resolve_out,rest' = + strengthen_and_subst_struct rest subst mp_alias mp_from mp_to alias incl resolver in - if is_functor mb_out.mod_type then (add_mp_delta_resolver - mp_to' mp_to' resolve_out),item':: rest' else + (* if mb is a functor we should not derive new equivalences + on names, hence we add the fact that the functor can only + be equivalent to itself. If we adopt an applicative + semantic for functor this should be changed.*) + if is_functor mb_out.mod_type then + (add_mp_delta_resolver + mp_to' mp_to' resolve_out),item':: rest' + else add_delta_resolver resolve_out mb_out.mod_delta, item':: rest' | (l,SFBmodtype mty) :: rest -> @@ -474,27 +487,30 @@ and strengthen_and_subst_struct let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in let mty = subst_modtype subst' (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in - let env' = add_modtype mp_from' mty env in - let resolve_out,rest' = strengthen_and_subst_struct rest subst env' + 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' -let strengthen_and_subst_mb mb mp env include_b = + +(* 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 + the substitution {P <- M} on the type of P and the second one is strenghtening. *) +let strengthen_and_subst_mb mb mp include_b = 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 the strengthening is useless + (*if mb.mod_mp is an alias then the strengthening is useless (i.e. it is already done)*) - let mp_alias = delta_of_mp mb.mod_delta mb.mod_mp in + let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in let new_resolver = add_mp_delta_resolver mp mp_alias - (subst_dom_delta_resolver subst_resolver mb.mod_delta) in + (subst_dom_delta_resolver subst_resolver mb.mod_delta) in let subst = map_mp mb.mod_mp mp new_resolver in let resolver_out,new_sig = - strengthen_and_subst_struct str subst env - mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta + strengthen_and_subst_struct str subst + mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta in {mb with mod_mp = mp; @@ -509,7 +525,7 @@ let strengthen_and_subst_mb mb mp env include_b = | _ -> anomaly "Modops:the evaluation of the structure failed " -let subst_modtype_and_resolver mtb mp env = +let subst_modtype_and_resolver mtb mp = let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in let full_subst = (map_mp mtb.typ_mp mp new_delta) in |