src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 45685 e2e928af750b
parent 45420 d17556b9a89b
child 45725 2987b29518aa
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 30 09:21:09 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Nov 30 09:21:11 2011 +0100
     1.3 @@ -222,7 +222,7 @@
     1.4    let val ({elapsed, ...}, result) = Timing.timing e ()
     1.5    in (result, (description, Time.toMilliseconds elapsed)) end
     1.6    
     1.7 -fun value (contains_existentials, (quiet, size)) ctxt cookie (code, value_name) =
     1.8 +fun value (contains_existentials, ((potential, quiet), size)) ctxt cookie (code, value_name) =
     1.9    let
    1.10      val (get, put, put_ml) = cookie
    1.11      fun message s = if quiet then () else Output.urgent_message s
    1.12 @@ -242,7 +242,8 @@
    1.13            "import System;\n" ^
    1.14            "import Narrowing_Engine;\n" ^
    1.15            "import Generated_Code;\n\n" ^
    1.16 -          "main = getArgs >>= \\[size] -> Narrowing_Engine.depthCheck (read size) (Generated_Code.value ())\n\n" ^
    1.17 +          "main = getArgs >>= \\[potential, size] -> " ^
    1.18 +          "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
    1.19            "}\n"
    1.20          val code' = prefix "module Generated_Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    1.21            (unprefix "module Generated_Code where {" code)
    1.22 @@ -257,6 +258,7 @@
    1.23          val (result, compilation_time) =
    1.24            elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
    1.25          val _ = Quickcheck.add_timing compilation_time current_result
    1.26 +        fun haskell_string_of_bool v = if v then "True" else "False"
    1.27          val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.28          fun with_size k =
    1.29            if k > size then
    1.30 @@ -266,7 +268,8 @@
    1.31                val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
    1.32                val _ = current_size := k
    1.33                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    1.34 -                (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
    1.35 +                (fn () => Isabelle_System.bash_output
    1.36 +                  (executable ^ " " ^ haskell_string_of_bool potential  ^ " " ^ string_of_int k))
    1.37                val _ = Quickcheck.add_timing timing current_result
    1.38              in
    1.39                if response = "NONE\n" then
    1.40 @@ -415,7 +418,8 @@
    1.41    let
    1.42      fun dest_result (Quickcheck.Result r) = r 
    1.43      val opts =
    1.44 -      (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
    1.45 +      ((Config.get ctxt Quickcheck.potential, Config.get ctxt Quickcheck.quiet),
    1.46 +        Config.get ctxt Quickcheck.size)
    1.47      val thy = Proof_Context.theory_of ctxt
    1.48      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
    1.49      val pnf_t = make_pnf_term thy t'