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