modernizing predicate_compile_quickcheck
authorbulwahn
Thu Oct 20 09:11:13 2011 +0200 (2011-10-20)
changeset 4521466ba67adafab
parent 45213 92e03ea2b5cf
child 45215 1b2132017774
modernizing predicate_compile_quickcheck
src/HOL/Lazy_Sequence.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Lazy_Sequence.thy	Thu Oct 20 08:20:35 2011 +0200
     1.2 +++ b/src/HOL/Lazy_Sequence.thy	Thu Oct 20 09:11:13 2011 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  subsubsection {* Small lazy typeclasses *}
     1.5  
     1.6  class small_lazy =
     1.7 -  fixes small_lazy :: "int \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
     1.8 +  fixes small_lazy :: "code_numeral \<Rightarrow> 'a Lazy_Sequence.lazy_sequence"
     1.9  
    1.10  instantiation unit :: small_lazy
    1.11  begin
    1.12 @@ -178,7 +178,7 @@
    1.13  termination 
    1.14    by (relation "measure (%(d, i). nat (d + 1 - i))") auto
    1.15  
    1.16 -definition "small_lazy d = small_lazy' d (- d)"
    1.17 +definition "small_lazy d = small_lazy' (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.18  
    1.19  instance ..
    1.20  
    1.21 @@ -197,7 +197,7 @@
    1.22  instantiation list :: (small_lazy) small_lazy
    1.23  begin
    1.24  
    1.25 -fun small_lazy_list :: "int => 'a list Lazy_Sequence.lazy_sequence"
    1.26 +fun small_lazy_list :: "code_numeral => 'a list Lazy_Sequence.lazy_sequence"
    1.27  where
    1.28    "small_lazy_list d = Lazy_Sequence.append (Lazy_Sequence.single []) (if d > 0 then Lazy_Sequence.bind (product (small_lazy (d - 1)) (small_lazy (d - 1))) (%(x, xs). Lazy_Sequence.single (x # xs)) else Lazy_Sequence.empty)"
    1.29  
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 20 08:20:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Oct 20 09:11:13 2011 +0200
     2.3 @@ -519,14 +519,8 @@
     2.4    compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
     2.5    mk_random =
     2.6      (fn T => fn additional_arguments =>
     2.7 -      let
     2.8 -        val small_lazy =
     2.9 -         Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
    2.10 -         @{typ "Int.int"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T])) 
    2.11 -      in
    2.12 -        absdummy @{typ code_numeral} (small_lazy $ HOLogic.mk_number @{typ int} 3)
    2.13 -      end
    2.14 -    ),
    2.15 +      Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
    2.16 +        @{typ "Code_Numeral.code_numeral"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
    2.17    modify_funT = I,
    2.18    additional_arguments = K [],
    2.19    wrap_compilation = K (K (K (K (K I))))
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Oct 20 08:20:35 2011 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Thu Oct 20 09:11:13 2011 +0200
     3.3 @@ -18,10 +18,7 @@
     3.4        Proof.context -> Proof.context;
     3.5    val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
     3.6      Proof.context -> Proof.context
     3.7 -
     3.8 -  val tracing : bool Unsynchronized.ref;
     3.9 -  val quiet : bool Unsynchronized.ref;
    3.10 -  val test_goals : (Predicate_Compile_Aux.compilation * bool * bool * int) ->
    3.11 +  val test_goals : (Predicate_Compile_Aux.compilation * bool * bool) ->
    3.12      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
    3.13        -> Quickcheck.result list
    3.14    val nrandom : int Unsynchronized.ref;
    3.15 @@ -70,10 +67,6 @@
    3.16  );
    3.17  val put_new_dseq_result = New_Dseq_Result.put;
    3.18  
    3.19 -val tracing = Unsynchronized.ref false;
    3.20 -
    3.21 -val quiet = Unsynchronized.ref true;
    3.22 -
    3.23  val target = "Quickcheck"
    3.24  
    3.25  val nrandom = Unsynchronized.ref 3;
    3.26 @@ -331,16 +324,22 @@
    3.27      prog
    3.28    end
    3.29  
    3.30 -fun try_upto quiet f i =
    3.31 +fun try_upto_depth ctxt f =
    3.32    let
    3.33 -    fun try' j =
    3.34 -      if j <= i then
    3.35 +    val max_depth = Config.get ctxt Quickcheck.depth
    3.36 +    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    3.37 +    fun try' i =
    3.38 +      if i <= max_depth then
    3.39          let
    3.40 -          val _ = if quiet then () else Output.urgent_message ("Executing depth " ^ string_of_int j)
    3.41 +          val _ = message ("Depth: " ^ string_of_int i)
    3.42 +          val (result, time) =
    3.43 +            cpu_time ("Depth " ^ string_of_int i) (fn () =>
    3.44 +              f i handle Match => (if Config.get ctxt Quickcheck.quiet then ()
    3.45 +                    else warning "Exception Match raised during quickcheck"; NONE))
    3.46 +         val _ = if Config.get ctxt Quickcheck.timing then
    3.47 +           message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
    3.48          in
    3.49 -          case f j handle Match => (if quiet then ()
    3.50 -             else warning "Exception Match raised during quickcheck"; NONE)
    3.51 -          of NONE => try' (j + 1) | SOME q => SOME q
    3.52 +          case result of NONE => try' (i + 1) | SOME q => SOME q
    3.53          end
    3.54        else
    3.55          NONE
    3.56 @@ -350,35 +349,35 @@
    3.57  
    3.58  (* quickcheck interface functions *)
    3.59  
    3.60 -fun compile_term' compilation options depth ctxt (t, eval_terms) =
    3.61 +fun compile_term' compilation options ctxt (t, eval_terms) =
    3.62    let
    3.63      val size = Config.get ctxt Quickcheck.size
    3.64      val c = compile_term compilation options ctxt t
    3.65 -    val counterexample = try_upto (!quiet) (c size (!nrandom)) depth
    3.66 +    val counterexample = try_upto_depth ctxt (c size (!nrandom))
    3.67    in
    3.68      Quickcheck.Result
    3.69        {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
    3.70         evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
    3.71    end
    3.72  
    3.73 -fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
    3.74 +fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening =
    3.75    let
    3.76       val options =
    3.77         set_fail_safe_function_flattening fail_safe_function_flattening
    3.78           (set_function_flattening function_flattening (get_options ()))
    3.79    in
    3.80 -    compile_term' compilation options depth
    3.81 +    compile_term' compilation options
    3.82    end
    3.83  
    3.84  
    3.85  fun test_goals options ctxt (limit_time, is_interactive) insts goals =
    3.86    let
    3.87 -    val (compilation, function_flattening, fail_safe_function_flattening, depth) = options
    3.88 -    val correct_inst_goals = Quickcheck.instantiate_goals ctxt insts goals
    3.89 +    val (compilation, function_flattening, fail_safe_function_flattening) = options
    3.90 +    val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
    3.91      val test_term =
    3.92 -      quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth
    3.93 +      quickcheck_compile_term compilation function_flattening fail_safe_function_flattening
    3.94    in
    3.95 -    Quickcheck.collect_results (test_term ctxt)
    3.96 +    Quickcheck_Common.collect_results (test_term ctxt)
    3.97        (maps (map snd) correct_inst_goals) []
    3.98    end
    3.99    
   3.100 @@ -388,11 +387,11 @@
   3.101  
   3.102  val setup = 
   3.103    Context.theory_map (Quickcheck.add_tester ("predicate_compile_wo_ff",
   3.104 -    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true, 4))))
   3.105 +    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, false, true))))
   3.106    #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_fs",
   3.107 -    (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4))))
   3.108 +    (ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true))))
   3.109    #> Context.theory_map (Quickcheck.add_tester ("predicate_compile_ff_nofs",
   3.110 -    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true, 4))))
   3.111 +    (wo_ff_active, test_goals (Predicate_Compile_Aux.New_Pos_Random_DSeq, true, true))))
   3.112  
   3.113  
   3.114  end;