feat(tracing): introduce term/const serialization

- use a record instead of 1st class module for `Const.ops`, so it
  can be mutually recursive with the definition of `term`
- remove unused `Const.ops.opaque_to_cc`
- constants are serializable using `Ser_value`

src/arith/sidekick_arith.ml

@@ -7,6 +7,8 @@ module type NUM = sig
   val abs : t -> t
   val sign : t -> int
   val of_int : int -> t
+  val to_string : t -> string
+  val of_string : string -> t option
 
   include Sidekick_sigs.EQ with type t := t
   include Sidekick_sigs.ORD with type t := t

src/base/Data_ty.ml

@@ -81,31 +81,39 @@ type Const.view +=
   | Is_a of cstor
 
 let ops =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | Data d -> pp out d
-      | Data d -> pp out d
+    | Cstor c -> Cstor.pp out c
-      | Cstor c -> Cstor.pp out c
+    | Select s -> Select.pp out s
-      | Select s -> Select.pp out s
+    | Is_a c -> Fmt.fprintf out "(_ is %a)" Cstor.pp c
-      | Is_a c -> Fmt.fprintf out "(_ is %a)" Cstor.pp c
+    | _ -> assert false
-      | _ -> assert false
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | Data a, Data b -> equal a b
+    | Data a, Data b -> equal a b
-      | Cstor a, Cstor b -> Cstor.equal a b
+    | Cstor a, Cstor b -> Cstor.equal a b
-      | Select a, Select b -> Select.equal a b
+    | Select a, Select b -> Select.equal a b
-      | Is_a a, Is_a b -> Cstor.equal a b
+    | Is_a a, Is_a b -> Cstor.equal a b
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Data d -> Hash.combine2 592 (hash d)
+    | Data d -> Hash.combine2 592 (hash d)
-      | Cstor c -> Hash.combine2 593 (Cstor.hash c)
+    | Cstor c -> Hash.combine2 593 (Cstor.hash c)
-      | Select s -> Hash.combine2 594 (Select.hash s)
+    | Select s -> Hash.combine2 594 (Select.hash s)
-      | Is_a c -> Hash.combine2 595 (Cstor.hash c)
+    | Is_a c -> Hash.combine2 595 (Cstor.hash c)
-      | _ -> assert false
+    | _ -> assert false
+  in
+  let ser ser_t = function
+    | Data d -> assert false (* TODO *)
+    | Cstor c -> assert false (* TODO *)
+    | Select s -> assert false (* TODO *)
+    | Is_a c -> assert false (* TODO *)
+    | _ -> assert false
+  in
 
-    let opaque_to_cc _ = false
+  { Const.Ops.pp; hash; equal; ser }
-  end : Const.DYN_OPS)
 
 let data_as_ty (d : data) = Lazy.force d.data_as_ty
 

src/base/Form.ml

@@ -18,27 +18,36 @@ type 'a view = 'a Sidekick_core.Bool_view.t =
 
 type Const.view += C_and | C_or | C_imply
 
-let ops : Const.ops =
+let ops =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | C_and -> Fmt.string out "and"
-      | C_and -> Fmt.string out "and"
+    | C_or -> Fmt.string out "or"
-      | C_or -> Fmt.string out "or"
+    | C_imply -> Fmt.string out "=>"
-      | C_imply -> Fmt.string out "=>"
+    | _ -> assert false
-      | _ -> assert false
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | C_and, C_and | C_or, C_or | C_imply, C_imply -> true
+    | C_and, C_and | C_or, C_or | C_imply, C_imply -> true
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | C_and -> Hash.int 425
+    | C_and -> Hash.int 425
-      | C_or -> Hash.int 426
+    | C_or -> Hash.int 426
-      | C_imply -> Hash.int 427
+    | C_imply -> Hash.int 427
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let opaque_to_cc _ = true
+  let ser _sink =
-  end)
+    Ser_value.(
+      function
+      | C_and -> "and", null
+      | C_or -> "or", null
+      | C_imply -> "=>", null
+      | _ -> assert false)
+  in
+  { Const.Ops.pp; equal; hash; ser }
 
 (* ### view *)
 

src/base/ID.ml

@@ -21,6 +21,14 @@ let pp_name out a = CCFormat.string out a.name
 let pp = pp_name
 let to_string_full a = Printf.sprintf "%s/%d" a.name a.id
 
+let ser (self : t) =
+  Ser_value.(dict_of_list [ "id", int self.id; "n", string self.name ])
+
+let deser =
+  Ser_decode.(
+    let+ id = dict_field "id" int and+ name = dict_field "n" string in
+    { id; name })
+
 module AsKey = struct
   type nonrec t = t
 

src/base/ID.mli

@@ -37,6 +37,9 @@ val to_string : t -> string
 val to_string_full : t -> string
 (** Printer name and unique counter for this ID. *)
 
+val ser : t -> Ser_value.t
+val deser : t Ser_decode.t
+
 include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
 
 val pp_name : t CCFormat.printer

src/base/LRA_term.ml

@@ -17,6 +17,15 @@ module Pred = struct
     | Gt -> ">"
     | Geq -> ">="
 
+  let of_string = function
+    | "<" -> Some Lt
+    | "<=" -> Some Leq
+    | "!=_LRA" -> Some Neq
+    | "=_LRA" -> Some Eq
+    | ">" -> Some Gt
+    | ">=" -> Some Geq
+    | _ -> None
+
   let equal : t -> t -> bool = ( = )
   let hash : t -> int = Hashtbl.hash
   let pp out p = Fmt.string out (to_string p)
@@ -29,6 +38,11 @@ module Op = struct
     | Plus -> "+"
     | Minus -> "-"
 
+  let of_string = function
+    | "+" -> Some Plus
+    | "-" -> Some Minus
+    | _ -> None
+
   let equal : t -> t -> bool = ( = )
   let hash : t -> int = Hashtbl.hash
   let pp out p = Fmt.string out (to_string p)
@@ -90,32 +104,60 @@ type term = Term.t
 type ty = Term.t
 type Const.view += Const of Q.t | Pred of Pred.t | Op of Op.t | Mult_by of Q.t
 
-let ops : Const.ops =
+let ops =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | Const q -> Q.pp_print out q
-      | Const q -> Q.pp_print out q
+    | Pred p -> Pred.pp out p
-      | Pred p -> Pred.pp out p
+    | Op o -> Op.pp out o
-      | Op o -> Op.pp out o
+    | Mult_by q -> Fmt.fprintf out "(* %a)" Q.pp_print q
-      | Mult_by q -> Fmt.fprintf out "(* %a)" Q.pp_print q
+    | _ -> assert false
-      | _ -> assert false
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | Const a, Const b -> Q.equal a b
+    | Const a, Const b -> Q.equal a b
-      | Pred a, Pred b -> Pred.equal a b
+    | Pred a, Pred b -> Pred.equal a b
-      | Op a, Op b -> Op.equal a b
+    | Op a, Op b -> Op.equal a b
-      | Mult_by a, Mult_by b -> Q.equal a b
+    | Mult_by a, Mult_by b -> Q.equal a b
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Const q -> Sidekick_zarith.Rational.hash q
+    | Const q -> Sidekick_zarith.Rational.hash q
-      | Pred p -> Pred.hash p
+    | Pred p -> Pred.hash p
-      | Op o -> Op.hash o
+    | Op o -> Op.hash o
-      | Mult_by q -> Hash.(combine2 135 (Sidekick_zarith.Rational.hash q))
+    | Mult_by q -> Hash.(combine2 135 (Sidekick_zarith.Rational.hash q))
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let opaque_to_cc _ = true
+  let ser _sink =
-  end)
+    Ser_value.(
+      function
+      | Const q -> "Qn", string (Sidekick_zarith.Rational.to_string q)
+      | Pred p -> "Qp", string (Pred.to_string p)
+      | Op o -> "Qo", string (Op.to_string o)
+      | Mult_by q -> "Q*", string (Sidekick_zarith.Rational.to_string q)
+      | _ -> assert false)
+  in
+  { Const.Ops.equal; hash; ser; pp }
+
+(* TODO
+   let deser _tst =
+     Ser_decode.
+       [
+         ( "Qn",
+           let* s = string in
+           let+ q =
+             unwrap_opt "expected rational number"
+               (Sidekick_zarith.Rational.of_string s)
+           in
+           Const q );
+         ( "Qp",
+           let* s = string in
+           let+ p = unwrap_opt "expected predicate" (Pred.of_string s) in
+           Pred p );
+       ]
+*)
 
 let real tst = Ty.real tst
 let has_ty_real t = Ty.is_real (T.ty t)

src/base/Ty.ml

@@ -8,35 +8,46 @@ let pp = pp_debug
 type Const.view += Ty of ty_view
 type data = Types_.data
 
-let ops_ty : Const.ops =
+let ops_ty =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | Ty ty ->
-      | Ty ty ->
+      (match ty with
-        (match ty with
+      | Ty_real -> Fmt.string out "Real"
-        | Ty_real -> Fmt.string out "Real"
+      | Ty_int -> Fmt.string out "Int"
-        | Ty_int -> Fmt.string out "Int"
+      | Ty_uninterpreted { id; _ } -> ID.pp out id)
-        | Ty_uninterpreted { id; _ } -> ID.pp out id)
+    | _ -> ()
-      | _ -> ()
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | Ty a, Ty b ->
+    | Ty a, Ty b ->
-        (match a, b with
+      (match a, b with
-        | Ty_int, Ty_int | Ty_real, Ty_real -> true
+      | Ty_int, Ty_int | Ty_real, Ty_real -> true
-        | Ty_uninterpreted u1, Ty_uninterpreted u2 -> ID.equal u1.id u2.id
+      | Ty_uninterpreted u1, Ty_uninterpreted u2 -> ID.equal u1.id u2.id
-        | (Ty_real | Ty_int | Ty_uninterpreted _), _ -> false)
+      | (Ty_real | Ty_int | Ty_uninterpreted _), _ -> false)
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Ty a ->
+    | Ty a ->
+      (match a with
+      | Ty_real -> Hash.int 2
+      | Ty_int -> Hash.int 3
+      | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id))
+    | _ -> assert false
+  in
+
+  let ser _sink = function
+    | Ty a ->
+      Ser_value.(
         (match a with
-        | Ty_real -> Hash.int 2
+        | Ty_real -> "ty.Real", null
-        | Ty_int -> Hash.int 3
+        | Ty_int -> "ty.Int", null
-        | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id))
+        | Ty_uninterpreted { id; finite } ->
-      | _ -> assert false
+          "ty.id", dict_of_list [ "id", ID.ser id; "fin", bool finite ]))
-
+    | _ -> assert false
-    let opaque_to_cc _ = true
+  in
-  end)
+  { Const.Ops.pp; equal; hash; ser }
 
 open struct
   let mk_ty0 tst view =

src/base/Uconst.ml

@@ -13,22 +13,28 @@ let pp out c = ID.pp out c.uc_id
 type Const.view += Uconst of t
 
 let ops =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | Uconst c -> pp out c
-      | Uconst c -> pp out c
+    | _ -> assert false
-      | _ -> assert false
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | Uconst a, Uconst b -> equal a b
+    | Uconst a, Uconst b -> equal a b
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Uconst c -> Hash.combine2 522660 (hash c)
+    | Uconst c -> Hash.combine2 522660 (hash c)
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let opaque_to_cc _ = false
+  let ser ser_t = function
-  end : Const.DYN_OPS)
+    | Uconst { uc_id; uc_ty } ->
+      "uc", Ser_value.(list [ ID.ser uc_id; ser_t uc_ty ])
+    | _ -> assert false
+  in
+  { Const.Ops.pp; equal; hash; ser }
 
 let[@inline] make uc_id uc_ty : t = { uc_id; uc_ty }
 

src/bencode/Sidekick_bencode.ml

@@ -10,6 +10,7 @@ module Encode = struct
 
     let rec enc_v (v : t) : unit =
       match v with
+      | Null -> str "0:"
       | Int i ->
         char 'i';
         int i;

src/core-logic/bvar.ml

@@ -5,5 +5,6 @@ type t = bvar = { bv_idx: int; bv_ty: term }
 let equal (v1 : t) v2 = v1.bv_idx = v2.bv_idx && Term_.equal v1.bv_ty v2.bv_ty
 let hash v = H.combine2 (H.int v.bv_idx) (Term_.hash v.bv_ty)
 let pp out v = Fmt.fprintf out "bv[%d]" v.bv_idx
+let[@inline] idx self = self.bv_idx
 let[@inline] ty self = self.bv_ty
 let make i ty : t = { bv_idx = i; bv_ty = ty }

src/core-logic/bvar.mli

@@ -7,4 +7,5 @@ type t = bvar = { bv_idx: int; bv_ty: term }
 include EQ_HASH_PRINT with type t := t
 
 val make : int -> term -> t
+val idx : t -> int
 val ty : t -> term

src/core-logic/const.ml

@@ -2,32 +2,26 @@ open Types_
 
 type view = const_view = ..
 
-module type DYN_OPS = sig
+module Ops = struct
-  val pp : view Fmt.printer
+  type t = const_ops = {
-  val equal : view -> view -> bool
+    pp: const_view Fmt.printer;  (** Pretty-print constant *)
-  val hash : view -> int
+    equal: const_view -> const_view -> bool;
-  (* TODO
+    hash: const_view -> int;  (** Hash constant *)
-     val ser : view -> Ser_value.t
+    ser: (term -> Ser_value.t) -> const_view -> string * Ser_value.t;
-     val deser : view Ser_decode.t
+  }
-  *)
 end
 
-type ops = (module DYN_OPS)
+type t = const = { c_view: view; c_ops: Ops.t; c_ty: term }
-type t = const = { c_view: view; c_ops: ops; c_ty: term }
 
 let[@inline] view self = self.c_view
 let[@inline] ty self = self.c_ty
 
-let equal (a : t) b =
+let[@inline] equal (a : t) b =
-  let (module O) = a.c_ops in
+  a.c_ops.equal a.c_view b.c_view && Term_.equal a.c_ty b.c_ty
-  O.equal a.c_view b.c_view && Term_.equal a.c_ty b.c_ty
 
-let hash (a : t) : int =
+let[@inline] hash (a : t) : int =
-  let (module O) = a.c_ops in
+  H.combine2 (a.c_ops.hash a.c_view) (Term_.hash a.c_ty)
-  H.combine2 (O.hash a.c_view) (Term_.hash a.c_ty)
-
-let pp out (a : t) =
-  let (module O) = a.c_ops in
-  O.pp out a.c_view
 
+let pp out (a : t) = a.c_ops.pp out a.c_view
+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 }

src/core-logic/const.mli

@@ -6,21 +6,22 @@ open Types_
 
 type view = const_view = ..
 
-module type DYN_OPS = sig
+module Ops : sig
-  val pp : view Fmt.printer
+  type t = const_ops = {
-  val equal : view -> view -> bool
+    pp: const_view Fmt.printer;  (** Pretty-print constant *)
-  val hash : view -> int
+    equal: const_view -> const_view -> bool;
-  (* TODO
+        (** Equality of constant with any other constant *)
-     val ser : view -> Ser_value.t
+    hash: const_view -> int;  (** Hash constant *)
-     val deser : view Ser_decode.t
+    ser: (term -> Ser_value.t) -> const_view -> string * Ser_value.t;
-  *)
+        (** Serialize a constant, along with a tag to recognize it. *)
+  }
 end
 
-type ops = (module DYN_OPS)
+type t = const = { c_view: view; c_ops: Ops.t; c_ty: term }
-type t = const = { c_view: view; c_ops: ops; c_ty: term }
 
 val view : t -> view
-val make : view -> ops -> ty:term -> t
+val make : view -> Ops.t -> ty:term -> t
+val ser : ser_t:(term -> Ser_value.t) -> t -> string * Ser_value.t
 val ty : t -> term
 
 include EQ_HASH_PRINT with type t := t

src/core-logic/sidekick_core_logic.ml

@@ -4,6 +4,7 @@ module Bvar = Bvar
 module Const = Const
 module Subst = Subst
 module T_builtins = T_builtins
+module Ser_sink = Ser_sink
 module Store = Term.Store
 
 (* TODO: move to separate library? *)

src/core-logic/str_const.ml

@@ -2,22 +2,29 @@ open Types_
 
 type const_view += Str of string
 
-let ops : Const.ops =
+let ops =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | Str s -> Fmt.string out s
-      | Str s -> Fmt.string out s
+    | _ -> assert false
-      | _ -> assert false
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | Str s1, Str s2 -> s1 = s2
+    | Str s1, Str s2 -> s1 = s2
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Str s -> CCHash.string s
+    | Str s -> CCHash.string s
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let opaque_to_cc _ = false
+  let ser _sink = function
-  end)
+    | Str s -> "c.str", Ser_value.string s
+    | _ -> assert false
+  in
+  { Const.Ops.pp; equal; hash; ser }
+
+(* TODO: deser *)
 
 let make name ~ty : Const.t = Const.make (Str name) ops ~ty

src/core-logic/t_builtins.ml

@@ -3,39 +3,59 @@ open Term
 
 type const_view += C_bool | C_eq | C_ite | C_not | C_true | C_false
 
+let to_string = function
+  | C_bool -> "Bool"
+  | C_eq -> "="
+  | C_ite -> "ite"
+  | C_not -> "not"
+  | C_true -> "true"
+  | C_false -> "false"
+  | _ -> assert false
+
+let of_string = function
+  | "Bool" -> Some C_bool
+  | "=" -> Some C_eq
+  | "ite" -> Some C_ite
+  | "not" -> Some C_not
+  | "true" -> Some C_true
+  | "false" -> Some C_false
+  | _ -> None
+
 let ops : const_ops =
-  (module struct
+  let equal a b =
-    let equal a b =
+    match a, b with
-      match a, b with
+    | C_bool, C_bool
-      | C_bool, C_bool
+    | C_eq, C_eq
-      | C_eq, C_eq
+    | C_ite, C_ite
-      | C_ite, C_ite
+    | C_not, C_not
-      | C_not, C_not
+    | C_true, C_true
-      | C_true, C_true
+    | C_false, C_false ->
-      | C_false, C_false ->
+      true
-        true
+    | _ -> false
-      | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | C_bool -> CCHash.int 167
+    | C_bool -> CCHash.int 167
-      | C_eq -> CCHash.int 168
+    | C_eq -> CCHash.int 168
-      | C_ite -> CCHash.int 169
+    | C_ite -> CCHash.int 169
-      | C_not -> CCHash.int 170
+    | C_not -> CCHash.int 170
-      | C_true -> CCHash.int 171
+    | C_true -> CCHash.int 171
-      | C_false -> CCHash.int 172
+    | C_false -> CCHash.int 172
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let pp out = function
+  let pp out self = Fmt.string out (to_string self) in
-      | C_bool -> Fmt.string out "Bool"
+  let ser _sink self = "builtin", Ser_value.(string (to_string self)) in
-      | C_eq -> Fmt.string out "="
+  { Const.Ops.equal; hash; pp; ser }
-      | C_ite -> Fmt.string out "ite"
-      | C_not -> Fmt.string out "not"
-      | C_true -> Fmt.string out "true"
-      | C_false -> Fmt.string out "false"
-      | _ -> assert false
 
-    let opaque_to_cc _ = false
+(* TODO
-  end)
+   let deser _tst =
+     Ser_decode.(
+       let* v = string in
+       match of_string v with
+       | Some c -> return c
+       | None -> fail "expected builtin")
+*)
 
 let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store)
 let true_ store = const store @@ Const.make C_true ops ~ty:(bool store)

src/core-logic/t_builtins.mli

@@ -13,6 +13,11 @@ val true_ : store -> t
 val false_ : store -> t
 val bool_val : store -> bool -> t
 
+(* TODO
+   val deser : Term.store -> (string * Term.t) Ser_decode.t list
+   (** Deserializers, to be registered *)
+*)
+
 val eq : store -> t -> t -> t
 (** [eq a b] is [a = b] *)
 

src/core-logic/term.ml

@@ -1,7 +1,7 @@
 open Types_
 
-type nonrec var = var
+type var = Var.t
-type nonrec bvar = bvar
+type bvar = Bvar.t
 type nonrec term = term
 
 type view = term_view =

src/core-logic/term.mli

@@ -9,8 +9,8 @@
 
 open Types_
 
-type nonrec var = var
+type var = Var.t
-type nonrec bvar = bvar
+type bvar = Bvar.t
 type nonrec term = term
 
 type t = term

src/core-logic/types_.ml

@@ -2,27 +2,6 @@ module H = CCHash
 
 type const_view = ..
 
-module type DYN_CONST_OPS = sig
-  val pp : const_view Fmt.printer
-  (** Pretty-print constant *)
-
-  val equal : const_view -> const_view -> bool
-  (** Equality of constant with any other constant *)
-
-  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)
-
 type term_view =
   | E_type of int
   | E_var of var
@@ -41,6 +20,15 @@ and var = { v_name: string; v_ty: term }
 and bvar = { bv_idx: int; bv_ty: term }
 and const = { c_view: const_view; c_ops: const_ops; c_ty: term }
 
+and const_ops = {
+  pp: const_view Fmt.printer;  (** Pretty-print constant *)
+  equal: const_view -> const_view -> bool;
+      (** Equality of constant with any other constant *)
+  hash: const_view -> int;  (** Hash constant *)
+  ser: (term -> Ser_value.t) -> const_view -> string * Ser_value.t;
+      (** Serialize a constant, along with a tag to recognize it. *)
+}
+
 and term = {
   view: term_view;
   (* computed on demand *)

src/core/box.ml

@@ -2,23 +2,28 @@ open Sidekick_core_logic
 
 type Const.view += Box of Term.t
 
-let ops : Const.ops =
+let ops =
-  (module struct
+  let pp out = function
-    let pp out = function
+    | Box t -> Fmt.fprintf out "(@[box@ %a@])" Term.pp_debug t
-      | Box t -> Fmt.fprintf out "(@[box@ %a@])" Term.pp_debug t
+    | _ -> assert false
-      | _ -> assert false
+  in
 
-    let equal a b =
+  let equal a b =
-      match a, b with
+    match a, b with
-      | Box a, Box b -> Term.equal a b
+    | Box a, Box b -> Term.equal a b
-      | _ -> false
+    | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Box t -> Hash.(combine2 10 (Term.hash t))
+    | Box t -> Hash.(combine2 10 (Term.hash t))
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let opaque_to_cc _ = false
+  let ser ser_t = function
-  end)
+    | Box t -> "box", ser_t t
+    | _ -> assert false
+  in
+  { Const.Ops.pp; equal; hash; ser }
 
 let as_box t =
   match Term.view t with

src/core/gensym.ml

@@ -9,29 +9,32 @@ type Const.view +=
       gensym_id: int;  (** Id of the gensym *)
       pre: string;  (** Printing prefix *)
       ty: ty;
-      opaque_to_cc: bool;
     }
 
 let ops =
-  (module struct
+  let equal a b =
-    let equal a b =
+    match a, b with
-      match a, b with
+    | Fresh a, Fresh b -> a.id = b.id && a.gensym_id = b.gensym_id
-      | Fresh a, Fresh b -> a.id = b.id && a.gensym_id = b.gensym_id
+    | _ -> false
-      | _ -> false
+  in
 
-    let hash = function
+  let hash = function
-      | Fresh { id; gensym_id; _ } ->
+    | Fresh { id; gensym_id; _ } ->
-        Hash.combine3 15232 (Hash.int id) (Hash.int gensym_id)
+      Hash.combine3 15232 (Hash.int id) (Hash.int gensym_id)
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let pp out = function
+  let pp out = function
-      | Fresh { id; pre; _ } -> Fmt.fprintf out "$%s[%d]" pre id
+    | Fresh { id; pre; _ } -> Fmt.fprintf out "$%s[%d]" pre id
-      | _ -> assert false
+    | _ -> assert false
+  in
 
-    let opaque_to_cc = function
+  let ser ser_t = function
-      | Fresh f -> f.opaque_to_cc
+    | Fresh { id; pre; ty; _ } ->
-      | _ -> assert false
+      "gensym", Ser_value.(list [ int id; string pre; ser_t ty ])
-  end : Const.DYN_OPS)
+    | _ -> assert false
+  in
+  { Const.Ops.equal; hash; pp; ser }
 
 type t = { tst: Term.store; self_id: int; mutable fresh: int }
 
@@ -45,13 +48,11 @@ let create tst : t =
 
 let reset self = self.fresh <- 0
 
-let fresh_term ?(opaque_to_cc = false) (self : t) ~pre (ty : ty) : Term.t =
+let fresh_term (self : t) ~pre (ty : ty) : Term.t =
   let id = self.fresh in
   self.fresh <- 1 + self.fresh;
   let c =
     Term.const self.tst
-    @@ Const.make
+    @@ Const.make (Fresh { id; gensym_id = self.self_id; pre; ty }) ops ~ty
-         (Fresh { id; gensym_id = self.self_id; pre; ty; opaque_to_cc })
-         ops ~ty
   in
   c

src/core/gensym.mli

@@ -15,7 +15,7 @@ type t
 val create : Term.store -> t
 (** New (stateful) generator instance. *)
 
-val fresh_term : ?opaque_to_cc:bool -> t -> pre:string -> ty -> term
+val fresh_term : t -> pre:string -> ty -> term
 (** Make a fresh term of the given type *)
 
 val reset : t -> unit

src/core/t_tracer.ml

@@ -3,34 +3,53 @@ module Tr = Sidekick_trace
 module T = Term
 
 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_const of { c: Const.view; c_ops: Const.Ops.t; 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 }
+  (* FIXME: remove when we decode *)
+  [@@ocaml.warning "-38"]
 
 (* 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 =
+let emit (self : t) (t : T.t) : term_ref =
   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 loop' t = V.int (loop t :> int) in
       let tag, v =
         match T.view t with
-        | T.E_var v ->
+        | T.E_var v -> "TV", V.(list [ string (Var.name v); loop' v.v_ty ])
-          let ty = loop (Var.ty v) in
+        | T.E_bound_var v -> "Tv", V.(list [ int (Bvar.idx v); loop' v.bv_ty ])
-          "TV", V.(list [ string (Var.name v); int (ty :> int) ])
+        | T.E_app (f, a) -> "T@", V.(list [ loop' f; loop' a ])
-        | _ -> assert false
+        | T.E_type i -> "Ty", V.int i
+        | T.E_const ({ Const.c_ty; _ } as const) ->
+          let tag, view = Const.ser ~ser_t:loop' const in
+          ( "Tc",
+            let fields =
+              (if V.is_null view then
+                []
+              else
+                [ "v", view ])
+              @ [ "ty", loop' c_ty; "tag", V.string tag ]
+            in
+            V.dict_of_list fields )
+        | T.E_app_fold { f; args; acc0 } ->
+          "Tf@", V.(list [ loop' f; list (List.map loop' args); loop' acc0 ])
+        | T.E_lam (name, ty, bod) ->
+          "Tl", V.(list [ string name; loop' ty; loop' bod ])
+        | T.E_pi (name, ty, bod) ->
+          "Tp", V.(list [ string name; loop' ty; loop' bod ])
       in
 
       let id = Tr.Sink.emit self.sink ~tag v in
@@ -38,3 +57,5 @@ let emit (self : t) (t : T.t) : Tr.Entry_id.t =
       id
   in
   loop t
+
+let emit' self t : unit = ignore (emit self t : term_ref)

src/core/t_tracer.mli

@@ -16,11 +16,18 @@ type Tr.entry_view +=
   | 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_const of { c: Const.view; c_ops: Const.Ops.t; 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 }
+  (* FIXME: remove *)
+  [@@ocaml.warning "-38"]
 
 type t
 
 val create : sink:Tr.Sink.t -> unit -> t
 val emit : t -> Term.t -> term_ref
+val emit' : t -> Term.t -> unit
+
+(* TODO
+   val reader : Term.store -> Tr.Entry_read.reader
+*)

src/main/pure_sat_solver.ml

@@ -4,187 +4,45 @@ open Sidekick_core
 module E = CCResult
 module SS = Sidekick_sat
 
-(* FIXME
-   (* TODO: on the fly compression *)
-   module Proof : sig
-     include module type of struct
-       include Proof_trace
-     end
-
-     type in_memory
-
-     val create_in_memory : unit -> t * in_memory
-     val to_string : in_memory -> string
-     val to_chan : out_channel -> in_memory -> unit
-     val create_to_file : string -> t
-     val close : t -> unit
-
-     type event = Sidekick_bin_lib.Drup_parser.event =
-       | Input of int list
-       | Add of int list
-       | Delete of int list
-
-     val iter_events : in_memory -> event Iter.t
-   end = struct
-     include Proof_trace
-     module PT = Proof_term
-
-     let bpf = Printf.bprintf
-     let fpf = Printf.fprintf
-
-     type lit = Lit.t
-     type in_memory = Buffer.t
-
-     let to_string = Buffer.contents
-
-     (*
-     type t =
-       | Dummy
-       | Inner of in_memory
-       | Out of { oc: out_channel; close: unit -> unit }
-       *)
-
-     let[@inline] emit_lits_buf_ buf lits = lits (fun i -> bpf buf "%d " i)
-     let[@inline] emit_lits_out_ oc lits = lits (fun i -> fpf oc "%d " i)
-
-     let create_in_memory () =
-       let buf = Buffer.create 1_024 in
-       let pr =
-         (module struct
-           let enabled () = true
-           let add_step s = assert false
-
-           (* TODO: helper to flatten?
-              let pt : PT.t = s () in
-               match pt.
-           *)
-
-           (* TODO *)
-           let add_unsat _ = ()
-
-           (* TODO *)
-           let delete _ = ()
-         end : DYN)
-       in
-       pr, buf
-
-     (*
-     module Rule = struct
-       type nonrec lit = lit
-       type nonrec rule = rule
-       type nonrec step_id = step_id
-
-       let sat_input_clause lits self =
-         match self with
-         | Dummy -> ()
-         | Inner buf ->
-           bpf buf "i ";
-           emit_lits_buf_ buf lits;
-           bpf buf "0\n"
-         | Out { oc; _ } ->
-           fpf oc "i ";
-           emit_lits_out_ oc lits;
-           fpf oc "0\n"
-
-       let sat_redundant_clause lits ~hyps:_ self =
-         match self with
-         | Dummy -> ()
-         | Inner buf ->
-           bpf buf "r ";
-           emit_lits_buf_ buf lits;
-           bpf buf "0\n"
-         | Out { oc; _ } ->
-           fpf oc "r ";
-           emit_lits_out_ oc lits;
-           fpf oc "0\n"
-
-       let sat_unsat_core _ _ = ()
-     end
-
-     let del_clause () lits self =
-       match self with
-       | Dummy -> ()
-       | Inner buf ->
-         bpf buf "d ";
-         emit_lits_buf_ buf lits;
-         bpf buf "0\n"
-       | Out { oc; _ } ->
-         fpf oc "d ";
-         emit_lits_out_ oc lits;
-         fpf oc "0\n"
-
-
-     let create_in_memory () : t * in_memory =
-       let buf = Buffer.create 1_024 in
-       Inner buf, buf
-
-     let create_to_file file =
-       let oc, close =
-         match Filename.extension file with
-         | ".gz" ->
-           let cmd = Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file) in
-           Log.debugf 1 (fun k -> k "proof file: command is %s" cmd);
-           let oc = Unix.open_process_out cmd in
-           oc, fun () -> ignore (Unix.close_process_out oc : Unix.process_status)
-         | ".drup" ->
-           let oc = open_out_bin file in
-           oc, fun () -> close_out_noerr oc
-         | s -> Error.errorf "unknown file extension '%s'" s
-       in
-       Out { oc; close }
-
-     let close = function
-       | Dummy | Inner _ -> ()
-       | Out { close; oc } ->
-         flush oc;
-         close ()
-
-     let to_string = Buffer.contents
-     let to_chan = Buffer.output_buffer
-
-     module DP = Sidekick_bin_lib.Drup_parser
-
-     type event = DP.event =
-       | Input of int list
-       | Add of int list
-       | Delete of int list
-
-     (* parse the proof back *)
-     let iter_events (self : in_memory) : DP.event Iter.t =
-       let dp = DP.create_string (to_string self) in
-       DP.iter dp
-
-       *)
-   end
-*)
-
 module I_const : sig
   val make : Term.store -> int -> Lit.t
 end = struct
   type Const.view += I of int
 
   let ops =
-    (module struct
+    let equal a b =
-      let equal a b =
+      match a, b with
-        match a, b with
+      | I a, I b -> a = b
-        | I a, I b -> a = b
+      | _ -> false
-        | _ -> false
+    in
 
-      let hash = function
+    let hash = function
-        | I i -> Hash.int i
+      | I i -> Hash.int i
-        | _ -> assert false
+      | _ -> assert false
+    in
 
-      let pp out = function
+    let pp out = function
-        | I i -> Fmt.int out i
+      | I i -> Fmt.int out i
-        | _ -> assert false
+      | _ -> assert false
+    in
 
-      (* irrelevant *)
+    let ser _sink = function
-      let opaque_to_cc _ = true
+      | I i -> "sat.lit", Ser_value.(int i)
-    end : Const.DYN_OPS)
+      | _ -> assert false
+    in
+    { Const.Ops.equal; hash; pp; ser }
 
   let make tst i : Lit.t =
     let t = Term.const tst @@ Const.make (I (abs i)) ops ~ty:(Term.bool tst) in
     Lit.atom ~sign:(i > 0) tst t
+
+  let deser _tst =
+    Ser_decode.(
+      ( "sat.lit",
+        [
+          (let+ i = int in
+           I i);
+        ] ))
 end
 
 module SAT = Sidekick_sat

src/trace/entry_id.ml

@@ -1,7 +1,8 @@
-type t = int
+(** Entry in the sink.
 
-let pp = Fmt.int
+   This integer tag represent a single entry in a trace, for example
+   a line if we serialized using line-separate json values.
+   In general each entry has its own unique ID that is monotonically
+   increasing with time. *)
 
-module Internal_ = struct
+include Int_id.Make ()
-  let make x = x
-end

src/trace/entry_id.mli

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

src/trace/sink.ml

@@ -4,12 +4,13 @@
     writes entries that are emitted into it.
 *)
 
+type tag = string
+
 module type S = sig
-  val emit : tag:string -> Ser_value.t -> Entry_id.t
+  val emit : tag:tag -> Ser_value.t -> Entry_id.t
 end
 
 type t = (module S)
-(** Trace sink *)
 
 let[@inline] emit (module Sink : S) ~tag (v : Ser_value.t) : Entry_id.t =
   Sink.emit v ~tag
@@ -17,14 +18,13 @@ let[@inline] emit (module Sink : S) ~tag (v : Ser_value.t) : Entry_id.t =
 let[@inline] emit' (self : t) ~tag v : unit =
   ignore (emit self ~tag v : Entry_id.t)
 
-(** 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 ~tag (v : Ser_value.t) =
       assert (Buffer.length buf = 0);
-      let id = Entry_id.Internal_.make !id_ in
+      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 ])

src/trace/sink.mli

@@ -1,18 +1,20 @@
-(** An IO sink for traces.
+(** An IO sink for serialization/tracing
 
     A trace is emitted on the fly into a sink. The sink collects or
     writes entries that are emitted into it.
 *)
 
+type tag = string
+
 module type S = sig
-  val emit : tag:string -> Ser_value.t -> Entry_id.t
+  val emit : tag:tag -> Ser_value.t -> Entry_id.t
 end
 
 type t = (module S)
 (** Trace sink *)
 
-val emit : t -> tag:string -> Ser_value.t -> Entry_id.t
+val emit : t -> tag:tag -> Ser_value.t -> Entry_id.t
-val emit' : t -> tag:string -> Ser_value.t -> unit
+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 *)

src/util/Sidekick_util.ml

@@ -25,5 +25,6 @@ module Profile = Profile
 module Chunk_stack = Chunk_stack
 module Ser_value = Ser_value
 module Ser_decode = Ser_decode
+module Ser_sink = Ser_sink
 
 let[@inline] ( let@ ) f x = f x

src/util/ser_decode.ml

@@ -30,6 +30,11 @@ let[@inline] fail_ msg v = raise_notrace (Fail (Error.mk msg v))
 let[@inline] fail_e e = raise_notrace (Fail e)
 let return x = { deser = (fun _ -> x) }
 let fail s = { deser = (fun v -> fail_ s v) }
+
+let unwrap_opt msg = function
+  | Some x -> return x
+  | None -> fail msg
+
 let any = { deser = (fun v -> v) }
 
 let bool =

src/util/ser_decode.mli

@@ -10,6 +10,8 @@ val bool : bool t
 val string : string t
 val return : 'a -> 'a t
 val fail : string -> 'a t
+val unwrap_opt : string -> 'a option -> 'a t
+(** Unwrap option, or fail *)
 val any : Ser_value.t t
 val list : 'a t -> 'a list t
 val dict_field : string -> 'a t -> 'a t

src/util/ser_value.ml

@@ -1,6 +1,7 @@
 module Fmt = CCFormat
 
 type t =
+  | Null
   | Bool of bool
   | Str of string
   | Bytes of string
@@ -8,6 +9,7 @@ type t =
   | List of t list
   | Dict of t Util.Str_map.t
 
+let null = Null
 let bool b : t = Bool b
 let int i : t = Int i
 let string x : t = Str x
@@ -16,8 +18,13 @@ let list x : t = List x
 let dict x : t = Dict x
 let dict_of_list l = dict (Util.Str_map.of_list l)
 
+let is_null = function
+  | Null -> true
+  | _ -> false
+
 let rec pp out (self : t) =
   match self with
+  | Null -> Fmt.string out "null"
   | Bool b -> Fmt.bool out b
   | Int i -> Fmt.int out i
   | Str s -> Fmt.Dump.string out s

src/util/ser_value.mli

@@ -7,6 +7,7 @@
 *)
 
 type t = private
+  | Null
   | Bool of bool
   | Str of string
   | Bytes of string
@@ -14,6 +15,7 @@ type t = private
   | List of t list
   | Dict of t Util.Str_map.t
 
+val null : t
 val bool : bool -> t
 val int : int -> t
 val string : string -> t
@@ -21,5 +23,6 @@ val bytes : string -> t
 val list : t list -> t
 val dict : t Util.Str_map.t -> t
 val dict_of_list : (string * t) list -> t
+val is_null : t -> bool
 
 include Sidekick_sigs.PRINT with type t := t

src/zarith/sidekick_zarith.ml

@@ -11,6 +11,8 @@ module Int : Sidekick_arith.INT_FULL with type t = Z.t = struct
     | 0 -> false
     | 1 | 2 -> true
     | _ -> assert false
+
+  let of_string s = try Some (of_string s) with _ -> None
 end
 
 module Rational :
@@ -43,4 +45,5 @@ module Rational :
       Z.(n + one)
 
   let pp_approx n out q = Format.fprintf out "%*.1f" n (Q.to_float q)
+  let of_string s = try Some (of_string s) with _ -> None
 end