src/HOL/Library/SML_Quickcheck.thy
author bulwahn
Tue Apr 05 09:38:28 2011 +0200 (2011-04-05)
changeset 42231 bc1891226d00
parent 42161 d1b39536e1fb
child 42427 5611f178a747
permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
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
haftmann@33084
     8
setup {*
haftmann@37390
     9
  Inductive_Codegen.quickcheck_setup #>
bulwahn@40919
    10
  Context.theory_map (Quickcheck.add_generator ("SML",
bulwahn@42159
    11
    fn ctxt => fn [(t, eval_terms)] =>
bulwahn@40919
    12
      let
bulwahn@42161
    13
        val prop = list_abs_free (Term.add_frees t [], t)
bulwahn@42161
    14
        val test_fun = Codegen.test_term ctxt prop 
bulwahn@40919
    15
        val iterations = Config.get ctxt Quickcheck.iterations
bulwahn@40919
    16
        fun iterate size 0 = NONE
bulwahn@40919
    17
          | iterate size j =
bulwahn@40919
    18
            let
bulwahn@40919
    19
              val result = test_fun size handle Match => 
bulwahn@40919
    20
                (if Config.get ctxt Quickcheck.quiet then ()
bulwahn@40919
    21
                 else warning "Exception Match raised during quickcheck"; NONE)
bulwahn@40919
    22
            in
bulwahn@40919
    23
              case result of NONE => iterate size (j - 1) | SOME q => SOME q
bulwahn@40919
    24
            end
bulwahn@42161
    25
     in fn [_, size] => (iterate size iterations, NONE) end))
haftmann@33084
    26
*}
haftmann@33084
    27
haftmann@33084
    28
end