src/HOL/Tools/typedef_codegen.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 35994 9cc3df9a606e
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann@19459
     1
(*  Title:      HOL/Tools/typedef_codegen.ML
haftmann@31597
     2
    Author:     Stefan Berghofer, TU Muenchen
haftmann@19459
     3
haftmann@19459
     4
Code generators for trivial typedefs.
haftmann@19459
     5
*)
haftmann@19459
     6
haftmann@19459
     7
signature TYPEDEF_CODEGEN =
haftmann@19459
     8
sig
haftmann@20428
     9
  val setup: theory -> theory
haftmann@19459
    10
end;
haftmann@19459
    11
haftmann@19459
    12
structure TypedefCodegen: TYPEDEF_CODEGEN =
haftmann@19459
    13
struct
haftmann@19459
    14
haftmann@28537
    15
fun typedef_codegen thy defs dep module brack t gr =
haftmann@19459
    16
  let
haftmann@19459
    17
    fun get_name (Type (tname, _)) = tname
haftmann@19459
    18
      | get_name _ = "";
haftmann@19459
    19
    fun mk_fun s T ts =
haftmann@19459
    20
      let
haftmann@28537
    21
        val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
haftmann@28537
    22
        val (ps, gr'') =
haftmann@28537
    23
          fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
haftmann@28537
    24
        val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
haftmann@28537
    25
      in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
haftmann@19459
    26
    fun lookup f T =
wenzelm@35743
    27
      (* FIXME handle multiple typedef interpretations (!??) *)
wenzelm@35743
    28
      (case Typedef.get_info_global thy (get_name T) of
wenzelm@35743
    29
        [info] => f info
wenzelm@35743
    30
      | _ => "");
haftmann@19459
    31
  in
haftmann@19459
    32
    (case strip_comb t of
haftmann@19459
    33
       (Const (s, Type ("fun", [T, U])), ts) =>
wenzelm@35994
    34
         if lookup (#Rep_name o #1) T = s andalso
haftmann@19459
    35
           is_none (Codegen.get_assoc_type thy (get_name T))
haftmann@19459
    36
         then mk_fun s T ts
wenzelm@35994
    37
         else if lookup (#Abs_name o #1) U = s andalso
haftmann@19459
    38
           is_none (Codegen.get_assoc_type thy (get_name U))
haftmann@19459
    39
         then mk_fun s U ts
haftmann@19459
    40
         else NONE
haftmann@19459
    41
     | _ => NONE)
haftmann@19459
    42
  end;
haftmann@19459
    43
berghofe@26975
    44
fun mk_tyexpr [] s = Codegen.str s
berghofe@26975
    45
  | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
haftmann@19459
    46
  | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
haftmann@19459
    47
haftmann@28537
    48
fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
wenzelm@35743
    49
      (case Typedef.get_info_global thy s of
wenzelm@35743
    50
        (* FIXME handle multiple typedef interpretations (!??) *)
wenzelm@35994
    51
        [({abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...}, _)] =>
wenzelm@35743
    52
          if is_some (Codegen.get_assoc_type thy tname) then NONE
wenzelm@35743
    53
          else
wenzelm@35743
    54
            let
wenzelm@35743
    55
              val module' = Codegen.if_library
wenzelm@35743
    56
                (Codegen.thyname_of_type thy tname) module;
wenzelm@35743
    57
              val node_id = tname ^ " (type)";
wenzelm@35743
    58
              val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
wenzelm@35743
    59
                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
wenzelm@35743
    60
                    Ts ||>>
wenzelm@35743
    61
                Codegen.mk_const_id module' Abs_name ||>>
wenzelm@35743
    62
                Codegen.mk_const_id module' Rep_name ||>>
wenzelm@35743
    63
                Codegen.mk_type_id module' s;
wenzelm@35743
    64
              val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
wenzelm@35743
    65
            in
wenzelm@35743
    66
              SOME (tyexpr, case try (Codegen.get_node gr') node_id of
wenzelm@35743
    67
                NONE =>
wenzelm@35743
    68
                  let
wenzelm@35743
    69
                    val (p :: ps, gr'') = fold_map
wenzelm@35743
    70
                      (Codegen.invoke_tycodegen thy defs node_id module' false)
wenzelm@35743
    71
                      (oldT :: Us) (Codegen.add_edge (node_id, dep)
wenzelm@35743
    72
                        (Codegen.new_node (node_id, (NONE, "", "")) gr'));
wenzelm@35743
    73
                    val s =
wenzelm@35743
    74
                      Codegen.string_of (Pretty.block [Codegen.str "datatype ",
wenzelm@35743
    75
                        mk_tyexpr ps (snd ty_id),
wenzelm@35743
    76
                        Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
wenzelm@35743
    77
                        Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
wenzelm@35743
    78
                      Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
wenzelm@35743
    79
                        Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
wenzelm@35743
    80
                        Codegen.str "x) = x;"]) ^ "\n\n" ^
haftmann@36692
    81
                      (if member (op =) (!Codegen.mode) "term_of" then
wenzelm@35743
    82
                        Codegen.string_of (Pretty.block [Codegen.str "fun ",
wenzelm@35743
    83
                          Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
wenzelm@35743
    84
                          Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
wenzelm@35743
    85
                          Codegen.str "x) =", Pretty.brk 1,
wenzelm@35743
    86
                          Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
wenzelm@35743
    87
                            Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
wenzelm@35743
    88
                            Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
wenzelm@35743
    89
                          Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
wenzelm@35743
    90
                          Codegen.str "x;"]) ^ "\n\n"
wenzelm@35743
    91
                       else "") ^
haftmann@36692
    92
                      (if member (op =) (!Codegen.mode) "test" then
wenzelm@35743
    93
                        Codegen.string_of (Pretty.block [Codegen.str "fun ",
wenzelm@35743
    94
                          Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
wenzelm@35743
    95
                          Codegen.str "i =", Pretty.brk 1,
wenzelm@35743
    96
                          Pretty.block [Codegen.str (Abs_id ^ " ("),
wenzelm@35743
    97
                            Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
wenzelm@35743
    98
                            Codegen.str "i);"]]) ^ "\n\n"
wenzelm@35743
    99
                       else "")
wenzelm@35743
   100
                  in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
wenzelm@35743
   101
              | SOME _ => Codegen.add_edge (node_id, dep) gr')
wenzelm@35743
   102
            end
wenzelm@35743
   103
      | _ => NONE)
haftmann@28537
   104
  | typedef_tycodegen thy defs dep module brack _ gr = NONE;
haftmann@19459
   105
haftmann@19459
   106
val setup =
haftmann@19459
   107
  Codegen.add_codegen "typedef" typedef_codegen
haftmann@19459
   108
  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
haftmann@19459
   109
haftmann@19459
   110
end;