feat(Tools/Spec_Check) major upgrade draft
authorKevin Kappelmann <kevin.kappelmann@tum.de>
Mon, 21 Jun 2021 16:08:36 +0200
changeset 74126 6c6938da7678
parent 74122 66bff50bc5f1
feat(Tools/Spec_Check) major upgrade term generators, lazy shrinking, detailled test output, pretty printing, modularisation, bug fixes
src/Tools/ROOT
src/Tools/Spec_Check/Examples.thy
src/Tools/Spec_Check/README
src/Tools/Spec_Check/README.md
src/Tools/Spec_Check/Spec_Check.thy
src/Tools/Spec_Check/Spec_Check_Base.thy
src/Tools/Spec_Check/base_generator.ML
src/Tools/Spec_Check/configuration.ML
src/Tools/Spec_Check/dynamic/Spec_Check_Dynamic.thy
src/Tools/Spec_Check/dynamic/dynamic_construct.ML
src/Tools/Spec_Check/dynamic/spec_check_dynamic.ML
src/Tools/Spec_Check/examples/Spec_Check_Examples.thy
src/Tools/Spec_Check/gen_construction.ML
src/Tools/Spec_Check/generator.ML
src/Tools/Spec_Check/generators/Spec_Check_Generators.thy
src/Tools/Spec_Check/generators/gen.ML
src/Tools/Spec_Check/generators/gen_base.ML
src/Tools/Spec_Check/generators/gen_function.ML
src/Tools/Spec_Check/generators/gen_int.ML
src/Tools/Spec_Check/generators/gen_real.ML
src/Tools/Spec_Check/generators/gen_term.ML
src/Tools/Spec_Check/generators/gen_text.ML
src/Tools/Spec_Check/generators/gen_types.ML
src/Tools/Spec_Check/lecker.ML
src/Tools/Spec_Check/output_style.ML
src/Tools/Spec_Check/output_styles/Spec_Check_Output_Style.thy
src/Tools/Spec_Check/output_styles/output_style.ML
src/Tools/Spec_Check/output_styles/output_style_custom.ML
src/Tools/Spec_Check/output_styles/output_style_perl.ML
src/Tools/Spec_Check/output_styles/output_style_types.ML
src/Tools/Spec_Check/property.ML
src/Tools/Spec_Check/random.ML
src/Tools/Spec_Check/show/Spec_Check_Show.thy
src/Tools/Spec_Check/show/show.ML
src/Tools/Spec_Check/show/show_base.ML
src/Tools/Spec_Check/show/show_types.ML
src/Tools/Spec_Check/shrink/Spec_Check_Shrink.thy
src/Tools/Spec_Check/shrink/shrink.ML
src/Tools/Spec_Check/shrink/shrink_base.ML
src/Tools/Spec_Check/shrink/shrink_types.ML
src/Tools/Spec_Check/spec_check.ML
src/Tools/Spec_Check/spec_check_base.ML
src/Tools/Spec_Check/util.ML
--- a/src/Tools/ROOT	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/Tools/ROOT	Mon Jun 21 16:08:36 2021 +0200
@@ -4,11 +4,6 @@
   theories
     Code_Generator
 
-session Spec_Check in Spec_Check = Pure +
-  theories
-    Spec_Check
-    Examples
-
 session SML in SML = Pure +
   theories
     Examples
@@ -18,3 +13,34 @@
     Haskell
   theories [condition = ISABELLE_GHC_STACK]
     Test
+
+session Spec_Check in Spec_Check = "Pure" +
+
+description
+\<open>SpecCheck is a specification-based testing environment for ML programs. It is based on QCheck
+(\<^url>\<open>https://github.com/league/qcheck/\<close>) by Christopher League (\<^url>\<open>https://contrapunctus.net/\<close>). It
+got adapted and extended to fit into the Isabelle/ML framework and resemble the very successful
+QuickCheck (\<^url>\<open>https://en.wikipedia.org/wiki/QuickCheck\<close>) more closely.\<close>
+directories
+  generators
+  output_styles
+  "show"
+  shrink
+
+theories
+  Spec_Check_Generators
+  Spec_Check_Output_Style
+  Spec_Check_Show
+  Spec_Check_Shrink
+  Spec_Check
+
+session Spec_Check_Dynamic in "Spec_Check/dynamic" = "Spec_Check" +
+description
+\<open>Dynamic generation of generators and show functions for SpecCheck tests specified in string
+formats.\<close>
+theories
+  Spec_Check_Dynamic
+
+session Spec_Check_Examples in "Spec_Check/examples" = "Spec_Check_Dynamic" +
+theories
+  Spec_Check_Examples
--- a/src/Tools/Spec_Check/Examples.thy	Fri Jun 18 15:03:12 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-theory Examples
-imports Spec_Check
-begin
-
-section \<open>List examples\<close>
-
-ML_command \<open>
-check_property "ALL xs. rev xs = xs";
-\<close>
-
-ML_command \<open>
-check_property "ALL xs. rev (rev xs) = xs";
-\<close>
-
-
-section \<open>AList Specification\<close>
-
-ML_command \<open>
-(* map_entry applies the function to the element *)
-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)";
-\<close>
-
-ML_command \<open>
-(* update always results in an entry *)
-check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
-\<close>
-
-ML_command \<open>
-(* update always writes the value *)
-check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
-\<close>
-
-ML_command \<open>
-(* default always results in an entry *)
-check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
-\<close>
-
-ML_command \<open>
-(* delete always removes the entry *)
-check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
-\<close>
-
-ML_command \<open>
-(* default writes the entry iff it didn't exist *)
-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))";
-\<close>
-
-section \<open>Examples on Types and Terms\<close>
-
-ML_command \<open>
-check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
-\<close>
-
-ML_command \<open>
-check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
-\<close>
-
-
-text \<open>One would think this holds:\<close>
-
-ML_command \<open>
-check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
-\<close>
-
-text \<open>But it only holds with this precondition:\<close>
-
-ML_command \<open>
-check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
-\<close>
-
-section \<open>Some surprises\<close>
-
-ML_command \<open>
-check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
-\<close>
-
-
-ML_command \<open>
-val thy = \<^theory>;
-check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
-\<close>
-
-end
--- a/src/Tools/Spec_Check/README	Fri Jun 18 15:03:12 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-This is a Quickcheck tool for Isabelle/ML.
-
-Authors
-
-  Lukas Bulwahn
-  Nicolai Schaffroth
-
-Quick Usage
-
-  - Import Spec_Check.thy in your development
-  - Look at examples in Examples.thy
-  - write specifications with the ML invocation
-      check_property "ALL x. P x"
-
-Notes
-
-Our specification-based testing tool originated from Christopher League's
-QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
-provides a rich and uniform ML platform (called Isabelle/ML), this
-testing tools is very different than the one for a typical ML developer.
-
-1. Isabelle/ML provides common data structures, which we can use in the
-tool's implementation for storing data and printing output.
-
-2. The implementation in Isabelle that will be checked with this tool
-commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
-but they do not use other integer types in ML, such as ML's Int.int,
-Word.word and others.
-
-3. As Isabelle can run heavily in parallel, we avoid reference types.
-
-4. Isabelle has special naming conventions and documentation of source
-code is only minimal to avoid parroting.
-
-Next steps:
-  - Remove all references and store the neccessary random seed in the
-    Isabelle's context.
-  - Simplify some existing random generators.
-    The original ones from Christopher League are so complicated to
-    support many integer types uniformly.
-
-License
-
-  The source code originated from Christopher League's QCheck, which is
-  licensed under the 2-clause BSD license. The current source code is
-  licensed under the compatible 3-clause BSD license of Isabelle.
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/README.md	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,56 @@
+# SpecCheck
+
+SpecCheck is a [QuickCheck](https://en.wikipedia.org/wiki/QuickCheck)-like testing framework for Isabelle/ML.
+You can use it to write input generators for and properties about ML functions.
+It helps you to identify bugs by printing counterexamples on failure.
+
+## Quick Usage
+1. Import `Spec_Check.Spec_Check` into your environment.
+2. Write specifications using the ML invocation: `check show gen name prop ctxt seed` where
+  * `show` converts values into `Pretty.T` types to show the failing inputs. See `show/`.
+  * `gen` is the value generator used for the test. See `generators/`.
+  * `name` is the shown name of the test
+  * `prop` is the property to be tested. See `property.ML`
+  * `seed` is the initial seed for the generator.
+
+You can also choose to omit the show method for rapid testing or add a shrinking method a la
+QuickCheck to get better counterexamples. See `spec_check.ML`.
+
+A deprecated alternative allows you to specify tests using strings:
+1. Import `Spec_Check_Dynamic.Dynamic` into your environment.
+2. `check_property "ALL x. P x"` where `P x` is some ML code evaluating to a boolean
+
+Examples can be found in `examples/`.
+
+## Notes
+
+SpecCheck is based on [QCheck](https://github.com/league/qcheck), a testing framework for Standard ML by
+[Christopher League](https://contrapunctus.net/league/).
+As Isabelle/ML provides a rich and uniform ML platform, some features where removed or adapted, in particular:
+
+1. Isabelle/ML provides common data structures, which we can use in the
+tool's implementation for storing data and printing output.
+
+2. Implementations in Isabelle/ML checked with this tool commonly use Isabelle/ML's `int` type
+(which corresponds ML's `IntInf.int`), but do not use other integer types in ML such as ML's `Int.int`,
+`Word.word`, and others.
+
+3. As Isabelle makes heavy use of parallelism, we avoid reference types.
+
+## Next Steps
+
+* Implement sizing methods (cf. QuickCheck's `sized`)
+* Implement shrinking methods for commonly used types
+
+## License
+
+The source code originated from Christopher League's QCheck, which is
+licensed under the 2-clause BSD license. The current source code is
+licensed under the compatible 3-clause BSD license of Isabelle.
+
+## Authors
+
+* Lukas Bulwahn
+* Nicolai Schaffroth
+* Sebastian Willenbrink
+* Kevin Kappelmann
--- a/src/Tools/Spec_Check/Spec_Check.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/Tools/Spec_Check/Spec_Check.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -1,13 +1,17 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>SpecCheck\<close>
 theory Spec_Check
-imports Pure
+imports
+  Spec_Check_Generators
+  Spec_Check_Show
+  Spec_Check_Shrink
+  Spec_Check_Output_Style
 begin
 
-ML_file \<open>random.ML\<close>
-ML_file \<open>property.ML\<close>
-ML_file \<open>base_generator.ML\<close>
-ML_file \<open>generator.ML\<close>
-ML_file \<open>gen_construction.ML\<close>
+paragraph \<open>Summary\<close>
+text \<open>The SpecCheck (specification based) testing environment and Lecker testing framework.\<close>
+
 ML_file \<open>spec_check.ML\<close>
-ML_file \<open>output_style.ML\<close>
+ML_file \<open>lecker.ML\<close>
 
-end
\ No newline at end of file
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/Spec_Check_Base.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,18 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>SpecCheck Base\<close>
+theory Spec_Check_Base
+imports Pure
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>Basic setup for SpecCheck.\<close>
+
+ML_file \<open>util.ML\<close>
+
+ML_file \<open>spec_check_base.ML\<close>
+ML_file \<open>property.ML\<close>
+ML_file \<open>configuration.ML\<close>
+
+ML_file \<open>random.ML\<close>
+
+end
--- a/src/Tools/Spec_Check/base_generator.ML	Fri Jun 18 15:03:12 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-(*  Title:      Tools/Spec_Check/base_generator.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Basic random generators.
-*)
-
-signature BASE_GENERATOR =
-sig
-
-type rand
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-val new : unit -> rand
-val range : int * int -> rand -> int * rand
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-
-val lift : 'a -> 'a gen
-val select : 'a vector -> 'a gen
-val choose : 'a gen vector -> 'a gen
-val choose' : (int * 'a gen) vector -> 'a gen
-val selectL : 'a list -> 'a gen
-val chooseL : 'a gen list -> 'a gen
-val chooseL' : (int * 'a gen) list -> 'a gen
-val filter : ('a -> bool) -> 'a gen -> 'a gen
-
-val zip : ('a gen * 'b gen) -> ('a * 'b) gen
-val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
-val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
-val map : ('a -> 'b) -> 'a gen -> 'b gen
-val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
-val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
-val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
-
-val flip : bool gen
-val flip' : int * int -> bool gen
-
-val list : bool gen -> 'a gen -> 'a list gen
-val option : bool gen -> 'a gen -> 'a option gen
-val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
-
-val variant : (int, 'b) co
-val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
-val cobool : (bool, 'b) co
-val colist : ('a, 'b) co -> ('a list, 'b) co
-val coopt : ('a, 'b) co -> ('a option, 'b) co
-
-type stream
-val start : rand -> stream
-val limit : int -> 'a gen -> ('a, stream) reader
-
-end
-
-structure Base_Generator : BASE_GENERATOR =
-struct
-
-(* random number engine *)
-
-type rand = real
-
-val a = 16807.0
-val m = 2147483647.0
-
-fun nextrand seed =
-  let
-    val t = a * seed
-  in
-    t - m * real (floor (t / m))
-  end
-
-val new = nextrand o Time.toReal o Time.now
-
-fun range (min, max) =
-  if min > max then raise Domain (* TODO: raise its own error *)
-  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
-
-fun split r =
-  let
-    val r = r / a
-    val r0 = real (floor r)
-    val r1 = r - r0
-  in
-    (nextrand r0, nextrand r1)
-  end
-
-(* generators *)
-
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-
-fun lift obj r = (obj, r)
-
-local (* Isabelle does not use vectors? *)
-  fun explode ((freq, gen), acc) =
-    List.tabulate (freq, fn _ => gen) @ acc
-in
-  fun choose v r =
-    let val (i, r) = range(0, Vector.length v - 1) r
-    in Vector.sub (v, i) r end
-  fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
-  fun select v = choose (Vector.map lift v)
-end
-
-fun chooseL l = choose (Vector.fromList l)
-fun chooseL' l = choose' (Vector.fromList l)
-fun selectL l = select (Vector.fromList l)
-
-fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
-
-fun zip3 (g1, g2, g3) =
-  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
-
-fun zip4 (g1, g2, g3, g4) =
-  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
-
-fun map f g = apfst f o g
-
-fun map2 f = map f o zip
-fun map3 f = map f o zip3
-fun map4 f = map f o zip4
-
-fun filter p gen r =
-  let
-    fun loop (x, r) = if p x then (x, r) else loop (gen r)
-  in
-    loop (gen r)
-  end
-
-val flip = selectL [true, false]
-fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
-
-fun list flip g r =
-  case flip r of
-      (true, r) => ([], r)
-    | (false, r) =>
-      let
-        val (x,r) = g r
-        val (xs,r) = list flip g r
-      in (x::xs, r) end
-
-fun option flip g r =
-  case flip r of
-    (true, r) => (NONE, r)
-  | (false, r) => map SOME g r
-
-fun vector tabulate (int, elem) r =
-  let
-    val (n, r) = int r
-    val p = Unsynchronized.ref r
-    fun g _ =
-      let
-        val (x,r) = elem(!p)
-      in x before p := r end
-  in
-    (tabulate(n, g), !p)
-  end
-
-type stream = rand Unsynchronized.ref * int
-
-fun start r = (Unsynchronized.ref r, 0)
-
-fun limit max gen =
-  let
-    fun next (p, i) =
-      if i >= max then NONE
-      else
-        let val (x, r) = gen(!p)
-        in SOME(x, (p, i+1)) before p := r end
-  in
-    next
-  end
-
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-fun variant v g r =
-  let
-    fun nth (i, r) =
-      let val (r1, r2) = split r
-      in if i = 0 then r1 else nth (i-1, r2) end
-  in
-    g (nth (v, r))
-  end
-
-fun arrow (cogen, gen) r =
-  let
-    val (r1, r2) = split r
-    fun g x = fst (cogen x gen r1)
-  in (g, r2) end
-
-fun cobool false = variant 0
-  | cobool true = variant 1
-
-fun colist _ [] = variant 0
-  | colist co (x::xs) = variant 1 o co x o colist co xs
-
-fun coopt _ NONE = variant 0
-  | coopt co (SOME x) = variant 1 o co x
-
-end
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/configuration.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,41 @@
+(*  Title:      Tools/Spec_Check/configuration.ML
+    Author:     Kevin Kappelmann
+
+Configuration options for SpecCheck.
+*)
+
+signature SPEC_CHECK_CONFIGURATION =
+sig
+
+  (*maximum number of successful tests before succeeding*)
+  val max_success : int Config.T
+  (*maximum number of discarded tests per successful test before giving up*)
+  val max_discard_ratio : int Config.T
+  (*maximum number of shrinks per counterexample*)
+  val max_shrinks : int Config.T
+  (*number of counterexamples shown*)
+  val num_counterexamples : int Config.T
+  (*sort counterexamples by size*)
+  val sort_counterexamples : bool Config.T
+  (*print timing etc. depending on style*)
+  val show_stats : bool Config.T
+
+end
+
+structure Spec_Check_Configuration : SPEC_CHECK_CONFIGURATION =
+struct
+
+val max_success = Attrib.setup_config_int \<^binding>\<open>spec_check_max_success\<close> (K 100)
+
+val max_discard_ratio = Attrib.setup_config_int \<^binding>\<open>spec_check_max_discard_ratio\<close> (K 10)
+
+val max_shrinks = Attrib.setup_config_int \<^binding>\<open>spec_check_max_shrinks\<close> (K 10000)
+
+val num_counterexamples = Attrib.setup_config_int \<^binding>\<open>spec_check_num_counterexamples\<close> (K 1)
+
+val sort_counterexamples =
+  Attrib.setup_config_bool \<^binding>\<open>spec_check_sort_counterexamples\<close> (K true)
+
+val show_stats = Attrib.setup_config_bool \<^binding>\<open>spec_check_show_stats\<close> (K true)
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/dynamic/Spec_Check_Dynamic.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,16 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Dynamic Generators\<close>
+theory Spec_Check_Dynamic
+imports Spec_Check.Spec_Check
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>Generators and show functions for SpecCheck that are dynamically derived from a given ML input
+string. This approach can be handy to quickly test a function during development, but it lacks
+customisability and is very brittle. See @{file "../examples/Spec_Check_Examples.thy"}} for some
+examples contrasting this approach to the standard one (specifying generators as ML code).\<close>
+
+ML_file \<open>dynamic_construct.ML\<close>
+ML_file \<open>spec_check_dynamic.ML\<close>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/dynamic/dynamic_construct.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,188 @@
+(*  Title:      Tools/Spec_Check/dynamic/dynamic_construct.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+
+Dynamic construction of generators and show functions (returned as strings that need to be compiled)
+from a given string representing ML code to be tested as a SpecCheck test.
+*)
+
+signature SPEC_CHECK_DYNAMIC_CONSTRUCT =
+sig
+  val register : string * (string * string) -> theory -> theory
+  type mltype
+  val parse_pred : string -> string * mltype
+  val build_check : Proof.context -> string -> mltype * string -> string
+  (*val safe_check : string -> mltype * string -> string*)
+  val string_of_bool : bool -> string
+  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
+end;
+
+structure Spec_Check_Dynamic_Construct : SPEC_CHECK_DYNAMIC_CONSTRUCT =
+struct
+
+(* Parsing ML types *)
+
+datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
+
+(*Split string into tokens for parsing*)
+fun split s =
+  let
+    fun split_symbol #"(" = "( "
+      | split_symbol #")" = " )"
+      | split_symbol #"," = " ,"
+      | split_symbol #":" = " :"
+      | split_symbol c = Char.toString c
+    fun is_space c = c = #" "
+  in String.tokens is_space (String.translate split_symbol s) end;
+
+(*Accept anything that is not a recognized symbol*)
+val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
+
+(*Turn a type list into a nested Con*)
+fun make_con [] = raise Empty
+  | make_con [c] = c
+  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
+
+(*Parse a type*)
+fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
+
+and parse_type_arg s = (parse_tuple || parse_type_single) s
+
+and parse_type_single s = (parse_con || parse_type_basic) s
+
+and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
+
+and parse_list s =
+  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
+
+and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
+
+and parse_con s = ((parse_con_nest
+  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
+  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
+  >> (make_con o rev)) s
+
+and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
+
+and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
+
+and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
+  >> (fn (t, tl) => Tuple (t :: tl))) s;
+
+(*Parse entire type + name*)
+fun parse_function s =
+  let
+    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
+    val (name, ty) = p (split s)
+    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+    val (typ, _) = Scan.finite stop parse_type ty
+  in (name, typ) end;
+
+(*Create desired output*)
+fun parse_pred s =
+  let
+    val (name, Con ("->", t :: _)) = parse_function s
+  in (name, t) end;
+
+(* Construct Generators and Pretty Printers *)
+
+(*copied from smt_config.ML *)
+fun string_of_bool b = if b then "true" else "false"
+
+fun string_of_ref f r = f (!r) ^ " ref";
+
+val initial_content = Symtab.make [
+  ("bool", ("Spec_Check_Generator.bernoulli 0.5", "Gen_Construction.string_of_bool")),
+  ("option", ("Spec_Check_Generator.option (Spec_Check_Generator.bernoulli (2.0 / 3.0))",
+              "ML_Syntax.print_option")),
+  ("list", ("Spec_Check_Generator.unfold_while (K (Spec_Check_Generator.bernoulli (2.0 / 3.0)))",
+            " ML_Syntax.print_list")),
+  ("unit", ("gen_unit", "fn () => \"()\"")),
+  ("int", ("Spec_Check_Generator.range_int (~2147483647,2147483647)", "string_of_int")),
+  ("real", ("Spec_Check_Generator.real", "string_of_real")),
+  ("char", ("Spec_Check_Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
+  ("string", ("Spec_Check_Generator.string (Spec_Check_Generator.nonneg 100) Spec_Check_Generator.char",
+              "ML_Syntax.print_string")),
+  ("->", ("Spec_Check_Generator.function' o snd", "fn (_, _) => fn _ => \"fn\"")),
+  ("typ", ("Spec_Check_Generator.typ'' (Spec_Check_Generator.return 8) (Spec_Check_Generator.nonneg 4) (Spec_Check_Generator.nonneg 4) (1,1,1)",
+           "Pretty.string_of o Syntax.pretty_typ (Context.the_local_context ())")),
+  ("term", ("Spec_Check_Generator.term_tree (fn h => fn _ => "
+            ^ "let val ngen = Spec_Check_Generator.nonneg (Int.max (0, 4-h))\n"
+            ^ "    val aterm_gen = Spec_Check_Generator.aterm' (Spec_Check_Generator.return 8) ngen (1,1,1,0)\n"
+            ^ "in Spec_Check_Generator.zip aterm_gen ngen end)",
+            "Pretty.string_of o Syntax.pretty_term (Context.the_local_context ())"))]
+
+structure Data = Theory_Data
+(
+  type T = (string * string) Symtab.table
+  val empty = initial_content
+  val extend = I
+  fun merge data : T = Symtab.merge (K true) data
+)
+
+fun data_of ctxt tycon =
+  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
+    SOME data => data
+  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
+
+val generator_of = fst oo data_of
+val printer_of = snd oo data_of
+
+fun register (ty, data) = Data.map (Symtab.update (ty, data))
+
+(*
+fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
+*)
+
+fun combine dict [] = dict
+  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
+
+fun compose_generator _ Var = "Spec_Check_Generator.range_int (~2147483647, 2147483647)"
+  | compose_generator ctxt (Con (s, types)) =
+      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
+  | compose_generator ctxt (Tuple t) =
+      let
+        fun tuple_body t = space_implode ""
+          (map
+            (fn (ty, n) => implode ["val (x", string_of_int n, ", r", string_of_int n, ") = ",
+              compose_generator ctxt ty, " r", string_of_int (n - 1), " "])
+            (t ~~ (1 upto (length t))))
+        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+      in
+        "fn r0 => let " ^ tuple_body t ^
+        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
+      end
+
+fun compose_printer _ Var = "Int.toString"
+  | compose_printer ctxt (Con (s, types)) =
+      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
+  | compose_printer ctxt (Tuple t) =
+      let
+        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+        fun tuple_body t = space_implode " ^ \", \" ^ "
+          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
+          (t ~~ (1 upto (length t))))
+      in implode ["fn (", tuple_head (length t), ") => \"(\" ^ ", tuple_body t, " ^ \")\""] end
+
+(*produce compilable string*)
+fun build_check ctxt name (ty, spec) = implode ["Spec_Check.check (Pretty.str o (",
+  compose_printer ctxt ty, ")) (", compose_generator ctxt ty, ")  \"", name,
+  "\" (Spec_Check_Property.prop (", spec,
+  ")) (Context.the_local_context ()) (Spec_Check_Random.new ());"]
+
+(*produce compilable string - non-eqtype functions*)
+(*
+fun safe_check name (ty, spec) =
+  let
+    val default =
+      (case AList.lookup (op =) (!gen_table) "->" of
+        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
+      | SOME entry => entry)
+  in
+   (gen_table :=
+     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
+    build_check name (ty, spec) before
+    gen_table := AList.update (op =) ("->", default) (!gen_table))
+  end;
+*)
+
+end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/dynamic/spec_check_dynamic.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,81 @@
+(*  Title:      Tools/Spec_Check/dynamic/spec_check_dynamic.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+
+This file allows to run SpecCheck tests specified as a string representing ML code.
+
+TODO: this module is not very well tested.
+*)
+
+signature SPEC_CHECK_DYNAMIC =
+sig
+  val check_dynamic : Proof.context -> string -> unit
+end
+
+structure Spec_Check_Dynamic : SPEC_CHECK_DYNAMIC =
+struct
+
+(*call the compiler and pass resulting type string to the parser*)
+fun determine_type ctxt s =
+  let
+    val return = Unsynchronized.ref "return"
+    val context : ML_Compiler0.context =
+     {name_space = #name_space ML_Env.context,
+      print_depth = SOME 1000000,
+      here = #here ML_Env.context,
+      print = fn r => return := r,
+      error = #error ML_Env.context}
+    val _ =
+      Context.setmp_generic_context (SOME (Context.Proof ctxt))
+        (fn () =>
+          ML_Compiler0.ML context
+            {line = 0, file = "generated code", verbose = true, debug = false} s) ()
+  in Spec_Check_Dynamic_Construct.parse_pred (! return) end;
+
+(*call the compiler and run the test*)
+fun run_test ctxt s =
+  Context.setmp_generic_context (SOME (Context.Proof ctxt))
+    (fn () =>
+      ML_Compiler0.ML ML_Env.context
+        {line = 0, file = "generated code", verbose = false, debug = false} s) ();
+
+(*split input into tokens*)
+fun input_split s =
+  let
+    fun dot c = c = #"."
+    fun space c = c = #" "
+    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
+  in
+   (String.tokens space (Substring.string head),
+    Substring.string (Substring.dropl dot code))
+  end;
+
+(*create the function from the input*)
+fun make_fun s =
+  let
+    val scan_param = Scan.one (fn s => s <> ";")
+    fun parameters s = Scan.repeat1 scan_param s
+    val p = $$ "ALL" |-- parameters
+    val (split, code) = input_split s
+    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
+    val (params, _) = Scan.finite stop p split
+  in "fn (" ^ commas params ^ ") => " ^ code end;
+
+(*read input and perform the test*)
+fun gen_check_property check ctxt s =
+  let
+    val func = make_fun s
+    val (_, ty) = determine_type ctxt func
+  in run_test ctxt (check ctxt "Dynamic Test" (ty, func)) end;
+
+val check_dynamic = gen_check_property Spec_Check_Dynamic_Construct.build_check
+(*val check_property_safe = gen_check_property Construct_Gen.safe_check*)
+
+(*perform test for specification function*)
+(*fun gen_check_property_f check ctxt s =
+  let
+    val (name, ty) = determine_type ctxt s
+  in run_test ctxt (check ctxt name (ty, s)) end;
+
+val check_property_f = gen_check_property_f Gen_Dynamic.build_check*)
+(*val check_property_safe_f_ = gen_check_property_f Construct_Gen.safe_check*)
+end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/examples/Spec_Check_Examples.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,129 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Examples\<close>
+theory Spec_Check_Examples
+imports Spec_Check_Dynamic.Spec_Check_Dynamic
+begin
+
+subsection \<open>List examples\<close>
+
+ML \<open>
+open Spec_Check
+open Spec_Check_Dynamic
+structure Gen = Spec_Check_Generator
+structure Prop = Spec_Check_Property
+structure Show = Spec_Check_Show
+structure Shrink = Spec_Check_Shrink
+structure Random = Spec_Check_Random
+\<close>
+
+ML_command \<open>
+let
+  val int_gen = Gen.range_int (~10000000, 10000000)
+  val size_gen = Gen.nonneg 10
+  val check_list = check_shrink (Show.list Show.int) (Shrink.list Shrink.int)
+    (Gen.list size_gen int_gen)
+  fun list_test (k, f, xs) =
+    AList.lookup (op=) (AList.map_entry (op=) k f xs) k = Option.map f (AList.lookup (op=) xs k)
+
+  val list_test_show = Show.zip3 Show.int Show.none (Show.list (Show.zip Show.int Show.int))
+  val list_test_gen = Gen.zip3 int_gen (Gen.function' int_gen)
+    (Gen.list size_gen (Gen.zip int_gen int_gen))
+in
+  Lecker.test_group @{context} (Random.new ()) [
+    Prop.prop (fn xs => rev xs = xs) |> check_list "rev = I",
+    Prop.prop (fn xs => rev (rev xs) = xs) |> check_list "rev o rev = I",
+    Prop.prop list_test |> check list_test_show list_test_gen "lookup map equiv map lookup"
+  ]
+end
+\<close>
+
+text \<open>The next three examples roughly correspond to the above test group (except that there's no
+shrinking). Compared to the string-based method, the method above is more flexible - you can change
+your generators, shrinking methods, and show instances - and robust - you are not reflecting strings
+(which might contain typos) but entering type-checked code. In exchange, it is a bit more work to
+set up the generators. However, in practice, one shouldn't rely on default generators in most cases
+anyway.\<close>
+
+ML_command \<open>
+check_dynamic @{context} "ALL xs. rev xs = xs";
+\<close>
+
+ML_command \<open>
+check_dynamic @{context} "ALL xs. rev (rev xs) = xs";
+\<close>
+
+subsection \<open>AList Specification\<close>
+
+ML_command \<open>
+(* map_entry applies the function to the element *)
+check_dynamic @{context} (implode
+  ["ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = ",
+   "Option.map f (AList.lookup (op =) xs k)"])
+\<close>
+
+ML_command \<open>
+(* update always results in an entry *)
+check_dynamic @{context} "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
+\<close>
+
+ML_command \<open>
+(* update always writes the value *)
+check_dynamic @{context}
+  "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
+\<close>
+
+ML_command \<open>
+(* default always results in an entry *)
+check_dynamic @{context} "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
+\<close>
+
+ML_command \<open>
+(* delete always removes the entry *)
+check_dynamic @{context} "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
+\<close>
+
+ML_command \<open>
+(* default writes the entry iff it didn't exist *)
+check_dynamic @{context} (implode
+  ["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))"])
+\<close>
+
+subsection \<open>Examples on Types and Terms\<close>
+
+ML_command \<open>
+check_dynamic @{context} "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
+\<close>
+
+ML_command \<open>
+check_dynamic @{context} "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
+\<close>
+
+
+text \<open>One would think this holds:\<close>
+
+ML_command \<open>
+check_dynamic @{context} "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
+\<close>
+
+text \<open>But it only holds with this precondition:\<close>
+
+ML_command \<open>
+check_dynamic @{context}
+  "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
+\<close>
+
+subsection \<open>Some surprises\<close>
+
+ML_command \<open>
+check_dynamic @{context} "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
+\<close>
+
+
+ML_command \<open>
+val thy = \<^theory>;
+check_dynamic (Context.the_local_context ())
+  "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
+\<close>
+
+end
--- a/src/Tools/Spec_Check/gen_construction.ML	Fri Jun 18 15:03:12 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-(*  Title:      Tools/Spec_Check/gen_construction.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Constructing generators and pretty printing function for complex types.
-*)
-
-signature GEN_CONSTRUCTION =
-sig
-  val register : string * (string * string) -> theory -> theory
-  type mltype
-  val parse_pred : string -> string * mltype
-  val build_check : Proof.context -> string -> mltype * string -> string
-  (*val safe_check : string -> mltype * string -> string*)
-  val string_of_bool : bool -> string
-  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
-end;
-
-structure Gen_Construction : GEN_CONSTRUCTION =
-struct
-
-(* Parsing ML types *)
-
-datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
-
-(*Split string into tokens for parsing*)
-fun split s =
-  let
-    fun split_symbol #"(" = "( "
-      | split_symbol #")" = " )"
-      | split_symbol #"," = " ,"
-      | split_symbol #":" = " :"
-      | split_symbol c = Char.toString c
-    fun is_space c = c = #" "
-  in String.tokens is_space (String.translate split_symbol s) end;
-
-(*Accept anything that is not a recognized symbol*)
-val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
-
-(*Turn a type list into a nested Con*)
-fun make_con [] = raise Empty
-  | make_con [c] = c
-  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
-
-(*Parse a type*)
-fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
-
-and parse_type_arg s = (parse_tuple || parse_type_single) s
-
-and parse_type_single s = (parse_con || parse_type_basic) s
-
-and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
-
-and parse_list s =
-  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
-
-and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
-
-and parse_con s = ((parse_con_nest
-  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
-  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
-  >> (make_con o rev)) s
-
-and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
-
-and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
-
-and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
-  >> (fn (t, tl) => Tuple (t :: tl))) s;
-
-(*Parse entire type + name*)
-fun parse_function s =
-  let
-    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
-    val (name, ty) = p (split s)
-    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
-    val (typ, _) = Scan.finite stop parse_type ty
-  in (name, typ) end;
-
-(*Create desired output*)
-fun parse_pred s =
-  let
-    val (name, Con ("->", t :: _)) = parse_function s
-  in (name, t) end;
-
-(* Construct Generators and Pretty Printers *)
-
-(*copied from smt_config.ML *)
-fun string_of_bool b = if b then "true" else "false"
-
-fun string_of_ref f r = f (!r) ^ " ref";
-
-val initial_content = Symtab.make
-  [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
-  ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
-  ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
-  ("unit", ("gen_unit", "fn () => \"()\"")),
-  ("int", ("Generator.int", "string_of_int")),
-  ("real", ("Generator.real", "string_of_real")),
-  ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
-  ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
-  ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
-  ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
-  ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
-
-structure Data = Theory_Data
-(
-  type T = (string * string) Symtab.table
-  val empty = initial_content
-  val extend = I
-  fun merge data : T = Symtab.merge (K true) data
-)
-
-fun data_of ctxt tycon =
-  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
-    SOME data => data
-  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
-
-val generator_of = fst oo data_of
-val printer_of = snd oo data_of
-
-fun register (ty, data) = Data.map (Symtab.update (ty, data))
-
-(*
-fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
-*)
-
-fun combine dict [] = dict
-  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
-
-fun compose_generator _ Var = "Generator.int"
-  | compose_generator ctxt (Con (s, types)) =
-      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
-  | compose_generator ctxt (Tuple t) =
-      let
-        fun tuple_body t = space_implode ""
-          (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
-          compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
-        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-      in
-        "fn r0 => let " ^ tuple_body t ^
-        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
-      end;
-
-fun compose_printer _ Var = "Int.toString"
-  | compose_printer ctxt (Con (s, types)) =
-      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
-  | compose_printer ctxt (Tuple t) =
-      let
-        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-        fun tuple_body t = space_implode " ^ \", \" ^ "
-          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
-          (t ~~ (1 upto (length t))))
-      in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
-
-(*produce compilable string*)
-fun build_check ctxt name (ty, spec) =
-  "Spec_Check.checkGen (Context.the_local_context ()) ("
-  ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
-  ^ name ^ "\", Property.pred (" ^ spec ^ "));";
-
-(*produce compilable string - non-eqtype functions*)
-(*
-fun safe_check name (ty, spec) =
-  let
-    val default =
-      (case AList.lookup (op =) (!gen_table) "->" of
-        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
-      | SOME entry => entry)
-  in
-   (gen_table :=
-     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
-    build_check name (ty, spec) before
-    gen_table := AList.update (op =) ("->", default) (!gen_table))
-  end;
-*)
-
-end;
-
--- a/src/Tools/Spec_Check/generator.ML	Fri Jun 18 15:03:12 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-(*  Title:      Tools/Spec_Check/generator.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Random generators for Isabelle/ML's types.
-*)
-
-signature GENERATOR = sig
-  include BASE_GENERATOR
-  (* text generators *)
-  val char : char gen
-  val charRange : char * char -> char gen
-  val charFrom : string -> char gen
-  val charByType : (char -> bool) -> char gen
-  val string : (int gen * char gen) -> string gen
-  val substring : string gen -> substring gen
-  val cochar : (char, 'b) co
-  val costring : (string, 'b) co
-  val cosubstring : (substring, 'b) co
-  (* integer generators *)
-  val int : int gen
-  val int_pos : int gen
-  val int_neg : int gen
-  val int_nonpos : int gen
-  val int_nonneg : int gen
-  val coint : (int, 'b) co
-  (* real generators *)
-  val real : real gen
-  val real_frac : real gen
-  val real_pos : real gen
-  val real_neg : real gen
-  val real_nonpos : real gen
-  val real_nonneg : real gen
-  val real_finite : real gen
-  (* function generators *)
-  val function_const : 'c * 'b gen -> ('a -> 'b) gen
-  val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
-  val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
-  val unit : unit gen
-  val ref' : 'a gen -> 'a Unsynchronized.ref gen
-  (* more generators *)
-  val term : int -> term gen
-  val typ : int -> typ gen
-
-  val stream : stream
-end
-
-structure Generator : GENERATOR =
-struct
-
-open Base_Generator
-
-val stream = start (new())
-
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-(* text *)
-
-type char = Char.char
-type string = String.string
-type substring = Substring.substring
-
-
-val char = map Char.chr (range (0, Char.maxOrd))
-fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
-
-fun charFrom s =
-  choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
-
-fun charByType p = filter p char
-
-val string = vector CharVector.tabulate
-
-fun substring gen r =
-  let
-    val (s, r') = gen r
-    val (i, r'') = range (0, String.size s) r'
-    val (j, r''') = range (0, String.size s - i) r''
-  in
-    (Substring.substring (s, i, j), r''')
-  end
-
-fun cochar c =
-  if Char.ord c = 0 then variant 0
-  else variant 1 o cochar (Char.chr (Char.ord c div 2))
-
-fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
-
-fun costring s = cosubstring (Substring.full s)
-
-(* integers *)
-val digit = charRange (#"0", #"9")
-val nonzero = string (lift 1, charRange (#"1", #"9"))
-fun digits' n = string (range (0, n-1), digit)
-fun digits n = map2 op^ (nonzero, digits' n)
-
-val maxDigits = 64
-val ratio = 49
-
-fun pos_or_neg f r =
-  let
-    val (s, r') = digits maxDigits r
-  in (f (the (Int.fromString s)), r') end
-
-val int_pos = pos_or_neg I
-val int_neg = pos_or_neg Int.~
-val zero = lift 0
-
-val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
-val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
-val int = chooseL [int_nonneg, int_nonpos]
-
-fun coint n =
-  if n = 0 then variant 0
-  else if n < 0 then variant 1 o coint (~ n)
-  else variant 2 o coint (n div 2)
-
-(* reals *)
-val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
-
-fun real_frac r =
-  let val (s, r') = digits r
-  in (the (Real.fromString s), r') end
-
-val {exp=minExp,...} = Real.toManExp Real.minPos
-val {exp=maxExp,...} = Real.toManExp Real.posInf
-
-val ratio = 99
-
-fun mk r =
-  let
-    val (a, r') = digits r
-    val (b, r'') = digits r'
-    val (e, r''') = range (minExp div 4, maxExp div 4) r''
-    val x = String.concat [a, ".", b, "E", Int.toString e]
-  in
-    (the (Real.fromString x), r''')
-  end
-
-val real_pos = chooseL' (List.map ((pair 1) o lift)
-    [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
-
-val real_neg = map Real.~ real_pos
-
-val real_zero = Real.fromInt 0
-val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
-val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
-
-val real = chooseL [real_nonneg, real_nonpos]
-
-val real_finite = filter Real.isFinite real
-
-(*alternate list generator - uses an integer generator to determine list length*)
-fun list' int gen = vector List.tabulate (int, gen);
-
-(* more function generators *)
-
-fun function_const (_, gen2) r =
-  let
-    val (v, r') = gen2 r
-  in (fn _ => v, r') end;
-
-fun function_strict size (gen1, gen2) r =
-  let
-    val (def, r') = gen2 r
-    val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
-  in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
-
-fun function_lazy (gen1, gen2) r =
-  let
-    val (initial1, r') = gen1 r
-    val (initial2, internal) = gen2 r'
-    val seed = Unsynchronized.ref internal
-    val table = Unsynchronized.ref [(initial1, initial2)]
-    fun new_entry k =
-      let
-        val (new_val, new_seed) = gen2 (!seed)
-        val _ =  seed := new_seed
-        val _ = table := AList.update (op =) (k, new_val) (!table)
-      in new_val end
-  in
-    (fn v1 =>
-      case AList.lookup (op =) (!table) v1 of
-        NONE => new_entry v1
-      | SOME v2 => v2, r')
-  end;
-
-(* unit *)
-
-fun unit r = ((), r);
-
-(* references *)
-
-fun ref' gen r =
-  let val (value, r') = gen r
-  in (Unsynchronized.ref value, r') end;
-
-(* types and terms *)
-
-val sort_string = selectL ["sort1", "sort2", "sort3"];
-val type_string = selectL ["TCon1", "TCon2", "TCon3"];
-val tvar_string = selectL ["a", "b", "c"];
-
-val const_string = selectL ["c1", "c2", "c3"];
-val var_string = selectL ["x", "y", "z"];
-val index = selectL [0, 1, 2, 3];
-val bound_index = selectL [0, 1, 2, 3];
-
-val sort = list (flip' (1, 2)) sort_string;
-
-fun typ n =
-  let
-    fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
-    val tfree = map TFree (zip (tvar_string, sort))
-    val tvar = map TVar (zip (zip (tvar_string, index), sort))
-  in
-    if n = 0 then chooseL [tfree, tvar]
-    else chooseL [type' (n div 2), tfree, tvar]
-  end;
-
-fun term n =
-  let
-    val const = map Const (zip (const_string, typ 10))
-    val free = map Free (zip (var_string, typ 10))
-    val var = map Var (zip (zip (var_string, index), typ 10))
-    val bound = map Bound bound_index
-    fun abs m = map Abs (zip3 (var_string, typ 10, term m))
-    fun app m = map (op $) (zip (term m, term m))
-  in
-    if n = 0 then chooseL [const, free, var, bound]
-    else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
-  end;
-
-end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/Spec_Check_Generators.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,20 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Generators\<close>
+theory Spec_Check_Generators
+imports Spec_Check_Base
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>Generators for SpecCheck take a state and return a pair consisting of a generated value and
+a new state. Refer to @{file "gen_base.ML"}} for the most basic combinators.\<close>
+
+ML_file \<open>gen_types.ML\<close>
+ML_file \<open>gen_base.ML\<close>
+ML_file \<open>gen_text.ML\<close>
+ML_file \<open>gen_int.ML\<close>
+ML_file \<open>gen_real.ML\<close>
+ML_file \<open>gen_function.ML\<close>
+ML_file \<open>gen_term.ML\<close>
+ML_file \<open>gen.ML\<close>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,15 @@
+(*  Title:      Tools/Spec_Check/generators/gen.ML
+    Author:     Kevin Kappelmann, TU Muenchen
+
+Structure containing all generators.
+*)
+structure Spec_Check_Generator =
+struct
+open Spec_Check_Gen_Types
+open Spec_Check_Gen_Base
+open Spec_Check_Gen_Text
+open Spec_Check_Gen_Real
+open Spec_Check_Gen_Int
+open Spec_Check_Gen_Function
+open Spec_Check_Gen_Term
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_base.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,240 @@
+(*  Title:      Tools/Spec_Check/generators/gen_base.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Basic utility functions to create and combine generators.
+*)
+
+signature SPEC_CHECK_GEN_BASE =
+sig
+  include SPEC_CHECK_GEN_TYPES
+
+  (*generator that always returns the passed value*)
+  val return : 'a -> ('a, 's) gen_state
+  val join : (('a, 's) gen_state, 's) gen_state -> ('a, 's) gen_state
+
+  val zip : ('a, 's) gen_state -> ('b, 's) gen_state -> ('a * 'b, 's) gen_state
+  val zip3 : ('a, 's) gen_state -> ('b, 's) gen_state -> ('c, 's) gen_state ->
+    ('a * 'b * 'c, 's) gen_state
+  val zip4 : ('a, 's) gen_state -> ('b, 's) gen_state -> ('c, 's) gen_state -> ('d, 's) gen_state ->
+    ('a * 'b * 'c * 'd, 's) gen_state
+  val map : ('a -> 'b) -> ('a, 's) gen_state -> ('b, 's) gen_state
+  val map2 : ('a -> 'b -> 'c) -> ('a, 's) gen_state -> ('b, 's) gen_state -> ('c, 's) gen_state
+  val map3 : ('a -> 'b -> 'c -> 'd) -> ('a, 's) gen_state -> ('b, 's) gen_state ->
+    ('c, 's) gen_state -> ('d, 's) gen_state
+  val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> ('a, 's) gen_state -> ('b, 's) gen_state ->
+    ('c, 's) gen_state -> ('d, 's) gen_state -> ('e, 's) gen_state
+
+  (*ensures that all generated values fulfill the predicate; loops if the predicate is never
+    satisfied by the generated values.*)
+  val filter : ('a -> bool) -> ('a, 's) gen_state -> ('a, 's) gen_state
+  val filter_bounded : int -> ('a -> bool) -> ('a, 's) gen_state -> ('a, 's) gen_state
+
+  (*bernoulli random variable with parameter p \<in> [0,1]*)
+  val bernoulli : real -> bool gen
+
+  (*random variable following a binomial distribution with parameters p \<in> [0,1] and n \<ge> 0*)
+  val binom_dist : real -> int -> int gen
+
+  (*range_int (x,y) r returns a value in [x;y]*)
+  val range_int : int * int -> int gen
+
+  (*randomly generates one of the given values*)
+  val elements : 'a vector -> 'a gen
+  (*randomly uses one of the given generators*)
+  val one_of : 'a gen vector -> 'a gen
+
+  (*randomly generates one of the given values*)
+  val elementsL : 'a list -> 'a gen
+  (*randomly uses one of the given generators*)
+  val one_ofL : 'a gen list -> 'a gen
+
+  (*chooses one of the given generators with a weighted random distribution.*)
+  val one_ofW : (int * 'a gen) vector -> 'a gen
+  (*chooses one of the given values with a weighted random distribution.*)
+  val elementsW : (int * 'a) vector -> 'a gen
+
+  (*chooses one of the given generators with a weighted random distribution.*)
+  val one_ofWL : (int * 'a gen) list -> 'a gen
+  (*chooses one of the given values with a weighted random distribution.*)
+  val elementsWL : (int * 'a) list -> 'a gen
+
+  (*creates a vector of length as returned by the passed int generator*)
+  val vector : (int, 's) gen_state -> ('a, 's) gen_state -> ('a vector, 's) gen_state
+
+  (*creates a list of length as returned by the passed int generator*)
+  val list : (int, 's) gen_state -> ('a, 's) gen_state -> ('a list, 's) gen_state
+
+  (*generates elements until the passed (generator) predicate fails;
+    returns a list of all values that satisfied the predicate*)
+  val unfold_while : ('a -> (bool, 's) gen_state) -> ('a, 's) gen_state -> ('a list, 's) gen_state
+  (*generates a random permutation of the given list*)
+  val shuffle : 'a list -> 'a list gen
+
+  (*generates SOME value if passed bool generator returns true and NONE otherwise*)
+  val option : (bool, 's) gen_state -> ('a, 's) gen_state -> ('a option, 's) gen_state
+
+  (*seq gen init_state creates a sequence where gen takes a state and returns the next element and
+    an updated state. The sequence stops when the first NONE value is returned by the generator.*)
+  val seq : ('a option, 's * Spec_Check_Random.rand) gen_state -> 's -> ('a Seq.seq) gen
+
+  (*creates a generator that returns all elements of the sequence in order*)
+  val of_seq : ('a option, 'a Seq.seq) gen_state
+
+  val unit : (unit, 's) gen_state
+  val ref_gen : ('a, 's) gen_state -> ('a Unsynchronized.ref, 's) gen_state
+
+  (*variant i g creates the ith variant of a given generator. It raises an error if i is negative.*)
+  val variant : (int, 'b) cogen
+  val cobool : (bool, 'b) cogen
+  val colist : ('a, 'b) cogen -> ('a list, 'b) cogen
+  val cooption : ('a, 'b) cogen -> ('a option, 'b) cogen
+
+end
+
+structure Spec_Check_Gen_Base : SPEC_CHECK_GEN_BASE =
+struct
+
+open Spec_Check_Gen_Types
+
+val return = pair
+fun join g = g #> (fn (g', r') => g' r')
+
+fun zip g1 g2 =
+  g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
+fun zip3 g1 g2 g3 =
+  zip g1 (zip g2 g3) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
+fun zip4 g1 g2 g3 g4 =
+  zip (zip g1 g2) (zip g3 g4) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
+
+fun map f g = g #>> f
+fun map2 f = map (uncurry f) oo zip
+fun map3 f = map (fn (a,b,c) => f a b c) ooo zip3
+fun map4 f = map (fn (a,b,c,d) => f a b c d) oooo zip4
+
+fun filter p gen r =
+  let fun loop (x, r) = if p x then (x, r) else loop (gen r)
+  in loop (gen r) end
+
+fun filter_bounded bound p gen r =
+  let fun loop 0 _ = raise Fail "Generator failed to satisfy predicate"
+        | loop n (x, r) = if p x then (x, r) else loop (n-1) (gen r)
+  in loop bound (gen r) end
+
+fun bernoulli p r = let val (x,r) = Spec_Check_Random.real_unit r in (x <= p, r) end
+
+fun binom_dist p n r =
+  let
+    fun binom_dist_unchecked _ 0 r = (0, r)
+      | binom_dist_unchecked p n r =
+        let fun int_of_bool b = if b then 1 else 0
+        in
+          bernoulli p r
+          |>> int_of_bool
+          ||> binom_dist_unchecked p (n-1)
+          |> (fn (x,(acc,r)) => (acc + x, r))
+        end
+   in if n < 0 then raise Domain else binom_dist_unchecked p n r end
+
+fun range_int (min, max) r =
+  if min > max
+  then raise Fail (Spec_Check_Util.spaces ["Range_Int:", string_of_int min, ">", string_of_int max])
+  else
+    Spec_Check_Random.real_unit r
+    |>> (fn s => Int.min (min + Real.floor (s * Real.fromInt (max - min + 1)), max))
+
+fun one_of v r =
+  let val (i, r) = range_int (0, Vector.length v - 1) r
+  in Vector.sub (v, i) r end
+
+fun one_ofW (v : (int * 'a gen) vector) r =
+  let
+    val weight_total = Vector.foldl (fn ((freq,_),acc) => freq + acc) 0 v
+    fun selectGen _ (_, Spec_Check_Util.Right gen) = Spec_Check_Util.Right gen
+      | selectGen rand ((weight, gen), Spec_Check_Util.Left acc) =
+      let val acc = acc + weight
+      in if acc < rand
+         then Spec_Check_Util.Left acc
+         else Spec_Check_Util.Right gen
+      end
+    val (threshhold, r) = range_int (1, weight_total) r
+    val gen = case Vector.foldl (selectGen threshhold) (Spec_Check_Util.Left 0) v of
+        Spec_Check_Util.Right gen => gen
+      | _ => raise Fail "Error in one_ofW - did you pass an empty vector or invalid frequencies?"
+  in gen r end
+
+fun elements v = one_of (Vector.map return v)
+fun elementsW v = one_ofW (Vector.map (fn p => p ||> return) v)
+
+fun one_ofL l = one_of (Vector.fromList l)
+fun one_ofWL l = one_ofW (Vector.fromList l)
+fun elementsL l = elements (Vector.fromList l)
+fun elementsWL l = elementsW (Vector.fromList l)
+
+fun list length_g g r =
+  let val (l, r) = length_g r
+  in fold_map (K g) (map_range I l) r end
+
+fun unfold_while bool_g_of_elem g r =
+  let
+    fun unfold_while_accum (xs, r) =
+      let
+        val (x, r) = g r
+        val (continue, r) = bool_g_of_elem x r
+      in
+        if continue
+        then unfold_while_accum (x::xs, r)
+        else (xs, r)
+      end
+  in unfold_while_accum ([], r) |>> rev end
+
+fun shuffle xs r =
+  let
+    val (ns, r) = list (return (length xs)) Spec_Check_Random.real_unit r
+    val real_ord = make_ord (op <=)
+    val xs = ListPair.zip (ns, xs) |> sort (real_ord o apply2 fst) |> List.map snd
+  in (xs, r) end
+
+fun vector length_g g = list length_g g #>> Vector.fromList
+
+fun option bool_g g r =
+  case bool_g r of
+    (false, r) => (NONE, r)
+  | (true, r) => map SOME g r
+
+fun seq gen xq r =
+  let
+    val (r1, r2) = Spec_Check_Random.split r
+    fun gen_next p () = case gen p of
+      (NONE, _) => NONE
+    | (SOME v, p) => SOME (v, Seq.make (gen_next p))
+  in (Seq.make (gen_next (xq, r1)), r2) end
+
+fun of_seq xq = case Seq.pull xq of
+    SOME (x, xq) => (SOME x, xq)
+  | NONE => (NONE, Seq.empty)
+
+fun unit s = return () s
+
+fun ref_gen gen r = let val (value, r) = gen r
+  in (Unsynchronized.ref value, r) end
+
+fun variant i g r =
+  if i < 0 then raise Subscript
+  else
+    let
+      fun nth i r =
+        let val (r1, r2) = Spec_Check_Random.split r
+        in if i = 0 then r1 else nth (i-1) r2 end
+    in g (nth i r) end
+
+fun cobool false = variant 0
+  | cobool true = variant 1
+
+fun colist _ [] = variant 0
+  | colist co (x::xs) = colist co xs o co x o variant 1
+
+fun cooption _ NONE = variant 0
+  | cooption co (SOME x) = co x o variant 1
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_function.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,41 @@
+(*  Title:      Tools/Spec_Check/generators/gen_function.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Random generators for functions.
+*)
+
+signature SPEC_CHECK_GEN_FUNCTION = sig
+  val function : ('a, 'b) Spec_Check_Gen_Types.cogen -> 'b Spec_Check_Gen_Types.gen ->
+    ('a -> 'b) Spec_Check_Gen_Types.gen
+  val function' : 'b Spec_Check_Gen_Types.gen -> (''a -> 'b) Spec_Check_Gen_Types.gen
+end
+
+structure Spec_Check_Gen_Function : SPEC_CHECK_GEN_FUNCTION =
+struct
+
+fun function cogen gen r =
+  let
+    val (r1, r2) = Spec_Check_Random.split r
+    fun g x = fst (cogen x gen r1)
+  in (g, r2) end
+
+fun function' gen r =
+  let
+    val (internal, external) = Spec_Check_Random.split r
+    val seed = Unsynchronized.ref internal
+    val table = Unsynchronized.ref []
+    fun new_entry k =
+      let
+        val (new_val, new_seed) = gen (!seed)
+        val _ =  seed := new_seed
+        val _ = table := AList.update (op =) (k, new_val) (!table)
+      in new_val end
+  in
+    (fn v1 =>
+      case AList.lookup (op =) (!table) v1 of
+        NONE => new_entry v1
+      | SOME v2 => v2, external)
+  end
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_int.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Tools/Spec_Check/generators/gen_int.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Random generators for ints.
+*)
+
+signature SPEC_CHECK_GEN_INT = sig
+
+  (*pos m generates an integer in [1, m]*)
+  val pos : int -> int Spec_Check_Gen_Types.gen
+  (*neg m generates an integer in [m, 1]*)
+  val neg : int -> int Spec_Check_Gen_Types.gen
+  (*nonneg m generates an integer in [0, m]*)
+  val nonneg : int -> int Spec_Check_Gen_Types.gen
+  (*nonpos m generates an integer in [m, 0]*)
+  val nonpos : int -> int Spec_Check_Gen_Types.gen
+
+  val coint : (int, 'b) Spec_Check_Gen_Types.cogen
+
+end
+
+structure Spec_Check_Gen_Int : SPEC_CHECK_GEN_INT =
+struct
+
+open Spec_Check_Gen_Base
+
+fun pos m = range_int (1, m)
+fun neg m = range_int (m, ~1)
+fun nonneg m = range_int (0, m)
+fun nonpos m = range_int (m, 0)
+
+fun coint n =
+  if n = 0 then variant 0
+  else if n < 0 then coint (~n) o variant 1
+  else coint (n div 2) o variant 2
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_real.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,65 @@
+(*  Title:      Tools/Spec_Check/generators/gen_real.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Random generators for reals.
+*)
+
+signature SPEC_CHECK_GEN_REAL = sig
+
+  (*range_real (x,y) r returns a value in [x, y]*)
+  val range_real : real * real -> real Spec_Check_Gen_Types.gen
+
+  val real : real Spec_Check_Gen_Types.gen
+
+  val real_pos : real Spec_Check_Gen_Types.gen
+  val real_neg : real Spec_Check_Gen_Types.gen
+
+  val real_nonneg : real Spec_Check_Gen_Types.gen
+  val real_nonpos : real Spec_Check_Gen_Types.gen
+
+  val real_finite : real Spec_Check_Gen_Types.gen
+end
+
+structure Spec_Check_Gen_Real : SPEC_CHECK_GEN_REAL =
+struct
+
+open Spec_Check_Gen_Base
+open Spec_Check_Gen_Text
+
+fun range_real (min, max) r =
+  if min > max
+  then
+    raise Fail (Spec_Check_Util.spaces["Range_Real:", string_of_real min, ">", string_of_real max])
+  else Spec_Check_Random.real_unit r |>> (fn s => min + (s * max - s * min))
+
+val digits = string (range_int (1, Real.precision)) (range_char (#"0", #"9"))
+
+val {exp=minExp,...} = Real.toManExp Real.minPos
+val {exp=maxExp,...} = Real.toManExp Real.posInf
+
+val ratio = 99
+
+fun mk r =
+  let
+    val (a, r) = digits r
+    val (b, r) = digits r
+    val (e, r) = range_int (minExp div 4, maxExp div 4) r
+    val x = String.concat [a, ".", b, "E", Int.toString e]
+  in
+    (the (Real.fromString x), r)
+  end
+
+val real_pos = one_ofWL ((ratio, mk) ::
+  List.map ((pair 1) o return) [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos])
+
+val real_neg = map Real.~ real_pos
+
+val real_nonneg = one_ofWL [(1, return 0.0), (ratio, real_pos)]
+val real_nonpos = one_ofWL [(1, return 0.0), (ratio, real_neg)]
+
+val real = one_ofL [real_nonneg, real_nonpos]
+
+val real_finite = filter Real.isFinite real
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_term.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,269 @@
+(*  Title:      Tools/Spec_Check/generators/gen_term.ML
+    Author:     Sebastian Willenbrink and Kevin Kappelmann TU Muenchen
+
+Generators for terms and types.
+*)
+signature SPEC_CHECK_GEN_TERM = sig
+  (* sort generators *)
+
+  (*first parameter determines the number of classes to pick*)
+  val sort : (int, 's) Spec_Check_Gen_Types.gen_state -> (class, 's) Spec_Check_Gen_Types.gen_state
+    -> (sort, 's) Spec_Check_Gen_Types.gen_state
+  val dummyS : (sort, 's) Spec_Check_Gen_Types.gen_state
+
+  (* name generators *)
+  (*parameters: a base name and a generator for the number of variants to choose from based on then
+    passed base name*)
+  val basic_name : string -> int Spec_Check_Gen_Types.gen -> string Spec_Check_Gen_Types.gen
+
+  val indexname : (string, 's) Spec_Check_Gen_Types.gen_state ->
+    (int, 's) Spec_Check_Gen_Types.gen_state -> (indexname, 's) Spec_Check_Gen_Types.gen_state
+
+  (*a variant with base name "k"*)
+  val type_name : int Spec_Check_Gen_Types.gen -> string Spec_Check_Gen_Types.gen
+
+  (*creates a free type variable name from a passed basic name generator*)
+  val tfree_name : (string, 's) Spec_Check_Gen_Types.gen_state ->
+    (string, 's) Spec_Check_Gen_Types.gen_state
+  (*chooses a variant with base name "'a"*)
+  val tfree_name' : int Spec_Check_Gen_Types.gen -> string Spec_Check_Gen_Types.gen
+
+  (*creates a type variable name from a passed basic name (e.g. "a") generator*)
+  val tvar_name : (indexname, 's) Spec_Check_Gen_Types.gen_state ->
+    (indexname, 's) Spec_Check_Gen_Types.gen_state
+  (*chooses a variant with base name "'a"*)
+  val tvar_name' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    indexname Spec_Check_Gen_Types.gen
+
+  (*chooses a variant with base name "c"*)
+  val const_name : int Spec_Check_Gen_Types.gen -> string Spec_Check_Gen_Types.gen
+  (*chooses a variant with base name "f"*)
+  val free_name : int Spec_Check_Gen_Types.gen -> string Spec_Check_Gen_Types.gen
+  (*chooses a variant with base name "v*)
+  val var_name : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    indexname Spec_Check_Gen_Types.gen
+
+  (* typ  generators *)
+
+  val tfree : (string, 's) Spec_Check_Gen_Types.gen_state ->
+    (sort, 's) Spec_Check_Gen_Types.gen_state -> (typ, 's) Spec_Check_Gen_Types.gen_state
+  (*uses tfree_name' and dummyS to create a free type variable*)
+  val tfree' : int Spec_Check_Gen_Types.gen -> typ Spec_Check_Gen_Types.gen
+
+  val tvar : (indexname, 's) Spec_Check_Gen_Types.gen_state ->
+    (sort, 's) Spec_Check_Gen_Types.gen_state -> (typ, 's) Spec_Check_Gen_Types.gen_state
+  (*uses tvar' and dummyS to create a type variable*)
+  val tvar' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    typ Spec_Check_Gen_Types.gen
+
+  (*atyp tfree_gen tvar_gen (weight_tfree, weight_tvar)*)
+  val atyp : typ Spec_Check_Gen_Types.gen -> typ Spec_Check_Gen_Types.gen -> (int * int) ->
+    typ Spec_Check_Gen_Types.gen
+  (*uses tfree' and tvar' to create an atomic type*)
+  val atyp' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen -> (int * int) ->
+    typ Spec_Check_Gen_Types.gen
+
+  (*type' type_name_gen arity_gen tfree_gen tvar_gen (weight_type, weight_tfree, weight_tvar)*)
+  val type' : string Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    typ Spec_Check_Gen_Types.gen -> typ Spec_Check_Gen_Types.gen ->
+    (int * int * int) -> typ Spec_Check_Gen_Types.gen
+  (*uses type_name to generate a type*)
+  val type'' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    typ Spec_Check_Gen_Types.gen -> typ Spec_Check_Gen_Types.gen -> (int * int * int) ->
+    typ Spec_Check_Gen_Types.gen
+
+  (*typ type_gen tfree_gen tvar_gen (wtype, wtfree, wtvar)*)
+  val typ : typ Spec_Check_Gen_Types.gen -> typ Spec_Check_Gen_Types.gen ->
+    typ Spec_Check_Gen_Types.gen -> (int * int * int) -> typ Spec_Check_Gen_Types.gen
+  (*uses type'' for its type generator*)
+  val typ' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    typ Spec_Check_Gen_Types.gen -> typ Spec_Check_Gen_Types.gen -> (int * int * int) ->
+    typ Spec_Check_Gen_Types.gen
+  (*uses typ' with tfree' and tvar' parameters*)
+  val typ'' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    int Spec_Check_Gen_Types.gen -> (int * int * int) -> typ Spec_Check_Gen_Types.gen
+
+  val dummyT : (typ, 's) Spec_Check_Gen_Types.gen_state
+
+  (* term generators *)
+
+  val const : (string, 's) Spec_Check_Gen_Types.gen_state ->
+    (typ, 's) Spec_Check_Gen_Types.gen_state -> (term, 's) Spec_Check_Gen_Types.gen_state
+  (*uses const_name and dummyT to create a constant*)
+  val const' : int Spec_Check_Gen_Types.gen -> term Spec_Check_Gen_Types.gen
+
+  val free : (string, 's) Spec_Check_Gen_Types.gen_state ->
+    (typ, 's) Spec_Check_Gen_Types.gen_state -> (term, 's) Spec_Check_Gen_Types.gen_state
+  (*uses free_name and dummyT to create a free variable*)
+  val free' : int Spec_Check_Gen_Types.gen -> term Spec_Check_Gen_Types.gen
+
+  val var : (indexname, 's) Spec_Check_Gen_Types.gen_state ->
+    (typ, 's) Spec_Check_Gen_Types.gen_state -> (term, 's) Spec_Check_Gen_Types.gen_state
+  (*uses var_name and dummyT to create a variable*)
+  val var' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    term Spec_Check_Gen_Types.gen
+
+  val bound : (int, 's) Spec_Check_Gen_Types.gen_state -> (term, 's) Spec_Check_Gen_Types.gen_state
+
+  (*aterm const_gen free_gen var_gen bound_gen
+    (weight_const, weight_free, weight_var, weight_bound*)
+  val aterm : term Spec_Check_Gen_Types.gen -> term Spec_Check_Gen_Types.gen ->
+    term Spec_Check_Gen_Types.gen -> term Spec_Check_Gen_Types.gen -> (int * int * int * int) ->
+    term Spec_Check_Gen_Types.gen
+  (*uses const', free', and var' to create an atomic term*)
+  val aterm' : int Spec_Check_Gen_Types.gen -> int Spec_Check_Gen_Types.gen ->
+    (int * int * int * int) -> term Spec_Check_Gen_Types.gen
+
+  (*term_tree f init_state - where "f height index state" returns "((term, num_args), new_state)" -
+    generates a term by applying f to every node and expanding that node depending
+    on num_args returned by f.
+    Traversal order: function \<rightarrow> first argument \<rightarrow> ... \<rightarrow> last argument
+    The tree is returned in its applicative term form: (...((root $ child1) $ child2) .. $ childn).
+
+    Arguments of f:
+    - height describes the distance from the root (starts at 0)
+    - index describes the global index in that tree layer, left to right (0 \<le> index < width)
+    - state is passed along according to above traversal order
+
+    Return value of f:
+    - term is the term whose arguments will be generated next.
+    - num_args specifies how many arguments should be passed to the term.
+    - new_state is passed along according to the traversal above.*)
+  val term_tree : (int -> int -> (term * int, 's) Spec_Check_Gen_Types.gen_state) ->
+    (term, 's) Spec_Check_Gen_Types.gen_state
+
+  (*In contrast to term_tree, f now takes a (term, index_of_argument) list which specifies the path
+    from the root to the current node.*)
+  val term_tree_path : ((term * int) list -> (term * int, 's) Spec_Check_Gen_Types.gen_state) ->
+    (term, 's) Spec_Check_Gen_Types.gen_state
+
+end
+
+structure Spec_Check_Gen_Term : SPEC_CHECK_GEN_TERM =
+struct
+
+structure Gen = Spec_Check_Gen_Base
+
+fun sort size_gen = Gen.list size_gen
+fun dummyS s = Gen.return Term.dummyS s
+
+fun basic_name name num_variants_gen =
+  num_variants_gen
+  #>> (fn i => name ^ "_" ^ string_of_int i)
+
+fun indexname basic_name_gen = Gen.zip basic_name_gen
+
+fun type_name num_variants_gen = basic_name "k" num_variants_gen
+
+fun tfree_name basic_name_gen = Gen.map (curry op^"'") basic_name_gen
+fun tfree_name' num_variants_gen = tfree_name (basic_name "a" num_variants_gen)
+
+fun tvar_name indexname_gen = Gen.map (curry op^"'" |> apfst) indexname_gen
+fun tvar_name' num_variants_gen =
+  tvar_name o indexname (basic_name "a" num_variants_gen)
+
+fun const_name num_variants_gen = basic_name "c" num_variants_gen
+fun free_name num_variants_gen = basic_name "v" num_variants_gen
+fun var_name num_variants_gen = indexname (free_name num_variants_gen)
+
+(* types *)
+
+fun tfree name_gen = Gen.map TFree o Gen.zip name_gen
+fun tfree' num_variants_gen =
+  tfree_name' num_variants_gen
+  |> (fn name_gen => tfree name_gen dummyS)
+
+fun tvar idx_gen = Gen.map TVar o Gen.zip idx_gen
+fun tvar' num_variants_gen =
+  tvar_name' num_variants_gen
+  #> (fn name_gen => tvar name_gen dummyS)
+
+fun atyp tfree_gen tvar_gen (wtfree, wtvar) =
+  Gen.one_ofWL [(wtfree, tfree_gen), (wtvar, tvar_gen)]
+fun atyp' num_variants_gen = atyp (tfree' num_variants_gen) o tvar' num_variants_gen
+
+fun type' type_name_gen arity_gen tfree_gen tvar_gen (weights as (wtype, wtfree, wtvar)) =
+  (*eta-abstract to avoid strict evaluation, causing an infinite loop*)
+  [(wtype, fn r => type' type_name_gen arity_gen tfree_gen tvar_gen weights r),
+   (wtfree, fn r => tfree_gen r), (wtvar, fn r => tvar_gen r)]
+  |> Gen.one_ofWL
+  |> Gen.list arity_gen
+  |> Gen.zip type_name_gen
+  |> Gen.map Type
+
+fun type'' num_variants_gen = type_name num_variants_gen |> type'
+
+fun typ type_gen tfree_gen tvar_gen (wtype, wtfree, wtvar) =
+  Gen.one_ofWL [(wtype, type_gen), (wtfree, tfree_gen), (wtvar, tvar_gen)]
+fun typ' num_variants_gen arity_gen tfree_gen tvar_gen weights =
+  typ (type'' num_variants_gen arity_gen tfree_gen tvar_gen weights) tfree_gen tvar_gen weights
+fun typ'' num_variants_gen arity_gen =
+  typ' num_variants_gen arity_gen (tfree' num_variants_gen) o tvar' num_variants_gen
+
+fun dummyT s = Gen.return Term.dummyT s
+
+(* terms *)
+
+fun const name_gen = Gen.map Const o Gen.zip name_gen
+fun const' num_variants_gen =
+  const_name num_variants_gen
+  |> (fn name_gen => const name_gen dummyT)
+
+fun free name_gen = Gen.map Free o Gen.zip name_gen
+fun free' num_variants_gen =
+  free_name num_variants_gen
+  |> (fn name_gen => free name_gen dummyT)
+
+fun var idx_gen = Gen.map Var o Gen.zip idx_gen
+fun var' num_variants_gen =
+  var_name num_variants_gen
+  #> (fn name_gen => var name_gen dummyT)
+
+fun bound int_gen = Gen.map Bound int_gen
+
+fun aterm const_gen free_gen var_gen bound_gen (wconst, wfree, wvar, wbound) =
+  Gen.one_ofWL [(wconst, const_gen), (wfree, free_gen), (wvar, var_gen), (wbound, bound_gen)]
+fun aterm' num_variants_gen index_gen =
+  aterm (const' num_variants_gen) (free' num_variants_gen) (var' num_variants_gen index_gen)
+    (bound num_variants_gen)
+
+(*nth_map has no default*)
+fun nth_map_default 0 f _ (x::xs) = f x :: xs
+  | nth_map_default 0 f d [] = [f d]
+  | nth_map_default n f d [] = replicate (n-1) d @ [f d]
+  | nth_map_default n f d (x::xs) = x :: nth_map_default (n-1) f d xs
+
+fun term_tree term_gen state =
+  let
+    fun nth_incr n = nth_map_default n (curry op+ 1) (~1)
+    fun build_tree indices height state =
+      let
+        (*indices stores the number of nodes visited so far at each height*)
+        val indices = nth_incr height indices
+        val index = nth indices height
+        (*generate the term for the current node*)
+        val ((term, num_args), state) = term_gen height index state
+        fun build_child (children, indices, state) =
+          build_tree indices (height + 1) state
+          |> (fn (child, indices, state) => (child :: children, indices, state))
+        (*generate the subtrees for each argument*)
+        val (children, indices, state) = fold (K build_child) (1 upto num_args) ([], indices, state)
+      in (Term.list_comb (term, (rev children)), indices, state) end
+  in
+    build_tree [] 0 state
+    |> (fn (term, _, state) => (term, state))
+  end
+
+fun term_tree_path f init_state =
+  let
+    fun build_tree path state =
+      let
+        val ((term, num_args), state) = f path state
+        fun build_children i (args, state) =
+          build_tree ((term, i) :: path) state
+          |>> (fn x => x :: args)
+        val (children, state) = fold build_children (0 upto num_args-1) ([], state)
+      in (Term.list_comb (term, (rev children)), state) end
+  in build_tree [] init_state end
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_text.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Tools/Spec_Check/generators/gen_text.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Random generators for chars and strings.
+*)
+
+signature SPEC_CHECK_GEN_TEXT = sig
+
+  val range_char : char * char -> char Spec_Check_Gen_Types.gen
+  val char : char Spec_Check_Gen_Types.gen
+
+  val char_of : string -> char Spec_Check_Gen_Types.gen
+
+  val string : int Spec_Check_Gen_Types.gen -> char Spec_Check_Gen_Types.gen ->
+    string Spec_Check_Gen_Types.gen
+
+  val substring : string Spec_Check_Gen_Types.gen -> substring Spec_Check_Gen_Types.gen
+
+  val cochar : (char, 'b) Spec_Check_Gen_Types.cogen
+  val costring : (string, 'b) Spec_Check_Gen_Types.cogen
+  val cosubstring : (substring, 'b) Spec_Check_Gen_Types.cogen
+
+  val digit : char Spec_Check_Gen_Types.gen
+  val lowercase_letter : char Spec_Check_Gen_Types.gen
+  val uppercase_letter : char Spec_Check_Gen_Types.gen
+  val letter : char Spec_Check_Gen_Types.gen
+end
+
+structure Spec_Check_Gen_Text : SPEC_CHECK_GEN_TEXT =
+struct
+
+open Spec_Check_Gen_Base
+
+type char = Char.char
+type string = String.string
+type substring = Substring.substring
+
+fun range_char (lo, hi) = map Char.chr (range_int (Char.ord lo, Char.ord hi))
+val char = range_char (Char.minChar, Char.maxChar)
+
+fun char_of s =
+  one_of (Vector.tabulate (String.size s, fn i => return (String.sub (s, i))))
+
+fun string length_g g = list length_g g #>> CharVector.fromList
+
+fun substring gen r =
+  let
+    val (s, r) = gen r
+    val (i, r) = range_int (0, String.size s) r
+    val (j, r) = range_int (0, String.size s - i) r
+  in
+    (Substring.substring (s, i, j), r)
+  end
+
+fun cochar c =
+  if Char.ord c = 0 then variant 0
+  else cochar (Char.chr (Char.ord c div 2)) o variant 1
+
+fun cosubstring s = colist cochar (Substring.explode s)
+
+fun costring s = cosubstring (Substring.full s)
+
+val digit = range_char (#"0", #"9")
+
+val lowercase_letter = range_char (#"a", #"z")
+val uppercase_letter = range_char (#"A", #"Z")
+val letter = one_ofL [lowercase_letter, uppercase_letter]
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/generators/gen_types.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,34 @@
+(*  Title:      Tools/Spec_Check/generators/gen_types.ML
+    Author:     Kevin Kappelmann
+
+Shared type definitions for SpecCheck generators.
+*)
+
+signature SPEC_CHECK_GEN_TYPES =
+sig
+
+  (*consumes a state and returns a new state along with a generated value*)
+  type ('a, 's) gen_state = 's -> 'a * 's
+  (*consumes a random seed and returns an unused one along with a generated value*)
+  type 'a gen = ('a, Spec_Check_Random.rand) gen_state
+
+  (*a cogenerator produces new generators depending on an input element and an existing generator.*)
+  type ('a, 'b, 's) cogen_state = 'a -> ('b, 's) gen_state -> ('b, 's) gen_state
+
+  (*a cogenerator produces new generators depending on an input element and an existing generator.*)
+  type ('a, 'b) cogen = ('a, 'b, Spec_Check_Random.rand) cogen_state
+
+end
+
+structure Spec_Check_Gen_Types : SPEC_CHECK_GEN_TYPES =
+struct
+
+type ('a, 's) gen_state = 's -> 'a * 's
+
+type 'a gen = ('a, Spec_Check_Random.rand) gen_state
+
+type ('a, 'b, 's) cogen_state = 'a -> ('b, 's) gen_state -> ('b, 's) gen_state
+
+type ('a, 'b) cogen = ('a, 'b, Spec_Check_Random.rand) cogen_state
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/lecker.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,23 @@
+(*  Title:      Tools/Spec_Check/lecker.ML
+    Author:     Kevin Kappelmann
+
+Testing framework that lets you combine SpecCheck tests into test suites.
+
+TODO: this file can be largely extended to become a pendant of Haskell's tasty:
+https://hackage.haskell.org/package/tasty
+*)
+
+signature LECKER =
+sig
+  (*the first parameter to test_group will usually be a context*)
+  val test_group : 'a -> 's -> ('a -> 's -> 's) list -> 's
+end
+
+structure Lecker : LECKER =
+struct
+
+fun test_group _ s [] = s
+  | test_group fixed_param s (t::ts) =
+      fold (fn t => (Pretty.writeln (Pretty.para ""); t fixed_param)) ts (t fixed_param s)
+
+end
--- a/src/Tools/Spec_Check/output_style.ML	Fri Jun 18 15:03:12 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(*  Title:      Tools/Spec_Check/output_style.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Output styles for presenting Spec_Check's results.
-*)
-
-structure Output_Style : sig end =
-struct
-
-(* perl style *)
-
-val perl_style =
-  Spec_Check.register_style "Perl"
-    (fn ctxt => fn tag =>
-      let
-        val target = Config.get ctxt Spec_Check.gen_target
-        val namew = Config.get ctxt Spec_Check.column_width
-        val sort_examples = Config.get ctxt Spec_Check.sort_examples
-        val show_stats = Config.get ctxt Spec_Check.show_stats
-        val limit = Config.get ctxt Spec_Check.examples
-
-        val resultw = 8
-        val countw = 20
-        val allw = namew + resultw + countw + 2
-
-        val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I
-
-        fun result ({count = 0, ...}, _) _ = "dubious"
-          | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
-          | result ({count, tags}, badobjs) true =
-              if not (null badobjs) then "FAILED"
-              else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
-              else "ok"
-
-        fun ratio (0, _) = "(0/0 passed)"
-          | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
-          | ratio (count, n) =
-              "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
-
-        fun update (stats, badobjs) donep =
-          "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
-          StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
-          StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
-
-        fun status (_, result, (stats, badobjs)) =
-          if Property.failure result then warning (update (stats, badobjs) false) else ()
-
-        fun prtag count (tag, n) first =
-          if String.isPrefix "__" tag then ("", first)
-          else
-             let
-               val ratio = round ((real n / real count) * 100.0)
-             in
-               (((if first then "" else StringCvt.padRight #" " allw "\n") ^
-                 StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
-               false)
-             end
-
-        fun prtags ({count, tags} : Property.stats) =
-          if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
-
-        fun err badobjs =
-          let
-            fun iter [] _ = ()
-              | iter (e :: es) k =
-                  (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
-                    StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
-                  iter es (k + 1))
-          in
-            iter (maybe_sort (take limit (map_filter I badobjs))) 0
-          end
-
-        fun finish (stats, badobjs) =
-          if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
-          else (warning (update (stats, badobjs) true); err badobjs)
-      in
-        {status = status, finish = finish}
-      end)
-
-val _ = Theory.setup perl_style;
-
-
-(* CM style: meshes with CM output; highlighted in sml-mode *)
-
-val cm_style =
-  Spec_Check.register_style "CM"
-    (fn ctxt => fn tag =>
-      let
-        fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
-        val gen_target = Config.get ctxt Spec_Check.gen_target
-        val _ = writeln ("[testing " ^ tag ^ "... ")
-        fun finish ({count, ...} : Property.stats, badobjs) =
-          (case (count, badobjs) of
-            (0, []) => warning ("no valid cases generated]")
-          | (n, []) => writeln (
-                if n >= gen_target then "ok]"
-                else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
-          | (_, es) =>
-              let
-                val wd = size (string_of_int (length es))
-                fun each (NONE, _) = ()
-                  | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
-              in
-                (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
-              end)
-      in
-        {status = K (), finish = finish}
-      end)
-
-val _ = Theory.setup cm_style;
-
-end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_styles/Spec_Check_Output_Style.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,20 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Output Styles\<close>
+theory Spec_Check_Output_Style
+imports
+  Spec_Check_Base
+  Spec_Check_Show
+begin
+
+
+paragraph \<open>Summary\<close>
+text \<open>Output styles for SpecCheck take the result of a test run and process it accordingly,
+e.g. by printing it or storing it to a file.\<close>
+
+
+ML_file \<open>output_style_types.ML\<close>
+ML_file \<open>output_style_perl.ML\<close>
+ML_file \<open>output_style_custom.ML\<close>
+ML_file \<open>output_style.ML\<close>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_styles/output_style.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,20 @@
+(*  Title:      Tools/Spec_Check/output_styles/output_style.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Output styles for presenting SpecCheck results.
+*)
+
+signature SPEC_CHECK_DEFAULT_OUTPUT_STYLE =
+sig
+  include SPEC_CHECK_OUTPUT_STYLE_TYPES
+  val default : 'a output_style
+end
+
+structure Spec_Check_Default_Output_Style : SPEC_CHECK_DEFAULT_OUTPUT_STYLE =
+struct
+
+open Spec_Check_Output_Style_Types
+val default = Spec_Check_Output_Style_Custom.style
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_styles/output_style_custom.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,83 @@
+(*  Title:      Tools/Spec_Check/output_style/output_style_custom.ML
+    Author:     Lukas Bulwahn, Nicolai Schaffroth, Kevin Kappelmann TU Muenchen
+    Author:     Christopher League
+
+Custom-made, QuickCheck-inspired output style for SpecCheck.
+*)
+
+structure Spec_Check_Output_Style_Custom : SPEC_CHECK_OUTPUT_STYLE =
+struct
+
+open Spec_Check_Base
+
+fun print_success stats =
+  let
+    val num_success_tests = string_of_int (#num_success_tests stats)
+    val num_discarded_tests = #num_discarded_tests stats
+    val discarded_str =
+      if num_discarded_tests = 0
+      then "."
+      else Spec_Check_Util.spaces [";", string_of_int num_discarded_tests,  "discarded."]
+  in
+    implode ["OK, passed ", num_success_tests, " tests", discarded_str]
+    |> Spec_Check_Util.pwriteln
+  end
+
+fun print_gave_up stats =
+  let
+    val num_success_tests = string_of_int (#num_success_tests stats)
+    val num_discarded_tests = string_of_int (#num_discarded_tests stats)
+  in
+    Spec_Check_Util.spaces ["Gave up! Passed only", num_success_tests, "test(s);", num_discarded_tests,
+      "discarded test(s)."]
+    |> Spec_Check_Util.pwarning
+  end
+
+fun print_failure_data ctxt show_opt failure_data =
+  case #the_exception failure_data of
+    SOME exn =>
+      cat_lines ["Exception during test run:", exnMessage exn]
+      |> Spec_Check_Util.pwarning
+  | NONE => case show_opt of
+      NONE => ()
+    | SOME show =>
+      let
+        val sort_counterexamples = Config.get ctxt Spec_Check_Configuration.sort_counterexamples
+        val maybe_sort = if sort_counterexamples then sort (int_ord o apply2 size) else I
+        val counterexamples =
+          #counterexamples failure_data
+          |> map (Pretty.string_of o show)
+          |> maybe_sort
+      in fold (fn x => fn _ => Spec_Check_Util.pwarning x) counterexamples () end
+
+fun print_failure ctxt show_opt (stats, failure_data) =
+  ((Spec_Check_Util.spaces ["Failed! Falsified (after", string_of_int (num_tests stats), "test(s) and ",
+    string_of_int (num_shrinks stats), "shrink(s)):"] |> Spec_Check_Util.pwarning);
+  print_failure_data ctxt show_opt failure_data)
+
+fun print_stats ctxt stats total_time =
+  let
+    val show_stats = Config.get ctxt Spec_Check_Configuration.show_stats
+    (*the time spent in the test function in relation to the total time spent;
+      the latter includes generating test cases and overhead from the framework*)
+    fun show_time {elapsed, ...} =
+      implode ["Time: ", Time.toString elapsed, "s (run) / ", Time.toString (#elapsed total_time),
+        "s (total)"]
+  in
+    if not show_stats
+    then ()
+    else Spec_Check_Util.pwriteln (show_time (#timing stats))
+  end
+
+fun style show_opt ctxt name total_time result =
+  let val stats = stats_of_result result
+  in
+    Spec_Check_Util.pwriteln (Spec_Check_Util.spaces ["Testing:", name]);
+    (case result of
+      Success _ => print_success stats
+    | Gave_Up _ => print_gave_up stats
+    | Failure data => print_failure ctxt show_opt data);
+    print_stats ctxt stats total_time
+  end
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_styles/output_style_perl.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,55 @@
+(*  Title:      Tools/Spec_Check/output_styles/output_style_perl.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Perl output styles for SpecCheck.
+*)
+
+structure Spec_Check_Output_Style_Perl : SPEC_CHECK_OUTPUT_STYLE =
+struct
+
+open Spec_Check_Configuration
+open Spec_Check_Base
+
+fun style show_opt ctxt name timing result =
+  let
+    val sort_counterexamples =  Config.get ctxt sort_counterexamples
+    val maybe_sort = if sort_counterexamples then sort (int_ord o apply2 size) else I
+
+    val stats = stats_of_result result
+    val num_failed_tests = #num_failed_tests stats
+
+    fun code (Success _) = "ok"
+      | code (Gave_Up _) = "Gave up!"
+      | code (Failure _) = "FAILED"
+
+    fun ratio stats =
+      let
+        val num_success_tests = #num_success_tests stats
+      in
+        if num_failed_tests = 0
+        then implode ["(", string_of_int num_success_tests, " passed)"]
+        else implode ["(", string_of_int num_success_tests, "/",
+          string_of_int (num_success_tests + num_failed_tests),  " passed)"]
+      end
+
+    val result_string = name ^ ".\n" ^ code result ^ " " ^ ratio stats
+
+    fun show_counterexamples counterexamples =
+      case show_opt of
+        SOME show =>
+          (case maybe_sort (map (Pretty.string_of o show) counterexamples) of
+            [] => ()
+          | es => (Spec_Check_Util.pwarning "Counterexamples:";
+              fold (fn x => fn _ => Spec_Check_Util.pwarning x) es ()))
+      | NONE => ()
+
+  in
+    case result of
+      Success _ => Spec_Check_Util.pwriteln result_string
+    | Gave_Up _ => Spec_Check_Util.pwarning result_string
+    | Failure (_, failure_data) =>
+        (Spec_Check_Util.pwarning result_string; show_counterexamples (#counterexamples failure_data))
+  end
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/output_styles/output_style_types.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,24 @@
+(*  Title:      Tools/Spec_Check/output_styles/output_style_types.ML
+    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Christopher League
+
+Shared types for SpecCheck output styles.
+*)
+signature SPEC_CHECK_OUTPUT_STYLE_TYPES =
+sig
+  type 'a output_style = 'a Spec_Check_Show.show option -> Proof.context -> string ->
+    Timing.timing -> 'a Spec_Check_Base.result -> unit
+end
+
+structure Spec_Check_Output_Style_Types : SPEC_CHECK_OUTPUT_STYLE_TYPES =
+struct
+
+type 'a output_style = 'a Spec_Check_Show.show option -> Proof.context -> string -> Timing.timing ->
+  'a Spec_Check_Base.result -> unit
+
+end
+
+signature SPEC_CHECK_OUTPUT_STYLE =
+sig
+  val style : 'a Spec_Check_Output_Style_Types.output_style
+end
--- a/src/Tools/Spec_Check/property.ML	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/Tools/Spec_Check/property.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -2,76 +2,45 @@
     Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     Author:     Christopher League
 
-Conditional properties that can track argument distribution.
+The base module of testable properties.
+A property is the type of values that SpecCheck knows how to test.
+Properties not only test whether a given predicate holds, but, for example, can also have
+preconditions.
 *)
 
-signature PROPERTY =
+signature SPEC_CHECK_PROPERTY =
 sig
 
-type 'a pred = 'a -> bool
-type 'a prop
-val pred : 'a pred -> 'a prop
-val pred2 : ('a * 'b) pred -> 'b -> 'a  prop
-val implies : 'a pred * 'a prop -> 'a prop
-val ==> : 'a pred * 'a pred -> 'a prop
-val trivial : 'a pred -> 'a prop -> 'a prop
-val classify : 'a pred -> string -> 'a prop -> 'a prop
-val classify' : ('a -> string option) -> 'a prop -> 'a prop
-
-(*Results*)
-type result = bool option
-type stats = { tags : (string * int) list, count : int }
-val test : 'a prop -> 'a * stats -> result * stats
-val stats : stats
-val success : result pred
-val failure : result pred
+  type 'a pred = 'a -> bool
+  (*the type of values testable by SpecCheck*)
+  type 'a prop
+  (*transforms a predicate into a testable property*)
+  val prop : 'a pred -> 'a prop
+  (*implication for properties: if the first argument evaluates to false, the test case is
+    discarded*)
+  val implies : 'a pred -> 'a prop -> 'a prop
+  (*convenient notation for `implies` working on predicates*)
+  val ==> : 'a pred * 'a pred -> 'a prop
 
 end
 
-structure Property : PROPERTY =
+structure Spec_Check_Property : SPEC_CHECK_PROPERTY =
 struct
 
-type result = bool option
-type stats = { tags : (string * int) list, count : int }
 type 'a pred = 'a -> bool
-type 'a prop = 'a * stats -> result * stats
-
-fun success (SOME true) = true
-  | success _ = false
+type 'a prop = 'a -> Spec_Check_Base.result_single
 
-fun failure (SOME false) = true
-  | failure _ = false
-
-fun apply f x = (case try f x of NONE => SOME false | some => some)
-fun pred f (x,s) = (apply f x, s)
-fun pred2 f z = pred (fn x => f (x, z))
-
-fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
-
-fun ==> (p1, p2) = implies (p1, pred p2)
+fun apply f x = Spec_Check_Base.Result (f x)
+  (*testcode may throw arbitrary exceptions; interrupts must not be caught!*)
+  handle exn => if Exn.is_interrupt exn then Exn.reraise exn else Spec_Check_Base.Exception exn
 
-fun wrap trans p (x,s) =
-  let val (result,s) = p (x,s)
-  in (result, trans (x, result, s)) end
+fun prop f x = apply f x
 
-fun classify' f =
-  wrap (fn (x, result, {tags, count}) =>
-    { tags =
-        if is_some result then
-          (case f x of
-            NONE => tags
-          | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
-        else tags,
-     count = count })
+fun implies cond prop x =
+  if cond x
+  then prop x
+  else Spec_Check_Base.Discard
 
-fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
-
-fun trivial cond = classify cond "trivial"
-
-fun test p =
-  wrap (fn (_, result, {tags, count}) =>
-    { tags = tags, count = if is_some result then count + 1 else count }) p
-
-val stats = { tags = [], count = 0 }
+fun ==> (p1, p2) = implies p1 (prop p2)
 
 end
--- a/src/Tools/Spec_Check/random.ML	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/Tools/Spec_Check/random.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -2,45 +2,60 @@
     Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
     Author:     Christopher League
 
-Random number engine.
+A Lehmer random number generator:
+https://en.wikipedia.org/wiki/Lehmer_random_number_generator
+We use int to avoid any float imprecision problems (and the seed is an int anyway).
+The parameters "a" and "m" are selected according to the recommendation in above article;
+they are an an improved version of the so-called "minimal standard" (MINSTD) generator.
+
+This file only contains those functions that rely on the internal integer representation of rand.
 *)
 
-signature RANDOM =
+signature SPEC_CHECK_RANDOM =
 sig
   type rand
+  (*creates a new random seed*)
   val new : unit -> rand
-  val range : int * int -> rand -> int * rand
+  (*creates a new random seed from a given one*)
+  val next : rand -> rand
+  (*use this function for reproducible randomness; inputs \<le> 0 are mapped to 1*)
+  val deterministic_seed : int -> rand
+
+  (*returns a real in the unit interval [0;1]; theoretically, with 2^31-2 equidistant discrete
+    values*)
+  val real_unit : rand -> real * rand
+
+  (*splits a seed into two new independent seeds*)
   val split : rand -> rand * rand
 end
 
-structure Random : RANDOM  =
+structure Spec_Check_Random : SPEC_CHECK_RANDOM  =
 struct
 
-type rand = real
+type rand = int
 
-val a = 16807.0
-val m = 2147483647.0
+val a = 48271
+val m = 2147483647 (* 2^31 - 1 *)
+
+fun next seed = (seed * a) mod m
 
-fun nextrand seed =
-  let
-    val t = a * seed
-  in
-    t - m * real(floor(t/m))
-  end
+(*TODO: Time is not sufficiently random when polled rapidly!*)
+fun new () =
+  Time.now ()
+  |> Time.toMicroseconds
+  |> (fn x => Int.max (1, x mod m)) (*The seed must be within [1;m)*)
+  |> next
 
-val new = nextrand o Time.toReal o Time.now
+fun deterministic_seed r = Int.max (1, r mod m)
 
-fun range (min, max) =
-  if min > max then raise Domain (* TODO: raise its own error *)
-  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
+fun real_unit r = ((Real.fromInt (r - 1)) / (Real.fromInt (m - 2)), next r)
 
+(*TODO: In theory, the current implementation could return two seeds directly adjacent in the
+sequence of the pseudorandom number generator. Practically, however, it should be good enough.*)
 fun split r =
   let
-    val r = r / a
-    val r0 = real(floor r)
+    val r0 = next r
     val r1 = r - r0
-  in
-    (nextrand r0, nextrand r1)
-  end
+  in (next r0, next r1) end
 
 end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/show/Spec_Check_Show.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,15 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Show\<close>
+theory Spec_Check_Show
+imports Pure
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>Show functions (pretty-printers) for SpecCheck take a value and return a @{ML_type Pretty.T}
+representation of the value. Refer to @{file "show_base.ML"}} for some basic examples.\<close>
+
+ML_file \<open>show_types.ML\<close>
+ML_file \<open>show_base.ML\<close>
+ML_file \<open>show.ML\<close>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/show/show.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,9 @@
+(*  Title:      Tools/Spec_Check/show/show.ML
+    Author:     Kevin Kappelmann, TU Muenchen
+
+Structure containing all show functions.
+*)
+structure Spec_Check_Show =
+struct
+open Spec_Check_Show_Base
+end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/show/show_base.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,47 @@
+(*  Title:      Tools/Spec_Check/show/show_base.ML
+    Author:     Kevin Kappelmann
+
+Basic utility functions to create and combine show functions.
+*)
+
+signature SPEC_CHECK_SHOW_BASE =
+sig
+  include SPEC_CHECK_SHOW_TYPES
+
+  val none : 'a show
+  val char : char show
+  val string : string show
+  val int : int show
+  val real : real show
+  val bool : bool show
+  val list : 'a show -> ('a list) show
+  val option : 'a show -> ('a option) show
+
+  val zip : 'a show -> 'b show -> ('a * 'b) show
+  val zip3 : 'a show -> 'b show -> 'c show -> ('a * 'b * 'c) show
+  val zip4 : 'a show -> 'b show -> 'c show -> 'd show -> ('a * 'b * 'c * 'd) show
+
+end
+
+structure Spec_Check_Show_Base : SPEC_CHECK_SHOW_BASE =
+struct
+
+open Spec_Check_Show_Types
+
+fun none _ = Pretty.str "<NO_SHOW>"
+val char = Pretty.enclose "'" "'" o single o Pretty.str o Char.toString
+val string = Pretty.quote o Pretty.str
+val int = Pretty.str o string_of_int
+val real = Pretty.str o string_of_real
+fun bool b = Pretty.str (if b then "true" else "false")
+fun list show = Pretty.list "[" "]" o map show
+fun option _ NONE = Pretty.str "NONE"
+  | option show (SOME v) = Pretty.block [Pretty.str "SOME ", show v]
+
+fun pretty_tuple ps = ps |> Pretty.commas |> Pretty.enclose "(" ")"
+
+fun zip showA showB (a, b) = pretty_tuple [showA a, showB b]
+fun zip3 showA showB showC (a, b, c) = pretty_tuple [showA a, showB b, showC c]
+fun zip4 showA showB showC showD (a, b, c, d) = pretty_tuple [showA a, showB b, showC c, showD d]
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/show/show_types.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Tools/Spec_Check/show/show_types.ML
+    Author:     Kevin Kappelmann
+
+Shared type definitions for SpecCheck showable types.
+*)
+
+signature SPEC_CHECK_SHOW_TYPES =
+sig
+  type 'a show = 'a -> Pretty.T
+end
+
+structure Spec_Check_Show_Types : SPEC_CHECK_SHOW_TYPES =
+struct
+
+type 'a show = 'a -> Pretty.T
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/shrink/Spec_Check_Shrink.thy	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,15 @@
+\<^marker>\<open>creator "Kevin Kappelmann"\<close>
+section \<open>Shrinkers\<close>
+theory Spec_Check_Shrink
+imports Spec_Check_Generators
+begin
+
+paragraph \<open>Summary\<close>
+text \<open>Shrinkers for SpecCheck take a value and return a sequqence of smaller values derived from it.
+Refer to @{file "shrink_base.ML"}} for some basic examples.\<close>
+
+ML_file \<open>shrink_types.ML\<close>
+ML_file \<open>shrink_base.ML\<close>
+ML_file \<open>shrink.ML\<close>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/shrink/shrink.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,11 @@
+(*  Title:      Tools/Spec_Check/shrink/shrink.ML
+    Author:     Kevin Kappelmann, TU Muenchen
+
+Structure containing all shrink functions.
+*)
+structure Spec_Check_Shrink =
+struct
+
+open Spec_Check_Shrink_Base
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/shrink/shrink_base.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,89 @@
+(*  Title:      Tools/Spec_Check/shrink/shrink_base.ML
+    Author:     Kevin Kappelmann
+
+Basic utility functions to create and combine shrink functions.
+*)
+
+signature SPEC_CHECK_SHRINK_BASE =
+sig
+  include SPEC_CHECK_SHRINK_TYPES
+
+  val none : 'a shrink
+
+  val product : 'a shrink -> 'b shrink -> ('a * 'b) shrink
+  val product3 : 'a shrink -> 'b shrink -> 'c shrink -> ('a * 'b * 'c) shrink
+  val product4 : 'a shrink -> 'b shrink -> 'c shrink -> 'd shrink -> ('a * 'b * 'c * 'd) shrink
+
+  val int : int shrink
+
+  val list : 'a shrink -> ('a list shrink)
+  val list' : ('a list) shrink
+
+  val term : term shrink
+
+end
+
+structure Spec_Check_Shrink_Base : SPEC_CHECK_SHRINK_BASE =
+struct
+open Spec_Check_Shrink_Types
+
+fun none _ = Seq.empty
+
+fun product_seq xq yq (x, y) =
+  let
+    val yqy = Seq.append yq (Seq.single y)
+    val zq1 = Seq.maps (fn x => Seq.map (pair x) yqy) xq
+    val zq2 = Seq.map (pair x) yq
+  in Seq.append zq1 zq2 end
+
+fun product shrinkA shrinkB (a, b) = product_seq (shrinkA a) (shrinkB b) (a, b)
+
+fun product3 shrinkA shrinkB shrinkC (a, b, c) =
+  product shrinkA shrinkB (a, b)
+  |> (fn abq => product_seq abq (shrinkC c) ((a,b),c))
+  |> Seq.map (fn ((a,b),c) => (a,b,c))
+
+fun product4 shrinkA shrinkB shrinkC shrinkD (a, b, c, d) =
+  product3 shrinkA shrinkB shrinkC (a, b, c)
+  |> (fn abcq => product_seq abcq (shrinkD d) ((a,b,c),d))
+  |> Seq.map (fn ((a,b,c),d) => (a,b,c,d))
+
+(*bit-shift right until it hits zero (some special care needs to be taken for negative numbers*)
+fun int 0 = Seq.empty
+  | int i =
+    let
+      val absi = abs i
+      val signi = Int.sign i
+      fun seq 0w0 () = NONE
+        | seq w () =
+          let
+            val next_value = signi * IntInf.~>> (absi, w)
+            val next_word = Word.- (w, 0w1)
+          in SOME (next_value, Seq.make (seq next_word)) end
+      val w = Word.fromInt (IntInf.log2 (abs i))
+    in Seq.cons 0 (Seq.make (seq w)) end
+
+fun list _ [] = Seq.single []
+  | list elem_shrink [x] = Seq.cons [] (Seq.map single (elem_shrink x))
+  | list elem_shrink (x::xs) =
+    let
+      val elems = Seq.append (elem_shrink x) (Seq.single x)
+      val seq = Seq.maps (fn xs => Seq.map (fn x => x :: xs) elems) (list elem_shrink xs)
+    in Seq.cons [] seq end
+
+fun list' xs = list none xs
+
+fun term (t1 $ t2) =
+    let
+      val s1 = Seq.append (term t1) (Seq.single t1)
+      val s2 = Seq.append (term t2) (Seq.single t2)
+      val s3 = Seq.map (op$) (product term term (t1, t2))
+    in Seq.append s1 (Seq.append s2 s3) end
+  | term (Abs (x, T, t)) =
+      let
+        val s1 = Seq.append (term t) (Seq.single t)
+        val s2 = Seq.map (fn t => Abs (x, T, t)) (term t)
+      in Seq.append s1 s2 end
+  | term _ = Seq.empty
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/shrink/shrink_types.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,17 @@
+(*  Title:      Tools/Spec_Check/shrink/shrink_types.ML
+    Author:     Kevin Kappelmann
+
+Shared type definitions for SpecCheck shrinkable types.
+*)
+
+signature SPEC_CHECK_SHRINK_TYPES =
+sig
+  type 'a shrink = 'a -> 'a Seq.seq
+end
+
+structure Spec_Check_Shrink_Types : SPEC_CHECK_SHRINK_TYPES =
+struct
+
+type 'a shrink = 'a -> 'a Seq.seq
+
+end
--- a/src/Tools/Spec_Check/spec_check.ML	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -1,196 +1,205 @@
 (*  Title:      Tools/Spec_Check/spec_check.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
+    Author:     Lukas Bulwahn, Nicolai Schaffroth, and Kevin Kappelmann TU Muenchen
     Author:     Christopher League
 
-Specification-based testing of ML programs with random values.
+Specification-based testing of ML programs.
 *)
 
 signature SPEC_CHECK =
 sig
-  val gen_target : int Config.T
-  val gen_max : int Config.T
-  val examples : int Config.T
-  val sort_examples : bool Config.T
-  val show_stats : bool Config.T
-  val column_width : int Config.T
-  val style : string Config.T
+
+  (*tries to shrink a given (failing) input to a smaller, failing input*)
+  val try_shrink : 'a Spec_Check_Property.prop -> 'a Spec_Check_Shrink.shrink -> 'a -> int ->
+    Spec_Check_Base.stats -> ('a * Spec_Check_Base.stats)
+
+  (*runs a property for a given test case and returns the result and the updated the statistics*)
+  val run_a_test : 'a Spec_Check_Property.prop -> 'a -> Spec_Check_Base.stats ->
+    Spec_Check_Base.result_single * Spec_Check_Base.stats
 
-  type output_style = Proof.context -> string ->
-    {status : string option * Property.result * (Property.stats  * string option list) -> unit,
-     finish: Property.stats * string option list -> unit}
-
-  val register_style : string -> output_style -> theory -> theory
+  (*returns the new state after executing the test*)
+  val check_style : 'a Spec_Check_Output_Style_Types.output_style ->
+    ('a Spec_Check_Show.show) option ->  'a Spec_Check_Shrink.shrink ->
+    ('a, 's) Spec_Check_Generator.gen_state -> string -> 'a Spec_Check_Property.prop ->
+    Proof.context -> 's -> 's
+  val check_shrink : 'a Spec_Check_Show.show -> 'a Spec_Check_Shrink.shrink ->
+    ('a, 's) Spec_Check_Generator.gen_state -> string -> 'a Spec_Check_Property.prop ->
+    Proof.context -> 's -> 's
+  val check : 'a Spec_Check_Show.show -> ('a, 's) Spec_Check_Generator.gen_state -> string ->
+    'a Spec_Check_Property.prop -> Proof.context -> 's -> 's
+  val check_base : ('a, 's) Spec_Check_Generator.gen_state -> string ->
+    'a Spec_Check_Property.prop -> Proof.context -> 's -> 's
 
-  val checkGen : Proof.context ->
-    'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
+  (*returns all unprocessed elements of the sequence*)
+  val check_seq_style : 'a Spec_Check_Output_Style_Types.output_style ->
+    ('a Spec_Check_Show.show) option -> 'a Seq.seq -> string -> 'a Spec_Check_Property.prop ->
+    Proof.context -> 'a Seq.seq
+  val check_seq : 'a Spec_Check_Show.show -> 'a Seq.seq -> string -> 'a Spec_Check_Property.prop ->
+    Proof.context -> 'a Seq.seq
+  val check_seq_base : 'a Seq.seq -> string -> 'a Spec_Check_Property.prop -> Proof.context ->
+    'a Seq.seq
 
-  val check_property : Proof.context -> string -> unit
-end;
+  (*returns all unused elements of the list*)
+  val check_list_style : 'a Spec_Check_Output_Style_Types.output_style ->
+    ('a Spec_Check_Show.show) option -> 'a list -> string -> 'a Spec_Check_Property.prop ->
+    Proof.context -> 'a Seq.seq
+  val check_list : 'a Spec_Check_Show.show -> 'a list -> string -> 'a Spec_Check_Property.prop ->
+    Proof.context -> 'a Seq.seq
+  val check_list_base : 'a list -> string -> 'a Spec_Check_Property.prop -> Proof.context ->
+    'a Seq.seq
 
+end
+                                                                   
 structure Spec_Check : SPEC_CHECK =
 struct
 
-(* configurations *)
-
-val gen_target = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_target\<close> (K 100)
-val gen_max = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_max\<close> (K 400)
-val examples = Attrib.setup_config_int \<^binding>\<open>spec_check_examples\<close> (K 5)
+open Spec_Check_Base
 
-val sort_examples = Attrib.setup_config_bool \<^binding>\<open>spec_check_sort_examples\<close> (K true)
-val show_stats = Attrib.setup_config_bool \<^binding>\<open>spec_check_show_stats\<close> (K true)
-val column_width = Attrib.setup_config_int \<^binding>\<open>spec_check_column_width\<close> (K 22)
-val style = Attrib.setup_config_string \<^binding>\<open>spec_check_style\<close> (K "Perl")
-
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-type 'a rep = ('a -> string) option
-
-type output_style = Proof.context -> string ->
-  {status: string option * Property.result * (Property.stats * string option list) -> unit,
-   finish: Property.stats * string option list -> unit}
+fun run_a_test prop input {
+    num_success_tests,
+    num_failed_tests,
+    num_discarded_tests,
+    num_recently_discarded_tests,
+    num_success_shrinks,
+    num_failed_shrinks,
+    timing
+  } =
+  let
+    val (time, result) = Timing.timing (fn () => prop input) ()
+    val is_success = case result of Result is_success => is_success | _ => false
+    val is_discard = case result of Discard => true | _ => false
+    val is_failure = not is_discard andalso not is_success
 
-fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
-
-structure Style = Theory_Data
-(
-  type T = output_style Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge data : T = Symtab.merge (K true) data
-)
+    val num_success_tests = num_success_tests + (if is_success then 1 else 0)
+    val num_failed_tests = num_failed_tests + (if is_failure then 1 else 0)
+    val num_discarded_tests = num_discarded_tests + (if is_discard then 1 else 0)
+    val num_recently_discarded_tests = if is_discard then num_recently_discarded_tests + 1 else 0
+    val timing = add_timing timing time
 
-fun get_style ctxt =
-  let val name = Config.get ctxt style in
-    (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
-      SOME style => style ctxt
-    | NONE => error ("No style called " ^ quote name ^ " found"))
-  end
-
-fun register_style name style = Style.map (Symtab.update (name, style))
-
+    val stats = {
+      num_success_tests = num_success_tests,
+      num_failed_tests = num_failed_tests,
+      num_discarded_tests = num_discarded_tests,
+      num_recently_discarded_tests = num_recently_discarded_tests,
+      num_success_shrinks = num_success_shrinks,
+      num_failed_shrinks = num_failed_shrinks,
+      timing = timing
+    }
+  in (result, stats) end
 
-(* testing functions *)
-
-fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
-  let
-    val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
+fun add_num_success_shrinks stats n = {
+  num_success_tests = #num_success_tests stats,
+  num_failed_tests = #num_failed_tests stats,
+  num_discarded_tests = #num_discarded_tests stats,
+  num_recently_discarded_tests = #num_recently_discarded_tests stats,
+  num_success_shrinks = #num_success_shrinks stats + n,
+  num_failed_shrinks = #num_failed_shrinks stats,
+  timing = #timing stats
+}
 
-    val {status, finish} = get_style ctxt tag
-    fun status' (obj, result, (stats, badobjs)) =
-      let
-        val badobjs' = if Property.failure result then obj :: badobjs else badobjs
-        val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
-      in badobjs' end
+fun add_num_failed_shrinks stats n = {
+  num_success_tests = #num_success_tests stats,
+  num_failed_tests = #num_failed_tests stats,
+  num_discarded_tests = #num_discarded_tests stats,
+  num_recently_discarded_tests = #num_recently_discarded_tests stats,
+  num_success_shrinks = #num_success_shrinks stats,
+  num_failed_shrinks = #num_failed_shrinks stats + n,
+  timing = #timing stats
+}
 
-    fun try_shrink (obj, result, stats') (stats, badobjs) =
-      let
-        fun is_failure s =
-          let val (result, stats') = Property.test prop (s, stats)
-          in if Property.failure result then SOME (s, result, stats') else NONE end
-      in
-        case get_first is_failure (shrink obj) of
-          SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
-        | NONE => status' (obj, result, (stats', badobjs))
-      end
-
-    fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
-      | iter (SOME (obj, stream), (stats, badobjs)) =
-        if #count stats >= Config.get ctxt gen_target then
-          finish (stats, map apply_show badobjs)
-        else
-          let
-            val (result, stats') = Property.test prop (obj, stats)
-            val badobjs' = if Property.failure result then
-                try_shrink (obj, result, stats') (stats, badobjs)
-              else
-                status' (obj, result, (stats', badobjs))
-          in iter (next stream, (stats', badobjs')) end
+fun try_shrink prop shrink input max_shrinks stats =
+  let
+    fun is_failure input = case run_a_test prop input empty_stats |> fst of
+        Result is_success => not is_success
+      | Discard => false
+      | Exception _ => false (*do not count exceptions as a failure because the shrinker might
+                               just have broken some invariant of the function*)
+    fun find_first_failure xq pulls_left stats =
+      if pulls_left <= 0
+      then (NONE, pulls_left, stats)
+      else
+        case Seq.pull xq of
+          NONE => (NONE, pulls_left, stats)
+        | SOME (x, xq) =>
+          if is_failure x
+          then (SOME x, pulls_left - 1, add_num_success_shrinks stats 1)
+          else find_first_failure xq (pulls_left - 1) (add_num_failed_shrinks stats 1)
   in
-    fn stream => iter (next stream, (s0, []))
+    (*always try the first successful branch and abort without backtracking once no further
+      shrink is possible.*)
+    case find_first_failure (shrink input) max_shrinks stats of
+      (*recursively shrink*)
+      (SOME input, shrinks_left, stats) => try_shrink prop shrink input shrinks_left stats
+    | (NONE, _, stats) => (input, stats)
   end
 
-fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
-fun check ctxt = check' ctxt Property.stats
-fun checks ctxt = cpsCheck ctxt Property.stats
-
-fun checkGen ctxt (gen, show) (tag, prop) =
-  check' ctxt {count = 0, tags = [("__GEN", 0)]}
-    (limit ctxt gen, show) (tag, prop) Generator.stream
-
-fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
-  cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
-    (limit ctxt gen, show) (tag, prop) Generator.stream
-
-fun checkOne ctxt show (tag, prop) obj =
-  check ctxt (List.getItem, show) (tag, prop) [obj]
-
-(*call the compiler and pass resulting type string to the parser*)
-fun determine_type ctxt s =
+fun test output_style init_stats show_opt shrink opt_gen name prop ctxt state =
   let
-    val return = Unsynchronized.ref "return"
-    val context : ML_Compiler0.context =
-     {name_space = #name_space ML_Env.context,
-      print_depth = SOME 1000000,
-      here = #here ML_Env.context,
-      print = fn r => return := r,
-      error = #error ML_Env.context}
-    val _ =
-      Context.setmp_generic_context (SOME (Context.Proof ctxt))
-        (fn () =>
-          ML_Compiler0.ML context
-            {line = 0, file = "generated code", verbose = true, debug = false} s) ()
-  in
-    Gen_Construction.parse_pred (! return)
-  end;
-
-(*call the compiler and run the test*)
-fun run_test ctxt s =
-  Context.setmp_generic_context (SOME (Context.Proof ctxt))
-    (fn () =>
-      ML_Compiler0.ML ML_Env.context
-        {line = 0, file = "generated code", verbose = false, debug = false} s) ();
+    val max_discard_ratio = Config.get ctxt Spec_Check_Configuration.max_discard_ratio
+    val max_success = Config.get ctxt Spec_Check_Configuration.max_success
+    (*number of counterexamples to generate before stopping the test*)
+    val num_counterexamples =
+      let val conf_num_counterexamples =
+        Config.get ctxt Spec_Check_Configuration.num_counterexamples
+      in if conf_num_counterexamples > 0 then conf_num_counterexamples else ~1 end
+    val max_shrinks = Config.get ctxt Spec_Check_Configuration.max_shrinks
 
-(*split input into tokens*)
-fun input_split s =
-  let
-    fun dot c = c = #"."
-    fun space c = c = #" "
-    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
+    fun run_tests opt_gen state stats counterexamples =
+      (*stop the test run if enough (successful) tests were run or counterexamples were found*)
+      if #num_success_tests stats >= max_success then (Success stats, state)
+      else if num_tests stats >= max_success orelse
+              #num_failed_tests stats = num_counterexamples
+      then (Failure (stats, failure_data counterexamples), state)
+      else (*test input and attempt to shrink on failure*)
+        let val (input_opt, state) = opt_gen state
+        in
+          case input_opt of
+            NONE =>
+              if #num_failed_tests stats > 0
+              then (Failure (stats, failure_data counterexamples), state)
+              else (Success stats, state)
+          | SOME input =>
+            let val (result, stats) = run_a_test prop input stats
+            in
+              case result of
+                Result true => run_tests opt_gen state stats counterexamples
+              | Result false =>
+                  let val (counterexample, stats) = try_shrink prop shrink input max_shrinks stats
+                  in run_tests opt_gen state stats (counterexample :: counterexamples) end
+              | Discard =>
+                  if #num_recently_discarded_tests stats > max_discard_ratio
+                  then
+                    if #num_failed_tests stats > 0
+                    then (Failure (stats, failure_data counterexamples), state)
+                    else (Gave_Up stats, state)
+                  else run_tests opt_gen state stats counterexamples
+              | Exception exn =>
+                  (Failure (stats, failure_data_exn (input :: counterexamples) exn), state)
+            end
+        end
   in
-   (String.tokens space (Substring.string head),
-    Substring.string (Substring.dropl dot code))
-  end;
-
-(*create the function from the input*)
-fun make_fun s =
-  let
-    val scan_param = Scan.one (fn s => s <> ";")
-    fun parameters s = Scan.repeat1 scan_param s
-    val p = $$ "ALL" |-- parameters
-    val (split, code) = input_split s
-    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
-    val (params, _) = Scan.finite stop p split
-  in "fn (" ^ commas params ^ ") => " ^ code end;
+    Timing.timing (fn _ => run_tests opt_gen state init_stats []) ()
+    |> uncurry (apfst o output_style show_opt ctxt name)
+    |> snd
+  end
 
-(*read input and perform the test*)
-fun gen_check_property check ctxt s =
-  let
-    val func = make_fun s
-    val (_, ty) = determine_type ctxt func
-  in run_test ctxt (check ctxt "Check" (ty, func)) end;
+fun check_style style show_opt shrink =
+  test style empty_stats show_opt shrink o Spec_Check_Generator.map SOME
 
-val check_property = gen_check_property Gen_Construction.build_check
-(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
+fun check_shrink show = check_style Spec_Check_Default_Output_Style.default (SOME show)
+fun check show = check_shrink show Spec_Check_Shrink.none
+
+fun check_base gen =
+  check_style Spec_Check_Default_Output_Style.default NONE Spec_Check_Shrink.none gen
 
-(*perform test for specification function*)
-fun gen_check_property_f check ctxt s =
-  let
-    val (name, ty) = determine_type ctxt s
-  in run_test ctxt (check ctxt name (ty, s)) end;
+fun check_seq_style style show_opt xq name prop ctxt =
+  test style empty_stats show_opt Spec_Check_Shrink.none Spec_Check_Generator.of_seq name prop ctxt
+    xq
 
-val check_property_f = gen_check_property_f Gen_Construction.build_check
-(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
+fun check_seq show = check_seq_style Spec_Check_Default_Output_Style.default (SOME show)
+fun check_seq_base xq = check_seq_style Spec_Check_Default_Output_Style.default NONE xq
 
-end;
+fun check_list_style style show = check_seq_style style show o Seq.of_list
+fun check_list show = check_seq show o Seq.of_list
+fun check_list_base xs = check_seq_base (Seq.of_list xs)
 
-fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;
-
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/spec_check_base.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,111 @@
+(*  Title:      Tools/Spec_Check/spec_check_base.ML
+    Author:     Kevin Kappelmann
+
+Types returned by single tests and complete test runs as well as simple utility methods on them.
+*)
+
+signature SPEC_CHECK_BASE =
+sig
+
+  datatype result_single = Result of bool | Discard | Exception of exn
+
+  type stats = {
+    num_success_tests : int,
+    num_failed_tests : int,
+    num_discarded_tests : int,
+    num_recently_discarded_tests : int,
+    num_success_shrinks : int,
+    num_failed_shrinks : int,
+    timing : Timing.timing
+  }
+
+  val add_timing : Timing.timing -> Timing.timing -> Timing.timing
+
+  val empty_stats : stats
+  val num_tests : stats -> int
+  val num_shrinks : stats -> int
+
+  type 'a failure_data = {
+    counterexamples : 'a list,
+    the_exception : exn option
+  }
+
+  val failure_data : 'a list -> 'a failure_data
+  val failure_data_exn : 'a list -> exn -> 'a failure_data
+
+  datatype 'a result =
+    Success of stats |
+    Gave_Up of stats |
+    Failure of stats * 'a failure_data
+
+  val stats_of_result : 'a result -> stats
+
+end
+
+structure Spec_Check_Base : SPEC_CHECK_BASE =
+struct
+
+datatype result_single = Result of bool | Discard | Exception of exn
+
+type stats = {
+  num_success_tests : int,
+  num_failed_tests : int,
+  num_discarded_tests : int,
+  num_recently_discarded_tests : int,
+  num_success_shrinks : int,
+  num_failed_shrinks : int,
+  timing : Timing.timing
+}
+
+val empty_stats = {
+  num_success_tests = 0,
+  num_failed_tests = 0,
+  num_discarded_tests = 0,
+  num_recently_discarded_tests = 0,
+  num_success_shrinks = 0,
+  num_failed_shrinks = 0,
+  timing = {
+    cpu = Time.zeroTime,
+    elapsed = Time.zeroTime,
+    gc = Time.zeroTime
+  }
+}
+
+fun add_timing {elapsed = elapsed1, cpu = cpu1, gc = gc1}
+  {elapsed = elapsed2, cpu = cpu2, gc = gc2} = {
+  elapsed = elapsed1 + elapsed2,
+  cpu = cpu1 + cpu2,
+  gc = gc1 + gc2
+}
+
+fun num_tests {num_success_tests, num_failed_tests, ...} =
+  num_success_tests + num_failed_tests
+
+fun num_shrinks {num_success_shrinks, num_failed_shrinks, ...} =
+  num_success_shrinks + num_failed_shrinks
+
+type 'a failure_data = {
+  counterexamples : 'a list,
+  the_exception : exn option
+}
+
+fun failure_data counterexamples = {
+  counterexamples = counterexamples,
+  the_exception = NONE
+}
+
+fun failure_data_exn counterexamples exn = {
+  counterexamples = counterexamples,
+  the_exception = SOME exn
+}
+
+datatype 'a result =
+  Success of stats |
+  Gave_Up of stats |
+  Failure of stats * 'a failure_data
+
+fun stats_of_result (Success stats) = stats
+  | stats_of_result (Gave_Up stats) = stats
+  | stats_of_result (Failure (stats, _)) = stats
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Spec_Check/util.ML	Mon Jun 21 16:08:36 2021 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Tools/Spec_Check/util.ML
+    Author:     Kevin Kappelmann
+
+Some utility functions that maybe should be put somewhere else in Pure.
+*)
+
+signature SPEC_CHECK_UTIL =
+sig
+
+datatype ('a,'b) either = Left of 'a | Right of 'b
+
+val spaces : string list -> string
+
+val pwriteln : string -> unit
+val pwarning : string -> unit
+
+end
+
+structure Spec_Check_Util : SPEC_CHECK_UTIL =
+struct
+
+datatype ('a,'b) either = Left of 'a | Right of 'b
+
+val spaces = space_implode " "
+
+fun pretty_output output =
+  space_explode " "
+  #> map Pretty.str
+  #> Pretty.breaks
+  #> pair 0
+  #> Pretty.blk
+  #> output
+
+val pwriteln = pretty_output Pretty.writeln
+
+val pwarning = pretty_output (Output.warning o Pretty.string_of)
+
+end
\ No newline at end of file