From 8811699410b52ad8462e29caa779d8c563adc960 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 10 Sep 2022 14:09:55 -0400
Subject: [PATCH] feat(term): add `open_eq`

---
 src/core-logic/t_builtins.ml  | 6 ++++++
 src/core-logic/t_builtins.mli | 3 +++
 src/core-logic/term.ml        | 2 +-
 src/core-logic/types_.ml      | 3 +++
 4 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml
index 86265e7a..29a65153 100644
--- a/src/core-logic/t_builtins.ml
+++ b/src/core-logic/t_builtins.ml
@@ -116,3 +116,9 @@ let as_bool_val t =
   | Term.E_const { c_view = C_true; _ } -> Some true
   | Term.E_const { c_view = C_false; _ } -> Some false
   | _ -> None
+
+let[@inline] open_eq t =
+  let f, args = unfold_app t in
+  match view f, args with
+  | E_const { c_view = C_eq; _ }, [ _ty; a; b ] -> Some (a, b)
+  | _ -> None
diff --git a/src/core-logic/t_builtins.mli b/src/core-logic/t_builtins.mli
index 521fcfe1..a864d7f8 100644
--- a/src/core-logic/t_builtins.mli
+++ b/src/core-logic/t_builtins.mli
@@ -33,3 +33,6 @@ val abs : store -> t -> bool * t
     should return [(true, t)]. *)
 
 val as_bool_val : t -> bool option
+
+val open_eq : t -> (t * t) option
+(** [open_eq (a=b)] returns [Some (a,b)], [None] for other terms. *)
diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml
index 5f8bd6e8..70292904 100644
--- a/src/core-logic/term.ml
+++ b/src/core-logic/term.ml
@@ -47,7 +47,7 @@ let[@inline] ty e : term =
   | T_ty_delayed f -> ty_force_delayed_ e f
 
 (* open an application *)
-let unfold_app (e : term) : term * term list =
+let[@inline] unfold_app (e : term) : term * term list =
   let[@unroll 1] rec aux acc e =
     match e.view with
     | E_app (f, a) -> aux (a :: acc) f
diff --git a/src/core-logic/types_.ml b/src/core-logic/types_.ml
index 6464fdce..79804928 100644
--- a/src/core-logic/types_.ml
+++ b/src/core-logic/types_.ml
@@ -5,10 +5,13 @@ type const_view = ..
 module type DYN_CONST_OPS = sig
   val pp : const_view Fmt.printer
   (** Pretty-print constant *)
+
   val equal : const_view -> const_view -> bool
   (** Equality of constant with any other constant *)
+
   val hash : const_view -> int
   (** Hash constant *)
+
   val opaque_to_cc : const_view -> bool
   (** If true, congruence closure will not apply for applications of this
       constant. In other words, [c t1…tn] will appear to the congruence