author | wenzelm |
Fri, 16 Mar 2012 18:20:12 +0100 | |
changeset 46961 | 5c6955f487e5 |
parent 46949 | 94aa7b81bcf6 |
child 55951 | c07d184aebe9 |
permissions | -rw-r--r-- |
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 |
|
46564
daa915508f63
adding parsing of an optional predicate with quickcheck_generator command
bulwahn
parents:
45940
diff
changeset
|
9 |
val quickcheck_generator : string -> term option -> term list -> theory -> theory |
45925 | 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 |
||
46564
daa915508f63
adding parsing of an optional predicate with quickcheck_generator command
bulwahn
parents:
45940
diff
changeset
|
31 |
fun gen_quickcheck_generator prep_tyco prep_term tyco_raw opt_pred_raw constrs_raw thy = |
45925 | 32 |
let |
33 |
val ctxt = Proof_Context.init_global thy |
|
34 |
val tyco = prep_tyco ctxt tyco_raw |
|
46565 | 35 |
val opt_pred = Option.map (prep_term ctxt) opt_pred_raw |
45925 | 36 |
val constrs = map (prep_term ctxt) constrs_raw |
46565 | 37 |
val _ = check_constrs ctxt tyco constrs |
45925 | 38 |
val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs))))) |
39 |
val name = Long_Name.base_name tyco |
|
40 |
fun mk_dconstrs (Const (s, T)) = |
|
41 |
(s, map (Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T)) |
|
42 |
| mk_dconstrs t = error (Syntax.string_of_term ctxt t ^ |
|
43 |
" is not a valid constructor for quickcheck_generator, which expects a constant.") |
|
46564
daa915508f63
adding parsing of an optional predicate with quickcheck_generator command
bulwahn
parents:
45940
diff
changeset
|
44 |
fun the_descr _ _ = |
45925 | 45 |
let |
46 |
val descr = [(0, (tyco, map Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))] |
|
47 |
in |
|
48 |
(descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], [])) |
|
49 |
end |
|
45940
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
50 |
fun ensure_sort (sort, instantiate) = |
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
51 |
Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), sort), |
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
52 |
(the_descr, instantiate)) |
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
53 |
Datatype_Aux.default_config [tyco] |
45925 | 54 |
in |
45940
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
55 |
thy |
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
56 |
|> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype) |
46565 | 57 |
|> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype) |
45940
71970a26a269
quickcheck_generator command also creates random generators
bulwahn
parents:
45925
diff
changeset
|
58 |
|> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype) |
46565 | 59 |
|> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco))) |
45925 | 60 |
end |
61 |
||
62 |
val quickcheck_generator = gen_quickcheck_generator (K I) (K I) |
|
63 |
||
64 |
val quickcheck_generator_cmd = gen_quickcheck_generator |
|
65 |
(fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term |
|
66 |
||
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
67 |
val _ = |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
68 |
Outer_Syntax.command @{command_spec "quickcheck_generator"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
69 |
"define quickcheck generators for abstract types" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
70 |
((Parse.type_const -- |
46949 | 71 |
Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) -- |
72 |
(Args.$$$ "constructors" |-- @{keyword ":"} |-- Parse.list1 Parse.term) |
|
46564
daa915508f63
adding parsing of an optional predicate with quickcheck_generator command
bulwahn
parents:
45940
diff
changeset
|
73 |
>> (fn ((tyco, opt_pred), constrs) => |
daa915508f63
adding parsing of an optional predicate with quickcheck_generator command
bulwahn
parents:
45940
diff
changeset
|
74 |
Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs))) |
45925 | 75 |
|
76 |
end; |