Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: base_generator.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Tools/Spec_Check/base_generator.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Basic random generators.
*)

signature BASE_GENERATOR =
sig

type rand
type 'a gen = rand -> 'a * rand
type ('a, 'b) co = 'a -> 'b gen -> 'b gen

val new : unit -> rand
val range : int * int -> rand -> int * rand
type ('a, 'b) reader = 'b -> ('a * 'b) option

val lift : 'a -> 'a gen
val select : 'a vector -> 'a gen
val choose : 'a gen vector -> 'a gen
val choose' : (int * 'a gen) vector -> 'a gen
val selectL : 'a list -> 'a gen
val chooseL : 'a gen list -> 'a gen
val chooseL' : (int * 'a gen) list -> 'a gen
val filter : ('a -> bool) -> 'a gen -> 'a gen

val zip : ('a gen * 'b gen) -> ('a * 'b) gen
val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
val map : ('a -> 'b) -> 'a gen -> 'b gen
val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen

val flip : bool gen
val flip' : int * int -> bool gen

val list : bool gen -> 'a gen -> 'a list gen
val option : bool gen -> 'a gen -> 'a option gen
val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen

val variant : (int, 'b) co
val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
val cobool : (bool, 'b) co
val colist : ('a, 'b) co -> ('a list, 'b) co
val coopt : ('a, 'b) co -> ('a option, 'b) co

type stream
val start : rand -> stream
val limit : int -> 'a gen -> ('a, stream) reader

end

structure Base_Generator : BASE_GENERATOR =
struct

(* random number engine *)

type rand = real

val a = 16807.0
val m = 2147483647.0

fun nextrand seed =
  let
    val t = a * seed
  in
    t - m * real (floor (t / m))
  end

val new = nextrand o Time.toReal o Time.now

fun range (min, max) =
  if min > max then raise Domain (* TODO: raise its own error *)
  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)

fun split r =
  let
    val r = r / a
    val r0 = real (floor r)
    val r1 = r - r0
  in
    (nextrand r0, nextrand r1)
  end

(* generators *)

type 'a gen = rand -> 'a * rand
type ('a, 'b) reader = 'b -> ('a * 'b) option

fun lift obj r = (obj, r)

local (* Isabelle does not use vectors? *)
  fun explode ((freq, gen), acc) =
    List.tabulate (freq, fn _ => gen) @ acc
in
  fun choose v r =
    let val (i, r) = range(0, Vector.length v - 1) r
    in Vector.sub (v, i) r end
  fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
  fun select v = choose (Vector.map lift v)
end

fun chooseL l = choose (Vector.fromList l)
fun chooseL' l = choose' (Vector.fromList l)
fun selectL l = select (Vector.fromList l)

fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))

fun zip3 (g1, g2, g3) =
  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))

fun zip4 (g1, g2, g3, g4) =
  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))

fun map f g = apfst f o g

fun map2 f = map f o zip
fun map3 f = map f o zip3
fun map4 f = map f o zip4

fun filter p gen r =
  let
    fun loop (x, r) = if p x then (x, r) else loop (gen r)
  in
    loop (gen r)
  end

val flip = selectL [true, false]
fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]

fun list flip g r =
  case flip r of
      (true, r) => ([], r)
    | (false, r) =>
      let
        val (x,r) = g r
        val (xs,r) = list flip g r
      in (x::xs, r) end

fun option flip g r =
  case flip r of
    (true, r) => (NONE, r)
  | (false, r) => map SOME g r

fun vector tabulate (int, elem) r =
  let
    val (n, r) = int r
    val p = Unsynchronized.ref r
    fun g _ =
      let
        val (x,r) = elem(!p)
      in x before p := r end
  in
    (tabulate(n, g), !p)
  end

type stream = rand Unsynchronized.ref * int

fun start r = (Unsynchronized.ref r, 0)

fun limit max gen =
  let
    fun next (p, i) =
      if i >= max then NONE
      else
        let val (x, r) = gen(!p)
        in SOME(x, (p, i+1)) before p := r end
  in
    next
  end

type ('a, 'b) co = 'a -> 'b gen -> 'b gen

fun variant v g r =
  let
    fun nth (i, r) =
      let val (r1, r2) = split r
      in if i = 0 then r1 else nth (i-1, r2) end
  in
    g (nth (v, r))
  end

fun arrow (cogen, gen) r =
  let
    val (r1, r2) = split r
    fun g x = fst (cogen x gen r1)
  in (g, r2) end

fun cobool false = variant 0
  | cobool true = variant 1

fun colist _ [] = variant 0
  | colist co (x::xs) = variant 1 o co x o colist co xs

fun coopt _ NONE = variant 0
  | coopt co (SOME x) = variant 1 o co x

end

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.