src/HOL/Tools/typecopy_package.ML
author haftmann
Tue Aug 29 14:31:13 2006 +0200 (2006-08-29)
changeset 20426 9ffea7a8b31c
child 20483 04aa552a83bc
permissions -rw-r--r--
added typecopy_package
haftmann@20426
     1
(*  Title:      HOL/Tools/typecopy_package.ML
haftmann@20426
     2
    ID:         $Id$
haftmann@20426
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@20426
     4
haftmann@20426
     5
Introducing copies of types using trivial typedefs.
haftmann@20426
     6
*)
haftmann@20426
     7
haftmann@20426
     8
signature TYPECOPY_PACKAGE =
haftmann@20426
     9
sig
haftmann@20426
    10
  type info = {
haftmann@20426
    11
    vs: (string * sort) list,
haftmann@20426
    12
    constr: string,
haftmann@20426
    13
    typ: typ,
haftmann@20426
    14
    inject: thm,
haftmann@20426
    15
    proj: string * typ,
haftmann@20426
    16
    proj_def: thm
haftmann@20426
    17
  }
haftmann@20426
    18
  val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
haftmann@20426
    19
    -> theory -> info * theory
haftmann@20426
    20
  val get_typecopies: theory -> string list
haftmann@20426
    21
  val get_typecopy_info: theory -> string -> info option
haftmann@20426
    22
  type hook = string * info -> theory -> theory;
haftmann@20426
    23
  val add_hook: hook -> theory -> theory;
haftmann@20426
    24
  val typecopy_fun_extr: theory -> string * typ -> thm list option
haftmann@20426
    25
  val typecopy_type_extr: theory -> string
haftmann@20426
    26
    -> (((string * sort) list * (string * typ list) list) * tactic) option
haftmann@20426
    27
  val print: theory -> unit
haftmann@20426
    28
  val setup: theory -> theory
haftmann@20426
    29
end;
haftmann@20426
    30
haftmann@20426
    31
structure TypecopyPackage: TYPECOPY_PACKAGE =
haftmann@20426
    32
struct
haftmann@20426
    33
haftmann@20426
    34
(* theory context reference *)
haftmann@20426
    35
haftmann@20426
    36
val univ_witness = thm "Set.UNIV_witness"
haftmann@20426
    37
haftmann@20426
    38
haftmann@20426
    39
(* theory data *)
haftmann@20426
    40
haftmann@20426
    41
type info = {
haftmann@20426
    42
  vs: (string * sort) list,
haftmann@20426
    43
  constr: string,
haftmann@20426
    44
  typ: typ,
haftmann@20426
    45
  inject: thm,
haftmann@20426
    46
  proj: string * typ,
haftmann@20426
    47
  proj_def: thm
haftmann@20426
    48
};
haftmann@20426
    49
haftmann@20426
    50
type hook = string * info -> theory -> theory;
haftmann@20426
    51
haftmann@20426
    52
structure TypecopyData = TheoryDataFun
haftmann@20426
    53
(struct
haftmann@20426
    54
  val name = "HOL/typecopy_package";
haftmann@20426
    55
  type T = info Symtab.table * (serial * hook) list;
haftmann@20426
    56
  val empty = (Symtab.empty, []);
haftmann@20426
    57
  val copy = I;
haftmann@20426
    58
  val extend = I;
haftmann@20426
    59
  fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
haftmann@20426
    60
    (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
haftmann@20426
    61
  fun print thy (tab, _) =
haftmann@20426
    62
    let
haftmann@20426
    63
      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
haftmann@20426
    64
        (Pretty.block o Pretty.breaks) [
haftmann@20426
    65
          Sign.pretty_typ thy (Type (tyco, map TFree vs)),
haftmann@20426
    66
          Pretty.str "=",
haftmann@20426
    67
          (Pretty.str o Sign.extern_const thy) constr,
haftmann@20426
    68
          Sign.pretty_typ thy typ,
haftmann@20426
    69
          Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]
haftmann@20426
    70
        ];
haftmann@20426
    71
    in
haftmann@20426
    72
      (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
haftmann@20426
    73
        Pretty.str "type copies:"
haftmann@20426
    74
        :: map mk (Symtab.dest tab)
haftmann@20426
    75
      )
haftmann@20426
    76
    end;
haftmann@20426
    77
end);
haftmann@20426
    78
haftmann@20426
    79
val print = TypecopyData.print;
haftmann@20426
    80
val get_typecopies = Symtab.keys o fst o TypecopyData.get;
haftmann@20426
    81
val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
haftmann@20426
    82
haftmann@20426
    83
haftmann@20426
    84
(* hook management *)
haftmann@20426
    85
haftmann@20426
    86
fun add_hook hook =
haftmann@20426
    87
  (TypecopyData.map o apsnd o cons) (serial (), hook);
haftmann@20426
    88
haftmann@20426
    89
fun invoke_hooks tyco_info thy =
haftmann@20426
    90
  fold (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
haftmann@20426
    91
haftmann@20426
    92
haftmann@20426
    93
(* add a type copy *)
haftmann@20426
    94
haftmann@20426
    95
local
haftmann@20426
    96
haftmann@20426
    97
fun gen_add_typecopy prep_typ (tyco, raw_vs) raw_ty constr_proj thy =
haftmann@20426
    98
  let
haftmann@20426
    99
    val ty = prep_typ thy raw_ty;
haftmann@20426
   100
    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
haftmann@20426
   101
    val tac = Tactic.rtac UNIV_witness 1;
haftmann@20426
   102
    fun add_info ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
haftmann@20426
   103
      Rep_name = c_rep, Abs_inject = inject,
haftmann@20426
   104
      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = 
haftmann@20426
   105
        let
haftmann@20426
   106
          val Type (tyco', _) = ty_abs;
haftmann@20426
   107
          val exists_thm =
haftmann@20426
   108
            UNIV_I
haftmann@20426
   109
            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
haftmann@20426
   110
          val inject' = inject OF [exists_thm, exists_thm];
haftmann@20426
   111
          val proj_def = inverse OF [exists_thm];
haftmann@20426
   112
          val info = {
haftmann@20426
   113
            vs = vs,
haftmann@20426
   114
            constr = c_abs,
haftmann@20426
   115
            typ = ty_rep,
haftmann@20426
   116
            inject = inject',
haftmann@20426
   117
            proj = (c_rep, ty_abs --> ty_rep),
haftmann@20426
   118
            proj_def = proj_def
haftmann@20426
   119
          };
haftmann@20426
   120
        in
haftmann@20426
   121
          thy
haftmann@20426
   122
          |> (TypecopyData.map o apfst o Symtab.update_new) (tyco', info)
haftmann@20426
   123
          |> invoke_hooks (tyco', info)
haftmann@20426
   124
          |> pair info
haftmann@20426
   125
        end
haftmann@20426
   126
  in
haftmann@20426
   127
    thy
haftmann@20426
   128
    |> TypedefPackage.add_typedef_i false (SOME tyco) (tyco, map fst vs, NoSyn)
haftmann@20426
   129
          (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
haftmann@20426
   130
    |-> (fn info => add_info info)
haftmann@20426
   131
  end;
haftmann@20426
   132
haftmann@20426
   133
in
haftmann@20426
   134
haftmann@20426
   135
val add_typecopy = gen_add_typecopy Sign.certify_typ;
haftmann@20426
   136
haftmann@20426
   137
end; (*local*)
haftmann@20426
   138
haftmann@20426
   139
haftmann@20426
   140
(* theory setup *)
haftmann@20426
   141
haftmann@20426
   142
fun typecopy_type_extr thy tyco =
haftmann@20426
   143
  case get_typecopy_info thy tyco
haftmann@20426
   144
   of SOME { vs, constr, typ, inject, ... } => SOME ((vs, [(constr, [typ])]),
haftmann@20426
   145
       (ALLGOALS o match_tac) [eq_reflection]
haftmann@20426
   146
          THEN (ALLGOALS o match_tac) [inject])
haftmann@20426
   147
    | NONE => NONE;
haftmann@20426
   148
haftmann@20426
   149
fun typecopy_fun_extr thy (c, ty) =
haftmann@20426
   150
  case (fst o strip_type) ty
haftmann@20426
   151
   of Type (tyco, _) :: _ =>
haftmann@20426
   152
        (case get_typecopy_info thy tyco
haftmann@20426
   153
          of SOME { proj_def, proj as (c', _), ... } =>
haftmann@20426
   154
              if c = c' then SOME [proj_def] else NONE
haftmann@20426
   155
           | NONE => NONE)
haftmann@20426
   156
    | _ => NONE;
haftmann@20426
   157
haftmann@20426
   158
val setup =
haftmann@20426
   159
  TypecopyData.init
haftmann@20426
   160
  #> CodegenTheorems.add_fun_extr (these oo typecopy_fun_extr)
haftmann@20426
   161
  #> CodegenTheorems.add_datatype_extr typecopy_type_extr;
haftmann@20426
   162
haftmann@20426
   163
end; (*struct*)