✐‹creator "Kevin Kappelmann"›
section ‹SpecCheck Base›
theory SpecCheck_Base
imports Pure
begin

paragraph ‹Summary›
text ‹Basic setup for SpecCheck.›

ML_file ‹util.ML›

ML_file ‹speccheck_base.ML›
ML_file ‹property.ML›
ML_file ‹configuration.ML›

ML_file ‹random.ML›

end

(*  Title:      SpecCheck/util.ML
    Author:     Kevin Kappelmann

General utility functions for SpecCheck.
*)

signature SPECCHECK_UTIL =
sig

val spaces : string list -> string

end

structure SpecCheck_Util : SPECCHECK_UTIL =
struct

val spaces = space_implode " "

end

(*  Title:      SpecCheck/speccheck_base.ML
    Author:     Kevin Kappelmann

Types returned by single tests and complete test runs as well as simple utility methods on them.
*)

signature SPECCHECK_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 SpecCheck_Base : SPECCHECK_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

(*  Title:      SpecCheck/property.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

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 SPECCHECK_PROPERTY =
sig

  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 SpecCheck_Property : SPECCHECK_PROPERTY =
struct

type 'a pred = 'a -> bool
type 'a prop = 'a -> SpecCheck_Base.result_single

fun apply f x = SpecCheck_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 SpecCheck_Base.Exception exn

fun prop f x = apply f x

fun implies cond prop x =
  if cond x
  then prop x
  else SpecCheck_Base.Discard

fun ==> (p1, p2) = implies p1 (prop p2)

end

(*  Title:      SpecCheck/configuration.ML
    Author:     Kevin Kappelmann

Configuration options for SpecCheck.
*)

signature SPECCHECK_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 SpecCheck_Configuration : SPECCHECK_CONFIGURATION =
struct

val max_success = Attrib.setup_config_int \<^binding>‹speccheck_max_success› (K 100)

val max_discard_ratio = Attrib.setup_config_int \<^binding>‹speccheck_max_discard_ratio› (K 10)

val max_shrinks = Attrib.setup_config_int \<^binding>‹speccheck_max_shrinks› (K 10000)

val num_counterexamples = Attrib.setup_config_int \<^binding>‹speccheck_num_counterexamples› (K 1)

val sort_counterexamples =
  Attrib.setup_config_bool \<^binding>‹speccheck_sort_counterexamples› (K true)

val show_stats = Attrib.setup_config_bool \<^binding>‹speccheck_show_stats› (K true)

end

(*  Title:      SpecCheck/random.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

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 SPECCHECK_RANDOM =
sig
  type rand
  (*creates a new random seed*)
  val new : unit -> rand
  (*creates a new random seed from a given one*)
  val next : rand -> rand
  (*use this function for reproducible randomness; inputs ≤ 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 SpecCheck_Random : SPECCHECK_RANDOM  =
struct

type rand = int

val a = 48271
val m = 2147483647 (* 2^31 - 1 *)

fun next seed = (seed * a) mod m

(*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

fun deterministic_seed r = Int.max (1, r mod m)

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 r0 = next r
    val r1 = r - r0
  in (next r0, next r1) end

end

✐‹creator "Kevin Kappelmann"›
section ‹Generators›
theory SpecCheck_Generators
imports SpecCheck_Base
begin

paragraph ‹Summary›
text ‹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.›

ML_file ‹gen_types.ML›
ML_file ‹gen_base.ML›
ML_file ‹gen_text.ML›
ML_file ‹gen_int.ML›
ML_file ‹gen_real.ML›
ML_file ‹gen_function.ML›
ML_file ‹gen_term.ML›
ML_file ‹gen.ML›

end

(*  Title:      SpecCheck/generators/gen_types.ML
    Author:     Kevin Kappelmann

Shared type definitions for SpecCheck generators.
*)

signature SPECCHECK_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, SpecCheck_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, SpecCheck_Random.rand) cogen_state

end

structure SpecCheck_Gen_Types : SPECCHECK_GEN_TYPES =
struct

type ('a, 's) gen_state = 's -> 'a * 's

type 'a gen = ('a, SpecCheck_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, SpecCheck_Random.rand) cogen_state

end

(*  Title:      SpecCheck/generators/gen_base.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Basic utility functions to create and combine generators.
*)

signature SPECCHECK_GEN_BASE =
sig
  include SPECCHECK_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 ∈ [0,1]*)
  val bernoulli : real -> bool gen

  (*random variable following a binomial distribution with parameters p ∈ [0,1] and n ≥ 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 * SpecCheck_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 SpecCheck_Gen_Base : SPECCHECK_GEN_BASE =
struct

open SpecCheck_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) = SpecCheck_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 (SpecCheck_Util.spaces ["Range_Int:", string_of_int min, ">", string_of_int max])
  else
    SpecCheck_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

local
datatype ('a,'b) either = Left of 'a | Right of 'b
in
fun one_ofW (v : (int * 'a gen) vector) r =
  let
    val weight_total = Vector.foldl (fn ((freq,_),acc) => freq + acc) 0 v
    fun selectGen _ (_, Right gen) = Right gen
      | selectGen rand ((weight, gen), Left acc) =
      let val acc = acc + weight
      in if acc < rand
         then Left acc
         else Right gen
      end
    val (threshhold, r) = range_int (1, weight_total) r
    val gen = case Vector.foldl (selectGen threshhold) (Left 0) v of
        Right gen => gen
      | _ => raise Fail "Error in one_ofW - did you pass an empty vector or invalid frequencies?"
  in gen r end
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)) SpecCheck_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) = SpecCheck_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) = SpecCheck_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

(*  Title:      SpecCheck/generators/gen_text.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Random generators for chars and strings.
*)

signature SPECCHECK_GEN_TEXT = sig

  val range_char : char * char -> char SpecCheck_Gen_Types.gen
  val char : char SpecCheck_Gen_Types.gen

  val char_of : string -> char SpecCheck_Gen_Types.gen

  val string : int SpecCheck_Gen_Types.gen -> char SpecCheck_Gen_Types.gen ->
    string SpecCheck_Gen_Types.gen

  val substring : string SpecCheck_Gen_Types.gen -> substring SpecCheck_Gen_Types.gen

  val cochar : (char, 'b) SpecCheck_Gen_Types.cogen
  val costring : (string, 'b) SpecCheck_Gen_Types.cogen
  val cosubstring : (substring, 'b) SpecCheck_Gen_Types.cogen

  val digit : char SpecCheck_Gen_Types.gen
  val lowercase_letter : char SpecCheck_Gen_Types.gen
  val uppercase_letter : char SpecCheck_Gen_Types.gen
  val letter : char SpecCheck_Gen_Types.gen
end

structure SpecCheck_Gen_Text : SPECCHECK_GEN_TEXT =
struct

open SpecCheck_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

(*  Title:      SpecCheck/generators/gen_int.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Random generators for ints.
*)

signature SPECCHECK_GEN_INT = sig

  (*pos m generates an integer in [1, m]*)
  val pos : int -> int SpecCheck_Gen_Types.gen
  (*neg m generates an integer in [m, 1]*)
  val neg : int -> int SpecCheck_Gen_Types.gen
  (*nonneg m generates an integer in [0, m]*)
  val nonneg : int -> int SpecCheck_Gen_Types.gen
  (*nonpos m generates an integer in [m, 0]*)
  val nonpos : int -> int SpecCheck_Gen_Types.gen

  val coint : (int, 'b) SpecCheck_Gen_Types.cogen

end

structure SpecCheck_Gen_Int : SPECCHECK_GEN_INT =
struct

open SpecCheck_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

(*  Title:      SpecCheck/generators/gen_real.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Random generators for reals.
*)

signature SPECCHECK_GEN_REAL = sig

  (*range_real (x,y) r returns a value in [x, y]*)
  val range_real : real * real -> real SpecCheck_Gen_Types.gen

  val real : real SpecCheck_Gen_Types.gen

  val real_pos : real SpecCheck_Gen_Types.gen
  val real_neg : real SpecCheck_Gen_Types.gen

  val real_nonneg : real SpecCheck_Gen_Types.gen
  val real_nonpos : real SpecCheck_Gen_Types.gen

  val real_finite : real SpecCheck_Gen_Types.gen
end

structure SpecCheck_Gen_Real : SPECCHECK_GEN_REAL =
struct

open SpecCheck_Gen_Base
open SpecCheck_Gen_Text

fun range_real (min, max) r =
  if min > max
  then
    raise Fail (SpecCheck_Util.spaces ["Range_Real:", string_of_real min, ">", string_of_real max])
  else SpecCheck_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

(*  Title:      SpecCheck/generators/gen_function.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Random generators for functions.
*)

signature SPECCHECK_GEN_FUNCTION = sig
  val function : ('a, 'b) SpecCheck_Gen_Types.cogen -> 'b SpecCheck_Gen_Types.gen ->
    ('a -> 'b) SpecCheck_Gen_Types.gen
  val function' : 'b SpecCheck_Gen_Types.gen -> (''a -> 'b) SpecCheck_Gen_Types.gen
end

structure SpecCheck_Gen_Function : SPECCHECK_GEN_FUNCTION =
struct

fun function cogen gen r =
  let
    val (r1, r2) = SpecCheck_Random.split r
    fun g x = fst (cogen x gen r1)
  in (g, r2) end

fun function' gen r =
  let
    val (internal, external) = SpecCheck_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

(*  Title:      SpecCheck/generators/gen_term.ML
    Author:     Sebastian Willenbrink and Kevin Kappelmann TU Muenchen

Generators for terms and types.
*)
signature SPECCHECK_GEN_TERM = sig
  (* sort generators *)

  (*first parameter determines the number of classes to pick*)
  val sort : (int, 's) SpecCheck_Gen_Types.gen_state -> (class, 's) SpecCheck_Gen_Types.gen_state
    -> (sort, 's) SpecCheck_Gen_Types.gen_state
  val dummyS : (sort, 's) SpecCheck_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 SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen

  val indexname : (string, 's) SpecCheck_Gen_Types.gen_state ->
    (int, 's) SpecCheck_Gen_Types.gen_state -> (indexname, 's) SpecCheck_Gen_Types.gen_state

  (*a variant with base name "k"*)
  val type_name : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen

  (*creates a free type variable name from a passed basic name generator*)
  val tfree_name : (string, 's) SpecCheck_Gen_Types.gen_state ->
    (string, 's) SpecCheck_Gen_Types.gen_state
  (*chooses a variant with base name "'a"*)
  val tfree_name' : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen

  (*creates a type variable name from a passed basic name (e.g. "a") generator*)
  val tvar_name : (indexname, 's) SpecCheck_Gen_Types.gen_state ->
    (indexname, 's) SpecCheck_Gen_Types.gen_state
  (*chooses a variant with base name "'a"*)
  val tvar_name' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    indexname SpecCheck_Gen_Types.gen

  (*chooses a variant with base name "c"*)
  val const_name : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen
  (*chooses a variant with base name "f"*)
  val free_name : int SpecCheck_Gen_Types.gen -> string SpecCheck_Gen_Types.gen
  (*chooses a variant with base name "v*)
  val var_name : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    indexname SpecCheck_Gen_Types.gen

  (* typ  generators *)

  val tfree : (string, 's) SpecCheck_Gen_Types.gen_state ->
    (sort, 's) SpecCheck_Gen_Types.gen_state -> (typ, 's) SpecCheck_Gen_Types.gen_state
  (*uses tfree_name' and dummyS to create a free type variable*)
  val tfree' : int SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen

  val tvar : (indexname, 's) SpecCheck_Gen_Types.gen_state ->
    (sort, 's) SpecCheck_Gen_Types.gen_state -> (typ, 's) SpecCheck_Gen_Types.gen_state
  (*uses tvar' and dummyS to create a type variable*)
  val tvar' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    typ SpecCheck_Gen_Types.gen

  (*atyp tfree_gen tvar_gen (weight_tfree, weight_tvar)*)
  val atyp : typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> (int * int) ->
    typ SpecCheck_Gen_Types.gen
  (*uses tfree' and tvar' to create an atomic type*)
  val atyp' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen -> (int * int) ->
    typ SpecCheck_Gen_Types.gen

  (*type' type_name_gen arity_gen tfree_gen tvar_gen (weight_type, weight_tfree, weight_tvar)*)
  val type' : string SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen ->
    (int * int * int) -> typ SpecCheck_Gen_Types.gen
  (*uses type_name to generate a type*)
  val type'' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> (int * int * int) ->
    typ SpecCheck_Gen_Types.gen

  (*typ type_gen tfree_gen tvar_gen (wtype, wtfree, wtvar)*)
  val typ : typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen ->
    typ SpecCheck_Gen_Types.gen -> (int * int * int) -> typ SpecCheck_Gen_Types.gen
  (*uses type'' for its type generator*)
  val typ' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    typ SpecCheck_Gen_Types.gen -> typ SpecCheck_Gen_Types.gen -> (int * int * int) ->
    typ SpecCheck_Gen_Types.gen
  (*uses typ' with tfree' and tvar' parameters*)
  val typ'' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    int SpecCheck_Gen_Types.gen -> (int * int * int) -> typ SpecCheck_Gen_Types.gen

  val dummyT : (typ, 's) SpecCheck_Gen_Types.gen_state

  (* term generators *)

  val const : (string, 's) SpecCheck_Gen_Types.gen_state ->
    (typ, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state
  (*uses const_name and dummyT to create a constant*)
  val const' : int SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen

  val free : (string, 's) SpecCheck_Gen_Types.gen_state ->
    (typ, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state
  (*uses free_name and dummyT to create a free variable*)
  val free' : int SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen

  val var : (indexname, 's) SpecCheck_Gen_Types.gen_state ->
    (typ, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state
  (*uses var_name and dummyT to create a variable*)
  val var' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    term SpecCheck_Gen_Types.gen

  val bound : (int, 's) SpecCheck_Gen_Types.gen_state -> (term, 's) SpecCheck_Gen_Types.gen_state

  (*aterm const_gen free_gen var_gen bound_gen
    (weight_const, weight_free, weight_var, weight_bound*)
  val aterm : term SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen ->
    term SpecCheck_Gen_Types.gen -> term SpecCheck_Gen_Types.gen -> (int * int * int * int) ->
    term SpecCheck_Gen_Types.gen
  (*uses const', free', and var' to create an atomic term*)
  val aterm' : int SpecCheck_Gen_Types.gen -> int SpecCheck_Gen_Types.gen ->
    (int * int * int * int) -> term SpecCheck_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 → first argument → ... → 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 ≤ 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) SpecCheck_Gen_Types.gen_state) ->
    (term, 's) SpecCheck_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) SpecCheck_Gen_Types.gen_state) ->
    (term, 's) SpecCheck_Gen_Types.gen_state

end

structure SpecCheck_Gen_Term : SPECCHECK_GEN_TERM =
struct

structure Gen = SpecCheck_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

(*  Title:      SpecCheck/generators/gen.ML
    Author:     Kevin Kappelmann, TU Muenchen

Structure containing all generators.
*)
structure SpecCheck_Generator =
struct
open SpecCheck_Gen_Types
open SpecCheck_Gen_Base
open SpecCheck_Gen_Text
open SpecCheck_Gen_Real
open SpecCheck_Gen_Int
open SpecCheck_Gen_Function
open SpecCheck_Gen_Term
end

✐‹creator "Kevin Kappelmann"›
section ‹Show›
theory SpecCheck_Show
imports Pure
begin

paragraph ‹Summary›
text ‹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.›

ML_file ‹show_types.ML›
ML_file ‹show_base.ML›
ML_file ‹show.ML›

end

(*  Title:      SpecCheck/show/show_types.ML
    Author:     Kevin Kappelmann

Shared type definitions for SpecCheck showable types.
*)

signature SPECCHECK_SHOW_TYPES =
sig
  type 'a show = 'a -> Pretty.T
end

structure SpecCheck_Show_Types : SPECCHECK_SHOW_TYPES =
struct

type 'a show = 'a -> Pretty.T

end

(*  Title:      SpecCheck/show/show_base.ML
    Author:     Kevin Kappelmann

Basic utility functions to create and combine show functions.
*)

signature SPECCHECK_SHOW_BASE =
sig
  include SPECCHECK_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 SpecCheck_Show_Base : SPECCHECK_SHOW_BASE =
struct

open SpecCheck_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

(*  Title:      SpecCheck/show/show.ML
    Author:     Kevin Kappelmann, TU Muenchen

Structure containing all show functions.
*)
structure SpecCheck_Show =
struct
open SpecCheck_Show_Base
end

✐‹creator "Kevin Kappelmann"›
section ‹Output Styles›
theory SpecCheck_Output_Style
imports
  SpecCheck_Base
  SpecCheck_Show
begin


paragraph ‹Summary›
text ‹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.›


ML_file ‹output_style_types.ML›
ML_file ‹output_style_perl.ML›
ML_file ‹output_style_custom.ML›
ML_file ‹output_style.ML›

end

(*  Title:      SpecCheck/output_styles/output_style_types.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Shared types for SpecCheck output styles.
*)
signature SPECCHECK_OUTPUT_STYLE_TYPES =
sig
  type 'a output_style = 'a SpecCheck_Show.show option -> Proof.context -> string ->
    Timing.timing -> 'a SpecCheck_Base.result -> unit
end

structure SpecCheck_Output_Style_Types : SPECCHECK_OUTPUT_STYLE_TYPES =
struct

type 'a output_style = 'a SpecCheck_Show.show option -> Proof.context -> string -> Timing.timing ->
  'a SpecCheck_Base.result -> unit

end

signature SPECCHECK_OUTPUT_STYLE =
sig
  val style : 'a SpecCheck_Output_Style_Types.output_style
end

(*  Title:      SpecCheck/output_styles/output_style_perl.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Perl output styles for SpecCheck.
*)

structure SpecCheck_Output_Style_Perl : SPECCHECK_OUTPUT_STYLE =
struct

open SpecCheck_Configuration
open SpecCheck_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 => (warning "Counterexamples:"; fold (fn x => fn _ => warning x) es ()))
      | NONE => ()

  in
    case result of
      Success _ => writeln result_string
    | Gave_Up _ => warning result_string
    | Failure (_, failure_data) =>
        (warning result_string; show_counterexamples (#counterexamples failure_data))
  end

end

(*  Title:      SpecCheck/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 SpecCheck_Output_Style_Custom : SPECCHECK_OUTPUT_STYLE =
struct

open SpecCheck_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 SpecCheck_Util.spaces [";", string_of_int num_discarded_tests,  "discarded."]
  in
    implode ["OK, passed ", num_success_tests, " tests", discarded_str]
    |> writeln
  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
    SpecCheck_Util.spaces ["Gave up! Passed only", num_success_tests, "test(s);", num_discarded_tests,
      "discarded test(s)."]
    |> warning
  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]
      |> warning
  | NONE => case show_opt of
      NONE => ()
    | SOME show =>
      let
        val sort_counterexamples = Config.get ctxt SpecCheck_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 _ => warning x) counterexamples () end

fun print_failure ctxt show_opt (stats, failure_data) =
  ((SpecCheck_Util.spaces ["Failed! Falsified (after", string_of_int (num_tests stats), "test(s) and ",
    string_of_int (num_shrinks stats), "shrink(s)):"] |> warning);
  print_failure_data ctxt show_opt failure_data)

fun print_stats ctxt stats total_time =
  let
    val show_stats = Config.get ctxt SpecCheck_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 writeln (show_time (#timing stats))
  end

fun style show_opt ctxt name total_time result =
  let val stats = stats_of_result result
  in
    writeln (SpecCheck_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

(*  Title:      SpecCheck/output_styles/output_style.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Output styles for presenting SpecCheck results.
*)

signature SPECCHECK_DEFAULT_OUTPUT_STYLE =
sig
  include SPECCHECK_OUTPUT_STYLE_TYPES
  val default : 'a output_style
end

structure SpecCheck_Default_Output_Style : SPECCHECK_DEFAULT_OUTPUT_STYLE =
struct

open SpecCheck_Output_Style_Types
val default = SpecCheck_Output_Style_Custom.style

end

✐‹creator "Kevin Kappelmann"›
section ‹Shrinkers›
theory SpecCheck_Shrink
imports SpecCheck_Generators
begin

paragraph ‹Summary›
text ‹Shrinkers for SpecCheck take a value and return a sequence of smaller values derived from it.
Refer to @{file "shrink_base.ML"} for some basic examples.›

ML_file ‹shrink_types.ML›
ML_file ‹shrink_base.ML›
ML_file ‹shrink.ML›

end

(*  Title:      SpecCheck/shrink/shrink_types.ML
    Author:     Kevin Kappelmann

Shared type definitions for SpecCheck shrinkable types.
*)

signature SPECCHECK_SHRINK_TYPES =
sig
  type 'a shrink = 'a -> 'a Seq.seq
end

structure SpecCheck_Shrink_Types : SPECCHECK_SHRINK_TYPES =
struct

type 'a shrink = 'a -> 'a Seq.seq

end

(*  Title:      SpecCheck/shrink/shrink_base.ML
    Author:     Kevin Kappelmann

Basic utility functions to create and combine shrink functions.
*)

signature SPECCHECK_SHRINK_BASE =
sig
  include SPECCHECK_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 SpecCheck_Shrink_Base : SPECCHECK_SHRINK_BASE =
struct
open SpecCheck_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

(*  Title:      SpecCheck/shrink/shrink.ML
    Author:     Kevin Kappelmann, TU Muenchen

Structure containing all shrink functions.
*)
structure SpecCheck_Shrink =
struct

open SpecCheck_Shrink_Base

end

✐‹creator "Kevin Kappelmann"›
section ‹SpecCheck›
theory SpecCheck
imports
  SpecCheck_Generators
  SpecCheck_Show
  SpecCheck_Shrink
  SpecCheck_Output_Style
begin

paragraph ‹Summary›
text ‹The SpecCheck (specification based) testing environment and Lecker testing framework.›

ML_file ‹speccheck.ML›
ML_file ‹lecker.ML›

end

(*  Title:      SpecCheck/speccheck.ML
    Author:     Lukas Bulwahn, Nicolai Schaffroth, and Kevin Kappelmann TU Muenchen
    Author:     Christopher League

Specification-based testing of ML programs.
*)

signature SPECCHECK =
sig

  (*tries to shrink a given (failing) input to a smaller, failing input*)
  val try_shrink : 'a SpecCheck_Property.prop -> 'a SpecCheck_Shrink.shrink -> 'a -> int ->
    SpecCheck_Base.stats -> ('a * SpecCheck_Base.stats)

  (*runs a property for a given test case and returns the result and the updated the statistics*)
  val run_a_test : 'a SpecCheck_Property.prop -> 'a -> SpecCheck_Base.stats ->
    SpecCheck_Base.result_single * SpecCheck_Base.stats

  (*returns the new state after executing the test*)
  val check_style : 'a SpecCheck_Output_Style_Types.output_style ->
    ('a SpecCheck_Show.show) option ->  'a SpecCheck_Shrink.shrink ->
    ('a, 's) SpecCheck_Generator.gen_state -> string -> 'a SpecCheck_Property.prop ->
    Proof.context -> 's -> 's
  val check_shrink : 'a SpecCheck_Show.show -> 'a SpecCheck_Shrink.shrink ->
    ('a, 's) SpecCheck_Generator.gen_state -> string -> 'a SpecCheck_Property.prop ->
    Proof.context -> 's -> 's
  val check : 'a SpecCheck_Show.show -> ('a, 's) SpecCheck_Generator.gen_state -> string ->
    'a SpecCheck_Property.prop -> Proof.context -> 's -> 's
  val check_base : ('a, 's) SpecCheck_Generator.gen_state -> string ->
    'a SpecCheck_Property.prop -> Proof.context -> 's -> 's

  (*returns all unprocessed elements of the sequence*)
  val check_seq_style : 'a SpecCheck_Output_Style_Types.output_style ->
    ('a SpecCheck_Show.show) option -> 'a Seq.seq -> string -> 'a SpecCheck_Property.prop ->
    Proof.context -> 'a Seq.seq
  val check_seq : 'a SpecCheck_Show.show -> 'a Seq.seq -> string -> 'a SpecCheck_Property.prop ->
    Proof.context -> 'a Seq.seq
  val check_seq_base : 'a Seq.seq -> string -> 'a SpecCheck_Property.prop -> Proof.context ->
    'a Seq.seq

  (*returns all unused elements of the list*)
  val check_list_style : 'a SpecCheck_Output_Style_Types.output_style ->
    ('a SpecCheck_Show.show) option -> 'a list -> string -> 'a SpecCheck_Property.prop ->
    Proof.context -> 'a Seq.seq
  val check_list : 'a SpecCheck_Show.show -> 'a list -> string -> 'a SpecCheck_Property.prop ->
    Proof.context -> 'a Seq.seq
  val check_list_base : 'a list -> string -> 'a SpecCheck_Property.prop -> Proof.context ->
    'a Seq.seq

end
                                                                   
structure SpecCheck : SPECCHECK =
struct

open SpecCheck_Base

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

    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

    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

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
}

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 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
    (*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 test output_style init_stats show_opt shrink opt_gen name prop ctxt state =
  let
    val max_discard_ratio = Config.get ctxt SpecCheck_Configuration.max_discard_ratio
    val max_success = Config.get ctxt SpecCheck_Configuration.max_success
    (*number of counterexamples to generate before stopping the test*)
    val num_counterexamples =
      let val conf_num_counterexamples =
        Config.get ctxt SpecCheck_Configuration.num_counterexamples
      in if conf_num_counterexamples > 0 then conf_num_counterexamples else ~1 end
    val max_shrinks = Config.get ctxt SpecCheck_Configuration.max_shrinks

    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
    Timing.timing (fn _ => run_tests opt_gen state init_stats []) ()
    |> uncurry (apfst o output_style show_opt ctxt name)
    |> snd
  end

fun check_style style show_opt shrink =
  test style empty_stats show_opt shrink o SpecCheck_Generator.map SOME

fun check_shrink show = check_style SpecCheck_Default_Output_Style.default (SOME show)
fun check show = check_shrink show SpecCheck_Shrink.none

fun check_base gen =
  check_style SpecCheck_Default_Output_Style.default NONE SpecCheck_Shrink.none gen

fun check_seq_style style show_opt xq name prop ctxt =
  test style empty_stats show_opt SpecCheck_Shrink.none SpecCheck_Generator.of_seq name prop ctxt
    xq

fun check_seq show = check_seq_style SpecCheck_Default_Output_Style.default (SOME show)
fun check_seq_base xq = check_seq_style SpecCheck_Default_Output_Style.default NONE xq

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)

end

(*  Title:      SpecCheck/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

✐‹creator "Kevin Kappelmann"›
section ‹Dynamic Generators›
theory SpecCheck_Dynamic
imports SpecCheck
begin

paragraph ‹Summary›
text ‹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/SpecCheck_Examples.thy"} for some
examples contrasting this approach to the standard one (specifying generators as ML code).›

ML_file ‹dynamic_construct.ML›
ML_file ‹speccheck_dynamic.ML›

end

(*  Title:      SpecCheck/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 SPECCHECK_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 SpecCheck_Dynamic_Construct : SPECCHECK_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", ("SpecCheck_Generator.bernoulli 0.5", "Gen_Construction.string_of_bool")),
  ("option", ("SpecCheck_Generator.option (SpecCheck_Generator.bernoulli (2.0 / 3.0))",
              "ML_Syntax.print_option")),
  ("list", ("SpecCheck_Generator.unfold_while (K (SpecCheck_Generator.bernoulli (2.0 / 3.0)))",
            " ML_Syntax.print_list")),
  ("unit", ("gen_unit", "fn () => \"()\"")),
  ("int", ("SpecCheck_Generator.range_int (~2147483647,2147483647)", "string_of_int")),
  ("real", ("SpecCheck_Generator.real", "string_of_real")),
  ("char", ("SpecCheck_Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
  ("string", ("SpecCheck_Generator.string (SpecCheck_Generator.nonneg 100) SpecCheck_Generator.char",
              "ML_Syntax.print_string")),
  ("->", ("SpecCheck_Generator.function' o snd", "fn (_, _) => fn _ => \"fn\"")),
  ("typ", ("SpecCheck_Generator.typ'' (SpecCheck_Generator.return 8) (SpecCheck_Generator.nonneg 4) (SpecCheck_Generator.nonneg 4) (1,1,1)",
           "Pretty.string_of o Syntax.pretty_typ (Context.the_local_context ())")),
  ("term", ("SpecCheck_Generator.term_tree (fn h => fn _ => "
            ^ "let val ngen = SpecCheck_Generator.nonneg (Int.max (0, 4-h))\n"
            ^ "    val aterm_gen = SpecCheck_Generator.aterm' (SpecCheck_Generator.return 8) ngen (1,1,1,0)\n"
            ^ "in SpecCheck_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 = "SpecCheck_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 ["SpecCheck.check (Pretty.str o (",
  compose_printer ctxt ty, ")) (", compose_generator ctxt ty, ")  \"", name,
  "\" (SpecCheck_Property.prop (", spec,
  ")) (Context.the_local_context ()) (SpecCheck_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;