src/HOL/Tools/typedef_codegen.ML
author haftmann
Fri Jun 19 17:23:21 2009 +0200 (2009-06-19)
changeset 31723 f5cafe803b55
parent 31597 9a59cf39ee78
child 35743 c506c029a082
permissions -rw-r--r--
discontinued ancient tradition to suffix certain ML module names with "_package"
     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       (case Typedef.get_info thy (get_name T) of
    28         NONE => ""
    29       | SOME info => f info);
    30   in
    31     (case strip_comb t of
    32        (Const (s, Type ("fun", [T, U])), ts) =>
    33          if lookup #Rep_name T = s andalso
    34            is_none (Codegen.get_assoc_type thy (get_name T))
    35          then mk_fun s T ts
    36          else if lookup #Abs_name U = s andalso
    37            is_none (Codegen.get_assoc_type thy (get_name U))
    38          then mk_fun s U ts
    39          else NONE
    40      | _ => NONE)
    41   end;
    42 
    43 fun mk_tyexpr [] s = Codegen.str s
    44   | mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
    45   | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    46 
    47 fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    48       (case Typedef.get_info thy s of
    49          NONE => NONE
    50        | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
    51            if is_some (Codegen.get_assoc_type thy tname) then NONE else
    52            let
    53              val module' = Codegen.if_library
    54                (Codegen.thyname_of_type thy tname) module;
    55              val node_id = tname ^ " (type)";
    56              val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
    57                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    58                    Ts ||>>
    59                Codegen.mk_const_id module' Abs_name ||>>
    60                Codegen.mk_const_id module' Rep_name ||>>
    61                Codegen.mk_type_id module' s;
    62              val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    63            in SOME (tyexpr, case try (Codegen.get_node gr') node_id of
    64                NONE =>
    65                let
    66                  val (p :: ps, gr'') = fold_map
    67                    (Codegen.invoke_tycodegen thy defs node_id module' false)
    68                    (oldT :: Us) (Codegen.add_edge (node_id, dep)
    69                       (Codegen.new_node (node_id, (NONE, "", "")) gr'));
    70                  val s =
    71                    Codegen.string_of (Pretty.block [Codegen.str "datatype ",
    72                      mk_tyexpr ps (snd ty_id),
    73                      Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"),
    74                      Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^
    75                    Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id),
    76                      Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    77                      Codegen.str "x) = x;"]) ^ "\n\n" ^
    78                    (if "term_of" mem !Codegen.mode then
    79                       Codegen.string_of (Pretty.block [Codegen.str "fun ",
    80                         Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    81                         Codegen.str ("(" ^ Abs_id), Pretty.brk 1,
    82                         Codegen.str "x) =", Pretty.brk 1,
    83                         Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","),
    84                           Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    85                           Codegen.str ")"], Codegen.str " $", Pretty.brk 1,
    86                         Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    87                         Codegen.str "x;"]) ^ "\n\n"
    88                     else "") ^
    89                    (if "test" mem !Codegen.mode then
    90                       Codegen.string_of (Pretty.block [Codegen.str "fun ",
    91                         Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    92                         Codegen.str "i =", Pretty.brk 1,
    93                         Pretty.block [Codegen.str (Abs_id ^ " ("),
    94                           Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
    95                           Codegen.str "i);"]]) ^ "\n\n"
    96                     else "")
    97                in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
    98              | SOME _ => Codegen.add_edge (node_id, dep) gr')
    99            end)
   100   | typedef_tycodegen thy defs dep module brack _ gr = NONE;
   101 
   102 val setup =
   103   Codegen.add_codegen "typedef" typedef_codegen
   104   #> Codegen.add_tycodegen "typedef" typedef_tycodegen
   105 
   106 end;