src/HOL/Spec_Check/spec_check.ML

added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;

(*  Title:      HOL/Spec_Check/spec_check.ML
    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
    Author:     Christopher League

Specification-based testing of ML programs with random values.
*)

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

  type output_style = Context.generic -> 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

  val checkGen : Context.generic -> 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit

  val check_property : Proof.context -> string -> unit
end;

structure Spec_Check : SPEC_CHECK =
struct

(* configurations *)

val gen_target = Attrib.setup_config_int @{binding spec_check_gen_target} (K 100)
val gen_max = Attrib.setup_config_int @{binding spec_check_gen_max} (K 400)
val examples = Attrib.setup_config_int @{binding spec_check_examples} (K 5)

val sort_examples = Attrib.setup_config_bool @{binding spec_check_sort_examples} (K true)
val show_stats = Attrib.setup_config_bool @{binding spec_check_show_stats} (K true)
val column_width = Attrib.setup_config_int @{binding spec_check_column_width} (K 22)
val style = Attrib.setup_config_string @{binding spec_check_style} (K "Perl")

open Property

type ('a, 'b) reader = 'b -> ('a * 'b) option
type 'a rep = ('a -> string) option

type output_style = Context.generic -> string ->
  {status: string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit}

fun limit ctxt gen = Generator.limit (Config.get_generic 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
)

fun get_style ctxt =
  let val name = Config.get_generic ctxt style
  in case Symtab.lookup (Style.get (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))

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

    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 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_generic 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
  in
    fn stream => iter (next stream, (s0, []))
  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]

(*calls the compiler and passes resulting type string to the parser*)
fun determine_type context s =
  let
    val ret = Unsynchronized.ref "return"
    val ctx : use_context = {
      tune_source = ML_Parse.fix_ints,
      name_space = ML_Env.name_space,
      str_of_pos = Position.here oo Position.line_file,
      print = fn r => ret := r,
      error = error
      }
    val _ = context |> Context.proof_map
      (ML_Context.exec (fn () => Secure.use_text ctx (0, "generated code") true s))
  in
    Gen_Construction.parse_pred (!ret)
  end;

(*calls the compiler and runs the test*)
fun run_test context s =
  let
    val _ = Context.proof_map
        (ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code")
        true s)) context
  in () end;

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

(*reads input and performs the test*)
fun gen_check_property check context s =
  let
    val func = make_fun s
    val (_, ty) = determine_type context func
  in run_test context (check (Proof_Context.theory_of context) "Check" (ty, func)) end;

val check_property = gen_check_property Gen_Construction.build_check
(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)

(*performs test for specification function*)
fun gen_check_property_f check context s =
  let
    val (name, ty) = determine_type context s
  in run_test context (check (Proof_Context.theory_of context) name (ty, s)) end;

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

end;

val check_property = Spec_Check.check_property;