45925
|
1 |
(* Title: HOL/Tools/Quickcheck/abstract_generators.ML
|
|
2 |
Author: Lukas Bulwahn, TU Muenchen
|
|
3 |
|
|
4 |
Quickcheck generators for abstract types.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature ABSTRACT_GENERATORS =
|
|
8 |
sig
|
|
9 |
val quickcheck_generator : string -> term list -> theory -> theory
|
|
10 |
end;
|
|
11 |
|
|
12 |
structure Abstract_Generators : ABSTRACT_GENERATORS =
|
|
13 |
struct
|
|
14 |
|
|
15 |
fun check_constrs ctxt tyco constrs =
|
|
16 |
let
|
|
17 |
fun check_type c =
|
|
18 |
case try (dest_Type o body_type o fastype_of) c of
|
|
19 |
NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
|
|
20 |
| SOME (tyco', vs) => if not (tyco' = tyco) then
|
|
21 |
error (Syntax.string_of_term ctxt c ^ " has mismatching result type. " ^
|
|
22 |
"Expected type constructor " ^ quote tyco ^ ", but found " ^ quote tyco' ^ ".")
|
|
23 |
else
|
|
24 |
case try (map dest_TFree) vs of
|
|
25 |
NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
|
|
26 |
| SOME _ => ()
|
|
27 |
in
|
|
28 |
map check_type constrs
|
|
29 |
end
|
|
30 |
|
|
31 |
fun gen_quickcheck_generator prep_tyco prep_term tyco_raw constrs_raw thy =
|
|
32 |
let
|
|
33 |
val ctxt = Proof_Context.init_global thy
|
|
34 |
val tyco = prep_tyco ctxt tyco_raw
|
|
35 |
val constrs = map (prep_term ctxt) constrs_raw
|
|
36 |
val _ = check_constrs ctxt tyco constrs
|
|
37 |
val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
|
|
38 |
val name = Long_Name.base_name tyco
|
|
39 |
fun mk_dconstrs (Const (s, T)) =
|
|
40 |
(s, map (Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
|
|
41 |
| mk_dconstrs t = error (Syntax.string_of_term ctxt t ^
|
|
42 |
" is not a valid constructor for quickcheck_generator, which expects a constant.")
|
|
43 |
fun the_descr thy _ =
|
|
44 |
let
|
|
45 |
val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
|
|
46 |
in
|
|
47 |
(descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], []))
|
|
48 |
end
|
|
49 |
in
|
|
50 |
Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}),
|
|
51 |
(the_descr, Exhaustive_Generators.instantiate_full_exhaustive_datatype))
|
|
52 |
Datatype_Aux.default_config [tyco] thy
|
|
53 |
end
|
|
54 |
|
|
55 |
val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
|
|
56 |
|
|
57 |
val quickcheck_generator_cmd = gen_quickcheck_generator
|
|
58 |
(fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
|
|
59 |
|
|
60 |
val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
|
|
61 |
Keyword.thy_decl (Parse.type_const -- (Args.$$$ "constructors" |-- Parse.$$$ ":" |-- Parse.list1 Parse.term)
|
|
62 |
>> (fn (tyco, constrs) => Toplevel.theory (quickcheck_generator_cmd tyco constrs)))
|
|
63 |
|
|
64 |
end; |