added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
authorbulwahn
Thu May 30 20:09:49 2013 +0200 (2013-05-30)
changeset 522482c893e0c1def
parent 52247 3244ccb7e9db
child 52249 f4bf6b126cab
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
src/HOL/ROOT
src/HOL/Spec_Check/Examples.thy
src/HOL/Spec_Check/README
src/HOL/Spec_Check/Spec_Check.thy
src/HOL/Spec_Check/base_generator.ML
src/HOL/Spec_Check/gen_construction.ML
src/HOL/Spec_Check/generator.ML
src/HOL/Spec_Check/output_style.ML
src/HOL/Spec_Check/property.ML
src/HOL/Spec_Check/random.ML
src/HOL/Spec_Check/spec_check.ML
     1.1 --- a/src/HOL/ROOT	Thu May 30 17:52:38 2013 +0200
     1.2 +++ b/src/HOL/ROOT	Thu May 30 20:09:49 2013 +0200
     1.3 @@ -740,6 +740,10 @@
     1.4    options [document = false]
     1.5    theories WordExamples
     1.6  
     1.7 +session "HOL-Spec_Check" in Spec_Check = HOL +
     1.8 +  theories
     1.9 +    Examples
    1.10 +
    1.11  session "HOL-Statespace" in Statespace = HOL +
    1.12    theories [skip_proofs = false]
    1.13      StateSpaceEx
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Spec_Check/Examples.thy	Thu May 30 20:09:49 2013 +0200
     2.3 @@ -0,0 +1,73 @@
     2.4 +theory Examples
     2.5 +imports Spec_Check
     2.6 +begin
     2.7 +
     2.8 +section {* List examples *}
     2.9 +
    2.10 +ML {*
    2.11 +check_property @{context} "ALL xs. rev xs = xs";
    2.12 +*}
    2.13 +
    2.14 +ML {*
    2.15 +check_property @{context} "ALL xs. rev (rev xs) = xs";
    2.16 +*}
    2.17 +
    2.18 +
    2.19 +section {* AList Specification *}
    2.20 +
    2.21 +ML {*
    2.22 +(* map_entry applies the function to the element *)
    2.23 +check_property @{context} "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
    2.24 +
    2.25 +(* update always results in an entry *)
    2.26 +check_property @{context} "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
    2.27 +
    2.28 +(* update always writes the value *)
    2.29 +check_property @{context} "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
    2.30 +
    2.31 +(* default always results in an entry *)
    2.32 +check_property @{context} "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
    2.33 +
    2.34 +(* delete always removes the entry *)
    2.35 +check_property @{context} "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
    2.36 +
    2.37 +(* default writes the entry iff it didn't exist *)
    2.38 +check_property @{context} "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
    2.39 +*}
    2.40 +
    2.41 +section {* Examples on Types and Terms *}
    2.42 +
    2.43 +ML {*
    2.44 +check_property @{context} "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
    2.45 +*}
    2.46 +
    2.47 +ML {*
    2.48 +check_property @{context} "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
    2.49 +*}
    2.50 +
    2.51 +text {* One would think this holds: *}
    2.52 +
    2.53 +ML {*
    2.54 +check_property @{context} "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
    2.55 +*}
    2.56 +
    2.57 +text {* But it only holds with this precondition: *}
    2.58 +
    2.59 +ML {*
    2.60 +check_property @{context} "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
    2.61 +*}
    2.62 +
    2.63 +section {* Some surprises *}
    2.64 +
    2.65 +ML {*
    2.66 +check_property @{context} "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
    2.67 +*}
    2.68 +
    2.69 +
    2.70 +
    2.71 +ML {* val thy = @{theory}; *}
    2.72 +ML {*
    2.73 +  check_property @{context} "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
    2.74 +*}
    2.75 +
    2.76 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Spec_Check/README	Thu May 30 20:09:49 2013 +0200
     3.3 @@ -0,0 +1,47 @@
     3.4 +This is a Quickcheck tool for Isabelle's ML environment.
     3.5 +
     3.6 +Authors
     3.7 +
     3.8 +  Lukas Bulwahn
     3.9 +  Nicolai Schaffroth
    3.10 +
    3.11 +Quick Usage
    3.12 +
    3.13 +  - Import Spec_Check.thy in your development
    3.14 +  - Look at examples in Examples.thy
    3.15 +  - write specifications with the ML function
    3.16 +      Spec_Check.check_property @{context} "ALL x. P x"
    3.17 +
    3.18 +Notes
    3.19 +
    3.20 +Our specification-based testing tool originated from Christopher League's
    3.21 +QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
    3.22 +provides a rich and uniform ML platform (called Isabelle/ML), this
    3.23 +testing tools is very different than the one for a typical ML developer.
    3.24 +
    3.25 +1. Isabelle/ML provides common data structures, which we can use in the
    3.26 +tool's implementation for storing data and printing output.
    3.27 +
    3.28 +2. The implementation in Isabelle that will be checked with this tool
    3.29 +commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
    3.30 +but they do not use other integer types in ML, such as ML's Int.int,
    3.31 +Word.word and others.
    3.32 +
    3.33 +3. As Isabelle can run heavily in parallel, we avoid reference types.
    3.34 +
    3.35 +4. Isabelle has special naming conventions and documentation of source
    3.36 +code is only minimal to avoid parroting.
    3.37 +
    3.38 +Next steps:
    3.39 +  - Remove all references and store the neccessary random seed in the
    3.40 +    Isabelle's context.
    3.41 +  - Simplify some existing random generators.
    3.42 +    The original ones from Christopher League are so complicated to
    3.43 +    support many integer types uniformly.
    3.44 +
    3.45 +License
    3.46 +
    3.47 +  The source code originated from Christopher League's QCheck, which is
    3.48 +  licensed under the 2-clause BSD license. The current source code is
    3.49 +  licensed under the compatible 3-clause BSD license of Isabelle.
    3.50 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Spec_Check/Spec_Check.thy	Thu May 30 20:09:49 2013 +0200
     4.3 @@ -0,0 +1,15 @@
     4.4 +theory Spec_Check
     4.5 +imports Main
     4.6 +begin
     4.7 +
     4.8 +ML_file "random.ML"
     4.9 +ML_file "property.ML"
    4.10 +ML_file "base_generator.ML"
    4.11 +ML_file "generator.ML"
    4.12 +ML_file "gen_construction.ML"
    4.13 +ML_file "spec_check.ML"
    4.14 +ML_file "output_style.ML"
    4.15 +
    4.16 +setup {* Perl_Style.setup #> CMStyle.setup *}
    4.17 +
    4.18 +end
    4.19 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Spec_Check/base_generator.ML	Thu May 30 20:09:49 2013 +0200
     5.3 @@ -0,0 +1,201 @@
     5.4 +(*  Title:      HOL/Spec_Check/base_generator.ML
     5.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     5.6 +    Author:     Christopher League
     5.7 +
     5.8 +Basic random generators.
     5.9 +*)
    5.10 +
    5.11 +signature BASE_GENERATOR =
    5.12 +sig
    5.13 +
    5.14 +type rand
    5.15 +type 'a gen = rand -> 'a * rand
    5.16 +type ('a, 'b) co = 'a -> 'b gen -> 'b gen
    5.17 +
    5.18 +val new : unit -> rand
    5.19 +val range : int * int -> rand -> int * rand
    5.20 +type ('a, 'b) reader = 'b -> ('a * 'b) option
    5.21 +
    5.22 +val lift : 'a -> 'a gen
    5.23 +val select : 'a vector -> 'a gen
    5.24 +val choose : 'a gen vector -> 'a gen
    5.25 +val choose' : (int * 'a gen) vector -> 'a gen
    5.26 +val selectL : 'a list -> 'a gen
    5.27 +val chooseL : 'a gen list -> 'a gen
    5.28 +val chooseL' : (int * 'a gen) list -> 'a gen
    5.29 +val filter : ('a -> bool) -> 'a gen -> 'a gen
    5.30 +
    5.31 +val zip : ('a gen * 'b gen) -> ('a * 'b) gen
    5.32 +val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
    5.33 +val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
    5.34 +val map : ('a -> 'b) -> 'a gen -> 'b gen
    5.35 +val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
    5.36 +val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
    5.37 +val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
    5.38 +
    5.39 +val flip : bool gen
    5.40 +val flip' : int * int -> bool gen
    5.41 +
    5.42 +val list : bool gen -> 'a gen -> 'a list gen
    5.43 +val option : bool gen -> 'a gen -> 'a option gen
    5.44 +val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
    5.45 +
    5.46 +val variant : (int, 'b) co
    5.47 +val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
    5.48 +val cobool : (bool, 'b) co
    5.49 +val colist : ('a, 'b) co -> ('a list, 'b) co
    5.50 +val coopt : ('a, 'b) co -> ('a option, 'b) co
    5.51 +
    5.52 +type stream
    5.53 +val start : rand -> stream
    5.54 +val limit : int -> 'a gen -> ('a, stream) reader
    5.55 +
    5.56 +end
    5.57 +
    5.58 +structure Base_Generator : BASE_GENERATOR =
    5.59 +struct
    5.60 +
    5.61 +(* random number engine *)
    5.62 +
    5.63 +type rand = real
    5.64 +
    5.65 +val a = 16807.0
    5.66 +val m = 2147483647.0
    5.67 +
    5.68 +fun nextrand seed =
    5.69 +  let
    5.70 +    val t = a * seed
    5.71 +  in
    5.72 +    t - m * real (floor (t / m))
    5.73 +  end
    5.74 +
    5.75 +val new = nextrand o Time.toReal o Time.now
    5.76 +
    5.77 +fun range (min, max) =
    5.78 +  if min > max then raise Domain (* TODO: raise its own error *)
    5.79 +  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
    5.80 +
    5.81 +fun split r =
    5.82 +  let
    5.83 +    val r = r / a
    5.84 +    val r0 = real (floor r)
    5.85 +    val r1 = r - r0
    5.86 +  in
    5.87 +    (nextrand r0, nextrand r1)
    5.88 +  end
    5.89 +
    5.90 +(* generators *)
    5.91 +
    5.92 +type 'a gen = rand -> 'a * rand
    5.93 +type ('a, 'b) reader = 'b -> ('a * 'b) option
    5.94 +
    5.95 +fun lift obj r = (obj, r)
    5.96 +
    5.97 +local open Vector (* Isabelle does not use vectors? *)
    5.98 +      fun explode ((freq, gen), acc) =
    5.99 +          List.tabulate (freq, fn _ => gen) @ acc
   5.100 +in fun choose v r =
   5.101 +       let val (i, r) = range(0, length v - 1) r
   5.102 +        in sub (v, i) r
   5.103 +       end
   5.104 +   fun choose' v = choose (fromList (foldr explode nil v))
   5.105 +   fun select v = choose (map lift v)
   5.106 +end
   5.107 +
   5.108 +fun chooseL l = choose (Vector.fromList l)
   5.109 +fun chooseL' l = choose' (Vector.fromList l)
   5.110 +fun selectL l = select (Vector.fromList l)
   5.111 +
   5.112 +fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
   5.113 +
   5.114 +fun zip3 (g1, g2, g3) =
   5.115 +  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
   5.116 +
   5.117 +fun zip4 (g1, g2, g3, g4) =
   5.118 +  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
   5.119 +
   5.120 +fun map f g = apfst f o g
   5.121 +
   5.122 +fun map2 f = map f o zip
   5.123 +fun map3 f = map f o zip3
   5.124 +fun map4 f = map f o zip4
   5.125 +
   5.126 +fun filter p gen r =
   5.127 +  let
   5.128 +    fun loop (x, r) = if p x then (x, r) else loop (gen r)
   5.129 +  in
   5.130 +    loop (gen r)
   5.131 +  end
   5.132 +
   5.133 +val flip = selectL [true, false]
   5.134 +fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
   5.135 +
   5.136 +fun list flip g r =
   5.137 +  case flip r of
   5.138 +      (true, r) => (nil, r)
   5.139 +    | (false, r) =>
   5.140 +      let
   5.141 +        val (x,r) = g r
   5.142 +        val (xs,r) = list flip g r
   5.143 +      in (x::xs, r) end
   5.144 +
   5.145 +fun option flip g r =
   5.146 +  case flip r of
   5.147 +    (true, r) => (NONE, r)
   5.148 +  | (false, r) => map SOME g r
   5.149 +
   5.150 +fun vector tabulate (int, elem) r =
   5.151 +  let
   5.152 +    val (n, r) = int r
   5.153 +    val p = Unsynchronized.ref r
   5.154 +    fun g _ =
   5.155 +      let
   5.156 +        val (x,r) = elem(!p)
   5.157 +      in x before p := r end
   5.158 +  in
   5.159 +    (tabulate(n, g), !p)
   5.160 +  end
   5.161 +
   5.162 +type stream = rand Unsynchronized.ref * int
   5.163 +
   5.164 +fun start r = (Unsynchronized.ref r, 0)
   5.165 +
   5.166 +fun limit max gen =
   5.167 +  let
   5.168 +    fun next (p, i) =
   5.169 +      if i >= max then NONE
   5.170 +      else
   5.171 +        let val (x, r) = gen(!p)
   5.172 +        in SOME(x, (p, i+1)) before p := r end
   5.173 +  in
   5.174 +    next
   5.175 +  end
   5.176 +
   5.177 +type ('a, 'b) co = 'a -> 'b gen -> 'b gen
   5.178 +
   5.179 +fun variant v g r =
   5.180 +  let
   5.181 +    fun nth (i, r) =
   5.182 +      let val (r1, r2) = split r
   5.183 +      in if i = 0 then r1 else nth (i-1, r2) end
   5.184 +  in
   5.185 +    g (nth (v, r))
   5.186 +  end
   5.187 +
   5.188 +fun arrow (cogen, gen) r =
   5.189 +  let
   5.190 +    val (r1, r2) = split r
   5.191 +    fun g x = fst (cogen x gen r1)
   5.192 +  in (g, r2) end
   5.193 +
   5.194 +fun cobool false = variant 0
   5.195 +  | cobool true = variant 1
   5.196 +
   5.197 +fun colist _ [] = variant 0
   5.198 +  | colist co (x::xs) = variant 1 o co x o colist co xs
   5.199 +
   5.200 +fun coopt _ NONE = variant 0
   5.201 +  | coopt co (SOME x) = variant 1 o co x
   5.202 +
   5.203 +end
   5.204 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 20:09:49 2013 +0200
     6.3 @@ -0,0 +1,171 @@
     6.4 +(*  Title:      HOL/Spec_Check/gen_construction.ML
     6.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     6.6 +    Author:     Christopher League
     6.7 +
     6.8 +Constructing generators and pretty printing function for complex types.
     6.9 +*)
    6.10 +
    6.11 +signature GEN_CONSTRUCTION =
    6.12 +sig
    6.13 +  val register : string * (string * string) -> theory -> theory
    6.14 +  type mltype
    6.15 +  val parse_pred : string -> string * mltype;
    6.16 +  val build_check : theory -> string -> mltype * string -> string
    6.17 +  (*val safe_check : string -> mltype * string -> string*)
    6.18 +  val string_of_bool : bool -> string
    6.19 +  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
    6.20 +end;
    6.21 +
    6.22 +structure Gen_Construction : GEN_CONSTRUCTION =
    6.23 +struct
    6.24 +
    6.25 +(* Parsing ML types *)
    6.26 +
    6.27 +datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
    6.28 +
    6.29 +(*Split string into tokens for parsing*)
    6.30 +fun split s =
    6.31 +  let
    6.32 +    fun split_symbol #"(" = "( "
    6.33 +      | split_symbol #")" = " )"
    6.34 +      | split_symbol #"," = " ,"
    6.35 +      | split_symbol #":" = " :"
    6.36 +      | split_symbol c = Char.toString c
    6.37 +    fun is_space c = c = #" "
    6.38 +  in String.tokens is_space (String.translate split_symbol s) end;
    6.39 +
    6.40 +(*Accept anything that is not a recognized symbol*)
    6.41 +val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
    6.42 +
    6.43 +(*Turn a type list into a nested Con*)
    6.44 +fun make_con nil = raise Empty
    6.45 +  | make_con [c] = c
    6.46 +  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
    6.47 +
    6.48 +(*Parse a type*)
    6.49 +fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
    6.50 +
    6.51 +and parse_type_arg s = (parse_tuple || parse_type_single) s
    6.52 +
    6.53 +and parse_type_single s = (parse_con || parse_type_basic) s
    6.54 +
    6.55 +and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
    6.56 +
    6.57 +and parse_list s =
    6.58 +  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
    6.59 +
    6.60 +and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
    6.61 +
    6.62 +and parse_con s = ((parse_con_nest
    6.63 +  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
    6.64 +  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
    6.65 +  >> (make_con o rev)) s
    6.66 +
    6.67 +and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, nil)))) s
    6.68 +
    6.69 +and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
    6.70 +
    6.71 +and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
    6.72 +  >> (fn (t, tl) => Tuple (t :: tl))) s;
    6.73 +
    6.74 +(*Parses entire type + name*)
    6.75 +fun parse_function s =
    6.76 +  let
    6.77 +    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
    6.78 +    val (name, ty) = p (split s)
    6.79 +    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
    6.80 +    val (typ, _) = Scan.finite stop parse_type ty
    6.81 +  in (name, typ) end;
    6.82 +
    6.83 +(*Creates desired output*)
    6.84 +fun parse_pred s =
    6.85 +  let
    6.86 +    val (name, Con ("->", t :: _)) = parse_function s
    6.87 +  in (name, t) end;
    6.88 +
    6.89 +(* Construct Generators and Pretty Printers *)
    6.90 +
    6.91 +(*copied from smt_config.ML *)
    6.92 +fun string_of_bool b = if b then "true" else "false"
    6.93 +
    6.94 +fun string_of_ref f r = f (!r) ^ " ref";
    6.95 +
    6.96 +val initial_content = Symtab.make
    6.97 +  [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
    6.98 +  ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
    6.99 +  ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
   6.100 +  ("unit", ("gen_unit", "fn () => \"()\"")),
   6.101 +  ("int", ("Generator.int", "string_of_int")),
   6.102 +  ("real", ("Generator.real", "string_of_real")),
   6.103 +  ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
   6.104 +  ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
   6.105 +  ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
   6.106 +  ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
   6.107 +  ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
   6.108 +
   6.109 +structure Data = Theory_Data
   6.110 +(
   6.111 +  type T = (string * string) Symtab.table
   6.112 +  val empty = initial_content
   6.113 +  val extend = I
   6.114 +  fun merge data : T = Symtab.merge (K true) data
   6.115 +)
   6.116 +
   6.117 +fun data_of thy tycon = case Symtab.lookup (Data.get thy) tycon of SOME data => data
   6.118 +  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon)
   6.119 +
   6.120 +val generator_of = fst oo data_of
   6.121 +val printer_of = snd oo data_of
   6.122 +
   6.123 +fun register (ty, data) = Data.map (Symtab.update (ty, data))
   6.124 +
   6.125 +(*
   6.126 +fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
   6.127 +*)
   6.128 +
   6.129 +fun combine dict [] = dict
   6.130 +  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
   6.131 +
   6.132 +fun compose_generator _ Var = "Generator.int"
   6.133 +  | compose_generator thy (Con (s, types)) =
   6.134 +      combine (generator_of thy s) (map (compose_generator thy) types)
   6.135 +  | compose_generator thy (Tuple t) =
   6.136 +    let
   6.137 +      fun tuple_body t = space_implode ""
   6.138 +        (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
   6.139 +        compose_generator thy ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
   6.140 +      fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
   6.141 +    in "fn r0 => let " ^ tuple_body t ^
   6.142 +      "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" end;
   6.143 +
   6.144 +fun compose_printer _ Var = "Int.toString"
   6.145 +  | compose_printer thy (Con (s, types)) =
   6.146 +      combine (printer_of thy s) (map (compose_printer thy) types)
   6.147 +  | compose_printer thy (Tuple t) =
   6.148 +    let
   6.149 +      fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
   6.150 +      fun tuple_body t = space_implode " ^ \", \" ^ "
   6.151 +        (map (fn (ty, n) => "(" ^ compose_printer thy ty ^ ") x" ^ string_of_int n)
   6.152 +        (t ~~ (1 upto (length t))))
   6.153 +    in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
   6.154 +
   6.155 +(*produces compilable string*)
   6.156 +fun build_check thy name (ty, spec) = "Spec_Check.checkGen (ML_Context.the_generic_context ()) ("
   6.157 +  ^ compose_generator thy ty ^ ", SOME (" ^ compose_printer thy ty ^ ")) (\""
   6.158 +  ^ name ^ "\", Property.pred (" ^ spec ^ "));";
   6.159 +
   6.160 +(*produces compilable string - non-eqtype functions*)
   6.161 +(*
   6.162 +fun safe_check name (ty, spec) =
   6.163 +  let
   6.164 +    val default = case AList.lookup (op =) (!gen_table) "->"
   6.165 +      of NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
   6.166 +      | SOME entry => entry
   6.167 +  in (gen_table := AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\""))
   6.168 +   (!gen_table);
   6.169 +    build_check name (ty, spec) before
   6.170 +    gen_table := AList.update (op =) ("->", default) (!gen_table)) end;
   6.171 +*)
   6.172 +
   6.173 +end;
   6.174 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Spec_Check/generator.ML	Thu May 30 20:09:49 2013 +0200
     7.3 @@ -0,0 +1,231 @@
     7.4 +(*  Title:      HOL/Spec_Check/generator.ML
     7.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     7.6 +    Author:     Christopher League
     7.7 +
     7.8 +Random generators for Isabelle/ML's types.
     7.9 +*)
    7.10 +
    7.11 +signature GENERATOR = sig
    7.12 +  include BASE_GENERATOR
    7.13 +  (* text generators *)
    7.14 +  val char : char gen
    7.15 +  val charRange : char * char -> char gen
    7.16 +  val charFrom : string -> char gen
    7.17 +  val charByType : (char -> bool) -> char gen
    7.18 +  val string : (int gen * char gen) -> string gen
    7.19 +  val substring : string gen -> substring gen
    7.20 +  val cochar : (char, 'b) co
    7.21 +  val costring : (string, 'b) co
    7.22 +  val cosubstring : (substring, 'b) co
    7.23 +  (* integer generators *)
    7.24 +  val int : int gen
    7.25 +  val int_pos : int gen
    7.26 +  val int_neg : int gen
    7.27 +  val int_nonpos : int gen
    7.28 +  val int_nonneg : int gen
    7.29 +  val coint : (int, 'b) co
    7.30 +  (* real generators *)
    7.31 +  val real : real gen
    7.32 +  val real_frac : real gen
    7.33 +  val real_pos : real gen
    7.34 +  val real_neg : real gen
    7.35 +  val real_nonpos : real gen
    7.36 +  val real_nonneg : real gen
    7.37 +  val real_finite : real gen
    7.38 +  (* function generators *)
    7.39 +  val function_const : 'c * 'b gen -> ('a -> 'b) gen
    7.40 +  val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
    7.41 +  val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
    7.42 +  val unit : unit gen
    7.43 +  val ref' : 'a gen -> 'a Unsynchronized.ref gen
    7.44 +  (* more generators *)
    7.45 +  val term : int -> term gen
    7.46 +  val typ : int -> typ gen
    7.47 +
    7.48 +  val stream : stream
    7.49 +end
    7.50 +
    7.51 +structure Generator : GENERATOR =
    7.52 +struct
    7.53 +
    7.54 +open Base_Generator
    7.55 +
    7.56 +val stream = start (new())
    7.57 +
    7.58 +type 'a gen = rand -> 'a * rand
    7.59 +type ('a, 'b) co = 'a -> 'b gen -> 'b gen
    7.60 +
    7.61 +(* text *)
    7.62 +
    7.63 +open Text
    7.64 +type char = Char.char
    7.65 +type string = String.string
    7.66 +type substring = Substring.substring
    7.67 +
    7.68 +
    7.69 +val char = map Char.chr (range (0, Char.maxOrd))
    7.70 +fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
    7.71 +
    7.72 +fun charFrom s =
    7.73 +  choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
    7.74 +
    7.75 +fun charByType p = filter p char
    7.76 +
    7.77 +val string = vector CharVector.tabulate
    7.78 +
    7.79 +fun substring gen r =
    7.80 +    let val (s, r') = gen r
    7.81 +        val (i, r'') = range (0, String.size s) r'
    7.82 +        val (j, r''') = range (0, String.size s - i) r''
    7.83 +    in
    7.84 +      (Substring.substring (s, i, j), r''')
    7.85 +    end
    7.86 +
    7.87 +fun cochar c =
    7.88 +  if Char.ord c = 0 then variant 0
    7.89 +  else variant 1 o cochar (Char.chr (Char.ord c div 2))
    7.90 +
    7.91 +fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
    7.92 +
    7.93 +fun costring s = cosubstring (Substring.full s)
    7.94 +
    7.95 +(* integers *)
    7.96 +val digit = charRange (#"0", #"9")
    7.97 +val nonzero = string (lift 1, charRange (#"1", #"9"))
    7.98 +fun digits' n = string (range (0, n-1), digit)
    7.99 +fun digits n = map2 op^ (nonzero, digits' n)
   7.100 +
   7.101 +val maxDigits = 64
   7.102 +val ratio = 49
   7.103 +
   7.104 +fun pos_or_neg f r =
   7.105 +  let
   7.106 +    val (s, r') = digits maxDigits r
   7.107 +  in (f (the (Int.fromString s)), r') end
   7.108 +
   7.109 +val int_pos = pos_or_neg I
   7.110 +val int_neg = pos_or_neg Int.~
   7.111 +val zero = lift 0
   7.112 +
   7.113 +val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
   7.114 +val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
   7.115 +val int = chooseL [int_nonneg, int_nonpos]
   7.116 +
   7.117 +fun coint n =
   7.118 +  if n = 0 then variant 0
   7.119 +  else if n < 0 then variant 1 o coint (~ n)
   7.120 +  else variant 2 o coint (n div 2)
   7.121 +
   7.122 +(* reals *)
   7.123 +val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
   7.124 +
   7.125 +fun real_frac r =
   7.126 +  let val (s, r') = digits r
   7.127 +  in (the (Real.fromString s), r') end
   7.128 +
   7.129 +val {exp=minExp,...} = Real.toManExp Real.minPos
   7.130 +val {exp=maxExp,...} = Real.toManExp Real.posInf
   7.131 +
   7.132 +val ratio = 99
   7.133 +
   7.134 +fun mk r =
   7.135 +  let
   7.136 +    val (a, r') = digits r
   7.137 +    val (b, r'') = digits r'
   7.138 +    val (e, r''') = range (minExp div 4, maxExp div 4) r''
   7.139 +    val x = String.concat [a, ".", b, "E", Int.toString e]
   7.140 +  in
   7.141 +    (the (Real.fromString x), r''')
   7.142 +  end
   7.143 +
   7.144 +val real_pos = chooseL' (List.map ((pair 1) o lift)
   7.145 +    [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
   7.146 +
   7.147 +val real_neg = map Real.~ real_pos
   7.148 +
   7.149 +val real_zero = Real.fromInt 0
   7.150 +val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
   7.151 +val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
   7.152 +
   7.153 +val real = chooseL [real_nonneg, real_nonpos]
   7.154 +
   7.155 +val real_finite = filter Real.isFinite real
   7.156 +
   7.157 +(*alternate list generator - uses an integer generator to determine list length*)
   7.158 +fun list' int gen = vector List.tabulate (int, gen);
   7.159 +
   7.160 +(* more function generators *)
   7.161 +
   7.162 +fun function_const (_, gen2) r =
   7.163 +  let
   7.164 +    val (v, r') = gen2 r
   7.165 +  in (fn _ => v, r') end;
   7.166 +
   7.167 +fun function_strict size (gen1, gen2) r =
   7.168 +  let
   7.169 +    val (def, r') = gen2 r
   7.170 +    val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
   7.171 +  in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
   7.172 +
   7.173 +fun function_lazy (gen1, gen2) r =
   7.174 +  let
   7.175 +    val (initial1, r') = gen1 r
   7.176 +    val (initial2, internal) = gen2 r'
   7.177 +    val seed = Unsynchronized.ref internal
   7.178 +    val table = Unsynchronized.ref [(initial1, initial2)]
   7.179 +    fun new_entry k =
   7.180 +      let
   7.181 +        val (new_val, new_seed) = gen2 (!seed)
   7.182 +        val _ =  seed := new_seed
   7.183 +        val _ = table := AList.update (op =) (k, new_val) (!table)
   7.184 +      in new_val end
   7.185 +  in (fn v1 => case AList.lookup (op =) (!table) v1 of
   7.186 +    NONE => new_entry v1 | SOME v2 => v2, r') end;
   7.187 +
   7.188 +(* unit *)
   7.189 +
   7.190 +fun unit r = ((), r);
   7.191 +
   7.192 +(* references *)
   7.193 +
   7.194 +fun ref' gen r =
   7.195 +  let val (value, r') = gen r
   7.196 +  in (Unsynchronized.ref value, r') end;
   7.197 +
   7.198 +(* types and terms *)
   7.199 +
   7.200 +val sort_string = selectL ["sort1", "sort2", "sort3"];
   7.201 +val type_string = selectL ["TCon1", "TCon2", "TCon3"];
   7.202 +val tvar_string = selectL ["a", "b", "c"];
   7.203 +
   7.204 +val const_string = selectL ["c1", "c2", "c3"];
   7.205 +val var_string = selectL ["x", "y", "z"];
   7.206 +val index = selectL [0, 1, 2, 3];
   7.207 +val bound_index = selectL [0, 1, 2, 3];
   7.208 +
   7.209 +val sort = list (flip' (1, 2)) sort_string;
   7.210 +
   7.211 +fun typ n =
   7.212 +  let
   7.213 +    fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
   7.214 +    val tfree = map TFree (zip (tvar_string, sort))
   7.215 +    val tvar = map TVar (zip (zip (tvar_string, index), sort))
   7.216 +  in
   7.217 +    if n = 0 then chooseL [tfree, tvar]
   7.218 +    else chooseL [type' (n div 2), tfree, tvar]
   7.219 +  end;
   7.220 +
   7.221 +fun term n =
   7.222 +  let
   7.223 +    val const = map Const (zip (const_string, typ 10))
   7.224 +    val free = map Free (zip (var_string, typ 10))
   7.225 +    val var = map Var (zip (zip (var_string, index), typ 10))
   7.226 +    val bound = map Bound bound_index
   7.227 +    fun abs m = map Abs (zip3 (var_string, typ 10, term m))
   7.228 +    fun app m = map (op $) (zip (term m, term m))
   7.229 +  in
   7.230 +    if n = 0 then chooseL [const, free, var, bound]
   7.231 +    else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
   7.232 +  end;
   7.233 +
   7.234 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Spec_Check/output_style.ML	Thu May 30 20:09:49 2013 +0200
     8.3 @@ -0,0 +1,117 @@
     8.4 +(*  Title:      HOL/Spec_Check/output_style.ML
     8.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     8.6 +    Author:     Christopher League
     8.7 +
     8.8 +Output styles for presenting Spec_Check's results.
     8.9 +*)
    8.10 +
    8.11 +structure Perl_Style =
    8.12 +struct
    8.13 +
    8.14 +local
    8.15 +
    8.16 +open StringCvt
    8.17 +
    8.18 +fun new ctxt tag =
    8.19 +  let
    8.20 +    val target = Config.get_generic ctxt Spec_Check.gen_target
    8.21 +    val namew = Config.get_generic ctxt Spec_Check.column_width
    8.22 +    val sort_examples = Config.get_generic ctxt Spec_Check.sort_examples
    8.23 +    val show_stats = Config.get_generic ctxt Spec_Check.show_stats
    8.24 +    val limit = Config.get_generic ctxt Spec_Check.examples
    8.25 +
    8.26 +    val resultw = 8
    8.27 +    val countw = 20
    8.28 +    val allw = namew + resultw + countw + 2
    8.29 +
    8.30 +    val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
    8.31 +
    8.32 +    fun result ({count=0,...}, _) _ = "dubious"
    8.33 +      | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
    8.34 +      | result ({count,tags,...}, badobjs) true = if not (null badobjs) then "FAILED"
    8.35 +          else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" else "ok"
    8.36 +
    8.37 +    fun ratio (0, _) = "(0/0 passed)"
    8.38 +      | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
    8.39 +      | ratio (count, n) = "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
    8.40 +
    8.41 +    fun update (stats, badobjs) donep =
    8.42 +      "\r" ^ (padRight #"." namew tag) ^ "." ^ (padRight #" " resultw (result (stats, badobjs) donep))
    8.43 +      ^ (padRight #" " countw (ratio (#count stats, length badobjs)))
    8.44 +
    8.45 +    fun status (_, result, (stats, badobjs)) =
    8.46 +      if Property.failure result then Output.writeln (update (stats, badobjs) false) else ()
    8.47 +
    8.48 +    fun prtag count (tag, n) first =
    8.49 +      if String.isPrefix "__" tag then ("", first)
    8.50 +      else
    8.51 +         let
    8.52 +           val ratio = round ((real n / real count) * 100.0)
    8.53 +         in
    8.54 +           (((if first then "" else padRight #" " allw "\n") ^
    8.55 +             padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
    8.56 +           false)
    8.57 +         end
    8.58 +
    8.59 +    fun prtags ({count, tags, ...} : Property.stats) =
    8.60 +      if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
    8.61 +
    8.62 +    fun err badobjs =
    8.63 +      let
    8.64 +        fun iter [] _ = ()
    8.65 +          | iter (e :: es) k =
    8.66 +              (Output.writeln (padLeft #" " namew (if k > 0 then "" else "counter-examples")
    8.67 +                ^ padRight #" " resultw (if k > 0 then "" else ":") ^ e);
    8.68 +              iter es (k + 1))
    8.69 +      in
    8.70 +        iter (maybe_sort (take limit (map_filter I badobjs))) 0
    8.71 +      end
    8.72 +
    8.73 +    fun finish (stats, badobjs) =
    8.74 +      if null badobjs then Output.writeln (update (stats, badobjs) true ^ prtags stats)
    8.75 +      else (Output.writeln (update (stats, badobjs) true); err badobjs)
    8.76 +  in
    8.77 +    {status=status, finish=finish}
    8.78 +  end
    8.79 +
    8.80 +in
    8.81 +  val setup = Spec_Check.register_style ("Perl", new)
    8.82 +end
    8.83 +
    8.84 +end
    8.85 +
    8.86 +(* CM style: meshes with CM output; highlighted in sml-mode *)
    8.87 +
    8.88 +structure CMStyle =
    8.89 +struct
    8.90 +
    8.91 +local
    8.92 +
    8.93 +fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
    8.94 +
    8.95 +fun new ctxt tag =
    8.96 +  let
    8.97 +    val gen_target = Config.get_generic ctxt Spec_Check.gen_target
    8.98 +    val _ = Output.writeln ("[testing " ^ tag ^ "... ") (* TODO: Output without line break *)
    8.99 +    fun finish ({count, ...}, badobjs) = case (count, badobjs) of
   8.100 +        (0, []) => Output.writeln ("no valid cases generated]")
   8.101 +      | (n, []) => Output.writeln (
   8.102 +            if n >= gen_target then "ok]"
   8.103 +            else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
   8.104 +      | (_, es) =>
   8.105 +        let
   8.106 +          val wd = size (string_of_int (length es))
   8.107 +          fun each (NONE, _) = ()
   8.108 +            | each (SOME e, i) = Output.writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
   8.109 +         in
   8.110 +           (Output.writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ())
   8.111 +         end
   8.112 +  in
   8.113 +    {status = K (), finish = finish}
   8.114 +  end
   8.115 +
   8.116 +in
   8.117 +  val setup = Spec_Check.register_style ("CM", new)
   8.118 +end
   8.119 +
   8.120 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Spec_Check/property.ML	Thu May 30 20:09:49 2013 +0200
     9.3 @@ -0,0 +1,73 @@
     9.4 +(*  Title:      HOL/Spec_Check/property.ML
     9.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     9.6 +    Author:     Christopher League
     9.7 +
     9.8 +Conditional properties that can track argument distribution.
     9.9 +*)
    9.10 +
    9.11 +signature PROPERTY =
    9.12 +sig
    9.13 +
    9.14 +type 'a pred = 'a -> bool
    9.15 +type 'a prop
    9.16 +val pred : 'a pred -> 'a prop
    9.17 +val pred2 : ('a * 'b) pred -> 'b -> 'a  prop
    9.18 +val implies : 'a pred * 'a prop -> 'a prop
    9.19 +val ==> : 'a pred * 'a pred -> 'a prop
    9.20 +val trivial : 'a pred -> 'a prop -> 'a prop
    9.21 +val classify : 'a pred -> string -> 'a prop -> 'a prop
    9.22 +val classify' : ('a -> string option) -> 'a prop -> 'a prop
    9.23 +
    9.24 +(*Results*)
    9.25 +type result = bool option
    9.26 +type stats = { tags : (string * int) list, count : int }
    9.27 +val test : 'a prop -> 'a * stats -> result * stats
    9.28 +val stats : stats
    9.29 +val success : result pred
    9.30 +val failure : result pred
    9.31 +
    9.32 +end
    9.33 +
    9.34 +structure Property : PROPERTY =
    9.35 +struct
    9.36 +
    9.37 +type result = bool option
    9.38 +type stats = { tags : (string * int) list, count : int }
    9.39 +type 'a pred = 'a -> bool
    9.40 +type 'a prop = 'a * stats -> result * stats
    9.41 +
    9.42 +fun success (SOME true) = true
    9.43 +  | success _ = false
    9.44 +
    9.45 +fun failure (SOME false) = true
    9.46 +  | failure _ = false
    9.47 +
    9.48 +fun apply f x = SOME (f x) handle _ => SOME false (* TODO: do not catch all exceptions! *)
    9.49 +fun pred f (x,s) = (apply f x, s)
    9.50 +fun pred2 f z = pred (fn x => f (x, z))
    9.51 +
    9.52 +fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
    9.53 +
    9.54 +fun ==> (p1, p2) = implies (p1, pred p2)
    9.55 +
    9.56 +fun wrap trans p (x,s) =
    9.57 +  let val (result,s) = p (x,s)
    9.58 +  in (result, trans (x, result, s)) end
    9.59 +
    9.60 +fun classify' f =
    9.61 +  wrap (fn (x, result, {tags, count}) =>
    9.62 +    { tags = if is_some result then
    9.63 +        case f x of NONE => tags | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags
    9.64 +      else tags, count = count })
    9.65 +
    9.66 +fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
    9.67 +
    9.68 +fun trivial cond = classify cond "trivial"
    9.69 +
    9.70 +fun test p =
    9.71 +  wrap (fn (_, result, {tags, count}) =>
    9.72 +    { tags = tags, count = if is_some result then count + 1 else count }) p
    9.73 +
    9.74 +val stats = { tags = [], count = 0 }
    9.75 +
    9.76 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Spec_Check/random.ML	Thu May 30 20:09:49 2013 +0200
    10.3 @@ -0,0 +1,46 @@
    10.4 +(*  Title:      HOL/Spec_Check/random.ML
    10.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    10.6 +    Author:     Christopher League
    10.7 +
    10.8 +Random number engine.
    10.9 +*)
   10.10 +
   10.11 +signature RANDOM =
   10.12 +sig
   10.13 +  type rand
   10.14 +  val new : unit -> rand
   10.15 +  val range : int * int -> rand -> int * rand
   10.16 +  val split : rand -> rand * rand
   10.17 +end
   10.18 +
   10.19 +structure Random : RANDOM  =
   10.20 +struct
   10.21 +
   10.22 +type rand = real
   10.23 +
   10.24 +val a = 16807.0
   10.25 +val m = 2147483647.0
   10.26 +
   10.27 +fun nextrand seed =
   10.28 +  let
   10.29 +    val t = a * seed
   10.30 +  in
   10.31 +    t - m * real(floor(t/m))
   10.32 +  end
   10.33 +
   10.34 +val new = nextrand o Time.toReal o Time.now
   10.35 +
   10.36 +fun range (min, max) =
   10.37 +  if min > max then raise Domain (* TODO: raise its own error *)
   10.38 +  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
   10.39 +
   10.40 +fun split r =
   10.41 +  let
   10.42 +    val r = r / a
   10.43 +    val r0 = real(floor r)
   10.44 +    val r1 = r - r0
   10.45 +  in
   10.46 +    (nextrand r0, nextrand r1)
   10.47 +  end
   10.48 +
   10.49 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 20:09:49 2013 +0200
    11.3 @@ -0,0 +1,190 @@
    11.4 +(*  Title:      HOL/Spec_Check/spec_check.ML
    11.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    11.6 +    Author:     Christopher League
    11.7 +
    11.8 +Specification-based testing of ML programs with random values.
    11.9 +*)
   11.10 +
   11.11 +signature SPEC_CHECK =
   11.12 +sig
   11.13 +
   11.14 +  val gen_target : int Config.T
   11.15 +  val gen_max : int Config.T
   11.16 +  val examples : int Config.T
   11.17 +  val sort_examples : bool Config.T
   11.18 +  val show_stats : bool Config.T
   11.19 +  val column_width : int Config.T
   11.20 +  val style : string Config.T
   11.21 +
   11.22 +  type output_style = Context.generic -> string ->
   11.23 +    {status : string option * Property.result * (Property.stats  * string option list) -> unit, finish: Property.stats * string option list -> unit}
   11.24 +
   11.25 +  val register_style : (string * output_style) -> theory -> theory
   11.26 +
   11.27 +  val checkGen : Context.generic -> 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
   11.28 +
   11.29 +  val check_property : Proof.context -> string -> unit
   11.30 +end;
   11.31 +
   11.32 +structure Spec_Check : SPEC_CHECK =
   11.33 +struct
   11.34 +
   11.35 +(* configurations *)
   11.36 +
   11.37 +val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
   11.38 +val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
   11.39 +val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
   11.40 +
   11.41 +val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
   11.42 +val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
   11.43 +val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
   11.44 +val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
   11.45 +
   11.46 +open Property
   11.47 +
   11.48 +type ('a, 'b) reader = 'b -> ('a * 'b) option
   11.49 +type 'a rep = ('a -> string) option
   11.50 +
   11.51 +type output_style = Context.generic -> string ->
   11.52 +  {status: string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit}
   11.53 +
   11.54 +fun limit ctxt gen = Generator.limit (Config.get_generic ctxt gen_max) gen
   11.55 +
   11.56 +structure Style = Theory_Data
   11.57 +(
   11.58 +  type T = output_style Symtab.table
   11.59 +  val empty = Symtab.empty
   11.60 +  val extend = I
   11.61 +  fun merge data : T = Symtab.merge (K true) data
   11.62 +)
   11.63 +
   11.64 +fun get_style ctxt =
   11.65 +  let val name = Config.get_generic ctxt style
   11.66 +  in case Symtab.lookup (Style.get (Context.theory_of ctxt)) name of
   11.67 +      SOME style => style ctxt
   11.68 +    | NONE => error ("No style called " ^ quote name ^ " found")
   11.69 +  end
   11.70 +
   11.71 +fun register_style (name, style) = Style.map (Symtab.update (name, style))
   11.72 +
   11.73 +(* testing functions *)
   11.74 +
   11.75 +fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
   11.76 +  let
   11.77 +    val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
   11.78 +
   11.79 +    val {status, finish} = get_style ctxt tag
   11.80 +    fun status' (obj, result, (stats, badobjs)) =
   11.81 +      let
   11.82 +        val badobjs' = if Property.failure result then obj :: badobjs else badobjs
   11.83 +        val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
   11.84 +      in badobjs' end
   11.85 +
   11.86 +    fun try_shrink (obj, result, stats') (stats, badobjs) =
   11.87 +      let
   11.88 +        fun is_failure s =
   11.89 +          let val (result, stats') = Property.test prop (s, stats)
   11.90 +          in if Property.failure result then SOME (s, result, stats') else NONE end
   11.91 +      in
   11.92 +        case get_first is_failure (shrink obj) of
   11.93 +          SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
   11.94 +        | NONE => status' (obj, result, (stats', badobjs))
   11.95 +      end
   11.96 +
   11.97 +    fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
   11.98 +      | iter (SOME (obj, stream), (stats, badobjs)) =
   11.99 +        if #count stats >= Config.get_generic ctxt gen_target then
  11.100 +          finish (stats, map apply_show badobjs)
  11.101 +        else
  11.102 +          let
  11.103 +            val (result, stats') = Property.test prop (obj, stats)
  11.104 +            val badobjs' = if Property.failure result then
  11.105 +                try_shrink (obj, result, stats') (stats, badobjs)
  11.106 +              else
  11.107 +                status' (obj, result, (stats', badobjs))
  11.108 +          in iter (next stream, (stats', badobjs')) end
  11.109 +  in
  11.110 +    fn stream => iter (next stream, (s0, []))
  11.111 +  end
  11.112 +
  11.113 +fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
  11.114 +fun check ctxt = check' ctxt Property.stats
  11.115 +fun checks ctxt = cpsCheck ctxt Property.stats
  11.116 +
  11.117 +fun checkGen ctxt (gen, show) (tag, prop) =
  11.118 +    check' ctxt {count=0, tags=[("__GEN", 0)]} (limit ctxt gen, show) (tag, prop) Generator.stream
  11.119 +
  11.120 +fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
  11.121 +    cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
  11.122 +           (limit ctxt gen, show) (tag, prop) Generator.stream
  11.123 +
  11.124 +fun checkOne ctxt show (tag, prop) obj = check ctxt (List.getItem, show) (tag, prop) [obj]
  11.125 +
  11.126 +(*calls the compiler and passes resulting type string to the parser*)
  11.127 +fun determine_type context s =
  11.128 +  let
  11.129 +    val ret = Unsynchronized.ref "return"
  11.130 +    val ctx : use_context = {
  11.131 +      tune_source = ML_Parse.fix_ints,
  11.132 +      name_space = ML_Env.name_space,
  11.133 +      str_of_pos = Position.here oo Position.line_file,
  11.134 +      print = fn r => ret := r,
  11.135 +      error = error
  11.136 +      }
  11.137 +    val _ = context |> Context.proof_map
  11.138 +      (ML_Context.exec (fn () => Secure.use_text ctx (0, "generated code") true s))
  11.139 +  in
  11.140 +    Gen_Construction.parse_pred (!ret)
  11.141 +  end;
  11.142 +
  11.143 +(*calls the compiler and runs the test*)
  11.144 +fun run_test context s =
  11.145 +  let
  11.146 +    val _ = Context.proof_map
  11.147 +        (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code")
  11.148 +        true s)) context
  11.149 +  in () end;
  11.150 +
  11.151 +(*split input into tokens*)
  11.152 +fun input_split s =
  11.153 +  let
  11.154 +    fun dot c = c = #"."
  11.155 +    fun space c = c = #" "
  11.156 +    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
  11.157 +  in (String.tokens space (Substring.string head),
  11.158 +    Substring.string (Substring.dropl dot code)) end;
  11.159 +
  11.160 +(*create the function from the input*)
  11.161 +fun make_fun s =
  11.162 +  let
  11.163 +    val scan_param = Scan.one (fn s => s <> ";")
  11.164 +    fun parameters s = Scan.repeat1 scan_param s
  11.165 +    val p = $$ "ALL" |-- parameters
  11.166 +    val (split, code) = input_split s
  11.167 +    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
  11.168 +    val (params, _) = Scan.finite stop p split
  11.169 +  in "fn (" ^ commas params ^ ") => " ^ code end;
  11.170 +
  11.171 +(*reads input and performs the test*)
  11.172 +fun gen_check_property check context s =
  11.173 +  let
  11.174 +    val func = make_fun s
  11.175 +    val (_, ty) = determine_type context func
  11.176 +  in run_test context (check (Proof_Context.theory_of context) "Check" (ty, func)) end;
  11.177 +
  11.178 +val check_property = gen_check_property Gen_Construction.build_check
  11.179 +(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
  11.180 +
  11.181 +(*performs test for specification function*)
  11.182 +fun gen_check_property_f check context s =
  11.183 +  let
  11.184 +    val (name, ty) = determine_type context s
  11.185 +  in run_test context (check (Proof_Context.theory_of context) name (ty, s)) end;
  11.186 +
  11.187 +val check_property_f = gen_check_property_f Gen_Construction.build_check
  11.188 +(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
  11.189 +
  11.190 +end;
  11.191 +
  11.192 +val check_property = Spec_Check.check_property;
  11.193 +