diff --git a/src/base/Form.ml b/src/base/Form.ml index aa47046d..bb8d3184 100644 --- a/src/base/Form.ml +++ b/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)); diff --git a/src/base/Ty.ml b/src/base/Ty.ml index 26e35434..823ad41c 100644 --- a/src/base/Ty.ml +++ b/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)); diff --git a/src/base/Uconst.ml b/src/base/Uconst.ml index 250249d6..b295f67e 100644 --- a/src/base/Uconst.ml +++ b/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, diff --git a/src/bencode/Sidekick_bencode.ml b/src/bencode/Sidekick_bencode.ml index 2681ea3e..cb32c3e3 100644 --- a/src/bencode/Sidekick_bencode.ml +++ b/src/bencode/Sidekick_bencode.ml @@ -45,8 +45,8 @@ end module Decode = struct exception Fail - let of_string s = - let i = ref 0 in + let of_string ?(idx = 0) s = + 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 = - match of_string s with + let of_string_exn ?idx s = + match of_string ?idx s with | Some x -> x | None -> failwith "bencode.decode: invalid string" end diff --git a/src/bencode/Sidekick_bencode.mli b/src/bencode/Sidekick_bencode.mli index 1a377b67..4b521156 100644 --- a/src/bencode/Sidekick_bencode.mli +++ b/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 diff --git a/src/core-logic/const.ml b/src/core-logic/const.ml index 51bfeddb..46b1c639 100644 --- a/src/core-logic/const.ml +++ b/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.t Ser_decode.t -> view Ser_decode.t)) list + (string * Ops.t * (term Ser_decode.t -> view Ser_decode.t)) list diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli index 8f635df1..8fdd2f2d 100644 --- a/src/core-logic/const.mli +++ b/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.t Ser_decode.t -> view Ser_decode.t)) list + (string * Ops.t * (term 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. *) diff --git a/src/core-logic/str_const.ml b/src/core-logic/str_const.ml index ddb61ed1..3da8fe85 100644 --- a/src/core-logic/str_const.ml +++ b/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, diff --git a/src/core-logic/t_builtins.ml b/src/core-logic/t_builtins.ml index 5977036a..95cf4834 100644 --- a/src/core-logic/t_builtins.ml +++ b/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 -> diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index 32114358..25545ea5 100644 --- a/src/core/Sidekick_core.ml +++ b/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 diff --git a/src/core/box.ml b/src/core/box.ml index 53e9f14a..09c964a8 100644 --- a/src/core/box.ml +++ b/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, diff --git a/src/core/gensym.ml b/src/core/gensym.ml index c24ade0e..a171ea64 100644 --- a/src/core/gensym.ml +++ b/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, diff --git a/src/core/t_trace_read.ml b/src/core/t_trace_reader.ml similarity index 97% rename from src/core/t_trace_read.ml rename to src/core/t_trace_reader.ml index c6745712..4e1df71f 100644 --- a/src/core/t_trace_read.ml +++ b/src/core/t_trace_reader.ml @@ -15,8 +15,7 @@ type t = { (** tag -> const decoder *) } -let add_const_decoders (self : t) decs : unit = - let decs = decs self.tst in +let add_const_decoders (self : t) (decs : Const.decoders) : unit = List.iter (fun (tag, ops, dec) -> (* check that there is no tag collision *) diff --git a/src/core/t_trace_read.mli b/src/core/t_trace_reader.mli similarity index 100% rename from src/core/t_trace_read.mli rename to src/core/t_trace_reader.mli diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml index 1e1de9b7..c7e72dc5 100644 --- a/src/main/pure_sat_solver.ml +++ b/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, diff --git a/src/trace/sidekick_trace.ml b/src/trace/sidekick_trace.ml index 7b8965b4..046fd0e6 100644 --- a/src/trace/sidekick_trace.ml +++ b/src/trace/sidekick_trace.ml @@ -16,8 +16,6 @@ *) -open Sidekick_sigs - (** {2 Exports} *) module Entry_view = Entry_view diff --git a/src/trace/sink.ml b/src/trace/sink.ml index 8c1d2833..948f65d7 100644 --- a/src/trace/sink.ml +++ b/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' = - Ser_value.(dict_of_list [ "id", int !id_; "T", string tag; "v", v ]) - in + let v' = Ser_value.(list [ int id; string tag; 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) diff --git a/src/trace/sink.mli b/src/trace/sink.mli index ad7ebf7c..15e6091e 100644 --- a/src/trace/sink.mli +++ b/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. *) diff --git a/src/trace/source.ml b/src/trace/source.ml index b4cfa0cf..aef90071 100644 --- a/src/trace/source.ml +++ b/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) diff --git a/src/trace/source.mli b/src/trace/source.mli index 6bbbd5d4..e0f1ec49 100644 --- a/src/trace/source.mli +++ b/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 *)