src/Tools/Metis/src/Random.sig
author wenzelm
Thu, 11 Nov 2010 13:07:41 +0100
changeset 40476 515eab39b6c2
parent 39443 e330437cd22a
permissions -rw-r--r--
reduced danger of line breaks within minipage;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(*  Title:      Tools/random_word.ML
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
    Author:     Makarius
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     3
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
Simple generator for pseudo-random numbers, using unboxed word
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
arithmetic only.  Unprotected concurrency introduces some true
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
randomness.
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
*)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
signature Random =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
sig
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    11
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
  val nextWord : unit -> word
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
  val nextBool : unit -> bool
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
  val nextInt : int -> int  (* k -> [0,k) *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
  val nextReal : unit -> real  (* () -> [0,1) *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
end;