diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-11-17 12:44:14 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-11-17 12:44:14 -0500 |
| commit | 4bc02a044fde4fb5c6f347e942202307a2dbdaaa (patch) | |
| tree | 9e63f1f3850a9309718b5c95fde780c56c801325 | |
| parent | 1eaec00255adfefbfdf4c25a77f03a107cd96fbd (diff) | |
Hooks for measuring how much interesting proving is going on in elaboration
| -rw-r--r-- | demo/batchFun.urp | 2 | ||||
| -rw-r--r-- | demo/crud.urp | 2 | ||||
| -rw-r--r-- | src/disjoint.sig | 3 | ||||
| -rw-r--r-- | src/disjoint.sml | 5 | ||||
| -rw-r--r-- | src/elab_ops.sig | 5 | ||||
| -rw-r--r-- | src/elab_ops.sml | 14 |
6 files changed, 30 insertions, 1 deletions
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 () |