--- a/src/Tools/Metis/metis.ML Thu Dec 20 14:33:40 2007 +0100
+++ b/src/Tools/Metis/metis.ML Thu Dec 20 14:33:41 2007 +0100
@@ -9,101 +9,6 @@
structure Metis = struct structure Word = Word structure Array = Array end;
-(**** Original file: Random.sig ****)
-
-(* Random -- random number generator *)
-
-signature Random =
-sig
-
-type generator
-
-val newgenseed : real -> generator
-val newgen : unit -> generator
-val random : generator -> real
-val randomlist : int * generator -> real list
-val range : int * int -> generator -> int
-val rangelist : int * int -> int * generator -> int list
-
-end
-
-(*
- [generator] is the type of random number generators, here the
- linear congruential generators from Paulson 1991, 1996.
-
- [newgenseed seed] returns a random number generator with the given seed.
-
- [newgen ()] returns a random number generator, taking the seed from
- the system clock.
-
- [random gen] returns a random number in the interval [0..1).
-
- [randomlist (n, gen)] returns a list of n random numbers in the
- interval [0,1).
-
- [range (min, max) gen] returns an integral random number in the
- range [min, max). Raises Fail if min > max.
-
- [rangelist (min, max) (n, gen)] returns a list of n integral random
- numbers in the range [min, max). Raises Fail if min > max.
-*)
-
-(**** Original file: Random.sml ****)
-
-structure Metis = struct open Metis
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-(* Random -- Moscow ML library 1995-04-23, 1999-02-24 *)
-
-structure Random :> Random =
-struct
-
-type generator = {seedref : real ref}
-
-(* Generating random numbers. Paulson, page 96 *)
-
-val a = 16807.0
-val m = 2147483647.0
-fun nextrand seed =
- let val t = a*seed
- in t - m * real(floor(t/m)) end
-
-fun newgenseed seed =
- {seedref = ref (nextrand seed)};
-
-fun newgen () = newgenseed (Time.toReal (Time.now ()));
-
-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);
-
-fun range (min, max) =
- if min > max then raise Fail "Random.range: empty range"
- else
- 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}) => 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)
-
-end
-end;
-
(**** Original file: Portable.sig ****)
(* ========================================================================= *)
--- a/src/Tools/Metis/src/FILES Thu Dec 20 14:33:40 2007 +0100
+++ b/src/Tools/Metis/src/FILES Thu Dec 20 14:33:41 2007 +0100
@@ -1,39 +1,38 @@
-Random.sig Random.sml
Portable.sig PortableIsabelle.sml
-PP.sig PP.sml
-Useful.sig Useful.sml
-Lazy.sig Lazy.sml
-Ordered.sig Ordered.sml
-Set.sig RandomSet.sml Set.sml
-ElementSet.sig ElementSet.sml
-Map.sig RandomMap.sml Map.sml
-KeyMap.sig KeyMap.sml
-Sharing.sig Sharing.sml
-Stream.sig Stream.sml
-Heap.sig Heap.sml
-Parser.sig Parser.sml
-Options.sig Options.sml
-Name.sig Name.sml
-Term.sig Term.sml
-Subst.sig Subst.sml
-Atom.sig Atom.sml
-Formula.sig Formula.sml
-Literal.sig Literal.sml
-Thm.sig Thm.sml
-Proof.sig Proof.sml
-Rule.sig Rule.sml
-Normalize.sig Normalize.sml
-Model.sig Model.sml
-Problem.sig Problem.sml
-TermNet.sig TermNet.sml
-AtomNet.sig AtomNet.sml
-LiteralNet.sig LiteralNet.sml
-Subsume.sig Subsume.sml
-KnuthBendixOrder.sig KnuthBendixOrder.sml
-Rewrite.sig Rewrite.sml
-Units.sig Units.sml
-Clause.sig Clause.sml
-Active.sig Active.sml
-Waiting.sig Waiting.sml
+PP.sig PP.sml
+Useful.sig Useful.sml
+Lazy.sig Lazy.sml
+Ordered.sig Ordered.sml
+Set.sig RandomSet.sml Set.sml
+ElementSet.sig ElementSet.sml
+Map.sig RandomMap.sml Map.sml
+KeyMap.sig KeyMap.sml
+Sharing.sig Sharing.sml
+Stream.sig Stream.sml
+Heap.sig Heap.sml
+Parser.sig Parser.sml
+Options.sig Options.sml
+Name.sig Name.sml
+Term.sig Term.sml
+Subst.sig Subst.sml
+Atom.sig Atom.sml
+Formula.sig Formula.sml
+Literal.sig Literal.sml
+Thm.sig Thm.sml
+Proof.sig Proof.sml
+Rule.sig Rule.sml
+Normalize.sig Normalize.sml
+Model.sig Model.sml
+Problem.sig Problem.sml
+TermNet.sig TermNet.sml
+AtomNet.sig AtomNet.sml
+LiteralNet.sig LiteralNet.sml
+Subsume.sig Subsume.sml
+KnuthBendixOrder.sig KnuthBendixOrder.sml
+Rewrite.sig Rewrite.sml
+Units.sig Units.sml
+Clause.sig Clause.sml
+Active.sig Active.sml
+Waiting.sig Waiting.sml
Resolution.sig Resolution.sml
-Tptp.sig Tptp.sml
+Tptp.sig Tptp.sml
--- a/src/Tools/Metis/src/Random.sig Thu Dec 20 14:33:40 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-(* Random -- random number generator *)
-
-signature Random =
-sig
-
-type generator
-
-val newgenseed : real -> generator
-val newgen : unit -> generator
-val random : generator -> real
-val randomlist : int * generator -> real list
-val range : int * int -> generator -> int
-val rangelist : int * int -> int * generator -> int list
-
-end
-
-(*
- [generator] is the type of random number generators, here the
- linear congruential generators from Paulson 1991, 1996.
-
- [newgenseed seed] returns a random number generator with the given seed.
-
- [newgen ()] returns a random number generator, taking the seed from
- the system clock.
-
- [random gen] returns a random number in the interval [0..1).
-
- [randomlist (n, gen)] returns a list of n random numbers in the
- interval [0,1).
-
- [range (min, max) gen] returns an integral random number in the
- range [min, max). Raises Fail if min > max.
-
- [rangelist (min, max) (n, gen)] returns a list of n integral random
- numbers in the range [min, max). Raises Fail if min > max.
-*)
--- a/src/Tools/Metis/src/Random.sml Thu Dec 20 14:33:40 2007 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* Random -- Moscow ML library 1995-04-23, 1999-02-24 *)
-
-structure Random :> Random =
-struct
-
-type generator = {seedref : real ref}
-
-(* Generating random numbers. Paulson, page 96 *)
-
-val a = 16807.0
-val m = 2147483647.0
-fun nextrand seed =
- let val t = a*seed
- in t - m * real(floor(t/m)) end
-
-fun newgenseed seed =
- {seedref = ref (nextrand seed)};
-
-fun newgen () = newgenseed (Time.toReal (Time.now ()));
-
-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);
-
-fun range (min, max) =
- if min > max then raise Fail "Random.range: empty range"
- else
- 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}) => 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)
-
-end