From 4bc02a044fde4fb5c6f347e942202307a2dbdaaa Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 17 Nov 2009 12:44:14 -0500
Subject: Hooks for measuring how much interesting proving is going on in
 elaboration

---
 demo/batchFun.urp |  2 ++
 demo/crud.urp     |  2 ++
 src/disjoint.sig  |  3 +++
 src/disjoint.sml  |  5 +++++
 src/elab_ops.sig  |  5 +++++
 src/elab_ops.sml  | 14 +++++++++++++-
 6 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 demo/batchFun.urp
 create mode 100644 demo/crud.urp

diff --git a/demo/batchFun.urp b/demo/batchFun.urp
new file mode 100644
index 00000000..48f4d27a
--- /dev/null
+++ b/demo/batchFun.urp
@@ -0,0 +1,2 @@
+
+batchFun
diff --git a/demo/crud.urp b/demo/crud.urp
new file mode 100644
index 00000000..223bc7af
--- /dev/null
+++ b/demo/crud.urp
@@ -0,0 +1,2 @@
+
+crud
diff --git a/src/disjoint.sig b/src/disjoint.sig
index 0d386d1a..7ca05fd9 100644
--- a/src/disjoint.sig
+++ b/src/disjoint.sig
@@ -40,4 +40,7 @@ signature DISJOINT = sig
 
     val p_env : env -> unit
 
+    val proved : int ref
+    val reset : unit -> unit
+
 end
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 5cc9d1fb..8fa8834c 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -161,6 +161,10 @@ fun prove1 denv (p1, p2) =
             NONE => false
           | SOME pset => PS.member (pset, p2)
 
+val proved = ref 0
+fun reset () = (ElabOps.reset ();
+                proved := 0)
+
 fun decomposeRow env c =
     let
         val loc = #2 c
@@ -248,6 +252,7 @@ and assert env denv (c1, c2) =
 
 and prove env denv (c1, c2, loc) =
     let
+        val () = proved := !proved + 1
         val ps1 = decomposeRow env c1
         val ps2 = decomposeRow env c2
 
diff --git a/src/elab_ops.sig b/src/elab_ops.sig
index 7088bf06..adf69696 100644
--- a/src/elab_ops.sig
+++ b/src/elab_ops.sig
@@ -39,4 +39,9 @@ signature ELAB_OPS = sig
 
     val hnormCon : ElabEnv.env -> Elab.con -> Elab.con
 
+    val identity : int ref
+    val distribute : int ref
+    val fuse : int ref
+    val reset : unit -> unit
+
 end
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index f005ab04..6465668f 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -143,6 +143,13 @@ val occurs =
                                | _ => n}
                   0
 
+val identity = ref 0
+val distribute = ref 0
+val fuse = ref 0
+
+fun reset () = (identity := 0;
+                distribute := 0;
+                fuse := 0)
 
 fun hnormCon env (cAll as (c, loc)) =
     case c of
@@ -219,6 +226,8 @@ fun hnormCon env (cAll as (c, loc)) =
                                       (TDisjoint (_, _, c), _) => unconstraint c
                                     | c => c
 
+                              fun inc r = r := !r + 1
+
                               fun tryDistributivity () =
                                   case hnormCon env c2 of
                                       (CConcat (c1, c2'), _) =>
@@ -230,6 +239,7 @@ fun hnormCon env (cAll as (c, loc)) =
                                           val c2 = (CApp (c, c2'), loc)
                                           val c = (CConcat (c1, c2), loc)
                                       in
+                                          inc distribute;
                                           hnormCon env c
                                       end
                                     | _ => default ()
@@ -253,6 +263,7 @@ fun hnormCon env (cAll as (c, loc)) =
                                                     val c = (CApp (c, f'), loc)
                                                     val c = (CApp (c, r'), loc)
                                                 in
+                                                    inc fuse;
                                                     hnormCon env c
                                                 end
                                               | _ => tryDistributivity ())
@@ -275,7 +286,8 @@ fun hnormCon env (cAll as (c, loc)) =
                                       case unconstraint c of
                                           (CUnif (_, _, _, vR'), _) =>
                                           if vR' = vR then
-                                              hnormCon env c2
+                                              (inc identity;
+                                               hnormCon env c2)
                                           else
                                               tryFusion ()
                                         | _ => tryFusion ()
-- 
cgit v1.2.3