src/HOL/Tools/typecopy_package.ML
author paulson
Tue May 22 17:56:06 2007 +0200 (2007-05-22)
changeset 23075 69e30a7e8880
parent 22846 fb79144af9a3
child 24219 e558fe311376
permissions -rw-r--r--
Some hacks for SPASS format
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@20855
     5
Introducing copies of types using trivial typedefs; datatype-like abstraction.
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@20483
    19
    -> theory -> (string * info) * theory
haftmann@20426
    20
  val get_typecopies: theory -> string list
haftmann@20426
    21
  val get_typecopy_info: theory -> string -> info option
haftmann@20835
    22
  type hook = string * info -> theory -> theory
haftmann@20835
    23
  val add_hook: hook -> theory -> theory
haftmann@20835
    24
  val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
haftmann@20835
    25
  val get_eq: theory -> string -> thm
wenzelm@22846
    26
  val print_typecopies: theory -> unit
haftmann@20426
    27
  val setup: theory -> theory
haftmann@20426
    28
end;
haftmann@20426
    29
haftmann@20426
    30
structure TypecopyPackage: TYPECOPY_PACKAGE =
haftmann@20426
    31
struct
haftmann@20426
    32
haftmann@20426
    33
(* theory data *)
haftmann@20426
    34
haftmann@20426
    35
type info = {
haftmann@20426
    36
  vs: (string * sort) list,
haftmann@20426
    37
  constr: string,
haftmann@20426
    38
  typ: typ,
haftmann@20426
    39
  inject: thm,
haftmann@20426
    40
  proj: string * typ,
haftmann@20426
    41
  proj_def: thm
haftmann@20426
    42
};
haftmann@20426
    43
haftmann@20426
    44
type hook = string * info -> theory -> theory;
haftmann@20426
    45
haftmann@20426
    46
structure TypecopyData = TheoryDataFun
wenzelm@22846
    47
(
haftmann@20426
    48
  type T = info Symtab.table * (serial * hook) list;
haftmann@20426
    49
  val empty = (Symtab.empty, []);
haftmann@20426
    50
  val copy = I;
haftmann@20426
    51
  val extend = I;
haftmann@20426
    52
  fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
haftmann@20426
    53
    (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
wenzelm@22846
    54
);
wenzelm@22846
    55
wenzelm@22846
    56
fun print_typecopies thy =
wenzelm@22846
    57
  let
wenzelm@22846
    58
    val (tab, _) = TypecopyData.get thy;
wenzelm@22846
    59
    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
wenzelm@22846
    60
      (Pretty.block o Pretty.breaks) [
wenzelm@22846
    61
        Sign.pretty_typ thy (Type (tyco, map TFree vs)),
wenzelm@22846
    62
        Pretty.str "=",
wenzelm@22846
    63
        (Pretty.str o Sign.extern_const thy) constr,
wenzelm@22846
    64
        Sign.pretty_typ thy typ,
wenzelm@22846
    65
        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
haftmann@20426
    66
    in
wenzelm@22846
    67
      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
wenzelm@22846
    68
        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
haftmann@20426
    69
    end;
haftmann@20426
    70
haftmann@20426
    71
val get_typecopies = Symtab.keys o fst o TypecopyData.get;
haftmann@20426
    72
val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
haftmann@20426
    73
haftmann@20426
    74
haftmann@20426
    75
(* hook management *)
haftmann@20426
    76
haftmann@20426
    77
fun add_hook hook =
haftmann@20426
    78
  (TypecopyData.map o apsnd o cons) (serial (), hook);
haftmann@20426
    79
haftmann@20426
    80
fun invoke_hooks tyco_info thy =
haftmann@20426
    81
  fold (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
haftmann@20426
    82
haftmann@20426
    83
haftmann@20426
    84
(* add a type copy *)
haftmann@20426
    85
haftmann@20426
    86
local
haftmann@20426
    87
haftmann@20483
    88
fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
haftmann@20426
    89
  let
haftmann@20426
    90
    val ty = prep_typ thy raw_ty;
haftmann@20426
    91
    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
haftmann@20426
    92
    val tac = Tactic.rtac UNIV_witness 1;
haftmann@20483
    93
    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
haftmann@20426
    94
      Rep_name = c_rep, Abs_inject = inject,
wenzelm@21708
    95
      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
haftmann@20426
    96
        let
haftmann@20426
    97
          val exists_thm =
haftmann@20426
    98
            UNIV_I
haftmann@20426
    99
            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
haftmann@20426
   100
          val inject' = inject OF [exists_thm, exists_thm];
haftmann@20426
   101
          val proj_def = inverse OF [exists_thm];
haftmann@20426
   102
          val info = {
haftmann@20426
   103
            vs = vs,
haftmann@20426
   104
            constr = c_abs,
haftmann@20426
   105
            typ = ty_rep,
haftmann@20426
   106
            inject = inject',
haftmann@20426
   107
            proj = (c_rep, ty_abs --> ty_rep),
haftmann@20426
   108
            proj_def = proj_def
haftmann@20426
   109
          };
haftmann@20426
   110
        in
haftmann@20426
   111
          thy
haftmann@20483
   112
          |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info)
haftmann@20483
   113
          |> invoke_hooks (tyco, info)
haftmann@20483
   114
          |> pair (tyco, info)
haftmann@20426
   115
        end
haftmann@20426
   116
  in
haftmann@20426
   117
    thy
haftmann@20483
   118
    |> setmp TypedefPackage.quiet_mode true
haftmann@20483
   119
        (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
haftmann@20483
   120
          (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac
haftmann@20483
   121
    |-> (fn (tyco, info) => add_info tyco info)
haftmann@20426
   122
  end;
haftmann@20426
   123
haftmann@20426
   124
in
haftmann@20426
   125
haftmann@20426
   126
val add_typecopy = gen_add_typecopy Sign.certify_typ;
haftmann@20426
   127
wenzelm@22846
   128
end;
haftmann@20426
   129
haftmann@20426
   130
haftmann@22423
   131
(* equality function equation and datatype specification *)
haftmann@20835
   132
haftmann@20835
   133
fun get_eq thy tyco =
haftmann@20835
   134
  (#inject o the o get_typecopy_info thy) tyco;
haftmann@20835
   135
haftmann@20835
   136
fun get_spec thy tyco =
haftmann@20835
   137
  let
haftmann@20835
   138
    val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
haftmann@20835
   139
  in (vs, [(constr, [typ])]) end;
haftmann@20835
   140
haftmann@20835
   141
haftmann@20835
   142
(* hook for projection function code *)
haftmann@20426
   143
wenzelm@21708
   144
fun add_project (_ , {proj_def, ...} : info) =
haftmann@22484
   145
  CodegenData.add_func true proj_def;
haftmann@20426
   146
wenzelm@22846
   147
val setup = add_hook add_project;
haftmann@20426
   148
wenzelm@22846
   149
end;