# HG changeset patch
# User berghofe
# Date 1199988608 -3600
# Node ID 7753e0d81b7a8a3278fd0a7633ab193a45750dd4
# Parent  6fbc3f54f8198aeef6a618e237f965d9f6310822
Added test data generator for function type (from Pure/codegen.ML).

diff -r 6fbc3f54f819 -r 7753e0d81b7a src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jan 10 19:09:21 2008 +0100
+++ b/src/HOL/Fun.thy	Thu Jan 10 19:10:08 2008 +0100
@@ -497,6 +497,28 @@
 
 subsection {* Code generator setup *}
 
+types_code
+  "fun"  ("(_ ->/ _)")
+attach (term_of) {*
+fun term_of_fun_type _ aT _ bT _ = Free ("<function>", aT --> bT);
+*}
+attach (test) {*
+fun gen_fun_type aF aT bG bT i =
+  let
+    val tab = ref [];
+    fun mk_upd (x, (_, y)) t = Const ("Fun.fun_upd",
+      (aT --> bT) --> aT --> bT --> aT --> bT) $ t $ aF x $ y ()
+  in
+    (fn x =>
+       case AList.lookup op = (!tab) x of
+         NONE =>
+           let val p as (y, _) = bG i
+           in (tab := (x, p) :: !tab; y) end
+       | SOME (y, _) => y,
+     fn () => Basics.fold mk_upd (!tab) (Const ("arbitrary", aT --> bT)))
+  end;
+*}
+
 code_const "op \<circ>"
   (SML infixl 5 "o")
   (Haskell infixr 9 ".")