clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
authorwenzelm
Fri Aug 23 12:40:55 2013 +0200 (2013-08-23)
changeset 53164beb4ee344c22
parent 53163 7c2b13a53d69
child 53165 787d04a7c2d5
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
just one src/Tools/ROOT;
Admin/isatest/isatest-stats
CONTRIBUTORS
NEWS
ROOTS
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
src/Tools/Spec_Check/Examples.thy
src/Tools/Spec_Check/README
src/Tools/Spec_Check/Spec_Check.thy
src/Tools/Spec_Check/base_generator.ML
src/Tools/Spec_Check/gen_construction.ML
src/Tools/Spec_Check/generator.ML
src/Tools/Spec_Check/output_style.ML
src/Tools/Spec_Check/property.ML
src/Tools/Spec_Check/random.ML
src/Tools/Spec_Check/spec_check.ML
src/Tools/WWW_Find/ROOT
     1.1 --- a/Admin/isatest/isatest-stats	Fri Aug 23 12:30:51 2013 +0200
     1.2 +++ b/Admin/isatest/isatest-stats	Fri Aug 23 12:40:55 2013 +0200
     1.3 @@ -65,7 +65,6 @@
     1.4    HOL-SPARK
     1.5    HOL-SPARK-Examples
     1.6    HOL-SPARK-Manual
     1.7 -  HOL-Spec_Check
     1.8    HOL-Statespace
     1.9    HOL-TLA
    1.10    HOL-TLA-Buffer
    1.11 @@ -91,6 +90,7 @@
    1.12    IOA-Storage
    1.13    IOA-ex
    1.14    Pure
    1.15 +  Spec_Check
    1.16    ZF
    1.17    ZF-AC
    1.18    ZF-Coind
     2.1 --- a/CONTRIBUTORS	Fri Aug 23 12:30:51 2013 +0200
     2.2 +++ b/CONTRIBUTORS	Fri Aug 23 12:40:55 2013 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4    Ephemeral interpretation in local theories.
     2.5  
     2.6  * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM
     2.7 -  HOL-Spec_Check: A Quickcheck tool for Isabelle's ML environment.
     2.8 +  Spec_Check: A Quickcheck tool for Isabelle/ML.
     2.9  
    2.10  * April 2013: Stefan Berghofer, secunet Security Networks AG
    2.11    Dmitriy Traytel, TUM
     3.1 --- a/NEWS	Fri Aug 23 12:30:51 2013 +0200
     3.2 +++ b/NEWS	Fri Aug 23 12:40:55 2013 +0200
     3.3 @@ -312,13 +312,6 @@
     3.4    - Renamed option:
     3.5        isar_shrink ~> isar_compress
     3.6  
     3.7 -* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment.
     3.8 -  
     3.9 -  With HOL-Spec_Check, ML developers can check specifications with the
    3.10 -  ML function check_property. The specifications must be of the form
    3.11 -  "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in
    3.12 -  src/HOL/Spec_Check/Examples.thy.
    3.13 -
    3.14  * Imperative-HOL: The MREC combinator is considered legacy and no
    3.15  longer included by default. INCOMPATIBILITY, use partial_function
    3.16  instead, or import theory Legacy_Mrec as a fallback.
    3.17 @@ -331,6 +324,11 @@
    3.18  
    3.19  *** ML ***
    3.20  
    3.21 +* Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
    3.22 +"check_property" allows to check specifications of the form "ALL x y
    3.23 +z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
    3.24 +Examples.thy in particular.
    3.25 +
    3.26  * More uniform naming of goal functions for skipped proofs:
    3.27  
    3.28      Skip_Proof.prove  ~>  Goal.prove_sorry
     4.1 --- a/ROOTS	Fri Aug 23 12:30:51 2013 +0200
     4.2 +++ b/ROOTS	Fri Aug 23 12:40:55 2013 +0200
     4.3 @@ -9,3 +9,5 @@
     4.4  src/LCF
     4.5  src/Sequents
     4.6  src/Doc
     4.7 +src/Tools
     4.8 +
     5.1 --- a/src/HOL/ROOT	Fri Aug 23 12:30:51 2013 +0200
     5.2 +++ b/src/HOL/ROOT	Fri Aug 23 12:40:55 2013 +0200
     5.3 @@ -741,12 +741,6 @@
     5.4    options [document = false]
     5.5    theories WordExamples
     5.6  
     5.7 -session "HOL-Spec_Check" in Spec_Check = HOL +
     5.8 -  theories
     5.9 -    Spec_Check
    5.10 -  theories [condition = ISABELLE_POLYML]
    5.11 -    Examples
    5.12 -
    5.13  session "HOL-Statespace" in Statespace = HOL +
    5.14    theories [skip_proofs = false]
    5.15      StateSpaceEx
     6.1 --- a/src/HOL/Spec_Check/Examples.thy	Fri Aug 23 12:30:51 2013 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,83 +0,0 @@
     6.4 -theory Examples
     6.5 -imports Spec_Check
     6.6 -begin
     6.7 -
     6.8 -section {* List examples *}
     6.9 -
    6.10 -ML_command {*
    6.11 -check_property "ALL xs. rev xs = xs";
    6.12 -*}
    6.13 -
    6.14 -ML_command {*
    6.15 -check_property "ALL xs. rev (rev xs) = xs";
    6.16 -*}
    6.17 -
    6.18 -
    6.19 -section {* AList Specification *}
    6.20 -
    6.21 -ML_command {*
    6.22 -(* map_entry applies the function to the element *)
    6.23 -check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
    6.24 -*}
    6.25 -
    6.26 -ML_command {*
    6.27 -(* update always results in an entry *)
    6.28 -check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
    6.29 -*}
    6.30 -
    6.31 -ML_command {*
    6.32 -(* update always writes the value *)
    6.33 -check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
    6.34 -*}
    6.35 -
    6.36 -ML_command {*
    6.37 -(* default always results in an entry *)
    6.38 -check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
    6.39 -*}
    6.40 -
    6.41 -ML_command {*
    6.42 -(* delete always removes the entry *)
    6.43 -check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
    6.44 -*}
    6.45 -
    6.46 -ML_command {*
    6.47 -(* default writes the entry iff it didn't exist *)
    6.48 -check_property "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))";
    6.49 -*}
    6.50 -
    6.51 -section {* Examples on Types and Terms *}
    6.52 -
    6.53 -ML_command {*
    6.54 -check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
    6.55 -*}
    6.56 -
    6.57 -ML_command {*
    6.58 -check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
    6.59 -*}
    6.60 -
    6.61 -
    6.62 -text {* One would think this holds: *}
    6.63 -
    6.64 -ML_command {*
    6.65 -check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
    6.66 -*}
    6.67 -
    6.68 -text {* But it only holds with this precondition: *}
    6.69 -
    6.70 -ML_command {*
    6.71 -check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
    6.72 -*}
    6.73 -
    6.74 -section {* Some surprises *}
    6.75 -
    6.76 -ML_command {*
    6.77 -check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
    6.78 -*}
    6.79 -
    6.80 -
    6.81 -ML_command {*
    6.82 -val thy = @{theory};
    6.83 -check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
    6.84 -*}
    6.85 -
    6.86 -end
     7.1 --- a/src/HOL/Spec_Check/README	Fri Aug 23 12:30:51 2013 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,47 +0,0 @@
     7.4 -This is a Quickcheck tool for Isabelle's ML environment.
     7.5 -
     7.6 -Authors
     7.7 -
     7.8 -  Lukas Bulwahn
     7.9 -  Nicolai Schaffroth
    7.10 -
    7.11 -Quick Usage
    7.12 -
    7.13 -  - Import Spec_Check.thy in your development
    7.14 -  - Look at examples in Examples.thy
    7.15 -  - write specifications with the ML invocation
    7.16 -      check_property "ALL x. P x"
    7.17 -
    7.18 -Notes
    7.19 -
    7.20 -Our specification-based testing tool originated from Christopher League's
    7.21 -QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
    7.22 -provides a rich and uniform ML platform (called Isabelle/ML), this
    7.23 -testing tools is very different than the one for a typical ML developer.
    7.24 -
    7.25 -1. Isabelle/ML provides common data structures, which we can use in the
    7.26 -tool's implementation for storing data and printing output.
    7.27 -
    7.28 -2. The implementation in Isabelle that will be checked with this tool
    7.29 -commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
    7.30 -but they do not use other integer types in ML, such as ML's Int.int,
    7.31 -Word.word and others.
    7.32 -
    7.33 -3. As Isabelle can run heavily in parallel, we avoid reference types.
    7.34 -
    7.35 -4. Isabelle has special naming conventions and documentation of source
    7.36 -code is only minimal to avoid parroting.
    7.37 -
    7.38 -Next steps:
    7.39 -  - Remove all references and store the neccessary random seed in the
    7.40 -    Isabelle's context.
    7.41 -  - Simplify some existing random generators.
    7.42 -    The original ones from Christopher League are so complicated to
    7.43 -    support many integer types uniformly.
    7.44 -
    7.45 -License
    7.46 -
    7.47 -  The source code originated from Christopher League's QCheck, which is
    7.48 -  licensed under the 2-clause BSD license. The current source code is
    7.49 -  licensed under the compatible 3-clause BSD license of Isabelle.
    7.50 -
     8.1 --- a/src/HOL/Spec_Check/Spec_Check.thy	Fri Aug 23 12:30:51 2013 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,14 +0,0 @@
     8.4 -theory Spec_Check
     8.5 -imports Main
     8.6 -begin
     8.7 -
     8.8 -ML_file "random.ML"
     8.9 -ML_file "property.ML"
    8.10 -ML_file "base_generator.ML"
    8.11 -ML_file "generator.ML"
    8.12 -ML_file "gen_construction.ML"
    8.13 -ML_file "spec_check.ML"
    8.14 -ML_file "output_style.ML"
    8.15 -setup Output_Style.setup
    8.16 -
    8.17 -end
    8.18 \ No newline at end of file
     9.1 --- a/src/HOL/Spec_Check/base_generator.ML	Fri Aug 23 12:30:51 2013 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,201 +0,0 @@
     9.4 -(*  Title:      HOL/Spec_Check/base_generator.ML
     9.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     9.6 -    Author:     Christopher League
     9.7 -
     9.8 -Basic random generators.
     9.9 -*)
    9.10 -
    9.11 -signature BASE_GENERATOR =
    9.12 -sig
    9.13 -
    9.14 -type rand
    9.15 -type 'a gen = rand -> 'a * rand
    9.16 -type ('a, 'b) co = 'a -> 'b gen -> 'b gen
    9.17 -
    9.18 -val new : unit -> rand
    9.19 -val range : int * int -> rand -> int * rand
    9.20 -type ('a, 'b) reader = 'b -> ('a * 'b) option
    9.21 -
    9.22 -val lift : 'a -> 'a gen
    9.23 -val select : 'a vector -> 'a gen
    9.24 -val choose : 'a gen vector -> 'a gen
    9.25 -val choose' : (int * 'a gen) vector -> 'a gen
    9.26 -val selectL : 'a list -> 'a gen
    9.27 -val chooseL : 'a gen list -> 'a gen
    9.28 -val chooseL' : (int * 'a gen) list -> 'a gen
    9.29 -val filter : ('a -> bool) -> 'a gen -> 'a gen
    9.30 -
    9.31 -val zip : ('a gen * 'b gen) -> ('a * 'b) gen
    9.32 -val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
    9.33 -val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
    9.34 -val map : ('a -> 'b) -> 'a gen -> 'b gen
    9.35 -val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
    9.36 -val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
    9.37 -val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
    9.38 -
    9.39 -val flip : bool gen
    9.40 -val flip' : int * int -> bool gen
    9.41 -
    9.42 -val list : bool gen -> 'a gen -> 'a list gen
    9.43 -val option : bool gen -> 'a gen -> 'a option gen
    9.44 -val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
    9.45 -
    9.46 -val variant : (int, 'b) co
    9.47 -val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
    9.48 -val cobool : (bool, 'b) co
    9.49 -val colist : ('a, 'b) co -> ('a list, 'b) co
    9.50 -val coopt : ('a, 'b) co -> ('a option, 'b) co
    9.51 -
    9.52 -type stream
    9.53 -val start : rand -> stream
    9.54 -val limit : int -> 'a gen -> ('a, stream) reader
    9.55 -
    9.56 -end
    9.57 -
    9.58 -structure Base_Generator : BASE_GENERATOR =
    9.59 -struct
    9.60 -
    9.61 -(* random number engine *)
    9.62 -
    9.63 -type rand = real
    9.64 -
    9.65 -val a = 16807.0
    9.66 -val m = 2147483647.0
    9.67 -
    9.68 -fun nextrand seed =
    9.69 -  let
    9.70 -    val t = a * seed
    9.71 -  in
    9.72 -    t - m * real (floor (t / m))
    9.73 -  end
    9.74 -
    9.75 -val new = nextrand o Time.toReal o Time.now
    9.76 -
    9.77 -fun range (min, max) =
    9.78 -  if min > max then raise Domain (* TODO: raise its own error *)
    9.79 -  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
    9.80 -
    9.81 -fun split r =
    9.82 -  let
    9.83 -    val r = r / a
    9.84 -    val r0 = real (floor r)
    9.85 -    val r1 = r - r0
    9.86 -  in
    9.87 -    (nextrand r0, nextrand r1)
    9.88 -  end
    9.89 -
    9.90 -(* generators *)
    9.91 -
    9.92 -type 'a gen = rand -> 'a * rand
    9.93 -type ('a, 'b) reader = 'b -> ('a * 'b) option
    9.94 -
    9.95 -fun lift obj r = (obj, r)
    9.96 -
    9.97 -local (* Isabelle does not use vectors? *)
    9.98 -  fun explode ((freq, gen), acc) =
    9.99 -    List.tabulate (freq, fn _ => gen) @ acc
   9.100 -in
   9.101 -  fun choose v r =
   9.102 -    let val (i, r) = range(0, Vector.length v - 1) r
   9.103 -    in Vector.sub (v, i) r end
   9.104 -  fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
   9.105 -  fun select v = choose (Vector.map lift v)
   9.106 -end
   9.107 -
   9.108 -fun chooseL l = choose (Vector.fromList l)
   9.109 -fun chooseL' l = choose' (Vector.fromList l)
   9.110 -fun selectL l = select (Vector.fromList l)
   9.111 -
   9.112 -fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
   9.113 -
   9.114 -fun zip3 (g1, g2, g3) =
   9.115 -  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
   9.116 -
   9.117 -fun zip4 (g1, g2, g3, g4) =
   9.118 -  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
   9.119 -
   9.120 -fun map f g = apfst f o g
   9.121 -
   9.122 -fun map2 f = map f o zip
   9.123 -fun map3 f = map f o zip3
   9.124 -fun map4 f = map f o zip4
   9.125 -
   9.126 -fun filter p gen r =
   9.127 -  let
   9.128 -    fun loop (x, r) = if p x then (x, r) else loop (gen r)
   9.129 -  in
   9.130 -    loop (gen r)
   9.131 -  end
   9.132 -
   9.133 -val flip = selectL [true, false]
   9.134 -fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
   9.135 -
   9.136 -fun list flip g r =
   9.137 -  case flip r of
   9.138 -      (true, r) => ([], r)
   9.139 -    | (false, r) =>
   9.140 -      let
   9.141 -        val (x,r) = g r
   9.142 -        val (xs,r) = list flip g r
   9.143 -      in (x::xs, r) end
   9.144 -
   9.145 -fun option flip g r =
   9.146 -  case flip r of
   9.147 -    (true, r) => (NONE, r)
   9.148 -  | (false, r) => map SOME g r
   9.149 -
   9.150 -fun vector tabulate (int, elem) r =
   9.151 -  let
   9.152 -    val (n, r) = int r
   9.153 -    val p = Unsynchronized.ref r
   9.154 -    fun g _ =
   9.155 -      let
   9.156 -        val (x,r) = elem(!p)
   9.157 -      in x before p := r end
   9.158 -  in
   9.159 -    (tabulate(n, g), !p)
   9.160 -  end
   9.161 -
   9.162 -type stream = rand Unsynchronized.ref * int
   9.163 -
   9.164 -fun start r = (Unsynchronized.ref r, 0)
   9.165 -
   9.166 -fun limit max gen =
   9.167 -  let
   9.168 -    fun next (p, i) =
   9.169 -      if i >= max then NONE
   9.170 -      else
   9.171 -        let val (x, r) = gen(!p)
   9.172 -        in SOME(x, (p, i+1)) before p := r end
   9.173 -  in
   9.174 -    next
   9.175 -  end
   9.176 -
   9.177 -type ('a, 'b) co = 'a -> 'b gen -> 'b gen
   9.178 -
   9.179 -fun variant v g r =
   9.180 -  let
   9.181 -    fun nth (i, r) =
   9.182 -      let val (r1, r2) = split r
   9.183 -      in if i = 0 then r1 else nth (i-1, r2) end
   9.184 -  in
   9.185 -    g (nth (v, r))
   9.186 -  end
   9.187 -
   9.188 -fun arrow (cogen, gen) r =
   9.189 -  let
   9.190 -    val (r1, r2) = split r
   9.191 -    fun g x = fst (cogen x gen r1)
   9.192 -  in (g, r2) end
   9.193 -
   9.194 -fun cobool false = variant 0
   9.195 -  | cobool true = variant 1
   9.196 -
   9.197 -fun colist _ [] = variant 0
   9.198 -  | colist co (x::xs) = variant 1 o co x o colist co xs
   9.199 -
   9.200 -fun coopt _ NONE = variant 0
   9.201 -  | coopt co (SOME x) = variant 1 o co x
   9.202 -
   9.203 -end
   9.204 -
    10.1 --- a/src/HOL/Spec_Check/gen_construction.ML	Fri Aug 23 12:30:51 2013 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,179 +0,0 @@
    10.4 -(*  Title:      HOL/Spec_Check/gen_construction.ML
    10.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    10.6 -    Author:     Christopher League
    10.7 -
    10.8 -Constructing generators and pretty printing function for complex types.
    10.9 -*)
   10.10 -
   10.11 -signature GEN_CONSTRUCTION =
   10.12 -sig
   10.13 -  val register : string * (string * string) -> theory -> theory
   10.14 -  type mltype
   10.15 -  val parse_pred : string -> string * mltype
   10.16 -  val build_check : Proof.context -> string -> mltype * string -> string
   10.17 -  (*val safe_check : string -> mltype * string -> string*)
   10.18 -  val string_of_bool : bool -> string
   10.19 -  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
   10.20 -end;
   10.21 -
   10.22 -structure Gen_Construction : GEN_CONSTRUCTION =
   10.23 -struct
   10.24 -
   10.25 -(* Parsing ML types *)
   10.26 -
   10.27 -datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
   10.28 -
   10.29 -(*Split string into tokens for parsing*)
   10.30 -fun split s =
   10.31 -  let
   10.32 -    fun split_symbol #"(" = "( "
   10.33 -      | split_symbol #")" = " )"
   10.34 -      | split_symbol #"," = " ,"
   10.35 -      | split_symbol #":" = " :"
   10.36 -      | split_symbol c = Char.toString c
   10.37 -    fun is_space c = c = #" "
   10.38 -  in String.tokens is_space (String.translate split_symbol s) end;
   10.39 -
   10.40 -(*Accept anything that is not a recognized symbol*)
   10.41 -val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
   10.42 -
   10.43 -(*Turn a type list into a nested Con*)
   10.44 -fun make_con [] = raise Empty
   10.45 -  | make_con [c] = c
   10.46 -  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
   10.47 -
   10.48 -(*Parse a type*)
   10.49 -fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
   10.50 -
   10.51 -and parse_type_arg s = (parse_tuple || parse_type_single) s
   10.52 -
   10.53 -and parse_type_single s = (parse_con || parse_type_basic) s
   10.54 -
   10.55 -and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
   10.56 -
   10.57 -and parse_list s =
   10.58 -  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
   10.59 -
   10.60 -and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
   10.61 -
   10.62 -and parse_con s = ((parse_con_nest
   10.63 -  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
   10.64 -  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
   10.65 -  >> (make_con o rev)) s
   10.66 -
   10.67 -and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
   10.68 -
   10.69 -and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
   10.70 -
   10.71 -and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
   10.72 -  >> (fn (t, tl) => Tuple (t :: tl))) s;
   10.73 -
   10.74 -(*Parse entire type + name*)
   10.75 -fun parse_function s =
   10.76 -  let
   10.77 -    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
   10.78 -    val (name, ty) = p (split s)
   10.79 -    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
   10.80 -    val (typ, _) = Scan.finite stop parse_type ty
   10.81 -  in (name, typ) end;
   10.82 -
   10.83 -(*Create desired output*)
   10.84 -fun parse_pred s =
   10.85 -  let
   10.86 -    val (name, Con ("->", t :: _)) = parse_function s
   10.87 -  in (name, t) end;
   10.88 -
   10.89 -(* Construct Generators and Pretty Printers *)
   10.90 -
   10.91 -(*copied from smt_config.ML *)
   10.92 -fun string_of_bool b = if b then "true" else "false"
   10.93 -
   10.94 -fun string_of_ref f r = f (!r) ^ " ref";
   10.95 -
   10.96 -val initial_content = Symtab.make
   10.97 -  [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
   10.98 -  ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
   10.99 -  ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
  10.100 -  ("unit", ("gen_unit", "fn () => \"()\"")),
  10.101 -  ("int", ("Generator.int", "string_of_int")),
  10.102 -  ("real", ("Generator.real", "string_of_real")),
  10.103 -  ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
  10.104 -  ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
  10.105 -  ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
  10.106 -  ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
  10.107 -  ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
  10.108 -
  10.109 -structure Data = Theory_Data
  10.110 -(
  10.111 -  type T = (string * string) Symtab.table
  10.112 -  val empty = initial_content
  10.113 -  val extend = I
  10.114 -  fun merge data : T = Symtab.merge (K true) data
  10.115 -)
  10.116 -
  10.117 -fun data_of ctxt tycon =
  10.118 -  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
  10.119 -    SOME data => data
  10.120 -  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
  10.121 -
  10.122 -val generator_of = fst oo data_of
  10.123 -val printer_of = snd oo data_of
  10.124 -
  10.125 -fun register (ty, data) = Data.map (Symtab.update (ty, data))
  10.126 -
  10.127 -(*
  10.128 -fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
  10.129 -*)
  10.130 -
  10.131 -fun combine dict [] = dict
  10.132 -  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
  10.133 -
  10.134 -fun compose_generator _ Var = "Generator.int"
  10.135 -  | compose_generator ctxt (Con (s, types)) =
  10.136 -      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
  10.137 -  | compose_generator ctxt (Tuple t) =
  10.138 -      let
  10.139 -        fun tuple_body t = space_implode ""
  10.140 -          (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
  10.141 -          compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
  10.142 -        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
  10.143 -      in
  10.144 -        "fn r0 => let " ^ tuple_body t ^
  10.145 -        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
  10.146 -      end;
  10.147 -
  10.148 -fun compose_printer _ Var = "Int.toString"
  10.149 -  | compose_printer ctxt (Con (s, types)) =
  10.150 -      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
  10.151 -  | compose_printer ctxt (Tuple t) =
  10.152 -      let
  10.153 -        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
  10.154 -        fun tuple_body t = space_implode " ^ \", \" ^ "
  10.155 -          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
  10.156 -          (t ~~ (1 upto (length t))))
  10.157 -      in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
  10.158 -
  10.159 -(*produce compilable string*)
  10.160 -fun build_check ctxt name (ty, spec) =
  10.161 -  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
  10.162 -  ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
  10.163 -  ^ name ^ "\", Property.pred (" ^ spec ^ "));";
  10.164 -
  10.165 -(*produce compilable string - non-eqtype functions*)
  10.166 -(*
  10.167 -fun safe_check name (ty, spec) =
  10.168 -  let
  10.169 -    val default =
  10.170 -      (case AList.lookup (op =) (!gen_table) "->" of
  10.171 -        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
  10.172 -      | SOME entry => entry)
  10.173 -  in
  10.174 -   (gen_table :=
  10.175 -     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
  10.176 -    build_check name (ty, spec) before
  10.177 -    gen_table := AList.update (op =) ("->", default) (!gen_table))
  10.178 -  end;
  10.179 -*)
  10.180 -
  10.181 -end;
  10.182 -
    11.1 --- a/src/HOL/Spec_Check/generator.ML	Fri Aug 23 12:30:51 2013 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,235 +0,0 @@
    11.4 -(*  Title:      HOL/Spec_Check/generator.ML
    11.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    11.6 -    Author:     Christopher League
    11.7 -
    11.8 -Random generators for Isabelle/ML's types.
    11.9 -*)
   11.10 -
   11.11 -signature GENERATOR = sig
   11.12 -  include BASE_GENERATOR
   11.13 -  (* text generators *)
   11.14 -  val char : char gen
   11.15 -  val charRange : char * char -> char gen
   11.16 -  val charFrom : string -> char gen
   11.17 -  val charByType : (char -> bool) -> char gen
   11.18 -  val string : (int gen * char gen) -> string gen
   11.19 -  val substring : string gen -> substring gen
   11.20 -  val cochar : (char, 'b) co
   11.21 -  val costring : (string, 'b) co
   11.22 -  val cosubstring : (substring, 'b) co
   11.23 -  (* integer generators *)
   11.24 -  val int : int gen
   11.25 -  val int_pos : int gen
   11.26 -  val int_neg : int gen
   11.27 -  val int_nonpos : int gen
   11.28 -  val int_nonneg : int gen
   11.29 -  val coint : (int, 'b) co
   11.30 -  (* real generators *)
   11.31 -  val real : real gen
   11.32 -  val real_frac : real gen
   11.33 -  val real_pos : real gen
   11.34 -  val real_neg : real gen
   11.35 -  val real_nonpos : real gen
   11.36 -  val real_nonneg : real gen
   11.37 -  val real_finite : real gen
   11.38 -  (* function generators *)
   11.39 -  val function_const : 'c * 'b gen -> ('a -> 'b) gen
   11.40 -  val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
   11.41 -  val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
   11.42 -  val unit : unit gen
   11.43 -  val ref' : 'a gen -> 'a Unsynchronized.ref gen
   11.44 -  (* more generators *)
   11.45 -  val term : int -> term gen
   11.46 -  val typ : int -> typ gen
   11.47 -
   11.48 -  val stream : stream
   11.49 -end
   11.50 -
   11.51 -structure Generator : GENERATOR =
   11.52 -struct
   11.53 -
   11.54 -open Base_Generator
   11.55 -
   11.56 -val stream = start (new())
   11.57 -
   11.58 -type 'a gen = rand -> 'a * rand
   11.59 -type ('a, 'b) co = 'a -> 'b gen -> 'b gen
   11.60 -
   11.61 -(* text *)
   11.62 -
   11.63 -type char = Char.char
   11.64 -type string = String.string
   11.65 -type substring = Substring.substring
   11.66 -
   11.67 -
   11.68 -val char = map Char.chr (range (0, Char.maxOrd))
   11.69 -fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
   11.70 -
   11.71 -fun charFrom s =
   11.72 -  choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
   11.73 -
   11.74 -fun charByType p = filter p char
   11.75 -
   11.76 -val string = vector CharVector.tabulate
   11.77 -
   11.78 -fun substring gen r =
   11.79 -  let
   11.80 -    val (s, r') = gen r
   11.81 -    val (i, r'') = range (0, String.size s) r'
   11.82 -    val (j, r''') = range (0, String.size s - i) r''
   11.83 -  in
   11.84 -    (Substring.substring (s, i, j), r''')
   11.85 -  end
   11.86 -
   11.87 -fun cochar c =
   11.88 -  if Char.ord c = 0 then variant 0
   11.89 -  else variant 1 o cochar (Char.chr (Char.ord c div 2))
   11.90 -
   11.91 -fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
   11.92 -
   11.93 -fun costring s = cosubstring (Substring.full s)
   11.94 -
   11.95 -(* integers *)
   11.96 -val digit = charRange (#"0", #"9")
   11.97 -val nonzero = string (lift 1, charRange (#"1", #"9"))
   11.98 -fun digits' n = string (range (0, n-1), digit)
   11.99 -fun digits n = map2 op^ (nonzero, digits' n)
  11.100 -
  11.101 -val maxDigits = 64
  11.102 -val ratio = 49
  11.103 -
  11.104 -fun pos_or_neg f r =
  11.105 -  let
  11.106 -    val (s, r') = digits maxDigits r
  11.107 -  in (f (the (Int.fromString s)), r') end
  11.108 -
  11.109 -val int_pos = pos_or_neg I
  11.110 -val int_neg = pos_or_neg Int.~
  11.111 -val zero = lift 0
  11.112 -
  11.113 -val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
  11.114 -val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
  11.115 -val int = chooseL [int_nonneg, int_nonpos]
  11.116 -
  11.117 -fun coint n =
  11.118 -  if n = 0 then variant 0
  11.119 -  else if n < 0 then variant 1 o coint (~ n)
  11.120 -  else variant 2 o coint (n div 2)
  11.121 -
  11.122 -(* reals *)
  11.123 -val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
  11.124 -
  11.125 -fun real_frac r =
  11.126 -  let val (s, r') = digits r
  11.127 -  in (the (Real.fromString s), r') end
  11.128 -
  11.129 -val {exp=minExp,...} = Real.toManExp Real.minPos
  11.130 -val {exp=maxExp,...} = Real.toManExp Real.posInf
  11.131 -
  11.132 -val ratio = 99
  11.133 -
  11.134 -fun mk r =
  11.135 -  let
  11.136 -    val (a, r') = digits r
  11.137 -    val (b, r'') = digits r'
  11.138 -    val (e, r''') = range (minExp div 4, maxExp div 4) r''
  11.139 -    val x = String.concat [a, ".", b, "E", Int.toString e]
  11.140 -  in
  11.141 -    (the (Real.fromString x), r''')
  11.142 -  end
  11.143 -
  11.144 -val real_pos = chooseL' (List.map ((pair 1) o lift)
  11.145 -    [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
  11.146 -
  11.147 -val real_neg = map Real.~ real_pos
  11.148 -
  11.149 -val real_zero = Real.fromInt 0
  11.150 -val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
  11.151 -val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
  11.152 -
  11.153 -val real = chooseL [real_nonneg, real_nonpos]
  11.154 -
  11.155 -val real_finite = filter Real.isFinite real
  11.156 -
  11.157 -(*alternate list generator - uses an integer generator to determine list length*)
  11.158 -fun list' int gen = vector List.tabulate (int, gen);
  11.159 -
  11.160 -(* more function generators *)
  11.161 -
  11.162 -fun function_const (_, gen2) r =
  11.163 -  let
  11.164 -    val (v, r') = gen2 r
  11.165 -  in (fn _ => v, r') end;
  11.166 -
  11.167 -fun function_strict size (gen1, gen2) r =
  11.168 -  let
  11.169 -    val (def, r') = gen2 r
  11.170 -    val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
  11.171 -  in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
  11.172 -
  11.173 -fun function_lazy (gen1, gen2) r =
  11.174 -  let
  11.175 -    val (initial1, r') = gen1 r
  11.176 -    val (initial2, internal) = gen2 r'
  11.177 -    val seed = Unsynchronized.ref internal
  11.178 -    val table = Unsynchronized.ref [(initial1, initial2)]
  11.179 -    fun new_entry k =
  11.180 -      let
  11.181 -        val (new_val, new_seed) = gen2 (!seed)
  11.182 -        val _ =  seed := new_seed
  11.183 -        val _ = table := AList.update (op =) (k, new_val) (!table)
  11.184 -      in new_val end
  11.185 -  in
  11.186 -    (fn v1 =>
  11.187 -      case AList.lookup (op =) (!table) v1 of
  11.188 -        NONE => new_entry v1
  11.189 -      | SOME v2 => v2, r')
  11.190 -  end;
  11.191 -
  11.192 -(* unit *)
  11.193 -
  11.194 -fun unit r = ((), r);
  11.195 -
  11.196 -(* references *)
  11.197 -
  11.198 -fun ref' gen r =
  11.199 -  let val (value, r') = gen r
  11.200 -  in (Unsynchronized.ref value, r') end;
  11.201 -
  11.202 -(* types and terms *)
  11.203 -
  11.204 -val sort_string = selectL ["sort1", "sort2", "sort3"];
  11.205 -val type_string = selectL ["TCon1", "TCon2", "TCon3"];
  11.206 -val tvar_string = selectL ["a", "b", "c"];
  11.207 -
  11.208 -val const_string = selectL ["c1", "c2", "c3"];
  11.209 -val var_string = selectL ["x", "y", "z"];
  11.210 -val index = selectL [0, 1, 2, 3];
  11.211 -val bound_index = selectL [0, 1, 2, 3];
  11.212 -
  11.213 -val sort = list (flip' (1, 2)) sort_string;
  11.214 -
  11.215 -fun typ n =
  11.216 -  let
  11.217 -    fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
  11.218 -    val tfree = map TFree (zip (tvar_string, sort))
  11.219 -    val tvar = map TVar (zip (zip (tvar_string, index), sort))
  11.220 -  in
  11.221 -    if n = 0 then chooseL [tfree, tvar]
  11.222 -    else chooseL [type' (n div 2), tfree, tvar]
  11.223 -  end;
  11.224 -
  11.225 -fun term n =
  11.226 -  let
  11.227 -    val const = map Const (zip (const_string, typ 10))
  11.228 -    val free = map Free (zip (var_string, typ 10))
  11.229 -    val var = map Var (zip (zip (var_string, index), typ 10))
  11.230 -    val bound = map Bound bound_index
  11.231 -    fun abs m = map Abs (zip3 (var_string, typ 10, term m))
  11.232 -    fun app m = map (op $) (zip (term m, term m))
  11.233 -  in
  11.234 -    if n = 0 then chooseL [const, free, var, bound]
  11.235 -    else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
  11.236 -  end;
  11.237 -
  11.238 -end
    12.1 --- a/src/HOL/Spec_Check/output_style.ML	Fri Aug 23 12:30:51 2013 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,119 +0,0 @@
    12.4 -(*  Title:      HOL/Spec_Check/output_style.ML
    12.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    12.6 -    Author:     Christopher League
    12.7 -
    12.8 -Output styles for presenting Spec_Check's results.
    12.9 -*)
   12.10 -
   12.11 -signature OUTPUT_STYLE =
   12.12 -sig
   12.13 -  val setup : theory -> theory
   12.14 -end
   12.15 -
   12.16 -structure Output_Style : OUTPUT_STYLE =
   12.17 -struct
   12.18 -
   12.19 -(* perl style *)
   12.20 -
   12.21 -val perl_style =
   12.22 -  Spec_Check.register_style "Perl"
   12.23 -    (fn ctxt => fn tag =>
   12.24 -      let
   12.25 -        val target = Config.get ctxt Spec_Check.gen_target
   12.26 -        val namew = Config.get ctxt Spec_Check.column_width
   12.27 -        val sort_examples = Config.get ctxt Spec_Check.sort_examples
   12.28 -        val show_stats = Config.get ctxt Spec_Check.show_stats
   12.29 -        val limit = Config.get ctxt Spec_Check.examples
   12.30 -
   12.31 -        val resultw = 8
   12.32 -        val countw = 20
   12.33 -        val allw = namew + resultw + countw + 2
   12.34 -
   12.35 -        val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
   12.36 -
   12.37 -        fun result ({count = 0, ...}, _) _ = "dubious"
   12.38 -          | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
   12.39 -          | result ({count, tags}, badobjs) true =
   12.40 -              if not (null badobjs) then "FAILED"
   12.41 -              else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
   12.42 -              else "ok"
   12.43 -
   12.44 -        fun ratio (0, _) = "(0/0 passed)"
   12.45 -          | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
   12.46 -          | ratio (count, n) =
   12.47 -              "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
   12.48 -
   12.49 -        fun update (stats, badobjs) donep =
   12.50 -          "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
   12.51 -          StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
   12.52 -          StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
   12.53 -
   12.54 -        fun status (_, result, (stats, badobjs)) =
   12.55 -          if Property.failure result then warning (update (stats, badobjs) false) else ()
   12.56 -
   12.57 -        fun prtag count (tag, n) first =
   12.58 -          if String.isPrefix "__" tag then ("", first)
   12.59 -          else
   12.60 -             let
   12.61 -               val ratio = round ((real n / real count) * 100.0)
   12.62 -             in
   12.63 -               (((if first then "" else StringCvt.padRight #" " allw "\n") ^
   12.64 -                 StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
   12.65 -               false)
   12.66 -             end
   12.67 -
   12.68 -        fun prtags ({count, tags} : Property.stats) =
   12.69 -          if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
   12.70 -
   12.71 -        fun err badobjs =
   12.72 -          let
   12.73 -            fun iter [] _ = ()
   12.74 -              | iter (e :: es) k =
   12.75 -                  (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
   12.76 -                    StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
   12.77 -                  iter es (k + 1))
   12.78 -          in
   12.79 -            iter (maybe_sort (take limit (map_filter I badobjs))) 0
   12.80 -          end
   12.81 -
   12.82 -        fun finish (stats, badobjs) =
   12.83 -          if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
   12.84 -          else (warning (update (stats, badobjs) true); err badobjs)
   12.85 -      in
   12.86 -        {status = status, finish = finish}
   12.87 -      end)
   12.88 -
   12.89 -
   12.90 -(* CM style: meshes with CM output; highlighted in sml-mode *)
   12.91 -
   12.92 -val cm_style =
   12.93 -  Spec_Check.register_style "CM"
   12.94 -    (fn ctxt => fn tag =>
   12.95 -      let
   12.96 -        fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
   12.97 -        val gen_target = Config.get ctxt Spec_Check.gen_target
   12.98 -        val _ = writeln ("[testing " ^ tag ^ "... ")
   12.99 -        fun finish ({count, ...} : Property.stats, badobjs) =
  12.100 -          (case (count, badobjs) of
  12.101 -            (0, []) => warning ("no valid cases generated]")
  12.102 -          | (n, []) => writeln (
  12.103 -                if n >= gen_target then "ok]"
  12.104 -                else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
  12.105 -          | (_, es) =>
  12.106 -              let
  12.107 -                val wd = size (string_of_int (length es))
  12.108 -                fun each (NONE, _) = ()
  12.109 -                  | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
  12.110 -              in
  12.111 -                (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
  12.112 -              end)
  12.113 -      in
  12.114 -        {status = K (), finish = finish}
  12.115 -      end)
  12.116 -
  12.117 -
  12.118 -(* setup *)
  12.119 -
  12.120 -val setup = perl_style #> cm_style
  12.121 -
  12.122 -end
    13.1 --- a/src/HOL/Spec_Check/property.ML	Fri Aug 23 12:30:51 2013 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,77 +0,0 @@
    13.4 -(*  Title:      HOL/Spec_Check/property.ML
    13.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    13.6 -    Author:     Christopher League
    13.7 -
    13.8 -Conditional properties that can track argument distribution.
    13.9 -*)
   13.10 -
   13.11 -signature PROPERTY =
   13.12 -sig
   13.13 -
   13.14 -type 'a pred = 'a -> bool
   13.15 -type 'a prop
   13.16 -val pred : 'a pred -> 'a prop
   13.17 -val pred2 : ('a * 'b) pred -> 'b -> 'a  prop
   13.18 -val implies : 'a pred * 'a prop -> 'a prop
   13.19 -val ==> : 'a pred * 'a pred -> 'a prop
   13.20 -val trivial : 'a pred -> 'a prop -> 'a prop
   13.21 -val classify : 'a pred -> string -> 'a prop -> 'a prop
   13.22 -val classify' : ('a -> string option) -> 'a prop -> 'a prop
   13.23 -
   13.24 -(*Results*)
   13.25 -type result = bool option
   13.26 -type stats = { tags : (string * int) list, count : int }
   13.27 -val test : 'a prop -> 'a * stats -> result * stats
   13.28 -val stats : stats
   13.29 -val success : result pred
   13.30 -val failure : result pred
   13.31 -
   13.32 -end
   13.33 -
   13.34 -structure Property : PROPERTY =
   13.35 -struct
   13.36 -
   13.37 -type result = bool option
   13.38 -type stats = { tags : (string * int) list, count : int }
   13.39 -type 'a pred = 'a -> bool
   13.40 -type 'a prop = 'a * stats -> result * stats
   13.41 -
   13.42 -fun success (SOME true) = true
   13.43 -  | success _ = false
   13.44 -
   13.45 -fun failure (SOME false) = true
   13.46 -  | failure _ = false
   13.47 -
   13.48 -fun apply f x = (case try f x of NONE => SOME false | some => some)
   13.49 -fun pred f (x,s) = (apply f x, s)
   13.50 -fun pred2 f z = pred (fn x => f (x, z))
   13.51 -
   13.52 -fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
   13.53 -
   13.54 -fun ==> (p1, p2) = implies (p1, pred p2)
   13.55 -
   13.56 -fun wrap trans p (x,s) =
   13.57 -  let val (result,s) = p (x,s)
   13.58 -  in (result, trans (x, result, s)) end
   13.59 -
   13.60 -fun classify' f =
   13.61 -  wrap (fn (x, result, {tags, count}) =>
   13.62 -    { tags =
   13.63 -        if is_some result then
   13.64 -          (case f x of
   13.65 -            NONE => tags
   13.66 -          | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
   13.67 -        else tags,
   13.68 -     count = count })
   13.69 -
   13.70 -fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
   13.71 -
   13.72 -fun trivial cond = classify cond "trivial"
   13.73 -
   13.74 -fun test p =
   13.75 -  wrap (fn (_, result, {tags, count}) =>
   13.76 -    { tags = tags, count = if is_some result then count + 1 else count }) p
   13.77 -
   13.78 -val stats = { tags = [], count = 0 }
   13.79 -
   13.80 -end
    14.1 --- a/src/HOL/Spec_Check/random.ML	Fri Aug 23 12:30:51 2013 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,46 +0,0 @@
    14.4 -(*  Title:      HOL/Spec_Check/random.ML
    14.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    14.6 -    Author:     Christopher League
    14.7 -
    14.8 -Random number engine.
    14.9 -*)
   14.10 -
   14.11 -signature RANDOM =
   14.12 -sig
   14.13 -  type rand
   14.14 -  val new : unit -> rand
   14.15 -  val range : int * int -> rand -> int * rand
   14.16 -  val split : rand -> rand * rand
   14.17 -end
   14.18 -
   14.19 -structure Random : RANDOM  =
   14.20 -struct
   14.21 -
   14.22 -type rand = real
   14.23 -
   14.24 -val a = 16807.0
   14.25 -val m = 2147483647.0
   14.26 -
   14.27 -fun nextrand seed =
   14.28 -  let
   14.29 -    val t = a * seed
   14.30 -  in
   14.31 -    t - m * real(floor(t/m))
   14.32 -  end
   14.33 -
   14.34 -val new = nextrand o Time.toReal o Time.now
   14.35 -
   14.36 -fun range (min, max) =
   14.37 -  if min > max then raise Domain (* TODO: raise its own error *)
   14.38 -  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
   14.39 -
   14.40 -fun split r =
   14.41 -  let
   14.42 -    val r = r / a
   14.43 -    val r0 = real(floor r)
   14.44 -    val r1 = r - r0
   14.45 -  in
   14.46 -    (nextrand r0, nextrand r1)
   14.47 -  end
   14.48 -
   14.49 -end
    15.1 --- a/src/HOL/Spec_Check/spec_check.ML	Fri Aug 23 12:30:51 2013 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,192 +0,0 @@
    15.4 -(*  Title:      HOL/Spec_Check/spec_check.ML
    15.5 -    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    15.6 -    Author:     Christopher League
    15.7 -
    15.8 -Specification-based testing of ML programs with random values.
    15.9 -*)
   15.10 -
   15.11 -signature SPEC_CHECK =
   15.12 -sig
   15.13 -  val gen_target : int Config.T
   15.14 -  val gen_max : int Config.T
   15.15 -  val examples : int Config.T
   15.16 -  val sort_examples : bool Config.T
   15.17 -  val show_stats : bool Config.T
   15.18 -  val column_width : int Config.T
   15.19 -  val style : string Config.T
   15.20 -
   15.21 -  type output_style = Proof.context -> string ->
   15.22 -    {status : string option * Property.result * (Property.stats  * string option list) -> unit,
   15.23 -     finish: Property.stats * string option list -> unit}
   15.24 -
   15.25 -  val register_style : string -> output_style -> theory -> theory
   15.26 -
   15.27 -  val checkGen : Proof.context ->
   15.28 -    'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
   15.29 -
   15.30 -  val check_property : Proof.context -> string -> unit
   15.31 -end;
   15.32 -
   15.33 -structure Spec_Check : SPEC_CHECK =
   15.34 -struct
   15.35 -
   15.36 -(* configurations *)
   15.37 -
   15.38 -val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
   15.39 -val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
   15.40 -val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
   15.41 -
   15.42 -val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
   15.43 -val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
   15.44 -val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
   15.45 -val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
   15.46 -
   15.47 -type ('a, 'b) reader = 'b -> ('a * 'b) option
   15.48 -type 'a rep = ('a -> string) option
   15.49 -
   15.50 -type output_style = Proof.context -> string ->
   15.51 -  {status: string option * Property.result * (Property.stats * string option list) -> unit,
   15.52 -   finish: Property.stats * string option list -> unit}
   15.53 -
   15.54 -fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
   15.55 -
   15.56 -structure Style = Theory_Data
   15.57 -(
   15.58 -  type T = output_style Symtab.table
   15.59 -  val empty = Symtab.empty
   15.60 -  val extend = I
   15.61 -  fun merge data : T = Symtab.merge (K true) data
   15.62 -)
   15.63 -
   15.64 -fun get_style ctxt =
   15.65 -  let val name = Config.get ctxt style in
   15.66 -    (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
   15.67 -      SOME style => style ctxt
   15.68 -    | NONE => error ("No style called " ^ quote name ^ " found"))
   15.69 -  end
   15.70 -
   15.71 -fun register_style name style = Style.map (Symtab.update (name, style))
   15.72 -
   15.73 -
   15.74 -(* testing functions *)
   15.75 -
   15.76 -fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
   15.77 -  let
   15.78 -    val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
   15.79 -
   15.80 -    val {status, finish} = get_style ctxt tag
   15.81 -    fun status' (obj, result, (stats, badobjs)) =
   15.82 -      let
   15.83 -        val badobjs' = if Property.failure result then obj :: badobjs else badobjs
   15.84 -        val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
   15.85 -      in badobjs' end
   15.86 -
   15.87 -    fun try_shrink (obj, result, stats') (stats, badobjs) =
   15.88 -      let
   15.89 -        fun is_failure s =
   15.90 -          let val (result, stats') = Property.test prop (s, stats)
   15.91 -          in if Property.failure result then SOME (s, result, stats') else NONE end
   15.92 -      in
   15.93 -        case get_first is_failure (shrink obj) of
   15.94 -          SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
   15.95 -        | NONE => status' (obj, result, (stats', badobjs))
   15.96 -      end
   15.97 -
   15.98 -    fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
   15.99 -      | iter (SOME (obj, stream), (stats, badobjs)) =
  15.100 -        if #count stats >= Config.get ctxt gen_target then
  15.101 -          finish (stats, map apply_show badobjs)
  15.102 -        else
  15.103 -          let
  15.104 -            val (result, stats') = Property.test prop (obj, stats)
  15.105 -            val badobjs' = if Property.failure result then
  15.106 -                try_shrink (obj, result, stats') (stats, badobjs)
  15.107 -              else
  15.108 -                status' (obj, result, (stats', badobjs))
  15.109 -          in iter (next stream, (stats', badobjs')) end
  15.110 -  in
  15.111 -    fn stream => iter (next stream, (s0, []))
  15.112 -  end
  15.113 -
  15.114 -fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
  15.115 -fun check ctxt = check' ctxt Property.stats
  15.116 -fun checks ctxt = cpsCheck ctxt Property.stats
  15.117 -
  15.118 -fun checkGen ctxt (gen, show) (tag, prop) =
  15.119 -  check' ctxt {count = 0, tags = [("__GEN", 0)]}
  15.120 -    (limit ctxt gen, show) (tag, prop) Generator.stream
  15.121 -
  15.122 -fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
  15.123 -  cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
  15.124 -    (limit ctxt gen, show) (tag, prop) Generator.stream
  15.125 -
  15.126 -fun checkOne ctxt show (tag, prop) obj =
  15.127 -  check ctxt (List.getItem, show) (tag, prop) [obj]
  15.128 -
  15.129 -(*call the compiler and pass resulting type string to the parser*)
  15.130 -fun determine_type ctxt s =
  15.131 -  let
  15.132 -    val return = Unsynchronized.ref "return"
  15.133 -    val use_context : use_context =
  15.134 -     {tune_source = #tune_source ML_Env.local_context,
  15.135 -      name_space = #name_space ML_Env.local_context,
  15.136 -      str_of_pos = #str_of_pos ML_Env.local_context,
  15.137 -      print = fn r => return := r,
  15.138 -      error = #error ML_Env.local_context}
  15.139 -    val _ =
  15.140 -      Context.setmp_thread_data (SOME (Context.Proof ctxt))
  15.141 -        (fn () => Secure.use_text use_context (0, "generated code") true s) ()
  15.142 -  in
  15.143 -    Gen_Construction.parse_pred (! return)
  15.144 -  end;
  15.145 -
  15.146 -(*call the compiler and run the test*)
  15.147 -fun run_test ctxt s =
  15.148 -  Context.setmp_thread_data (SOME (Context.Proof ctxt))
  15.149 -    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
  15.150 -
  15.151 -(*split input into tokens*)
  15.152 -fun input_split s =
  15.153 -  let
  15.154 -    fun dot c = c = #"."
  15.155 -    fun space c = c = #" "
  15.156 -    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
  15.157 -  in
  15.158 -   (String.tokens space (Substring.string head),
  15.159 -    Substring.string (Substring.dropl dot code))
  15.160 -  end;
  15.161 -
  15.162 -(*create the function from the input*)
  15.163 -fun make_fun s =
  15.164 -  let
  15.165 -    val scan_param = Scan.one (fn s => s <> ";")
  15.166 -    fun parameters s = Scan.repeat1 scan_param s
  15.167 -    val p = $$ "ALL" |-- parameters
  15.168 -    val (split, code) = input_split s
  15.169 -    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
  15.170 -    val (params, _) = Scan.finite stop p split
  15.171 -  in "fn (" ^ commas params ^ ") => " ^ code end;
  15.172 -
  15.173 -(*read input and perform the test*)
  15.174 -fun gen_check_property check ctxt s =
  15.175 -  let
  15.176 -    val func = make_fun s
  15.177 -    val (_, ty) = determine_type ctxt func
  15.178 -  in run_test ctxt (check ctxt "Check" (ty, func)) end;
  15.179 -
  15.180 -val check_property = gen_check_property Gen_Construction.build_check
  15.181 -(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
  15.182 -
  15.183 -(*perform test for specification function*)
  15.184 -fun gen_check_property_f check ctxt s =
  15.185 -  let
  15.186 -    val (name, ty) = determine_type ctxt s
  15.187 -  in run_test ctxt (check ctxt name (ty, s)) end;
  15.188 -
  15.189 -val check_property_f = gen_check_property_f Gen_Construction.build_check
  15.190 -(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
  15.191 -
  15.192 -end;
  15.193 -
  15.194 -fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
  15.195 -
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/Spec_Check/Examples.thy	Fri Aug 23 12:40:55 2013 +0200
    16.3 @@ -0,0 +1,83 @@
    16.4 +theory Examples
    16.5 +imports Spec_Check
    16.6 +begin
    16.7 +
    16.8 +section {* List examples *}
    16.9 +
   16.10 +ML_command {*
   16.11 +check_property "ALL xs. rev xs = xs";
   16.12 +*}
   16.13 +
   16.14 +ML_command {*
   16.15 +check_property "ALL xs. rev (rev xs) = xs";
   16.16 +*}
   16.17 +
   16.18 +
   16.19 +section {* AList Specification *}
   16.20 +
   16.21 +ML_command {*
   16.22 +(* map_entry applies the function to the element *)
   16.23 +check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
   16.24 +*}
   16.25 +
   16.26 +ML_command {*
   16.27 +(* update always results in an entry *)
   16.28 +check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
   16.29 +*}
   16.30 +
   16.31 +ML_command {*
   16.32 +(* update always writes the value *)
   16.33 +check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
   16.34 +*}
   16.35 +
   16.36 +ML_command {*
   16.37 +(* default always results in an entry *)
   16.38 +check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
   16.39 +*}
   16.40 +
   16.41 +ML_command {*
   16.42 +(* delete always removes the entry *)
   16.43 +check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
   16.44 +*}
   16.45 +
   16.46 +ML_command {*
   16.47 +(* default writes the entry iff it didn't exist *)
   16.48 +check_property "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))";
   16.49 +*}
   16.50 +
   16.51 +section {* Examples on Types and Terms *}
   16.52 +
   16.53 +ML_command {*
   16.54 +check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
   16.55 +*}
   16.56 +
   16.57 +ML_command {*
   16.58 +check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
   16.59 +*}
   16.60 +
   16.61 +
   16.62 +text {* One would think this holds: *}
   16.63 +
   16.64 +ML_command {*
   16.65 +check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
   16.66 +*}
   16.67 +
   16.68 +text {* But it only holds with this precondition: *}
   16.69 +
   16.70 +ML_command {*
   16.71 +check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
   16.72 +*}
   16.73 +
   16.74 +section {* Some surprises *}
   16.75 +
   16.76 +ML_command {*
   16.77 +check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
   16.78 +*}
   16.79 +
   16.80 +
   16.81 +ML_command {*
   16.82 +val thy = @{theory};
   16.83 +check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
   16.84 +*}
   16.85 +
   16.86 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Tools/Spec_Check/README	Fri Aug 23 12:40:55 2013 +0200
    17.3 @@ -0,0 +1,47 @@
    17.4 +This is a Quickcheck tool for Isabelle/ML.
    17.5 +
    17.6 +Authors
    17.7 +
    17.8 +  Lukas Bulwahn
    17.9 +  Nicolai Schaffroth
   17.10 +
   17.11 +Quick Usage
   17.12 +
   17.13 +  - Import Spec_Check.thy in your development
   17.14 +  - Look at examples in Examples.thy
   17.15 +  - write specifications with the ML invocation
   17.16 +      check_property "ALL x. P x"
   17.17 +
   17.18 +Notes
   17.19 +
   17.20 +Our specification-based testing tool originated from Christopher League's
   17.21 +QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
   17.22 +provides a rich and uniform ML platform (called Isabelle/ML), this
   17.23 +testing tools is very different than the one for a typical ML developer.
   17.24 +
   17.25 +1. Isabelle/ML provides common data structures, which we can use in the
   17.26 +tool's implementation for storing data and printing output.
   17.27 +
   17.28 +2. The implementation in Isabelle that will be checked with this tool
   17.29 +commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
   17.30 +but they do not use other integer types in ML, such as ML's Int.int,
   17.31 +Word.word and others.
   17.32 +
   17.33 +3. As Isabelle can run heavily in parallel, we avoid reference types.
   17.34 +
   17.35 +4. Isabelle has special naming conventions and documentation of source
   17.36 +code is only minimal to avoid parroting.
   17.37 +
   17.38 +Next steps:
   17.39 +  - Remove all references and store the neccessary random seed in the
   17.40 +    Isabelle's context.
   17.41 +  - Simplify some existing random generators.
   17.42 +    The original ones from Christopher League are so complicated to
   17.43 +    support many integer types uniformly.
   17.44 +
   17.45 +License
   17.46 +
   17.47 +  The source code originated from Christopher League's QCheck, which is
   17.48 +  licensed under the 2-clause BSD license. The current source code is
   17.49 +  licensed under the compatible 3-clause BSD license of Isabelle.
   17.50 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Tools/Spec_Check/Spec_Check.thy	Fri Aug 23 12:40:55 2013 +0200
    18.3 @@ -0,0 +1,14 @@
    18.4 +theory Spec_Check
    18.5 +imports Pure
    18.6 +begin
    18.7 +
    18.8 +ML_file "random.ML"
    18.9 +ML_file "property.ML"
   18.10 +ML_file "base_generator.ML"
   18.11 +ML_file "generator.ML"
   18.12 +ML_file "gen_construction.ML"
   18.13 +ML_file "spec_check.ML"
   18.14 +ML_file "output_style.ML"
   18.15 +setup Output_Style.setup
   18.16 +
   18.17 +end
   18.18 \ No newline at end of file
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/Tools/Spec_Check/base_generator.ML	Fri Aug 23 12:40:55 2013 +0200
    19.3 @@ -0,0 +1,201 @@
    19.4 +(*  Title:      Tools/Spec_Check/base_generator.ML
    19.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    19.6 +    Author:     Christopher League
    19.7 +
    19.8 +Basic random generators.
    19.9 +*)
   19.10 +
   19.11 +signature BASE_GENERATOR =
   19.12 +sig
   19.13 +
   19.14 +type rand
   19.15 +type 'a gen = rand -> 'a * rand
   19.16 +type ('a, 'b) co = 'a -> 'b gen -> 'b gen
   19.17 +
   19.18 +val new : unit -> rand
   19.19 +val range : int * int -> rand -> int * rand
   19.20 +type ('a, 'b) reader = 'b -> ('a * 'b) option
   19.21 +
   19.22 +val lift : 'a -> 'a gen
   19.23 +val select : 'a vector -> 'a gen
   19.24 +val choose : 'a gen vector -> 'a gen
   19.25 +val choose' : (int * 'a gen) vector -> 'a gen
   19.26 +val selectL : 'a list -> 'a gen
   19.27 +val chooseL : 'a gen list -> 'a gen
   19.28 +val chooseL' : (int * 'a gen) list -> 'a gen
   19.29 +val filter : ('a -> bool) -> 'a gen -> 'a gen
   19.30 +
   19.31 +val zip : ('a gen * 'b gen) -> ('a * 'b) gen
   19.32 +val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
   19.33 +val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
   19.34 +val map : ('a -> 'b) -> 'a gen -> 'b gen
   19.35 +val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
   19.36 +val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
   19.37 +val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
   19.38 +
   19.39 +val flip : bool gen
   19.40 +val flip' : int * int -> bool gen
   19.41 +
   19.42 +val list : bool gen -> 'a gen -> 'a list gen
   19.43 +val option : bool gen -> 'a gen -> 'a option gen
   19.44 +val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
   19.45 +
   19.46 +val variant : (int, 'b) co
   19.47 +val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
   19.48 +val cobool : (bool, 'b) co
   19.49 +val colist : ('a, 'b) co -> ('a list, 'b) co
   19.50 +val coopt : ('a, 'b) co -> ('a option, 'b) co
   19.51 +
   19.52 +type stream
   19.53 +val start : rand -> stream
   19.54 +val limit : int -> 'a gen -> ('a, stream) reader
   19.55 +
   19.56 +end
   19.57 +
   19.58 +structure Base_Generator : BASE_GENERATOR =
   19.59 +struct
   19.60 +
   19.61 +(* random number engine *)
   19.62 +
   19.63 +type rand = real
   19.64 +
   19.65 +val a = 16807.0
   19.66 +val m = 2147483647.0
   19.67 +
   19.68 +fun nextrand seed =
   19.69 +  let
   19.70 +    val t = a * seed
   19.71 +  in
   19.72 +    t - m * real (floor (t / m))
   19.73 +  end
   19.74 +
   19.75 +val new = nextrand o Time.toReal o Time.now
   19.76 +
   19.77 +fun range (min, max) =
   19.78 +  if min > max then raise Domain (* TODO: raise its own error *)
   19.79 +  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
   19.80 +
   19.81 +fun split r =
   19.82 +  let
   19.83 +    val r = r / a
   19.84 +    val r0 = real (floor r)
   19.85 +    val r1 = r - r0
   19.86 +  in
   19.87 +    (nextrand r0, nextrand r1)
   19.88 +  end
   19.89 +
   19.90 +(* generators *)
   19.91 +
   19.92 +type 'a gen = rand -> 'a * rand
   19.93 +type ('a, 'b) reader = 'b -> ('a * 'b) option
   19.94 +
   19.95 +fun lift obj r = (obj, r)
   19.96 +
   19.97 +local (* Isabelle does not use vectors? *)
   19.98 +  fun explode ((freq, gen), acc) =
   19.99 +    List.tabulate (freq, fn _ => gen) @ acc
  19.100 +in
  19.101 +  fun choose v r =
  19.102 +    let val (i, r) = range(0, Vector.length v - 1) r
  19.103 +    in Vector.sub (v, i) r end
  19.104 +  fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
  19.105 +  fun select v = choose (Vector.map lift v)
  19.106 +end
  19.107 +
  19.108 +fun chooseL l = choose (Vector.fromList l)
  19.109 +fun chooseL' l = choose' (Vector.fromList l)
  19.110 +fun selectL l = select (Vector.fromList l)
  19.111 +
  19.112 +fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
  19.113 +
  19.114 +fun zip3 (g1, g2, g3) =
  19.115 +  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
  19.116 +
  19.117 +fun zip4 (g1, g2, g3, g4) =
  19.118 +  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
  19.119 +
  19.120 +fun map f g = apfst f o g
  19.121 +
  19.122 +fun map2 f = map f o zip
  19.123 +fun map3 f = map f o zip3
  19.124 +fun map4 f = map f o zip4
  19.125 +
  19.126 +fun filter p gen r =
  19.127 +  let
  19.128 +    fun loop (x, r) = if p x then (x, r) else loop (gen r)
  19.129 +  in
  19.130 +    loop (gen r)
  19.131 +  end
  19.132 +
  19.133 +val flip = selectL [true, false]
  19.134 +fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
  19.135 +
  19.136 +fun list flip g r =
  19.137 +  case flip r of
  19.138 +      (true, r) => ([], r)
  19.139 +    | (false, r) =>
  19.140 +      let
  19.141 +        val (x,r) = g r
  19.142 +        val (xs,r) = list flip g r
  19.143 +      in (x::xs, r) end
  19.144 +
  19.145 +fun option flip g r =
  19.146 +  case flip r of
  19.147 +    (true, r) => (NONE, r)
  19.148 +  | (false, r) => map SOME g r
  19.149 +
  19.150 +fun vector tabulate (int, elem) r =
  19.151 +  let
  19.152 +    val (n, r) = int r
  19.153 +    val p = Unsynchronized.ref r
  19.154 +    fun g _ =
  19.155 +      let
  19.156 +        val (x,r) = elem(!p)
  19.157 +      in x before p := r end
  19.158 +  in
  19.159 +    (tabulate(n, g), !p)
  19.160 +  end
  19.161 +
  19.162 +type stream = rand Unsynchronized.ref * int
  19.163 +
  19.164 +fun start r = (Unsynchronized.ref r, 0)
  19.165 +
  19.166 +fun limit max gen =
  19.167 +  let
  19.168 +    fun next (p, i) =
  19.169 +      if i >= max then NONE
  19.170 +      else
  19.171 +        let val (x, r) = gen(!p)
  19.172 +        in SOME(x, (p, i+1)) before p := r end
  19.173 +  in
  19.174 +    next
  19.175 +  end
  19.176 +
  19.177 +type ('a, 'b) co = 'a -> 'b gen -> 'b gen
  19.178 +
  19.179 +fun variant v g r =
  19.180 +  let
  19.181 +    fun nth (i, r) =
  19.182 +      let val (r1, r2) = split r
  19.183 +      in if i = 0 then r1 else nth (i-1, r2) end
  19.184 +  in
  19.185 +    g (nth (v, r))
  19.186 +  end
  19.187 +
  19.188 +fun arrow (cogen, gen) r =
  19.189 +  let
  19.190 +    val (r1, r2) = split r
  19.191 +    fun g x = fst (cogen x gen r1)
  19.192 +  in (g, r2) end
  19.193 +
  19.194 +fun cobool false = variant 0
  19.195 +  | cobool true = variant 1
  19.196 +
  19.197 +fun colist _ [] = variant 0
  19.198 +  | colist co (x::xs) = variant 1 o co x o colist co xs
  19.199 +
  19.200 +fun coopt _ NONE = variant 0
  19.201 +  | coopt co (SOME x) = variant 1 o co x
  19.202 +
  19.203 +end
  19.204 +
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Tools/Spec_Check/gen_construction.ML	Fri Aug 23 12:40:55 2013 +0200
    20.3 @@ -0,0 +1,179 @@
    20.4 +(*  Title:      Tools/Spec_Check/gen_construction.ML
    20.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    20.6 +    Author:     Christopher League
    20.7 +
    20.8 +Constructing generators and pretty printing function for complex types.
    20.9 +*)
   20.10 +
   20.11 +signature GEN_CONSTRUCTION =
   20.12 +sig
   20.13 +  val register : string * (string * string) -> theory -> theory
   20.14 +  type mltype
   20.15 +  val parse_pred : string -> string * mltype
   20.16 +  val build_check : Proof.context -> string -> mltype * string -> string
   20.17 +  (*val safe_check : string -> mltype * string -> string*)
   20.18 +  val string_of_bool : bool -> string
   20.19 +  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
   20.20 +end;
   20.21 +
   20.22 +structure Gen_Construction : GEN_CONSTRUCTION =
   20.23 +struct
   20.24 +
   20.25 +(* Parsing ML types *)
   20.26 +
   20.27 +datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
   20.28 +
   20.29 +(*Split string into tokens for parsing*)
   20.30 +fun split s =
   20.31 +  let
   20.32 +    fun split_symbol #"(" = "( "
   20.33 +      | split_symbol #")" = " )"
   20.34 +      | split_symbol #"," = " ,"
   20.35 +      | split_symbol #":" = " :"
   20.36 +      | split_symbol c = Char.toString c
   20.37 +    fun is_space c = c = #" "
   20.38 +  in String.tokens is_space (String.translate split_symbol s) end;
   20.39 +
   20.40 +(*Accept anything that is not a recognized symbol*)
   20.41 +val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
   20.42 +
   20.43 +(*Turn a type list into a nested Con*)
   20.44 +fun make_con [] = raise Empty
   20.45 +  | make_con [c] = c
   20.46 +  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
   20.47 +
   20.48 +(*Parse a type*)
   20.49 +fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
   20.50 +
   20.51 +and parse_type_arg s = (parse_tuple || parse_type_single) s
   20.52 +
   20.53 +and parse_type_single s = (parse_con || parse_type_basic) s
   20.54 +
   20.55 +and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
   20.56 +
   20.57 +and parse_list s =
   20.58 +  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
   20.59 +
   20.60 +and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
   20.61 +
   20.62 +and parse_con s = ((parse_con_nest
   20.63 +  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
   20.64 +  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
   20.65 +  >> (make_con o rev)) s
   20.66 +
   20.67 +and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
   20.68 +
   20.69 +and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
   20.70 +
   20.71 +and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
   20.72 +  >> (fn (t, tl) => Tuple (t :: tl))) s;
   20.73 +
   20.74 +(*Parse entire type + name*)
   20.75 +fun parse_function s =
   20.76 +  let
   20.77 +    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
   20.78 +    val (name, ty) = p (split s)
   20.79 +    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
   20.80 +    val (typ, _) = Scan.finite stop parse_type ty
   20.81 +  in (name, typ) end;
   20.82 +
   20.83 +(*Create desired output*)
   20.84 +fun parse_pred s =
   20.85 +  let
   20.86 +    val (name, Con ("->", t :: _)) = parse_function s
   20.87 +  in (name, t) end;
   20.88 +
   20.89 +(* Construct Generators and Pretty Printers *)
   20.90 +
   20.91 +(*copied from smt_config.ML *)
   20.92 +fun string_of_bool b = if b then "true" else "false"
   20.93 +
   20.94 +fun string_of_ref f r = f (!r) ^ " ref";
   20.95 +
   20.96 +val initial_content = Symtab.make
   20.97 +  [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
   20.98 +  ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
   20.99 +  ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
  20.100 +  ("unit", ("gen_unit", "fn () => \"()\"")),
  20.101 +  ("int", ("Generator.int", "string_of_int")),
  20.102 +  ("real", ("Generator.real", "string_of_real")),
  20.103 +  ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
  20.104 +  ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
  20.105 +  ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
  20.106 +  ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
  20.107 +  ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
  20.108 +
  20.109 +structure Data = Theory_Data
  20.110 +(
  20.111 +  type T = (string * string) Symtab.table
  20.112 +  val empty = initial_content
  20.113 +  val extend = I
  20.114 +  fun merge data : T = Symtab.merge (K true) data
  20.115 +)
  20.116 +
  20.117 +fun data_of ctxt tycon =
  20.118 +  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
  20.119 +    SOME data => data
  20.120 +  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
  20.121 +
  20.122 +val generator_of = fst oo data_of
  20.123 +val printer_of = snd oo data_of
  20.124 +
  20.125 +fun register (ty, data) = Data.map (Symtab.update (ty, data))
  20.126 +
  20.127 +(*
  20.128 +fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
  20.129 +*)
  20.130 +
  20.131 +fun combine dict [] = dict
  20.132 +  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
  20.133 +
  20.134 +fun compose_generator _ Var = "Generator.int"
  20.135 +  | compose_generator ctxt (Con (s, types)) =
  20.136 +      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
  20.137 +  | compose_generator ctxt (Tuple t) =
  20.138 +      let
  20.139 +        fun tuple_body t = space_implode ""
  20.140 +          (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
  20.141 +          compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
  20.142 +        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
  20.143 +      in
  20.144 +        "fn r0 => let " ^ tuple_body t ^
  20.145 +        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
  20.146 +      end;
  20.147 +
  20.148 +fun compose_printer _ Var = "Int.toString"
  20.149 +  | compose_printer ctxt (Con (s, types)) =
  20.150 +      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
  20.151 +  | compose_printer ctxt (Tuple t) =
  20.152 +      let
  20.153 +        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
  20.154 +        fun tuple_body t = space_implode " ^ \", \" ^ "
  20.155 +          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
  20.156 +          (t ~~ (1 upto (length t))))
  20.157 +      in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
  20.158 +
  20.159 +(*produce compilable string*)
  20.160 +fun build_check ctxt name (ty, spec) =
  20.161 +  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
  20.162 +  ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
  20.163 +  ^ name ^ "\", Property.pred (" ^ spec ^ "));";
  20.164 +
  20.165 +(*produce compilable string - non-eqtype functions*)
  20.166 +(*
  20.167 +fun safe_check name (ty, spec) =
  20.168 +  let
  20.169 +    val default =
  20.170 +      (case AList.lookup (op =) (!gen_table) "->" of
  20.171 +        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
  20.172 +      | SOME entry => entry)
  20.173 +  in
  20.174 +   (gen_table :=
  20.175 +     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
  20.176 +    build_check name (ty, spec) before
  20.177 +    gen_table := AList.update (op =) ("->", default) (!gen_table))
  20.178 +  end;
  20.179 +*)
  20.180 +
  20.181 +end;
  20.182 +
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/Tools/Spec_Check/generator.ML	Fri Aug 23 12:40:55 2013 +0200
    21.3 @@ -0,0 +1,235 @@
    21.4 +(*  Title:      Tools/Spec_Check/generator.ML
    21.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    21.6 +    Author:     Christopher League
    21.7 +
    21.8 +Random generators for Isabelle/ML's types.
    21.9 +*)
   21.10 +
   21.11 +signature GENERATOR = sig
   21.12 +  include BASE_GENERATOR
   21.13 +  (* text generators *)
   21.14 +  val char : char gen
   21.15 +  val charRange : char * char -> char gen
   21.16 +  val charFrom : string -> char gen
   21.17 +  val charByType : (char -> bool) -> char gen
   21.18 +  val string : (int gen * char gen) -> string gen
   21.19 +  val substring : string gen -> substring gen
   21.20 +  val cochar : (char, 'b) co
   21.21 +  val costring : (string, 'b) co
   21.22 +  val cosubstring : (substring, 'b) co
   21.23 +  (* integer generators *)
   21.24 +  val int : int gen
   21.25 +  val int_pos : int gen
   21.26 +  val int_neg : int gen
   21.27 +  val int_nonpos : int gen
   21.28 +  val int_nonneg : int gen
   21.29 +  val coint : (int, 'b) co
   21.30 +  (* real generators *)
   21.31 +  val real : real gen
   21.32 +  val real_frac : real gen
   21.33 +  val real_pos : real gen
   21.34 +  val real_neg : real gen
   21.35 +  val real_nonpos : real gen
   21.36 +  val real_nonneg : real gen
   21.37 +  val real_finite : real gen
   21.38 +  (* function generators *)
   21.39 +  val function_const : 'c * 'b gen -> ('a -> 'b) gen
   21.40 +  val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
   21.41 +  val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
   21.42 +  val unit : unit gen
   21.43 +  val ref' : 'a gen -> 'a Unsynchronized.ref gen
   21.44 +  (* more generators *)
   21.45 +  val term : int -> term gen
   21.46 +  val typ : int -> typ gen
   21.47 +
   21.48 +  val stream : stream
   21.49 +end
   21.50 +
   21.51 +structure Generator : GENERATOR =
   21.52 +struct
   21.53 +
   21.54 +open Base_Generator
   21.55 +
   21.56 +val stream = start (new())
   21.57 +
   21.58 +type 'a gen = rand -> 'a * rand
   21.59 +type ('a, 'b) co = 'a -> 'b gen -> 'b gen
   21.60 +
   21.61 +(* text *)
   21.62 +
   21.63 +type char = Char.char
   21.64 +type string = String.string
   21.65 +type substring = Substring.substring
   21.66 +
   21.67 +
   21.68 +val char = map Char.chr (range (0, Char.maxOrd))
   21.69 +fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
   21.70 +
   21.71 +fun charFrom s =
   21.72 +  choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
   21.73 +
   21.74 +fun charByType p = filter p char
   21.75 +
   21.76 +val string = vector CharVector.tabulate
   21.77 +
   21.78 +fun substring gen r =
   21.79 +  let
   21.80 +    val (s, r') = gen r
   21.81 +    val (i, r'') = range (0, String.size s) r'
   21.82 +    val (j, r''') = range (0, String.size s - i) r''
   21.83 +  in
   21.84 +    (Substring.substring (s, i, j), r''')
   21.85 +  end
   21.86 +
   21.87 +fun cochar c =
   21.88 +  if Char.ord c = 0 then variant 0
   21.89 +  else variant 1 o cochar (Char.chr (Char.ord c div 2))
   21.90 +
   21.91 +fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
   21.92 +
   21.93 +fun costring s = cosubstring (Substring.full s)
   21.94 +
   21.95 +(* integers *)
   21.96 +val digit = charRange (#"0", #"9")
   21.97 +val nonzero = string (lift 1, charRange (#"1", #"9"))
   21.98 +fun digits' n = string (range (0, n-1), digit)
   21.99 +fun digits n = map2 op^ (nonzero, digits' n)
  21.100 +
  21.101 +val maxDigits = 64
  21.102 +val ratio = 49
  21.103 +
  21.104 +fun pos_or_neg f r =
  21.105 +  let
  21.106 +    val (s, r') = digits maxDigits r
  21.107 +  in (f (the (Int.fromString s)), r') end
  21.108 +
  21.109 +val int_pos = pos_or_neg I
  21.110 +val int_neg = pos_or_neg Int.~
  21.111 +val zero = lift 0
  21.112 +
  21.113 +val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
  21.114 +val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
  21.115 +val int = chooseL [int_nonneg, int_nonpos]
  21.116 +
  21.117 +fun coint n =
  21.118 +  if n = 0 then variant 0
  21.119 +  else if n < 0 then variant 1 o coint (~ n)
  21.120 +  else variant 2 o coint (n div 2)
  21.121 +
  21.122 +(* reals *)
  21.123 +val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
  21.124 +
  21.125 +fun real_frac r =
  21.126 +  let val (s, r') = digits r
  21.127 +  in (the (Real.fromString s), r') end
  21.128 +
  21.129 +val {exp=minExp,...} = Real.toManExp Real.minPos
  21.130 +val {exp=maxExp,...} = Real.toManExp Real.posInf
  21.131 +
  21.132 +val ratio = 99
  21.133 +
  21.134 +fun mk r =
  21.135 +  let
  21.136 +    val (a, r') = digits r
  21.137 +    val (b, r'') = digits r'
  21.138 +    val (e, r''') = range (minExp div 4, maxExp div 4) r''
  21.139 +    val x = String.concat [a, ".", b, "E", Int.toString e]
  21.140 +  in
  21.141 +    (the (Real.fromString x), r''')
  21.142 +  end
  21.143 +
  21.144 +val real_pos = chooseL' (List.map ((pair 1) o lift)
  21.145 +    [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
  21.146 +
  21.147 +val real_neg = map Real.~ real_pos
  21.148 +
  21.149 +val real_zero = Real.fromInt 0
  21.150 +val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
  21.151 +val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
  21.152 +
  21.153 +val real = chooseL [real_nonneg, real_nonpos]
  21.154 +
  21.155 +val real_finite = filter Real.isFinite real
  21.156 +
  21.157 +(*alternate list generator - uses an integer generator to determine list length*)
  21.158 +fun list' int gen = vector List.tabulate (int, gen);
  21.159 +
  21.160 +(* more function generators *)
  21.161 +
  21.162 +fun function_const (_, gen2) r =
  21.163 +  let
  21.164 +    val (v, r') = gen2 r
  21.165 +  in (fn _ => v, r') end;
  21.166 +
  21.167 +fun function_strict size (gen1, gen2) r =
  21.168 +  let
  21.169 +    val (def, r') = gen2 r
  21.170 +    val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
  21.171 +  in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
  21.172 +
  21.173 +fun function_lazy (gen1, gen2) r =
  21.174 +  let
  21.175 +    val (initial1, r') = gen1 r
  21.176 +    val (initial2, internal) = gen2 r'
  21.177 +    val seed = Unsynchronized.ref internal
  21.178 +    val table = Unsynchronized.ref [(initial1, initial2)]
  21.179 +    fun new_entry k =
  21.180 +      let
  21.181 +        val (new_val, new_seed) = gen2 (!seed)
  21.182 +        val _ =  seed := new_seed
  21.183 +        val _ = table := AList.update (op =) (k, new_val) (!table)
  21.184 +      in new_val end
  21.185 +  in
  21.186 +    (fn v1 =>
  21.187 +      case AList.lookup (op =) (!table) v1 of
  21.188 +        NONE => new_entry v1
  21.189 +      | SOME v2 => v2, r')
  21.190 +  end;
  21.191 +
  21.192 +(* unit *)
  21.193 +
  21.194 +fun unit r = ((), r);
  21.195 +
  21.196 +(* references *)
  21.197 +
  21.198 +fun ref' gen r =
  21.199 +  let val (value, r') = gen r
  21.200 +  in (Unsynchronized.ref value, r') end;
  21.201 +
  21.202 +(* types and terms *)
  21.203 +
  21.204 +val sort_string = selectL ["sort1", "sort2", "sort3"];
  21.205 +val type_string = selectL ["TCon1", "TCon2", "TCon3"];
  21.206 +val tvar_string = selectL ["a", "b", "c"];
  21.207 +
  21.208 +val const_string = selectL ["c1", "c2", "c3"];
  21.209 +val var_string = selectL ["x", "y", "z"];
  21.210 +val index = selectL [0, 1, 2, 3];
  21.211 +val bound_index = selectL [0, 1, 2, 3];
  21.212 +
  21.213 +val sort = list (flip' (1, 2)) sort_string;
  21.214 +
  21.215 +fun typ n =
  21.216 +  let
  21.217 +    fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
  21.218 +    val tfree = map TFree (zip (tvar_string, sort))
  21.219 +    val tvar = map TVar (zip (zip (tvar_string, index), sort))
  21.220 +  in
  21.221 +    if n = 0 then chooseL [tfree, tvar]
  21.222 +    else chooseL [type' (n div 2), tfree, tvar]
  21.223 +  end;
  21.224 +
  21.225 +fun term n =
  21.226 +  let
  21.227 +    val const = map Const (zip (const_string, typ 10))
  21.228 +    val free = map Free (zip (var_string, typ 10))
  21.229 +    val var = map Var (zip (zip (var_string, index), typ 10))
  21.230 +    val bound = map Bound bound_index
  21.231 +    fun abs m = map Abs (zip3 (var_string, typ 10, term m))
  21.232 +    fun app m = map (op $) (zip (term m, term m))
  21.233 +  in
  21.234 +    if n = 0 then chooseL [const, free, var, bound]
  21.235 +    else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
  21.236 +  end;
  21.237 +
  21.238 +end
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/Tools/Spec_Check/output_style.ML	Fri Aug 23 12:40:55 2013 +0200
    22.3 @@ -0,0 +1,119 @@
    22.4 +(*  Title:      Tools/Spec_Check/output_style.ML
    22.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    22.6 +    Author:     Christopher League
    22.7 +
    22.8 +Output styles for presenting Spec_Check's results.
    22.9 +*)
   22.10 +
   22.11 +signature OUTPUT_STYLE =
   22.12 +sig
   22.13 +  val setup : theory -> theory
   22.14 +end
   22.15 +
   22.16 +structure Output_Style : OUTPUT_STYLE =
   22.17 +struct
   22.18 +
   22.19 +(* perl style *)
   22.20 +
   22.21 +val perl_style =
   22.22 +  Spec_Check.register_style "Perl"
   22.23 +    (fn ctxt => fn tag =>
   22.24 +      let
   22.25 +        val target = Config.get ctxt Spec_Check.gen_target
   22.26 +        val namew = Config.get ctxt Spec_Check.column_width
   22.27 +        val sort_examples = Config.get ctxt Spec_Check.sort_examples
   22.28 +        val show_stats = Config.get ctxt Spec_Check.show_stats
   22.29 +        val limit = Config.get ctxt Spec_Check.examples
   22.30 +
   22.31 +        val resultw = 8
   22.32 +        val countw = 20
   22.33 +        val allw = namew + resultw + countw + 2
   22.34 +
   22.35 +        val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I
   22.36 +
   22.37 +        fun result ({count = 0, ...}, _) _ = "dubious"
   22.38 +          | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
   22.39 +          | result ({count, tags}, badobjs) true =
   22.40 +              if not (null badobjs) then "FAILED"
   22.41 +              else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
   22.42 +              else "ok"
   22.43 +
   22.44 +        fun ratio (0, _) = "(0/0 passed)"
   22.45 +          | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
   22.46 +          | ratio (count, n) =
   22.47 +              "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
   22.48 +
   22.49 +        fun update (stats, badobjs) donep =
   22.50 +          "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
   22.51 +          StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
   22.52 +          StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
   22.53 +
   22.54 +        fun status (_, result, (stats, badobjs)) =
   22.55 +          if Property.failure result then warning (update (stats, badobjs) false) else ()
   22.56 +
   22.57 +        fun prtag count (tag, n) first =
   22.58 +          if String.isPrefix "__" tag then ("", first)
   22.59 +          else
   22.60 +             let
   22.61 +               val ratio = round ((real n / real count) * 100.0)
   22.62 +             in
   22.63 +               (((if first then "" else StringCvt.padRight #" " allw "\n") ^
   22.64 +                 StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
   22.65 +               false)
   22.66 +             end
   22.67 +
   22.68 +        fun prtags ({count, tags} : Property.stats) =
   22.69 +          if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
   22.70 +
   22.71 +        fun err badobjs =
   22.72 +          let
   22.73 +            fun iter [] _ = ()
   22.74 +              | iter (e :: es) k =
   22.75 +                  (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
   22.76 +                    StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
   22.77 +                  iter es (k + 1))
   22.78 +          in
   22.79 +            iter (maybe_sort (take limit (map_filter I badobjs))) 0
   22.80 +          end
   22.81 +
   22.82 +        fun finish (stats, badobjs) =
   22.83 +          if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
   22.84 +          else (warning (update (stats, badobjs) true); err badobjs)
   22.85 +      in
   22.86 +        {status = status, finish = finish}
   22.87 +      end)
   22.88 +
   22.89 +
   22.90 +(* CM style: meshes with CM output; highlighted in sml-mode *)
   22.91 +
   22.92 +val cm_style =
   22.93 +  Spec_Check.register_style "CM"
   22.94 +    (fn ctxt => fn tag =>
   22.95 +      let
   22.96 +        fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
   22.97 +        val gen_target = Config.get ctxt Spec_Check.gen_target
   22.98 +        val _ = writeln ("[testing " ^ tag ^ "... ")
   22.99 +        fun finish ({count, ...} : Property.stats, badobjs) =
  22.100 +          (case (count, badobjs) of
  22.101 +            (0, []) => warning ("no valid cases generated]")
  22.102 +          | (n, []) => writeln (
  22.103 +                if n >= gen_target then "ok]"
  22.104 +                else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
  22.105 +          | (_, es) =>
  22.106 +              let
  22.107 +                val wd = size (string_of_int (length es))
  22.108 +                fun each (NONE, _) = ()
  22.109 +                  | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
  22.110 +              in
  22.111 +                (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
  22.112 +              end)
  22.113 +      in
  22.114 +        {status = K (), finish = finish}
  22.115 +      end)
  22.116 +
  22.117 +
  22.118 +(* setup *)
  22.119 +
  22.120 +val setup = perl_style #> cm_style
  22.121 +
  22.122 +end
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/Tools/Spec_Check/property.ML	Fri Aug 23 12:40:55 2013 +0200
    23.3 @@ -0,0 +1,77 @@
    23.4 +(*  Title:      Tools/Spec_Check/property.ML
    23.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    23.6 +    Author:     Christopher League
    23.7 +
    23.8 +Conditional properties that can track argument distribution.
    23.9 +*)
   23.10 +
   23.11 +signature PROPERTY =
   23.12 +sig
   23.13 +
   23.14 +type 'a pred = 'a -> bool
   23.15 +type 'a prop
   23.16 +val pred : 'a pred -> 'a prop
   23.17 +val pred2 : ('a * 'b) pred -> 'b -> 'a  prop
   23.18 +val implies : 'a pred * 'a prop -> 'a prop
   23.19 +val ==> : 'a pred * 'a pred -> 'a prop
   23.20 +val trivial : 'a pred -> 'a prop -> 'a prop
   23.21 +val classify : 'a pred -> string -> 'a prop -> 'a prop
   23.22 +val classify' : ('a -> string option) -> 'a prop -> 'a prop
   23.23 +
   23.24 +(*Results*)
   23.25 +type result = bool option
   23.26 +type stats = { tags : (string * int) list, count : int }
   23.27 +val test : 'a prop -> 'a * stats -> result * stats
   23.28 +val stats : stats
   23.29 +val success : result pred
   23.30 +val failure : result pred
   23.31 +
   23.32 +end
   23.33 +
   23.34 +structure Property : PROPERTY =
   23.35 +struct
   23.36 +
   23.37 +type result = bool option
   23.38 +type stats = { tags : (string * int) list, count : int }
   23.39 +type 'a pred = 'a -> bool
   23.40 +type 'a prop = 'a * stats -> result * stats
   23.41 +
   23.42 +fun success (SOME true) = true
   23.43 +  | success _ = false
   23.44 +
   23.45 +fun failure (SOME false) = true
   23.46 +  | failure _ = false
   23.47 +
   23.48 +fun apply f x = (case try f x of NONE => SOME false | some => some)
   23.49 +fun pred f (x,s) = (apply f x, s)
   23.50 +fun pred2 f z = pred (fn x => f (x, z))
   23.51 +
   23.52 +fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
   23.53 +
   23.54 +fun ==> (p1, p2) = implies (p1, pred p2)
   23.55 +
   23.56 +fun wrap trans p (x,s) =
   23.57 +  let val (result,s) = p (x,s)
   23.58 +  in (result, trans (x, result, s)) end
   23.59 +
   23.60 +fun classify' f =
   23.61 +  wrap (fn (x, result, {tags, count}) =>
   23.62 +    { tags =
   23.63 +        if is_some result then
   23.64 +          (case f x of
   23.65 +            NONE => tags
   23.66 +          | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
   23.67 +        else tags,
   23.68 +     count = count })
   23.69 +
   23.70 +fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
   23.71 +
   23.72 +fun trivial cond = classify cond "trivial"
   23.73 +
   23.74 +fun test p =
   23.75 +  wrap (fn (_, result, {tags, count}) =>
   23.76 +    { tags = tags, count = if is_some result then count + 1 else count }) p
   23.77 +
   23.78 +val stats = { tags = [], count = 0 }
   23.79 +
   23.80 +end
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/Tools/Spec_Check/random.ML	Fri Aug 23 12:40:55 2013 +0200
    24.3 @@ -0,0 +1,46 @@
    24.4 +(*  Title:      Tools/Spec_Check/random.ML
    24.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    24.6 +    Author:     Christopher League
    24.7 +
    24.8 +Random number engine.
    24.9 +*)
   24.10 +
   24.11 +signature RANDOM =
   24.12 +sig
   24.13 +  type rand
   24.14 +  val new : unit -> rand
   24.15 +  val range : int * int -> rand -> int * rand
   24.16 +  val split : rand -> rand * rand
   24.17 +end
   24.18 +
   24.19 +structure Random : RANDOM  =
   24.20 +struct
   24.21 +
   24.22 +type rand = real
   24.23 +
   24.24 +val a = 16807.0
   24.25 +val m = 2147483647.0
   24.26 +
   24.27 +fun nextrand seed =
   24.28 +  let
   24.29 +    val t = a * seed
   24.30 +  in
   24.31 +    t - m * real(floor(t/m))
   24.32 +  end
   24.33 +
   24.34 +val new = nextrand o Time.toReal o Time.now
   24.35 +
   24.36 +fun range (min, max) =
   24.37 +  if min > max then raise Domain (* TODO: raise its own error *)
   24.38 +  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
   24.39 +
   24.40 +fun split r =
   24.41 +  let
   24.42 +    val r = r / a
   24.43 +    val r0 = real(floor r)
   24.44 +    val r1 = r - r0
   24.45 +  in
   24.46 +    (nextrand r0, nextrand r1)
   24.47 +  end
   24.48 +
   24.49 +end
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Fri Aug 23 12:40:55 2013 +0200
    25.3 @@ -0,0 +1,192 @@
    25.4 +(*  Title:      Tools/Spec_Check/spec_check.ML
    25.5 +    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    25.6 +    Author:     Christopher League
    25.7 +
    25.8 +Specification-based testing of ML programs with random values.
    25.9 +*)
   25.10 +
   25.11 +signature SPEC_CHECK =
   25.12 +sig
   25.13 +  val gen_target : int Config.T
   25.14 +  val gen_max : int Config.T
   25.15 +  val examples : int Config.T
   25.16 +  val sort_examples : bool Config.T
   25.17 +  val show_stats : bool Config.T
   25.18 +  val column_width : int Config.T
   25.19 +  val style : string Config.T
   25.20 +
   25.21 +  type output_style = Proof.context -> string ->
   25.22 +    {status : string option * Property.result * (Property.stats  * string option list) -> unit,
   25.23 +     finish: Property.stats * string option list -> unit}
   25.24 +
   25.25 +  val register_style : string -> output_style -> theory -> theory
   25.26 +
   25.27 +  val checkGen : Proof.context ->
   25.28 +    'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
   25.29 +
   25.30 +  val check_property : Proof.context -> string -> unit
   25.31 +end;
   25.32 +
   25.33 +structure Spec_Check : SPEC_CHECK =
   25.34 +struct
   25.35 +
   25.36 +(* configurations *)
   25.37 +
   25.38 +val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
   25.39 +val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
   25.40 +val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)
   25.41 +
   25.42 +val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
   25.43 +val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
   25.44 +val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
   25.45 +val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")
   25.46 +
   25.47 +type ('a, 'b) reader = 'b -> ('a * 'b) option
   25.48 +type 'a rep = ('a -> string) option
   25.49 +
   25.50 +type output_style = Proof.context -> string ->
   25.51 +  {status: string option * Property.result * (Property.stats * string option list) -> unit,
   25.52 +   finish: Property.stats * string option list -> unit}
   25.53 +
   25.54 +fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
   25.55 +
   25.56 +structure Style = Theory_Data
   25.57 +(
   25.58 +  type T = output_style Symtab.table
   25.59 +  val empty = Symtab.empty
   25.60 +  val extend = I
   25.61 +  fun merge data : T = Symtab.merge (K true) data
   25.62 +)
   25.63 +
   25.64 +fun get_style ctxt =
   25.65 +  let val name = Config.get ctxt style in
   25.66 +    (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
   25.67 +      SOME style => style ctxt
   25.68 +    | NONE => error ("No style called " ^ quote name ^ " found"))
   25.69 +  end
   25.70 +
   25.71 +fun register_style name style = Style.map (Symtab.update (name, style))
   25.72 +
   25.73 +
   25.74 +(* testing functions *)
   25.75 +
   25.76 +fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
   25.77 +  let
   25.78 +    val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
   25.79 +
   25.80 +    val {status, finish} = get_style ctxt tag
   25.81 +    fun status' (obj, result, (stats, badobjs)) =
   25.82 +      let
   25.83 +        val badobjs' = if Property.failure result then obj :: badobjs else badobjs
   25.84 +        val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
   25.85 +      in badobjs' end
   25.86 +
   25.87 +    fun try_shrink (obj, result, stats') (stats, badobjs) =
   25.88 +      let
   25.89 +        fun is_failure s =
   25.90 +          let val (result, stats') = Property.test prop (s, stats)
   25.91 +          in if Property.failure result then SOME (s, result, stats') else NONE end
   25.92 +      in
   25.93 +        case get_first is_failure (shrink obj) of
   25.94 +          SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
   25.95 +        | NONE => status' (obj, result, (stats', badobjs))
   25.96 +      end
   25.97 +
   25.98 +    fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
   25.99 +      | iter (SOME (obj, stream), (stats, badobjs)) =
  25.100 +        if #count stats >= Config.get ctxt gen_target then
  25.101 +          finish (stats, map apply_show badobjs)
  25.102 +        else
  25.103 +          let
  25.104 +            val (result, stats') = Property.test prop (obj, stats)
  25.105 +            val badobjs' = if Property.failure result then
  25.106 +                try_shrink (obj, result, stats') (stats, badobjs)
  25.107 +              else
  25.108 +                status' (obj, result, (stats', badobjs))
  25.109 +          in iter (next stream, (stats', badobjs')) end
  25.110 +  in
  25.111 +    fn stream => iter (next stream, (s0, []))
  25.112 +  end
  25.113 +
  25.114 +fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
  25.115 +fun check ctxt = check' ctxt Property.stats
  25.116 +fun checks ctxt = cpsCheck ctxt Property.stats
  25.117 +
  25.118 +fun checkGen ctxt (gen, show) (tag, prop) =
  25.119 +  check' ctxt {count = 0, tags = [("__GEN", 0)]}
  25.120 +    (limit ctxt gen, show) (tag, prop) Generator.stream
  25.121 +
  25.122 +fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
  25.123 +  cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
  25.124 +    (limit ctxt gen, show) (tag, prop) Generator.stream
  25.125 +
  25.126 +fun checkOne ctxt show (tag, prop) obj =
  25.127 +  check ctxt (List.getItem, show) (tag, prop) [obj]
  25.128 +
  25.129 +(*call the compiler and pass resulting type string to the parser*)
  25.130 +fun determine_type ctxt s =
  25.131 +  let
  25.132 +    val return = Unsynchronized.ref "return"
  25.133 +    val use_context : use_context =
  25.134 +     {tune_source = #tune_source ML_Env.local_context,
  25.135 +      name_space = #name_space ML_Env.local_context,
  25.136 +      str_of_pos = #str_of_pos ML_Env.local_context,
  25.137 +      print = fn r => return := r,
  25.138 +      error = #error ML_Env.local_context}
  25.139 +    val _ =
  25.140 +      Context.setmp_thread_data (SOME (Context.Proof ctxt))
  25.141 +        (fn () => Secure.use_text use_context (0, "generated code") true s) ()
  25.142 +  in
  25.143 +    Gen_Construction.parse_pred (! return)
  25.144 +  end;
  25.145 +
  25.146 +(*call the compiler and run the test*)
  25.147 +fun run_test ctxt s =
  25.148 +  Context.setmp_thread_data (SOME (Context.Proof ctxt))
  25.149 +    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
  25.150 +
  25.151 +(*split input into tokens*)
  25.152 +fun input_split s =
  25.153 +  let
  25.154 +    fun dot c = c = #"."
  25.155 +    fun space c = c = #" "
  25.156 +    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
  25.157 +  in
  25.158 +   (String.tokens space (Substring.string head),
  25.159 +    Substring.string (Substring.dropl dot code))
  25.160 +  end;
  25.161 +
  25.162 +(*create the function from the input*)
  25.163 +fun make_fun s =
  25.164 +  let
  25.165 +    val scan_param = Scan.one (fn s => s <> ";")
  25.166 +    fun parameters s = Scan.repeat1 scan_param s
  25.167 +    val p = $$ "ALL" |-- parameters
  25.168 +    val (split, code) = input_split s
  25.169 +    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
  25.170 +    val (params, _) = Scan.finite stop p split
  25.171 +  in "fn (" ^ commas params ^ ") => " ^ code end;
  25.172 +
  25.173 +(*read input and perform the test*)
  25.174 +fun gen_check_property check ctxt s =
  25.175 +  let
  25.176 +    val func = make_fun s
  25.177 +    val (_, ty) = determine_type ctxt func
  25.178 +  in run_test ctxt (check ctxt "Check" (ty, func)) end;
  25.179 +
  25.180 +val check_property = gen_check_property Gen_Construction.build_check
  25.181 +(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
  25.182 +
  25.183 +(*perform test for specification function*)
  25.184 +fun gen_check_property_f check ctxt s =
  25.185 +  let
  25.186 +    val (name, ty) = determine_type ctxt s
  25.187 +  in run_test ctxt (check ctxt name (ty, s)) end;
  25.188 +
  25.189 +val check_property_f = gen_check_property_f Gen_Construction.build_check
  25.190 +(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
  25.191 +
  25.192 +end;
  25.193 +
  25.194 +fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;
  25.195 +
    26.1 --- a/src/Tools/WWW_Find/ROOT	Fri Aug 23 12:30:51 2013 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,3 +0,0 @@
    26.4 -session WWW_Find = Pure +
    26.5 -  theories [condition = ISABELLE_POLYML] WWW_Find
    26.6 -