feat(core): make CC_view part of the core library; with default CC view

src/core/CC_view.ml

@@ -0,0 +1,38 @@
+type ('f, 't, 'ts) t =
+  | Bool of bool
+  | App_fun of 'f * 'ts
+  | App_ho of 't * 't
+  | If of 't * 't * 't
+  | Eq of 't * 't
+  | Not of 't
+  | Opaque of 't
+(* do not enter *)
+
+let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
+  match v with
+  | Bool b -> Bool b
+  | App_fun (f, args) -> App_fun (f_f f, f_ts args)
+  | App_ho (f, a) -> App_ho (f_t f, f_t a)
+  | Not t -> Not (f_t t)
+  | If (a, b, c) -> If (f_t a, f_t b, f_t c)
+  | Eq (a, b) -> Eq (f_t a, f_t b)
+  | Opaque t -> Opaque (f_t t)
+
+let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
+  match v with
+  | Bool _ -> ()
+  | App_fun (f, args) ->
+    f_f f;
+    f_ts args
+  | App_ho (f, a) ->
+    f_t f;
+    f_t a
+  | Not t -> f_t t
+  | If (a, b, c) ->
+    f_t a;
+    f_t b;
+    f_t c
+  | Eq (a, b) ->
+    f_t a;
+    f_t b
+  | Opaque t -> f_t t

src/core/CC_view.mli

@@ -0,0 +1,33 @@
+(** View terms through the lens of a Congruence Closure *)
+
+(** A view of a term fron the point of view of a congruence closure.
+
+  - ['f] is the type of function symbols
+  - ['t] is the type of terms
+  - ['ts] is the type of sequences of terms (arguments of function application)
+  *)
+type ('f, 't, 'ts) t =
+  | Bool of bool
+  | App_fun of 'f * 'ts
+  | App_ho of 't * 't
+  | If of 't * 't * 't
+  | Eq of 't * 't
+  | Not of 't
+  | Opaque of 't  (** do not enter *)
+
+val map_view :
+  f_f:('a -> 'b) ->
+  f_t:('c -> 'd) ->
+  f_ts:('e -> 'f) ->
+  ('a, 'c, 'e) t ->
+  ('b, 'd, 'f) t
+(** Map function over a view, one level deep.
+    Each function maps over a different type, e.g. [f_t] maps over terms *)
+
+val iter_view :
+  f_f:('a -> unit) ->
+  f_t:('b -> unit) ->
+  f_ts:('c -> unit) ->
+  ('a, 'b, 'c) t ->
+  unit
+(** Iterate over a view, one level deep. *)

src/core/Sidekick_core.ml

@@ -14,7 +14,7 @@
 
 module Fmt = CCFormat
 
-(* re-export *)
+(** {2 Re-exports from core-logic} *)
 
 module Const = Sidekick_core_logic.Const
 
@@ -23,7 +23,14 @@ module Term = struct
   include Sidekick_core_logic.T_builtins
 end
 
+(** {2 view} *)
+
 module Bool_view = Bool_view
+module CC_view = CC_view
+module Default_cc_view = Default_cc_view
+
+(** {2 Main modules} *)
+
 module Bvar = Sidekick_core_logic.Bvar
 module Lit = Lit
 module Proof_step = Proof_step

src/core/default_cc_view.ml

@@ -0,0 +1,16 @@
+open Sidekick_core_logic
+module View = CC_view
+
+let view_as_cc (t : Term.t) : _ CC_view.t =
+  let f, args = Term.unfold_app t in
+  match Term.view f, args with
+  | _, [ _; t; u ] when T_builtins.is_eq f -> View.Eq (t, u)
+  | Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] ->
+    View.If (a, b, c)
+  | Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a
+  | _ ->
+    (match Term.view t with
+    | Term.E_app (f, a) -> View.App_ho (f, a)
+    | Term.E_const { Const.c_view = T_builtins.C_true; _ } -> View.Bool true
+    | Term.E_const { Const.c_view = T_builtins.C_false; _ } -> View.Bool false
+    | _ -> View.Opaque t)

src/core/default_cc_view.mli

@@ -0,0 +1,3 @@
+open Sidekick_core_logic
+
+val view_as_cc : Term.t -> (Const.t, Term.t, Term.t list) CC_view.t