feat(core): add box, with a box constant

this is a good alternative to gensym for preprocessing, as it is
idempotent and functional.

src/core/Sidekick_core.ml

@@ -43,5 +43,6 @@ module Proof_trace = Proof_trace
 module Proof_term = Proof_term
 module Subst = Sidekick_core_logic.Subst
 module Var = Sidekick_core_logic.Var
+module Box = Box
 
 exception Resource_exhausted

src/core/box.ml

@@ -0,0 +1,33 @@
+open Sidekick_core_logic
+
+type Const.view += Box of Term.t
+
+let ops : Const.ops =
+  (module struct
+    let pp out = function
+      | Box t -> Fmt.fprintf out "(@[box@ %a@])" Term.pp_debug t
+      | _ -> assert false
+
+    let equal a b =
+      match a, b with
+      | Box a, Box b -> Term.equal a b
+      | _ -> false
+
+    let hash = function
+      | Box t -> Hash.(combine2 10 (Term.hash t))
+      | _ -> assert false
+
+    let opaque_to_cc _ = false
+  end)
+
+let as_box t =
+  match Term.view t with
+  | Term.E_const { Const.c_view = Box u; _ } -> Some u
+  | _ -> None
+
+let box tst t : Term.t =
+  match Term.view t with
+  | Term.E_const { Const.c_view = Box _; _ } -> t
+  | _ ->
+    let c = Const.make (Box t) ~ty:(Term.ty t) ops in
+    Term.const tst c

src/core/box.mli

@@ -0,0 +1,9 @@
+open Sidekick_core_logic
+
+type Const.view += private Box of Term.t
+
+val box : Term.store -> Term.t -> Term.t
+(** [box tst t] makes a new constant that "boxes" [t].
+  This way it will be opaque. *)
+
+val as_box : Term.t -> Term.t option

src/core/t_printer.ml

@@ -23,7 +23,15 @@ let pp_builtins_ : hook =
     true
   | _ -> false
 
-let default_ : Hooks.t = Hooks.(empty |> add pp_builtins_)
+let pp_box : hook =
+ fun ~recurse out t ->
+  match Box.as_box t with
+  | Some b ->
+    Fmt.fprintf out "[[ @[%a@] ]]" recurse b;
+    true
+  | None -> false
+
+let default_ : Hooks.t = Hooks.(empty |> add pp_builtins_ |> add pp_box)
 let default_hooks = ref default_
 
 (* debug printer *)