src/HOL/Tools/typedef_codegen.ML
author haftmann
Tue Aug 08 08:19:39 2006 +0200 (2006-08-08)
changeset 20354 0bfdbbe657eb
parent 19704 9b2612b807ab
child 20428 67fa1c6ba89e
permissions -rw-r--r--
improved & fixed code generator theorem generation
     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 typedef_fun_extr: theory -> string * typ -> thm list option
    11   val typedef_type_extr: theory -> string
    12       -> (((string * sort) list * (string * typ list) list) * tactic) option
    13   val setup: theory -> theory;
    14 end;
    15 
    16 structure TypedefCodegen: TYPEDEF_CODEGEN =
    17 struct
    18 
    19 fun typedef_codegen thy defs gr dep module brack t =
    20   let
    21     fun get_name (Type (tname, _)) = tname
    22       | get_name _ = "";
    23     fun mk_fun s T ts =
    24       let
    25         val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
    26         val (gr'', ps) =
    27           foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
    28         val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
    29       in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
    30     fun lookup f T =
    31       (case TypedefPackage.get_info thy (get_name T) of
    32         NONE => ""
    33       | SOME info => f info);
    34   in
    35     (case strip_comb t of
    36        (Const (s, Type ("fun", [T, U])), ts) =>
    37          if lookup #Rep_name T = s andalso
    38            is_none (Codegen.get_assoc_type thy (get_name T))
    39          then mk_fun s T ts
    40          else if lookup #Abs_name U = s andalso
    41            is_none (Codegen.get_assoc_type thy (get_name U))
    42          then mk_fun s U ts
    43          else NONE
    44      | _ => NONE)
    45   end;
    46 
    47 fun mk_tyexpr [] s = Pretty.str s
    48   | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)]
    49   | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
    50 
    51 fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
    52       (case TypedefPackage.get_info thy s of
    53          NONE => NONE
    54        | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
    55            if is_some (Codegen.get_assoc_type thy tname) then NONE else
    56            let
    57              val module' = Codegen.if_library
    58                (Codegen.thyname_of_type tname thy) module;
    59              val node_id = tname ^ " (type)";
    60              val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
    61                  (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
    62                    (gr, Ts) |>>>
    63                Codegen.mk_const_id module' Abs_name |>>>
    64                Codegen.mk_const_id module' Rep_name |>>>
    65                Codegen.mk_type_id module' s;
    66              val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
    67            in SOME (case try (Codegen.get_node gr') node_id of
    68                NONE =>
    69                let
    70                  val (gr'', p :: ps) = foldl_map
    71                    (Codegen.invoke_tycodegen thy defs node_id module' false)
    72                    (Codegen.add_edge (node_id, dep)
    73                       (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
    74                  val s =
    75                    Pretty.string_of (Pretty.block [Pretty.str "datatype ",
    76                      mk_tyexpr ps (snd ty_id),
    77                      Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"),
    78                      Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^
    79                    Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id),
    80                      Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    81                      Pretty.str "x) = x;"]) ^ "\n\n" ^
    82                    (if "term_of" mem !Codegen.mode then
    83                       Pretty.string_of (Pretty.block [Pretty.str "fun ",
    84                         Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1,
    85                         Pretty.str ("(" ^ Abs_id), Pretty.brk 1,
    86                         Pretty.str "x) =", Pretty.brk 1,
    87                         Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","),
    88                           Pretty.brk 1, Codegen.mk_type false (oldT --> newT),
    89                           Pretty.str ")"], Pretty.str " $", Pretty.brk 1,
    90                         Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1,
    91                         Pretty.str "x;"]) ^ "\n\n"
    92                     else "") ^
    93                    (if "test" mem !Codegen.mode then
    94                       Pretty.string_of (Pretty.block [Pretty.str "fun ",
    95                         Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1,
    96                         Pretty.str "i =", Pretty.brk 1,
    97                         Pretty.block [Pretty.str (Abs_id ^ " ("),
    98                           Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1,
    99                           Pretty.str "i);"]]) ^ "\n\n"
   100                     else "")
   101                in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
   102              | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
   103            end)
   104   | typedef_tycodegen thy defs gr dep module brack _ = NONE;
   105 
   106 fun typedef_type_extr thy tyco =
   107   case TypedefPackage.get_info thy tyco
   108    of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep,
   109      set_def = SOME def, Abs_inject = inject, ...} =>
   110         let
   111           val exists_thm =
   112             UNIV_I
   113             |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
   114             |> rewrite_rule [symmetric def];
   115         in case try (op OF) (inject, [exists_thm, exists_thm])
   116          of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
   117              (ALLGOALS o match_tac) [eq_reflection]
   118             THEN (ALLGOALS o match_tac) [eq_thm])
   119           | NONE => NONE
   120         end
   121     | _ => NONE;
   122 
   123 fun typedef_fun_extr thy (c, ty) =
   124   case (fst o strip_type) ty
   125    of Type (tyco, _) :: _ =>
   126     (case TypedefPackage.get_info thy tyco
   127      of SOME {abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep,
   128        set_def = SOME def, Abs_inverse = inverse, ...} =>
   129           if c = c_rep then
   130             let
   131               val exists_thm =
   132                 UNIV_I
   133                 |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
   134                 |> rewrite_rule [symmetric def]
   135             in case try (op OF) (inverse, [exists_thm, exists_thm])
   136              of SOME eq_thm => SOME [eq_thm]
   137               | NONE => NONE
   138             end
   139           else NONE
   140       | _ => NONE)
   141     | _ => NONE;
   142 
   143 val setup =
   144   Codegen.add_codegen "typedef" typedef_codegen
   145   #> Codegen.add_tycodegen "typedef" typedef_tycodegen
   146   #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
   147   #> CodegenTheorems.add_datatype_extr typedef_type_extr
   148 
   149 end;