|
1 (* Title: Pure/Tools/quickcheck.ML |
|
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, Florian Haftmann, TU Muenchen |
|
4 |
|
5 Generic counterexample search engine. |
|
6 *) |
|
7 |
|
8 signature QUICKCHECK = |
|
9 sig |
|
10 (*val test: Proof.context -> int -> int -> term -> (string * term) list option |
|
11 val test_select: string -> Proof.context -> int -> int -> term -> (string * term) list option |
|
12 val test_cmd: string option -> string list -> string -> Toplevel.state -> unit*) |
|
13 val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory |
|
14 end; |
|
15 |
|
16 structure Quickcheck : QUICKCHECK = |
|
17 struct |
|
18 |
|
19 structure Generator = TheoryDataFun( |
|
20 type T = (string * (Proof.context -> term -> int -> term list option)) list; |
|
21 val empty = []; |
|
22 val copy = I; |
|
23 val extend = I; |
|
24 fun merge pp = AList.merge (op =) (K true); |
|
25 ) |
|
26 |
|
27 val add_generator = Generator.map o AList.update (op =); |
|
28 |
|
29 (*fun value_select name ctxt = |
|
30 case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name |
|
31 of NONE => error ("No such evaluator: " ^ name) |
|
32 | SOME f => f ctxt; |
|
33 |
|
34 fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt) |
|
35 in if null evaluators then error "No evaluators" |
|
36 else let val (evaluators, (_, evaluator)) = split_last evaluators |
|
37 in case get_first (fn (_, f) => try (f ctxt) t) evaluators |
|
38 of SOME t' => t' |
|
39 | NONE => evaluator ctxt t |
|
40 end end; |
|
41 |
|
42 fun value_cmd some_name modes raw_t state = |
|
43 let |
|
44 val ctxt = Toplevel.context_of state; |
|
45 val t = Syntax.read_term ctxt raw_t; |
|
46 val t' = case some_name |
|
47 of NONE => value ctxt t |
|
48 | SOME name => value_select name ctxt t; |
|
49 val ty' = Term.type_of t'; |
|
50 val ctxt' = Variable.auto_fixes t ctxt; |
|
51 val p = PrintMode.with_modes modes (fn () => |
|
52 Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, |
|
53 Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); |
|
54 in Pretty.writeln p end;*) |
|
55 |
|
56 (*local structure P = OuterParse and K = OuterKeyword in |
|
57 |
|
58 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; |
|
59 |
|
60 val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag |
|
61 (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term |
|
62 >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep |
|
63 (value_cmd some_name modes t))); |
|
64 |
|
65 end; (*local*)*) |
|
66 |
|
67 end; |