author  haftmann 
Wed, 13 May 2009 18:41:40 +0200  
changeset 31138  a51ce445d498 
parent 30980  fe0855471964 
child 31153  6b31b143f18b 
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 

28315  9 
val auto: bool ref 
10 
val auto_time_limit: int 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 

28256  14 
end; 
15 

16 
structure Quickcheck : QUICKCHECK = 

17 
struct 

18 

30980  19 
(* preferences *) 
20 

21 
val auto = ref false; 

22 
val auto_time_limit = ref 2500; 

23 

24 
val _ = 

25 
ProofGeneralPgip.add_preference Preferences.category_tracing 

26 
(setmp auto true (fn () => 

27 
Preferences.bool_pref auto 

28 
"autoquickcheck" 

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

30 

31 
val _ = 

32 
ProofGeneralPgip.add_preference Preferences.category_tracing 

33 
(Preferences.nat_pref auto_time_limit 

34 
"autoquickchecktimelimit" 

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

36 

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

37 

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

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

42 

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

43 
fun dest_test_params (Test_Params { size, iterations, default_type }) = 
28315  44 
((size, iterations), default_type); 
28309  45 
fun mk_test_params ((size, iterations), default_type) = 
46 
Test_Params { size = size, iterations = iterations, default_type = default_type }; 

47 
fun map_test_params f (Test_Params { size, iterations, default_type}) = 

48 
mk_test_params (f ((size, iterations), default_type)); 

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

49 
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

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

53 

54 
structure Data = TheoryDataFun( 

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

56 
* test_params; 

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

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

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

62 
merge_test_params (params1, params2)); 

28256  63 
) 
64 

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

28315  67 

68 
(* generating tests *) 

69 

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

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

73 
 SOME generator => generator ctxt; 

74 

75 
fun mk_testers ctxt t = 

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

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

78 

79 
fun mk_testers_strict ctxt t = 

80 
let 

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

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

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

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

85 
else map_filter Exn.get_result testers 

86 
end; 

87 

28315  88 

89 
(* testing propositions *) 

90 

28309  91 
fun prep_test_term t = 
92 
let 

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

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

103 
val testers = case generator_name 

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

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

106 
fun iterate f 0 = NONE 

107 
 iterate f k = case f () handle Match => (if quiet then () 

108 
else warning "Exception Match raised during quickcheck"; NONE) 

109 
of NONE => iterate f (k  1)  SOME q => SOME q; 

110 
fun with_testers k [] = NONE 

111 
 with_testers k (tester :: testers) = 

112 
case iterate (fn () => tester k) i 

113 
of NONE => with_testers k testers 

114 
 SOME q => SOME q; 

115 
fun with_size k = if k > size then NONE 

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

117 
case with_testers k testers 

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

119 
in case with_size 1 

120 
of NONE => NONE 

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

122 
end; 

123 

124 
fun monomorphic_term thy insts default_T = 

125 
let 

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

127 
let 

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

129 
> the_default (the_default T default_T) 

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

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

134 
Syntax.string_of_sort_global thy S) 

135 
end 

136 
 subst T = T; 

137 
in (map_types o map_atyps) subst end; 

138 

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

142 
val thy = Proof.theory_of state; 

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

144 
 strip t = t; 

145 
val (_, (_, st)) = Proof.get_goal state; 

146 
val (gi, frees) = Logic.goal_params (prop_of st) i; 

147 
val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi)) 

148 
> monomorphic_term thy insts default_T 

149 
> ObjectLogic.atomize_term thy; 

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

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

153 
 pretty_counterex ctxt (SOME cex) = 

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

155 
map (fn (s, t) => 

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

157 

158 

159 
(* automatic testing *) 

28309  160 

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

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

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

167 
fun test () = 

168 
let 

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

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

173 
NONE => state 

174 
 SOME NONE => state 

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

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

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

178 
in 

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

180 
then test () 

181 
else state 

30980  182 
end)); 
28315  183 

184 

30980  185 
(* Isar commands *) 
28315  186 

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

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

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

28315  191 

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

194 
 parse_test_param ctxt ("iterations", arg) = 

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

196 
 parse_test_param ctxt ("default_type", arg) = 

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

198 
 parse_test_param ctxt (name, _) = 

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

28315  200 

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

203 
 parse_test_param_inst ctxt (name, arg) = 

204 
case try (ProofContext.read_typ ctxt) name 

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

206 
(v, ProofContext.read_typ ctxt arg) 

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

28309  208 

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

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

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

28336  218 
fun quickcheck_cmd args i state = 
28315  219 
let 
220 
val prf = Toplevel.proof_of state; 

221 
val thy = Toplevel.theory_of state; 

222 
val ctxt = Toplevel.context_of state; 

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, [])); 
28315  227 
val counterex = test_goal false generator_name size iterations 
228 
default_type insts i [] prf; 

229 
in (Pretty.writeln o pretty_counterex ctxt) counterex end; 

28309  230 

231 
local structure P = OuterParse and K = OuterKeyword in 

232 

28336  233 
val parse_arg = P.name  P.$$$ "="  P.name; 
234 
val parse_args = P.$$$ "["  P.list1 parse_arg  P.$$$ "]" 

235 
 Scan.succeed []; 

236 

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

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

28309  243 

244 
end; (*local*) 

245 

28315  246 
end; 
28309  247 

248 

28315  249 
val auto_quickcheck = Quickcheck.auto; 
250 
val auto_quickcheck_time_limit = Quickcheck.auto_time_limit; 