From 4bc02a044fde4fb5c6f347e942202307a2dbdaaa Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 17 Nov 2009 12:44:14 -0500 Subject: Hooks for measuring how much interesting proving is going on in elaboration --- src/elab_ops.sml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'src/elab_ops.sml') 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