Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Rely on kernel to know if a name is already used so as to be consiste…

…nt with it.

Maybe could we keep only the kernel check, but message would
certainly need to be reformulated then.

For instance, the message was previously different for an attempt to
redefine a name whether this name was in the same section or not.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14528 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit e6dd9e226f9df774ab57e3f65f2124c08f22d71b 1 parent 705d107
herbelin authored Maxime Dénès committed
View
22 kernel/safe_typing.ml
@@ -90,9 +90,6 @@ type module_info =
variant : modvariant;
resolver : delta_resolver;
resolver_of_param : delta_resolver;}
-
-let check_label l labset =
- if Labset.mem l labset then error_existing_label l
let set_engagement_opt oeng env =
match oeng with
@@ -114,6 +111,11 @@ type safe_environment =
local_retroknowledge : (Native.retro_action * constr) list
}
+let exists_label l senv = Labset.mem l senv.labset
+
+let check_label l senv =
+ if exists_label l senv then error_existing_label l
+
(* a small hack to avoid variants and an unused case in all functions *)
let rec empty_environment =
{ old = empty_environment;
@@ -241,7 +243,7 @@ let hcons_constant_body cb =
const_type = hcons_const_type cb.const_type }
let add_constant dir l decl senv =
- check_label l senv.labset;
+ check_label l senv;
let kn = make_con senv.modinfo.modpath dir l in
let cb =
match decl with
@@ -275,7 +277,7 @@ let add_mind dir l mie senv =
if l <> label_of_id id then
anomaly ("the label of inductive packet and its first inductive"^
" type do not match");
- check_label l senv.labset;
+ check_label l senv;
(* TODO: when we will allow reorderings we will have to verify
all labels *)
let kn = make_mind senv.modinfo.modpath dir l in
@@ -286,7 +288,7 @@ let add_mind dir l mie senv =
(* Insertion of module types *)
let add_modtype l mte inl senv =
- check_label l senv.labset;
+ check_label l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let mtb = translate_module_type senv.env mp inl mte in
let senv' = add_field (l,SFBmodtype mtb) (MT mp) senv in
@@ -300,7 +302,7 @@ let full_add_module mb senv =
(* Insertion of modules *)
let add_module l me inl senv =
- check_label l senv.labset;
+ check_label l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let mb = translate_module senv.env mp inl me in
let senv' = add_field (l,SFBmodule mb) M senv in
@@ -312,7 +314,7 @@ let add_module l me inl senv =
(* Interactive modules *)
let start_module l senv =
- check_label l senv.labset;
+ check_label l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let modinfo = { modpath = mp;
label = l;
@@ -465,7 +467,7 @@ let end_module l restype senv =
let senv = update_resolver (add_delta_resolver resolver) senv
in
let add senv ((l,elem) as field) =
- check_label l senv.labset;
+ check_label l senv;
let new_name = match elem with
| SFBconst _ ->
let kn = make_kn mp_sup empty_dirpath l in
@@ -527,7 +529,7 @@ let add_module_parameter mbid mte inl senv =
(* Interactive module types *)
let start_modtype l senv =
- check_label l senv.labset;
+ check_label l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let modinfo = { modpath = mp;
label = l;
View
3  kernel/safe_typing.mli
@@ -139,6 +139,9 @@ val safe_infer : safe_environment -> constr -> judgment * Univ.constraints
val typing : safe_environment -> constr -> judgment
+(** {7 Query } *)
+
+val exists_label : label -> safe_environment -> bool
(* Retroknowledge of inductive *)
View
20 library/declare.ml
@@ -112,11 +112,17 @@ let open_constant i ((sp,kn),_) =
let con = Global.constant_of_delta (constant_of_kn kn) in
Nametab.push (Nametab.Exactly i) sp (ConstRef con)
+let exists_name id =
+ variable_exists id or Global.exists_label (label_of_id id)
+
+let check_exists sp =
+ let id = basename sp in
+ if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+
let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
let id = basename sp in
let _,dir,_ = repr_kn kn in
- if variable_exists id or Nametab.exists_cci sp then
- alreadydeclared (pr_id id ++ str " already exists");
+ check_exists sp;
let kn' = Global.add_constant dir id cdt in
assert (kn' = constant_of_kn kn);
Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
@@ -197,16 +203,8 @@ let inductive_names sp kn mie =
([], 0) mie.mind_entry_inds
in names
-let check_exists_inductive (sp,_) =
- (if variable_exists (basename sp) then
- alreadydeclared (pr_id (basename sp) ++ str " already exists"));
- if Nametab.exists_cci sp then
- let (_,id) = repr_path sp in
- alreadydeclared (pr_id id ++ str " already exists")
-
let load_inductive i ((sp,kn),(_,mie)) =
let names = inductive_names sp kn mie in
- List.iter check_exists_inductive names;
List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names
let open_inductive i ((sp,kn),(_,mie)) =
@@ -215,7 +213,7 @@ let open_inductive i ((sp,kn),(_,mie)) =
let cache_inductive ((sp,kn),(dhyps,mie)) =
let names = inductive_names sp kn mie in
- List.iter check_exists_inductive names;
+ List.iter check_exists (List.map fst names);
let id = basename sp in
let _,dir,_ = repr_kn kn in
let kn' = Global.add_mind dir id mie in
View
1  library/declare.mli
@@ -80,3 +80,4 @@ val cofixpoint_message : identifier list -> unit
val recursive_message : bool (** true = fixpoint *) ->
int array option -> identifier list -> unit
+val exists_name : identifier -> bool
View
4 library/global.ml
@@ -128,7 +128,9 @@ let mind_of_delta mind =
let resolver,resolver_param = (delta_of_senv !global_env) in
Mod_subst.mind_of_delta resolver_param
(Mod_subst.mind_of_delta resolver mind)
-
+
+let exists_label id = exists_label id !global_env
+
let start_library dir =
let mp,newenv = start_library dir !global_env in
global_env := newenv;
View
1  library/global.mli
@@ -87,6 +87,7 @@ val lookup_module : module_path -> module_body
val lookup_modtype : module_path -> module_type_body
val constant_of_delta : constant -> constant
val mind_of_delta : mutual_inductive -> mutual_inductive
+val exists_label : label -> bool
(** Compiled modules *)
val start_library : dir_path -> module_path
View
1  library/libnames.ml
@@ -195,6 +195,7 @@ type full_path = {
basename : identifier }
let make_path pa id = { dirpath = pa; basename = id }
+
let repr_path { dirpath = pa; basename = id } = (pa,id)
(* parsing and printing of section paths *)
Please sign in to comment.
Something went wrong with that request. Please try again.