wip: feat(core): tracing terms, make constants (de)serializable

src/core-logic/const.ml

@@ -6,6 +6,10 @@ module type DYN_OPS = sig
   val pp : view Fmt.printer
   val equal : view -> view -> bool
   val hash : view -> int
+  (* TODO
+     val ser : view -> Ser_value.t
+     val deser : view Ser_decode.t
+  *)
 end
 
 type ops = (module DYN_OPS)

src/core-logic/const.mli

@@ -10,6 +10,10 @@ module type DYN_OPS = sig
   val pp : view Fmt.printer
   val equal : view -> view -> bool
   val hash : view -> int
+  (* TODO
+     val ser : view -> Ser_value.t
+     val deser : view Ser_decode.t
+  *)
 end
 
 type ops = (module DYN_OPS)

src/core-logic/types_.ml

@@ -11,6 +11,14 @@ module type DYN_CONST_OPS = sig
 
   val hash : const_view -> int
   (** Hash constant *)
+
+  (* TODO
+     val ser : const_view -> Ser_value.t
+     (** Serialize constant *)
+
+     val deser : const_view Ser_decode.t
+     (** Deserialize constant *)
+  *)
 end
 
 type const_ops = (module DYN_CONST_OPS)

src/core/t_tracer.ml

@@ -2,8 +2,39 @@ open Sidekick_core_logic
 module Tr = Sidekick_trace
 module T = Term
 
-type Tr.entry_view += private Def_term of { id: int }
+type term_ref = Tr.entry_id
+type const_ref = Tr.entry_id
+
+type Tr.entry_view +=
+  | T_ty of int
+  | T_app of term_ref * term_ref
+  | T_var of string * term_ref
+  | T_bvar of int * term_ref
+  | T_const of { c: Const.view; c_ops: Const.ops; ty: term_ref }
+  | T_lam of { v_name: string; v_ty: term_ref; body: term_ref }
+  | T_pi of { v_name: string; v_ty: term_ref; body: term_ref }
+
+(* tracer *)
 type t = { sink: Tr.Sink.t; emitted: Tr.Entry_id.t T.Weak_map.t }
 
 let create ~sink () : t = { sink; emitted = T.Weak_map.create 16 }
-let emit (self : t) (t : T.t) : Tr.Entry_id.t = assert false
+
+let emit (self : t) (t : T.t) : Tr.Entry_id.t =
+  let module V = Ser_value in
+  let rec loop t =
+    match T.Weak_map.find_opt self.emitted t with
+    | Some id -> id
+    | None ->
+      let tag, v =
+        match T.view t with
+        | T.E_var v ->
+          let ty = loop (Var.ty v) in
+          "TV", V.(list [ string (Var.name v); int (ty :> int) ])
+        | _ -> assert false
+      in
+
+      let id = Tr.Sink.emit self.sink ~tag v in
+      T.Weak_map.add self.emitted t id;
+      id
+  in
+  loop t

src/core/t_tracer.mli

@@ -8,8 +8,19 @@
 open Sidekick_core_logic
 module Tr = Sidekick_trace
 
-type Tr.entry_view += private Def_term of { id: int }
+type term_ref = private Tr.entry_id
+
+type Tr.entry_view +=
+  private
+  | T_ty of int
+  | T_app of term_ref * term_ref
+  | T_var of string * term_ref
+  | T_bvar of int * term_ref
+  | T_const of { c: Const.view; c_ops: Const.ops; ty: term_ref }
+  | T_lam of { v_name: string; v_ty: term_ref; body: term_ref }
+  | T_pi of { v_name: string; v_ty: term_ref; body: term_ref }
+
 type t
 
 val create : sink:Tr.Sink.t -> unit -> t
-val emit : t -> Term.t -> Tr.Entry_id.t
+val emit : t -> Term.t -> term_ref