# 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 ("", 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 \" (SML infixl 5 "o") (Haskell infixr 9 ".")