From ac030641db3a31d22f227741ad4f1906d7e54f4b Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 16 Feb 2019 15:23:57 -0600
Subject: [PATCH] refactor(ty): use `Hashcons` with weak table for types

---
 src/smt/Ty.ml | 26 ++++++++++++--------------
 1 file changed, 12 insertions(+), 14 deletions(-)

diff --git a/src/smt/Ty.ml b/src/smt/Ty.ml
index f175044e..cbef42b0 100644
--- a/src/smt/Ty.ml
+++ b/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
-    type t = ty_view
-    let equal a b = match a, b with
+module H = Hashcons.Make(struct
+    type t = ty
+    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 n = ref 0 in
-  fun c ->
-    try Tbl_cell.find tbl c
-    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 tbl : H.t = H.create ~size:128 () in
+  fun[@inline] c ->
+    let ty = {ty_id= -1; ty_view=c; } in
+    H.hashcons tbl ty
 
 let card t = match view t with
   | Ty_prop -> Finite