From 798993fee2bb6abf766fbbb3e38cd8c47d05675c Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 25 Sep 2022 21:29:53 -0400
Subject: [PATCH] feat(trace): start basic trace reader for terms, using Source

---
 src/core/t_trace_read.ml  | 81 +++++++++++++++++++++++++++++++++++++++
 src/core/t_trace_read.mli |  8 ++++
 2 files changed, 89 insertions(+)
 create mode 100644 src/core/t_trace_read.ml
 create mode 100644 src/core/t_trace_read.mli

diff --git a/src/core/t_trace_read.ml b/src/core/t_trace_read.ml
new file mode 100644
index 00000000..f93bc2e2
--- /dev/null
+++ b/src/core/t_trace_read.ml
@@ -0,0 +1,81 @@
+open Sidekick_core_logic
+module Tr = Sidekick_trace
+module ID_cache = LRU.Make (Tr.Entry_id)
+module Dec = Ser_decode
+
+type term_ref = Tr.entry_id
+
+type t = {
+  tst: Term.store;
+  src: Tr.Source.t;
+  cache: (Term.t, string) result ID_cache.t;
+  const_decode: (Term.t Dec.t -> Const.t Dec.t) Util.Str_map.t;
+      (** tag -> const decoder *)
+}
+
+(* TODO: list of toplevel registrations for constant decoders,
+   as [tst -> (tag*dec)list] *)
+
+let create ~source tst : t =
+  {
+    src = source;
+    tst;
+    cache = ID_cache.create ~size:1024 ();
+    const_decode = Util.Str_map.empty;
+  }
+
+let decode_term (self : t) ~read_subterm ~tag : Term.t Dec.t =
+  match tag with
+  | "TV" ->
+    Dec.(
+      let+ v, ty = tup2 string read_subterm in
+      Term.var_str self.tst v ~ty)
+  | "Tv" ->
+    Dec.(
+      let+ idx, ty = tup2 int read_subterm in
+      Term.bvar_i self.tst idx ~ty)
+  | "T@" ->
+    Dec.(
+      let+ f, a = tup2 read_subterm read_subterm in
+      Term.app self.tst f a)
+  | "Ty" ->
+    Dec.(
+      let+ i = int in
+      Term.type_of_univ self.tst i)
+  | "Tl" ->
+    Dec.(
+      let+ v, ty, bod = tup3 string read_subterm read_subterm in
+      Term.DB.lam_db self.tst ~var_name:v ~var_ty:ty bod)
+  | "Tp" ->
+    Dec.(
+      let+ v, ty, bod = tup3 string read_subterm read_subterm in
+      Term.DB.pi_db self.tst ~var_name:v ~var_ty:ty bod)
+  | "Tc" ->
+    Dec.(
+      let* view = dict_field_opt "v" any and* c_tag = dict_field "tag" string in
+      let view = Option.value view ~default:Ser_value.null in
+      (* look for the decoder for this constant tag *)
+      (match Util.Str_map.find_opt c_tag self.const_decode with
+      | None -> failf "unknown constant tag %S" c_tag
+      | Some c_dec ->
+        let+ c = reflect_or_fail (c_dec read_subterm) view in
+        Term.const self.tst c))
+  | "Tf@" -> assert false (* TODO *)
+  | _ -> Dec.failf "unknown tag %S for a term" tag
+
+let rec read_term (self : t) (id : term_ref) : _ result =
+  (* decoder for subterms *)
+  let read_subterm : Term.t Dec.t =
+    Dec.(
+      let* id = int in
+      match read_term self id with
+      | Ok x -> return x
+      | Error e -> fail e)
+  in
+
+  ID_cache.get self.cache id ~compute:(fun id ->
+      match Tr.Source.get_entry self.src id with
+      | None -> Error (Printf.sprintf "invalid entry: %d" id)
+      | Some (tag, v) ->
+        let dec = decode_term self ~tag ~read_subterm in
+        Dec.run dec v |> Result.map_error Dec.Error.to_string)
diff --git a/src/core/t_trace_read.mli b/src/core/t_trace_read.mli
new file mode 100644
index 00000000..a384b88f
--- /dev/null
+++ b/src/core/t_trace_read.mli
@@ -0,0 +1,8 @@
+open Sidekick_core_logic
+module Tr = Sidekick_trace
+
+type term_ref = Tr.entry_id
+type t
+
+val create : source:Tr.Source.t -> Term.store -> t
+val read_term : t -> term_ref -> (Term.t, string) result