--- a/src/Tools/Spec_Check/base_generator.ML Wed Aug 25 22:17:38 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-(* 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
-