src/Tools/Spec_Check/base_generator.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 53164 beb4ee344c22
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Tools/Spec_Check/base_generator.ML
     2     Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     3     Author:     Christopher League
     4 
     5 Basic random generators.
     6 *)
     7 
     8 signature BASE_GENERATOR =
     9 sig
    10 
    11 type rand
    12 type 'a gen = rand -> 'a * rand
    13 type ('a, 'b) co = 'a -> 'b gen -> 'b gen
    14 
    15 val new : unit -> rand
    16 val range : int * int -> rand -> int * rand
    17 type ('a, 'b) reader = 'b -> ('a * 'b) option
    18 
    19 val lift : 'a -> 'a gen
    20 val select : 'a vector -> 'a gen
    21 val choose : 'a gen vector -> 'a gen
    22 val choose' : (int * 'a gen) vector -> 'a gen
    23 val selectL : 'a list -> 'a gen
    24 val chooseL : 'a gen list -> 'a gen
    25 val chooseL' : (int * 'a gen) list -> 'a gen
    26 val filter : ('a -> bool) -> 'a gen -> 'a gen
    27 
    28 val zip : ('a gen * 'b gen) -> ('a * 'b) gen
    29 val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
    30 val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
    31 val map : ('a -> 'b) -> 'a gen -> 'b gen
    32 val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
    33 val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
    34 val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
    35 
    36 val flip : bool gen
    37 val flip' : int * int -> bool gen
    38 
    39 val list : bool gen -> 'a gen -> 'a list gen
    40 val option : bool gen -> 'a gen -> 'a option gen
    41 val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
    42 
    43 val variant : (int, 'b) co
    44 val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
    45 val cobool : (bool, 'b) co
    46 val colist : ('a, 'b) co -> ('a list, 'b) co
    47 val coopt : ('a, 'b) co -> ('a option, 'b) co
    48 
    49 type stream
    50 val start : rand -> stream
    51 val limit : int -> 'a gen -> ('a, stream) reader
    52 
    53 end
    54 
    55 structure Base_Generator : BASE_GENERATOR =
    56 struct
    57 
    58 (* random number engine *)
    59 
    60 type rand = real
    61 
    62 val a = 16807.0
    63 val m = 2147483647.0
    64 
    65 fun nextrand seed =
    66   let
    67     val t = a * seed
    68   in
    69     t - m * real (floor (t / m))
    70   end
    71 
    72 val new = nextrand o Time.toReal o Time.now
    73 
    74 fun range (min, max) =
    75   if min > max then raise Domain (* TODO: raise its own error *)
    76   else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
    77 
    78 fun split r =
    79   let
    80     val r = r / a
    81     val r0 = real (floor r)
    82     val r1 = r - r0
    83   in
    84     (nextrand r0, nextrand r1)
    85   end
    86 
    87 (* generators *)
    88 
    89 type 'a gen = rand -> 'a * rand
    90 type ('a, 'b) reader = 'b -> ('a * 'b) option
    91 
    92 fun lift obj r = (obj, r)
    93 
    94 local (* Isabelle does not use vectors? *)
    95   fun explode ((freq, gen), acc) =
    96     List.tabulate (freq, fn _ => gen) @ acc
    97 in
    98   fun choose v r =
    99     let val (i, r) = range(0, Vector.length v - 1) r
   100     in Vector.sub (v, i) r end
   101   fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
   102   fun select v = choose (Vector.map lift v)
   103 end
   104 
   105 fun chooseL l = choose (Vector.fromList l)
   106 fun chooseL' l = choose' (Vector.fromList l)
   107 fun selectL l = select (Vector.fromList l)
   108 
   109 fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
   110 
   111 fun zip3 (g1, g2, g3) =
   112   zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
   113 
   114 fun zip4 (g1, g2, g3, g4) =
   115   zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
   116 
   117 fun map f g = apfst f o g
   118 
   119 fun map2 f = map f o zip
   120 fun map3 f = map f o zip3
   121 fun map4 f = map f o zip4
   122 
   123 fun filter p gen r =
   124   let
   125     fun loop (x, r) = if p x then (x, r) else loop (gen r)
   126   in
   127     loop (gen r)
   128   end
   129 
   130 val flip = selectL [true, false]
   131 fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
   132 
   133 fun list flip g r =
   134   case flip r of
   135       (true, r) => ([], r)
   136     | (false, r) =>
   137       let
   138         val (x,r) = g r
   139         val (xs,r) = list flip g r
   140       in (x::xs, r) end
   141 
   142 fun option flip g r =
   143   case flip r of
   144     (true, r) => (NONE, r)
   145   | (false, r) => map SOME g r
   146 
   147 fun vector tabulate (int, elem) r =
   148   let
   149     val (n, r) = int r
   150     val p = Unsynchronized.ref r
   151     fun g _ =
   152       let
   153         val (x,r) = elem(!p)
   154       in x before p := r end
   155   in
   156     (tabulate(n, g), !p)
   157   end
   158 
   159 type stream = rand Unsynchronized.ref * int
   160 
   161 fun start r = (Unsynchronized.ref r, 0)
   162 
   163 fun limit max gen =
   164   let
   165     fun next (p, i) =
   166       if i >= max then NONE
   167       else
   168         let val (x, r) = gen(!p)
   169         in SOME(x, (p, i+1)) before p := r end
   170   in
   171     next
   172   end
   173 
   174 type ('a, 'b) co = 'a -> 'b gen -> 'b gen
   175 
   176 fun variant v g r =
   177   let
   178     fun nth (i, r) =
   179       let val (r1, r2) = split r
   180       in if i = 0 then r1 else nth (i-1, r2) end
   181   in
   182     g (nth (v, r))
   183   end
   184 
   185 fun arrow (cogen, gen) r =
   186   let
   187     val (r1, r2) = split r
   188     fun g x = fst (cogen x gen r1)
   189   in (g, r2) end
   190 
   191 fun cobool false = variant 0
   192   | cobool true = variant 1
   193 
   194 fun colist _ [] = variant 0
   195   | colist co (x::xs) = variant 1 o co x o colist co xs
   196 
   197 fun coopt _ NONE = variant 0
   198   | coopt co (SOME x) = variant 1 o co x
   199 
   200 end
   201