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