src/HOL/ex/Quickcheck.thy
changeset 28309 c24bc53c815c
parent 28228 7ebe8dc06cbb
child 28315 d3cf88fe77bc
equal deleted inserted replaced
28308:d4396a28fb29 28309:c24bc53c815c
   242 
   242 
   243 ML {*
   243 ML {*
   244 structure Quickcheck =
   244 structure Quickcheck =
   245 struct
   245 struct
   246 
   246 
       
   247 open Quickcheck;
       
   248 
   247 val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
   249 val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
   248 
   250 
   249 fun mk_generator_expr thy prop tys =
   251 fun mk_generator_expr thy prop tys =
   250   let
   252   let
   251     val bound_max = length tys - 1;
   253     val bound_max = length tys - 1;
   265     fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
   267     fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
   266       (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
   268       (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
   267     val t = fold_rev mk_bindclause bounds (return $ check);
   269     val t = fold_rev mk_bindclause bounds (return $ check);
   268   in Abs ("n", @{typ index}, t) end;
   270   in Abs ("n", @{typ index}, t) end;
   269 
   271 
   270 fun compile_generator_expr thy prop tys =
   272 fun compile_generator_expr thy t =
   271   let
   273   let
   272     val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy
   274     val tys = (map snd o fst o strip_abs) t;
   273       (mk_generator_expr thy prop tys) [];
   275     val t' = mk_generator_expr thy t tys;
       
   276     val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' [];
   274   in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
   277   in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
   275 
   278 
   276 fun VALUE prop tys thy =
   279 end
   277   let
   280 *}
   278     val t = mk_generator_expr thy prop tys;
   281 
   279     val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t)
   282 setup {*
   280   in
   283   Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
   281     thy
       
   282     |> TheoryTarget.init NONE
       
   283     |> Specification.definition (NONE, (Attrib.no_binding, eq))
       
   284     |> snd
       
   285     |> LocalTheory.exit
       
   286     |> ProofContext.theory_of
       
   287   end;
       
   288 
       
   289 end
       
   290 *}
   284 *}
   291 
   285 
   292 subsection {* Examples *}
   286 subsection {* Examples *}
   293 
   287 
   294 (*export_code "random :: index \<Rightarrow> seed \<Rightarrow> ((_ \<Rightarrow> _) \<times> (unit \<Rightarrow> term)) \<times> seed"
   288 (*lemma
   295   in SML file -*)
   289   fixes n m :: nat
   296 
   290   shows "n + m \<le> n * m"
   297 (*setup {* Quickcheck.VALUE
   291 ;test_goal [code];
   298   @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
   292 oops*)
   299 
   293 
   300 export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"
   294 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   301 use "~~/../../gen_code/quickcheck.ML"
   295   @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} *}
   302 ML {* Random_Engine.run (QuickcheckExample.range 1) *}*)
       
   303 
       
   304 (*definition "FOO = (True, Suc 0)"
       
   305 
       
   306 code_module (test) QuickcheckExample
       
   307   file "~~/../../gen_code/quickcheck'.ML"
       
   308   contains FOO*)
       
   309 
       
   310 ML {* val f = Quickcheck.compile_generator_expr @{theory}
       
   311   @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
       
   312 
   296 
   313 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   297 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   314 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   298 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   315 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   299 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   316 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   300 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   321 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   305 ML {* f 1 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   322 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   306 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   323 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   307 ML {* f 2 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   324 
   308 
   325 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   309 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   326   @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
   310   @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} *}
   327 
   311 
   328 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   312 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   329 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   313 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   330 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   314 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   331 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   315 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   339 ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   323 ML {* f 3 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   340 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   324 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   341 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   325 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   342 
   326 
   343 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   327 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   344   @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"}
   328   @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"} *}
   345   [@{typ "int list"}, @{typ "int list"}] *}
       
   346 
   329 
   347 ML {* f 15 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   330 ML {* f 15 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   348 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   331 ML {* f 5 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   349 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   332 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   350 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   333 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   371 ML {* f 6 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   354 ML {* f 6 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   372 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   355 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   373 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   356 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   374 
   357 
   375 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   358 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   376   @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *}
   359   @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} *}
   377 
   360 
   378 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   361 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   379 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   362 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   380 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   363 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   381 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   364 ML {* f 4 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   382 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   365 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   383 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   366 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   384 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   367 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   385 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   368 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   386 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   369 ML {* f 10 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   387 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   370 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   388 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   371 ML {* f 8 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   389 
   372 
   390 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   373 ML {* val f = Quickcheck.compile_generator_expr @{theory}
   391   @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
   374   @{term "\<lambda>f k. int (f k) = k"} *}
   392 
   375 
   393 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   376 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   394 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   377 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   395 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   378 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   396 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   379 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   397 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   380 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   398 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   381 ML {* f 20 |> (Option.map o map) (Syntax.string_of_term @{context}) *}
   399 
   382 
   400 end
   383 end