# HG changeset patch # User bulwahn # Date 1316669213 -7200 # Node ID 632a033616e933a4a3d222cf223ca889a64c7926 # Parent e24bf05dd27309222e5aff5c4a146e9094e0e830 adding post-processing of terms to narrowing-based Quickcheck diff -r e24bf05dd273 -r 632a033616e9 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Sep 21 17:43:13 2011 -0700 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Sep 22 07:26:53 2011 +0200 @@ -353,6 +353,19 @@ (names ~~ boundTs', t') end +fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT) + +fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) = + absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) + | eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) = + let + val (T1, T2) = dest_ffun (body_type T) + in + Quickcheck_Common.mk_fun_upd T1 T2 + (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) + end + | eval_finite_functions t = t + (** tester **) val rewrs = @@ -389,12 +402,15 @@ | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) = if p = 0 then t else mk_case_term ctxt (p - 1) qs' c +val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions + fun mk_terms ctxt qs result = let val ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs) in map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps + |> map (apsnd post_process) end fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) = @@ -436,7 +452,8 @@ thy (apfst o Option.map o map) (ensure_testable (finitize t')) in Quickcheck.Result - {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample, + {counterexample = + Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = #timings (dest_result result), reports = #reports (dest_result result)} end diff -r e24bf05dd273 -r 632a033616e9 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Sep 21 17:43:13 2011 -0700 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Sep 22 07:26:53 2011 +0200 @@ -18,6 +18,7 @@ val gen_mk_parametric_generator_expr : (((Proof.context -> term * term list -> term) * term) * typ) -> Proof.context -> (term * term list) list -> term + val mk_fun_upd : typ -> typ -> term * term -> term -> term val post_process_term : term -> term end;