From 0ff197d56c872e96c7b1797dfea37dc31a5ff4e2 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 22 Aug 2022 22:01:02 -0400
Subject: [PATCH] perf(core): have `eq` and `not_` be simplying

- `a=b` and `b=a` are now the same
- `not (not u)` and `u` are now the same
---
 src/core-logic/t_builtins.ml | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml
index 7dcb1b66..d8b61f0c 100644
--- a/src/core-logic/t_builtins.ml
+++ b/src/core-logic/t_builtins.ml
@@ -68,9 +68,28 @@ let c_not store =
   let ty = arrow store b b in
   const store @@ Const.make C_not ops ~ty
 
-let eq store a b = app_l store (c_eq store) [ ty a; a; b ]
+let eq store a b =
+  if equal a b then
+    true_ store
+  else (
+    let a, b =
+      if compare a b <= 0 then
+        a, b
+      else
+        b, a
+    in
+    app_l store (c_eq store) [ ty a; a; b ]
+  )
+
 let ite store a b c = app_l store (c_ite store) [ ty b; a; b; c ]
-let not store a = app store (c_not store) a
+
+let not store a =
+  (* turn [not (not u)] into [u] *)
+  match view a with
+  | E_app ({ view = E_const { c_view = C_not; _ }; _ }, u) -> u
+  | E_const { c_view = C_true; _ } -> false_ store
+  | E_const { c_view = C_false; _ } -> true_ store
+  | _ -> app store (c_not store) a
 
 let is_bool t =
   match view t with