src/HOL/Tools/typecopy_package.ML
author wenzelm
Thu Mar 27 14:41:09 2008 +0100 (2008-03-27)
changeset 26424 a6cad32a27b0
parent 25864 11f531354852
child 26475 3cc1e48d0ce1
permissions -rw-r--r--
eliminated theory ProtoPure;
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@25506
    21
  val get_info: theory -> string -> info option
haftmann@25489
    22
  val interpretation: (string -> theory -> theory) -> theory -> theory
wenzelm@22846
    23
  val print_typecopies: theory -> unit
haftmann@20426
    24
  val setup: theory -> theory
haftmann@20426
    25
end;
haftmann@20426
    26
haftmann@20426
    27
structure TypecopyPackage: TYPECOPY_PACKAGE =
haftmann@20426
    28
struct
haftmann@20426
    29
haftmann@20426
    30
(* theory data *)
haftmann@20426
    31
haftmann@20426
    32
type info = {
haftmann@20426
    33
  vs: (string * sort) list,
haftmann@20426
    34
  constr: string,
haftmann@20426
    35
  typ: typ,
haftmann@20426
    36
  inject: thm,
haftmann@20426
    37
  proj: string * typ,
haftmann@20426
    38
  proj_def: thm
haftmann@20426
    39
};
haftmann@20426
    40
haftmann@20426
    41
structure TypecopyData = TheoryDataFun
wenzelm@22846
    42
(
haftmann@24626
    43
  type T = info Symtab.table;
haftmann@24626
    44
  val empty = Symtab.empty;
haftmann@20426
    45
  val copy = I;
haftmann@20426
    46
  val extend = I;
haftmann@24626
    47
  fun merge _ = Symtab.merge (K true);
wenzelm@22846
    48
);
wenzelm@22846
    49
wenzelm@22846
    50
fun print_typecopies thy =
wenzelm@22846
    51
  let
haftmann@24626
    52
    val tab = TypecopyData.get thy;
wenzelm@22846
    53
    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
wenzelm@22846
    54
      (Pretty.block o Pretty.breaks) [
wenzelm@22846
    55
        Sign.pretty_typ thy (Type (tyco, map TFree vs)),
wenzelm@22846
    56
        Pretty.str "=",
wenzelm@22846
    57
        (Pretty.str o Sign.extern_const thy) constr,
wenzelm@22846
    58
        Sign.pretty_typ thy typ,
wenzelm@22846
    59
        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
haftmann@20426
    60
    in
wenzelm@22846
    61
      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
wenzelm@22846
    62
        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
haftmann@20426
    63
    end;
haftmann@20426
    64
haftmann@24626
    65
val get_typecopies = Symtab.keys o TypecopyData.get;
haftmann@25506
    66
val get_info = Symtab.lookup o TypecopyData.get;
haftmann@20426
    67
haftmann@20426
    68
haftmann@25489
    69
(* interpretation of type copies *)
haftmann@20426
    70
wenzelm@24711
    71
structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
haftmann@25489
    72
val interpretation = TypecopyInterpretation.interpretation;
haftmann@20426
    73
haftmann@20426
    74
haftmann@20426
    75
(* add a type copy *)
haftmann@20426
    76
haftmann@20426
    77
local
haftmann@20426
    78
haftmann@20483
    79
fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
haftmann@20426
    80
  let
haftmann@20426
    81
    val ty = prep_typ thy raw_ty;
haftmann@20426
    82
    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
haftmann@20426
    83
    val tac = Tactic.rtac UNIV_witness 1;
haftmann@20483
    84
    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
haftmann@20426
    85
      Rep_name = c_rep, Abs_inject = inject,
wenzelm@21708
    86
      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
haftmann@20426
    87
        let
haftmann@20426
    88
          val exists_thm =
haftmann@20426
    89
            UNIV_I
haftmann@20426
    90
            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
haftmann@20426
    91
          val inject' = inject OF [exists_thm, exists_thm];
haftmann@20426
    92
          val proj_def = inverse OF [exists_thm];
haftmann@20426
    93
          val info = {
haftmann@20426
    94
            vs = vs,
haftmann@20426
    95
            constr = c_abs,
haftmann@20426
    96
            typ = ty_rep,
haftmann@20426
    97
            inject = inject',
haftmann@20426
    98
            proj = (c_rep, ty_abs --> ty_rep),
haftmann@20426
    99
            proj_def = proj_def
haftmann@20426
   100
          };
haftmann@20426
   101
        in
haftmann@20426
   102
          thy
haftmann@24626
   103
          |> (TypecopyData.map o Symtab.update_new) (tyco, info)
wenzelm@24711
   104
          |> TypecopyInterpretation.data tyco
haftmann@20483
   105
          |> pair (tyco, info)
haftmann@20426
   106
        end
haftmann@20426
   107
  in
haftmann@20426
   108
    thy
haftmann@20483
   109
    |> setmp TypedefPackage.quiet_mode true
haftmann@20483
   110
        (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
haftmann@20483
   111
          (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac
haftmann@20483
   112
    |-> (fn (tyco, info) => add_info tyco info)
haftmann@20426
   113
  end;
haftmann@20426
   114
haftmann@20426
   115
in
haftmann@20426
   116
haftmann@20426
   117
val add_typecopy = gen_add_typecopy Sign.certify_typ;
haftmann@20426
   118
wenzelm@22846
   119
end;
haftmann@20426
   120
haftmann@20426
   121
haftmann@25489
   122
(* code generator setup *)
haftmann@20835
   123
haftmann@25489
   124
fun add_typecopy_spec tyco thy =
haftmann@25489
   125
  let
haftmann@25534
   126
    val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;
haftmann@25864
   127
    val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;
haftmann@25506
   128
    val ty = Logic.unvarifyT (Sign.the_const_type thy constr);
haftmann@25489
   129
  in
haftmann@25506
   130
    thy
haftmann@25506
   131
    |> Code.add_datatype [(constr, ty)]
haftmann@25506
   132
    |> Code.add_func proj_def
haftmann@25864
   133
    |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])
haftmann@25569
   134
    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
haftmann@25569
   135
    |> LocalTheory.exit
haftmann@25569
   136
    |> ProofContext.theory_of
haftmann@25534
   137
    |> Code.add_func (CodeUnit.constrain_thm [HOLogic.class_eq] inject)
haftmann@25489
   138
  end;
haftmann@20426
   139
haftmann@25489
   140
val setup =
haftmann@25489
   141
  TypecopyInterpretation.init
haftmann@25489
   142
  #> interpretation add_typecopy_spec
haftmann@20426
   143
wenzelm@22846
   144
end;