src/HOL/Tools/typedef_codegen.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 20597 65fe827aa595
child 26975 103dca19ef2e
permissions -rw-r--r--
Some hacks for SPASS format
     1 (*  Title:      HOL/Tools/typedef_codegen.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
     4 
     5 Code generators for trivial typedefs.
     6 *)
     7 
     8 signature TYPEDEF_CODEGEN =
     9 sig
    10   val setup: theory -> theory
    11 end;
    12 
    13 structure TypedefCodegen: TYPEDEF_CODEGEN =
    14 struct
    15 
    16 fun typedef_codegen thy defs gr dep module brack t =
    17   let
    18     fun get_name (Type (tname, _)) = tname
    19       | get_name _ = "";
    20     fun mk_fun s T ts =
    21       let
    22         val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
    23         val (gr'', ps) =
    24           foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    25         val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    26       in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    27     fun lookup f T =
    28       (case TypedefPackage.get_info thy (get_name T) of
    29         NONE => ""
    30       | SOME info => f info);
    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 = Pretty.str s
    45   | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    46   | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    47 
    48 fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    49       (case TypedefPackage.get_info thy s of
    50          NONE => NONE
    51        | SOME {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 else
    53            let
    54              val module' = Codegen.if_library
    55                (Codegen.thyname_of_type tname thy) module;
    56              val node_id = tname ^ " (type)";
    57              val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    58                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    59                    (gr, Ts) |>>>
    60                Codegen.mk_const_id module' Abs_name |>>>
    61                Codegen.mk_const_id module' Rep_name |>>>
    62                Codegen.mk_type_id module' s;
    63              val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    64            in SOME (case try (Codegen.get_node gr') node_id of
    65                NONE =>
    66                let
    67                  val (gr'', p :: ps) = foldl_map
    68                    (Codegen.invoke_tycodegen thy defs node_id module' false)
    69                    (Codegen.add_edge (node_id, dep)
    70                       (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
    71                  val s =
    72                    Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    73                      mk_tyexpr ps (snd ty_id),
    74                      Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
    75                      Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
    76                    Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
    77                      Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    78                      Pretty.str "x) = x;"]) ^ "\n\n" ^
    79                    (if "term_of" mem !Codegen.mode then
    80                       Pretty.string_of (Pretty.block [Pretty.str "fun ",
    81                         Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    82                         Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    83                         Pretty.str "x) =", Pretty.brk 1,
    84                         Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    85                           Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    86                           Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    87                         Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    88                         Pretty.str "x;"]) ^ "\n\n"
    89                     else "") ^
    90                    (if "test" mem !Codegen.mode then
    91                       Pretty.string_of (Pretty.block [Pretty.str "fun ",
    92                         Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    93                         Pretty.str "i =", Pretty.brk 1,
    94                         Pretty.block [Pretty.str (Abs_id ^ " ("),
    95                           Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
    96                           Pretty.str "i);"]]) ^ "\n\n"
    97                     else "")
    98                in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
    99              | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
   100            end)
   101   | typedef_tycodegen thy defs gr dep module brack _ = NONE;
   102 
   103 val setup =
   104   Codegen.add_codegen "typedef" typedef_codegen
   105   #> Codegen.add_tycodegen "typedef" typedef_tycodegen
   106 
   107 end;