From c2af58928202d60afce7fd27536a4df32c88baed Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 7 Aug 2022 22:40:39 -0400
Subject: [PATCH] add core.bool_view

---
 src/core/Sidekick_core.ml                     |  1 +
 src/core/bool_view.ml                         | 15 +++++++++++++++
 src/th-bool-static/Sidekick_th_bool_static.ml |  4 +---
 src/th-bool-static/intf.ml                    |  3 +--
 4 files changed, 18 insertions(+), 5 deletions(-)
 create mode 100644 src/core/bool_view.ml

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 204c1174..ca4699d7 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -23,6 +23,7 @@ module Term = struct
   include Sidekick_core_logic.T_builtins
 end
 
+module Bool_view = Bool_view
 module Bvar = Sidekick_core_logic.Bvar
 module Lit = Lit
 module Proof_step = Proof_step
diff --git a/src/core/bool_view.ml b/src/core/bool_view.ml
new file mode 100644
index 00000000..6842efc7
--- /dev/null
+++ b/src/core/bool_view.ml
@@ -0,0 +1,15 @@
+(** Boolean-oriented view of terms *)
+
+(** View *)
+type ('a, 'args) t =
+  | B_bool of bool
+  | B_not of 'a
+  | B_and of 'args
+  | B_or of 'args
+  | B_imply of 'args * 'a
+  | B_equiv of 'a * 'a
+  | B_xor of 'a * 'a
+  | B_eq of 'a * 'a
+  | B_neq of 'a * 'a
+  | B_ite of 'a * 'a * 'a
+  | B_atom of 'a
diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml
index 130735c1..dde8ae39 100644
--- a/src/th-bool-static/Sidekick_th_bool_static.ml
+++ b/src/th-bool-static/Sidekick_th_bool_static.ml
@@ -53,7 +53,7 @@ end = struct
     | B_not u when is_true u -> ret_bequiv t (T.false_ tst)
     | B_not u when is_false u -> ret_bequiv t (T.true_ tst)
     | B_not _ -> None
-    | B_opaque_bool _ -> None
+    | B_atom _ -> None
     | B_and a ->
       if Iter.exists is_false a then
         ret (T.false_ tst)
@@ -102,7 +102,6 @@ end = struct
     | B_eq (a, b) when T.equal a b -> ret_bequiv t (T.true_ tst)
     | B_neq (a, b) when T.equal a b -> ret_bequiv t (T.true_ tst)
     | B_eq _ | B_neq _ -> None
-    | B_atom _ -> None
 
   let fresh_term self ~for_t ~pre ty =
     let u = A.Gensym.fresh_term self.gensym ~pre ty in
@@ -164,7 +163,6 @@ end = struct
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
     (match A.view_as_bool t with
-    | B_opaque_bool _ -> ()
     | B_bool _ -> ()
     | B_not _ -> ()
     | B_and l ->
diff --git a/src/th-bool-static/intf.ml b/src/th-bool-static/intf.ml
index e25335a2..a348d9df 100644
--- a/src/th-bool-static/intf.ml
+++ b/src/th-bool-static/intf.ml
@@ -6,7 +6,7 @@ type term = Term.t
 type ty = Term.t
 
 (** Boolean-oriented view of terms *)
-type ('a, 'args) bool_view =
+type ('a, 'args) bool_view = ('a, 'args) Bool_view.t =
   | B_bool of bool
   | B_not of 'a
   | B_and of 'args
@@ -17,7 +17,6 @@ type ('a, 'args) bool_view =
   | B_eq of 'a * 'a
   | B_neq of 'a * 'a
   | B_ite of 'a * 'a * 'a
-  | B_opaque_bool of 'a (* do not enter *)
   | B_atom of 'a
 
 module type PROOF_RULES = sig