quickcheck narrowing continues searching after found a potentially spurious counterexample
authorbulwahn
Mon Dec 05 12:35:58 2011 +0100 (2011-12-05)
changeset 45756295658b28d3b
parent 45755 b27a06dfb2ef
child 45757 e32dd098f57a
quickcheck narrowing continues searching after found a potentially spurious counterexample
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Dec 05 12:35:06 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Dec 05 12:35:58 2011 +0100
     1.3 @@ -52,12 +52,12 @@
     1.4    ", " ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
     1.5  
     1.6  eval :: Bool -> Bool -> (Bool -> Bool -> IO a) -> (Pos -> IO a) -> IO a;
     1.7 -eval potential p k u = answer potential p (\genuine p -> answer potential p k u) u;
     1.8 +eval potential p k u = answer potential p k u;
     1.9  
    1.10  ref :: Bool -> Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.11  ref potential r xs = eval potential (apply_fun r xs) (\genuine res -> if res then return 1 else report genuine r xs)
    1.12    (\p -> sumMapM (ref potential r) 1 (refineList xs p));
    1.13 -          
    1.14 +
    1.15  refute :: Bool -> Result -> IO Int;
    1.16  refute potential r = ref potential r (args r);
    1.17  
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:35:06 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Dec 05 12:35:58 2011 +0100
     2.3 @@ -222,9 +222,9 @@
     2.4    let val ({elapsed, ...}, result) = Timing.timing e ()
     2.5    in (result, (description, Time.toMilliseconds elapsed)) end
     2.6    
     2.7 -fun value (contains_existentials, ((potential, quiet), size)) ctxt cookie (code, value_name) =
     2.8 +fun value (contains_existentials, ((genuine_only, quiet), size)) ctxt cookie (code, value_name) =
     2.9    let
    2.10 -    val (get, put, put_ml) = cookie
    2.11 +    val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
    2.12      fun message s = if quiet then () else Output.urgent_message s
    2.13      val current_size = Unsynchronized.ref 0
    2.14      val current_result = Unsynchronized.ref Quickcheck.empty_result 
    2.15 @@ -260,7 +260,7 @@
    2.16          val _ = Quickcheck.add_timing compilation_time current_result
    2.17          fun haskell_string_of_bool v = if v then "True" else "False"
    2.18          val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    2.19 -        fun with_size k =
    2.20 +        fun with_size genuine_only k =
    2.21            if k > size then
    2.22              (NONE, !current_result)
    2.23            else
    2.24 @@ -269,11 +269,11 @@
    2.25                val _ = current_size := k
    2.26                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    2.27                  (fn () => Isabelle_System.bash_output
    2.28 -                  (executable ^ " " ^ haskell_string_of_bool potential  ^ " " ^ string_of_int k))
    2.29 +                  (executable ^ " " ^ haskell_string_of_bool (not genuine_only) ^ " " ^ string_of_int k))
    2.30                val _ = Quickcheck.add_timing timing current_result
    2.31              in
    2.32                if response = "NONE\n" then
    2.33 -                with_size (k + 1)
    2.34 +                with_size genuine_only (k + 1)
    2.35                else
    2.36                  let
    2.37                    val output_value = the_default "NONE"
    2.38 @@ -283,10 +283,22 @@
    2.39                      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    2.40                    val ctxt' = ctxt
    2.41                      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    2.42 -                    |> Context.proof_map (exec false ml_code);
    2.43 -                in (get ctxt' (), !current_result) end
    2.44 +                    |> Context.proof_map (exec false ml_code);                 
    2.45 +                  val counterexample =  get ctxt' ()
    2.46 +                in
    2.47 +                  if is_genuine counterexample then
    2.48 +                    (counterexample, !current_result)
    2.49 +                  else
    2.50 +                    let
    2.51 +                      val cex = Option.map (rpair []) (counterexample_of counterexample)
    2.52 +                    in
    2.53 +                      (Output.urgent_message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
    2.54 +                      Output.urgent_message "Quickcheck continues to find a genuine counterexample...";
    2.55 +                      with_size true (k + 1))
    2.56 +                    end
    2.57 +               end
    2.58              end 
    2.59 -      in with_size 0 end
    2.60 +      in with_size genuine_only 0 end
    2.61    in
    2.62      with_tmp_dir tmp_prefix run
    2.63    end;
    2.64 @@ -294,8 +306,9 @@
    2.65  fun dynamic_value_strict opts cookie thy postproc t =
    2.66    let
    2.67      val ctxt = Proof_Context.init_global thy
    2.68 -    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie)
    2.69 -      (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
    2.70 +    fun evaluator naming program ((_, vs_ty), t) deps =
    2.71 +      Exn.interruptible_capture (value opts ctxt cookie)
    2.72 +        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
    2.73    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    2.74  
    2.75  (** counterexample generator **)
    2.76 @@ -418,7 +431,7 @@
    2.77    let
    2.78      fun dest_result (Quickcheck.Result r) = r 
    2.79      val opts =
    2.80 -      ((Config.get ctxt Quickcheck.potential, Config.get ctxt Quickcheck.quiet),
    2.81 +      ((not (Config.get ctxt Quickcheck.potential), Config.get ctxt Quickcheck.quiet),
    2.82          Config.get ctxt Quickcheck.size)
    2.83      val thy = Proof_Context.theory_of ctxt
    2.84      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
    2.85 @@ -432,8 +445,8 @@
    2.86          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    2.87          val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
    2.88          val (counterexample, result) = dynamic_value_strict (true, opts)
    2.89 -          (Existential_Counterexample.get, Existential_Counterexample.put,
    2.90 -            "Narrowing_Generators.put_existential_counterexample")
    2.91 +          ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
    2.92 +            "Narrowing_Generators.put_existential_counterexample"))
    2.93            thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
    2.94        in
    2.95          Quickcheck.Result
    2.96 @@ -443,18 +456,22 @@
    2.97        end
    2.98      else
    2.99        let
   2.100 -        val t' = fold_rev absfree (Term.add_frees t []) t
   2.101 +        val frees = Term.add_frees t []
   2.102 +        val t' = fold_rev absfree frees t
   2.103          fun wrap f t = list_abs (f (strip_abs t))
   2.104          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   2.105          fun ensure_testable t =
   2.106            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   2.107 +        fun is_genuine (SOME (true, _)) = true 
   2.108 +          | is_genuine _ = false
   2.109 +        val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
   2.110          val (counterexample, result) = dynamic_value_strict (false, opts)
   2.111 -          (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   2.112 +          ((is_genuine, counterexample_of),
   2.113 +            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
   2.114            thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
   2.115        in
   2.116          Quickcheck.Result
   2.117 -         {counterexample =
   2.118 -           Option.map (apsnd (((curry (op ~~)) (Term.add_free_names t [])) o map post_process)) counterexample,
   2.119 +         {counterexample = counterexample_of counterexample,
   2.120            evaluation_terms = Option.map (K []) counterexample,
   2.121            timings = #timings (dest_result result), reports = #reports (dest_result result)}
   2.122        end