added combi in simp util

zxcalc · Dec 5, 2014 · e6ab4aa · e6ab4aa
1 parent 9e294e6
commit e6ab4aa
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/core/rewriting/simp_util.ML b/core/rewriting/simp_util.ML
@@ -13,6 +13,9 @@ sig
                     -> (R.name * Theory.Rule.T)
                     -> simproc
 
+  val REDUCE_WHILE : (Theory.Graph.T -> bool)
+                     -> (R.name * Theory.Rule.T)
+                     -> simproc
   val REDUCE_METRIC : (Theory.Graph.T -> int)
                       -> (R.name * Theory.Rule.T)
                       -> simproc
@@ -101,6 +104,8 @@ fun REDUCE_METRIC_TO i metric =
 
 val REDUCE_METRIC = REDUCE_METRIC_TO 0
 
+fun REDUCE_WHILE b = REDUCE_WITH { PRE = b, POST = K true }
+
 (*fun REDUCE_METRIC_TO i metric rule graph =
   Seq.make (fn () => (
     let