author | wenzelm |
Fri, 13 May 2011 22:55:00 +0200 | |
changeset 42793 | 88bee9f6eec7 |
parent 42361 | 23f352990944 |
child 44241 | 7943b69f0188 |
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 |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
14 |
val ensure_sort_datatype: |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
15 |
((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
16 |
-> 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
|
17 |
-> 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
|
18 |
val gen_mk_parametric_generator_expr : |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
19 |
(((Proof.context -> term * term list -> term) * term) * typ) |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
20 |
-> Proof.context -> (term * term list) list -> term |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
21 |
val post_process_term : term -> term |
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
22 |
end; |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
23 |
|
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
24 |
structure Quickcheck_Common : QUICKCHECK_COMMON = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
25 |
struct |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
26 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
27 |
(* static options *) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
28 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
29 |
val define_foundationally = false |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
30 |
|
42195
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
31 |
(* 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
|
32 |
|
1e7b62c93f5d
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
bulwahn
parents:
42159
diff
changeset
|
33 |
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
|
34 |
| 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
|
35 |
|
42214
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
36 |
fun mk_undefined T = Const(@{const_name undefined}, T) |
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 |
(* defining functions *) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
39 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
40 |
fun pat_completeness_auto ctxt = |
42793 | 41 |
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
|
42 |
|
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
43 |
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
|
44 |
if define_foundationally andalso is_some termination_tac then |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
45 |
let |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
46 |
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
|
47 |
in |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
48 |
Function.add_function |
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
49 |
(map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn)) |
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
50 |
(names ~~ Ts)) |
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
42229
diff
changeset
|
51 |
(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
|
52 |
Function_Common.default_config pat_completeness_auto |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
53 |
#> snd |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
54 |
#> Local_Theory.restore |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
55 |
#> (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
|
56 |
#> snd |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
57 |
end |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
58 |
else |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
59 |
fold_map (fn (name, T) => Local_Theory.define |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
60 |
((Binding.conceal (Binding.name name), NoSyn), |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
61 |
(apfst Binding.conceal Attrib.empty_binding, mk_undefined T)) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
62 |
#> apfst fst) (names ~~ Ts) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
63 |
#> (fn (consts, lthy) => |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
64 |
let |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
65 |
val eqs_t = mk_equations consts |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
66 |
val eqs = map (fn eq => Goal.prove lthy argnames [] eq |
42361 | 67 |
(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
|
68 |
in |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
69 |
fold (fn (name, eq) => Local_Theory.note |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
70 |
((Binding.conceal (Binding.qualify true prfx |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
71 |
(Binding.qualify true name (Binding.name "simps"))), |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
72 |
Code.add_default_eqn_attrib :: map (Attrib.internal o K) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
73 |
[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
|
74 |
end) |
9ca13615c619
refactoring generator definition in quickcheck and removing clone
bulwahn
parents:
42195
diff
changeset
|
75 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
76 |
(** ensuring sort constraints **) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
77 |
|
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
78 |
fun perhaps_constrain thy insts raw_vs = |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
79 |
let |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
80 |
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
|
81 |
(Logic.varifyT_global T, sort); |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
82 |
val vtab = Vartab.empty |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
83 |
|> 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
|
84 |
|> fold meet insts; |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
85 |
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
|
86 |
end handle Sorts.CLASS_ERROR _ => NONE; |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
87 |
|
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
88 |
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
|
89 |
let |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
90 |
val algebra = Sign.classes_of thy; |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
(Datatype_Aux.interpret_construction descr vs constr) |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
95 |
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
|
96 |
@ insts_of aux_sort { atyp = K [], dtyp = K o K } |
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
97 |
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
|
98 |
in if has_inst then thy |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
99 |
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
|
100 |
of SOME constrain => instantiate_datatype config descr |
42229
1491b7209e76
generalizing ensure_sort_datatype for bounded_forall instances
bulwahn
parents:
42214
diff
changeset
|
101 |
(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
|
102 |
((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
|
103 |
| NONE => thy |
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
104 |
end; |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
105 |
|
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
|
106 |
(** 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
|
107 |
|
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
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
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
|
113 |
(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
|
114 |
in |
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
|
115 |
absdummy (@{typ "code_numeral"}, fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) |
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
|
116 |
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
|
117 |
|
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
118 |
(** post-processing of function terms **) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
119 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
120 |
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
|
121 |
| 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
|
122 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
123 |
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
|
124 |
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
|
125 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
126 |
fun dest_fun_upds t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
127 |
case try dest_fun_upd t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
128 |
NONE => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
129 |
(case t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
130 |
Abs (_, _, _) => ([], t) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
131 |
| _ => raise TERM ("dest_fun_upds", [t])) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
132 |
| 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
|
133 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
134 |
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
|
135 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
136 |
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
|
137 |
| 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
|
138 |
| make_set T1 ((t1, @{const True}) :: tps) = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
139 |
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
|
140 |
$ t1 $ (make_set T1 tps) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
141 |
| 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
|
142 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
143 |
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
|
144 |
| make_coset T tps = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
145 |
let |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
146 |
val U = T --> @{typ bool} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
147 |
fun invert @{const False} = @{const True} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
148 |
| invert @{const True} = @{const False} |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
149 |
in |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
150 |
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
|
151 |
$ 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
|
152 |
end |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
153 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
154 |
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
|
155 |
| 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
|
156 |
| 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
|
157 |
|
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
158 |
fun post_process_term t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
159 |
let |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
160 |
fun map_Abs f t = |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
161 |
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
|
162 |
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
|
163 |
(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
|
164 |
in |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
165 |
case fastype_of t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
166 |
Type (@{type_name fun}, [T1, T2]) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
167 |
(case try dest_fun_upds t of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
168 |
SOME (tps, t) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
169 |
(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
|
170 |
|> (case T2 of |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
171 |
@{typ bool} => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
172 |
(case t of |
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
173 |
Abs(_, _, @{const False}) => fst #> rev #> make_set T1 |
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
174 |
| 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
|
175 |
| 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
|
176 |
| _ => raise TERM ("post_process_term", [t])) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
177 |
| Type (@{type_name option}, _) => |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
178 |
(case t of |
42110
17e0cd9bc259
fixed postprocessing for term presentation in quickcheck; tuned spacing
bulwahn
parents:
41938
diff
changeset
|
179 |
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
|
180 |
| 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
|
181 |
| _ => make_fun_upds T1 T2) |
41935
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
182 |
| _ => make_fun_upds T1 T2) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
183 |
| NONE => process_args t) |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
184 |
| _ => process_args t |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
185 |
end |
d786a8a3dc47
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn
parents:
41927
diff
changeset
|
186 |
|
41927
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
187 |
|
8759e9d043f9
adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn
parents:
diff
changeset
|
188 |
end; |