simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

minor change in term tracer

Browse source
This commit is contained in:
Simon Cruanes 2022-09-25 21:27:42 -04:00
parent 27b0374c62
commit ca3262eac3
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/t_tracer.ml
View file

@ -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_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_app (f, a) -> "T@", V.(list [ loop' f; loop' a ])
| T.E_type i -> "Ty", V.int i | 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 let tag, view = Const.ser ~ser_t:loop' const in
( "Tc", ( "Tc",
let fields = let fields =
@ -41,7 +41,7 @@ let emit (self : t) (t : T.t) : term_ref =
[] []
else else
[ "v", view ]) [ "v", view ])
@ [ "ty", loop' c_ty; "tag", V.string tag ] @ [ "tag", V.string tag ]
in in
V.dict_of_list fields ) V.dict_of_list fields )
| T.E_app_fold { f; args; acc0 } -> | T.E_app_fold { f; args; acc0 } ->

5
src/core/t_tracer.mli
View file

@ -8,7 +8,7 @@
open Sidekick_core_logic open Sidekick_core_logic
module Tr = Sidekick_trace module Tr = Sidekick_trace
type term_ref = private Tr.entry_id type term_ref = Tr.entry_id
type Tr.entry_view += type Tr.entry_view +=
private private
@ -25,6 +25,9 @@ type Tr.entry_view +=
type t type t
val create : sink:Tr.Sink.t -> unit -> 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 -> term_ref
val emit' : t -> Term.t -> unit val emit' : t -> Term.t -> unit