summaryrefslogtreecommitdiff
path: root/kernel/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/modops.ml')
-rw-r--r--kernel/modops.ml404
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