From 36d143d6a8a514ac7af4bd95b4e174dea46430ef Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 11 Jun 2024 13:52:46 +0200 Subject: [PATCH] Use a polymorphic variant for the enum flag --- src/lib/frontend/d_cnf.ml | 7 +++++-- src/lib/frontend/typechecker.ml | 10 +++++----- src/lib/reasoners/adt_rel.ml | 2 +- src/lib/structures/fpa_rounding.ml | 2 +- src/lib/structures/ty.ml | 6 +++--- src/lib/structures/ty.mli | 14 +++++++------- 6 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index fd8d2bc6a..bb03097ca 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/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 diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 0f8500d46..7227f9098 100644 --- a/src/lib/frontend/typechecker.ml +++ b/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 diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index d2f02ebcd..ca13e5c76 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/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 = diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index bb59c2c9e..73fb653e1 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/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 = diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 3afbd598b..ed9c2fe70 100644 --- a/src/lib/structures/ty.ml +++ b/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 diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index d71753441..c532b433b 100644 --- a/src/lib/structures/ty.mli +++ b/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 ->