From 13580590d3102de0ed80b67b4fffb41bf72ed541 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 12 Nov 2024 11:38:19 +0100
Subject: [PATCH 1/3] Remove mutable field `value` in `tvar`

We do not need a value field in the type variable of Alt-Ergo.
These values were only used by the unification of the types in the legacy
typechecker.
---
 src/lib/structures/expr.ml |  2 +-
 src/lib/structures/ty.ml   | 95 ++++++++------------------------------
 src/lib/structures/ty.mli  |  4 +-
 3 files changed, 20 insertions(+), 81 deletions(-)

diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 2b05a3d49..864b6eabc 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -1782,7 +1782,7 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } =
 
 let free_type_vars_as_types e =
   Ty.Svty.fold
-    (fun i z -> Ty.Set.add (Ty.Tvar {Ty.v=i; value = None}) z)
+    (fun v z -> Ty.Set.add (Ty.Tvar { v }) z)
     (free_type_vars e) Ty.Set.empty
 
 
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 31716e50a..72d30e22d 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -38,7 +38,7 @@ type t =
   | Tadt of DE.ty_cst * t list
   | Trecord of trecord
 
-and tvar = { v : int ; mutable value : t option }
+and tvar = { v : int } [@@unboxed]
 
 and trecord = {
   mutable args : t list;
@@ -62,14 +62,12 @@ module Smtlib = struct
     | Text (args, name)
     | Trecord { args; name; _ } | Tadt (name, args) ->
       Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args)
-    | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v
-    | Tvar { value = Some t; _ } -> pp ppf t
+    | Tvar { v } -> Fmt.pf ppf "A%d" v
 end
 
 let pp_smtlib = Smtlib.pp
 
 exception TypeClash of t*t
-exception Shorten of t
 
 type adt_constr =
   { constr : DE.term_cst ;
@@ -96,7 +94,6 @@ let assoc_destrs hs cases =
 
 (*** pretty print ***)
 let print_generic body_of =
-  let h = Hashtbl.create 17 in
   let rec print =
     let open Format in
     fun body_of fmt -> function
@@ -104,17 +101,7 @@ let print_generic body_of =
       | Treal -> fprintf fmt "real"
       | Tbool -> fprintf fmt "bool"
       | Tbitv n -> fprintf fmt "bitv[%d]" n
-      | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v
-      | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } ->
-        if Hashtbl.mem h v then
-          fprintf fmt "%a %a" print_list l DE.Ty.Const.print n
-        else
-          (Hashtbl.add h v ();
-           (*fprintf fmt "('a_%d->%a)" v print t *)
-           print body_of fmt t)
-      | Tvar{ value = Some t; _ } ->
-        (*fprintf fmt "('a_%d->%a)" v print t *)
-        print body_of fmt t
+      | Tvar{ v } -> fprintf fmt "'a_%d" v
       | Text(l, s) when l == [] ->
         fprintf fmt "<ext>%a" DE.Ty.Const.print s
       | Text(l,s) ->
@@ -190,47 +177,12 @@ let print      = fst (print_generic None) None
 
 let fresh_var =
   let cpt = ref (-1) in
-  fun () -> incr cpt; {v= !cpt ; value = None }
+  fun () -> incr cpt; { v = !cpt }
 
 let fresh_tvar () = Tvar (fresh_var ())
 
-let rec shorten ty =
-  match ty with
-  | Tvar { value = None; _ }  -> ty
-  | Tvar { value = Some (Tvar{ value = None; _ } as t'); _ } -> t'
-  | Tvar ({ value = Some (Tvar t2); _ } as t1) ->
-    t1.value <- t2.value; shorten ty
-  | Tvar { value = Some t'; _ } -> shorten t'
-
-  | Text (l,s) ->
-    let l, same = My_list.apply shorten l in
-    if same then ty else Text(l,s)
-
-  | Tfarray (t1,t2) ->
-    let t1' = shorten t1 in
-    let t2' = shorten t2 in
-    if t1 == t1' && t2 == t2' then ty
-    else Tfarray(t1', t2')
-
-  | Trecord r ->
-    r.args <- List.map shorten r.args;
-    r.lbs <- List.map (fun (lb, ty) -> lb, shorten ty) r.lbs;
-    ty
-
-  | Tadt (n, args) ->
-    let args' = List.map shorten args in
-    shorten_body n args;
-    (* should not rebuild the type if no changes are made *)
-    Tadt (n, args')
-
-  | Tint | Treal | Tbool | Tbitv _ -> ty
-
-and shorten_body _ _ =
-  ()
-  [@ocaml.ppwarning "TODO: should be implemented ?"]
-
 let rec compare t1 t2 =
-  match shorten t1 , shorten t2 with
+  match t1, t2 with
   | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Int.compare v1 v2
   | Tvar _, _ -> -1 | _ , Tvar _ -> 1
   | Text(l1, s1) , Text(l2, s2) ->
@@ -282,8 +234,8 @@ and compare_list l1 l2 = match l1, l2 with
 
 let rec equal t1 t2 =
   t1 == t2 ||
-  match shorten t1 , shorten t2 with
-  | Tvar{ v = v1; _ }, Tvar{ v = v2; _ } -> v1 = v2
+  match t1, t2 with
+  | Tvar{ v = v1 }, Tvar{ v = v2 } -> v1 = v2
   | Text(l1, s1), Text(l2, s2) ->
     (try DE.Ty.Const.equal s1 s2 && List.for_all2 equal l1 l2
      with Invalid_argument _ -> false)
@@ -319,10 +271,12 @@ let esubst = M.empty
 
 let rec matching s pat t =
   match pat , t with
-  | Tvar {v=n;value=None} , _ ->
-    (try if not (equal (M.find n s) t) then raise (TypeClash(pat,t)); s
-     with Not_found -> M.add n t s)
-  | Tvar { value = _; _ }, _ -> raise (Shorten pat)
+  | Tvar { v } , _ ->
+    (try
+       if not (equal (M.find v s) t) then
+         raise (TypeClash(pat,t));
+       s
+     with Not_found -> M.add v t s)
   | Text (l1,s1) , Text (l2,s2) when DE.Ty.Const.equal s1 s2 ->
     List.fold_left2 matching s l1 l2
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
@@ -375,17 +329,12 @@ let apply_subst =
 (* Assume that [shorten] have been applied on [ty]. *)
 let rec fresh ty subst =
   match ty with
-  | Tvar { value = Some _; _ } ->
-    (* This case is eliminated by the normalization performed
-       in [shorten]. *)
-    assert false
-
-  | Tvar { v= x; _ } ->
+  | Tvar { v } ->
     begin
-      try M.find x subst, subst
+      try M.find v subst, subst
       with Not_found ->
         let nv = Tvar (fresh_var()) in
-        nv, M.add x nv subst
+        nv, M.add v nv subst
     end
   | Text (args, n) ->
     let args, subst = fresh_list args subst in
@@ -415,10 +364,6 @@ and fresh_list lty subst =
        let ty, subst = fresh ty subst in
        ty::lty, subst) lty ([], subst)
 
-let fresh ty subst = fresh (shorten ty) subst
-
-let fresh_list lty subst = fresh_list (List.map shorten lty) subst
-
 module Decls = struct
 
   module MH = Map.Make (DE.Ty.Const)
@@ -480,10 +425,8 @@ module Decls = struct
           try
             List.fold_left2
               (fun sbt vty ty ->
-                 let vty = shorten vty in
                  match vty with
-                 | Tvar { value = Some _ ; _ } -> assert false
-                 | Tvar {v ; value = None}   ->
+                 | Tvar { v } ->
                    if equal vty ty then sbt else M.add v ty sbt
                  | _ ->
                    Printer.print_err "vty = %a and ty = %a"
@@ -599,9 +542,8 @@ module Set =
 
 let vty_of t =
   let rec vty_of_rec acc t =
-    let t = shorten t in
     match t with
-    | Tvar { v = i ; value = None } -> Svty.add i acc
+    | Tvar { v = i } -> Svty.add i acc
     | Text(l,_) -> List.fold_left vty_of_rec acc l
     | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2
     | Trecord { args; lbs; _ } ->
@@ -610,7 +552,6 @@ let vty_of t =
     | Tadt(_, args) ->
       List.fold_left vty_of_rec acc args
 
-    | Tvar { value = Some _ ; _ }
     | Tint | Treal | Tbool | Tbitv _ ->
       acc
   in
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 4bb69218b..c9baf48f4 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -66,9 +66,7 @@ type t =
 and tvar = {
   v : int;
   (** Unique identifier *)
-  mutable value : t option;
-  (** Pointer to the current value of the type variable. *)
-}
+} [@@unboxed]
 (** Type variables.
     The [value] field is mutated during unification,
     hence distinct types should have disjoints sets of

From 46240f54f5849e9a17db6010cfb15ee9d92b5a14 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Fri, 25 Oct 2024 12:42:55 +0200
Subject: [PATCH 2/3] Use type variables of Dolmen directly

---
 src/lib/frontend/translate.ml | 14 +++---
 src/lib/structures/expr.ml    | 90 +++++++++++++++++------------------
 src/lib/structures/expr.mli   |  4 +-
 src/lib/structures/ty.ml      | 71 +++++++++++++--------------
 src/lib/structures/ty.mli     | 30 ++++--------
 5 files changed, 94 insertions(+), 115 deletions(-)

diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml
index 7455aacdd..0b3f5c803 100644
--- a/src/lib/frontend/translate.ml
+++ b/src/lib/frontend/translate.ml
@@ -523,8 +523,8 @@ and handle_ty_app ?(update = false) ty_c l =
      variable. *)
   let rec apply_ty_substs tysubsts ty =
     match ty with
-    | Ty.Tvar { v; _ } ->
-      Ty.M.find v tysubsts
+    | Ty.Tvar v ->
+      Ty.TvMap.find v tysubsts
 
     | Text (tyl, hs) ->
       Ty.Text (List.map (apply_ty_substs tysubsts) tyl, hs)
@@ -561,9 +561,9 @@ and handle_ty_app ?(update = false) ty_c l =
       List.fold_left2 (
         fun acc tv ty ->
           match tv with
-          | Ty.Tvar { v; _ } -> Ty.M.add v ty acc
+          | Ty.Tvar v -> Ty.TvMap.add v ty acc
           | _ -> assert false
-      ) Ty.M.empty args tyl
+      ) Ty.TvMap.empty args tyl
     in
     apply_ty_substs tysubsts ty
 
@@ -1749,7 +1749,7 @@ let make_form name_base f loc ~decl_kind =
   in
   assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
   let ff = E.purify_form ff in
-  if Ty.Svty.is_empty (E.free_type_vars ff) then ff
+  if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
   else
     E.mk_forall name_base loc Var.Map.empty [] ff ~toplevel:true ~decl_kind
 
@@ -2005,7 +2005,7 @@ let make dloc_file acc stmt =
                 assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
                 let ff = E.purify_form ff in
                 let e =
-                  if Ty.Svty.is_empty (E.free_type_vars ff) then ff
+                  if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
                   else
                     E.mk_forall name_base loc
                       Var.Map.empty [] ff ~toplevel:true ~decl_kind
@@ -2026,7 +2026,7 @@ let make dloc_file acc stmt =
                 assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
                 let ff = E.purify_form ff in
                 let e =
-                  if Ty.Svty.is_empty (E.free_type_vars ff) then ff
+                  if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
                   else
                     E.mk_forall name_base loc
                       Var.Map.empty [] ff ~toplevel:true ~decl_kind
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 864b6eabc..778659801 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -42,7 +42,7 @@ and term_view = {
   bind : bind_kind;
   tag: int;
   vars : (Ty.t * int) Var.Map.t; (* vars to types and nb of occurences *)
-  vty : Ty.Svty.t;
+  vty : Ty.TvSet.t;
   depth: int;
   nb_nodes : int;
   pure : bool;
@@ -244,11 +244,11 @@ module Msbt : Map.S with type key = expr Var.Map.t =
       let compare a b = Var.Map.compare compare a b
     end)
 
-module Msbty : Map.S with type key = Ty.t Ty.M.t =
+module Msbty : Map.S with type key = Ty.subst =
   Map.Make
     (struct
-      type t = Ty.t Ty.M.t
-      let compare a b = Ty.M.compare Ty.compare a b
+      type t = Ty.subst
+      let compare = Ty.compare_subst
     end)
 
 module TSet : Set.S with type elt = expr =
@@ -335,7 +335,7 @@ module SmtPrinter = struct
 
   (* This printer follows the convention used to print
      type variables in the module [Ty]. *)
-  let pp_tyvar ppf v = Fmt.pf ppf "A%d" v
+  let pp_tvar ppf v = Fmt.pf ppf "A%a" DE.Ty.Var.print v
 
   let rec pp_main bind ppf { user_trs; main; binders; _ } =
     if not @@ Var.Map.is_empty binders then
@@ -348,9 +348,9 @@ module SmtPrinter = struct
       pp_boxed ppf main
 
   and pp_quantified bind ppf q =
-    if q.toplevel && not @@ Ty.Svty.is_empty q.main.vty then
+    if q.toplevel && not @@ Ty.TvSet.is_empty q.main.vty then
       Fmt.pf ppf "@[<2>(par (%a)@, %a)@]"
-        Fmt.(box @@ iter ~sep:sp Ty.Svty.iter pp_tyvar) q.main.vty
+        Fmt.(box @@ iter ~sep:sp Ty.TvSet.iter pp_tvar) q.main.vty
         (pp_main bind) q
     else
       pp_main bind ppf q
@@ -802,7 +802,7 @@ let free_type_vars t = t.vty
 
 let is_ground t =
   Var.Map.is_empty (free_vars t Var.Map.empty) &&
-  Ty.Svty.is_empty (free_type_vars t)
+  Ty.TvSet.is_empty (free_type_vars t)
 
 let size t = t.nb_nodes
 
@@ -876,7 +876,7 @@ let free_vars_non_form s l ty =
   | _, e::r -> List.fold_left (fun s t -> merge_vars s t.vars) e.vars r
 
 let free_type_vars_non_form l ty =
-  List.fold_left (fun acc t -> Ty.Svty.union acc t.vty) (Ty.vty_of ty) l
+  List.fold_left (fun acc t -> Ty.TvSet.union acc t.vty) (Ty.vty_of ty) l
 
 let is_ite s = match s with
   | Sy.Op Sy.Tite -> true
@@ -960,7 +960,7 @@ let vrai =
   let res =
     let nb_nodes = 0 in
     let vars = Var.Map.empty in
-    let vty = Ty.Svty.empty in
+    let vty = Ty.TvSet.empty in
     let faux =
       HC.make
         {f = Sy.False; xs = []; ty = Ty.Tbool; depth = -2; (*smallest depth*)
@@ -1040,7 +1040,7 @@ let mk_or f1 f2 is_impl =
     let d = (max f1.depth f2.depth) in (* the +1 causes regression *)
     let nb_nodes = f1.nb_nodes + f2.nb_nodes + 1 in
     let vars = merge_vars f1.vars f2.vars in
-    let vty = Ty.Svty.union f1.vty f2.vty in
+    let vty = Ty.TvSet.union f1.vty f2.vty in
     let pos =
       HC.make {f=Sy.Form (Sy.F_Clause is_impl); xs=[f1; f2]; ty=Ty.Tbool;
                depth=d; tag= -42; vars; vty; nb_nodes; neg = None;
@@ -1070,7 +1070,7 @@ let mk_iff f1 f2 =
     let d = (max f1.depth f2.depth) in (* the +1 causes regression *)
     let nb_nodes = f1.nb_nodes + f2.nb_nodes + 1 in
     let vars = merge_vars f1.vars f2.vars in
-    let vty = Ty.Svty.union f1.vty f2.vty in
+    let vty = Ty.TvSet.union f1.vty f2.vty in
     let pos =
       HC.make {f=Sy.Form Sy.F_Iff; xs=[f1; f2]; ty=Ty.Tbool;
                depth=d; tag= -42; vars; vty; nb_nodes; neg = None;
@@ -1156,7 +1156,7 @@ let mk_forall_ter =
            lemma. Otherwise (if not toplevel), the free vtys of the lemma
            are those of lem.main *)
         let vty =
-          if new_q.toplevel then Ty.Svty.empty
+          if new_q.toplevel then Ty.TvSet.empty
           else free_type_vars new_q.main
         in
         let vars =
@@ -1191,7 +1191,7 @@ let no_occur_check v e =
   not (Var.Map.mem v e.vars)
 
 let no_vtys l =
-  List.for_all (fun e -> Ty.Svty.is_empty e.vty) l
+  List.for_all (fun e -> Ty.TvSet.is_empty e.vty) l
 
 (** smart constructors for literals *)
 
@@ -1356,12 +1356,12 @@ let no_capture_issue s_t binders =
     end
 
 let rec apply_subst_aux (s_t, s_ty) t =
-  if is_ground t || (Var.Map.is_empty s_t && Ty.M.is_empty s_ty) then t
+  if is_ground t || (Var.Map.is_empty s_t && Ty.TvMap.is_empty s_ty) then t
   else
     let { f; xs; ty; vars; vty; bind; _ } = t in
     let s_t = Var.Map.filter (fun v _ -> Var.Map.mem v vars) s_t in
-    let s_ty = Ty.M.filter (fun tvar _ -> Ty.Svty.mem tvar vty) s_ty in
-    if Var.Map.is_empty s_t && Ty.M.is_empty s_ty then t
+    let s_ty = Ty.TvMap.filter (fun tvar _ -> Ty.TvSet.mem tvar vty) s_ty in
+    if Var.Map.is_empty s_t && Ty.TvMap.is_empty s_ty then t
     else
       let s = s_t, s_ty in
       let xs', same = My_list.apply (apply_subst_aux s) xs in
@@ -1501,7 +1501,7 @@ and mk_let_aux ({ let_v; let_e; in_e; _ } as x) =
       let nb_nodes = let_e.nb_nodes + in_e.nb_nodes + 1 (* approx *) in
       (* do not include free vars in let_sko that have been simplified *)
       let vars = merge_vars let_e.vars (Var.Map.remove let_v in_e.vars) in
-      let vty = Ty.Svty.union let_e.vty in_e.vty in
+      let vty = Ty.TvSet.union let_e.vty in_e.vty in
       let pos =
         HC.make {f=Sy.Let; xs=[]; ty;
                  depth=d; tag= -42; vars; vty; nb_nodes; neg = None;
@@ -1524,7 +1524,7 @@ and mk_forall_bis (q : quantified) =
   let binders =  (* ignore binders that are not used in f *)
     Var.Map.filter (fun v _ -> Var.Map.mem v q.main.vars) q.binders
   in
-  if Var.Map.is_empty binders && Ty.Svty.is_empty q.main.vty then q.main
+  if Var.Map.is_empty binders && Ty.TvSet.is_empty q.main.vty then q.main
   else
     let q = {q with binders} in
     (* Attempt to reduce the number of quantifiers. We try to find a
@@ -1582,7 +1582,7 @@ and find_particular_subst =
   in
   fun binders trs f ->
     (* TODO: move the test for `trs` outside. *)
-    if not (Ty.Svty.is_empty f.vty) || has_hypotheses trs ||
+    if not (Ty.TvSet.is_empty f.vty) || has_hypotheses trs ||
        has_semantic_triggers trs
     then
       None
@@ -1699,7 +1699,7 @@ let resolution_of_literal a binders free_vty acc =
   match lit_view a with
   | Pred(t, _) ->
     let cond =
-      Ty.Svty.subset free_vty (free_type_vars t) &&
+      Ty.TvSet.subset free_vty (free_type_vars t) &&
       let vars = free_vars t Var.Map.empty in
       Var.Map.for_all (fun v _ -> Var.Map.mem v vars) binders
     in
@@ -1781,8 +1781,8 @@ let resolution_triggers ~is_back { kind; main = f; binders; _ } =
         )cand []
 
 let free_type_vars_as_types e =
-  Ty.Svty.fold
-    (fun v z -> Ty.Set.add (Ty.Tvar { v }) z)
+  Ty.TvSet.fold
+    (fun tv z -> Ty.Set.add (Ty.Tvar tv) z)
     (free_type_vars e) Ty.Set.empty
 
 
@@ -1806,7 +1806,7 @@ let mk_let let_v let_e in_e =
 
 let skolemize { main = f; binders; sko_v; sko_vty; _ } =
   let print fmt ty =
-    assert (Ty.Svty.is_empty (Ty.vty_of ty));
+    assert (Ty.TvSet.is_empty (Ty.vty_of ty));
     Format.fprintf fmt "<%a>" Ty.print ty
   in
   let pp_sep_nospace fmt () = Format.fprintf fmt "" in
@@ -1928,13 +1928,11 @@ let elim_iff f1 f2 ~with_conj =
 
 module Triggers = struct
 
-  module Svty = Ty.Svty
-
   (* Set of patterns with their sets of free term and type variables. *)
   module STRS =
     Set.Make(
     struct
-      type t = expr * Var.Set.t * Svty.t
+      type t = expr * Var.Set.t * Ty.TvSet.t
 
       let compare (t1,_,_) (t2,_,_) = compare t1 t2
     end)
@@ -2105,7 +2103,7 @@ module Triggers = struct
     fun l ->
       unique (List.stable_sort cmp_trig_term_list l) []
 
-  let vty_of_term acc t = Svty.union acc t.vty
+  let vty_of_term acc t = Ty.TvSet.union acc t.vty
 
   let not_pure t = not t.pure
 
@@ -2126,11 +2124,11 @@ module Triggers = struct
             variables. *)
          not (List.exists not_pure l) &&
          let s1 = List.fold_left (vars_of_term bv) Var.Set.empty l in
-         let s2 = List.fold_left vty_of_term Svty.empty l in
+         let s2 = List.fold_left vty_of_term Ty.TvSet.empty l in
          (* TODO: we can replace `Var.Set.subset bv s1`
             by `Var.Seq.equal bv s1`. By construction `s1` is
             a subset of `bv`. *)
-         Var.Set.subset bv s1 && Svty.subset vty s2 )
+         Var.Set.subset bv s1 && Ty.TvSet.subset vty s2 )
       trs
 
   (* unused
@@ -2142,8 +2140,8 @@ module Triggers = struct
         if List.exists not_pure l then
           failwith "If-Then-Else are not allowed in (theory triggers)";
         let s1 = List.fold_left (vars_of_term bv) SSet.empty l in
-        let s2 = List.fold_left vty_of_term Svty.empty l in
-        if not (Svty.subset vty s2) || not (SSet.subset bv s1) then
+        let s2 = List.fold_left vty_of_term Ty.TvSet.empty l in
+        if not (Ty.TvSet.subset vty s2) || not (SSet.subset bv s1) then
           failwith "Triggers of a theory should contain every quantified \
                     types and variables.")
       trs;
@@ -2171,7 +2169,7 @@ module Triggers = struct
   module SLLT =
     Set.Make(
     struct
-      type t = expr list * Var.Set.t * Svty.t
+      type t = expr list * Var.Set.t * Ty.TvSet.t
       let compare (a, y1, _) (b, y2, _)  =
         let c = try compare_lists a b compare; 0 with Util.Cmp c -> c in
         if c <> 0 then c else Var.Set.compare y1 y2
@@ -2222,14 +2220,14 @@ module Triggers = struct
         let llt, llt_ok =
           SLLT.fold
             (fun (l, bv2, vty2) (llt, llt_ok) ->
-               if Var.Set.subset bv1 bv2 && Svty.subset vty1 vty2 then
+               if Var.Set.subset bv1 bv2 && Ty.TvSet.subset vty1 vty2 then
                  (* t doesn't bring new vars *)
                  llt, llt_ok
                else
                  let bv3 = Var.Set.union bv2 bv1 in
-                 let vty3 = Svty.union vty2 vty1 in
+                 let vty3 = Ty.TvSet.union vty2 vty1 in
                  let e = t::l, bv3, vty3 in
-                 if Var.Set.subset bv bv3 && Svty.subset vty vty3 then
+                 if Var.Set.subset bv bv3 && Ty.TvSet.subset vty vty3 then
                    (* The multi-trigger [e] cover all the free variables [bv]
                       and [vty]. *)
                    llt, SLLT.add e llt_ok
@@ -2258,17 +2256,17 @@ module Triggers = struct
       List.exists
         (fun (_, bv',vty') ->
            (Var.Set.subset bv bv' && not(Var.Set.equal bv bv')
-            && Svty.subset vty vty')
-           || (Svty.subset vty vty' && not(Svty.equal vty vty')
+            && Ty.TvSet.subset vty vty')
+           || (Ty.TvSet.subset vty vty' && not(Ty.TvSet.equal vty vty')
                && Var.Set.subset bv bv') ) l
     in fun bv_a vty_a l ->
       let rec simpl_rec acc = function
         | [] -> acc
         | ((_, bv, vty) as e)::l ->
           if strict_subset bv vty l || strict_subset bv vty acc ||
-             (Var.Set.subset bv_a bv && Svty.subset vty_a vty) ||
+             (Var.Set.subset bv_a bv && Ty.TvSet.subset vty_a vty) ||
              (Var.Set.equal (Var.Set.inter bv_a bv) Var.Set.empty &&
-              Svty.equal (Svty.inter vty_a vty) Svty.empty)
+              Ty.TvSet.equal (Ty.TvSet.inter vty_a vty) Ty.TvSet.empty)
           then simpl_rec acc l
           else simpl_rec (e::acc) l
       in
@@ -2294,7 +2292,7 @@ module Triggers = struct
        and [vtype]. *)
     let mono = List.filter
         (fun (_, bv_t, vty_t) ->
-           Var.Set.subset vterm bv_t && Svty.subset vtype vty_t) trs
+           Var.Set.subset vterm bv_t && Ty.TvSet.subset vtype vty_t) trs
     in
     let trs_v, trs_nv = List.partition (fun (t, _, _) -> is_var t) mono in
     let base = if menv.Util.triggers_var then trs_nv @ trs_v else trs_nv in
@@ -2383,7 +2381,7 @@ module Triggers = struct
       Var.Map.exists (fun e _ -> Var.Set.mem e bv) bv_lf
     in
     let has_tyvar vty vty_lf =
-      Svty.exists (fun e -> Svty.mem e vty) vty_lf
+      Ty.TvSet.exists (fun e -> Ty.TvSet.mem e vty) vty_lf
     in
     let args_of e lets =
       match e.bind with
@@ -2479,9 +2477,9 @@ module Triggers = struct
       )terms terms
 
   let check_user_triggers f toplevel binders trs0 ~decl_kind =
-    if Var.Map.is_empty binders && Ty.Svty.is_empty f.vty then trs0
+    if Var.Map.is_empty binders && Ty.TvSet.is_empty f.vty then trs0
     else
-      let vtype = if toplevel then f.vty else Ty.Svty.empty in
+      let vtype = if toplevel then f.vty else Ty.TvSet.empty in
       let vterm =
         Var.Map.fold (fun v _ s -> Var.Set.add v s) binders Var.Set.empty
       in
@@ -2498,7 +2496,7 @@ module Triggers = struct
         filter_good_triggers (vterm, vtype) trs0
 
   let make f binders decl_kind mconf =
-    if Var.Map.is_empty binders && Ty.Svty.is_empty f.vty then []
+    if Var.Map.is_empty binders && Ty.TvSet.is_empty f.vty then []
     else
       let vtype = f.vty in
       let vterm =
@@ -2604,7 +2602,7 @@ let mk_forall name loc binders trs f ~toplevel ~decl_kind =
      user_trs = trs; main = f; sko_v; sko_vty; kind = decl_kind}
 
 let mk_exists name loc binders trs f ~toplevel ~decl_kind =
-  if not toplevel || Ty.Svty.is_empty f.vty then
+  if not toplevel || Ty.TvSet.is_empty f.vty then
     neg (mk_forall name loc binders trs (neg f) ~toplevel ~decl_kind)
   else
     (* If there are type variables in a toplevel exists: 1 - we add
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 6dec2b1ab..bb0460449 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -49,7 +49,7 @@ type term_view = private {
   (** Map of free term variables in the term to their type and
       number of occurrences. *)
 
-  vty : Ty.Svty.t;
+  vty : Ty.TvSet.t;
   (** Map of free type variables in the term. *)
 
   depth: int;
@@ -222,7 +222,7 @@ val compare_let : letin -> letin -> int
 
 (** Some auxiliary functions *)
 val free_vars : t -> (Ty.t * int) Var.Map.t -> (Ty.t * int) Var.Map.t
-val free_type_vars : t -> Ty.Svty.t
+val free_type_vars : t -> Ty.TvSet.t
 val is_ground : t -> bool
 val size : t -> int
 val depth : t -> int
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 72d30e22d..1d1fd4730 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -27,6 +27,11 @@
 
 module DE = Dolmen.Std.Expr
 
+module TvSet = Set.Make (DE.Ty.Var)
+module TvMap = Map.Make (DE.Ty.Var)
+
+type tvar = DE.ty_var
+
 type t =
   | Tint
   | Treal
@@ -38,8 +43,6 @@ type t =
   | Tadt of DE.ty_cst * t list
   | Trecord of trecord
 
-and tvar = { v : int } [@@unboxed]
-
 and trecord = {
   mutable args : t list;
   name : DE.ty_cst;
@@ -62,7 +65,7 @@ module Smtlib = struct
     | Text (args, name)
     | Trecord { args; name; _ } | Tadt (name, args) ->
       Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args)
-    | Tvar { v } -> Fmt.pf ppf "A%d" v
+    | Tvar tv -> DE.Ty.Var.print ppf tv
 end
 
 let pp_smtlib = Smtlib.pp
@@ -101,7 +104,7 @@ let print_generic body_of =
       | Treal -> fprintf fmt "real"
       | Tbool -> fprintf fmt "bool"
       | Tbitv n -> fprintf fmt "bitv[%d]" n
-      | Tvar{ v } -> fprintf fmt "'a_%d" v
+      | Tvar tv -> fprintf fmt "'a_%a" DE.Ty.Var.print tv
       | Text(l, s) when l == [] ->
         fprintf fmt "<ext>%a" DE.Ty.Const.print s
       | Text(l,s) ->
@@ -174,16 +177,11 @@ let print_generic body_of =
 let print_list = snd (print_generic None)
 let print      = fst (print_generic None) None
 
-
-let fresh_var =
-  let cpt = ref (-1) in
-  fun () -> incr cpt; { v = !cpt }
-
-let fresh_tvar () = Tvar (fresh_var ())
+let fresh_tvar () = Tvar (DE.Ty.Var.mk "A")
 
 let rec compare t1 t2 =
   match t1, t2 with
-  | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Int.compare v1 v2
+  | Tvar v1, Tvar v2 -> DE.Ty.Var.compare v1 v2
   | Tvar _, _ -> -1 | _ , Tvar _ -> 1
   | Text(l1, s1) , Text(l2, s2) ->
     let c = DE.Ty.Const.compare s1 s2 in
@@ -235,7 +233,7 @@ and compare_list l1 l2 = match l1, l2 with
 let rec equal t1 t2 =
   t1 == t2 ||
   match t1, t2 with
-  | Tvar{ v = v1 }, Tvar{ v = v2 } -> v1 = v2
+  | Tvar v1, Tvar v2 -> DE.Ty.Var.equal v1 v2
   | Text(l1, s1), Text(l2, s2) ->
     (try DE.Ty.Const.equal s1 s2 && List.for_all2 equal l1 l2
      with Invalid_argument _ -> false)
@@ -264,19 +262,18 @@ let rec equal t1 t2 =
   | _ -> false
 
 (*** matching with a substitution mechanism ***)
-module M = Util.MI
-type subst = t M.t
+type subst = t TvMap.t
 
-let esubst = M.empty
+let esubst = TvMap.empty
 
 let rec matching s pat t =
   match pat , t with
-  | Tvar { v } , _ ->
+  | Tvar v , _ ->
     (try
-       if not (equal (M.find v s) t) then
-         raise (TypeClash(pat,t));
+       if not (equal (TvMap.find v s) t) then
+         raise (TypeClash (pat,t));
        s
-     with Not_found -> M.add v t s)
+     with Not_found -> TvMap.add v t s)
   | Text (l1,s1) , Text (l2,s2) when DE.Ty.Const.equal s1 s2 ->
     List.fold_left2 matching s l1 l2
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
@@ -295,8 +292,8 @@ let rec matching s pat t =
 let apply_subst =
   let rec apply_subst s ty =
     match ty with
-    | Tvar { v= n; _ } ->
-      (try M.find n s with Not_found -> ty)
+    | Tvar v ->
+      (try TvMap.find v s with Not_found -> ty)
 
     | Text (l,e) ->
       let l, same = My_list.apply (apply_subst s) l in
@@ -324,17 +321,16 @@ let apply_subst =
 
     | Tint | Treal | Tbool | Tbitv _ -> ty
   in
-  fun s ty -> if M.is_empty s then ty else apply_subst s ty
+  fun s ty -> if TvMap.is_empty s then ty else apply_subst s ty
 
-(* Assume that [shorten] have been applied on [ty]. *)
 let rec fresh ty subst =
   match ty with
-  | Tvar { v } ->
+  | Tvar v ->
     begin
-      try M.find v subst, subst
+      try TvMap.find v subst, subst
       with Not_found ->
-        let nv = Tvar (fresh_var()) in
-        nv, M.add v nv subst
+        let nv = fresh_tvar () in
+        nv, TvMap.add v nv subst
     end
   | Text (args, n) ->
     let args, subst = fresh_list args subst in
@@ -357,7 +353,6 @@ let rec fresh ty subst =
     Tadt (s, args), subst
   | t -> t, subst
 
-(* Assume that [shorten] have been applied on [lty]. *)
 and fresh_list lty subst =
   List.fold_right
     (fun ty (lty, subst) ->
@@ -426,13 +421,13 @@ module Decls = struct
             List.fold_left2
               (fun sbt vty ty ->
                  match vty with
-                 | Tvar { v } ->
-                   if equal vty ty then sbt else M.add v ty sbt
+                 | Tvar v ->
+                   if equal vty ty then sbt else TvMap.add v ty sbt
                  | _ ->
                    Printer.print_err "vty = %a and ty = %a"
                      print vty print ty;
                    assert false
-              )M.empty params args
+              ) TvMap.empty params args
           with Invalid_argument _ -> assert false
         in
         let cases =
@@ -507,7 +502,7 @@ let trecord ~record_constr lv name lbs =
 
 let rec hash t =
   match t with
-  | Tvar{ v; _ } -> v
+  | Tvar tv -> DE.Ty.Var.hash tv
   | Text(l,s) ->
     abs (List.fold_left (fun acc x-> acc*19 + hash x) (DE.Ty.Const.hash s) l)
   | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2)
@@ -527,9 +522,9 @@ let rec hash t =
 
   | _ -> Hashtbl.hash t
 
-let compare_subst = M.compare compare
+let compare_subst = TvMap.compare compare
 
-let equal_subst = M.equal equal
+let equal_subst = TvMap.equal equal
 
 module Svty = Util.SI
 
@@ -543,8 +538,8 @@ module Set =
 let vty_of t =
   let rec vty_of_rec acc t =
     match t with
-    | Tvar { v = i } -> Svty.add i acc
-    | Text(l,_) -> List.fold_left vty_of_rec acc l
+    | Tvar tv -> TvSet.add tv acc
+    | Text (l,_) -> List.fold_left vty_of_rec acc l
     | Tfarray (t1,t2) -> vty_of_rec (vty_of_rec acc t1) t2
     | Trecord { args; lbs; _ } ->
       let acc = List.fold_left vty_of_rec acc args in
@@ -555,12 +550,12 @@ let vty_of t =
     | Tint | Treal | Tbool | Tbitv _ ->
       acc
   in
-  vty_of_rec Svty.empty t
+  vty_of_rec TvSet.empty t
 
 let print_subst =
   let sep ppf () = Fmt.pf ppf " -> " in
   Fmt.(box @@ braces
-       @@ iter_bindings ~sep:comma M.iter (pair ~sep int print))
+       @@ iter_bindings ~sep:comma TvMap.iter (pair ~sep DE.Ty.Var.print print))
 
 let print_full =
   fst (print_generic (Some type_body)) (Some type_body)
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index c9baf48f4..168c95b69 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -31,6 +31,12 @@
 
 (** {2 Definition} *)
 
+type tvar = Dolmen.Std.Expr.ty_var
+(** Type of type variable. *)
+
+module TvSet : Set.S with type elt = tvar
+module TvMap : Map.S with type key = tvar
+
 type t =
   | Tint
   (** Integer numbers *)
@@ -63,15 +69,6 @@ type t =
   | Trecord of trecord
   (** Record type. *)
 
-and tvar = {
-  v : int;
-  (** Unique identifier *)
-} [@@unboxed]
-(** Type variables.
-    The [value] field is mutated during unification,
-    hence distinct types should have disjoints sets of
-    type variables (see function {!val:fresh}). *)
-
 and trecord = {
   mutable args : t list;
   (** Arguments passed to the record constructor *)
@@ -100,13 +97,9 @@ type adt_constr =
     for recursive ADTs *)
 type type_body = adt_constr list
 
-module Svty : Set.S with type elt = int
-(** Sets of type variables, indexed by their identifier. *)
-
 module Set : Set.S with type elt = t
 (** Sets of types *)
 
-
 val assoc_destrs :
   Dolmen.Std.Expr.term_cst ->
   adt_constr list ->
@@ -142,7 +135,7 @@ val print_list : Format.formatter -> t list -> unit
 val print_full : Format.formatter -> t -> unit
 (** Print function including the record fields. *)
 
-val vty_of : t -> Svty.t
+val vty_of : t -> TvSet.t
 (** Returns the set of type variables that occur in a given type. *)
 
 
@@ -151,10 +144,6 @@ val vty_of : t -> Svty.t
 val tunit : t
 (** The unit type. *)
 
-val fresh_var : unit -> tvar
-(** Generate a fresh type variable, guaranteed to be distinct
-    from any other previously generated by this function. *)
-
 val fresh_tvar : unit -> t
 (** Wrap the {!val:fresh_var} function to return a type. *)
 
@@ -191,10 +180,7 @@ val trecord :
 
 (** {2 Substitutions} *)
 
-module M : Map.S with type key = int
-(** Maps from type variables identifiers. *)
-
-type subst = t M.t
+type subst = t TvMap.t
 (** The type of substitution, i.e. maps
     from type variables identifiers to types.*)
 

From 2f89b247c3eb7d7288e3ee602e9f297bc599c742 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 12 Nov 2024 13:49:01 +0100
Subject: [PATCH 3/3] change review

---
 src/lib/structures/expr.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 778659801..3c5313c7d 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -333,10 +333,6 @@ module SmtPrinter = struct
     | `Forall -> Fmt.pf ppf "forall"
     | `Exists -> Fmt.pf ppf "exists"
 
-  (* This printer follows the convention used to print
-     type variables in the module [Ty]. *)
-  let pp_tvar ppf v = Fmt.pf ppf "A%a" DE.Ty.Var.print v
-
   let rec pp_main bind ppf { user_trs; main; binders; _ } =
     if not @@ Var.Map.is_empty binders then
       Fmt.pf ppf "@[<2>(%a (%a)@, %a@, %a)@]"
@@ -350,7 +346,7 @@ module SmtPrinter = struct
   and pp_quantified bind ppf q =
     if q.toplevel && not @@ Ty.TvSet.is_empty q.main.vty then
       Fmt.pf ppf "@[<2>(par (%a)@, %a)@]"
-        Fmt.(box @@ iter ~sep:sp Ty.TvSet.iter pp_tvar) q.main.vty
+        Fmt.(box @@ iter ~sep:sp Ty.TvSet.iter DE.Ty.Var.print) q.main.vty
         (pp_main bind) q
     else
       pp_main bind ppf q