Use Dolmen identifiers directly in Uid

Author: Halbaroth

src/lib/frontend/typechecker.ml

@@ -210,7 +210,7 @@ module Types = struct
         Errors.typing_error WrongNumberOfLabels loc;
       List.iter
         (fun (lb, _) ->
-           try ignore (Uid.list_assoc lb l)
+           try ignore (Lists.assoc Uid.equal lb l)
            with Not_found ->
              Errors.typing_error
                (WrongLabel((Hstring.make @@ Uid.show lb), ty)) loc) lbs;
@@ -869,7 +869,8 @@ let rec type_term ?(call_from_type_form=false) env f =
         | Ty.Trecord { Ty.name = g; lbs; _ } ->
           begin
             try
-              TTdot(te, Hstring.make a), Uid.list_assoc (Uid.of_string a) lbs
+              TTdot(te, Hstring.make a),
+              Lists.assoc Uid.equal (Uid.of_string a) lbs
             with Not_found ->
               let g = Uid.show g in
               Errors.typing_error (ShouldHaveLabel(g,a)) t.pp_loc

src/lib/reasoners/adt_rel.ml

@@ -208,7 +208,7 @@ let calc_destructor d e uf =
   let r, ex = Uf.find uf e in
   match Th.embed r with
   | Constr { c_args; _ } ->
-    begin match Lists.assoc Hstring.equal d c_args with
+    begin match Lists.assoc Uid.equal d c_args with
       | v -> Some (v, ex)
       | exception Not_found -> None
     end

src/lib/reasoners/records.ml

@@ -123,7 +123,7 @@ module Shostak (X : ALIEN) = struct
     | Access (a, x, ty) ->
       begin
         match normalize x with
-        | Record (lbs, _) -> Uid.list_assoc a lbs
+        | Record (lbs, _) -> Lists.assoc Uid.equal a lbs
         | x_n -> Access (a, x_n, ty)
       end
     | Other _ -> v
@@ -326,7 +326,7 @@ module Shostak (X : ALIEN) = struct
      | Record (lbs, ty) ->
       Record (List.map (fun (n,e') -> n, subst_access x s e') lbs, ty)
      | Access (lb, e', _) when compare_mine x e' = 0 ->
-      Uid.list_assoc lb s
+      Lists.assoc Uid.equal lb s
      | Access (lb', e', ty) -> Access (lb', subst_access x s e', ty)
      | Other _ -> e
   *)

src/lib/structures/fpa_rounding.ml

@@ -88,8 +88,23 @@ let hstring_ae_reprs =
 (* The rounding mode is the enum with the SMT values.
    The Alt-Ergo values are injected in this type. *)
 let fpa_rounding_mode =
-  let fake_reprs = List.map Uid.of_hstring hstring_smt_reprs in
-  Ty.Tsum (Uid.of_string "RoundingMode", fake_reprs)
+  let module DStd = Dolmen.Std in
+  let cstrs =
+    List.map
+      (fun cstr ->
+         DStd.Expr.Id.mk ~builtin:DStd.Builtin.Base
+           (DStd.Path.global @@ Hstring.view cstr)
+           DStd.Expr.{ arity = 0; alias = No_alias }
+         |> Uid.of_dolmen
+      )
+      hstring_smt_reprs
+  in
+  let name =
+    DStd.Expr.Ty.Const.mk
+      (DStd.Path.global "RoundingMode") 0
+    |> Uid.of_dolmen
+  in
+  Ty.Tsum (name, cstrs)
 
 let rounding_mode_of_smt_hs =
   let table = Hashtbl.create 5 in

src/lib/structures/uid.ml

@@ -32,8 +32,8 @@ module DStd = Dolmen.Std
 module DE = DStd.Expr
 
 type t =
-  | Hstring of Hstring.t
-  | Unique of { name : Hstring.t; index : int }
+  | Hstring : Hstring.t -> t
+  | Dolmen : 'a DE.id -> t
 
 (** Helper function: returns the basename of a dolmen path, since in AE
     the problems are contained in one-file (for now at least), the path is
@@ -52,38 +52,32 @@ let get_basename = function
           | _ -> ()
         ) path
 
-let[@inline always] of_dolmen DE.{ path; index; _ } =
-  let name = Hstring.make @@ get_basename path in
-  Unique { name; index = (index :> int) }
-
+let[@inline always] of_dolmen id = Dolmen id
 let[@inline always] of_hstring hs = Hstring hs
 let[@inline always] of_string s = of_hstring @@ Hstring.make s
 
 let hash = function
   | Hstring hs -> Hstring.hash hs
-  | Unique { index; _ } -> index
+  | Dolmen { index; _ } -> (index :> int)
 
 let pp ppf = function
   | Hstring hs -> Hstring.print ppf hs
-  | Unique { name; _ } -> Hstring.print ppf name
+  | Dolmen { path; _ } -> Fmt.string ppf @@ get_basename path
 
 let show = Fmt.to_to_string pp
 
 let equal u1 u2 =
   match u1, u2 with
   | Hstring hs1, Hstring hs2 -> Hstring.equal hs1 hs2
-  | Unique { index = i1; _ }, Unique { index = i2; _ }-> i1 = i2
-  | _ -> false
+  | Dolmen id1, Dolmen id2 -> DE.Id.equal id1 id2
+  | _ ->
+    Hstring.equal (Hstring.make @@ show u1) (Hstring.make @@ show u2)
 
 let compare u1 u2 =
   match u1, u2 with
   | Hstring hs1, Hstring hs2 -> Hstring.compare hs1 hs2
-  | Unique { index = i1; _ }, Unique { index = i2; _ } -> i1 - i2
-  | _ -> -1
-
-let rec list_assoc x = function
-  | [] -> raise Not_found
-  | (y, v) :: l -> if equal x y then v else list_assoc x l
+  | Dolmen id1, Dolmen id2 -> DE.Id.compare id1 id2
+  | _ -> Hstring.compare (Hstring.make @@ show u1) (Hstring.make @@ show u2)
 
 module Set = Set.Make
     (struct

src/lib/structures/uid.mli

@@ -30,9 +30,7 @@
 
 module DE = Dolmen.Std.Expr
 
-type t = private
-  | Hstring of Hstring.t
-  | Unique of { name : Hstring.t; index : int }
+type t
 
 val of_dolmen : 'a DE.Id.t -> t
 val of_string : string -> t
@@ -42,7 +40,6 @@ val pp : t Fmt.t
 val show : t -> string
 val equal : t -> t -> bool
 val compare : t -> t -> int
-val list_assoc : t -> (t * 'a) list -> 'a
 
 module Set : Set.S with type elt = t
 module Map : Map.S with type key = t