From b0e71d0b469719bf542023d8d176fde6d4f0f6b4 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 9 Oct 2024 15:58:18 +0200 Subject: [PATCH] review changes --- src/lib/reasoners/adt_rel.ml | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index b9a35df2e..87e10b0bc 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -169,19 +169,15 @@ module Domains = struct let filter_ty = is_adt_ty - 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 is_enum_constr DE.{ builtin; _ } = + match builtin with + | B.Constructor { adt ; case } -> + begin match DE.Ty.definition adt with + | Some Adt { cases; _ } -> + Array.length cases.(case).dstrs = 0 + | _ -> assert false + end + | _ -> false let internal_update r nd t = let domains = MX.add r nd t.domains in