6 |
6 |
7 signature PREDICATE_COMPILE_QUICKCHECK = |
7 signature PREDICATE_COMPILE_QUICKCHECK = |
8 sig |
8 sig |
9 val quickcheck : Proof.context -> term -> int -> term list option |
9 val quickcheck : Proof.context -> term -> int -> term list option |
10 val test_ref : |
10 val test_ref : |
11 ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref |
11 ((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref |
|
12 val tracing : bool Unsynchronized.ref; |
12 end; |
13 end; |
13 |
14 |
14 structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = |
15 structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = |
15 struct |
16 struct |
16 |
17 |
17 open Predicate_Compile_Aux; |
18 open Predicate_Compile_Aux; |
18 |
19 |
19 val test_ref = |
20 val test_ref = |
20 Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) |
21 Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option); |
|
22 |
|
23 val tracing = Unsynchronized.ref false; |
21 |
24 |
22 val target = "Quickcheck" |
25 val target = "Quickcheck" |
23 |
26 |
24 val options = Options { |
27 val options = Options { |
25 expected_modes = NONE, |
28 expected_modes = NONE, |
26 proposed_modes = NONE, |
29 proposed_modes = NONE, |
27 proposed_names = [], |
30 proposed_names = [], |
28 show_steps = true, |
31 show_steps = true, |
29 show_intermediate_results = true, |
32 show_intermediate_results = true, |
30 show_proof_trace = false, |
33 show_proof_trace = false, |
31 show_modes = true, |
34 show_modes = false, |
32 show_mode_inference = false, |
35 show_mode_inference = false, |
33 show_compilation = true, |
36 show_compilation = false, |
34 skip_proof = false, |
37 skip_proof = false, |
35 |
38 compilation = Random, |
36 inductify = false, |
39 inductify = false |
37 random = false, |
|
38 depth_limited = false, |
|
39 annotated = false |
|
40 } |
40 } |
41 |
41 |
42 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs |
42 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs |
43 val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) |
43 val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) |
44 val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns) |
44 val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns) |
63 |
63 |
64 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
64 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
65 |
65 |
66 fun quickcheck ctxt t = |
66 fun quickcheck ctxt t = |
67 let |
67 let |
68 val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) |
68 (*val () = |
|
69 if !tracing then |
|
70 tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) |
|
71 else |
|
72 ()*) |
69 val ctxt' = ProofContext.theory (Context.copy_thy) ctxt |
73 val ctxt' = ProofContext.theory (Context.copy_thy) ctxt |
70 val thy = (ProofContext.theory_of ctxt') |
74 val thy = (ProofContext.theory_of ctxt') |
71 val (vs, t') = strip_abs t |
75 val (vs, t') = strip_abs t |
72 val vs' = Variable.variant_frees ctxt' [] vs |
76 val vs' = Variable.variant_frees ctxt' [] vs |
73 val t'' = subst_bounds (map Free (rev vs'), t') |
77 val t'' = subst_bounds (map Free (rev vs'), t') |
74 val (prems, concl) = strip_horn t'' |
78 val (prems, concl) = strip_horn t'' |
75 val constname = "pred_compile_quickcheck" |
79 val constname = "pred_compile_quickcheck" |
76 val full_constname = Sign.full_bname thy constname |
80 val full_constname = Sign.full_bname thy constname |
77 val constT = map snd vs' ---> @{typ bool} |
81 val constT = map snd vs' ---> @{typ bool} |
78 val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy |
82 val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy |
|
83 val const = Const (full_constname, constT) |
79 val t = Logic.list_implies |
84 val t = Logic.list_implies |
80 (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), |
85 (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), |
81 HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) |
86 HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) |
82 val tac = fn _ => Skip_Proof.cheat_tac thy' |
87 val tac = fn _ => Skip_Proof.cheat_tac thy1 |
83 val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac |
88 val intro = Goal.prove (ProofContext.init thy1) (map fst vs') [] t tac |
84 val _ = tracing (Display.string_of_thm ctxt' intro) |
89 (*val _ = tracing (Display.string_of_thm ctxt' intro)*) |
85 val thy'' = thy' |
90 val thy2 = (*Output.cond_timeit (!Quickcheck.timing) "predicate intros" |
86 |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) |
91 (fn () => *)(Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1) |
87 |> Predicate_Compile.preprocess options full_constname |
92 val thy3 = (*Output.cond_timeit (!Quickcheck.timing) "predicate preprocessing" |
88 |> Predicate_Compile_Core.add_equations options [full_constname] |
93 (fn () =>*) (Predicate_Compile.preprocess options const thy2) |
89 (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) |
94 val thy4 = Output.cond_timeit (!Quickcheck.timing) "random_dseq compilation" |
90 |> Predicate_Compile_Core.add_quickcheck_equations options [full_constname] |
95 (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3) |
91 val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname |
96 (*val depth_limited_modes = Predicate_Compile_Core.modes_of Depth_Limited thy'' full_constname*) |
92 val modes = Predicate_Compile_Core.random_modes_of thy'' full_constname |
97 val modes = Predicate_Compile_Core.modes_of Random_DSeq thy4 full_constname |
|
98 val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool |
93 val prog = |
99 val prog = |
94 if member (op =) modes ([], []) then |
100 if member eq_mode modes output_mode then |
95 let |
101 let |
96 val name = Predicate_Compile_Core.random_function_name_of thy'' full_constname ([], []) |
102 val name = Predicate_Compile_Core.function_name_of Random_DSeq thy4 full_constname output_mode |
97 val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) |
103 val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) |
98 in Const (name, T) $ Bound 0 end |
104 in |
|
105 Const (name, T) |
|
106 end |
99 (*else if member (op =) depth_limited_modes ([], []) then |
107 (*else if member (op =) depth_limited_modes ([], []) then |
100 let |
108 let |
101 val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) |
109 val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) |
102 val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) |
110 val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) |
103 in lift_pred (Const (name, T) $ Bound 0) end*) |
111 in lift_pred (Const (name, T) $ Bound 0) end*) |
104 else error "Predicate Compile Quickcheck failed" |
112 else error "Predicate Compile Quickcheck failed" |
105 val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog, |
113 val qc_term = mk_bind (prog, |
106 mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} |
114 mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} |
107 (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) |
115 (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))) |
108 val _ = tracing (Syntax.string_of_term ctxt' qc_term) |
116 val compilation = |
109 val compile = Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) |
117 Code_Eval.eval NONE ("Predicate_Compile_Quickcheck.test_ref", test_ref) |
110 (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) |
118 (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc) |
111 thy'' qc_term [] |
119 thy4 qc_term [] |
112 in |
120 in |
113 ((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield)) |
121 (fn size => |
|
122 Option.map fst (DSequence.yield (compilation size size |> Random_Engine.run) size true)) |
114 end |
123 end |
115 |
124 |
116 end; |
125 end; |