# HG changeset patch
# User bulwahn
# Date 1333527474 -7200
# Node ID 8fe04753a210174217ccc7236362e493f4f28606
# Parent  b9e115d4c5daa6654d15fa6767010947d7fdae5f
rudimentary handling of products in finitize_functions in Quickcheck-Narrowing

diff -r b9e115d4c5da -r 8fe04753a210 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 04 10:17:08 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 04 10:17:54 2012 +0200
@@ -363,6 +363,16 @@
             (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
               Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
       end
+      | eval_function (T as Type (@{type_name prod}, [fT, sT])) =
+        let
+          val (ft', fT') = eval_function fT
+          val (st', sT') = eval_function sT
+          val T' = Type (@{type_name prod}, [fT', sT'])
+          val map_const = Const (@{const_name map_pair}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
+          fun apply_dummy T t = absdummy T (t (Bound 0))
+        in
+          (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
+        end
       | eval_function T = (I, T)
     val (tt, boundTs') = split_list (map eval_function boundTs)
     val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t)