1.1 --- a/src/Tools/Metis/src/Clause.sml Fri Aug 17 23:10:49 2007 +0200
1.2 +++ b/src/Tools/Metis/src/Clause.sml Fri Aug 17 23:10:50 2007 +0200
1.3 @@ -16,7 +16,8 @@
1.4 let
1.5 val r = ref 0
1.6 in
1.7 - fn () => case r of ref n => let val () = r := n + 1 in n end
1.8 + fn () => CRITICAL (fn () =>
1.9 + case r of ref n => let val () = r := n + 1 in n end)
1.10 end;
1.11
1.12 (* ------------------------------------------------------------------------- *)
2.1 --- a/src/Tools/Metis/src/Normalize.sml Fri Aug 17 23:10:49 2007 +0200
2.2 +++ b/src/Tools/Metis/src/Normalize.sml Fri Aug 17 23:10:50 2007 +0200
2.3 @@ -795,14 +795,14 @@
2.4 let
2.5 val counter : int NameMap.map ref = ref (NameMap.new ())
2.6 in
2.7 - fn n =>
2.8 + fn n => CRITICAL (fn () =>
2.9 let
2.10 val ref m = counter
2.11 val i = Option.getOpt (NameMap.peek m n, 0)
2.12 val () = counter := NameMap.insert m (n, i + 1)
2.13 in
2.14 "skolem_" ^ n ^ (if i = 0 then "" else "_" ^ Int.toString i)
2.15 - end
2.16 + end)
2.17 end;
2.18
2.19 fun skolemize fv bv fm =
2.20 @@ -993,13 +993,13 @@
2.21 let
2.22 val counter : int ref = ref 0
2.23 in
2.24 - fn () =>
2.25 + fn () => CRITICAL (fn () =>
2.26 let
2.27 val ref i = counter
2.28 val () = counter := i + 1
2.29 in
2.30 "defCNF_" ^ Int.toString i
2.31 - end
2.32 + end)
2.33 end;
2.34
2.35 fun newDefinition def =
3.1 --- a/src/Tools/Metis/src/Portable.sig Fri Aug 17 23:10:49 2007 +0200
3.2 +++ b/src/Tools/Metis/src/Portable.sig Fri Aug 17 23:10:50 2007 +0200
3.3 @@ -24,4 +24,10 @@
3.4
3.5 val time : ('a -> 'b) -> 'a -> 'b
3.6
3.7 +(* ------------------------------------------------------------------------- *)
3.8 +(* Critical section markup (multiprocessing) *)
3.9 +(* ------------------------------------------------------------------------- *)
3.10 +
3.11 +val CRITICAL: (unit -> 'a) -> 'a
3.12 +
3.13 end
4.1 --- a/src/Tools/Metis/src/PortableIsabelle.sml Fri Aug 17 23:10:49 2007 +0200
4.2 +++ b/src/Tools/Metis/src/PortableIsabelle.sml Fri Aug 17 23:10:50 2007 +0200
4.3 @@ -23,6 +23,12 @@
4.4
4.5 val time = timeap;
4.6
4.7 +(* ------------------------------------------------------------------------- *)
4.8 +(* Critical section markup (multiprocessing) *)
4.9 +(* ------------------------------------------------------------------------- *)
4.10 +
4.11 +val CRITICAL = CRITICAL;
4.12 +
4.13 end
4.14
4.15 (* ------------------------------------------------------------------------- *)
5.1 --- a/src/Tools/Metis/src/PortableMlton.sml Fri Aug 17 23:10:49 2007 +0200
5.2 +++ b/src/Tools/Metis/src/PortableMlton.sml Fri Aug 17 23:10:50 2007 +0200
5.3 @@ -56,6 +56,12 @@
5.4 y
5.5 end;
5.6
5.7 +(* ------------------------------------------------------------------------- *)
5.8 +(* Critical section markup (multiprocessing) *)
5.9 +(* ------------------------------------------------------------------------- *)
5.10 +
5.11 +fun CRITICAL e = e (); (*dummy*)
5.12 +
5.13 end
5.14
5.15 (* ------------------------------------------------------------------------- *)
6.1 --- a/src/Tools/Metis/src/PortableMosml.sml Fri Aug 17 23:10:49 2007 +0200
6.2 +++ b/src/Tools/Metis/src/PortableMosml.sml Fri Aug 17 23:10:50 2007 +0200
6.3 @@ -26,6 +26,12 @@
6.4
6.5 val time = Mosml.time;
6.6
6.7 +(* ------------------------------------------------------------------------- *)
6.8 +(* Critical section markup (multiprocessing) *)
6.9 +(* ------------------------------------------------------------------------- *)
6.10 +
6.11 +fun CRITICAL e = e (); (*dummy*)
6.12 +
6.13 end
6.14
6.15 (* ------------------------------------------------------------------------- *)
7.1 --- a/src/Tools/Metis/src/PortableSmlNJ.sml Fri Aug 17 23:10:49 2007 +0200
7.2 +++ b/src/Tools/Metis/src/PortableSmlNJ.sml Fri Aug 17 23:10:50 2007 +0200
7.3 @@ -52,6 +52,12 @@
7.4 y
7.5 end;
7.6
7.7 +(* ------------------------------------------------------------------------- *)
7.8 +(* Critical section markup (multiprocessing) *)
7.9 +(* ------------------------------------------------------------------------- *)
7.10 +
7.11 +fun CRITICAL e = e (); (*dummy*)
7.12 +
7.13 end
7.14
7.15 (* ------------------------------------------------------------------------- *)
8.1 --- a/src/Tools/Metis/src/Random.sml Fri Aug 17 23:10:49 2007 +0200
8.2 +++ b/src/Tools/Metis/src/Random.sml Fri Aug 17 23:10:50 2007 +0200
8.3 @@ -18,27 +18,29 @@
8.4
8.5 fun newgen () = newgenseed (Time.toReal (Time.now ()));
8.6
8.7 -fun random {seedref as ref seed} =
8.8 - (seedref := nextrand seed; seed / m);
8.9 +fun random {seedref} = CRITICAL (fn () =>
8.10 + (seedref := nextrand (! seedref); ! seedref / m));
8.11
8.12 -fun randomlist (n, {seedref as ref seed0}) =
8.13 - let fun h 0 seed res = (seedref := seed; res)
8.14 +fun randomlist (n, {seedref}) = CRITICAL (fn () =>
8.15 + let val seed0 = ! seedref
8.16 + fun h 0 seed res = (seedref := seed; res)
8.17 | h i seed res = h (i-1) (nextrand seed) (seed / m :: res)
8.18 - in h n seed0 [] end;
8.19 + in h n seed0 [] end);
8.20
8.21 fun range (min, max) =
8.22 if min > max then raise Fail "Random.range: empty range"
8.23 else
8.24 - fn {seedref as ref seed} =>
8.25 - (seedref := nextrand seed; min + (floor(real(max-min) * seed / m)));
8.26 + fn {seedref} => CRITICAL (fn () =>
8.27 + (seedref := nextrand (! seedref); min + (floor(real(max-min) * ! seedref / m))));
8.28
8.29 fun rangelist (min, max) =
8.30 if min > max then raise Fail "Random.rangelist: empty range"
8.31 else
8.32 - fn (n, {seedref as ref seed0}) =>
8.33 - let fun h 0 seed res = (seedref := seed; res)
8.34 + fn (n, {seedref}) => CRITICAL (fn () =>
8.35 + let val seed0 = ! seedref
8.36 + fun h 0 seed res = (seedref := seed; res)
8.37 | h i seed res = h (i-1) (nextrand seed)
8.38 (min + floor(real(max-min) * seed / m) :: res)
8.39 - in h n seed0 [] end
8.40 + in h n seed0 [] end)
8.41
8.42 end
9.1 --- a/src/Tools/Metis/src/Useful.sml Fri Aug 17 23:10:49 2007 +0200
9.2 +++ b/src/Tools/Metis/src/Useful.sml Fri Aug 17 23:10:50 2007 +0200
9.3 @@ -377,7 +377,7 @@
9.4
9.5 val primesList = ref (calcPrimes 10);
9.6 in
9.7 - fun primes n =
9.8 + fun primes n = CRITICAL (fn () =>
9.9 if length (!primesList) <= n then List.take (!primesList,n)
9.10 else
9.11 let
9.12 @@ -385,9 +385,9 @@
9.13 val () = primesList := l
9.14 in
9.15 l
9.16 - end;
9.17 + end);
9.18
9.19 - fun primesUpTo n =
9.20 + fun primesUpTo n = CRITICAL (fn () =>
9.21 let
9.22 fun f k [] =
9.23 let
9.24 @@ -400,7 +400,7 @@
9.25 if p <= n then f (k + 1) ps else List.take (!primesList, k)
9.26 in
9.27 f 0 (!primesList)
9.28 - end;
9.29 + end);
9.30 end;
9.31
9.32 (* ------------------------------------------------------------------------- *)
9.33 @@ -572,22 +572,22 @@
9.34 local
9.35 val generator = ref 0
9.36 in
9.37 - fun newInt () =
9.38 + fun newInt () = CRITICAL (fn () =>
9.39 let
9.40 val n = !generator
9.41 val () = generator := n + 1
9.42 in
9.43 n
9.44 - end;
9.45 + end);
9.46
9.47 fun newInts 0 = []
9.48 - | newInts k =
9.49 + | newInts k = CRITICAL (fn () =>
9.50 let
9.51 val n = !generator
9.52 val () = generator := n + k
9.53 in
9.54 interval n k
9.55 - end;
9.56 + end);
9.57 end;
9.58
9.59 local