src/HOL/Library/SML_Quickcheck.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 42161 d1b39536e1fb
child 42427 5611f178a747
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     1 
     2 header {* Install quickcheck of SML code generator *}
     3 
     4 theory SML_Quickcheck
     5 imports Main
     6 begin
     7 
     8 setup {*
     9   Inductive_Codegen.quickcheck_setup #>
    10   Context.theory_map (Quickcheck.add_generator ("SML",
    11     fn ctxt => fn [(t, eval_terms)] =>
    12       let
    13         val prop = list_abs_free (Term.add_frees t [], t)
    14         val test_fun = Codegen.test_term ctxt prop 
    15         val iterations = Config.get ctxt Quickcheck.iterations
    16         fun iterate size 0 = NONE
    17           | iterate size j =
    18             let
    19               val result = test_fun size handle Match => 
    20                 (if Config.get ctxt Quickcheck.quiet then ()
    21                  else warning "Exception Match raised during quickcheck"; NONE)
    22             in
    23               case result of NONE => iterate size (j - 1) | SOME q => SOME q
    24             end
    25      in fn [_, size] => (iterate size iterations, NONE) end))
    26 *}
    27 
    28 end