change signature of Const.decoders; add bencode decoder

src/base/Form.ml

@@ -50,7 +50,6 @@ let ops =
   { Const.Ops.pp; equal; hash; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
     ("and", ops, Ser_decode.(fun _ -> return C_and));
     ("or", ops, Ser_decode.(fun _ -> return C_or));

src/base/Ty.ml

@@ -50,7 +50,6 @@ let ops_ty =
   { Const.Ops.pp; equal; hash; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
     ("ty.Real", ops_ty, Ser_decode.(fun _ -> return @@ Ty Ty_real));
     ("ty.Int", ops_ty, Ser_decode.(fun _ -> return @@ Ty Ty_int));

src/base/Uconst.ml

@@ -37,7 +37,6 @@ let ops =
   { Const.Ops.pp; equal; hash; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
     ( "uc",
       ops,

src/bencode/Sidekick_bencode.ml

@@ -45,8 +45,8 @@ end
 module Decode = struct
   exception Fail
 
-  let of_string s =
+  let of_string ?(idx = 0) s =
-    let i = ref 0 in
+    let i = ref idx in
 
     let[@inline] check_not_eof () =
       if !i >= String.length s then raise_notrace Fail
@@ -113,8 +113,8 @@ module Decode = struct
 
     try Some (top ()) with Fail -> None
 
-  let of_string_exn s =
+  let of_string_exn ?idx s =
-    match of_string s with
+    match of_string ?idx s with
     | Some x -> x
     | None -> failwith "bencode.decode: invalid string"
 end

src/bencode/Sidekick_bencode.mli

@@ -6,9 +6,11 @@ module Encode : sig
 end
 
 module Decode : sig
-  val of_string : string -> t option
+  val of_string : ?idx:int -> string -> t option
+  (** Decode string.
+    @param idx initial index (default 0) *)
 
-  val of_string_exn : string -> t
+  val of_string_exn : ?idx:int -> string -> t
   (** Parse string.
       @raise Error.Error if the string is not valid bencode. *)
 end

src/core-logic/const.ml

@@ -27,5 +27,4 @@ let ser ~ser_t (self : t) = self.c_ops.ser ser_t self.c_view
 let make c_view c_ops ~ty:c_ty : t = { c_view; c_ops; c_ty }
 
 type decoders =
-  Term.store ->
+  (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list
-  (string * Ops.t * (Term.t Ser_decode.t -> view Ser_decode.t)) list

src/core-logic/const.mli

@@ -25,8 +25,7 @@ val ser : ser_t:(term -> Ser_value.t) -> t -> string * Ser_value.t
 val ty : t -> term
 
 type decoders =
-  Term.store ->
+  (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list
-  (string * Ops.t * (Term.t Ser_decode.t -> view Ser_decode.t)) list
 (** Decoders for constants: given a term store, return a list
     of supported tags, and for each tag, a decoder for constants
     that have this particular tag. *)

src/core-logic/str_const.ml

@@ -26,7 +26,6 @@ let ops =
   { Const.Ops.pp; equal; hash; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
     ( "c.str",
       ops,

src/core-logic/t_builtins.ml

@@ -45,13 +45,12 @@ let ops : const_ops =
   in
 
   let pp out self = Fmt.string out (to_string self) in
-  let ser _sink self = "builtin", Ser_value.(string (to_string self)) in
+  let ser _sink self = "B", Ser_value.(string (to_string self)) in
   { Const.Ops.equal; hash; pp; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
-    ( "builtin",
+    ( "B",
       ops,
       Ser_decode.(
         fun _dec_term ->

src/core/Sidekick_core.ml

@@ -23,6 +23,7 @@ module Term = struct
   include Sidekick_core_logic.T_builtins
   include T_printer
   module Tracer = T_tracer
+  module Trace_reader = T_trace_reader
 end
 
 module Gensym = Gensym

src/core/box.ml

@@ -26,7 +26,6 @@ let ops =
   { Const.Ops.pp; equal; hash; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
     ( "box",
       ops,

src/core/gensym.ml

@@ -37,7 +37,6 @@ let ops =
   { Const.Ops.equal; hash; pp; ser }
 
 let const_decoders : Const.decoders =
- fun _tst ->
   [
     ( "gensym",
       ops,

src/core/t_trace_reader.ml

@@ -15,8 +15,7 @@ type t = {
       (** tag -> const decoder *)
 }
 
-let add_const_decoders (self : t) decs : unit =
+let add_const_decoders (self : t) (decs : Const.decoders) : unit =
-  let decs = decs self.tst in
   List.iter
     (fun (tag, ops, dec) ->
       (* check that there is no tag collision *)

src/main/pure_sat_solver.ml

@@ -34,7 +34,6 @@ end = struct
     { Const.Ops.equal; hash; pp; ser }
 
   let const_decoders : Const.decoders =
-   fun _tst ->
     [
       ( "sat.lit",
         ops,

src/trace/sidekick_trace.ml

@@ -16,8 +16,6 @@
 
 *)
 
-open Sidekick_sigs
-
 (** {2 Exports} *)
 
 module Entry_view = Entry_view

src/trace/sink.ml

@@ -26,12 +26,21 @@ let of_out_channel_using_bencode (oc : out_channel) : t =
       assert (Buffer.length buf = 0);
       let id = Entry_id.of_int_unsafe !id_ in
       (* add tag+id around *)
-      let v' =
+      let v' = Ser_value.(list [ int id; string tag; v ]) in
-        Ser_value.(dict_of_list [ "id", int !id_; "T", string tag; "v", v ])
-      in
       incr id_;
       Sidekick_bencode.Encode.to_buffer buf v';
       Buffer.output_buffer oc buf;
       Buffer.clear buf;
       id
   end)
+
+let of_buffer_using_bencode (buf : Buffer.t) : t =
+  (module struct
+    let emit ~tag (v : Ser_value.t) =
+      let id = Entry_id.of_int_unsafe @@ Buffer.length buf in
+      (* add tag+id around *)
+      let v' = Ser_value.(list [ int id; string tag; v ]) in
+      Sidekick_bencode.Encode.to_buffer buf v';
+      Buffer.add_char buf '\n';
+      id
+  end)

src/trace/sink.mli

@@ -18,3 +18,6 @@ val emit' : t -> tag:tag -> Ser_value.t -> unit
 
 val of_out_channel_using_bencode : out_channel -> t
 (** A sink that emits entries using Bencode into the given channel *)
+
+val of_buffer_using_bencode : Buffer.t -> t
+(** Emit entries into the given buffer, in Bencode. *)

src/trace/source.ml

@@ -13,3 +13,35 @@ let get_entry (module S : S) id : _ option =
   try Some (S.get_entry id) with Not_found -> None
 
 let iter_all (module S : S) f : unit = S.iter_all f
+
+let decode_bencode_entry_ =
+  Ser_decode.(
+    let+ id, tag, view = tup3 int string any in
+    id, tag, view)
+
+let of_string_using_bencode (str : string) : t =
+  (module struct
+    let iter_all f =
+      let i = ref 0 in
+      while !i < String.length str do
+        match Sidekick_bencode.Decode.of_string ~idx:!i str with
+        | None -> i := String.length str
+        | Some b ->
+          (match Ser_decode.run decode_bencode_entry_ b with
+          | Error err ->
+            Error.errorf "cannot decode string entry: %a" Ser_decode.Error.pp
+              err
+          | Ok (id, tag, v) -> f id ~tag v)
+      done
+
+    let get_entry id : tag * Ser_value.t =
+      match Sidekick_bencode.Decode.of_string str ~idx:id with
+      | None -> Error.errorf "invalid offset %d" id
+      | Some b ->
+        (match Ser_decode.run decode_bencode_entry_ b with
+        | Error err ->
+          Error.errorf "cannot decode string entry: %a" Ser_decode.Error.pp err
+        | Ok (_id, tag, v) ->
+          assert (id = _id);
+          tag, v)
+  end)

src/trace/source.mli

@@ -20,3 +20,6 @@ type t = (module S)
 val get_entry : t -> Entry_id.t -> (tag * Ser_value.t) option
 val get_entry_exn : t -> Entry_id.t -> tag * Ser_value.t
 val iter_all : t -> (Entry_id.t -> tag:tag -> Ser_value.t -> unit) -> unit
+
+val of_string_using_bencode : string -> t
+(** Decode string, where entries are offsets *)