(fix) Proper CTO file for the monitor output and cleanup

Signed-off-by: Jerome Simeon <[email protected]>

extraction/src/Monitor.atd

@@ -14,19 +14,21 @@
 
 <doc text="Ergo monitor data structure.
 
-   Based on the documentation available at:
-   XXXX
+   Provdes processing time information for various compilation phases
 
 ">
 
 type phase = {
+    class <json name="$class"> : string;
     name : string;
-    cputime : float;
+    single : float;
     cummulative : float;
+    total : float;
     subphases : phase list;
-  } <ocaml field_prefix="ergo_monitor_">
+  } <ocaml field_prefix="monitor_phase_">
 
 type monitor = {
+    class <json name="$class"> : string;
     phases : phase list;
-} <ocaml field_prefix="ergo_monitor_">
+} <ocaml field_prefix="monitor_">
 

extraction/src/Util.ml

@@ -245,6 +245,7 @@ let class_prefix_of_filename filename =
 (* monitor contains a mapping from compilation phase to (f1,f2) where f1 is the new time entering the phase and f2 is the total time in that phase *)
 let monitor : (string, float * float) Hashtbl.t = Hashtbl.create 37
 let monitoring = ref false
+let monitoring_start = Sys.time ()
 let monitor_output : (Monitor_j.phase list) Stack.t =
   let s = Stack.create () in
   Stack.push [] s;
@@ -264,23 +265,32 @@ let exit_monitor monitor output phase =
   begin try
     let (f1,f2) = Hashtbl.find monitor phase in
     let picktime : float = Sys.time () in
-    let cputime : float = picktime -. f1 in
-    let cummtime : float = picktime -. f1 +. f2 in
-    Hashtbl.replace monitor phase (0.0, cummtime);
+    let single : float = picktime -. f1 in
+    let cummul : float = picktime -. f1 +. f2 in
+    let total : float = picktime -. monitoring_start in
+    Hashtbl.replace monitor phase (0.0, cummul);
     Stack.push (prevprev @ [{
-      ergo_monitor_name = phase;
-      ergo_monitor_cputime = cputime;
-      ergo_monitor_cummulative = cummtime;
-      ergo_monitor_subphases =prev
+      monitor_phase_class = "org.accordproject.ergo.monitor.Phase";
+      monitor_phase_name = phase;
+      monitor_phase_single = single;
+      monitor_phase_cummulative = cummul;
+      monitor_phase_total = total;
+      monitor_phase_subphases =prev
     }]) output
   with _ ->
     begin
+      let picktime : float = Sys.time () in
+      let single : float = 0.0 in
+      let cummul : float = 0.0 in
+      let total : float = picktime -. monitoring_start in
       Hashtbl.add monitor phase (0.0, 0.0); (* Should never happen *)
       Stack.push (prevprev @ [{
-        ergo_monitor_name = phase;
-        ergo_monitor_cputime = 0.0;
-        ergo_monitor_cummulative = 0.0;
-        ergo_monitor_subphases = prev
+        monitor_phase_class = "org.accordproject.ergo.monitor.Phase";
+        monitor_phase_name = phase;
+        monitor_phase_single = single;
+        monitor_phase_cummulative = cummul;
+        monitor_phase_total = total;
+        monitor_phase_subphases = prev
       }]) output
     end
   end
@@ -299,5 +309,8 @@ let coq_time phase f x =
     f x
 
 let get_monitor_output () =
-  string_of_monitor { ergo_monitor_phases = Stack.top monitor_output }
+  string_of_monitor {
+    monitor_class = "org.accordproject.ergo.monitor.Monitor";
+    monitor_phases = Stack.top monitor_output
+  }
 

extraction/stdlib/monitor.cto

@@ -0,0 +1,34 @@
+/*
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+namespace org.accordproject.ergo.monitor
+
+/**
+ * Describes a phase
+ */
+concept Phase {
+  o String name
+  o Double single
+  o Double cummulative
+  o Double total
+  o Phase[] subphases
+}
+
+/**
+ * Monitor
+ */
+concept Monitor {
+  o Phase[] phases
+}
+