--- a/src/Tools/Metis/src/Clause.sml Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sml Wed Sep 15 15:15:49 2010 +0200
@@ -16,7 +16,9 @@
let
val r = ref 0
in
- fn () => case r of ref n => let val () = r := n + 1 in n end
+ (* MODIFIED by Jasmin Blanchette *)
+ fn () => CRITICAL (fn () =>
+ case r of ref n => let val () = r := n + 1 in n end)
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Normalize.sml Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sml Wed Sep 15 15:15:49 2010 +0200
@@ -689,7 +689,8 @@
let
val counter : int StringMap.map ref = ref (StringMap.new ())
in
- fn n =>
+ (* MODIFIED by Jasmin Blanchette *)
+ fn n => CRITICAL (fn () =>
let
val ref m = counter
val s = Name.toString n
@@ -699,7 +700,7 @@
val s = skolemPrefix ^ "_" ^ s ^ i
in
Name.fromString s
- end
+ end)
end;
fun skolemize fv bv fm =
@@ -1243,13 +1244,14 @@
let
val counter : int ref = ref 0
in
- fn () =>
+ (* MODIFIED by Jasmin Blanchette *)
+ fn () => CRITICAL (fn () =>
let
val ref i = counter
val () = counter := i + 1
in
definitionPrefix ^ "_" ^ Int.toString i
- end
+ end)
end;
fun newDefinition def =
--- a/src/Tools/Metis/src/PortablePolyml.sml Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml Wed Sep 15 15:15:49 2010 +0200
@@ -56,6 +56,7 @@
y
end;
+
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Random.sig Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Random.sig Wed Sep 15 15:15:49 2010 +0200
@@ -8,6 +8,7 @@
signature Random =
sig
+ val CRITICAL: (unit -> 'a) -> 'a (* MODIFIED by Jasmin Blanchette *)
val nextWord : unit -> word
--- a/src/Tools/Metis/src/Random.sml Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Random.sml Wed Sep 15 15:15:49 2010 +0200
@@ -9,6 +9,9 @@
structure Random :> Random =
struct
+(* MODIFIED by Jasmin Blanchette *)
+fun CRITICAL e = NAMED_CRITICAL "metis" e;
+
(* random words: 0w0 <= result <= max_word *)
(*minimum length of unboxed words on all supported ML platforms*)
@@ -25,7 +28,8 @@
fun change r f = r := f (!r);
local val rand = (*Unsynchronized.*)ref 0w1
-in fun nextWord () = ((*Unsynchronized.*)change rand step; ! rand) end;
+(* MODIFIED by Jasmin Blanchette *)
+in fun nextWord () = CRITICAL (fn () => ((*Unsynchronized.*)change rand step; ! rand)) end;
(*NB: higher bits are more random than lower ones*)
fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;
--- a/src/Tools/Metis/src/Useful.sml Wed Sep 15 14:24:29 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml Wed Sep 15 15:15:49 2010 +0200
@@ -454,7 +454,8 @@
val primesList = ref [2];
in
- fun primes n =
+ (* MODIFIED by Jasmin Blanchette *)
+ fun primes n = CRITICAL (fn () =>
let
val ref ps = primesList
@@ -469,10 +470,11 @@
in
ps
end
- end;
+ end);
end;
-fun primesUpTo n =
+(* MODIFIED by Jasmin Blanchette *)
+fun primesUpTo n = CRITICAL (fn () =>
let
fun f k =
let
@@ -484,7 +486,7 @@
end
in
f 8
- end;
+ end);
(* ------------------------------------------------------------------------- *)
(* Strings. *)
@@ -702,22 +704,24 @@
local
val generator = ref 0
in
- fun newInt () =
+ (* MODIFIED by Jasmin Blanchette *)
+ fun newInt () = CRITICAL (fn () =>
let
val n = !generator
val () = generator := n + 1
in
n
- end;
+ end);
fun newInts 0 = []
- | newInts k =
+ (* MODIFIED by Jasmin Blanchette *)
+ | newInts k = CRITICAL (fn () =>
let
val n = !generator
val () = generator := n + k
in
interval n k
- end;
+ end);
end;
fun withRef (r,new) f x =