1.1 --- a/src/HOL/Library/SML_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -5,29 +5,43 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -setup {*
     1.8 +ML {*
     1.9 +signature SML_QUICKCHECK =
    1.10 +sig
    1.11 +  val active : bool Config.T
    1.12 +  val setup : theory -> theory  
    1.13 +end;
    1.14 +
    1.15 +structure SML_Quickcheck : SML_QUICKCHECK =
    1.16 +struct
    1.17 +
    1.18 +val active = Attrib.setup_config_bool @{binding quickcheck_SML_active} (K true);
    1.19 +
    1.20 +fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
    1.21    let
    1.22 -    fun compile_generator_expr ctxt [(t, eval_terms)] =
    1.23 -      let
    1.24 -        val prop = list_abs_free (Term.add_frees t [], t)
    1.25 -        val test_fun = Codegen.test_term ctxt prop
    1.26 -        val iterations = Config.get ctxt Quickcheck.iterations
    1.27 -        fun iterate size 0 = NONE
    1.28 -          | iterate size j =
    1.29 -              let
    1.30 -                val result = test_fun size handle Match =>
    1.31 -                  (if Config.get ctxt Quickcheck.quiet then ()
    1.32 -                   else warning "Exception Match raised during quickcheck"; NONE)
    1.33 -              in
    1.34 -                case result of NONE => iterate size (j - 1) | SOME q => SOME q
    1.35 -              end
    1.36 -      in fn [_, size] => (iterate size iterations, NONE) end))
    1.37 -    val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
    1.38 -  in
    1.39 -    Inductive_Codegen.quickcheck_setup
    1.40 -    #> Context.theory_map (Quickcheck.add_generator ("SML", compile_generator_expr))
    1.41 -    #> Context.theory_map (Quickcheck.add_tester ("SML", test_goals))
    1.42 -  end
    1.43 +    val prop = list_abs_free (Term.add_frees t [], t)
    1.44 +    val test_fun = Codegen.test_term ctxt prop
    1.45 +    val iterations = Config.get ctxt Quickcheck.iterations
    1.46 +    fun iterate size 0 = NONE
    1.47 +      | iterate size j =
    1.48 +          let
    1.49 +            val result = test_fun size handle Match =>
    1.50 +              (if Config.get ctxt Quickcheck.quiet then ()
    1.51 +               else warning "Exception Match raised during quickcheck"; NONE)
    1.52 +          in
    1.53 +            case result of NONE => iterate size (j - 1) | SOME q => SOME q
    1.54 +          end
    1.55 +  in (iterate size iterations, NONE) end
    1.56 +
    1.57 +val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
    1.58 +
    1.59 +val setup =
    1.60 +  Inductive_Codegen.quickcheck_setup
    1.61 +  #> Context.theory_map (Quickcheck.add_tester ("SML", (active, test_goals)))
    1.62 +
    1.63 +end;
    1.64  *}
    1.65  
    1.66 +setup {* SML_Quickcheck.setup *}
    1.67 +
    1.68  end