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 


173 
val arg_nat = Args.name #> (fn s => case (Library.read_int o Symbol.explode) s


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


175 
else Scan.fail ("Not a natural number: " ^ s)


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


177 


178 
val parse_test_param =


179 
Scan.lift (Args.$$$ "size"  Args.$$$ "="  arg_nat) >> (apfst o apfst o K)


180 
 Scan.lift (Args.$$$ "iterations"  Args.$$$ "="  arg_nat) >> (apfst o apsnd o K)


181 
 Scan.lift (Args.$$$ "default_type"  Args.$$$ "=")  Args.typ >> (apsnd o K o SOME);


182 


183 
val parse_test_param_inst =


184 
Scan.lift (Args.$$$ "generator"  Args.$$$ "="  Args.name)


185 
>> (apsnd o apfst o K o SOME)


186 
 parse_test_param >> apfst


187 
 Args.tyname  Scan.lift (Args.$$$ "=")  Args.typ


188 
>> (apsnd o apsnd o AList.update (op =));

28309

189 

28315

190 
fun quickcheck_params_cmd pos args thy =


191 
let


192 
val ctxt = ProofContext.init thy;


193 
val src = Args.src (("quickcheck_params", args), pos);


194 
val (fs, _) = Args.context_syntax "quickcheck_params"


195 
(Scan.repeat parse_test_param) src ctxt;


196 
in


197 
thy


198 
> (Data.map o apsnd o map_test_params) (Library.apply fs)


199 
end;


200 


201 
fun quickcheck_cmd pos args i state =


202 
let


203 
val prf = Toplevel.proof_of state;


204 
val thy = Toplevel.theory_of state;


205 
val ctxt = Toplevel.context_of state;


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


207 
val src = Args.src (("quickcheck", args), pos);


208 
val (fs, _) = Args.context_syntax "quickcheck"


209 
(Scan.repeat parse_test_param_inst) src ctxt;


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


211 
Library.apply fs (default_params, (NONE, []));


212 
val counterex = test_goal false generator_name size iterations


213 
default_type insts i [] prf;


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

28309

215 


216 
local structure P = OuterParse and K = OuterKeyword in


217 

28315

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


219 
(P.$$$ "["  P.position (OuterParse.enum "," Args.parse)  P.$$$ "]"


220 
>> (fn (args, pos) => Toplevel.theory


221 
(quickcheck_params_cmd pos (flat args))));

28309

222 

28315

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


224 
(P.position (Scan.optional (P.$$$ "["  OuterParse.enum "," Args.parse  P.$$$ "]") [])


225 
 Scan.optional P.nat 1


226 
>> (fn ((args, pos), i) => Toplevel.no_timing o Toplevel.keep


227 
(quickcheck_cmd pos (flat args) i)));

28309

228 


229 
end; (*local*)


230 

28315

231 
end;

28309

232 


233 

28315

234 
val auto_quickcheck = Quickcheck.auto;


235 
val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;
