Test data generation and conversion to terms are now more closely
authorberghofe
Thu Jan 10 19:28:02 2008 +0100 (2008-01-10)
changeset 258923ff9d646a66a
parent 25891 1bd12187a96e
child 25893 b06a09abf79e
Test data generation and conversion to terms are now more closely
intertwined, to allow displaying of functions in test data.
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Thu Jan 10 19:25:08 2008 +0100
     1.2 +++ b/src/Pure/codegen.ML	Thu Jan 10 19:28:02 2008 +0100
     1.3 @@ -67,6 +67,8 @@
     1.4    val is_instance: typ -> typ -> bool
     1.5    val parens: Pretty.T -> Pretty.T
     1.6    val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
     1.7 +  val mk_tuple: Pretty.T list -> Pretty.T
     1.8 +  val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T
     1.9    val eta_expand: term -> term list -> int -> term
    1.10    val strip_tname: string -> string
    1.11    val mk_type: bool -> typ -> Pretty.T
    1.12 @@ -789,6 +791,19 @@
    1.13    add_tycodegen "default" default_tycodegen);
    1.14  
    1.15  
    1.16 +fun mk_tuple [p] = p
    1.17 +  | mk_tuple ps = Pretty.block (Pretty.str "(" ::
    1.18 +      List.concat (separate [Pretty.str ",", Pretty.brk 1] (map single ps)) @
    1.19 +        [Pretty.str ")"]);
    1.20 +
    1.21 +fun mk_let bindings body =
    1.22 +  Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
    1.23 +    Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) =>
    1.24 +      Pretty.block [Pretty.str "val ", pat, Pretty.str " =", Pretty.brk 1,
    1.25 +      rhs, Pretty.str ";"]) bindings)),
    1.26 +    Pretty.brk 1, Pretty.str "in", Pretty.brk 1, body,
    1.27 +    Pretty.brk 1, Pretty.str "end"]);
    1.28 +
    1.29  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
    1.30  
    1.31  fun add_to_module name s = AList.map_entry (op =) name (suffix s);
    1.32 @@ -902,11 +917,16 @@
    1.33  fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str
    1.34        (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G")
    1.35    | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G")
    1.36 -  | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I)
    1.37 +  | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
    1.38        (Pretty.block (separate (Pretty.brk 1)
    1.39          (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
    1.40            (if member (op =) xs s then "'" else "")) ::
    1.41 -         map (mk_gen gr module true xs a) Ts @
    1.42 +         (case tyc of
    1.43 +            ("fun", [T, U]) =>
    1.44 +              [mk_term_of gr module true T, mk_type true T,
    1.45 +               mk_gen gr module true xs a U, mk_type true U]
    1.46 +          | _ => maps (fn T =>
    1.47 +              [mk_gen gr module true xs a T, mk_type true T]) Ts) @
    1.48           (if member (op =) xs s then [Pretty.str a] else []))));
    1.49  
    1.50  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
    1.51 @@ -927,13 +947,11 @@
    1.52        "\nopen Generated;\n\n" ^ Pretty.string_of
    1.53          (Pretty.block [Pretty.str "val () = Codegen.test_fn :=",
    1.54            Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1,
    1.55 -          Pretty.blk (0, [Pretty.str "let", Pretty.brk 1,
    1.56 -            Pretty.blk (0, separate Pretty.fbrk (map (fn ((s, T), s') =>
    1.57 -              Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1,
    1.58 -              mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
    1.59 -              Pretty.str "i;"]) frees')),
    1.60 -            Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
    1.61 -            Pretty.block [Pretty.str "if ",
    1.62 +          mk_let (map (fn ((s, T), s') =>
    1.63 +              (mk_tuple [Pretty.str s', Pretty.str (s' ^ "_t")],
    1.64 +               Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
    1.65 +                 Pretty.str "i"])) frees')
    1.66 +            (Pretty.block [Pretty.str "if ",
    1.67                mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'),
    1.68                Pretty.brk 1, Pretty.str "then NONE",
    1.69                Pretty.brk 1, Pretty.str "else ",
    1.70 @@ -941,10 +959,9 @@
    1.71                  flat (separate [Pretty.str ",", Pretty.brk 1]
    1.72                    (map (fn ((s, T), s') => [Pretty.block
    1.73                      [Pretty.str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
    1.74 -                     mk_app false (mk_term_of gr "Generated" false T)
    1.75 -                       [Pretty.str s'], Pretty.str ")"]]) frees')) @
    1.76 -                  [Pretty.str "]"])]],
    1.77 -            Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
    1.78 +                     Pretty.str (s' ^ "_t ())")]]) frees')) @
    1.79 +                  [Pretty.str "]"])]]),
    1.80 +          Pretty.str ");"]) ^
    1.81        "\n\nend;\n") ();
    1.82      val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy));
    1.83      fun iter f k = if k > i then NONE
    1.84 @@ -1087,21 +1104,6 @@
    1.85       (p, []) => p
    1.86     | _ => error ("Malformed annotation: " ^ quote s));
    1.87  
    1.88 -val _ = Context.add_setup
    1.89 -  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
    1.90 -     [("term_of",
    1.91 -       "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
    1.92 -      ("test",
    1.93 -       "fun gen_fun_type _ G i =\n\
    1.94 -       \  let\n\
    1.95 -       \    val f = ref (fn x => raise Match);\n\
    1.96 -       \    val _ = (f := (fn x =>\n\
    1.97 -       \      let\n\
    1.98 -       \        val y = G i;\n\
    1.99 -       \        val f' = !f\n\
   1.100 -       \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
   1.101 -       \  in (fn x => !f x) end;\n")]))]);
   1.102 -
   1.103  
   1.104  structure P = OuterParse and K = OuterKeyword;
   1.105