# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1258479854 18000
# Node ID a779402841f65510a078ceccf11352e28bf0e2e4
# Parent  b734ff578ac74851f70669bd63c9ed71c1da5890
Hooks for measuring how much interesting proving is going on in elaboration

diff -r b734ff578ac7 -r a779402841f6 demo/batchFun.urp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/batchFun.urp	Tue Nov 17 12:44:14 2009 -0500
@@ -0,0 +1,2 @@
+
+batchFun
diff -r b734ff578ac7 -r a779402841f6 demo/crud.urp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/demo/crud.urp	Tue Nov 17 12:44:14 2009 -0500
@@ -0,0 +1,2 @@
+
+crud
diff -r b734ff578ac7 -r a779402841f6 src/disjoint.sig
--- a/src/disjoint.sig	Sun Nov 08 12:26:03 2009 -0500
+++ b/src/disjoint.sig	Tue Nov 17 12:44:14 2009 -0500
@@ -40,4 +40,7 @@
 
     val p_env : env -> unit
 
+    val proved : int ref
+    val reset : unit -> unit
+
 end
diff -r b734ff578ac7 -r a779402841f6 src/disjoint.sml
--- a/src/disjoint.sml	Sun Nov 08 12:26:03 2009 -0500
+++ b/src/disjoint.sml	Tue Nov 17 12:44:14 2009 -0500
@@ -161,6 +161,10 @@
             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 prove env denv (c1, c2, loc) =
     let
+        val () = proved := !proved + 1
         val ps1 = decomposeRow env c1
         val ps2 = decomposeRow env c2
 
diff -r b734ff578ac7 -r a779402841f6 src/elab_ops.sig
--- a/src/elab_ops.sig	Sun Nov 08 12:26:03 2009 -0500
+++ b/src/elab_ops.sig	Tue Nov 17 12:44:14 2009 -0500
@@ -39,4 +39,9 @@
 
     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 -r b734ff578ac7 -r a779402841f6 src/elab_ops.sml
--- a/src/elab_ops.sml	Sun Nov 08 12:26:03 2009 -0500
+++ b/src/elab_ops.sml	Tue Nov 17 12:44:14 2009 -0500
@@ -143,6 +143,13 @@
                                | _ => 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 @@
                                       (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 @@
                                           val c2 = (CApp (c, c2'), loc)
                                           val c = (CConcat (c1, c2), loc)
                                       in
+                                          inc distribute;
                                           hnormCon env c
                                       end
                                     | _ => default ()
@@ -253,6 +263,7 @@
                                                     val c = (CApp (c, f'), loc)
                                                     val c = (CApp (c, r'), loc)
                                                 in
+                                                    inc fuse;
                                                     hnormCon env c
                                                 end
                                               | _ => tryDistributivity ())
@@ -275,7 +286,8 @@
                                       case unconstraint c of
                                           (CUnif (_, _, _, vR'), _) =>
                                           if vR' = vR then
-                                              hnormCon env c2
+                                              (inc identity;
+                                               hnormCon env c2)
                                           else
                                               tryFusion ()
                                         | _ => tryFusion ()