src/Tools/Metis/metis.ML

 (* ------------------------------------------------------------------------- *)
 (* Timing function applications                                              *)
 (* ------------------------------------------------------------------------- *)
 
 val time : ('a -> 'b) -> 'a -> 'b
+
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL: (unit -> 'a) -> 'a
 
 end
 
 (**** Original file: PortableIsabelle.sml ****)
 

 (* ------------------------------------------------------------------------- *)
 (* Timing function applications a la Mosml.time.                             *)
 (* ------------------------------------------------------------------------- *)
 
 val time = timeap;
+
+(* ------------------------------------------------------------------------- *)
+(* Critical section markup (multiprocessing)                                 *)
+(* ------------------------------------------------------------------------- *)
+
+val CRITICAL = CRITICAL;
 
 end
 
 (* ------------------------------------------------------------------------- *)
 (* Quotations a la Moscow ML.                                                *)

 fun newgenseed seed =
     {seedref = ref (nextrand seed)};
 
 fun newgen () = newgenseed (Time.toReal (Time.now ()));
 
-fun random {seedref as ref seed} = 
-    (seedref := nextrand seed; seed / m);
-
-fun randomlist (n, {seedref as ref seed0}) = 
-    let fun h 0 seed res = (seedref := seed; res)
+fun random {seedref} = CRITICAL (fn () => 
+    (seedref := nextrand (! seedref); ! seedref / m));
+
+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
 end;
 
 (**** Original file: Useful.sig ****)

 
   fun calcPrimes n = looking [] n (K true) 2
 
   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
           val l = calcPrimes n
           val () = primesList := l
         in
           l
-        end;
-
-  fun primesUpTo n =
+        end);
+
+  fun primesUpTo n = CRITICAL (fn () =>
       let
         fun f k [] =
             let
               val l = calcPrimes (2 * k)
               val () = primesList := l

             end
           | f k (p :: ps) =
             if p <= n then f (k + 1) ps else List.take (!primesList, k)
       in
         f 0 (!primesList)
-      end;
+      end);
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Strings.                                                                  *)
 (* ------------------------------------------------------------------------- *)

 (* ------------------------------------------------------------------------- *)
 
 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
   val gen = Random.newgenseed 1.0;
 in

 
 val newSkolemFunction =
     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 =
     let
       val fv = NameSet.transform Term.Var fv

 
 val newDefinitionRelation =
     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 =
     let
       val fv = freeVars def

 
 val newId =
     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;
 
 (* ------------------------------------------------------------------------- *)
 (* A type of clause.                                                         *)
 (* ------------------------------------------------------------------------- *)