author | bulwahn |
Wed, 09 Nov 2011 11:34:53 +0100 | |
changeset 45416 | cf31fe74b05a |
parent 45159 | 3f1d1ce024cb |
child 45417 | cae3ba9be892 |
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 |
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
9 |
val strip_imp : term -> (term list * term) |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
10 |
val define_functions : ((term list -> term list) * (Proof.context -> tactic) option) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
11 |
-> 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
|
12 |
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
|
13 |
-> (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
|
14 |
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
|
15 |
-> (typ option * (term * term list)) 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
|
16 |
val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result 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 |
type compile_generator = |
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
|
18 |
Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option |
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
|
19 |
val generator_test_goal_terms : compile_generator -> Proof.context -> bool * bool |
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
|
20 |
-> (string * typ) list -> (term * term list) list -> Quickcheck.result list |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
21 |
val ensure_sort_datatype: |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
22 |
((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
23 |
-> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory) |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
24 |
-> Datatype.config -> string list -> 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
|
25 |
val gen_mk_parametric_generator_expr : |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
26 |
(((Proof.context -> term * term list -> term) * term) * typ) |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
27 |
-> Proof.context -> (term * term list) list -> term |
45039
632a033616e9
adding post-processing of terms to narrowing-based Quickcheck
bulwahn
parents:
44241
diff
changeset
|
28 |
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
|
29 |
val post_process_term : term -> term |
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
|
30 |
val test_term : compile_generator -> Proof.context -> bool * bool -> term * term list -> Quickcheck.result |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
31 |
end; |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
32 |
|
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
33 |
structure Quickcheck_Common : QUICKCHECK_COMMON = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
34 |
struct |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
35 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
36 |
(* static options *) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
37 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
38 |
val define_foundationally = false |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
39 |
|
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
40 |
(* 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
|
41 |
|
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
42 |
fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B) |
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
43 |
| 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
|
44 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
45 |
fun mk_undefined T = Const(@{const_name undefined}, 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
|
46 |
|
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
|
47 |
(* 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
|
48 |
|
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
|
49 |
type compile_generator = |
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
|
50 |
Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option |
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
|
51 |
|
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
|
52 |
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
|
53 |
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
|
54 |
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse |
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
|
55 |
error "Term to be tested contains type variables"; |
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
|
56 |
val _ = null (Term.add_vars t []) orelse |
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
|
57 |
error "Term to be tested contains schematic variables"; |
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
|
58 |
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
|
59 |
|
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
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
|
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
|
64 |
fun test_term compile ctxt (limit_time, is_interactive) (t, 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
|
65 |
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
|
66 |
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
|
67 |
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
|
68 |
val current_size = Unsynchronized.ref 0 |
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
|
69 |
val current_result = Unsynchronized.ref Quickcheck.empty_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
|
70 |
fun excipit () = |
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
|
71 |
"Quickcheck ran out of time while testing at size " ^ string_of_int (!current_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
|
72 |
fun with_size test_fun k = |
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 |
if k > Config.get ctxt Quickcheck.size 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
|
74 |
NONE |
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 |
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
|
76 |
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
|
77 |
val _ = Quickcheck.message ctxt ("Test data size: " ^ string_of_int k) |
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
|
78 |
val _ = current_size := k |
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
|
79 |
val ((result, report), 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
|
80 |
cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1]) |
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
|
81 |
val _ = Quickcheck.add_timing timing 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
|
82 |
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
|
83 |
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
|
84 |
case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q |
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 |
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
|
86 |
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
|
87 |
(*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( |
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
|
88 |
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
|
89 |
val (test_fun, comp_time) = cpu_time "quickcheck compilation" |
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
|
90 |
(fn () => compile ctxt [(t, 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
|
91 |
val _ = Quickcheck.add_timing comp_time 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
|
92 |
val (response, exec_time) = |
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 |
cpu_time "quickcheck execution" (fn () => with_size test_fun 1) |
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 _ = Quickcheck.add_response names eval_terms response 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
|
95 |
val _ = Quickcheck.add_timing exec_time 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
|
96 |
in !current_result 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
|
97 |
(* (fn () => (message (excipit ()); !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
|
98 |
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
|
99 |
|
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
|
100 |
fun validate_terms ctxt 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
|
101 |
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
|
102 |
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
|
103 |
val size = 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
|
104 |
val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" |
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
|
105 |
(fn () => Quickcheck.mk_batch_validator ctxt 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
|
106 |
fun with_size tester k = |
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 |
if k > size then true |
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
|
108 |
else if tester k then with_size tester (k + 1) else false |
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
|
109 |
val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => |
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
|
110 |
Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) |
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
|
111 |
(fn () => with_size test_fun 1) () |
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
|
112 |
handle TimeLimit.TimeOut => true)) test_funs) |
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
|
113 |
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
|
114 |
(results, [comp_time, exec_time]) |
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 |
end |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
116 |
|
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
|
117 |
fun test_terms ctxt 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
|
118 |
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
|
119 |
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
|
120 |
val size = 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
|
121 |
val namess = map (fn t => Term.add_free_names t []) 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
|
122 |
val (test_funs, comp_time) = |
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
|
123 |
cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt 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
|
124 |
fun with_size tester k = |
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
|
125 |
if k > size then NONE |
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
|
126 |
else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) |
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
|
127 |
val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => |
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
|
128 |
Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) |
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
|
129 |
(fn () => with_size test_fun 1) () |
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
|
130 |
handle TimeLimit.TimeOut => NONE)) test_funs) |
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
|
131 |
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
|
132 |
(Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results, |
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
|
133 |
[comp_time, exec_time]) |
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 |
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
|
135 |
|
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
|
136 |
|
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
|
137 |
fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) 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
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
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
|
143 |
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
|
144 |
val current_result = Unsynchronized.ref Quickcheck.empty_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
|
145 |
fun test_card_size test_fun (card, 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
|
146 |
(* FIXME: why decrement size by one? *) |
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
|
147 |
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
|
148 |
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
|
149 |
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) |
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 |
(fn () => fst (test_fun [card, size - 1])) |
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
|
151 |
val _ = Quickcheck.add_timing timing 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
|
152 |
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
|
153 |
Option.map (pair card) 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
|
154 |
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
|
155 |
val enumeration_card_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
|
156 |
if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts 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
|
157 |
(* size does not matter *) |
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 |
map (rpair 0) (1 upto (length 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
|
159 |
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
|
160 |
(* size does matter *) |
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
|
161 |
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
|
162 |
|> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) |
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
|
163 |
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
|
164 |
(*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( |
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 |
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
|
166 |
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt 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
|
167 |
val _ = Quickcheck.add_timing comp_time 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
|
168 |
val _ = case get_first (test_card_size test_fun) enumeration_card_size of |
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
|
169 |
SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) 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
|
170 |
| NONE => () |
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
|
171 |
in !current_result 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
|
172 |
(*(fn () => (message "Quickcheck ran out of time"; !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
|
173 |
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
|
174 |
|
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
|
175 |
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
|
176 |
fst (chop (Config.get ctxt Quickcheck.finite_type_size) |
45416 | 177 |
[@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"}, |
178 |
@{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
|
179 |
|
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
|
180 |
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
|
181 |
|
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
|
182 |
fun monomorphic_term thy insts default_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
|
183 |
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
|
184 |
fun subst (T as TFree (v, S)) = |
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
|
185 |
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
|
186 |
val T' = AList.lookup (op =) insts v |
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
|
187 |
|> the_default default_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
|
188 |
in if Sign.of_sort thy (T', S) then 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
|
189 |
else raise (WELLSORTED ("For instantiation with default_type " ^ |
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
|
190 |
Syntax.string_of_typ_global thy default_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
|
191 |
":\n" ^ Syntax.string_of_typ_global thy 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
|
192 |
" to be substituted for variable " ^ |
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
|
193 |
Syntax.string_of_typ_global thy T ^ " does not have sort " ^ |
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
|
194 |
Syntax.string_of_sort_global thy S)) |
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
|
195 |
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
|
196 |
| subst T = 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
|
197 |
in (map_types o map_atyps) subst 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
|
198 |
|
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
|
199 |
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
|
200 |
|
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
|
201 |
fun instantiate_goals lthy insts 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
|
202 |
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
|
203 |
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
|
204 |
val thy = Proof_Context.theory_of lthy |
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
|
205 |
val default_insts = |
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
|
206 |
if Config.get lthy Quickcheck.finite_types then (get_finite_types lthy) else (Quickcheck.default_type lthy) |
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
|
207 |
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
|
208 |
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
|
209 |
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
|
210 |
map (fn 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
|
211 |
(pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy)) |
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 |
(map_goal_and_eval_terms (monomorphic_term thy insts T) (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
|
213 |
handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts |
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
|
214 |
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
|
215 |
[(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) 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
|
216 |
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
|
217 |
cat_lines |
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
|
218 |
(maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) 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
|
219 |
fun is_wellsorted_term (T, Term t) = SOME (T, 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
|
220 |
| is_wellsorted_term (_, Wellsorted_Error s) = NONE |
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
|
221 |
val correct_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
|
222 |
case map (map_filter is_wellsorted_term) inst_goals of |
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
|
223 |
[[]] => error 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
|
224 |
| xs => xs |
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
|
225 |
val _ = if Config.get lthy Quickcheck.quiet then () else warning 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
|
226 |
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
|
227 |
correct_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
|
228 |
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
|
229 |
|
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 |
fun collect_results f [] results = results |
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 |
| collect_results f (t :: ts) results = |
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 |
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
|
233 |
val result = f 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
|
234 |
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
|
235 |
if Quickcheck.found_counterexample result 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
|
236 |
(result :: results) |
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
|
237 |
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
|
238 |
collect_results f ts (result :: results) |
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
|
239 |
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
|
240 |
|
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
|
241 |
fun add_equation_eval_terms (t, 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
|
242 |
case try HOLogic.dest_eq (snd (strip_imp t)) of |
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
|
243 |
SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs]) |
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
|
244 |
| NONE => (t, 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
|
245 |
|
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
|
246 |
fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts 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
|
247 |
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
|
248 |
fun test_term' goal = |
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
|
249 |
case goal of |
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
|
250 |
[(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) 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
|
251 |
| ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd 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
|
252 |
val goals' = instantiate_goals ctxt insts 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
|
253 |
|> 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
|
254 |
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
|
255 |
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
|
256 |
collect_results test_term' 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
|
257 |
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
|
258 |
collect_results (test_term compile ctxt (limit_time, is_interactive)) |
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
|
259 |
(maps (map snd) 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
|
260 |
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
|
261 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
262 |
(* defining functions *) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
263 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
264 |
fun pat_completeness_auto ctxt = |
42793 | 265 |
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
|
266 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
267 |
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
|
268 |
if define_foundationally andalso is_some termination_tac then |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
269 |
let |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
270 |
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
|
271 |
in |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
272 |
Function.add_function |
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
273 |
(map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn)) |
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
274 |
(names ~~ Ts)) |
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
275 |
(map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t) |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
276 |
Function_Common.default_config pat_completeness_auto |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
277 |
#> snd |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
278 |
#> Local_Theory.restore |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
279 |
#> (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
|
280 |
#> snd |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
281 |
end |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
282 |
else |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
283 |
fold_map (fn (name, T) => Local_Theory.define |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
284 |
((Binding.conceal (Binding.name name), NoSyn), |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
285 |
(apfst Binding.conceal Attrib.empty_binding, mk_undefined T)) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
286 |
#> apfst fst) (names ~~ Ts) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
287 |
#> (fn (consts, lthy) => |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
288 |
let |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
289 |
val eqs_t = mk_equations consts |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
290 |
val eqs = map (fn eq => Goal.prove lthy argnames [] eq |
42361 | 291 |
(fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t |
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
292 |
in |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
293 |
fold (fn (name, eq) => Local_Theory.note |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
294 |
((Binding.conceal (Binding.qualify true prfx |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
295 |
(Binding.qualify true name (Binding.name "simps"))), |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
296 |
Code.add_default_eqn_attrib :: map (Attrib.internal o K) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
297 |
[Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (names ~~ eqs) lthy |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
298 |
end) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
299 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
300 |
(** ensuring sort constraints **) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
301 |
|
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
302 |
fun perhaps_constrain thy insts raw_vs = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
303 |
let |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
304 |
fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
305 |
(Logic.varifyT_global T, sort); |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
306 |
val vtab = Vartab.empty |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
307 |
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
308 |
|> fold meet insts; |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
309 |
in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
310 |
end handle Sorts.CLASS_ERROR _ => NONE; |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
311 |
|
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
312 |
fun ensure_sort_datatype (((sort_vs, aux_sort), sort), instantiate_datatype) config raw_tycos thy = |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
313 |
let |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
314 |
val algebra = Sign.classes_of thy; |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
315 |
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = Datatype.the_descr thy raw_tycos |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
316 |
val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
317 |
fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd) |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
318 |
(Datatype_Aux.interpret_construction descr vs constr) |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
319 |
val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] } |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
320 |
@ insts_of aux_sort { atyp = K [], dtyp = K o K } |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
321 |
val has_inst = exists (fn tyco => can (Sorts.mg_domain algebra tyco) sort) tycos; |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
322 |
in if has_inst then thy |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
323 |
else case perhaps_constrain thy insts vs |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
324 |
of SOME constrain => instantiate_datatype config descr |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
325 |
(map constrain vs) tycos prfx (names, auxnames) |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
326 |
((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
327 |
| NONE => thy |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
328 |
end; |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
329 |
|
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
|
330 |
(** 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
|
331 |
|
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
|
332 |
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
|
333 |
let |
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
|
334 |
val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) |
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
|
335 |
fun mk_if (index, (t, eval_terms)) else_t = |
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
|
336 |
if_t $ (HOLogic.eq_const @{typ code_numeral} $ Bound 0 $ HOLogic.mk_number @{typ code_numeral} index) $ |
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
|
337 |
(mk_generator_expr ctxt (t, eval_terms)) $ else_t |
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
|
338 |
in |
44241 | 339 |
absdummy @{typ "code_numeral"} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) |
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
|
340 |
end |
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
|
341 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
342 |
(** post-processing of function terms **) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
343 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
344 |
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
|
345 |
| 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
|
346 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
347 |
fun mk_fun_upd T1 T2 (t1, t2) t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
348 |
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
|
349 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
350 |
fun dest_fun_upds t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
351 |
case try dest_fun_upd t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
352 |
NONE => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
353 |
(case t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
354 |
Abs (_, _, _) => ([], t) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
355 |
| _ => raise TERM ("dest_fun_upds", [t])) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
356 |
| SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
357 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
358 |
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
|
359 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
360 |
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
|
361 |
| 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
|
362 |
| make_set T1 ((t1, @{const True}) :: tps) = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
363 |
Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
364 |
$ t1 $ (make_set T1 tps) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
365 |
| make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t]) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
366 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
367 |
fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool}) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
368 |
| make_coset T tps = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
369 |
let |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
370 |
val U = T --> @{typ bool} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
371 |
fun invert @{const False} = @{const True} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
372 |
| invert @{const True} = @{const False} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
373 |
in |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
374 |
Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
375 |
$ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
376 |
end |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
377 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
378 |
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
|
379 |
| 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
|
380 |
| make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
381 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
382 |
fun post_process_term t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
383 |
let |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
384 |
fun map_Abs f t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
385 |
case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
386 |
fun process_args t = case strip_comb t of |
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
387 |
(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
|
388 |
in |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
389 |
case fastype_of t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
390 |
Type (@{type_name fun}, [T1, T2]) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
391 |
(case try dest_fun_upds t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
392 |
SOME (tps, t) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
393 |
(map (pairself post_process_term) tps, map_Abs post_process_term t) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
394 |
|> (case T2 of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
395 |
@{typ bool} => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
396 |
(case t of |
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
397 |
Abs(_, _, @{const False}) => fst #> rev #> make_set T1 |
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
398 |
| Abs(_, _, @{const True}) => fst #> rev #> make_coset T1 |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
399 |
| Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1 |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
400 |
| _ => raise TERM ("post_process_term", [t])) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
401 |
| Type (@{type_name option}, _) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
402 |
(case t of |
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
403 |
Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2 |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
404 |
| Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2 |
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
405 |
| _ => make_fun_upds T1 T2) |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
406 |
| _ => make_fun_upds T1 T2) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
407 |
| NONE => process_args t) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
408 |
| _ => process_args t |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
409 |
end |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
410 |
|
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
411 |
|
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
412 |
end; |