# HG changeset patch # User wenzelm # Date 1198157621 -3600 # Node ID dfb7fee72ff24fd2b8bce6e7db6d1415a25b2855 # Parent 71e33d95ac55bd6bbbadd34a93dd1c620875ccc7 removed obsolete (slow!) Random implementation; diff -r 71e33d95ac55 -r dfb7fee72ff2 src/Tools/Metis/metis.ML --- 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 ****) (* ========================================================================= *) diff -r 71e33d95ac55 -r dfb7fee72ff2 src/Tools/Metis/src/FILES --- 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 diff -r 71e33d95ac55 -r dfb7fee72ff2 src/Tools/Metis/src/Random.sig --- 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. -*) diff -r 71e33d95ac55 -r dfb7fee72ff2 src/Tools/Metis/src/Random.sml --- 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