more static analysis on the Automath text

[helm.git] / helm / software / lambda-delta / automath / autOutput.ml

diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml
index ffbdfdb2096eeac175e3e86ee1af854c60fe100a..2f1a4d91c4715ab67b739c40f6b5e1348a734c48 100644 (file)
--- a/helm/software/lambda-delta/automath/autOutput.ml
+++ b/helm/software/lambda-delta/automath/autOutput.ml
@@ -12,6 +12,7 @@
 module P = Printf
 module L = Log
 module A = Aut
+module R = AutProcess
 
 type counters = {
    sections: int;
@@ -85,3 +86,14 @@ let print_counters f c =
    L.warn (P.sprintf "    Global Int. Complexity:   unknown");
    L.warn (P.sprintf "      + Abbreviation nodes:   %7u" c.xnodes);
    f ()
+
+let print_process_counters f c =
+   let f iao iar iac iag =
+      L.warn (P.sprintf "  Automath process summary");
+      L.warn (P.sprintf "    Implicit after opening:   %7u" iao);
+      L.warn (P.sprintf "    Implicit after reopening: %7u" iar);
+      L.warn (P.sprintf "    Implicit after closing:   %7u" iac);
+      L.warn (P.sprintf "    Implicit after global:    %7u" iag);
+      f ()
+   in
+   R.get_counters f c