--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generator.ML Fri Aug 23 12:40:55 2013 +0200
@@ -0,0 +1,235 @@
+(* Title: Tools/Spec_Check/generator.ML
+ Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+ Author: Christopher League
+
+Random generators for Isabelle/ML's types.
+*)
+
+signature GENERATOR = sig
+ include BASE_GENERATOR
+ (* text generators *)
+ val char : char gen
+ val charRange : char * char -> char gen
+ val charFrom : string -> char gen
+ val charByType : (char -> bool) -> char gen
+ val string : (int gen * char gen) -> string gen
+ val substring : string gen -> substring gen
+ val cochar : (char, 'b) co
+ val costring : (string, 'b) co
+ val cosubstring : (substring, 'b) co
+ (* integer generators *)
+ val int : int gen
+ val int_pos : int gen
+ val int_neg : int gen
+ val int_nonpos : int gen
+ val int_nonneg : int gen
+ val coint : (int, 'b) co
+ (* real generators *)
+ val real : real gen
+ val real_frac : real gen
+ val real_pos : real gen
+ val real_neg : real gen
+ val real_nonpos : real gen
+ val real_nonneg : real gen
+ val real_finite : real gen
+ (* function generators *)
+ val function_const : 'c * 'b gen -> ('a -> 'b) gen
+ val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
+ val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
+ val unit : unit gen
+ val ref' : 'a gen -> 'a Unsynchronized.ref gen
+ (* more generators *)
+ val term : int -> term gen
+ val typ : int -> typ gen
+
+ val stream : stream
+end
+
+structure Generator : GENERATOR =
+struct
+
+open Base_Generator
+
+val stream = start (new())
+
+type 'a gen = rand -> 'a * rand
+type ('a, 'b) co = 'a -> 'b gen -> 'b gen
+
+(* text *)
+
+type char = Char.char
+type string = String.string
+type substring = Substring.substring
+
+
+val char = map Char.chr (range (0, Char.maxOrd))
+fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
+
+fun charFrom s =
+ choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
+
+fun charByType p = filter p char
+
+val string = vector CharVector.tabulate
+
+fun substring gen r =
+ let
+ val (s, r') = gen r
+ val (i, r'') = range (0, String.size s) r'
+ val (j, r''') = range (0, String.size s - i) r''
+ in
+ (Substring.substring (s, i, j), r''')
+ end
+
+fun cochar c =
+ if Char.ord c = 0 then variant 0
+ else variant 1 o cochar (Char.chr (Char.ord c div 2))
+
+fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
+
+fun costring s = cosubstring (Substring.full s)
+
+(* integers *)
+val digit = charRange (#"0", #"9")
+val nonzero = string (lift 1, charRange (#"1", #"9"))
+fun digits' n = string (range (0, n-1), digit)
+fun digits n = map2 op^ (nonzero, digits' n)
+
+val maxDigits = 64
+val ratio = 49
+
+fun pos_or_neg f r =
+ let
+ val (s, r') = digits maxDigits r
+ in (f (the (Int.fromString s)), r') end
+
+val int_pos = pos_or_neg I
+val int_neg = pos_or_neg Int.~
+val zero = lift 0
+
+val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
+val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
+val int = chooseL [int_nonneg, int_nonpos]
+
+fun coint n =
+ if n = 0 then variant 0
+ else if n < 0 then variant 1 o coint (~ n)
+ else variant 2 o coint (n div 2)
+
+(* reals *)
+val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
+
+fun real_frac r =
+ let val (s, r') = digits r
+ in (the (Real.fromString s), r') end
+
+val {exp=minExp,...} = Real.toManExp Real.minPos
+val {exp=maxExp,...} = Real.toManExp Real.posInf
+
+val ratio = 99
+
+fun mk r =
+ let
+ val (a, r') = digits r
+ val (b, r'') = digits r'
+ val (e, r''') = range (minExp div 4, maxExp div 4) r''
+ val x = String.concat [a, ".", b, "E", Int.toString e]
+ in
+ (the (Real.fromString x), r''')
+ end
+
+val real_pos = chooseL' (List.map ((pair 1) o lift)
+ [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
+
+val real_neg = map Real.~ real_pos
+
+val real_zero = Real.fromInt 0
+val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
+val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
+
+val real = chooseL [real_nonneg, real_nonpos]
+
+val real_finite = filter Real.isFinite real
+
+(*alternate list generator - uses an integer generator to determine list length*)
+fun list' int gen = vector List.tabulate (int, gen);
+
+(* more function generators *)
+
+fun function_const (_, gen2) r =
+ let
+ val (v, r') = gen2 r
+ in (fn _ => v, r') end;
+
+fun function_strict size (gen1, gen2) r =
+ let
+ val (def, r') = gen2 r
+ val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
+ in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
+
+fun function_lazy (gen1, gen2) r =
+ let
+ val (initial1, r') = gen1 r
+ val (initial2, internal) = gen2 r'
+ val seed = Unsynchronized.ref internal
+ val table = Unsynchronized.ref [(initial1, initial2)]
+ fun new_entry k =
+ let
+ val (new_val, new_seed) = gen2 (!seed)
+ val _ = seed := new_seed
+ val _ = table := AList.update (op =) (k, new_val) (!table)
+ in new_val end
+ in
+ (fn v1 =>
+ case AList.lookup (op =) (!table) v1 of
+ NONE => new_entry v1
+ | SOME v2 => v2, r')
+ end;
+
+(* unit *)
+
+fun unit r = ((), r);
+
+(* references *)
+
+fun ref' gen r =
+ let val (value, r') = gen r
+ in (Unsynchronized.ref value, r') end;
+
+(* types and terms *)
+
+val sort_string = selectL ["sort1", "sort2", "sort3"];
+val type_string = selectL ["TCon1", "TCon2", "TCon3"];
+val tvar_string = selectL ["a", "b", "c"];
+
+val const_string = selectL ["c1", "c2", "c3"];
+val var_string = selectL ["x", "y", "z"];
+val index = selectL [0, 1, 2, 3];
+val bound_index = selectL [0, 1, 2, 3];
+
+val sort = list (flip' (1, 2)) sort_string;
+
+fun typ n =
+ let
+ fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
+ val tfree = map TFree (zip (tvar_string, sort))
+ val tvar = map TVar (zip (zip (tvar_string, index), sort))
+ in
+ if n = 0 then chooseL [tfree, tvar]
+ else chooseL [type' (n div 2), tfree, tvar]
+ end;
+
+fun term n =
+ let
+ val const = map Const (zip (const_string, typ 10))
+ val free = map Free (zip (var_string, typ 10))
+ val var = map Var (zip (zip (var_string, index), typ 10))
+ val bound = map Bound bound_index
+ fun abs m = map Abs (zip3 (var_string, typ 10, term m))
+ fun app m = map (op $) (zip (term m, term m))
+ in
+ if n = 0 then chooseL [const, free, var, bound]
+ else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
+ end;
+
+end