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