From 2309a0fd6775e3d1381d54d1fe1fd1550454e503 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Sun, 17 Jul 2022 14:04:11 +0200
Subject: [PATCH] [ADT] choice on filed of type bool was not done.
It is complicated to know who is responsible for this choice
---
src_colibri2/theories/ADT/adt.ml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index cef2681da..a2a97564c 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -122,8 +122,12 @@ let converter d (f : Ground.t) =
app = { builtin = Expr.Destructor { case; field; adt; _ }; _ };
args;
tyargs;
+ ty;
_;
} ->
+ (* not completely satisfactory but needed, it is not yet clear who has the responsibility of choice for booleans *)
+ if Ground.Ty.(equal ty bool) then
+ Choice.register_thterm d (Ground.thterm f) (Boolean.chobool r);
let case = case_of_int case in
let field = field_of_int field in
let adt = Option.value_exn (Adt_value.MonoAdt.index adt tyargs) in
--
GitLab