aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-02-03 14:34:06 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-02-03 17:35:54 +0100
commit3ad26e3de5780b84b2723d44d52094bab6b23786 (patch)
tree35c9f8b7d5ec87c3f6125acdd4febdeef0d701dc /library
parent5d7081cccd661a4acd5c3acbff80156bff32322e (diff)
Allocation-friendly mapping functions in Nametab.
Diffstat (limited to 'library')
-rw-r--r--library/nametab.ml73
1 files changed, 38 insertions, 35 deletions
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