From 226fda18dad3a90ed112009e195a2a4baa933fe5 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Tue, 11 Jun 2024 11:24:14 +0200
Subject: [PATCH] poetry

---
 src/lib/frontend/typechecker.ml | 6 +++---
 src/lib/reasoners/adt_rel.ml    | 6 +++++-
 src/lib/structures/ty.mli       | 9 ++++++---
 3 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index 3bb0f2c5c..aeecef050 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -302,7 +302,7 @@ module Env = struct
     | Ty.Tadt (name, [], true) ->
       let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
-      List.find (fun c -> String.equal n @@ Uid.show c) cstrs
+      List.find (Uid.equal n) cstrs
     | _ ->
       assert false
 
@@ -329,9 +329,9 @@ module Env = struct
     let nte = Fpa_rounding.string_of_rounding_mode NearestTiesToEven in
     let tname = Fpa_rounding.fpa_rounding_mode_ae_type_name in
     let float32 = float (int "24") (int "149") in
-    let float32d = float32 (mode nte) in
+    let float32d = float32 (mode (Uid.of_string nte)) in
     let float64 = float (int "53") (int "1074") in
-    let float64d = float64 (mode nte) in
+    let float64d = float64 (mode (Uid.of_string nte)) in
     let op n op profile =
       MString.add n @@ `Term (Symbols.Op op, profile, Other)
     in
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index a15f656ec..d2f02ebcd 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -660,6 +660,10 @@ let split_enum env uf =
   if can_split env n then
     let _, cons = Option.get @@ build_constr_eq r c in
     let nr, ctx = X.make cons in
+    (* In the current implementation of `X.make`, we produce
+       a nonempty context only for interpreted semantic values
+       of the `Arith` and `Records` theories. The semantic
+       values `cons` never involves such values. *)
     assert (Lists.is_empty ctx);
     Some (LR.mkv_eq r nr)
   else
@@ -672,11 +676,11 @@ let split_best_domain ~for_model uf =
     let ds = Uf.(GlobalDomains.find (module Domains) @@ domains uf) in
     let* r, c = pick_best ds in
     let _, cons = Option.get @@ build_constr_eq r c in
+    let nr, ctx = X.make cons in
     (* In the current implementation of `X.make`, we produce
        a nonempty context only for interpreted semantic values
        of the `Arith` and `Records` theories. The semantic
        values `cons` never involves such values. *)
-    let nr, ctx = X.make cons in
     assert (Lists.is_empty ctx);
     Some (LR.mkv_eq r nr)
 
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 01770e072..d71753441 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -59,8 +59,8 @@ type t =
       [params]. The flag [enum] determines if the ADT is an enum.
 
       For instance the type of integer lists can be represented by the
-      value [Tadt (Hstring.make "list", [Tint])] where the identifier "list"
-      denotes a polymorphic ADT defined by the user with [t_adt]. *)
+      value [Tadt (Hstring.make "list", [Tint], false)] where the identifier
+      {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *)
 
   | Trecord of trecord
   (** Record type. *)
@@ -176,7 +176,10 @@ val t_adt :
     its destructors with their respective types. If [body] is none,
     then no definition will be registered for this type. The second
     argument is the name of the type. The third one provides its list
-    of arguments. *)
+    of arguments.
+
+    The flag [enum] is used to annotate ADT whose all the constructors have no
+    payload. *)
 
 val trecord :
   ?sort_fields:bool ->