# 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;