summaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml56
1 files changed, 36 insertions, 20 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c2d71ebb..d7a8b005 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -101,7 +101,8 @@ type safe_environment =
{ old : safe_environment;
env : env;
modinfo : module_info;
- labset : Labset.t;
+ modlabels : Labset.t;
+ objlabels : Labset.t;
revstruct : structure_body;
univ : Univ.constraints;
engagement : engagement option;
@@ -109,13 +110,16 @@ type safe_environment =
loads : (module_path * module_body) list;
local_retroknowledge : Retroknowledge.action list}
-let exists_label l senv = Labset.mem l senv.labset
+let exists_modlabel l senv = Labset.mem l senv.modlabels
+let exists_objlabel l senv = Labset.mem l senv.objlabels
-let check_label l senv =
- if exists_label l senv then error_existing_label l
+let check_modlabel l senv =
+ if exists_modlabel l senv then error_existing_label l
+let check_objlabel l senv =
+ if exists_objlabel l senv then error_existing_label l
-let check_labels ls senv =
- Labset.iter (fun l -> check_label l senv) ls
+let check_objlabels ls senv =
+ Labset.iter (fun l -> check_objlabel l senv) ls
let labels_of_mib mib =
let add,get =
@@ -140,7 +144,8 @@ let rec empty_environment =
variant = NONE;
resolver = empty_delta_resolver;
resolver_of_param = empty_delta_resolver};
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -172,11 +177,15 @@ type generic_name =
| M
let add_field ((l,sfb) as field) gn senv =
- let labels = match sfb with
- | SFBmind mib -> labels_of_mib mib
- | _ -> Labset.singleton l
+ let mlabs,olabs = match sfb with
+ | SFBmind mib ->
+ let l = labels_of_mib mib in
+ check_objlabels l senv; (Labset.empty,l)
+ | SFBconst _ ->
+ check_objlabel l senv; (Labset.empty, Labset.singleton l)
+ | SFBmodule _ | SFBmodtype _ ->
+ check_modlabel l senv; (Labset.singleton l, Labset.empty)
in
- check_labels labels senv;
let senv = add_constraints (constraints_of_sfb sfb) senv in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -187,7 +196,8 @@ let add_field ((l,sfb) as field) gn senv =
in
{ senv with
env = env';
- labset = Labset.union labels senv.labset;
+ modlabels = Labset.union mlabs senv.modlabels;
+ objlabels = Labset.union olabs senv.objlabels;
revstruct = field :: senv.revstruct }
(* Applying a certain function to the resolver of a safe environment *)
@@ -320,7 +330,7 @@ let add_module l me inl senv =
(* Interactive modules *)
let start_module l senv =
- check_label l senv;
+ check_modlabel l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let modinfo = { modpath = mp;
label = l;
@@ -331,7 +341,8 @@ let start_module l senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -415,7 +426,8 @@ let end_module l restype senv =
mp,resolver,{ old = oldsenv.old;
env = newenv;
modinfo = modinfo;
- labset = Labset.add l oldsenv.labset;
+ modlabels = Labset.add l oldsenv.modlabels;
+ objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
univ = Univ.union_constraints senv'.univ oldsenv.univ;
(* engagement is propagated to the upper level *)
@@ -510,7 +522,8 @@ let add_module_parameter mbid mte inl senv =
variant = new_variant;
resolver_of_param = add_delta_resolver
resolver_of_param senv.modinfo.resolver_of_param};
- labset = senv.labset;
+ modlabels = senv.modlabels;
+ objlabels = senv.objlabels;
revstruct = [];
univ = senv.univ;
engagement = senv.engagement;
@@ -522,7 +535,7 @@ let add_module_parameter mbid mte inl senv =
(* Interactive module types *)
let start_modtype l senv =
- check_label l senv;
+ check_modlabel l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let modinfo = { modpath = mp;
label = l;
@@ -533,7 +546,8 @@ let start_modtype l senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -584,7 +598,8 @@ let end_modtype l senv =
mp, { old = oldsenv.old;
env = newenv;
modinfo = oldsenv.modinfo;
- labset = Labset.add l oldsenv.labset;
+ modlabels = Labset.add l oldsenv.modlabels;
+ objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
univ = Univ.union_constraints senv.univ oldsenv.univ;
engagement = senv.engagement;
@@ -643,7 +658,8 @@ let start_library dir senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;