src/HOL/Library/SML_Quickcheck.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 43880 2eb76746c408
permissions -rw-r--r--
add nat => enat coercion
haftmann@33084
     1
haftmann@33084
     2
header {* Install quickcheck of SML code generator *}
haftmann@33084
     3
haftmann@33084
     4
theory SML_Quickcheck
haftmann@33084
     5
imports Main
haftmann@33084
     6
begin
haftmann@33084
     7
bulwahn@43880
     8
ML {*
bulwahn@43880
     9
signature SML_QUICKCHECK =
bulwahn@43880
    10
sig
bulwahn@43880
    11
  val active : bool Config.T
bulwahn@43880
    12
  val setup : theory -> theory  
bulwahn@43880
    13
end;
bulwahn@43880
    14
bulwahn@43880
    15
structure SML_Quickcheck : SML_QUICKCHECK =
bulwahn@43880
    16
struct
bulwahn@43880
    17
bulwahn@43880
    18
val active = Attrib.setup_config_bool @{binding quickcheck_SML_active} (K true);
bulwahn@43880
    19
bulwahn@43880
    20
fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
bulwahn@43876
    21
  let
bulwahn@43880
    22
    val prop = list_abs_free (Term.add_frees t [], t)
bulwahn@43880
    23
    val test_fun = Codegen.test_term ctxt prop
bulwahn@43880
    24
    val iterations = Config.get ctxt Quickcheck.iterations
bulwahn@43880
    25
    fun iterate size 0 = NONE
bulwahn@43880
    26
      | iterate size j =
bulwahn@43880
    27
          let
bulwahn@43880
    28
            val result = test_fun size handle Match =>
bulwahn@43880
    29
              (if Config.get ctxt Quickcheck.quiet then ()
bulwahn@43880
    30
               else warning "Exception Match raised during quickcheck"; NONE)
bulwahn@43880
    31
          in
bulwahn@43880
    32
            case result of NONE => iterate size (j - 1) | SOME q => SOME q
bulwahn@43880
    33
          end
bulwahn@43880
    34
  in (iterate size iterations, NONE) end
bulwahn@43880
    35
bulwahn@43880
    36
val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
bulwahn@43880
    37
bulwahn@43880
    38
val setup =
bulwahn@43880
    39
  Inductive_Codegen.quickcheck_setup
bulwahn@43880
    40
  #> Context.theory_map (Quickcheck.add_tester ("SML", (active, test_goals)))
bulwahn@43880
    41
bulwahn@43880
    42
end;
haftmann@33084
    43
*}
haftmann@33084
    44
bulwahn@43880
    45
setup {* SML_Quickcheck.setup *}
bulwahn@43880
    46
haftmann@33084
    47
end