--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sat Jan 16 21:14:15 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Jan 20 11:56:45 2010 +0100
@@ -8,7 +8,8 @@
sig
val quickcheck : Proof.context -> term -> int -> term list option
val test_ref :
- ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref
+ ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
+ val tracing : bool Unsynchronized.ref;
end;
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK =
@@ -17,7 +18,9 @@
open Predicate_Compile_Aux;
val test_ref =
- Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option)
+ Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option);
+
+val tracing = Unsynchronized.ref false;
val target = "Quickcheck"
@@ -28,15 +31,12 @@
show_steps = true,
show_intermediate_results = true,
show_proof_trace = false,
- show_modes = true,
+ show_modes = false,
show_mode_inference = false,
- show_compilation = true,
+ show_compilation = false,
skip_proof = false,
-
- inductify = false,
- random = false,
- depth_limited = false,
- annotated = false
+ compilation = Random,
+ inductify = false
}
fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
@@ -65,7 +65,11 @@
fun quickcheck ctxt t =
let
- val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
+ (*val () =
+ if !tracing then
+ tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t))
+ else
+ ()*)
val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
val thy = (ProofContext.theory_of ctxt')
val (vs, t') = strip_abs t
@@ -75,42 +79,47 @@
val constname = "pred_compile_quickcheck"
val full_constname = Sign.full_bname thy constname
val constT = map snd vs' ---> @{typ bool}
- val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
+ val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
+ val const = Const (full_constname, constT)
val t = Logic.list_implies
- (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+ (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
- val tac = fn _ => Skip_Proof.cheat_tac thy'
- val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
- val _ = tracing (Display.string_of_thm ctxt' intro)
- val thy'' = thy'
- |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro)
- |> Predicate_Compile.preprocess options full_constname
- |> Predicate_Compile_Core.add_equations options [full_constname]
- (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
- |> Predicate_Compile_Core.add_quickcheck_equations options [full_constname]
- val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname
- val modes = Predicate_Compile_Core.random_modes_of thy'' full_constname
+ val tac = fn _ => Skip_Proof.cheat_tac thy1
+ val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac
+ (*val _ = tracing (Display.string_of_thm ctxt' intro)*)
+ val thy2 = (*Output.cond_timeit (!Quickcheck.timing) "predicate intros"
+ (fn () => *)(Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1)
+ val thy3 = (*Output.cond_timeit (!Quickcheck.timing) "predicate preprocessing"
+ (fn () =>*) (Predicate_Compile.preprocess options const thy2)
+ val thy4 = Output.cond_timeit (!Quickcheck.timing) "random_dseq compilation"
+ (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3)
+ (*val depth_limited_modes = Predicate_Compile_Core.modes_of Depth_Limited thy'' full_constname*)
+ val modes = Predicate_Compile_Core.modes_of Random_DSeq thy4 full_constname
+ val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
val prog =
- if member (op =) modes ([], []) then
+ if member eq_mode modes output_mode then
let
- val name = Predicate_Compile_Core.random_function_name_of thy'' full_constname ([], [])
- val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
- in Const (name, T) $ Bound 0 end
+ val name = Predicate_Compile_Core.function_name_of Random_DSeq thy4 full_constname output_mode
+ val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
+ in
+ Const (name, T)
+ end
(*else if member (op =) depth_limited_modes ([], []) then
let
val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], [])
val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs')))
in lift_pred (Const (name, T) $ Bound 0) end*)
else error "Predicate Compile Quickcheck failed"
- val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog,
+ val qc_term = mk_bind (prog,
mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
- val _ = tracing (Syntax.string_of_term ctxt' qc_term)
- val compile = Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
- (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc)
- thy'' qc_term []
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+ val compilation =
+ Code_Eval.eval NONE ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+ (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
+ thy4 qc_term []
in
- ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield))
+ (fn size =>
+ Option.map fst (DSequence.yield (compilation size size |> Random_Engine.run) size true))
end
end;