wip: tracing system

src/core/Sidekick_core.ml

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

src/core/dune

@@ -2,4 +2,5 @@
  (name Sidekick_core)
  (public_name sidekick.core)
  (flags :standard -open Sidekick_util)
- (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic))
+ (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic
+   sidekick.trace))

src/core/t_tracer.ml

@@ -0,0 +1,9 @@
+open Sidekick_core_logic
+module Tr = Sidekick_trace
+module T = Term
+
+type Tr.entry_view += private Def_term of { id: int }
+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

src/core/t_tracer.mli

@@ -0,0 +1,15 @@
+(** Emit terms in traces.
+
+  Traces will contains terms, encoded as a DAG. Each subterm is its own
+  event, and gets a term identifier used in other subsequent entries
+  to refer to it.
+*)
+
+open Sidekick_core_logic
+module Tr = Sidekick_trace
+
+type Tr.entry_view += private Def_term of { id: int }
+type t
+
+val create : sink:Tr.Sink.t -> unit -> t
+val emit : t -> Term.t -> Tr.Entry_id.t

src/trace/dune

@@ -0,0 +1,6 @@
+(library
+ (name Sidekick_trace)
+ (public_name sidekick.trace)
+ (synopsis "Trace system for sidekick.")
+ (flags :standard -open Sidekick_util)
+ (libraries containers iter sidekick.util sidekick.sigs sidekick.core-logic))

src/trace/entry_id.ml

@@ -0,0 +1,7 @@
+type t = int
+
+let pp = Fmt.int
+
+module Internal_ = struct
+  let make x = x
+end

src/trace/entry_id.mli

@@ -0,0 +1,9 @@
+type t = private int
+
+include Sidekick_sigs.PRINT with type t := t
+
+(**/*)
+module Internal_ : sig
+  val make : int -> t
+end
+(**/*)

src/trace/entry_view.ml

@@ -0,0 +1,6 @@
+
+
+type t = ..
+(** Extensible type, each entry uses its own.
+
+   See {!Entry.t}. *)

src/trace/sidekick_trace.ml

@@ -0,0 +1,29 @@
+(** Tracing.
+
+    Sidekick should be able to emit traces of some or all of the events
+    happening inside its components (SAT solver, SMT solver, theories,
+    etc.).
+
+    Traces can be written to disk and read back later from another
+    process.
+
+    The two initial intended use cases are:
+
+      - proof production (trace all inferences; reconstruct a proof from them
+        starting from the inference of [false])
+      - debugging (trace some inferences/internal states/partial models;
+        double check them later)
+
+*)
+
+open Sidekick_sigs
+
+(** {2 Exports} *)
+
+module Entry_view = Entry_view
+module Write_value = Write_value
+module Sink = Sink
+module Entry_id = Entry_id
+
+type entry_id = Entry_id.t
+type entry_view = Entry_view.t = ..

src/trace/sink.ml

@@ -0,0 +1,62 @@
+(** An IO sink for traces.
+
+    A trace is emitted on the fly into a sink. The sink collects or
+    writes entries that are emitted into it.
+*)
+
+module type S = sig
+  val emit : Write_value.t -> Entry_id.t
+end
+
+type t = (module S)
+(** Trace sink *)
+
+let[@inline] emit (module Sink : S) (v : Write_value.t) : Entry_id.t =
+  Sink.emit v
+
+let[@inline] emit' (self : t) v : unit = ignore (emit self v : Entry_id.t)
+
+let bencode_buf_ (buf:Buffer.t) (v:Write_value.t) : unit =
+
+  let[@inline] char c = Buffer.add_char buf c in
+  let[@inline] str s = Buffer.add_string buf s in
+  let[@inline] int i = Printf.bprintf buf "%d" i in
+
+    let rec enc_v (v:Write_value.t) : unit =
+      let module V = Write_value in
+      match v with
+      | V.Int i -> char 'i'; int i; char 'e'
+      | V.Bool true -> str "i1e"
+      | V.Bool false -> str "i0e"
+      | V.Str s | Bytes s ->
+          int (String.length s);
+          char ':';
+          str s
+      | V.List l ->
+          char 'l';
+          List.iter (fun v -> enc_v (v ())) l;
+          char 'e'
+      | V.Dict l ->
+          char 'd';
+          List.iter (fun (k,v) ->
+            enc_v (V.string k);
+            enc_v (v ())) l;
+          char 'e'
+    in
+    enc_v v
+
+(** A sink that emits entries using Bencode into the given channel *)
+let of_out_channel_using_bencode (oc: out_channel): t =
+  let id_ = ref 0 in
+  let buf = Buffer.create 128 in
+  (module struct
+    let emit (v:Write_value.t) =
+      assert (Buffer.length buf = 0);
+      let id = Entry_id.Internal_.make !id_ in
+      incr id_;
+      bencode_buf_ buf v;
+      Buffer.output_buffer oc buf;
+      Buffer.clear buf;
+      id
+
+  end)

src/trace/sink.mli

@@ -0,0 +1,20 @@
+(** An IO sink for traces.
+
+    A trace is emitted on the fly into a sink. The sink collects or
+    writes entries that are emitted into it.
+*)
+
+module type S = sig
+  val emit : Write_value.t -> Entry_id.t
+end
+
+type t = (module S)
+(** Trace sink *)
+
+val emit : t -> Write_value.t -> Entry_id.t
+
+val emit' : t -> Write_value.t -> unit
+
+(** A sink that emits entries using Bencode into the given channel *)
+val of_out_channel_using_bencode : out_channel -> t
+

src/trace/write_entry.ml

@@ -0,0 +1,8 @@
+type entry_view = Entry_view.t
+
+module type OPS = sig
+  val write : entry_view -> Write_value.t
+end
+
+type ops = (module OPS)
+type t = { view: entry_view; ops: ops }

src/trace/write_entry.mli

@@ -0,0 +1,27 @@
+(** Entry to be written.
+
+    This is used when producing a trace, to emit a new entry.
+*)
+
+type entry_view = Entry_view.t
+
+(** Dynamic operations for {!t} *)
+module type OPS = sig
+  val write : entry_view -> Write_value.t
+
+  (*
+  val pp : entry_view Fmt.printer
+  *)
+  (* TODO: read *)
+end
+
+type ops = (module OPS)
+
+type t = { view: entry_view; ops: ops }
+(** A single entry to be written into the trace.
+
+    A trace is consistuted of entries, numbered
+    from [0] to [n], in the order of their production.
+    The number has no semantics besides a form of
+    causal order.
+*)

src/trace/write_value.ml

@@ -0,0 +1,23 @@
+(** Value writer.
+
+    A [Writer.t] value, describes how to write some structured
+    data into a {!Sink.t}. It reflects the shape of the structured
+    data but does not commit to a particular serialization format.
+*)
+
+type t =
+  | Bool of bool
+  | Str of string
+  | Bytes of string
+  | Int of int
+  | List of delayed list
+  | Dict of (string * delayed) list
+
+and delayed = unit -> t
+
+let bool b : t = Bool b
+let int i : t = Int i
+let string x : t = Str x
+let bytes x : t = Bytes x
+let list x : t = List x
+let dict x : t = Dict x

src/trace/write_value.mli

@@ -0,0 +1,23 @@
+(** Value writer.
+
+    A [Writer.t] value, describes how to write some structured
+    data into a {!Sink.t}. It reflects the shape of the structured
+    data but does not commit to a particular serialization format.
+*)
+
+type t = private
+  | Bool of bool
+  | Str of string
+  | Bytes of string
+  | Int of int
+  | List of delayed list
+  | Dict of (string * delayed) list
+
+and delayed = unit -> t
+
+val bool : bool -> t
+val int : int -> t
+val string : string -> t
+val bytes : string -> t
+val list : delayed list -> t
+val dict : (string * delayed) list -> t