feat(term): add open_eq

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

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. *)

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

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