summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--demo/batchFun.urp2
-rw-r--r--demo/crud.urp2
-rw-r--r--src/disjoint.sig3
-rw-r--r--src/disjoint.sml5
-rw-r--r--src/elab_ops.sig5
-rw-r--r--src/elab_ops.sml14
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 ()