Skip to content

Commit

Permalink
Merge PR coq#18191: HMap: avoid hashing when map is empty, use Int.Ma…
Browse files Browse the repository at this point in the history 
…p combinators more

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>
  • Loading branch information
@coqbot-app @ppedrot
coqbot-app[bot] and ppedrot authored Nov 17, 2023
2 parents 8f089e2 + 7a7074b commit c77019d
Show file tree
Hide file tree
Showing 2 changed files with 100 additions and 57 deletions.
104 changes: 57 additions & 47 deletions clib/hMap.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,8 @@ struct
let is_empty = Int.Map.is_empty

let mem x s =
if Int.Map.is_empty s then false
else
let h = M.hash x in
try
let m = Int.Map.find h s in
Expand All @@ -46,29 +48,27 @@ struct

let add x s =
let h = M.hash x in
try
let m = Int.Map.find h s in
let m = Set.add x m in
Int.Map.set h m s
with Not_found ->
let m = Set.singleton x in
Int.Map.add h m s
Int.Map.update h (function
| None -> Some (Set.singleton x)
| Some m -> Some (Set.add x m))
s

let singleton x =
let h = M.hash x in
let m = Set.singleton x in
Int.Map.singleton h m

let remove x s =
let h = M.hash x in
try
let m = Int.Map.find h s in
let m = Set.remove x m in
if Set.is_empty m then
Int.Map.remove h s
else
Int.Map.set h m s
with Not_found -> s
if Int.Map.is_empty s then s
else
let h = M.hash x in
Int.Map.update h (function
| None -> None
| Some m ->
let m = Set.remove x m in
if Set.is_empty m then None
else Some m)
s

let height s = Int.Map.height s

Expand Down Expand Up @@ -233,6 +233,8 @@ struct
let is_empty = Int.Map.is_empty

let mem k s =
if Int.Map.is_empty s then false
else
let h = M.hash k in
try
let m = Int.Map.find h s in
Expand All @@ -241,28 +243,26 @@ struct

let add k x s =
let h = M.hash k in
try
let m = Int.Map.find h s in
let m = Map.add k x m in
Int.Map.set h m s
with Not_found ->
let m = Map.singleton k x in
Int.Map.add h m s
Int.Map.update h (function
| None -> Some (Map.singleton k x)
| Some m -> Some (Map.add k x m))
s

let singleton k x =
let h = M.hash k in
Int.Map.singleton h (Map.singleton k x)

let remove k s =
if Int.Map.is_empty s then s
else
let h = M.hash k in
try
let m = Int.Map.find h s in
let m = Map.remove k m in
if Map.is_empty m then
Int.Map.remove h s
else
Int.Map.set h m s
with Not_found -> s
Int.Map.update h (function
| None -> None
| Some m ->
let m = Map.remove k m in
if Map.is_empty m then None
else Some m)
s

let merge f s1 s2 =
let fm h m1 m2 = match m1, m2 with
Expand Down Expand Up @@ -358,11 +358,15 @@ struct
with Not_found -> None

let find k s =
if Int.Map.is_empty s then raise Not_found
else
let h = M.hash k in
let m = Int.Map.find h s in
Map.find k m

let find_opt k s =
if Int.Map.is_empty s then None
else
let h = M.hash k in
match Int.Map.find_opt h s with
| None -> None
Expand All @@ -384,10 +388,10 @@ struct
Int.Map.map fs s

let modify k f s =
if Int.Map.is_empty s then raise Not_found
else
let h = M.hash k in
let m = Int.Map.find h s in
let m = Map.modify k f m in
Int.Map.set h m s
Int.Map.modify h (fun _ m -> Map.modify k f m) s

let bind f s =
let fb m = Map.bind f m in
Expand All @@ -396,10 +400,10 @@ struct
let domain s = Int.Map.map Map.domain s

let set k x s =
if Int.Map.is_empty s then raise Not_found
else
let h = M.hash k in
let m = Int.Map.find h s in
let m = Map.set k x m in
Int.Map.set h m s
Int.Map.modify h (fun _ m -> Map.set k x m) s

module Smart =
struct
Expand All @@ -425,16 +429,22 @@ struct
List.fold_left fold empty l

let update k f m =
let aux = function
| None -> (match f None with
| None -> None
| Some v -> Some (Map.singleton k v))
| Some m ->
let m = Map.update k f m in
if Map.is_empty m then None
else Some m
in
Int.Map.update (M.hash k) aux m
if Int.Map.is_empty m then
begin match f None with
| None -> m
| Some v -> singleton k v
end
else
let aux = function
| None -> (match f None with
| None -> None
| Some v -> Some (Map.singleton k v))
| Some m ->
let m = Map.update k f m in
if Map.is_empty m then None
else Some m
in
Int.Map.update (M.hash k) aux m

module Monad(M : CMap.MonadS) =
struct
Expand Down
53 changes: 43 additions & 10 deletions clib/int.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,30 +31,63 @@ struct

type 'a _map =
| MEmpty
| MNode of 'a map * int * 'a * 'a map * int
| MNode of {l:'a map; v:int; d:'a; r:'a map; h:int}

let map_prj : 'a map -> 'a _map = Obj.magic
let map_inj : 'a _map -> 'a map = Obj.magic

let rec find i s = match map_prj s with
| MEmpty -> raise Not_found
| MNode (l, k, v, r, h) ->
if i < k then find i l
else if i = k then v
| MNode {l; v; d; r; h} ->
if i < v then find i l
else if i = v then d
else find i r

let rec get i s = match map_prj s with
| MEmpty -> assert false
| MNode (l, k, v, r, h) ->
if i < k then get i l
else if i = k then v
| MNode {l; v; d; r; h} ->
if i < v then get i l
else if i = v then d
else get i r

let rec find_opt i s = match map_prj s with
| MEmpty -> None
| MNode (l, k, v, r, h) ->
if i < k then find_opt i l
else if i = k then Some v
| MNode {l; v; d; r; h} ->
if i < v then find_opt i l
else if i = v then Some d
else find_opt i r

let rec set k v (s : 'a map) : 'a map = match map_prj s with
| MEmpty -> raise Not_found
| MNode {l; v=k'; d=v'; r; h} ->
if k < k' then
let l' = set k v l in
if l == l' then s
else map_inj (MNode {l=l'; v=k'; d=v'; r; h})
else if k = k' then
if v' == v then s
else map_inj (MNode {l; v=k'; d=v; r; h})
else
let r' = set k v r in
if r == r' then s
else map_inj (MNode {l; v=k'; d=v'; r=r'; h})

let rec modify k f (s : 'a map) : 'a map = match map_prj s with
| MEmpty -> raise Not_found
| MNode {l; v; d; r; h} ->
if k < v then
let l' = modify k f l in
if l == l' then s
else map_inj (MNode {l=l'; v; d; r; h})
else if k = v then
let d' = f v d in
if d' == d then s
else map_inj (MNode {l; v; d=d'; r; h})
else
let r' = modify k f r in
if r == r' then s
else map_inj (MNode {l; v; d; r=r'; h})

end

module List = struct
Expand Down

0 comments on commit c77019d

Please sign in to comment.