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 /src/elab_ops.sml | |
| parent | 1eaec00255adfefbfdf4c25a77f03a107cd96fbd (diff) | |
Hooks for measuring how much interesting proving is going on in elaboration
Diffstat (limited to 'src/elab_ops.sml')
| -rw-r--r-- | src/elab_ops.sml | 14 |
1 files changed, 13 insertions, 1 deletions
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 () |