author | bulwahn |
Fri, 06 Nov 2009 08:11:58 +0100 | |
changeset 33475 | 42fed8eac357 |
parent 33375 | fd3e861f8d31 |
child 33486 | e1552d8718ac |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
3 |
|
33265 | 4 |
A quickcheck generator based on the predicate compiler. |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
5 |
*) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE_QUICKCHECK = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
sig |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
9 |
val quickcheck : Proof.context -> term -> int -> term list option |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
10 |
val test_ref : |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
11 |
((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
12 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
13 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
14 |
structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
15 |
struct |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
|
33257 | 17 |
open Predicate_Compile_Aux; |
18 |
||
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
val test_ref = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
20 |
Unsynchronized.ref (NONE : (unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
val target = "Quickcheck" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
23 |
|
33257 | 24 |
val options = Options { |
25 |
expected_modes = NONE, |
|
26 |
show_steps = true, |
|
27 |
show_intermediate_results = true, |
|
28 |
show_proof_trace = false, |
|
29 |
show_modes = true, |
|
30 |
show_mode_inference = false, |
|
31 |
show_compilation = true, |
|
32 |
skip_proof = false, |
|
33 |
||
34 |
inductify = false, |
|
33375 | 35 |
random = false, |
33475
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33375
diff
changeset
|
36 |
depth_limited = false, |
42fed8eac357
improved handling of overloaded constants; examples with numerals
bulwahn
parents:
33375
diff
changeset
|
37 |
annotated = false |
33257 | 38 |
} |
39 |
||
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
40 |
fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
41 |
val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns) |
33256
b350516cb1f9
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
bulwahn
parents:
33250
diff
changeset
|
42 |
val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns) |
b350516cb1f9
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
bulwahn
parents:
33250
diff
changeset
|
43 |
val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns) |
b350516cb1f9
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
bulwahn
parents:
33250
diff
changeset
|
44 |
val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
45 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
46 |
fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
47 |
| mk_split_lambda [x] t = lambda x t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
48 |
| mk_split_lambda xs t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
49 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
50 |
fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
51 |
| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
52 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
53 |
mk_split_lambda' xs t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
54 |
end; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
55 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
56 |
fun strip_imp_prems (Const("op -->", _) $ A $ B) = A :: strip_imp_prems B |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
57 |
| strip_imp_prems _ = []; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
58 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
59 |
fun strip_imp_concl (Const("op -->", _) $ A $ B) = strip_imp_concl B |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
60 |
| strip_imp_concl A = A : term; |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
61 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
62 |
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
63 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
64 |
fun quickcheck ctxt t = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
65 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
66 |
val _ = tracing ("Starting quickcheck with " ^ (Syntax.string_of_term ctxt t)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
67 |
val ctxt' = ProofContext.theory (Context.copy_thy) ctxt |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
68 |
val thy = (ProofContext.theory_of ctxt') |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
69 |
val (vs, t') = strip_abs t |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
70 |
val vs' = Variable.variant_frees ctxt' [] vs |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
71 |
val t'' = subst_bounds (map Free (rev vs'), t') |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
72 |
val (prems, concl) = strip_horn t'' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
73 |
val constname = "pred_compile_quickcheck" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
74 |
val full_constname = Sign.full_bname thy constname |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
75 |
val constT = map snd vs' ---> @{typ bool} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
76 |
val thy' = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
77 |
val t = Logic.list_implies |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
78 |
(map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]), |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
79 |
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs'))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
80 |
val tac = fn _ => Skip_Proof.cheat_tac thy' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
81 |
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
82 |
val _ = tracing (Display.string_of_thm ctxt' intro) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
83 |
val thy'' = thy' |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
84 |
|> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) |
33257 | 85 |
|> Predicate_Compile.preprocess options full_constname |
86 |
|> Predicate_Compile_Core.add_equations options [full_constname] |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
87 |
(* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) |
33257 | 88 |
|> Predicate_Compile_Core.add_quickcheck_equations options [full_constname] |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
89 |
val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
90 |
val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
91 |
val prog = |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
92 |
if member (op =) modes ([], []) then |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
93 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
94 |
val name = Predicate_Compile_Core.generator_name_of thy'' full_constname ([], []) |
33257 | 95 |
val T = [@{typ code_numeral}] ---> (mk_randompredT (HOLogic.mk_tupleT (map snd vs'))) |
96 |
in Const (name, T) $ Bound 0 end |
|
33256
b350516cb1f9
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
bulwahn
parents:
33250
diff
changeset
|
97 |
(*else if member (op =) depth_limited_modes ([], []) then |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
98 |
let |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
99 |
val name = Predicate_Compile_Core.depth_limited_function_name_of thy'' full_constname ([], []) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
100 |
val T = @{typ code_numeral} --> (mk_predT (HOLogic.mk_tupleT (map snd vs'))) |
33256
b350516cb1f9
adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
bulwahn
parents:
33250
diff
changeset
|
101 |
in lift_pred (Const (name, T) $ Bound 0) end*) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
102 |
else error "Predicate Compile Quickcheck failed" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
103 |
val qc_term = Abs ("size", @{typ code_numeral}, mk_bind (prog, |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
104 |
mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
105 |
(map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
106 |
val _ = tracing (Syntax.string_of_term ctxt' qc_term) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
107 |
val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
108 |
(fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
109 |
thy'' qc_term [] |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
110 |
in |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
111 |
((compile #> Random_Engine.run) #> (Option.map fst o Predicate.yield)) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
112 |
end |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
113 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
114 |
end; |