author | wenzelm |
Tue, 05 Apr 2016 20:03:24 +0200 | |
changeset 62876 | 507c90523113 |
parent 62549 | 9498623b27f0 |
child 62889 | 99c7f31615c2 |
permissions | -rw-r--r-- |
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
1 |
(* Title: HOL/Tools/Quickcheck/narrowing_generators.ML |
41905 | 2 |
Author: Lukas Bulwahn, TU Muenchen |
3 |
||
41938 | 4 |
Narrowing-based counterexample generation. |
41905 | 5 |
*) |
6 |
||
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
7 |
signature NARROWING_GENERATORS = |
41905 | 8 |
sig |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
9 |
val allow_existentials : bool Config.T |
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset
|
10 |
val finite_functions : bool Config.T |
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
11 |
val overlord : bool Config.T |
48270 | 12 |
val ghc_options : string Config.T (* FIXME prefer settings, i.e. getenv (!?) *) |
43891
4690f76f327a
making active configuration public in narrowing-based quickcheck
bulwahn
parents:
43878
diff
changeset
|
13 |
val active : bool Config.T |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
14 |
datatype counterexample = Universal_Counterexample of (term * counterexample) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
15 |
| Existential_Counterexample of (term * counterexample) list |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
16 |
| Empty_Assignment |
45725
2987b29518aa
the narrowing also indicates if counterexample is potentially spurious
bulwahn
parents:
45685
diff
changeset
|
17 |
val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
18 |
val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context |
41905 | 19 |
end; |
20 |
||
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
21 |
structure Narrowing_Generators : NARROWING_GENERATORS = |
41905 | 22 |
struct |
23 |
||
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset
|
24 |
(* configurations *) |
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset
|
25 |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
26 |
val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true) |
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42361
diff
changeset
|
27 |
val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true) |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
28 |
val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false) |
47843
4da917ed49b7
adding configuration to pass options to the ghc call in quickcheck[narrowing]
bulwahn
parents:
47330
diff
changeset
|
29 |
val ghc_options = Attrib.setup_config_string @{binding quickcheck_narrowing_ghc_options} (K "") |
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset
|
30 |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
31 |
(* partial_term_of instances *) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
32 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
33 |
fun mk_partial_term_of (x, T) = |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
34 |
Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of}, |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
35 |
Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) |
56242 | 36 |
$ Logic.mk_type T $ x |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
37 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
38 |
(** formal definition **) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
39 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
40 |
fun add_partial_term_of tyco raw_vs thy = |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
41 |
let |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
42 |
val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
43 |
val ty = Type (tyco, map TFree vs); |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
44 |
val lhs = Const (@{const_name partial_term_of}, |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
45 |
Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
46 |
$ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term}); |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
47 |
val rhs = @{term "undefined :: Code_Evaluation.term"}; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
48 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
49 |
fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
50 |
o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
51 |
in |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
52 |
thy |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
53 |
|> Class.instantiation ([tyco], vs, @{sort partial_term_of}) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
54 |
|> `(fn lthy => Syntax.check_term lthy eq) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
55 |
|-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
56 |
|> snd |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59434
diff
changeset
|
57 |
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
58 |
end; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
59 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
60 |
fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
61 |
let |
48272 | 62 |
val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of}) |
63 |
andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}; |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
64 |
in if need_inst then add_partial_term_of tyco raw_vs thy else thy end; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
65 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
66 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
67 |
(** code equations for datatypes **) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
68 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
69 |
fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
70 |
let |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43317
diff
changeset
|
71 |
val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys)) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50046
diff
changeset
|
72 |
val narrowing_term = @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50046
diff
changeset
|
73 |
$ HOLogic.mk_list @{typ narrowing_term} (rev frees) |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
74 |
val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
75 |
(map mk_partial_term_of (frees ~~ tys)) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
76 |
(@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
77 |
val insts = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59498
diff
changeset
|
78 |
map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
79 |
[Free ("ty", Term.itselfT ty), narrowing_term, rhs] |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59498
diff
changeset
|
80 |
val cty = Thm.global_ctyp_of thy ty; |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
81 |
in |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
82 |
@{thm partial_term_of_anything} |
60801 | 83 |
|> Thm.instantiate' [SOME cty] insts |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
84 |
|> Thm.varifyT_global |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
85 |
end |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
86 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
87 |
fun add_partial_term_of_code tyco raw_vs raw_cs thy = |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
88 |
let |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
89 |
val algebra = Sign.classes_of thy; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
90 |
val vs = map (fn (v, sort) => |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
91 |
(v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
92 |
val ty = Type (tyco, map TFree vs); |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
93 |
val cs = (map o apsnd o apsnd o map o map_atyps) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
94 |
(fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51143
diff
changeset
|
95 |
val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco); |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45159
diff
changeset
|
96 |
val var_insts = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59498
diff
changeset
|
97 |
map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) |
46758
4106258260b3
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
bulwahn
parents:
46587
diff
changeset
|
98 |
[Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"}, |
45344
e209da839ff4
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
wenzelm
parents:
45159
diff
changeset
|
99 |
@{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]; |
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
100 |
val var_eq = |
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
101 |
@{thm partial_term_of_anything} |
60801 | 102 |
|> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts |
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
103 |
|> Thm.varifyT_global |
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
104 |
val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs; |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
105 |
in |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
106 |
thy |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
107 |
|> Code.del_eqns const |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
108 |
|> fold Code.add_eqn eqs |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
109 |
end; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
110 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
111 |
fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
112 |
let |
48272 | 113 |
val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of}; |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
114 |
in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
115 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
116 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
117 |
(* narrowing generators *) |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
118 |
|
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
119 |
(** narrowing specific names and types **) |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
120 |
|
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
121 |
exception FUNCTION_TYPE; |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
122 |
|
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
123 |
val narrowingN = "narrowing"; |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
124 |
|
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
125 |
fun narrowingT T = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50046
diff
changeset
|
126 |
@{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T]) |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
127 |
|
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
128 |
fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
129 |
|
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
130 |
fun mk_apply (T, t) (U, u) = |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
131 |
let |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
132 |
val (_, U') = dest_funT U |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
133 |
in |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
134 |
(U', Const (@{const_name Quickcheck_Narrowing.apply}, |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
135 |
narrowingT U --> narrowingT T --> narrowingT U') $ u $ t) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
136 |
end |
59154 | 137 |
|
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
138 |
fun mk_sum (t, u) = |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
139 |
let |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
140 |
val T = fastype_of t |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
141 |
in |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
142 |
Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
143 |
end |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
144 |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
145 |
(** deriving narrowing instances **) |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
146 |
|
50046 | 147 |
fun mk_equations descr vs narrowings = |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
148 |
let |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
149 |
fun mk_call T = |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42184
diff
changeset
|
150 |
(T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)) |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
151 |
fun mk_aux_call fTs (k, _) (tyco, Ts) = |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
152 |
let |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
153 |
val T = Type (tyco, Ts) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
154 |
val _ = if not (null fTs) then raise FUNCTION_TYPE else () |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
155 |
in |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
156 |
(T, nth narrowings k) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
157 |
end |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
158 |
fun mk_consexpr simpleT (c, xs) = |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
159 |
let |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
160 |
val Ts = map fst xs |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
161 |
in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
162 |
fun mk_rhs exprs = foldr1 mk_sum exprs |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
163 |
val rhss = |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset
|
164 |
Old_Datatype_Aux.interpret_construction descr vs |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
165 |
{ atyp = mk_call, dtyp = mk_aux_call } |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
166 |
|> (map o apfst) Type |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
167 |
|> map (fn (T, cs) => map (mk_consexpr T) cs) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
168 |
|> map mk_rhs |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
169 |
val lhss = narrowings |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
170 |
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
171 |
in |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
172 |
eqs |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
173 |
end |
59154 | 174 |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
175 |
fun contains_recursive_type_under_function_types xs = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
176 |
exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset
|
177 |
(case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
178 |
|
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
179 |
fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
180 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset
|
181 |
val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..."; |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
182 |
val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames); |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
183 |
in |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
184 |
if not (contains_recursive_type_under_function_types descr) then |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
185 |
thy |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
186 |
|> Class.instantiation (tycos, vs, @{sort narrowing}) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
187 |
|> Quickcheck_Common.define_functions |
50046 | 188 |
(fn narrowings => mk_equations descr vs narrowings, NONE) |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
189 |
prfx [] narrowingsN (map narrowingT (Ts @ Us)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59434
diff
changeset
|
190 |
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
191 |
else |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
192 |
thy |
41963
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
193 |
end; |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
194 |
|
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
195 |
(* testing framework *) |
d8c3b26b3da4
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
bulwahn
parents:
41953
diff
changeset
|
196 |
|
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset
|
197 |
val target = "Haskell_Quickcheck" |
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
198 |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
199 |
(** invocation of Haskell interpreter **) |
41905 | 200 |
|
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset
|
201 |
val narrowing_engine = |
56135 | 202 |
File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"} |
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset
|
203 |
|
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43619
diff
changeset
|
204 |
val pnf_narrowing_engine = |
56135 | 205 |
File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"} |
41905 | 206 |
|
207 |
fun exec verbose code = |
|
60956 | 208 |
ML_Context.exec (fn () => |
62495 | 209 |
ML_Compiler0.use_text ML_Env.context |
60956 | 210 |
{line = 0, file = "generated code", verbose = verbose, debug = false} code) |
41905 | 211 |
|
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
212 |
fun with_overlord_dir name f = |
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
213 |
let |
43602 | 214 |
val path = |
215 |
Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
216 |
val _ = Isabelle_System.mkdirs path; |
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
217 |
in Exn.release (Exn.capture f path) end; |
43379
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset
|
218 |
|
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset
|
219 |
fun elapsed_time description e = |
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset
|
220 |
let val ({elapsed, ...}, result) = Timing.timing e () |
8c4b383e5143
quickcheck_narrowing returns some timing information
bulwahn
parents:
43329
diff
changeset
|
221 |
in (result, (description, Time.toMilliseconds elapsed)) end |
59154 | 222 |
|
50046 | 223 |
fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = |
41905 | 224 |
let |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
225 |
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie |
58843 | 226 |
fun message s = if quiet then () else writeln s |
227 |
fun verbose_message s = if not quiet andalso verbose then writeln s else () |
|
43585 | 228 |
val current_size = Unsynchronized.ref 0 |
59154 | 229 |
val current_result = Unsynchronized.ref Quickcheck.empty_result |
41930
1e008cc4883a
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn
parents:
41925
diff
changeset
|
230 |
val tmp_prefix = "Quickcheck_Narrowing" |
47843
4da917ed49b7
adding configuration to pass options to the ghc call in quickcheck[narrowing]
bulwahn
parents:
47330
diff
changeset
|
231 |
val ghc_options = Config.get ctxt ghc_options |
43079
4022892a2f28
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
bulwahn
parents:
43047
diff
changeset
|
232 |
val with_tmp_dir = |
59154 | 233 |
if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir |
234 |
fun run in_path = |
|
41905 | 235 |
let |
48568 | 236 |
fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs")) |
237 |
val generatedN = Code_Target.generatedN |
|
238 |
val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file; |
|
239 |
val code = the (AList.lookup (op =) code_modules generatedN) |
|
240 |
val code_file = mk_code_file generatedN |
|
241 |
val narrowing_engine_file = mk_code_file "Narrowing_Engine" |
|
242 |
val main_file = mk_code_file "Main" |
|
41905 | 243 |
val main = "module Main where {\n\n" ^ |
46335
0fd9ab902b5a
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
bulwahn
parents:
46316
diff
changeset
|
244 |
"import System.IO;\n" ^ |
0fd9ab902b5a
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
bulwahn
parents:
46316
diff
changeset
|
245 |
"import System.Environment;\n" ^ |
41933
10f254a4e5b9
adapting Main file generation for Quickcheck_Narrowing
bulwahn
parents:
41932
diff
changeset
|
246 |
"import Narrowing_Engine;\n" ^ |
48568 | 247 |
"import " ^ generatedN ^ " ;\n\n" ^ |
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45420
diff
changeset
|
248 |
"main = getArgs >>= \\[potential, size] -> " ^ |
48568 | 249 |
"Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^ |
41905 | 250 |
"}\n" |
48568 | 251 |
val _ = map (uncurry File.write) (includes @ |
252 |
[(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine), |
|
55676 | 253 |
(code_file, code), (main_file, main)]) |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62530
diff
changeset
|
254 |
val executable = File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")) |
44926
de3ed037c9a5
create central list for language extensions used by the haskell code generator
noschinl
parents:
44852
diff
changeset
|
255 |
val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ |
47843
4da917ed49b7
adding configuration to pass options to the ghc call in quickcheck[narrowing]
bulwahn
parents:
47330
diff
changeset
|
256 |
ghc_options ^ " " ^ |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62530
diff
changeset
|
257 |
(space_implode " " (map File.bash_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ |
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset
|
258 |
" -o " ^ executable ^ ";" |
50046 | 259 |
val (_, compilation_time) = |
48568 | 260 |
elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) |
43585 | 261 |
val _ = Quickcheck.add_timing compilation_time current_result |
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45420
diff
changeset
|
262 |
fun haskell_string_of_bool v = if v then "True" else "False" |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43702
diff
changeset
|
263 |
val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
264 |
fun with_size genuine_only k = |
43308
fd6cc1378fec
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
bulwahn
parents:
43240
diff
changeset
|
265 |
if k > size then |
43585 | 266 |
(NONE, !current_result) |
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset
|
267 |
else |
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset
|
268 |
let |
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45760
diff
changeset
|
269 |
val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) |
43585 | 270 |
val _ = current_size := k |
271 |
val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) |
|
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45420
diff
changeset
|
272 |
(fn () => Isabelle_System.bash_output |
45760
3b5a735897c3
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
bulwahn
parents:
45757
diff
changeset
|
273 |
(executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k)) |
43585 | 274 |
val _ = Quickcheck.add_timing timing current_result |
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset
|
275 |
in |
43585 | 276 |
if response = "NONE\n" then |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
277 |
with_size genuine_only (k + 1) |
43585 | 278 |
else |
279 |
let |
|
280 |
val output_value = the_default "NONE" |
|
281 |
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response) |
|
282 |
val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml |
|
62876 | 283 |
^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))"; |
43585 | 284 |
val ctxt' = ctxt |
285 |
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) |
|
59154 | 286 |
|> Context.proof_map (exec false ml_code); |
45757
e32dd098f57a
renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents:
45756
diff
changeset
|
287 |
val counterexample = get ctxt' () |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
288 |
in |
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
289 |
if is_genuine counterexample then |
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
290 |
(counterexample, !current_result) |
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
291 |
else |
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
292 |
let |
59434 | 293 |
val cex = Option.map (rpair []) (counterexample_of counterexample); |
294 |
val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); |
|
295 |
val _ = message "Quickcheck continues to find a genuine counterexample..."; |
|
296 |
in with_size true (k + 1) end |
|
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
297 |
end |
59154 | 298 |
end |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
299 |
in with_size genuine_only 0 end |
43585 | 300 |
in |
45418 | 301 |
with_tmp_dir tmp_prefix run |
43585 | 302 |
end; |
41905 | 303 |
|
55757 | 304 |
fun dynamic_value_strict opts cookie ctxt postproc t = |
41905 | 305 |
let |
56920
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56242
diff
changeset
|
306 |
fun evaluator program _ vs_ty_t deps = |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
307 |
Exn.interruptible_capture (value opts ctxt cookie) |
56920
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56242
diff
changeset
|
308 |
(Code_Target.evaluator ctxt target program deps true vs_ty_t); |
61077
06cca32aa519
thread context for exceptions from forks, e.g. relevant when printing errors;
wenzelm
parents:
60956
diff
changeset
|
309 |
in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end; |
41905 | 310 |
|
59154 | 311 |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
312 |
(** counterexample generator **) |
46042 | 313 |
|
59154 | 314 |
datatype counterexample = |
315 |
Universal_Counterexample of (term * counterexample) |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
316 |
| Existential_Counterexample of (term * counterexample) list |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
317 |
| Empty_Assignment |
59154 | 318 |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
319 |
fun map_counterexample f Empty_Assignment = Empty_Assignment |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
320 |
| map_counterexample f (Universal_Counterexample (t, c)) = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
321 |
Universal_Counterexample (f t, map_counterexample f c) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
322 |
| map_counterexample f (Existential_Counterexample cs) = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
323 |
Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
324 |
|
59154 | 325 |
structure Data = Proof_Data |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
326 |
( |
59154 | 327 |
type T = |
328 |
(unit -> (bool * term list) option) * |
|
329 |
(unit -> counterexample option); |
|
330 |
val empty: T = |
|
331 |
(fn () => raise Fail "counterexample", |
|
332 |
fn () => raise Fail "existential_counterexample"); |
|
333 |
fun init _ = empty; |
|
334 |
); |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
335 |
|
59154 | 336 |
val get_counterexample = #1 o Data.get; |
337 |
val get_existential_counterexample = #2 o Data.get; |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
338 |
|
59154 | 339 |
val put_counterexample = Data.map o @{apply 2(1)} o K; |
340 |
val put_existential_counterexample = Data.map o @{apply 2(2)} o K; |
|
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset
|
341 |
|
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
342 |
fun finitize_functions (xTs, t) = |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
343 |
let |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
344 |
val (names, boundTs) = split_list xTs |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
345 |
fun mk_eval_ffun dT rT = |
59154 | 346 |
Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
347 |
Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT) |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
348 |
fun mk_eval_cfun dT rT = |
59154 | 349 |
Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
350 |
Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT) |
50046 | 351 |
fun eval_function (Type (@{type_name fun}, [dT, rT])) = |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
352 |
let |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
353 |
val (rt', rT') = eval_function rT |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
354 |
in |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
355 |
case dT of |
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
356 |
Type (@{type_name fun}, _) => |
44241 | 357 |
(fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), |
358 |
Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT'])) |
|
359 |
| _ => |
|
360 |
(fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), |
|
361 |
Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT'])) |
|
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
362 |
end |
47330
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
363 |
| eval_function (T as Type (@{type_name prod}, [fT, sT])) = |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
364 |
let |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
365 |
val (ft', fT') = eval_function fT |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
366 |
val (st', sT') = eval_function sT |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
367 |
val T' = Type (@{type_name prod}, [fT', sT']) |
55932 | 368 |
val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T) |
47330
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
369 |
fun apply_dummy T t = absdummy T (t (Bound 0)) |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
370 |
in |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
371 |
(fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T') |
8fe04753a210
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
bulwahn
parents:
46758
diff
changeset
|
372 |
end |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
373 |
| eval_function T = (I, T) |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
374 |
val (tt, boundTs') = split_list (map eval_function boundTs) |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
375 |
val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t) |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
376 |
in |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
377 |
(names ~~ boundTs', t') |
42024
51df23535105
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation
bulwahn
parents:
42023
diff
changeset
|
378 |
end |
42023
1bd4b6d1c482
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
bulwahn
parents:
42020
diff
changeset
|
379 |
|
45039
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
380 |
fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT) |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
381 |
|
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
382 |
fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) = |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
383 |
absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
384 |
| eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) = |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
385 |
let |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
386 |
val (T1, T2) = dest_ffun (body_type T) |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
387 |
in |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
388 |
Quickcheck_Common.mk_fun_upd T1 T2 |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
389 |
(eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
390 |
end |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
391 |
| eval_finite_functions t = t |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
392 |
|
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset
|
393 |
(** tester **) |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
394 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
395 |
val rewrs = |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
396 |
map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
397 |
(@{thms all_simps} @ @{thms ex_simps}) |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
398 |
@ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) |
46316 | 399 |
[@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}, |
400 |
@{thm meta_eq_to_obj_eq [OF Ex1_def]}] |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
401 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
402 |
fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
403 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
404 |
fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
405 |
apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
406 |
| strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
407 |
apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
408 |
| strip_quantifiers t = ([], t) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
409 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
410 |
fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t)) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
411 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
412 |
fun mk_property qs t = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
413 |
let |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
414 |
fun enclose (@{const_name Ex}, (x, T)) t = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
415 |
Const (@{const_name Quickcheck_Narrowing.exists}, (T --> @{typ property}) --> @{typ property}) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
416 |
$ Abs (x, T, t) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
417 |
| enclose (@{const_name All}, (x, T)) t = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
418 |
Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property}) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
419 |
$ Abs (x, T, t) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
420 |
in |
45002
df36896aae0f
removing superfluous definition in the quickcheck narrowing invocation as the code generator now generates valid Haskell code with necessary type annotations without a separate definition
bulwahn
parents:
44926
diff
changeset
|
421 |
fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
422 |
end |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
423 |
|
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
424 |
fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = |
51673
4dfa00e264d8
separate data used for case translation from the datatype package
traytel
parents:
51672
diff
changeset
|
425 |
Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) => |
43317 | 426 |
(t, mk_case_term ctxt (p - 1) qs' c)) cs) |
50046 | 427 |
| mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) = |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
428 |
if p = 0 then t else mk_case_term ctxt (p - 1) qs' c |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
429 |
|
45039
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
430 |
val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions |
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
431 |
|
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
432 |
fun mk_terms ctxt qs result = |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
433 |
let |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
434 |
val |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
435 |
ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs) |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
436 |
in |
50046 | 437 |
map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps |
45039
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
45002
diff
changeset
|
438 |
|> map (apsnd post_process) |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
439 |
end |
59154 | 440 |
|
50046 | 441 |
fun test_term ctxt catch_code_errors (t, _) = |
41905 | 442 |
let |
59154 | 443 |
fun dest_result (Quickcheck.Result r) = r |
43585 | 444 |
val opts = |
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45760
diff
changeset
|
445 |
((Config.get ctxt Quickcheck.genuine_only, |
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45760
diff
changeset
|
446 |
(Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)), |
45685
e2e928af750b
quickcheck narrowing also shows potential counterexamples
bulwahn
parents:
45420
diff
changeset
|
447 |
Config.get ctxt Quickcheck.size) |
42361 | 448 |
val thy = Proof_Context.theory_of ctxt |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
449 |
val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
450 |
val pnf_t = make_pnf_term thy t' |
41905 | 451 |
in |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
452 |
if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then |
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
453 |
let |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
454 |
fun wrap f (qs, t) = |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
455 |
let val (qs1, qs2) = split_list qs in |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
456 |
apfst (map2 pair qs1) (f (qs2, t)) end |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
457 |
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
458 |
val (qs, prop_t) = finitize (strip_quantifiers pnf_t) |
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
459 |
val act = if catch_code_errors then try else (fn f => SOME o f) |
59154 | 460 |
val execute = |
461 |
dynamic_value_strict (true, opts) |
|
462 |
((K true, fn _ => error ""), |
|
463 |
(get_existential_counterexample, put_existential_counterexample, |
|
464 |
"Narrowing_Generators.put_existential_counterexample")) |
|
465 |
ctxt (apfst o Option.map o map_counterexample) |
|
466 |
in |
|
467 |
case act execute (mk_property qs prop_t) of |
|
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
468 |
SOME (counterexample, result) => Quickcheck.Result |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
469 |
{counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample, |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
470 |
evaluation_terms = Option.map (K []) counterexample, |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
471 |
timings = #timings (dest_result result), reports = #reports (dest_result result)} |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
472 |
| NONE => |
59434 | 473 |
(Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; |
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
474 |
Quickcheck.empty_result) |
43237
8f5c3c6c2909
adding compilation that allows existentials in Quickcheck_Narrowing
bulwahn
parents:
43114
diff
changeset
|
475 |
end |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
476 |
else |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
477 |
let |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
478 |
val frees = Term.add_frees t [] |
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
479 |
val t' = fold_rev absfree frees t |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46042
diff
changeset
|
480 |
fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t)) |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
481 |
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
482 |
fun ensure_testable t = |
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
483 |
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t |
59154 | 484 |
fun is_genuine (SOME (true, _)) = true |
45756
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
485 |
| is_genuine _ = false |
295658b28d3b
quickcheck narrowing continues searching after found a potentially spurious counterexample
bulwahn
parents:
45728
diff
changeset
|
486 |
val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process)) |
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
487 |
val act = if catch_code_errors then try else (fn f => SOME o f) |
59154 | 488 |
val execute = |
489 |
dynamic_value_strict (false, opts) |
|
490 |
((is_genuine, counterexample_of), |
|
491 |
(get_counterexample, put_counterexample, |
|
492 |
"Narrowing_Generators.put_counterexample")) |
|
493 |
ctxt (apfst o Option.map o apsnd o map) |
|
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
494 |
in |
59154 | 495 |
case act execute (ensure_testable (finitize t')) of |
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
496 |
SOME (counterexample, result) => |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
497 |
Quickcheck.Result |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
498 |
{counterexample = counterexample_of counterexample, |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
499 |
evaluation_terms = Option.map (K []) counterexample, |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
500 |
timings = #timings (dest_result result), |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
501 |
reports = #reports (dest_result result)} |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
502 |
| NONE => |
59434 | 503 |
(Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; |
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
504 |
Quickcheck.empty_result) |
43240
da47097bd589
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
bulwahn
parents:
43237
diff
changeset
|
505 |
end |
41905 | 506 |
end; |
507 |
||
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
508 |
fun test_goals ctxt catch_code_errors insts goals = |
43314
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset
|
509 |
if (not (getenv "ISABELLE_GHC" = "")) then |
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset
|
510 |
let |
59434 | 511 |
val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..."; |
45159
3f1d1ce024cb
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
bulwahn
parents:
45039
diff
changeset
|
512 |
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals |
43314
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset
|
513 |
in |
46309
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
514 |
Quickcheck_Common.collect_results (test_term ctxt catch_code_errors) |
693d8d7bc3cd
catching code generation errors in quickcheck-narrowing
bulwahn
parents:
46219
diff
changeset
|
515 |
(maps (map snd) correct_inst_goals) [] |
43314
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset
|
516 |
end |
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset
|
517 |
else |
58843 | 518 |
(if Config.get ctxt Quickcheck.quiet then () else writeln |
43314
a9090cabca14
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
bulwahn
parents:
43308
diff
changeset
|
519 |
("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set " |
43911
a1da544e2652
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
bulwahn
parents:
43910
diff
changeset
|
520 |
^ "this variable to your GHC Haskell compiler in your settings file. " |
a1da544e2652
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
bulwahn
parents:
43910
diff
changeset
|
521 |
^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false."); |
a1da544e2652
more information for the user how to deactivate quickcheck_narrowing if he does not want to use it
bulwahn
parents:
43910
diff
changeset
|
522 |
[Quickcheck.empty_result]) |
43114
b9fca691addd
Quickcheck Narrowing only requires one compilation with GHC now
bulwahn
parents:
43079
diff
changeset
|
523 |
|
43047
26774ccb1c74
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
bulwahn
parents:
42616
diff
changeset
|
524 |
(* setup *) |
41905 | 525 |
|
46587
d3bcc356cc60
preliminarily switching quickcheck-narrowing off by default (probably it should only be invoked if concrete testing does not work)
bulwahn
parents:
46335
diff
changeset
|
526 |
val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false); |
43878
eeb10fdd9535
changed every tester to have a configuration in quickcheck; enabling parallel testing of different testers in quickcheck
bulwahn
parents:
43850
diff
changeset
|
527 |
|
58826 | 528 |
val _ = |
529 |
Theory.setup |
|
530 |
(Code.datatype_interpretation ensure_partial_term_of |
|
531 |
#> Code.datatype_interpretation ensure_partial_term_of_code |
|
532 |
#> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing} |
|
533 |
(@{sort narrowing}, instantiate_narrowing_datatype) |
|
534 |
#> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))); |
|
59154 | 535 |
|
44272 | 536 |
end; |