author | wenzelm |
Mon, 30 May 2016 14:15:44 +0200 | |
changeset 63182 | b065b4833092 |
parent 63064 | 2f18172214c8 |
child 63239 | d562c9948dee |
permissions | -rw-r--r-- |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Quickcheck/quickcheck_common.ML |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, Lukas Bulwahn, TU Muenchen |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
3 |
|
41938 | 4 |
Common functions for quickcheck's generators. |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
5 |
*) |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
6 |
|
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
7 |
signature QUICKCHECK_COMMON = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
8 |
sig |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58186
diff
changeset
|
9 |
val compat_prefs : BNF_LFP_Compat.preference list |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
10 |
val strip_imp : term -> (term list * term) |
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset
|
11 |
val reflect_bool : bool -> term |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
12 |
val define_functions : ((term list -> term list) * (Proof.context -> tactic) option) |
62979 | 13 |
-> string -> string list -> string list -> typ list -> Proof.context -> Proof.context |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
14 |
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
15 |
-> (string * sort -> string * sort) option |
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
|
16 |
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list |
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
|
17 |
-> (typ option * (term * term list)) list list |
46565 | 18 |
val register_predicate : term * string -> Context.generic -> Context.generic |
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset
|
19 |
val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term |
62979 | 20 |
val collect_results : ('a -> Quickcheck.result) -> 'a list -> |
21 |
Quickcheck.result list -> Quickcheck.result list |
|
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
22 |
type result = (bool * term list) option * Quickcheck.report option |
62979 | 23 |
type generator = string * ((theory -> typ list -> bool) * |
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
24 |
(Proof.context -> (term * term list) list -> bool -> int list -> result)) |
45420
d17556b9a89b
more precise messages with the tester's name in quickcheck; tuned
bulwahn
parents:
45419
diff
changeset
|
25 |
val generator_test_goal_terms : |
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
26 |
generator -> Proof.context -> bool -> (string * typ) list |
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
27 |
-> (term * term list) list -> Quickcheck.result list |
62979 | 28 |
type instantiation = |
29 |
Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list -> |
|
30 |
string list -> string -> string list * string list -> typ list * typ list -> theory -> theory |
|
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
31 |
val ensure_sort : |
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
32 |
(((sort * sort) * sort) * |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset
|
33 |
((theory -> string list -> Old_Datatype_Aux.descr * (string * sort) list * string list |
62979 | 34 |
* string * (string list * string list) * (typ list * typ list)) * instantiation)) -> |
35 |
Old_Datatype_Aux.config -> string list -> theory -> theory |
|
36 |
val ensure_common_sort_datatype : (sort * instantiation) -> Old_Datatype_Aux.config -> |
|
37 |
string list -> theory -> theory |
|
58186 | 38 |
val datatype_interpretation : string -> sort * instantiation -> theory -> theory |
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
39 |
val gen_mk_parametric_generator_expr : |
62979 | 40 |
(((Proof.context -> term * term list -> term) * term) * typ) -> |
41 |
Proof.context -> (term * term list) list -> term |
|
45039
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
44241
diff
changeset
|
42 |
val mk_fun_upd : typ -> typ -> term * term -> term -> term |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
43 |
val post_process_term : term -> term |
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
44 |
val test_term : generator -> Proof.context -> bool -> term * term list -> Quickcheck.result |
62979 | 45 |
end |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
46 |
|
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
47 |
structure Quickcheck_Common : QUICKCHECK_COMMON = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
48 |
struct |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
49 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
50 |
(* static options *) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
51 |
|
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58186
diff
changeset
|
52 |
val compat_prefs = [BNF_LFP_Compat.Keep_Nesting, BNF_LFP_Compat.Include_GFPs] |
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58186
diff
changeset
|
53 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
54 |
val define_foundationally = false |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
55 |
|
62979 | 56 |
|
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
57 |
(* HOLogic's term functions *) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
58 |
|
62979 | 59 |
fun strip_imp (Const(@{const_name HOL.implies}, _) $ A $ B) = apfst (cons A) (strip_imp B) |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
60 |
| strip_imp A = ([], A) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
61 |
|
62979 | 62 |
fun reflect_bool b = if b then @{term True} else @{term False} |
45721
d1fb55c2ed65
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
bulwahn
parents:
45719
diff
changeset
|
63 |
|
62979 | 64 |
fun mk_undefined T = Const (@{const_name undefined}, T) |
65 |
||
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
|
66 |
|
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
|
67 |
(* testing functions: testing with increasing sizes (and cardinalities) *) |
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
|
68 |
|
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
69 |
type result = (bool * term list) option * Quickcheck.report option |
62979 | 70 |
type generator = |
71 |
string * ((theory -> typ list -> bool) * |
|
72 |
(Proof.context -> (term * term list) list -> bool -> int list -> result)) |
|
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
|
73 |
|
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
|
74 |
fun check_test_term t = |
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
|
75 |
let |
62979 | 76 |
val _ = |
77 |
(null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse |
|
78 |
error "Term to be tested contains type variables" |
|
79 |
val _ = |
|
80 |
null (Term.add_vars t []) orelse |
|
81 |
error "Term to be tested contains schematic variables" |
|
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
|
82 |
in () end |
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
|
83 |
|
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
|
84 |
fun cpu_time description e = |
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
|
85 |
let val ({cpu, ...}, result) = Timing.timing e () |
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
|
86 |
in (result, (description, Time.toMilliseconds cpu)) end |
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
|
87 |
|
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
88 |
fun test_term (name, (_, compile)) ctxt catch_code_errors (t, eval_terms) = |
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
|
89 |
let |
45757
e32dd098f57a
renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents:
45755
diff
changeset
|
90 |
val genuine_only = Config.get ctxt Quickcheck.genuine_only |
46478
cf1bcfb34c82
adding abort_potential functionality in quickcheck
bulwahn
parents:
46331
diff
changeset
|
91 |
val abort_potential = Config.get ctxt Quickcheck.abort_potential |
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
|
92 |
val _ = check_test_term t |
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
|
93 |
val names = Term.add_free_names t [] |
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
|
94 |
val current_size = Unsynchronized.ref 0 |
62979 | 95 |
val current_result = Unsynchronized.ref Quickcheck.empty_result |
96 |
val act = if catch_code_errors then try else (fn f => SOME o f) |
|
97 |
val (test_fun, comp_time) = |
|
98 |
cpu_time "quickcheck compilation" (fn () => act (compile ctxt) [(t, eval_terms)]) |
|
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset
|
99 |
val _ = Quickcheck.add_timing comp_time current_result |
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset
|
100 |
fun with_size test_fun genuine_only k = |
62979 | 101 |
if k > Config.get ctxt Quickcheck.size then NONE |
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
|
102 |
else |
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
|
103 |
let |
62979 | 104 |
val _ = |
105 |
Quickcheck.verbose_message ctxt |
|
106 |
("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k) |
|
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
|
107 |
val _ = current_size := k |
46565 | 108 |
val ((result, report), time) = |
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset
|
109 |
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1]) |
62979 | 110 |
val _ = |
111 |
if Config.get ctxt Quickcheck.timing then |
|
112 |
Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") |
|
113 |
else () |
|
46565 | 114 |
val _ = Quickcheck.add_timing time current_result |
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
|
115 |
val _ = Quickcheck.add_report k report current_result |
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
|
116 |
in |
62979 | 117 |
(case result of |
45754
394ecd91434a
dynamic genuine_flag in compilation of random and exhaustive
bulwahn
parents:
45753
diff
changeset
|
118 |
NONE => with_size test_fun genuine_only (k + 1) |
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset
|
119 |
| SOME (true, ts) => SOME (true, ts) |
45755
b27a06dfb2ef
outputing the potentially spurious counterexample and continue search
bulwahn
parents:
45754
diff
changeset
|
120 |
| SOME (false, ts) => |
62979 | 121 |
if abort_potential then SOME (false, ts) |
122 |
else |
|
123 |
let |
|
124 |
val (ts1, ts2) = chop (length names) ts |
|
125 |
val (eval_terms', _) = chop (length ts2) eval_terms |
|
126 |
val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) |
|
127 |
in |
|
128 |
Quickcheck.message ctxt |
|
129 |
(Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); |
|
130 |
Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample..."; |
|
131 |
with_size test_fun true k |
|
132 |
end) |
|
133 |
end |
|
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
|
134 |
in |
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset
|
135 |
case test_fun of |
62979 | 136 |
NONE => |
137 |
(Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); |
|
138 |
!current_result) |
|
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset
|
139 |
| SOME test_fun => |
62979 | 140 |
let |
141 |
val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...") |
|
142 |
val (response, exec_time) = |
|
143 |
cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1) |
|
144 |
val _ = Quickcheck.add_response names eval_terms response current_result |
|
145 |
val _ = Quickcheck.add_timing exec_time current_result |
|
146 |
in !current_result end |
|
147 |
end |
|
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
|
148 |
|
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
149 |
fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts = |
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
|
150 |
let |
45757
e32dd098f57a
renaming potential flag to genuine_only flag with an inverse semantics
bulwahn
parents:
45755
diff
changeset
|
151 |
val genuine_only = Config.get ctxt Quickcheck.genuine_only |
46478
cf1bcfb34c82
adding abort_potential functionality in quickcheck
bulwahn
parents:
46331
diff
changeset
|
152 |
val abort_potential = Config.get ctxt Quickcheck.abort_potential |
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
|
153 |
val thy = Proof_Context.theory_of ctxt |
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
|
154 |
val (ts', eval_terms) = split_list ts |
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
|
155 |
val _ = map check_test_term ts' |
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
|
156 |
val names = Term.add_free_names (hd ts') [] |
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
|
157 |
val Ts = map snd (Term.add_frees (hd ts') []) |
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
|
158 |
val current_result = Unsynchronized.ref Quickcheck.empty_result |
62979 | 159 |
fun test_card_size test_fun genuine_only (card, size) = (* FIXME: why decrement size by one? *) |
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
|
160 |
let |
45686
cf22004ad55d
adding more verbose messages to exhaustive quickcheck
bulwahn
parents:
45639
diff
changeset
|
161 |
val _ = |
45765
cb6ddee6a463
making the default behaviour of quickcheck a little bit less verbose;
bulwahn
parents:
45763
diff
changeset
|
162 |
Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^ |
46674 | 163 |
(if size = 0 then "" else "data size: " ^ string_of_int size ^ " and ") ^ |
62979 | 164 |
"cardinality: " ^ string_of_int card) |
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
|
165 |
val (ts, timing) = |
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
|
166 |
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) |
46674 | 167 |
(fn () => fst (test_fun genuine_only [card, size + 1])) |
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
|
168 |
val _ = Quickcheck.add_timing timing current_result |
62979 | 169 |
in Option.map (pair (card, size)) ts end |
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
|
170 |
val enumeration_card_size = |
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
171 |
if size_matters_for thy Ts then |
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
|
172 |
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size)) |
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
|
173 |
|> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) |
62979 | 174 |
else map (rpair 0) (1 upto (length ts)) |
45419
10ba32c347b0
quickcheck fails with code generator errors only if one tester is invoked
bulwahn
parents:
45418
diff
changeset
|
175 |
val act = if catch_code_errors then try else (fn f => SOME o f) |
10ba32c347b0
quickcheck fails with code generator errors only if one tester is invoked
bulwahn
parents:
45418
diff
changeset
|
176 |
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts) |
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset
|
177 |
val _ = Quickcheck.add_timing comp_time current_result |
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
|
178 |
in |
62979 | 179 |
(case test_fun of |
180 |
NONE => |
|
181 |
(Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); |
|
182 |
!current_result) |
|
45417
cae3ba9be892
removing deactivated timeout handling; catching compilation errors and only outputing an urgent message to enable parallel sucessful quickcheck compilations and runs to present their result
bulwahn
parents:
45416
diff
changeset
|
183 |
| SOME test_fun => |
62979 | 184 |
let |
185 |
val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...") |
|
186 |
fun test genuine_only enum = |
|
187 |
(case get_first (test_card_size test_fun genuine_only) enum of |
|
188 |
SOME ((card, _), (true, ts)) => |
|
189 |
Quickcheck.add_response names (nth eval_terms (card - 1)) |
|
190 |
(SOME (true, ts)) current_result |
|
191 |
| SOME ((card, size), (false, ts)) => |
|
192 |
if abort_potential then |
|
193 |
Quickcheck.add_response names (nth eval_terms (card - 1)) |
|
194 |
(SOME (false, ts)) current_result |
|
195 |
else |
|
196 |
let |
|
197 |
val (ts1, ts2) = chop (length names) ts |
|
198 |
val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1)) |
|
199 |
val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) |
|
200 |
in |
|
201 |
Quickcheck.message ctxt |
|
202 |
(Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); |
|
203 |
Quickcheck.message ctxt |
|
204 |
"Quickcheck continues to find a genuine counterexample..."; |
|
205 |
test true (snd (take_prefix (fn x => not (x = (card, size))) enum)) |
|
206 |
end |
|
207 |
| NONE => ()) |
|
208 |
in (test genuine_only enumeration_card_size; !current_result) end) |
|
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
|
209 |
end |
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
|
210 |
|
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
|
211 |
fun get_finite_types ctxt = |
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
|
212 |
fst (chop (Config.get ctxt Quickcheck.finite_type_size) |
62979 | 213 |
[@{typ Enum.finite_1}, @{typ Enum.finite_2}, @{typ Enum.finite_3}, |
214 |
@{typ Enum.finite_4}, @{typ Enum.finite_5}]) |
|
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
|
215 |
|
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
|
216 |
exception WELLSORTED of string |
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
|
217 |
|
62980 | 218 |
fun monomorphic_term ctxt insts default_T = |
219 |
(map_types o map_atyps) |
|
220 |
(fn T as TFree (v, S) => |
|
221 |
let val T' = AList.lookup (op =) insts v |> the_default default_T in |
|
222 |
if Sign.of_sort (Proof_Context.theory_of ctxt) (T', S) then T' |
|
223 |
else |
|
224 |
raise WELLSORTED ("For instantiation with default_type " ^ |
|
225 |
Syntax.string_of_typ ctxt default_T ^ ":\n" ^ Syntax.string_of_typ ctxt T' ^ |
|
226 |
" to be substituted for variable " ^ Syntax.string_of_typ ctxt T ^ |
|
227 |
" does not have sort " ^ Syntax.string_of_sort ctxt S) |
|
228 |
end |
|
229 |
| T => T) |
|
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
|
230 |
|
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
|
231 |
datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list |
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
|
232 |
|
62979 | 233 |
|
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
234 |
(* minimalistic preprocessing *) |
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
235 |
|
62979 | 236 |
fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = |
237 |
let val (a', t') = strip_all t |
|
238 |
in ((a, T) :: a', t') end |
|
239 |
| strip_all t = ([], t) |
|
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
240 |
|
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
241 |
fun preprocess ctxt t = |
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
242 |
let |
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
243 |
val thy = Proof_Context.theory_of ctxt |
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
244 |
val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of |
62979 | 245 |
val rewrs = |
246 |
map (swap o dest) @{thms all_simps} @ |
|
247 |
(map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}, |
|
248 |
@{thm bot_fun_def}, @{thm less_bool_def}]) |
|
59970 | 249 |
val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t) |
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
250 |
val (vs, body) = strip_all t' |
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
251 |
val vs' = Variable.variant_frees ctxt [t'] vs |
62979 | 252 |
in subst_bounds (map Free (rev vs'), body) end |
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
253 |
|
62979 | 254 |
|
46565 | 255 |
structure Subtype_Predicates = Generic_Data |
256 |
( |
|
257 |
type T = (term * string) list |
|
258 |
val empty = [] |
|
259 |
val extend = I |
|
46580 | 260 |
fun merge data : T = AList.merge (op =) (K true) data |
46565 | 261 |
) |
262 |
||
263 |
val register_predicate = Subtype_Predicates.map o AList.update (op =) |
|
264 |
||
265 |
fun subtype_preprocess ctxt (T, (t, ts)) = |
|
266 |
let |
|
267 |
val preds = Subtype_Predicates.get (Context.Proof ctxt) |
|
62979 | 268 |
fun matches (p $ _) = AList.defined Term.could_unify preds p |
46565 | 269 |
fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p) |
270 |
fun subst_of (tyco, v as Free (x, repT)) = |
|
271 |
let |
|
272 |
val [(info, _)] = Typedef.get_info ctxt tyco |
|
273 |
val repT' = Logic.varifyT_global (#rep_type info) |
|
62979 | 274 |
val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty |
46565 | 275 |
val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info)) |
276 |
in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end |
|
277 |
val (prems, concl) = strip_imp t |
|
278 |
val subst = map subst_of (map_filter get_match prems) |
|
279 |
val t' = Term.subst_free subst |
|
280 |
(fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl) |
|
62979 | 281 |
in (T, (t', ts)) end |
282 |
||
46565 | 283 |
|
45440
9f4d3e68ae98
adding a minimalistic preprocessing rewriting common boolean operators; tuned
bulwahn
parents:
45420
diff
changeset
|
284 |
(* instantiation of type variables with concrete types *) |
62979 | 285 |
|
62980 | 286 |
fun instantiate_goals ctxt insts goals = |
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
|
287 |
let |
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
|
288 |
fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) |
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
|
289 |
val default_insts = |
62980 | 290 |
if Config.get ctxt Quickcheck.finite_types |
62979 | 291 |
then get_finite_types else Quickcheck.default_type |
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
|
292 |
val inst_goals = |
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
|
293 |
map (fn (check_goal, eval_terms) => |
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
|
294 |
if not (null (Term.add_tfree_names check_goal [])) then |
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
|
295 |
map (fn T => |
62980 | 296 |
(pair (SOME T) o Term o apfst (preprocess ctxt)) |
297 |
(map_goal_and_eval_terms (monomorphic_term ctxt insts T) (check_goal, eval_terms)) |
|
298 |
handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts ctxt) |
|
299 |
else [(NONE, Term (preprocess ctxt check_goal, eval_terms))]) goals |
|
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
|
300 |
val error_msg = |
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
|
301 |
cat_lines |
50046 | 302 |
(maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) |
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
|
303 |
fun is_wellsorted_term (T, Term t) = SOME (T, t) |
50046 | 304 |
| is_wellsorted_term (_, Wellsorted_Error _) = NONE |
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
|
305 |
val correct_inst_goals = |
62979 | 306 |
(case map (map_filter is_wellsorted_term) inst_goals of |
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
|
307 |
[[]] => error error_msg |
62979 | 308 |
| xs => xs) |
62980 | 309 |
val _ = if Config.get ctxt Quickcheck.quiet then () else warning error_msg |
62979 | 310 |
in correct_inst_goals end |
311 |
||
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
|
312 |
|
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45687
diff
changeset
|
313 |
(* compilation of testing functions *) |
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45687
diff
changeset
|
314 |
|
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset
|
315 |
fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine = |
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset
|
316 |
let |
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset
|
317 |
val T = fastype_of then_t |
62979 | 318 |
val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T) |
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset
|
319 |
in |
62979 | 320 |
Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $ |
45761
90028fd2f1fa
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
bulwahn
parents:
45757
diff
changeset
|
321 |
(if_t $ cond $ then_t $ else_t genuine) $ |
45763
3bb2bdf654f7
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn
parents:
45761
diff
changeset
|
322 |
(if_t $ genuine_only $ none $ else_t false) |
45753
196697f71488
indicating where the restart should occur; making safe_if dynamic
bulwahn
parents:
45728
diff
changeset
|
323 |
end |
45718
8979b2463fc8
quickcheck random can also find potential counterexamples;
bulwahn
parents:
45687
diff
changeset
|
324 |
|
62980 | 325 |
fun collect_results _ [] results = results |
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
|
326 |
| collect_results f (t :: ts) results = |
62979 | 327 |
let val result = f t in |
328 |
if Quickcheck.found_counterexample result then result :: results |
|
329 |
else collect_results f ts (result :: results) |
|
330 |
end |
|
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
|
331 |
|
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
332 |
fun generator_test_goal_terms generator ctxt catch_code_errors insts goals = |
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
|
333 |
let |
46565 | 334 |
val use_subtype = Config.get ctxt Quickcheck.use_subtype |
45687
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset
|
335 |
fun add_eval_term t ts = if is_Free t then ts else ts @ [t] |
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset
|
336 |
fun add_equation_eval_terms (t, eval_terms) = |
62979 | 337 |
(case try HOLogic.dest_eq (snd (strip_imp t)) of |
45687
a07654c67f30
quickcheck does not show evaluation terms of equations if they are simply free variables to avoid duplicated output; tuned
bulwahn
parents:
45686
diff
changeset
|
338 |
SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms)) |
62979 | 339 |
| NONE => (t, eval_terms)) |
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
|
340 |
fun test_term' goal = |
62979 | 341 |
(case goal of |
46331
f5598b604a54
generalizing check if size matters because it is different for random and exhaustive testing
bulwahn
parents:
46327
diff
changeset
|
342 |
[(NONE, t)] => test_term generator ctxt catch_code_errors t |
62979 | 343 |
| ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)) |
344 |
val goals' = |
|
345 |
instantiate_goals ctxt insts goals |
|
46565 | 346 |
|> (if use_subtype then map (map (subtype_preprocess ctxt)) else I) |
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
|
347 |
|> map (map (apsnd add_equation_eval_terms)) |
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
|
348 |
in |
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
|
349 |
if Config.get ctxt Quickcheck.finite_types then |
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
|
350 |
collect_results test_term' goals' [] |
62979 | 351 |
else collect_results (test_term generator ctxt catch_code_errors) (maps (map snd) goals') [] |
352 |
end |
|
353 |
||
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
|
354 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
355 |
(* defining functions *) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
356 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
357 |
fun pat_completeness_auto ctxt = |
42793 | 358 |
Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
359 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
360 |
fun define_functions (mk_equations, termination_tac) prfx argnames names Ts = |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
361 |
if define_foundationally andalso is_some termination_tac then |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
362 |
let |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
363 |
val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
364 |
in |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
365 |
Function.add_function |
59859 | 366 |
(map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn)) |
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
367 |
(names ~~ Ts)) |
63182 | 368 |
(map (fn t => (((Binding.concealed Binding.empty, []), t), [], [])) eqs_t) |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
369 |
Function_Common.default_config pat_completeness_auto |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
370 |
#> snd |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
371 |
#> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
372 |
#> snd |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
373 |
end |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
374 |
else |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
375 |
fold_map (fn (name, T) => Local_Theory.define |
59859 | 376 |
((Binding.concealed (Binding.name name), NoSyn), |
377 |
(apfst Binding.concealed Attrib.empty_binding, mk_undefined T)) |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
378 |
#> apfst fst) (names ~~ Ts) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
379 |
#> (fn (consts, lthy) => |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
380 |
let |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
381 |
val eqs_t = mk_equations consts |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
382 |
val eqs = map (fn eq => Goal.prove lthy argnames [] eq |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset
|
383 |
(fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))) eqs_t |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
384 |
in |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
385 |
fold (fn (name, eq) => Local_Theory.note |
47204
6212bcc94bb0
refine bindings in quickcheck_common: do not conceal and do not declare as simps
bulwahn
parents:
46674
diff
changeset
|
386 |
((Binding.qualify true prfx |
6212bcc94bb0
refine bindings in quickcheck_common: do not conceal and do not declare as simps
bulwahn
parents:
46674
diff
changeset
|
387 |
(Binding.qualify true name (Binding.name "simps")), |
6212bcc94bb0
refine bindings in quickcheck_common: do not conceal and do not declare as simps
bulwahn
parents:
46674
diff
changeset
|
388 |
[Code.add_default_eqn_attrib]), [eq]) #> snd) |
45592 | 389 |
(names ~~ eqs) lthy |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
390 |
end) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
391 |
|
62979 | 392 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
393 |
(** ensuring sort constraints **) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
394 |
|
62979 | 395 |
type instantiation = |
396 |
Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list -> |
|
397 |
string list -> string -> string list * string list -> typ list * typ list -> theory -> theory |
|
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
398 |
|
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
399 |
fun perhaps_constrain thy insts raw_vs = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
400 |
let |
62979 | 401 |
fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT_global T, sort) |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
402 |
val vtab = Vartab.empty |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
403 |
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs |
62979 | 404 |
|> fold meet insts |
405 |
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) end |
|
406 |
handle Sorts.CLASS_ERROR _ => NONE |
|
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
407 |
|
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
408 |
fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy = |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
409 |
let |
62979 | 410 |
val algebra = Sign.classes_of thy |
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
411 |
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
412 |
val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs |
56375
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
51552
diff
changeset
|
413 |
fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd) |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57996
diff
changeset
|
414 |
(Old_Datatype_Aux.interpret_construction descr vs constr) |
56375
32e0da92c786
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
blanchet
parents:
51552
diff
changeset
|
415 |
val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] } |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
416 |
@ insts_of aux_sort { atyp = K [], dtyp = K o K } |
62979 | 417 |
val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos |
418 |
in |
|
419 |
if has_inst then thy |
|
420 |
else |
|
421 |
(case perhaps_constrain thy insts vs of |
|
422 |
SOME constrain => |
|
423 |
instantiate config descr |
|
424 |
(map constrain vs) tycos prfx (names, auxnames) |
|
425 |
((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy |
|
426 |
| NONE => thy) |
|
427 |
end |
|
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
428 |
|
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
429 |
fun ensure_common_sort_datatype (sort, instantiate) = |
58145
3cfbb68ad2e0
ported Quickcheck to support new datatypes better
blanchet
parents:
58112
diff
changeset
|
430 |
ensure_sort (((@{sort typerep}, @{sort term_of}), sort), |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58186
diff
changeset
|
431 |
(fn thy => BNF_LFP_Compat.the_descr thy compat_prefs, instantiate)) |
45923
473b744c23f2
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
bulwahn
parents:
45921
diff
changeset
|
432 |
|
58186 | 433 |
fun datatype_interpretation name = |
58354
04ac60da613e
support (finite values of) codatatypes in Quickcheck
blanchet
parents:
58186
diff
changeset
|
434 |
BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype |
62979 | 435 |
|
436 |
||
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
437 |
(** generic parametric compilation **) |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
438 |
|
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
439 |
fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts = |
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
440 |
let |
62979 | 441 |
val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T) |
442 |
fun mk_if (index, (t, eval_terms)) else_t = |
|
443 |
if_t $ (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $ |
|
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
444 |
(mk_generator_expr ctxt (t, eval_terms)) $ else_t |
62979 | 445 |
in absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) end |
446 |
||
42159
234ec7011e5d
generalizing compilation scheme of quickcheck generators to multiple arguments; changing random and exhaustive tester to use one code invocation for polymorphic instances with multiple cardinalities
bulwahn
parents:
42110
diff
changeset
|
447 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
448 |
(** post-processing of function terms **) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
449 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
450 |
fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2)) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
451 |
| dest_fun_upd t = raise TERM ("dest_fun_upd", [t]) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
452 |
|
62979 | 453 |
fun mk_fun_upd T1 T2 (t1, t2) t = |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
454 |
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2 |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
455 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
456 |
fun dest_fun_upds t = |
62979 | 457 |
(case try dest_fun_upd t of |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
458 |
NONE => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
459 |
(case t of |
62979 | 460 |
Abs (_, _, _) => ([], t) |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
461 |
| _ => raise TERM ("dest_fun_upds", [t])) |
62979 | 462 |
| SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)) |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
463 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
464 |
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
465 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
466 |
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool}) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
467 |
| make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
468 |
| make_set T1 ((t1, @{const True}) :: tps) = |
62979 | 469 |
Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) $ |
470 |
t1 $ (make_set T1 tps) |
|
50046 | 471 |
| make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t]) |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
472 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
473 |
fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool}) |
62979 | 474 |
| make_coset T tps = |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
475 |
let |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
476 |
val U = T --> @{typ bool} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
477 |
fun invert @{const False} = @{const True} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
478 |
| invert @{const True} = @{const False} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
479 |
in |
62979 | 480 |
Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) $ |
481 |
Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
482 |
end |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
483 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
484 |
fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
485 |
| make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
486 |
| make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) |
62979 | 487 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
488 |
fun post_process_term t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
489 |
let |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
490 |
fun map_Abs f t = |
62979 | 491 |
(case t of |
492 |
Abs (x, T, t') => Abs (x, T, f t') |
|
493 |
| _ => raise TERM ("map_Abs", [t])) |
|
494 |
fun process_args t = |
|
495 |
(case strip_comb t of |
|
496 |
(c as Const (_, _), ts) => list_comb (c, map post_process_term ts)) |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
497 |
in |
62979 | 498 |
(case fastype_of t of |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
499 |
Type (@{type_name fun}, [T1, T2]) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
500 |
(case try dest_fun_upds t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
501 |
SOME (tps, t) => |
62979 | 502 |
(map (apply2 post_process_term) tps, map_Abs post_process_term t) |> |
503 |
(case T2 of |
|
504 |
@{typ bool} => |
|
505 |
(case t of |
|
506 |
Abs(_, _, @{const False}) => fst #> rev #> make_set T1 |
|
507 |
| Abs(_, _, @{const True}) => fst #> rev #> make_coset T1 |
|
508 |
| Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1 |
|
509 |
| _ => raise TERM ("post_process_term", [t])) |
|
510 |
| Type (@{type_name option}, _) => |
|
511 |
(case t of |
|
512 |
Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2 |
|
513 |
| Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2 |
|
514 |
| _ => make_fun_upds T1 T2) |
|
515 |
| _ => make_fun_upds T1 T2) |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
516 |
| NONE => process_args t) |
62979 | 517 |
| _ => process_args t) |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
518 |
end |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
519 |
|
62979 | 520 |
end |