From ca3262eac3033d26c745256ba826fd0ae619f3b8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 25 Sep 2022 21:27:42 -0400 Subject: [PATCH] minor change in term tracer --- src/core/t_tracer.ml | 4 ++-- src/core/t_tracer.mli | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/core/t_tracer.ml b/src/core/t_tracer.ml index 2c73150a..489c1641 100644 --- a/src/core/t_tracer.ml +++ b/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.c_ty; _ } as const) -> + | T.E_const 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 ]) - @ [ "ty", loop' c_ty; "tag", V.string tag ] + @ [ "tag", V.string tag ] in V.dict_of_list fields ) | T.E_app_fold { f; args; acc0 } -> diff --git a/src/core/t_tracer.mli b/src/core/t_tracer.mli index b89e524c..394eea0e 100644 --- a/src/core/t_tracer.mli +++ b/src/core/t_tracer.mli @@ -8,7 +8,7 @@ open Sidekick_core_logic module Tr = Sidekick_trace -type term_ref = private Tr.entry_id +type term_ref = Tr.entry_id type Tr.entry_view += private @@ -25,6 +25,9 @@ type Tr.entry_view += type t val create : sink:Tr.Sink.t -> unit -> t +(** [create ~sink ()] makes a tracer that will write terms + into the given sink. *) + val emit : t -> Term.t -> term_ref val emit' : t -> Term.t -> unit