From f5a61bd847bd3f83757a5aec498f2bc83e30720a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20Ruet-Cros?= <cecile.ruet-cros@cea.fr>
Date: Fri, 5 Jul 2024 09:59:08 +0200
Subject: [PATCH] [wp] vset: cleanup & ready

---
 src/plugins/wp/Vset.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/plugins/wp/Vset.ml b/src/plugins/wp/Vset.ml
index dd2ce840c1e..a5b1b571e3d 100644
--- a/src/plugins/wp/Vset.ml
+++ b/src/plugins/wp/Vset.ml
@@ -98,16 +98,14 @@ let tau_of_set (te:tau) : tau = Logic.Data( adt_set , [te] )
 
 let typecheck_binop (params:tau option list) : tau =
   match params with
-  | [] | [ _ ] -> raise (Invalid_argument "WP.Vset.typecheck_binop: too few arguments")
-  | [ Some t ; _ ] -> t
-  | [ None ; Some t ] -> t
-  | _ -> raise (Invalid_argument "WP.Vset.typecheck_binop: too many arguments")
+  | [ Some t ; _ ] | [ _ ; Some t ]-> t
+  | _ -> raise (Invalid_argument "WP.Vset.typecheck_binop")
 
-let typecheck_unop (params:tau option list) : tau =
+
+let typecheck_singleton (params:tau option list) : tau =
   match params with
-  | [] -> raise (Invalid_argument "WP.Vset.typecheck_unop: too few arguments")
   | [ Some t ] -> tau_of_set t
-  | _ -> raise (Invalid_argument "WP.Vset.typecheck_unop: too many arguments")
+  | _ -> raise (Invalid_argument "WP.Vset.typecheck_unop")
 
 let typecheck_range (_:tau option list) : tau =
   tau_of_set Logic.Int
@@ -120,7 +118,7 @@ let f_range = Lang.extern_f ~library ~typecheck:typecheck_range "range"
 let f_range_sup = Lang.extern_f ~library ~typecheck:typecheck_range "range_sup"
 let f_range_inf = Lang.extern_f ~library ~typecheck:typecheck_range "range_inf"
 let f_range_all = Lang.extern_f ~library ~typecheck:typecheck_range "range_all"
-let f_singleton = Lang.extern_f ~library ~typecheck:typecheck_unop "singleton"
+let f_singleton = Lang.extern_f ~library ~typecheck:typecheck_singleton "singleton"
 
 let single a b = match a,b with
   | Some x , Some y when F.QED.equal x y -> a
-- 
GitLab