28256

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

28315

10 
val test_term: Proof.context > bool > string option > int > int > term > (string * term) list option;

28256

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

28315

12 
val auto: bool ref


13 
val auto_time_limit: int ref

28256

14 
end;


15 


16 
structure Quickcheck : QUICKCHECK =


17 
struct


18 

28315

19 
(* quickcheck configuration  default parameters, test generators *)


20 

28309

21 
datatype test_params = Test_Params of


22 
{ size: int, iterations: int, default_type: typ option };


23 

28315

24 
fun dest_test_params (Test_Params { size, iterations, default_type}) =


25 
((size, iterations), default_type);

28309

26 
fun mk_test_params ((size, iterations), default_type) =


27 
Test_Params { size = size, iterations = iterations, default_type = default_type };


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


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


30 
fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1},


31 
Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) =


32 
mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),


33 
case default_type1 of NONE => default_type2  _ => default_type1);


34 


35 
structure Data = TheoryDataFun(


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


37 
* test_params;


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

28256

39 
val copy = I;


40 
val extend = I;

28309

41 
fun merge pp ((generators1, params1), (generators2, params2)) =


42 
(AList.merge (op = : string * string > bool) (K true) (generators1, generators2),


43 
merge_test_params (params1, params2));

28256

44 
)


45 

28309

46 
val add_generator = Data.map o apfst o AList.update (op =);


47 

28315

48 


49 
(* generating tests *)


50 

28309

51 
fun mk_tester_select name ctxt =


52 
case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name


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


54 
 SOME generator => generator ctxt;


55 


56 
fun mk_testers ctxt t =


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


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


59 


60 
fun mk_testers_strict ctxt t =


61 
let


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


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


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


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


66 
else map_filter Exn.get_result testers


67 
end;


68 

28315

69 


70 
(* testing propositions *)


71 

28309

72 
fun prep_test_term t =


73 
let


74 
val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse


75 
error "Term to be tested contains type variables";


76 
val _ = null (term_vars t) orelse


77 
error "Term to be tested contains schematic variables";


78 
val frees = map dest_Free (term_frees t);


79 
in (map fst frees, list_abs_free (frees, t)) end

28256

80 

28315

81 
fun test_term ctxt quiet generator_name size i t =

28309

82 
let


83 
val (names, t') = prep_test_term t;


84 
val testers = case generator_name


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


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


87 
fun iterate f 0 = NONE


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


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


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


91 
fun with_testers k [] = NONE


92 
 with_testers k (tester :: testers) =


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


94 
of NONE => with_testers k testers


95 
 SOME q => SOME q;


96 
fun with_size k = if k > size then NONE


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


98 
case with_testers k testers


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


100 
in case with_size 1


101 
of NONE => NONE


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


103 
end;


104 


105 
fun monomorphic_term thy insts default_T =


106 
let


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


108 
let


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


110 
> the_default (the_default T default_T)

28315

111 
in if Sign.of_sort thy (T, S) then T'

28309

112 
else error ("Type " ^ Syntax.string_of_typ_global thy T ^


113 
" to be substituted for variable " ^


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


115 
Syntax.string_of_sort_global thy S)


116 
end


117 
 subst T = T;


118 
in (map_types o map_atyps) subst end;


119 

28315

120 
fun test_goal quiet generator_name size iterations default_T insts i assms state =

28309

121 
let


122 
val ctxt = Proof.context_of state;


123 
val thy = Proof.theory_of state;


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


125 
 strip t = t;


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


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


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


129 
> monomorphic_term thy insts default_T


130 
> ObjectLogic.atomize_term thy;

28315

131 
in test_term ctxt quiet generator_name size iterations gi' end;


132 


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


134 
 pretty_counterex ctxt (SOME cex) =


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


136 
map (fn (s, t) =>


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


138 


139 


140 
(* automatic testing *)

28309

141 


142 
val auto = ref false;


143 
val auto_time_limit = ref 5000;

28256

144 

28309

145 
fun test_goal_auto int state =


146 
let


147 
val ctxt = Proof.context_of state;


148 
val assms = map term_of (Assumption.assms_of ctxt);


149 
val Test_Params { size, iterations, default_type } =


150 
(snd o Data.get o Proof.theory_of) state;


151 
fun test () =


152 
let


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

28315

154 
(try (test_goal true NONE size iterations default_type [] 1 assms)) state;

28309

155 
in


156 
case res of


157 
NONE => state


158 
 SOME NONE => state


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


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


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


162 
in


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


164 
then test ()


165 
else state


166 
end;


167 

28315

168 
val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);


169 


170 


171 
(* Isar interfaces *)


172 

28336

173 
fun read_nat s = case (Library.read_int o Symbol.explode) s


174 
of (k, []) => if k >= 0 then k


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


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

28315

177 

28336

178 
fun parse_test_param ctxt ("size", arg) =


179 
(apfst o apfst o K) (read_nat arg)


180 
 parse_test_param ctxt ("iterations", arg) =


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


182 
 parse_test_param ctxt ("default_type", arg) =


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


184 
 parse_test_param ctxt (name, _) =


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

28315

186 

28336

187 
fun parse_test_param_inst ctxt ("generator", arg) =


188 
(apsnd o apfst o K o SOME) arg


189 
 parse_test_param_inst ctxt (name, arg) =


190 
case try (ProofContext.read_typ ctxt) name


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


192 
(v, ProofContext.read_typ ctxt arg)


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

28309

194 

28336

195 
fun quickcheck_params_cmd args thy =

28315

196 
let


197 
val ctxt = ProofContext.init thy;

28336

198 
val f = fold (parse_test_param ctxt) args;

28315

199 
in


200 
thy

28336

201 
> (Data.map o apsnd o map_test_params) f

28315

202 
end;


203 

28336

204 
fun quickcheck_cmd args i state =

28315

205 
let


206 
val prf = Toplevel.proof_of state;


207 
val thy = Toplevel.theory_of state;


208 
val ctxt = Toplevel.context_of state;


209 
val default_params = (dest_test_params o snd o Data.get) thy;

28336

210 
val f = fold (parse_test_param_inst ctxt) args;

28315

211 
val (((size, iterations), default_type), (generator_name, insts)) =

28336

212 
f (default_params, (NONE, []));

28315

213 
val counterex = test_goal false generator_name size iterations


214 
default_type insts i [] prf;


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

28309

216 


217 
local structure P = OuterParse and K = OuterKeyword in


218 

28336

219 
val parse_arg = P.name  P.$$$ "="  P.name;


220 
val parse_args = P.$$$ "["  P.list1 parse_arg  P.$$$ "]"


221 
 Scan.succeed [];


222 

28315

223 
val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl

28336

224 
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));

28309

225 

28315

226 
val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag

28336

227 
(parse_args  Scan.optional P.nat 1


228 
>> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));

28309

229 


230 
end; (*local*)


231 

28315

232 
end;

28309

233 


234 

28315

235 
val auto_quickcheck = Quickcheck.auto;


236 
val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;
