1.1 --- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -7,11 +7,14 @@
     1.4  uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
     1.5  begin
     1.6  
     1.7 -setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
     1.8 +setup {* Predicate_Compile_Quickcheck.setup *}
     1.9 +
    1.10 +(*setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
    1.11    Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4)) *}
    1.12  setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_fs",
    1.13    Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4)) *}
    1.14  setup {* Context.theory_map (Quickcheck.add_generator ("predicate_compile_ff_nofs",
    1.15    Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4)) *}
    1.16 +*)
    1.17  
    1.18  end
    1.19 \ No newline at end of file

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     2.3 @@ -21,13 +21,14 @@
     2.4  
     2.5    val tracing : bool Unsynchronized.ref;
     2.6    val quiet : bool Unsynchronized.ref;
     2.7 -  val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
     2.8 -    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option;
     2.9 -(*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
    2.10 +  val test_goals : (Predicate_Compile_Aux.compilation * bool * bool * int) ->
    2.11 +    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
    2.12 +      -> Quickcheck.result list
    2.13    val nrandom : int Unsynchronized.ref;
    2.14    val debug : bool Unsynchronized.ref;
    2.15    val function_flattening : bool Unsynchronized.ref;
    2.16    val no_higher_order_predicate : string list Unsynchronized.ref;
    2.17 +  val setup : theory -> theory
    2.18  end;
    2.19  
    2.20  structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
    2.21 @@ -215,7 +216,7 @@
    2.22    let val ({cpu, ...}, result) = Timing.timing e ()
    2.23    in (result, (description, Time.toMilliseconds cpu)) end
    2.24  
    2.25 -fun compile_term compilation options ctxt [(t, eval_terms)] =
    2.26 +fun compile_term compilation options ctxt t =
    2.27    let
    2.28      val t' = list_abs_free (Term.add_frees t [], t)
    2.29      val thy = Theory.copy (Proof_Context.theory_of ctxt)
    2.30 @@ -349,11 +350,15 @@
    2.31  
    2.32  (* quickcheck interface functions *)
    2.33  
    2.34 -fun compile_term' compilation options depth ctxt t =
    2.35 +fun compile_term' compilation options depth ctxt (t, eval_terms) =
    2.36    let
    2.37 +    val size = Config.get ctxt Quickcheck.size
    2.38      val c = compile_term compilation options ctxt t
    2.39 +    val counterexample = try_upto (!quiet) (c size (!nrandom)) depth
    2.40    in
    2.41 -    fn [card, size] => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
    2.42 +    Quickcheck.Result
    2.43 +      {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
    2.44 +       evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
    2.45    end
    2.46  
    2.47  fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
    2.48 @@ -365,4 +370,29 @@
    2.49      compile_term' compilation options depth
    2.50    end
    2.51  
    2.52 +
    2.53 +fun test_goals options ctxt (limit_time, is_interactive) insts goals =
    2.54 +  let
    2.55 +    val (compilation, function_flattening, fail_safe_function_flattening, depth) = options
    2.56 +    val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
    2.57 +    val test_term =
    2.58 +      quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth
    2.59 +  in
    2.60 +    Quickcheck.collect_results (test_term ctxt)
    2.61 +      (maps (map snd) correct_inst_goals) []
    2.62 +  end
    2.63 +  
    2.64 +val wo_ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_wo_ff_active} (K false);
    2.65 +val ff_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_active} (K false);
    2.66 +val ff_nofs_active = Attrib.setup_config_bool @{binding quickcheck_pc_ff_nofs_active} (K false);
    2.67 +
    2.68 +val setup = 
    2.69 +  Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff",
    2.70 +    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true, 4))))
    2.71 +  #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs",
    2.72 +    (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4))))
    2.73 +  #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs",
    2.74 +    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4))))
    2.75 +
    2.76 +
    2.77  end;