feat: implement some const decoders

src/base/Data_ty.ml

@@ -105,7 +105,7 @@ let ops =
     | Is_a c -> Hash.combine2 595 (Cstor.hash c)
     | _ -> assert false
   in
-  let ser ser_t = function
+  let ser _ser_t = function
     | Data d -> assert false (* TODO *)
     | Cstor c -> assert false (* TODO *)
     | Select s -> assert false (* TODO *)
@@ -115,6 +115,8 @@ let ops =
 
   { Const.Ops.pp; hash; equal; ser }
 
+(* TODO: const decoders *)
+
 let data_as_ty (d : data) = Lazy.force d.data_as_ty
 
 let data tst d : Term.t =

src/base/Form.ml

@@ -49,6 +49,14 @@ let ops =
   in
   { 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));
+    ("=>", ops, Ser_decode.(fun _ -> return C_imply));
+  ]
+
 (* ### view *)
 
 let view (t : T.t) : T.t view =

src/base/Form.mli

@@ -36,6 +36,7 @@ val equiv : Term.store -> term -> term -> term
 val xor : Term.store -> term -> term -> term
 val ite : Term.store -> term -> term -> term -> term
 val distinct_l : Term.store -> term list -> term
+val const_decoders : Const.decoders
 
 (* *)
 

src/base/Ty.ml

@@ -49,6 +49,20 @@ let ops_ty =
   in
   { 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));
+    ( "ty.id",
+      ops_ty,
+      Ser_decode.(
+        fun _ ->
+          let+ id = dict_field "id" ID.deser
+          and+ finite = dict_field "fin" bool in
+          Ty (Ty_uninterpreted { id; finite })) );
+  ]
+
 open struct
   let mk_ty0 tst view =
     let ty = Term.type_ tst in

src/base/Ty.mli

@@ -9,6 +9,7 @@ type data = Types_.data
 
 include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
 
+val const_decoders : Const.decoders
 val bool : store -> t
 val real : store -> t
 val int : store -> t

src/base/Uconst.ml

@@ -36,6 +36,17 @@ let ops =
   in
   { Const.Ops.pp; equal; hash; ser }
 
+let const_decoders : Const.decoders =
+ fun _tst ->
+  [
+    ( "uc",
+      ops,
+      Ser_decode.(
+        fun dec_t ->
+          let+ uc_id = ID.deser and+ uc_ty = dec_t in
+          Uconst { uc_id; uc_ty }) );
+  ]
+
 let[@inline] make uc_id uc_ty : t = { uc_id; uc_ty }
 
 let uconst tst (self : t) : Term.t =

src/base/Uconst.mli

@@ -12,6 +12,8 @@ type Const.view += private Uconst of t
 
 include Sidekick_sigs.EQ_ORD_HASH_PRINT with type t := t
 
+val const_decoders : Const.decoders
+
 val make : ID.t -> ty -> t
 (** Make a new uninterpreted function. *)
 

src/core-logic/const.ml

@@ -25,3 +25,7 @@ let[@inline] hash (a : t) : int =
 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 }
+
+type decoders =
+  Term.store ->
+  (string * Ops.t * (Term.t Ser_decode.t -> view Ser_decode.t)) list

src/core-logic/const.mli

@@ -24,4 +24,11 @@ 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
 
+type decoders =
+  Term.store ->
+  (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. *)
+
 include EQ_HASH_PRINT with type t := t

src/core-logic/str_const.ml

@@ -25,6 +25,15 @@ let ops =
   in
   { Const.Ops.pp; equal; hash; ser }
 
-(* TODO: deser *)
+let const_decoders : Const.decoders =
+ fun _tst ->
+  [
+    ( "c.str",
+      ops,
+      fun _dec_term ->
+        Ser_decode.(
+          let+ s = string in
+          Str s) );
+  ]
 
 let make name ~ty : Const.t = Const.make (Str name) ops ~ty

src/core-logic/str_const.mli

@@ -7,4 +7,5 @@ open Types_
 
 type const_view += private Str of string
 
+val const_decoders : Const.decoders
 val make : string -> ty:term -> const

src/core-logic/t_builtins.ml

@@ -48,14 +48,18 @@ let ops : const_ops =
   let ser _sink self = "builtin", Ser_value.(string (to_string self)) in
   { Const.Ops.equal; hash; pp; ser }
 
-(* TODO
+let const_decoders : Const.decoders =
-   let deser _tst =
+ fun _tst ->
-     Ser_decode.(
+  [
-       let* v = string in
+    ( "builtin",
-       match of_string v with
+      ops,
-       | Some c -> return c
+      Ser_decode.(
-       | None -> fail "expected builtin")
+        fun _dec_term ->
-*)
+          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

@@ -12,11 +12,7 @@ val c_ite : store -> t
 val true_ : store -> t
 val false_ : store -> t
 val bool_val : store -> bool -> t
-
+val const_decoders : Const.decoders
-(* 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/box.ml

@@ -25,6 +25,17 @@ let ops =
   in
   { Const.Ops.pp; equal; hash; ser }
 
+let const_decoders : Const.decoders =
+ fun _tst ->
+  [
+    ( "box",
+      ops,
+      Ser_decode.(
+        fun dec_t ->
+          let+ t = dec_t in
+          Box t) );
+  ]
+
 let as_box t =
   match Term.view t with
   | Term.E_const { Const.c_view = Box u; _ } -> Some u

src/core/box.mli

@@ -4,7 +4,8 @@ type Const.view += private Box of Term.t
 
 val box : Term.store -> Term.t -> Term.t
 (** [box tst t] makes a new constant that "boxes" [t].
-  This way it will be opaque. *)
+    This way it will be opaque. *)
 
+val const_decoders : Const.decoders
 val as_box : Term.t -> Term.t option
 val is_box : Term.t -> bool

src/core/gensym.ml

@@ -30,12 +30,23 @@ let ops =
   in
 
   let ser ser_t = function
-    | Fresh { id; pre; ty; _ } ->
+    | Fresh { id; pre; ty; gensym_id } ->
-      "gensym", Ser_value.(list [ int id; string pre; ser_t ty ])
+      "gensym", Ser_value.(list [ int id; int gensym_id; string pre; ser_t ty ])
     | _ -> assert false
   in
   { Const.Ops.equal; hash; pp; ser }
 
+let const_decoders : Const.decoders =
+ fun _tst ->
+  [
+    ( "gensym",
+      ops,
+      Ser_decode.(
+        fun dec_t ->
+          let+ id, gensym_id, pre, ty = tup4 int int string dec_t in
+          Fresh { id; gensym_id; pre; ty }) );
+  ]
+
 type t = { tst: Term.store; self_id: int; mutable fresh: int }
 
 (* TODO: use atomic *)

src/core/gensym.mli

@@ -15,6 +15,8 @@ type t
 val create : Term.store -> t
 (** New (stateful) generator instance. *)
 
+val const_decoders : Const.decoders
+
 val fresh_term : t -> pre:string -> ty -> term
 (** Make a fresh term of the given type *)
 

src/core/t_trace_read.ml

@@ -4,25 +4,38 @@ module ID_cache = LRU.Make (Tr.Entry_id)
 module Dec = Ser_decode
 
 type term_ref = Tr.entry_id
+type const_decoders = Const.decoders
 
 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;
+  mutable const_decode:
+    (Const.Ops.t * (Term.t Dec.t -> Const.view Dec.t)) Util.Str_map.t;
       (** tag -> const decoder *)
 }
 
-(* TODO: list of toplevel registrations for constant decoders,
+let add_const_decoders (self : t) decs : unit =
-   as [tst -> (tag*dec)list] *)
+  let decs = decs self.tst in
+  List.iter
+    (fun (tag, ops, dec) ->
+      (* check that there is no tag collision *)
+      if Util.Str_map.mem tag self.const_decode then
+        Error.errorf "Trace_reader: two distinct const decoders for tag %S" tag;
+      self.const_decode <- Util.Str_map.add tag (ops, dec) self.const_decode)
+    decs
 
-let create ~source tst : t =
+let create ?(const_decoders = []) ~source tst : t =
-  {
+  let self =
-    src = source;
+    {
-    tst;
+      src = source;
-    cache = ID_cache.create ~size:1024 ();
+      tst;
-    const_decode = Util.Str_map.empty;
+      cache = ID_cache.create ~size:1024 ();
-  }
+      const_decode = Util.Str_map.empty;
+    }
+  in
+  List.iter (add_const_decoders self) const_decoders;
+  self
 
 let decode_term (self : t) ~read_subterm ~tag : Term.t Dec.t =
   match tag with
@@ -52,14 +65,17 @@ let decode_term (self : t) ~read_subterm ~tag : Term.t Dec.t =
       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 = dict_field_opt "v" any
+      and* ty = dict_field "ty" read_subterm
+      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 ->
+      | Some (ops, c_dec) ->
-        let+ c = reflect_or_fail (c_dec read_subterm) view in
+        let+ c_view = reflect_or_fail (c_dec read_subterm) view in
-        Term.const self.tst c))
+        let const = Const.make c_view ops ~ty in
+        Term.const self.tst const))
   | "Tf@" -> assert false (* TODO *)
   | _ -> Dec.failf "unknown tag %S for a term" tag
 

src/core/t_trace_read.mli

@@ -1,8 +1,13 @@
 open Sidekick_core_logic
 module Tr = Sidekick_trace
+module Dec = Ser_decode
 
 type term_ref = Tr.entry_id
+type const_decoders = Const.decoders
 type t
 
-val create : source:Tr.Source.t -> Term.store -> t
+val create :
+  ?const_decoders:const_decoders list -> source:Tr.Source.t -> Term.store -> t
+
+val add_const_decoders : t -> const_decoders -> unit
 val read_term : t -> term_ref -> (Term.t, string) result

src/core/t_tracer.ml

@@ -33,7 +33,7 @@ let emit (self : t) (t : T.t) : term_ref =
         | T.E_bound_var v -> "Tv", V.(list [ int (Bvar.idx v); loop' v.bv_ty ])
         | T.E_app (f, a) -> "T@", V.(list [ loop' f; loop' a ])
         | T.E_type i -> "Ty", V.int i
-        | T.E_const const ->
+        | T.E_const ({ Const.c_ty; _ } as const) ->
           let tag, view = Const.ser ~ser_t:loop' const in
           ( "Tc",
             let fields =
@@ -41,7 +41,7 @@ let emit (self : t) (t : T.t) : term_ref =
                 []
               else
                 [ "v", view ])
-              @ [ "tag", V.string tag ]
+              @ [ "ty", loop' c_ty; "tag", V.string tag ]
             in
             V.dict_of_list fields )
         | T.E_app_fold { f; args; acc0 } ->

src/main/pure_sat_solver.ml

@@ -6,6 +6,7 @@ module SS = Sidekick_sat
 
 module I_const : sig
   val make : Term.store -> int -> Lit.t
+  val const_decoders : Const.decoders
 end = struct
   type Const.view += I of int
 
@@ -32,6 +33,17 @@ end = struct
     in
     { Const.Ops.equal; hash; pp; ser }
 
+  let const_decoders : Const.decoders =
+   fun _tst ->
+    [
+      ( "sat.lit",
+        ops,
+        Ser_decode.(
+          fun _tst ->
+            let+ i = int in
+            I i) );
+    ]
+
   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