src/Tools/Spec_Check/generator.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 53164 beb4ee344c22
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Tools/Spec_Check/generator.ML
     2     Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     3     Author:     Christopher League
     4 
     5 Random generators for Isabelle/ML's types.
     6 *)
     7 
     8 signature GENERATOR = sig
     9   include BASE_GENERATOR
    10   (* text generators *)
    11   val char : char gen
    12   val charRange : char * char -> char gen
    13   val charFrom : string -> char gen
    14   val charByType : (char -> bool) -> char gen
    15   val string : (int gen * char gen) -> string gen
    16   val substring : string gen -> substring gen
    17   val cochar : (char, 'b) co
    18   val costring : (string, 'b) co
    19   val cosubstring : (substring, 'b) co
    20   (* integer generators *)
    21   val int : int gen
    22   val int_pos : int gen
    23   val int_neg : int gen
    24   val int_nonpos : int gen
    25   val int_nonneg : int gen
    26   val coint : (int, 'b) co
    27   (* real generators *)
    28   val real : real gen
    29   val real_frac : real gen
    30   val real_pos : real gen
    31   val real_neg : real gen
    32   val real_nonpos : real gen
    33   val real_nonneg : real gen
    34   val real_finite : real gen
    35   (* function generators *)
    36   val function_const : 'c * 'b gen -> ('a -> 'b) gen
    37   val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
    38   val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
    39   val unit : unit gen
    40   val ref' : 'a gen -> 'a Unsynchronized.ref gen
    41   (* more generators *)
    42   val term : int -> term gen
    43   val typ : int -> typ gen
    44 
    45   val stream : stream
    46 end
    47 
    48 structure Generator : GENERATOR =
    49 struct
    50 
    51 open Base_Generator
    52 
    53 val stream = start (new())
    54 
    55 type 'a gen = rand -> 'a * rand
    56 type ('a, 'b) co = 'a -> 'b gen -> 'b gen
    57 
    58 (* text *)
    59 
    60 type char = Char.char
    61 type string = String.string
    62 type substring = Substring.substring
    63 
    64 
    65 val char = map Char.chr (range (0, Char.maxOrd))
    66 fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
    67 
    68 fun charFrom s =
    69   choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
    70 
    71 fun charByType p = filter p char
    72 
    73 val string = vector CharVector.tabulate
    74 
    75 fun substring gen r =
    76   let
    77     val (s, r') = gen r
    78     val (i, r'') = range (0, String.size s) r'
    79     val (j, r''') = range (0, String.size s - i) r''
    80   in
    81     (Substring.substring (s, i, j), r''')
    82   end
    83 
    84 fun cochar c =
    85   if Char.ord c = 0 then variant 0
    86   else variant 1 o cochar (Char.chr (Char.ord c div 2))
    87 
    88 fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
    89 
    90 fun costring s = cosubstring (Substring.full s)
    91 
    92 (* integers *)
    93 val digit = charRange (#"0", #"9")
    94 val nonzero = string (lift 1, charRange (#"1", #"9"))
    95 fun digits' n = string (range (0, n-1), digit)
    96 fun digits n = map2 op^ (nonzero, digits' n)
    97 
    98 val maxDigits = 64
    99 val ratio = 49
   100 
   101 fun pos_or_neg f r =
   102   let
   103     val (s, r') = digits maxDigits r
   104   in (f (the (Int.fromString s)), r') end
   105 
   106 val int_pos = pos_or_neg I
   107 val int_neg = pos_or_neg Int.~
   108 val zero = lift 0
   109 
   110 val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
   111 val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
   112 val int = chooseL [int_nonneg, int_nonpos]
   113 
   114 fun coint n =
   115   if n = 0 then variant 0
   116   else if n < 0 then variant 1 o coint (~ n)
   117   else variant 2 o coint (n div 2)
   118 
   119 (* reals *)
   120 val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
   121 
   122 fun real_frac r =
   123   let val (s, r') = digits r
   124   in (the (Real.fromString s), r') end
   125 
   126 val {exp=minExp,...} = Real.toManExp Real.minPos
   127 val {exp=maxExp,...} = Real.toManExp Real.posInf
   128 
   129 val ratio = 99
   130 
   131 fun mk r =
   132   let
   133     val (a, r') = digits r
   134     val (b, r'') = digits r'
   135     val (e, r''') = range (minExp div 4, maxExp div 4) r''
   136     val x = String.concat [a, ".", b, "E", Int.toString e]
   137   in
   138     (the (Real.fromString x), r''')
   139   end
   140 
   141 val real_pos = chooseL' (List.map ((pair 1) o lift)
   142     [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
   143 
   144 val real_neg = map Real.~ real_pos
   145 
   146 val real_zero = Real.fromInt 0
   147 val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
   148 val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
   149 
   150 val real = chooseL [real_nonneg, real_nonpos]
   151 
   152 val real_finite = filter Real.isFinite real
   153 
   154 (*alternate list generator - uses an integer generator to determine list length*)
   155 fun list' int gen = vector List.tabulate (int, gen);
   156 
   157 (* more function generators *)
   158 
   159 fun function_const (_, gen2) r =
   160   let
   161     val (v, r') = gen2 r
   162   in (fn _ => v, r') end;
   163 
   164 fun function_strict size (gen1, gen2) r =
   165   let
   166     val (def, r') = gen2 r
   167     val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
   168   in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
   169 
   170 fun function_lazy (gen1, gen2) r =
   171   let
   172     val (initial1, r') = gen1 r
   173     val (initial2, internal) = gen2 r'
   174     val seed = Unsynchronized.ref internal
   175     val table = Unsynchronized.ref [(initial1, initial2)]
   176     fun new_entry k =
   177       let
   178         val (new_val, new_seed) = gen2 (!seed)
   179         val _ =  seed := new_seed
   180         val _ = table := AList.update (op =) (k, new_val) (!table)
   181       in new_val end
   182   in
   183     (fn v1 =>
   184       case AList.lookup (op =) (!table) v1 of
   185         NONE => new_entry v1
   186       | SOME v2 => v2, r')
   187   end;
   188 
   189 (* unit *)
   190 
   191 fun unit r = ((), r);
   192 
   193 (* references *)
   194 
   195 fun ref' gen r =
   196   let val (value, r') = gen r
   197   in (Unsynchronized.ref value, r') end;
   198 
   199 (* types and terms *)
   200 
   201 val sort_string = selectL ["sort1", "sort2", "sort3"];
   202 val type_string = selectL ["TCon1", "TCon2", "TCon3"];
   203 val tvar_string = selectL ["a", "b", "c"];
   204 
   205 val const_string = selectL ["c1", "c2", "c3"];
   206 val var_string = selectL ["x", "y", "z"];
   207 val index = selectL [0, 1, 2, 3];
   208 val bound_index = selectL [0, 1, 2, 3];
   209 
   210 val sort = list (flip' (1, 2)) sort_string;
   211 
   212 fun typ n =
   213   let
   214     fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
   215     val tfree = map TFree (zip (tvar_string, sort))
   216     val tvar = map TVar (zip (zip (tvar_string, index), sort))
   217   in
   218     if n = 0 then chooseL [tfree, tvar]
   219     else chooseL [type' (n div 2), tfree, tvar]
   220   end;
   221 
   222 fun term n =
   223   let
   224     val const = map Const (zip (const_string, typ 10))
   225     val free = map Free (zip (var_string, typ 10))
   226     val var = map Var (zip (zip (var_string, index), typ 10))
   227     val bound = map Bound bound_index
   228     fun abs m = map Abs (zip3 (var_string, typ 10, term m))
   229     fun app m = map (op $) (zip (term m, term m))
   230   in
   231     if n = 0 then chooseL [const, free, var, bound]
   232     else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
   233   end;
   234 
   235 end