From 48ebeb37fb39bcc59574d9baceea9d5726d951fa Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 12 Oct 2022 22:19:13 -0400 Subject: [PATCH] refactor(proof): serialize pterms; tracer inherits term tracer --- src/proof/pterm.ml | 50 ++++++++++++++++++++++++++++++++++++++++++-- src/proof/pterm.mli | 8 +++++-- src/proof/step.ml | 2 ++ src/proof/tracer.ml | 29 ++++++++++++++++++++----- src/proof/tracer.mli | 8 +++++++ 5 files changed, 88 insertions(+), 9 deletions(-) diff --git a/src/proof/pterm.ml b/src/proof/pterm.ml index f2fd065c..9409f0d4 100644 --- a/src/proof/pterm.ml +++ b/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 ]) diff --git a/src/proof/pterm.mli b/src/proof/pterm.mli index aa31c333..11b71154 100644 --- a/src/proof/pterm.mli +++ b/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 *) diff --git a/src/proof/step.ml b/src/proof/step.ml index 86b7c8b8..d4c201e8 100644 --- a/src/proof/step.ml +++ b/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 diff --git a/src/proof/tracer.ml b/src/proof/tracer.ml index 875a8b43..2b0458a6 100644 --- a/src/proof/tracer.ml +++ b/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 diff --git a/src/proof/tracer.mli b/src/proof/tracer.mli index 9bf5858c..2bbefbbc 100644 --- a/src/proof/tracer.mli +++ b/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. *)