equal
deleted
inserted
replaced
72 |
72 |
73 fun compile_generator_expr thy t = |
73 fun compile_generator_expr thy t = |
74 let |
74 let |
75 val tys = (map snd o fst o strip_abs) t; |
75 val tys = (map snd o fst o strip_abs) t; |
76 val t' = mk_generator_expr thy t tys; |
76 val t' = mk_generator_expr thy t tys; |
77 val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) thy t' []; |
77 val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) |
78 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end; |
78 (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; |
|
79 in f #> Random_Engine.run end; |
79 |
80 |
80 end |
81 end |
81 *} |
82 *} |
82 |
83 |
83 setup {* |
84 setup {* |