# HG changeset patch
# User berghofe
# Date 1199989682 -3600
# Node ID 3ff9d646a66a6e817bc98e4c22b838e497f53683
# Parent  1bd12187a96e4f87038044b55ab2403ca76a858c
Test data generation and conversion to terms are now more closely
intertwined, to allow displaying of functions in test data.

diff -r 1bd12187a96e -r 3ff9d646a66a src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu Jan 10 19:25:08 2008 +0100
+++ b/src/Pure/codegen.ML	Thu Jan 10 19:28:02 2008 +0100
@@ -67,6 +67,8 @@
   val is_instance: typ -> typ -> bool
   val parens: Pretty.T -> Pretty.T
   val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
+  val mk_tuple: Pretty.T list -> Pretty.T
+  val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
   val eta_expand: term -> term list -> int -> term
   val strip_tname: string -> string
   val mk_type: bool -> typ -> Pretty.T
@@ -789,6 +791,19 @@
   add_tycodegen "default" default_tycodegen);
 
 
+fun mk_tuple [p] = p
+  | mk_tuple ps = Pretty.block (Pretty.str "(" ::
+      List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single ps)) @
+        [Pretty.str ")"]);
+
+fun mk_let bindings body =
+  Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
+    Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
+      Pretty.block [Pretty.str "val ", pat, Pretty.str " =", Pretty.brk 1,
+      rhs, Pretty.str ";"]) bindings)),
+    Pretty.brk 1, Pretty.str "in", Pretty.brk 1, body,
+    Pretty.brk 1, Pretty.str "end"]);
+
 fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
 
 fun add_to_module name s = AList.map_entry (op =) name (suffix s);
@@ -902,11 +917,16 @@
 fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str
       (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
   | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
-  | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I)
+  | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
       (Pretty.block (separate (Pretty.brk 1)
         (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
           (if member (op =) xs s then "'" else "")) ::
-         map (mk_gen gr module true xs a) Ts @
+         (case tyc of
+            ("fun", [T, U]) =>
+              [mk_term_of gr module true T, mk_type true T,
+               mk_gen gr module true xs a U, mk_type true U]
+          | _ => maps (fn T =>
+              [mk_gen gr module true xs a T, mk_type true T]) Ts) @
          (if member (op =) xs s then [Pretty.str a] else []))));
 
 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
@@ -927,13 +947,11 @@
       "\nopen Generated;\n\n" ^ Pretty.string_of
         (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
           Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
-          Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
-            Pretty.blk (0, separate Pretty.fbrk (map (fn ((s, T), s') =>
-              Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1,
-              mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
-              Pretty.str "i;"]) frees')),
-            Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
-            Pretty.block [Pretty.str "if ",
+          mk_let (map (fn ((s, T), s') =>
+              (mk_tuple [Pretty.str s', Pretty.str (s' ^ "_t")],
+               Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
+                 Pretty.str "i"])) frees')
+            (Pretty.block [Pretty.str "if ",
               mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'),
               Pretty.brk 1, Pretty.str "then NONE",
               Pretty.brk 1, Pretty.str "else ",
@@ -941,10 +959,9 @@
                 flat (separate [Pretty.str ",", Pretty.brk 1]
                   (map (fn ((s, T), s') => [Pretty.block
                     [Pretty.str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
-                     mk_app false (mk_term_of gr "Generated" false T)
-                       [Pretty.str s'], Pretty.str ")"]]) frees')) @
-                  [Pretty.str "]"])]],
-            Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
+                     Pretty.str (s' ^ "_t ())")]]) frees')) @
+                  [Pretty.str "]"])]]),
+          Pretty.str ");"]) ^
       "\n\nend;\n") ();
     val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy));
     fun iter f k = if k > i then NONE
@@ -1087,21 +1104,6 @@
      (p, []) => p
    | _ => error ("Malformed annotation: " ^ quote s));
 
-val _ = Context.add_setup
-  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
-     [("term_of",
-       "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
-      ("test",
-       "fun gen_fun_type _ G i =\n\
-       \  let\n\
-       \    val f = ref (fn x => raise Match);\n\
-       \    val _ = (f := (fn x =>\n\
-       \      let\n\
-       \        val y = G i;\n\
-       \        val f' = !f\n\
-       \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
-       \  in (fn x => !f x) end;\n")]))]);
-
 
 structure P = OuterParse and K = OuterKeyword;