author  wenzelm 
Sat, 17 Oct 2009 15:57:51 +0200  
changeset 32966  5b21661fe618 
parent 32859  204f749f35a9 
child 33291  93f0238151f6 
child 33560  b12ab081e5d1 
permissions  rwrr 
30824  1 
(* Title: Tools/quickcheck.ML 
28256  2 
Author: Stefan Berghofer, Florian Haftmann, TU Muenchen 
3 

4 
Generic counterexample search engine. 

5 
*) 

6 

7 
signature QUICKCHECK = 

8 
sig 

32740  9 
val auto: bool Unsynchronized.ref 
10 
val auto_time_limit: int Unsynchronized.ref 

30980  11 
val test_term: Proof.context > bool > string option > int > int > term > 
12 
(string * term) list option 

13 
val add_generator: string * (Proof.context > term > int > term list option) > theory > theory 

32297  14 
val quickcheck: (string * string) list > int > Proof.state > (string * term) list option 
28256  15 
end; 
16 

17 
structure Quickcheck : QUICKCHECK = 

18 
struct 

19 

30980  20 
(* preferences *) 
21 

32740  22 
val auto = Unsynchronized.ref false; 
23 
val auto_time_limit = Unsynchronized.ref 2500; 

30980  24 

25 
val _ = 

26 
ProofGeneralPgip.add_preference Preferences.category_tracing 

32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32859
diff
changeset

27 
(setmp_CRITICAL auto true (fn () => 
30980  28 
Preferences.bool_pref auto 
29 
"autoquickcheck" 

30 
"Whether to enable quickcheck automatically.") ()); 

31 

32 
val _ = 

33 
ProofGeneralPgip.add_preference Preferences.category_tracing 

34 
(Preferences.nat_pref auto_time_limit 

35 
"autoquickchecktimelimit" 

36 
"Time limit for automatic quickcheck (in milliseconds)."); 

37 

30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30824
diff
changeset

38 

28315  39 
(* quickcheck configuration  default parameters, test generators *) 
40 

28309  41 
datatype test_params = Test_Params of 
42 
{ size: int, iterations: int, default_type: typ option }; 

43 

30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30824
diff
changeset

44 
fun dest_test_params (Test_Params { size, iterations, default_type }) = 
28315  45 
((size, iterations), default_type); 
31599  46 
fun make_test_params ((size, iterations), default_type) = 
28309  47 
Test_Params { size = size, iterations = iterations, default_type = default_type }; 
48 
fun map_test_params f (Test_Params { size, iterations, default_type}) = 

31599  49 
make_test_params (f ((size, iterations), default_type)); 
30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30824
diff
changeset

50 
fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1 }, 
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30824
diff
changeset

51 
Test_Params { size = size2, iterations = iterations2, default_type = default_type2 }) = 
31599  52 
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)), 
28309  53 
case default_type1 of NONE => default_type2  _ => default_type1); 
54 

55 
structure Data = TheoryDataFun( 

56 
type T = (string * (Proof.context > term > int > term list option)) list 

57 
* test_params; 

58 
val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE }); 

28256  59 
val copy = I; 
60 
val extend = I; 

28309  61 
fun merge pp ((generators1, params1), (generators2, params2)) = 
62 
(AList.merge (op = : string * string > bool) (K true) (generators1, generators2), 

63 
merge_test_params (params1, params2)); 

28256  64 
) 
65 

28309  66 
val add_generator = Data.map o apfst o AList.update (op =); 
67 

28315  68 

69 
(* generating tests *) 

70 

28309  71 
fun mk_tester_select name ctxt = 
72 
case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name 

73 
of NONE => error ("No such quickcheck generator: " ^ name) 

74 
 SOME generator => generator ctxt; 

75 

76 
fun mk_testers ctxt t = 

77 
(map snd o fst o Data.get o ProofContext.theory_of) ctxt 

78 
> map_filter (fn generator => try (generator ctxt) t); 

79 

80 
fun mk_testers_strict ctxt t = 

81 
let 

82 
val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt) 

83 
val testers = map (fn generator => Exn.capture (generator ctxt) t) generators; 

84 
in if forall (is_none o Exn.get_result) testers 

85 
then [(Exn.release o snd o split_last) testers] 

86 
else map_filter Exn.get_result testers 

87 
end; 

88 

28315  89 

90 
(* testing propositions *) 

91 

28309  92 
fun prep_test_term t = 
93 
let 

29266  94 
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse 
28309  95 
error "Term to be tested contains type variables"; 
29266  96 
val _ = null (Term.add_vars t []) orelse 
28309  97 
error "Term to be tested contains schematic variables"; 
31138  98 
val frees = Term.add_frees t []; 
28309  99 
in (map fst frees, list_abs_free (frees, t)) end 
28256  100 

28315  101 
fun test_term ctxt quiet generator_name size i t = 
28309  102 
let 
103 
val (names, t') = prep_test_term t; 

104 
val testers = case generator_name 

105 
of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' 

106 
 SOME name => [mk_tester_select name ctxt t']; 

107 
fun iterate f 0 = NONE 

31153  108 
 iterate f j = case f () handle Match => (if quiet then () 
28309  109 
else warning "Exception Match raised during quickcheck"; NONE) 
31153  110 
of NONE => iterate f (j  1)  SOME q => SOME q; 
28309  111 
fun with_testers k [] = NONE 
112 
 with_testers k (tester :: testers) = 

31153  113 
case iterate (fn () => tester (k  1)) i 
28309  114 
of NONE => with_testers k testers 
115 
 SOME q => SOME q; 

116 
fun with_size k = if k > size then NONE 

117 
else (if quiet then () else priority ("Test data size: " ^ string_of_int k); 

118 
case with_testers k testers 

119 
of NONE => with_size (k + 1)  SOME q => SOME q); 

120 
in case with_size 1 

121 
of NONE => NONE 

122 
 SOME ts => SOME (names ~~ ts) 

123 
end; 

124 

125 
fun monomorphic_term thy insts default_T = 

126 
let 

127 
fun subst (T as TFree (v, S)) = 

128 
let 

129 
val T' = AList.lookup (op =) insts v 

130 
> the_default (the_default T default_T) 

28315  131 
in if Sign.of_sort thy (T, S) then T' 
28309  132 
else error ("Type " ^ Syntax.string_of_typ_global thy T ^ 
133 
" to be substituted for variable " ^ 

134 
Syntax.string_of_typ_global thy T ^ "\ndoes not have sort " ^ 

135 
Syntax.string_of_sort_global thy S) 

136 
end 

137 
 subst T = T; 

138 
in (map_types o map_atyps) subst end; 

139 

28315  140 
fun test_goal quiet generator_name size iterations default_T insts i assms state = 
28309  141 
let 
142 
val ctxt = Proof.context_of state; 

143 
val thy = Proof.theory_of state; 

144 
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t 

145 
 strip t = t; 

32859
204f749f35a9
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
wenzelm
parents:
32740
diff
changeset

146 
val (_, st) = Proof.flat_goal state; 
28309  147 
val (gi, frees) = Logic.goal_params (prop_of st) i; 
148 
val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi)) 

149 
> monomorphic_term thy insts default_T 

150 
> ObjectLogic.atomize_term thy; 

28315  151 
in test_term ctxt quiet generator_name size iterations gi' end; 
152 

153 
fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found." 

154 
 pretty_counterex ctxt (SOME cex) = 

155 
Pretty.chunks (Pretty.str "Counterexample found:\n" :: 

156 
map (fn (s, t) => 

157 
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex); 

158 

159 

160 
(* automatic testing *) 

28309  161 

30980  162 
val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state => 
28309  163 
let 
164 
val ctxt = Proof.context_of state; 

30473
e0b66c11e7e4
Assumption.all_prems_of, Assumption.all_assms_of;
wenzelm
parents:
29266
diff
changeset

165 
val assms = map term_of (Assumption.all_assms_of ctxt); 
28309  166 
val Test_Params { size, iterations, default_type } = 
167 
(snd o Data.get o Proof.theory_of) state; 

168 
fun test () = 

169 
let 

170 
val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit)) 

28315  171 
(try (test_goal true NONE size iterations default_type [] 1 assms)) state; 
28309  172 
in 
173 
case res of 

174 
NONE => state 

175 
 SOME NONE => state 

176 
 SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "", 

177 
Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state 

178 
end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state); 

179 
in 

180 
if int andalso !auto andalso not (!Toplevel.quiet) 

181 
then test () 

182 
else state 

30980  183 
end)); 
28315  184 

185 

30980  186 
(* Isar commands *) 
28315  187 

28336  188 
fun read_nat s = case (Library.read_int o Symbol.explode) s 
189 
of (k, []) => if k >= 0 then k 

190 
else error ("Not a natural number: " ^ s) 

191 
 (_, _ :: _) => error ("Not a natural number: " ^ s); 

28315  192 

28336  193 
fun parse_test_param ctxt ("size", arg) = 
194 
(apfst o apfst o K) (read_nat arg) 

195 
 parse_test_param ctxt ("iterations", arg) = 

196 
(apfst o apsnd o K) (read_nat arg) 

197 
 parse_test_param ctxt ("default_type", arg) = 

198 
(apsnd o K o SOME) (ProofContext.read_typ ctxt arg) 

199 
 parse_test_param ctxt (name, _) = 

200 
error ("Bad test parameter: " ^ name); 

28315  201 

28336  202 
fun parse_test_param_inst ctxt ("generator", arg) = 
203 
(apsnd o apfst o K o SOME) arg 

204 
 parse_test_param_inst ctxt (name, arg) = 

205 
case try (ProofContext.read_typ ctxt) name 

206 
of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =)) 

207 
(v, ProofContext.read_typ ctxt arg) 

208 
 _ => (apfst o parse_test_param ctxt) (name, arg); 

28309  209 

28336  210 
fun quickcheck_params_cmd args thy = 
28315  211 
let 
212 
val ctxt = ProofContext.init thy; 

28336  213 
val f = fold (parse_test_param ctxt) args; 
28315  214 
in 
215 
thy 

28336  216 
> (Data.map o apsnd o map_test_params) f 
28315  217 
end; 
218 

32297  219 
fun quickcheck args i state = 
28315  220 
let 
32297  221 
val thy = Proof.theory_of state; 
222 
val ctxt = Proof.context_of state; 

28315  223 
val default_params = (dest_test_params o snd o Data.get) thy; 
28336  224 
val f = fold (parse_test_param_inst ctxt) args; 
28315  225 
val (((size, iterations), default_type), (generator_name, insts)) = 
28336  226 
f (default_params, (NONE, [])); 
32297  227 
in 
228 
test_goal false generator_name size iterations default_type insts i [] state 

229 
end; 

230 

231 
fun quickcheck_cmd args i state = 

232 
quickcheck args i (Toplevel.proof_of state) 

233 
> Pretty.writeln o pretty_counterex (Toplevel.context_of state); 

28309  234 

235 
local structure P = OuterParse and K = OuterKeyword in 

236 

28336  237 
val parse_arg = P.name  P.$$$ "="  P.name; 
238 
val parse_args = P.$$$ "["  P.list1 parse_arg  P.$$$ "]" 

239 
 Scan.succeed []; 

240 

28315  241 
val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl 
28336  242 
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); 
28309  243 

28315  244 
val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag 
28336  245 
(parse_args  Scan.optional P.nat 1 
246 
>> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i))); 

28309  247 

248 
end; (*local*) 

249 

28315  250 
end; 
28309  251 

252 

28315  253 
val auto_quickcheck = Quickcheck.auto; 
254 
val auto_quickcheck_time_limit = Quickcheck.auto_time_limit; 