refactor(ty): use Hashcons with weak table for types

src/smt/Ty.ml

@@ -18,35 +18,33 @@ let equal_def d1 d2 = match d1, d2 with
   | Ty_uninterpreted _, _ | Ty_def _, _
     -> false
 
-module Tbl_cell = CCHashtbl.Make(struct
+module H = Hashcons.Make(struct
-    type t = ty_view
+    type t = ty
-    let equal a b = match a, b with
+    let equal a b = match a.ty_view, b.ty_view with
       | Ty_prop, Ty_prop -> true
       | Ty_atomic a1, Ty_atomic a2 ->
         equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
       | Ty_prop, _ | Ty_atomic _, _
        -> false
 
-    let hash t = match t with
+    let hash t = match t.ty_view with
       | Ty_prop -> 1
       | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
         Hash.combine3 10 (ID.hash id) (Hash.list hash args)
       | Ty_atomic {def=Ty_def d; args; _} ->
         Hash.combine3 20 (ID.hash d.id) (Hash.list hash args)
+
+    let set_id ty id =
+      assert (ty.ty_id < 0);
+      ty.ty_id <- id
   end)
 
 (* build a type *)
 let make_ : ty_view -> t =
-  let tbl : t Tbl_cell.t = Tbl_cell.create 128 in
+  let tbl : H.t = H.create ~size:128 () in
-  let n = ref 0 in
+  fun[@inline] c ->
-  fun c ->
+    let ty = {ty_id= -1; ty_view=c; } in
-    try Tbl_cell.find tbl c
+    H.hashcons tbl ty
-    with Not_found ->
-      let ty_id = !n in
-      incr n;
-      let ty = {ty_id; ty_view=c; } in
-      Tbl_cell.add tbl c ty;
-      ty
 
 let card t = match view t with
   | Ty_prop -> Finite