aboutsummaryrefslogtreecommitdiffhomepage
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, 28 insertions, 28 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c7bc76e57..823047974 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -80,7 +80,7 @@ type modvariant =
type module_info =
{modpath : module_path;
- label : label;
+ label : Label.t;
variant : modvariant;
resolver : delta_resolver;
resolver_of_param : delta_resolver;}
@@ -96,8 +96,8 @@ type safe_environment =
{ old : safe_environment;
env : env;
modinfo : module_info;
- modlabels : Labset.t;
- objlabels : Labset.t;
+ modlabels : Label.Set.t;
+ objlabels : Label.Set.t;
revstruct : structure_body;
univ : Univ.constraints;
engagement : engagement option;
@@ -105,8 +105,8 @@ type safe_environment =
loads : (module_path * module_body) list;
local_retroknowledge : Retroknowledge.action list}
-let exists_modlabel l senv = Labset.mem l senv.modlabels
-let exists_objlabel l senv = Labset.mem l senv.objlabels
+let exists_modlabel l senv = Label.Set.mem l senv.modlabels
+let exists_objlabel l senv = Label.Set.mem l senv.objlabels
let check_modlabel l senv =
if exists_modlabel l senv then error_existing_label l
@@ -114,12 +114,12 @@ let check_objlabel l senv =
if exists_objlabel l senv then error_existing_label l
let check_objlabels ls senv =
- Labset.iter (fun l -> check_objlabel l senv) ls
+ Label.Set.iter (fun l -> check_objlabel l senv) ls
let labels_of_mib mib =
let add,get =
- let labels = ref Labset.empty in
- (fun id -> labels := Labset.add (label_of_id id) !labels),
+ let labels = ref Label.Set.empty in
+ (fun id -> labels := Label.Set.add (Label.of_id id) !labels),
(fun () -> !labels)
in
let visit_mip mip =
@@ -135,12 +135,12 @@ let rec empty_environment =
env = empty_env;
modinfo = {
modpath = initial_path;
- label = mk_label "_";
+ label = Label.make "_";
variant = NONE;
resolver = empty_delta_resolver;
resolver_of_param = empty_delta_resolver};
- modlabels = Labset.empty;
- objlabels = Labset.empty;
+ modlabels = Label.Set.empty;
+ objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -175,11 +175,11 @@ let add_field ((l,sfb) as field) gn senv =
let mlabs,olabs = match sfb with
| SFBmind mib ->
let l = labels_of_mib mib in
- check_objlabels l senv; (Labset.empty,l)
+ check_objlabels l senv; (Label.Set.empty,l)
| SFBconst _ ->
- check_objlabel l senv; (Labset.empty, Labset.singleton l)
+ check_objlabel l senv; (Label.Set.empty, Label.Set.singleton l)
| SFBmodule _ | SFBmodtype _ ->
- check_modlabel l senv; (Labset.singleton l, Labset.empty)
+ check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
in
let senv = add_constraints (constraints_of_sfb sfb) senv in
let env' = match sfb, gn with
@@ -191,8 +191,8 @@ let add_field ((l,sfb) as field) gn senv =
in
{ senv with
env = env';
- modlabels = Labset.union mlabs senv.modlabels;
- objlabels = Labset.union olabs senv.objlabels;
+ modlabels = Label.Set.union mlabs senv.modlabels;
+ objlabels = Label.Set.union olabs senv.objlabels;
revstruct = field :: senv.revstruct }
(* Applying a certain function to the resolver of a safe environment *)
@@ -291,7 +291,7 @@ let add_mind dir l mie senv =
| _ -> ()
in
let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
- if not (eq_label l (label_of_id id)) then
+ if not (Label.equal l (Label.of_id id)) then
anomaly ("the label of inductive packet and its first inductive"^
" type do not match");
let kn = make_mind senv.modinfo.modpath dir l in
@@ -339,8 +339,8 @@ let start_module l senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- modlabels = Labset.empty;
- objlabels = Labset.empty;
+ modlabels = Label.Set.empty;
+ objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -361,7 +361,7 @@ let end_module l restype senv =
| NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
| STRUCT params -> params, (List.length params > 0)
in
- if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label;
+ if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label;
if not (empty_context senv.env) then error_non_empty_local_context None;
let functorize_struct tb =
List.fold_left
@@ -424,7 +424,7 @@ let end_module l restype senv =
mp,resolver,{ old = oldsenv.old;
env = newenv;
modinfo = modinfo;
- modlabels = Labset.add l oldsenv.modlabels;
+ modlabels = Label.Set.add l oldsenv.modlabels;
objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
univ = Univ.union_constraints senv'.univ oldsenv.univ;
@@ -547,8 +547,8 @@ let start_modtype l senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- modlabels = Labset.empty;
- objlabels = Labset.empty;
+ modlabels = Label.Set.empty;
+ objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -565,7 +565,7 @@ let end_modtype l senv =
| LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
| SIG params -> params
in
- if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label;
+ if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label;
if not (empty_context senv.env) then error_non_empty_local_context None;
let auto_tb =
SEBstruct (List.rev senv.revstruct)
@@ -599,7 +599,7 @@ let end_modtype l senv =
mp, { old = oldsenv.old;
env = newenv;
modinfo = oldsenv.modinfo;
- modlabels = Labset.add l oldsenv.modlabels;
+ modlabels = Label.Set.add l oldsenv.modlabels;
objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
univ = Univ.union_constraints senv.univ oldsenv.univ;
@@ -646,7 +646,7 @@ let start_library dir senv =
match (Dir_path.repr dir) with
[] -> anomaly "Empty dirpath in Safe_typing.start_library"
| hd::tl ->
- Dir_path.make tl, label_of_id hd
+ Dir_path.make tl, Label.of_id hd
in
let mp = MPfile dir in
let modinfo = {modpath = mp;
@@ -658,8 +658,8 @@ let start_library dir senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- modlabels = Labset.empty;
- objlabels = Labset.empty;
+ modlabels = Label.Set.empty;
+ objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 14:15:28 +0000