diff options
| -rw-r--r-- | kernel/names.ml | 1 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | library/nametab.ml | 73 |
3 files changed, 41 insertions, 36 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index e6c5686ed..7cb8dc4c4 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -122,6 +122,7 @@ type variable = Id.t type module_ident = Id.t +module ModIdset = Id.Set module ModIdmap = Id.Map (** {6 Directory paths = section names paths } *) diff --git a/kernel/names.mli b/kernel/names.mli index 16d0ae5d0..816467721 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -79,7 +79,8 @@ type name = Name.t = Name of Id.t | Anonymous type variable = Id.t type module_ident = Id.t -module ModIdmap : Map.S with type key = module_ident +module ModIdset : Set.S with type elt = module_ident +module ModIdmap : Map.ExtS with type key = module_ident and module Set := ModIdset (** {6 Directory paths = section names paths } *) diff --git a/library/nametab.ml b/library/nametab.ml index 7eb48a714..2863f6cae 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -110,10 +110,13 @@ struct let rec push_until uname o level tree = function | modid :: path -> - let mc = - try ModIdmap.find modid tree.map - with Not_found -> empty_tree - in + let modify _ mc = push_until uname o (level-1) mc path in + let map = + try ModIdmap.modify modid modify tree.map + with Not_found -> + let ptab = modify () empty_tree in + ModIdmap.add modid ptab tree.map + in let this = if level <= 0 then match tree.path with @@ -127,8 +130,7 @@ struct | Relative _ -> Relative (uname,o) else tree.path in - let ptab' = push_until uname o (level-1) mc path in - mktree this (ModIdmap.add modid ptab' tree.map) + mktree this map | [] -> match tree.path with | Absolute (uname',o') -> @@ -148,42 +150,43 @@ struct let rec push_exactly uname o level tree = function - | modid :: path -> - let mc = - try ModIdmap.find modid tree.map - with Not_found -> empty_tree - in - if Int.equal level 0 then - let this = - match tree.path with - | Absolute (n,_) -> - (* This is an absolute name, we must keep it - otherwise it may become unaccessible forever *) - msg_warning (str ("Trying to mask the absolute name \"" - ^ U.to_string n ^ "\"!")); - tree.path - | Nothing - | Relative _ -> Relative (uname,o) - in - mktree this tree.map - else (* not right level *) - let ptab' = push_exactly uname o (level-1) mc path in - mktree tree.path (ModIdmap.add modid ptab' tree.map) - | [] -> - anomaly (Pp.str "Prefix longer than path! Impossible!") +| [] -> + anomaly (Pp.str "Prefix longer than path! Impossible!") +| modid :: path -> + if Int.equal level 0 then + let this = + match tree.path with + | Absolute (n,_) -> + (* This is an absolute name, we must keep it + otherwise it may become unaccessible forever *) + msg_warning (str ("Trying to mask the absolute name \"" + ^ U.to_string n ^ "\"!")); + tree.path + | Nothing + | Relative _ -> Relative (uname,o) + in + mktree this tree.map + else (* not right level *) + let modify _ mc = push_exactly uname o (level-1) mc path in + let map = + try ModIdmap.modify modid modify tree.map + with Not_found -> + let ptab = modify () empty_tree in + ModIdmap.add modid ptab tree.map + in + mktree tree.path map let push visibility uname o tab = let id,dir = U.repr uname in - let ptab = - try Id.Map.find id tab - with Not_found -> empty_tree - in - let ptab' = match visibility with + let modify _ ptab = match visibility with | Until i -> push_until uname o (i-1) ptab dir | Exactly i -> push_exactly uname o (i-1) ptab dir in - Id.Map.add id ptab' tab + try Id.Map.modify id modify tab + with Not_found -> + let ptab = modify () empty_tree in + Id.Map.add id ptab tab let rec search tree = function |