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

28309

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

28256

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


12 
end;


13 


14 
structure Quickcheck : QUICKCHECK =


15 
struct


16 

28309

17 
datatype test_params = Test_Params of


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


19 


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


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


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


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


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


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


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


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


28 


29 
structure Data = TheoryDataFun(


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


31 
* test_params;


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

28256

33 
val copy = I;


34 
val extend = I;

28309

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


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


37 
merge_test_params (params1, params2));

28256

38 
)


39 

28309

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


41 


42 
fun mk_tester_select name ctxt =


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


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


45 
 SOME generator => generator ctxt;


46 


47 
fun mk_testers ctxt t =


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


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


50 


51 
fun mk_testers_strict ctxt t =


52 
let


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


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


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


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


57 
else map_filter Exn.get_result testers


58 
end;


59 


60 
fun prep_test_term t =


61 
let


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


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


64 
val _ = null (term_vars t) orelse


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


66 
val frees = map dest_Free (term_frees t);


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

28256

68 

28309

69 
fun test_term generator_name ctxt quiet size i t =


70 
let


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


72 
val testers = case generator_name


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


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


75 
fun iterate f 0 = NONE


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


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


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


79 
fun with_testers k [] = NONE


80 
 with_testers k (tester :: testers) =


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


82 
of NONE => with_testers k testers


83 
 SOME q => SOME q;


84 
fun with_size k = if k > size then NONE


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


86 
case with_testers k testers


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


88 
in case with_size 1


89 
of NONE => NONE


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


91 
end;


92 


93 
fun monomorphic_term thy insts default_T =


94 
let


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


96 
let


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


98 
> the_default (the_default T default_T)


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


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


101 
" to be substituted for variable " ^


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


103 
Syntax.string_of_sort_global thy S)


104 
end


105 
 subst T = T;


106 
in (map_types o map_atyps) subst end;


107 


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


109 
 pretty_counterex ctxt (SOME cex) =


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


111 
map (fn (s, t) =>


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


113 


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


115 
let


116 
val ctxt = Proof.context_of state;


117 
val thy = Proof.theory_of state;


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


119 
 strip t = t;


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


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


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


123 
> monomorphic_term thy insts default_T


124 
> ObjectLogic.atomize_term thy;


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


126 


127 
val auto = ref false;


128 
val auto_time_limit = ref 5000;

28256

129 

28309

130 
fun test_goal_auto int state =


131 
let


132 
val ctxt = Proof.context_of state;


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


134 
val Test_Params { size, iterations, default_type } =


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


136 
fun test () =


137 
let


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


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


140 
in


141 
case res of


142 
NONE => state


143 
 SOME NONE => state


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


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


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


147 
in


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


149 
then test ()


150 
else state


151 
end;


152 


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


154 


155 
fun test_goal_cmd generator_name i state =


156 
test_goal generator_name false 10 100 NONE [] i [] (Toplevel.proof_of state)


157 
> pretty_counterex (Toplevel.context_of state)


158 
> Pretty.writeln;


159 


160 
local structure P = OuterParse and K = OuterKeyword in


161 


162 
fun read_nothing x thy = x;


163 
fun read_typ raw_ty thy = Syntax.read_typ_global thy raw_ty;


164 


165 
val parse_test_param = (P.short_ident  P.$$$ "=" #>


166 
(fn "size" => P.nat >> (apfst o apfst o K)


167 
 "iterations" => P.nat >> (apfst o apsnd o K)


168 
 "default_type" => P.typ >> (apsnd o K)));


169 


170 
val parse_test_param_inst =


171 
P.type_ident  P.$$$ "="  P.typ >> (apsnd o AList.update (op =))


172 
 parse_test_param >> apfst;


173 


174 
(*fun quickcheck_test_params_cmd fs thy =


175 
(Data.map o apsnd o map_test_params) (Library.apply fs);*)


176 


177 
(*val _ =


178 
OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl


179 
(P.$$$ "["  P.list1 parse_test_param  P.$$$ "]" >>


180 
(Toplevel.theory o quickcheck_test_params_cmd));*)


181 


182 
(*


183 
val params =


184 
[("size", P.nat >> (K o set_size)),


185 
("iterations", P.nat >> (K o set_iterations)),


186 
("default_type", P.typ >> set_default_type)];


187 


188 
val parse_test_params = P.short_ident : (fn s =>


189 
P.$$$ "="  (AList.lookup (op =) params s > the_default Scan.fail));

28256

190 

28309

191 
fun parse_tyinst xs =


192 
(P.type_ident  P.$$$ "="  P.typ >> (fn (v, s) => fn thy =>


193 
fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;


194 


195 


196 
*)


197 


198 
val _ = OuterSyntax.improper_command "test_goal" "try to find counterexample for subgoal" K.diag


199 
(Scan.option (P.$$$ "["  P.xname  P.$$$ "]")  Scan.optional P.nat 1


200 
>> (fn (some_name, i) => Toplevel.no_timing o Toplevel.keep (test_goal_cmd some_name i)));


201 


202 
end; (*local*)


203 


204 


205 


206 
(*


207 
val _ =


208 
OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl


209 
(P.$$$ "["  P.list1 parse_test_params  P.$$$ "]" >>


210 
(fn fs => Toplevel.theory (fn thy =>


211 
map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));


212 


213 
val _ =


214 
OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag


215 
(Scan.option (P.$$$ "["  P.list1


216 
( parse_test_params >> (fn f => fn thy => apfst (f thy))


217 
 parse_tyinst)  P.$$$ "]")  Scan.optional P.nat 1 >>


218 
(fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st >


219 
test_goal false (Library.apply (the_default []


220 
(Option.map (map (fn f => f (Toplevel.theory_of st))) ps))


221 
(get_test_params (Toplevel.theory_of st), [])) g [] >


222 
pretty_counterex (Toplevel.context_of st) > Pretty.writeln)));


223 


224 
val auto_quickcheck = ref false;


225 
val auto_quickcheck_time_limit = ref 5000;


226 


227 
fun test_goal' int state =


228 
let


229 
val ctxt = Proof.context_of state;


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


231 
val params = get_test_params (Proof.theory_of state);


232 
fun test () =


233 
let


234 
val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))


235 
(try (test_goal true (params, []) 1 assms)) state;


236 
in


237 
case res of


238 
NONE => state


239 
 SOME NONE => state


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


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


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


243 
in


244 
if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)


245 
then test ()


246 
else state


247 
end;


248 
*)


249 


250 
(*

28256

251 
fun value_cmd some_name modes raw_t state =


252 
let


253 
val ctxt = Toplevel.context_of state;


254 
val t = Syntax.read_term ctxt raw_t;


255 
val t' = case some_name


256 
of NONE => value ctxt t


257 
 SOME name => value_select name ctxt t;


258 
val ty' = Term.type_of t';


259 
val ctxt' = Variable.auto_fixes t ctxt;


260 
val p = PrintMode.with_modes modes (fn () =>


261 
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,


262 
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();


263 
in Pretty.writeln p end;*)


264 

28309

265 
end;

28256

266 

28309

267 
(*val auto_quickcheck = Quickcheck.auto;


268 
val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;*)
