# HG changeset patch
# User wenzelm
# Date 1187385050 -7200
# Node ID 3880d21d6013ac69d4cc004b469625221ac4aafd
# Parent  09b35593d0912c3b44679bb2b1793bde2ff2c5f4
added CRITICAL section markup;

diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/Clause.sml
--- a/src/Tools/Metis/src/Clause.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Clause.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -16,7 +16,8 @@
     let
       val r = ref 0
     in
-      fn () => case r of ref n => let val () = r := n + 1 in n end
+      fn () => CRITICAL (fn () =>
+        case r of ref n => let val () = r := n + 1 in n end)
     end;
 
 (* ------------------------------------------------------------------------- *)
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/Normalize.sml
--- a/src/Tools/Metis/src/Normalize.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Normalize.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -795,14 +795,14 @@
     let
       val counter : int NameMap.map ref = ref (NameMap.new ())
     in
-      fn n =>
+      fn n => CRITICAL (fn () =>
       let
         val ref m = counter
         val i = Option.getOpt (NameMap.peek m n, 0)
         val () = counter := NameMap.insert m (n, i + 1)
       in
         "skolem_" ^ n ^ (if i = 0 then "" else "_" ^ Int.toString i)
-      end
+      end)
     end;
 
 fun skolemize fv bv fm =
@@ -993,13 +993,13 @@
     let
       val counter : int ref = ref 0
     in
-      fn () =>
+      fn () => CRITICAL (fn () =>
       let
         val ref i = counter
         val () = counter := i + 1
       in
         "defCNF_" ^ Int.toString i
-      end
+      end)
     end;
 
 fun newDefinition def =
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/Portable.sig
--- a/src/Tools/Metis/src/Portable.sig	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Portable.sig	Fri Aug 17 23:10:50 2007 +0200
@@ -24,4 +24,10 @@
 
 val time : ('a -> 'b) -> 'a -> 'b
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL: (unit -> 'a) -> 'a
+
 end
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/PortableIsabelle.sml
--- a/src/Tools/Metis/src/PortableIsabelle.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableIsabelle.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -23,6 +23,12 @@
 
 val time = timeap;
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL = CRITICAL;
+
 end
 
 (* ------------------------------------------------------------------------- *)
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/PortableMlton.sml
--- a/src/Tools/Metis/src/PortableMlton.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -56,6 +56,12 @@
       y
     end;
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun CRITICAL e = e ();     (*dummy*)
+
 end
 
 (* ------------------------------------------------------------------------- *)
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/PortableMosml.sml
--- a/src/Tools/Metis/src/PortableMosml.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -26,6 +26,12 @@
 
 val time = Mosml.time;
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun CRITICAL e = e ();     (*dummy*)
+
 end
 
 (* ------------------------------------------------------------------------- *)
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/PortableSmlNJ.sml
--- a/src/Tools/Metis/src/PortableSmlNJ.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/PortableSmlNJ.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -52,6 +52,12 @@
     y
   end;
 
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+fun CRITICAL e = e ();     (*dummy*)
+
 end
 
 (* ------------------------------------------------------------------------- *)
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/Random.sml
--- a/src/Tools/Metis/src/Random.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Random.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -18,27 +18,29 @@
 
 fun newgen () = newgenseed (Time.toReal (Time.now ()));
 
-fun random {seedref as ref seed} = 
-    (seedref := nextrand seed; seed / m);
+fun random {seedref} = CRITICAL (fn () => 
+    (seedref := nextrand (! seedref); ! seedref / m));
 
-fun randomlist (n, {seedref as ref seed0}) = 
-    let fun h 0 seed res = (seedref := seed; res)
+fun randomlist (n, {seedref}) = CRITICAL (fn () =>
+    let val seed0 = ! seedref
+        fun h 0 seed res = (seedref := seed; res)
 	  | h i seed res = h (i-1) (nextrand seed) (seed / m :: res)
-    in h n seed0 [] end;
+    in h n seed0 [] end);
 
 fun range (min, max) = 
     if min > max then raise Fail "Random.range: empty range" 
     else 
-	fn {seedref as ref seed} =>
-	(seedref := nextrand seed; min + (floor(real(max-min) * seed / m)));
+	fn {seedref} => CRITICAL (fn () =>
+	(seedref := nextrand (! seedref); min + (floor(real(max-min) * ! seedref / m))));
 
 fun rangelist (min, max) =
     if min > max then raise Fail "Random.rangelist: empty range" 
     else 
-	fn (n, {seedref as ref seed0}) => 
-	let fun h 0 seed res = (seedref := seed; res)
+	fn (n, {seedref}) => CRITICAL (fn () => 
+	let val seed0 = ! seedref
+            fun h 0 seed res = (seedref := seed; res)
 	      | h i seed res = h (i-1) (nextrand seed) 
 		               (min + floor(real(max-min) * seed / m) :: res)
-	in h n seed0 [] end
+	in h n seed0 [] end)
 
 end
diff -r 09b35593d091 -r 3880d21d6013 src/Tools/Metis/src/Useful.sml
--- a/src/Tools/Metis/src/Useful.sml	Fri Aug 17 23:10:49 2007 +0200
+++ b/src/Tools/Metis/src/Useful.sml	Fri Aug 17 23:10:50 2007 +0200
@@ -377,7 +377,7 @@
 
   val primesList = ref (calcPrimes 10);
 in
-  fun primes n =
+  fun primes n = CRITICAL (fn () =>
       if length (!primesList) <= n then List.take (!primesList,n)
       else
         let
@@ -385,9 +385,9 @@
           val () = primesList := l
         in
           l
-        end;
+        end);
 
-  fun primesUpTo n =
+  fun primesUpTo n = CRITICAL (fn () =>
       let
         fun f k [] =
             let
@@ -400,7 +400,7 @@
             if p <= n then f (k + 1) ps else List.take (!primesList, k)
       in
         f 0 (!primesList)
-      end;
+      end);
 end;
 
 (* ------------------------------------------------------------------------- *)
@@ -572,22 +572,22 @@
 local
   val generator = ref 0
 in
-  fun newInt () =
+  fun newInt () = CRITICAL (fn () =>
       let
         val n = !generator
         val () = generator := n + 1
       in
         n
-      end;
+      end);
 
   fun newInts 0 = []
-    | newInts k =
+    | newInts k = CRITICAL (fn () =>
       let
         val n = !generator
         val () = generator := n + k
       in
         interval n k
-      end;
+      end);
 end;
 
 local