Mercurial > urweb
changeset 1034:a779402841f6
Hooks for measuring how much interesting proving is going on in elaboration
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 17 Nov 2009 12:44:14 -0500 |
| parents | b734ff578ac7 |
| children | f87d0fedc54c |
| files | demo/batchFun.urp demo/crud.urp src/disjoint.sig src/disjoint.sml src/elab_ops.sig src/elab_ops.sml |
| diffstat | 6 files changed, 30 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- /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
--- /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
--- 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
--- 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
--- 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
--- 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 ()