mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-11 05:28:34 -05:00
54 lines
1.6 KiB
OCaml
54 lines
1.6 KiB
OCaml
module Tr = Sidekick_trace
|
|
|
|
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
|
|
|
|
let dummy : t = new dummy
|
|
|
|
class concrete ~sink : t =
|
|
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 =
|
|
if enabled then Tr.Sink.emit' sink ~tag:"Pd" (Ser_value.int id)
|
|
|
|
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
|