|
1 (* Title: HOL/Tools/Quickcheck/quickcheck_common.ML |
|
2 Author: Florian Haftmann, Lukas Bulwahn, TU Muenchen |
|
3 |
|
4 Common functions for quickcheck's generators |
|
5 |
|
6 *) |
|
7 |
|
8 signature QUICKCHECK_COMMON = |
|
9 sig |
|
10 val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list |
|
11 -> (string * sort -> string * sort) option |
|
12 val ensure_sort_datatype: |
|
13 sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string -> |
|
14 string list * string list -> typ list * typ list -> theory -> theory) |
|
15 -> Datatype.config -> string list -> theory -> theory |
|
16 end; |
|
17 |
|
18 structure Quickcheck_Common : QUICKCHECK_COMMON = |
|
19 struct |
|
20 |
|
21 fun perhaps_constrain thy insts raw_vs = |
|
22 let |
|
23 fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) |
|
24 (Logic.varifyT_global T, sort); |
|
25 val vtab = Vartab.empty |
|
26 |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs |
|
27 |> fold meet insts; |
|
28 in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) |
|
29 end handle Sorts.CLASS_ERROR _ => NONE; |
|
30 |
|
31 fun ensure_sort_datatype (sort, instantiate_datatype) config raw_tycos thy = |
|
32 let |
|
33 val algebra = Sign.classes_of thy; |
|
34 val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = |
|
35 Datatype.the_descr thy raw_tycos; |
|
36 val typerep_vs = (map o apsnd) |
|
37 (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs; |
|
38 val sort_insts = (map (rpair sort) o flat o maps snd o maps snd) |
|
39 (Datatype_Aux.interpret_construction descr typerep_vs |
|
40 { atyp = single, dtyp = (K o K o K) [] }); |
|
41 val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd) |
|
42 (Datatype_Aux.interpret_construction descr typerep_vs |
|
43 { atyp = K [], dtyp = K o K }); |
|
44 val has_inst = exists (fn tyco => |
|
45 can (Sorts.mg_domain algebra tyco) sort) tycos; |
|
46 in if has_inst then thy |
|
47 else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs |
|
48 of SOME constrain => instantiate_datatype config descr |
|
49 (map constrain typerep_vs) tycos prfx (names, auxnames) |
|
50 ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy |
|
51 | NONE => thy |
|
52 end; |
|
53 |
|
54 end; |