# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID 51df2353510541276cfa2767d9fba2d2ce01bd9b
# Parent  1bd4b6d1c482470dda00a2f8e99f635fb0fa26aa
handling a quite restricted set of functions in Quickcheck_Narrowing by an easy transformation

diff -r 1bd4b6d1c482 -r 51df23535105 src/HOL/Library/Quickcheck_Narrowing.thy
--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -458,16 +458,6 @@
 
 declare simp_thms(17,19)[code del]
 
-subsubsection {* Setting up the counterexample generator *}
-  
-use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
-
-setup {* Narrowing_Generators.setup *}
-
-hide_type (open) code_int type "term" cons
-hide_const (open) int_of of_int nth error toEnum map_index split_At empty
-  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
-
 subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
 
 datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
@@ -480,5 +470,23 @@
 hide_type (open) ffun
 hide_const (open) Constant Update eval_ffun
 
+datatype 'b cfun = Constant 'b
+
+primrec eval_cfun :: "'b cfun => 'a => 'b"
+where
+  "eval_cfun (Constant c) y = c"
+
+hide_type (open) cfun
+hide_const (open) Constant eval_cfun
+
+subsubsection {* Setting up the counterexample generator *}
+  
+use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
+
+setup {* Narrowing_Generators.setup *}
+
+hide_type (open) code_int type "term" cons
+hide_const (open) int_of of_int nth error toEnum map_index split_At empty
+  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
 
 end
\ No newline at end of file
diff -r 1bd4b6d1c482 -r 51df23535105 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -184,9 +184,34 @@
   fun init _ () = error "Counterexample"
 )
 
-val put_counterexample =  Counterexample.put
+val put_counterexample = Counterexample.put
 
-fun finitize_functions t = t
+fun finitize_functions t =
+  let
+    val ((names, Ts), t') = apfst split_list (strip_abs t)
+    fun mk_eval_ffun dT rT =
+      Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
+        Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
+    fun mk_eval_cfun dT rT =
+      Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
+        Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
+    fun eval_function (T as Type (@{type_name fun}, [dT, rT])) =
+      let
+        val (rt', rT') = eval_function rT
+      in
+        case dT of
+          Type (@{type_name fun}, _) =>
+            (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
+            Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
+        | _ => (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 = (I, T)
+    val (tt, Ts') = split_list (map eval_function Ts)
+    val t'' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) Ts), t')
+  in
+    list_abs (names ~~ Ts', t'')
+  end
 
 fun compile_generator_expr ctxt t size =
   let
diff -r 1bd4b6d1c482 -r 51df23535105 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -42,13 +42,32 @@
 declare [[quickcheck_finite_functions]]
 
 lemma "map f xs = map g xs"
-  quickcheck[tester = narrowing, finite_types = true]
+  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
 oops
 
 lemma "map f xs = map f ys ==> xs = ys"
-  quickcheck[tester = narrowing, finite_types = true]
+  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
+oops
+
+lemma
+  "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
+  quickcheck[tester = narrowing, expect = counterexample]
+oops
+
+lemma "map f xs = F f xs"
+  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
 oops
 
+lemma "map f xs = F f xs"
+  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+(* requires some work...
+lemma "R O S = S O R"
+  quickcheck[tester = narrowing, size = 2]
+oops
+*)
+
 subsection {* AVL Trees *}
 
 datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat