Skip to content

Commit

Permalink
hconstr use int map ref instead of hashtbl
Browse files Browse the repository at this point in the history
Not sure if I messed up the hashtbl usage but it seems to produce big
buckets, which we then need to linearly scan.

Int map has exactly one bucket per hash and ends up faster.

~~~coq
Require Import Ltac2.Ltac2.

Require Import PrimInt63.

Set Debug "hconstr".

Inductive tree := Leaf (_:int) | Node (_:tree) (_:tree).

Import Constr.Unsafe.

Ltac2 rec big' node leaf n :=
  if Int.equal n 0 then leaf()
  else
    let n := Int.sub n 1 in
    let c := big' node leaf n in
    let c' := big' node leaf n in
    make (App node [|c; c'|]).

Lemma baz : tree.
  Time let x := Ref.ref '(0 :> int) in
  let leaf := 'Leaf in
  let leaf () :=
    let c := Ref.get x in
    let c' := (eval cbv in (add $c 1)) in
    Ref.set x c';
    make (App leaf [|c|])
  in
  let c := big' 'Node leaf 17 in
  Std.exact_no_check c.

Time Defined.
(* 16 -> master: 2s, hconstr v2: 8s
   17 -> master: 8s, hconstr v2: 31s, hconstr v3: 8s
 *)

(*
v2:

Debug: [hconstr] num_bindings = 393217
                          num_buckets = 262144
                          max_bucket_length = 16385
Debug: [hconstr] num_bindings = 1
                          num_buckets = 64
                          max_bucket_length = 1
*)

(*
v3:
Debug: [hconstr] hashes = 392326
                          bindings = 393217
                          most_collisions = 256
Debug: [hconstr] hashes = 1
                          bindings = 1
                          most_collisions = 1

*)
~~~

(BTW the hcons debug says

~~~
Debug: [hcons] num_bindings = 393291
                        num_buckets = 67482
                        max_bucket_length = 4103
~~~

which is sgnificantly smaller than the hconstr max bucket length, IDK why)
  • Loading branch information
SkySkimmer committed Jun 8, 2024
1 parent dea9da9 commit 7da7692
Showing 1 changed file with 56 additions and 6 deletions.
62 changes: 56 additions & 6 deletions kernel/typeops.ml
Original file line number Diff line number Diff line change
Expand Up @@ -661,7 +661,13 @@ module HConstr : sig
(* May not be used on Rel! (subterms can be rels) *)
val of_kind_nohashcons : (t,t,Sorts.t,UVars.Instance.t,Sorts.relevance) kind_of_term -> t

module Tbl : Hashtbl.S with type key = t
module Tbl : sig
type key = t
type 'a t
val find_opt : 'a t -> key -> 'a option
val add : 'a t -> key -> 'a -> unit
val create : int -> 'a t
end

end = struct

Expand Down Expand Up @@ -775,7 +781,52 @@ let push_rel env =
cnt = env.cnt;
}

module Tbl = Hashtbl.Make(Self)
module Tbl = struct
type key = t

type 'a t = (key * 'a) list Int.Map.t ref

let create _ = ref Int.Map.empty

let add tbl key v =
tbl := Int.Map.update key.hash (function
| None -> Some [(key,v)]
| Some l -> Some ((key,v)::l))
!tbl

let find_opt tbl key =
match Int.Map.find_opt key.hash !tbl with
| None -> None
| Some l ->
List.find_map (fun (k',v) ->
if equal key k' then Some v else None)
l

type stats = {
hashes : int;
bindings : int;
most_collisions : int;
}

let empty_stats = {
hashes = 0;
bindings = 0;
most_collisions = 0;
}

let stats tbl =
Int.Map.fold (fun _ l acc ->
let len = List.length l in
{
hashes = acc.hashes + 1;
bindings = acc.bindings + len;
most_collisions = max acc.most_collisions len;
}
)
!tbl
empty_stats

end

let hash_annot = hash_annot Name.hash

Expand Down Expand Up @@ -971,12 +1022,11 @@ let of_constr env c =
let tbl = Tbl.create 57 in
let c = of_constr tbl local_env c in
dbg Pp.(fun () ->
let open Hashtbl in
let stats = Tbl.stats tbl in
v 0 (
str "num_bindings = " ++ int stats.num_bindings ++ spc() ++
str "num_buckets = " ++ int stats.num_buckets ++ spc() ++
str "max_bucket_length = " ++ int stats.max_bucket_length
str "hashes = " ++ int stats.Tbl.hashes ++ spc() ++
str "bindings = " ++ int stats.Tbl.bindings ++ spc() ++
str "most_collisions = " ++ int stats.Tbl.most_collisions
)
);
c
Expand Down

0 comments on commit 7da7692

Please sign in to comment.