From 72990de3732479128cff5ceedf5e4a38edfb7c60 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 19 Sep 2022 22:26:31 -0400
Subject: [PATCH] wip: feat(core): tracing terms, make constants
 (de)serializable

---
 src/core-logic/const.ml  |  4 ++++
 src/core-logic/const.mli |  4 ++++
 src/core-logic/types_.ml |  8 ++++++++
 src/core/t_tracer.ml     | 35 +++++++++++++++++++++++++++++++++--
 src/core/t_tracer.mli    | 15 +++++++++++++--
 5 files changed, 62 insertions(+), 4 deletions(-)

diff --git a/src/core-logic/const.ml b/src/core-logic/const.ml
index c7004f70..f875debf 100644
--- a/src/core-logic/const.ml
+++ b/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)
diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli
index 8fe1838d..52e8d27c 100644
--- a/src/core-logic/const.mli
+++ b/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)
diff --git a/src/core-logic/types_.ml b/src/core-logic/types_.ml
index 70b445c2..bd3db493 100644
--- a/src/core-logic/types_.ml
+++ b/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)
diff --git a/src/core/t_tracer.ml b/src/core/t_tracer.ml
index 00fffdc1..09677b62 100644
--- a/src/core/t_tracer.ml
+++ b/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
diff --git a/src/core/t_tracer.mli b/src/core/t_tracer.mli
index c6c150af..d182acc7 100644
--- a/src/core/t_tracer.mli
+++ b/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