diff --git a/lib/recorder.ml b/lib/recorder.ml new file mode 100644 index 0000000..d583917 --- /dev/null +++ b/lib/recorder.ml @@ -0,0 +1,22 @@ +open! Core +open Syntax +open Concrete_domains +(* open Interp_effects *) + +type event = + | Evt_update_st of (Path.t * Label.t * (value * Job_q.t)) + | Evt_set_dec of (Path.t * decision) + | Evt_enq_eff of (Path.t * clos) + | Evt_alloc_pt of Path.t + +(** TODO: *) +let record = function + | Evt_update_st (path, label, (v, q)) -> ignore (path, label, v, q) + | Evt_set_dec (path, dec) -> ignore (path, dec) + | Evt_enq_eff (path, clos) -> ignore (path, clos) + | Evt_alloc_pt path -> ignore path + +type diagnostics +(** TODO *) + +let diagnostics = ref (failwith "not implemented") diff --git a/lib/recorder.mli b/lib/recorder.mli new file mode 100644 index 0000000..763e940 --- /dev/null +++ b/lib/recorder.mli @@ -0,0 +1,15 @@ +open! Core +open Syntax +open Concrete_domains + +type event = + | Evt_update_st of (Path.t * Label.t * (value * Job_q.t)) + | Evt_set_dec of (Path.t * decision) + | Evt_enq_eff of (Path.t * clos) + | Evt_alloc_pt of Path.t + +val record : event -> unit + +type diagnostics + +val diagnostics : diagnostics ref