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