Use a polymorphic variant for the enum flag

src/lib/frontend/d_cnf.ml

@@ -632,7 +632,8 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
       ) ([], true) cases
     in
     let body = Some (List.rev rev_cs) in
-    let ty = Ty.t_adt ~enum:is_enum ~body uid tyvl in
+    let kind = if is_enum then `Enum else `Adt in
+    let ty = Ty.t_adt ~kind ~body uid tyvl in
     Cache.store_ty ty_c ty
 
   | None | Some Abstract ->
@@ -748,7 +749,9 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             if (record || Array.length cases = 1) && not contains_adts
             then
               Ty.trecord ~record_constr:uid tyvl uid []
-            else Ty.t_adt ~enum:is_enum uid tyvl
+            else
+              let kind = if is_enum then `Enum else `Adt in
+              Ty.t_adt ~kind uid tyvl
           in
           Cache.store_ty ty_c ty;
           (ty, Some adt) :: acc

src/lib/frontend/typechecker.ml

@@ -69,11 +69,11 @@ module Types = struct
     match ty with
     | Ty.Text (lty', s)
     | Ty.Trecord { Ty.args = lty'; name = s; _ }
-    | Ty.Tadt (s,lty',false) ->
+    | Ty.Tadt (s,lty',`Adt) ->
       if List.length lty <> List.length lty' then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       lty'
-    | Ty.Tadt (s,lty',true) ->
+    | Ty.Tadt (s,lty',`Enum) ->
       if List.length lty <> 0 || List.length lty' <> 0 then
         Errors.typing_error (WrongNumberofArgs (Uid.show s)) loc;
       []
@@ -149,7 +149,7 @@ module Types = struct
       if not (Lists.is_empty ty_vars) then
         Errors.typing_error (PolymorphicEnum id) loc;
       let body = List.map (fun constr -> Uid.of_string constr, []) l in
-      let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_string id) [] in
+      let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_string id) [] in
       ty, { env with to_ty = MString.add id ty env.to_ty }
     | Record (record_constr, lbs) ->
       let lbs =
@@ -275,7 +275,7 @@ module Env = struct
   let add_fpa_enum map =
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
-    | Ty.Tadt (name, [], true) ->
+    | Ty.Tadt (name, [], `Enum) ->
       let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
@@ -301,7 +301,7 @@ module Env = struct
 
   let find_builtin_cstr ty n =
     match ty with
-    | Ty.Tadt (name, [], true) ->
+    | Ty.Tadt (name, [], `Enum) ->
       let Adt cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.find (Uid.equal n) cstrs

src/lib/reasoners/adt_rel.ml

@@ -156,7 +156,7 @@ module Domains = struct
 
   let is_enum r =
     match X.type_info r with
-    | Ty.Tadt (_, [], true) -> true
+    | Ty.Tadt (_, [], `Enum) -> true
     | _ -> false
 
   let internal_update r nd t =

src/lib/structures/fpa_rounding.ml

@@ -96,7 +96,7 @@ let fpa_rounding_mode_dty, d_cstrs, fpa_rounding_mode =
   let body =
     List.map (fun (c, _) -> Uid.of_dolmen c, []) d_cstrs
   in
-  let ty = Ty.t_adt ~enum:true ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
+  let ty = Ty.t_adt ~kind:`Enum ~body:(Some body) (Uid.of_dolmen ty_cst) [] in
   DE.Ty.apply ty_cst [], d_cstrs, ty
 
 let rounding_mode_of_smt_hs =

src/lib/structures/ty.ml

@@ -34,7 +34,7 @@ type t =
   | Tbitv of int
   | Text of t list * Uid.t
   | Tfarray of t * t
-  | Tadt of Uid.t * t list * bool
+  | Tadt of Uid.t * t list * [`Adt | `Enum]
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
@@ -529,8 +529,8 @@ let fresh_empty_text =
     in
     text [] (Uid.of_dolmen id)
 
-let t_adt ?(enum=false) ?(body=None) s ty_vars =
-  let ty = Tadt (s, ty_vars, enum) in
+let t_adt ?(kind=`Adt) ?(body=None) s ty_vars =
+  let ty = Tadt (s, ty_vars, kind) in
   begin match body with
     | None -> ()
     | Some [] -> assert false

src/lib/structures/ty.mli

@@ -53,13 +53,13 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Uid.t * t list * bool
-  (** Application of algebraic data types. [Tadt (a, params, enum)] denotes
+  | Tadt of Uid.t * t list * [`Adt | `Enum]
+  (** Application of algebraic data types. [Tadt (a, params, kind)] denotes
       the application of the polymorphic datatype [a] to the types parameters
-      [params]. The flag [enum] determines if the ADT is an enum.
+      [params]. The flag [kind] 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], false)] where the identifier
+      value [Tadt (Hstring.make "list", [Tint], `Adt)] where the identifier
       {e list} denotes a polymorphic ADT defined by the user with [t_adt]. *)
 
   | Trecord of trecord
@@ -169,7 +169,7 @@ val text : t list -> Uid.t -> t
     given. *)
 
 val t_adt :
-  ?enum:bool ->
+  ?kind:[`Adt | `Enum] ->
   ?body: ((Uid.t * (Uid.t * t) list) list) option -> Uid.t -> t list -> t
 (** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of
@@ -178,8 +178,8 @@ val t_adt :
     argument is the name of the type. The third one provides its list
     of arguments.
 
-    The flag [enum] is used to annotate ADT whose all the constructors have no
-    payload. *)
+    The flag [kind] is used to annotate ADT that are enum types. [`Adt]
+    kind is the default. *)
 
 val trecord :
   ?sort_fields:bool ->