author | bulwahn |
Sat, 24 Oct 2009 16:55:42 +0200 | |
changeset 33140 | 83951822bfd0 |
parent 33139 | 9c01ee6f8ee9 |
child 33143 | 730a2e8a6ec6 |
permissions | -rw-r--r-- |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
2 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
3 |
A quickcheck generator based on the predicate compiler |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
4 |
*) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
5 |
|
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33139
diff
changeset
|
6 |
signature PREDICATE_COMPILE_QUICKCHECK = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
7 |
sig |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
8 |
val quickcheck : Proof.context -> term -> int -> term list option |
32740 | 9 |
val test_ref : |
10 |
((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
11 |
end; |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
12 |
|
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33139
diff
changeset
|
13 |
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
14 |
struct |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
15 |
|
32740 | 16 |
val test_ref = |
17 |
Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) |
|
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
18 |
val target = "Quickcheck" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
19 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
20 |
fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
21 |
val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
22 |
val mk_rpredT = #mk_predT (dest_compfuns Predicate_Compile_Core.rpred_compfuns) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
23 |
val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.rpred_compfuns) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
24 |
val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.rpred_compfuns) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
25 |
val lift_pred = #lift_pred (dest_compfuns Predicate_Compile_Core.rpred_compfuns) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
26 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
27 |
fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
28 |
| mk_split_lambda [x] t = lambda x t |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
29 |
| mk_split_lambda xs t = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
30 |
let |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
31 |
fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
32 |
| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
33 |
in |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
34 |
mk_split_lambda' xs t |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
35 |
end; |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
36 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
37 |
fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
38 |
| strip_imp_prems _ = []; |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
39 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
40 |
fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
41 |
| strip_imp_concl A = A : term; |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
42 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
43 |
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
44 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
45 |
fun quickcheck ctxt t = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
46 |
let |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
47 |
val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
48 |
val ctxt' = ProofContext.theory (Context.copy_thy) ctxt |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
49 |
val thy = (ProofContext.theory_of ctxt') |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
50 |
val (vs, t') = strip_abs t |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
51 |
val vs' = Variable.variant_frees ctxt' [] vs |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
52 |
val t'' = subst_bounds (map Free (rev vs'), t') |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
53 |
val (prems, concl) = strip_horn t'' |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
54 |
val constname = "pred_compile_quickcheck" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
55 |
val full_constname = Sign.full_bname thy constname |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
56 |
val constT = map snd vs' ---> @{typ bool} |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
57 |
val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
58 |
val t = Logic.list_implies |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
59 |
(map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
60 |
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
61 |
val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy') |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
62 |
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
63 |
val _ = tracing (Display.string_of_thm ctxt' intro) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
64 |
val thy'' = thy' |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
65 |
|> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) |
33123
3c7c4372f9ad
cleaned up debugging messages; added options to code_pred command
bulwahn
parents:
33114
diff
changeset
|
66 |
|> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33123
diff
changeset
|
67 |
|> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname] |
33139
9c01ee6f8ee9
added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents:
33138
diff
changeset
|
68 |
(* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) |
33132
07efd452a698
moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents:
33123
diff
changeset
|
69 |
|> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] |
33134
88c9c3460fe7
renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents:
33132
diff
changeset
|
70 |
val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
71 |
val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
72 |
val prog = |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
73 |
if member (op =) modes ([], []) then |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
74 |
let |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
75 |
val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) |
33138
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33134
diff
changeset
|
76 |
val T = [@{typ bool}, @{typ code_numeral}] ---> (mk_rpredT (HOLogic.mk_tupleT (map snd vs'))) |
e2e23987c59a
reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents:
33134
diff
changeset
|
77 |
in Const (name, T) $ @{term True} $ Bound 0 end |
33134
88c9c3460fe7
renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents:
33132
diff
changeset
|
78 |
else if member (op =) depth_limited_modes ([], []) then |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
79 |
let |
33134
88c9c3460fe7
renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents:
33132
diff
changeset
|
80 |
val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
81 |
val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
82 |
in lift_pred (Const (name, T) $ Bound 0) end |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
83 |
else error "Predicate Compile Quickcheck failed" |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
84 |
val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog, |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
85 |
mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
86 |
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
87 |
val _ = tracing (Syntax.string_of_term ctxt' qc_term) |
33140
83951822bfd0
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents:
33139
diff
changeset
|
88 |
val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) |
32672
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
89 |
(fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
90 |
thy'' qc_term [] |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
91 |
in |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
92 |
((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield)) |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
93 |
end |
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
94 |
|
90f3ce5d27ae
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents:
diff
changeset
|
95 |
end; |