From 25f68b219a7935e0e1a6da598630f50b3978a306 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 12:14:41 +0200 Subject: [PATCH] Better `is_enum_constr` test in Adt_rel As we do not use Hstring to identify ADT constructor, we can use the Dolmen type of a constructor to determine its arity. --- src/lib/reasoners/adt_rel.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index f156fd4da..b9a35df2e 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -169,23 +169,23 @@ module Domains = struct let filter_ty = is_adt_ty - (* TODO: This test is slow because we have to retrieve the list of - destructors of the constructor [c] by searching in the list [cases]. - - A better predicate will be easy to implement after getting rid of - the legacy frontend and switching from [Uid.t] to - [Dolmen.Std.Expr.term_cst] to store the constructors. Indeed, [term_cst] - contains the type of constructor and in particular its arity. *) - let is_enum_constr r c = - match X.type_info r with - | Tadt (name, args) -> - let cases = Ty.type_body name args in - Compat.List.is_empty @@ Ty.assoc_destrs c cases - | _ -> assert false + let is_enum_constr DE.{ id_ty; _ } = + let monomorphic_case id_ty = + match DE.Ty.view id_ty with + | `Arrow (l, _) -> Compat.List.is_empty l + | `App _ -> true + | _ -> + (* This case cannot occur as [id_ty] denotes the type of a monomorphic + ADT constructor. *) + assert false + in + match DE.Ty.view id_ty with + | `Pi (_, ty) -> monomorphic_case ty + | _ -> monomorphic_case id_ty let internal_update r nd t = let domains = MX.add r nd t.domains in - let is_enum_domain = Domain.for_all (is_enum_constr r) nd in + let is_enum_domain = Domain.for_all is_enum_constr nd in let enums = if is_enum_domain then SX.add r t.enums else t.enums in let changed = SX.add r t.changed in { domains; enums; changed }