refactor(proof): serialize pterms; tracer inherits term tracer

src/proof/pterm.ml

@@ -1,5 +1,3 @@
-open Sidekick_core_logic
-
 type step_id = Step.id
 type lit = Lit.t
 type local_ref = Step.id
@@ -34,6 +32,7 @@ let rec pp out = function
 let local_ref id = P_local id
 let ref id = P_ref id
 let[@inline] delay f = f
+let dummy = ref Step.dummy
 
 let let_ bs r =
   match bs with
@@ -51,3 +50,50 @@ let apply_rule ?(lits = []) ?(terms = []) ?(substs = []) ?(premises = [])
       premises;
       indices;
     }
+
+module V = Ser_value
+
+let ser_apply_rule (tracer : Term.Tracer.t) (r : rule_apply) : Ser_value.t =
+  let { rule_name; lit_args; subst_args; term_args; premises; indices } = r in
+
+  let enc_lit (lit : Lit.t) : V.t =
+    let sign = Lit.sign lit in
+    let id_t = Term.Tracer.emit tracer @@ Lit.term lit in
+    V.(list [ bool sign; int id_t ])
+  in
+
+  let enc_t t = V.int (Term.Tracer.emit tracer t) in
+  let enc_premise (p : step_id) = V.int p in
+  let enc_indice (p : step_id) = V.int p in
+  let enc_subst (_s : Subst.t) : V.t = assert false (* TODO *) in
+
+  (* add a field [x, v] if [v] is not the empty list *)
+  let add_ x v enc_v l =
+    match v with
+    | [] -> l
+    | _ ->
+      let v = V.list (List.map enc_v v) in
+      (x, v) :: l
+  in
+
+  let l =
+    [ "name", V.string rule_name ]
+    |> add_ "lits" lit_args enc_lit
+    |> add_ "su" subst_args enc_subst
+    |> add_ "t" term_args enc_t
+    |> add_ "ps" premises enc_premise
+    |> add_ "idx" indices enc_indice
+  in
+
+  V.dict_of_list l
+
+let rec to_ser (tracer : Term.Tracer.t) t : Ser_value.t =
+  let recurse = to_ser tracer in
+  V.(
+    match t with
+    | P_ref r -> list [ int 0; int r ]
+    | P_local id -> list [ int 1; int id ]
+    | P_apply r -> list [ int 2; ser_apply_rule tracer r ]
+    | P_let (bs, bod) ->
+      let ser_b (x, t) = list [ int x; recurse t ] in
+      list [ int 3; list (List.map ser_b bs); recurse bod ])

src/proof/pterm.mli

@@ -2,8 +2,6 @@
 
   A proof term is the description of a reasoning step, that yields a clause. *)
 
-open Sidekick_core_logic
-
 type step_id = Step.id
 type lit = Lit.t
 
@@ -36,6 +34,9 @@ val local_ref : local_ref -> t
 val let_ : (local_ref * t) list -> t -> t
 val delay : (unit -> t) -> delayed
 
+val dummy : t
+(** Reference to the dummy step *)
+
 val apply_rule :
   ?lits:lit list ->
   ?terms:Term.t list ->
@@ -44,3 +45,6 @@ val apply_rule :
   ?indices:int list ->
   string ->
   t
+
+val to_ser : Term.Tracer.t -> t -> Ser_value.t
+(** Serialize *)

src/proof/step.ml

@@ -1,3 +1,5 @@
 type id = Sidekick_trace.Entry_id.t
 
+let equal (a : id) (b : id) = a = b
+let dummy : id = Sidekick_trace.Entry_id.dummy
 let pp : id Fmt.printer = Fmt.int

src/proof/tracer.ml

@@ -4,19 +4,24 @@ type step_id = Step.id
 
 class type t =
   object
+    inherit Term.Tracer.t
     method proof_enabled : bool
+    method proof_enable : bool -> unit
     method emit_proof_step : Pterm.delayed -> step_id
     method emit_proof_delete : step_id -> unit
   end
 
 let[@inline] enabled (self : #t) : bool = self#proof_enabled
+let[@inline] enable (self : #t) (b : bool) : unit = self#proof_enable b
 let[@inline] add_step (self : #t) rule : step_id = self#emit_proof_step rule
 let[@inline] delete (self : #t) s : unit = self#emit_proof_delete s
 let dummy_step_id : step_id = Sidekick_trace.Entry_id.dummy
 
 class dummy : t =
   object
+    inherit Term.Tracer.dummy
     method proof_enabled = false
+    method proof_enable _ = ()
     method emit_proof_step _ = dummy_step_id
     method emit_proof_delete _ = ()
   end
@@ -24,12 +29,26 @@ class dummy : t =
 let dummy : t = new dummy
 
 class concrete ~sink : t =
-  object
-    method proof_enabled = true
+  object (self)
+    val mutable enabled = true
+    inherit Term.Tracer.concrete ~sink
+    method proof_enabled = enabled
+    method proof_enable b = enabled <- b
 
     method emit_proof_delete id : unit =
-      Tr.Sink.emit' sink ~tag:"Pd" (Ser_value.int id)
+      if enabled then Tr.Sink.emit' sink ~tag:"Pd" (Ser_value.int id)
 
-    method emit_proof_step (p : Pterm.delayed) : step_id = assert false
-    (* TODO *)
+    method emit_proof_step (p : Pterm.delayed) : step_id =
+      if enabled then (
+        let pt = p () in
+        match pt with
+        | Pterm.P_ref step when Step.equal step Step.dummy ->
+          (* special shortcut: [Ref dummy] is not emitted,
+             but just returns [dummy] *)
+          Step.dummy
+        | _ ->
+          let v = Pterm.to_ser (self :> Term.Tracer.t) pt in
+          Tr.Sink.emit sink ~tag:"Pt" v
+      ) else
+        Step.dummy
   end

src/proof/tracer.mli

@@ -20,9 +20,14 @@ type step_id = Step.id
 *)
 class type t =
   object
+    inherit Term.Tracer.t
+
     method proof_enabled : bool
     (** If proof tracing enabled? *)
 
+    method proof_enable : bool -> unit
+    (** Enable/disable proof tracing, if supported *)
+
     method emit_proof_step : Pterm.delayed -> step_id
     (** Create a new step in the trace. *)
 
@@ -34,6 +39,9 @@ class type t =
 val enabled : #t -> bool
 (** Is proof tracing enabled? *)
 
+val enable : #t -> bool -> unit
+(** Enable proof tracing *)
+
 val add_step : #t -> Pterm.delayed -> step_id
 (** Create a new step in the trace. *)