src/HOL/Tools/typecopy_package.ML
author wenzelm
Thu, 07 Dec 2006 23:16:55 +0100
changeset 21708 45e7491bea47
parent 21675 38f6cb45ce24
child 22423 c1836b14c63a
permissions -rw-r--r--
reorganized structure Tactic vs. MetaSimplifier;
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
20855
9f60d493c8fe clarified header comments
haftmann
parents: 20835
diff changeset
     5
Introducing copies of types using trivial typedefs; datatype-like abstraction.
20426
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
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
    19
    -> theory -> (string * info) * theory
20426
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
20835
haftmann
parents: 20597
diff changeset
    22
  type hook = string * info -> theory -> theory
haftmann
parents: 20597
diff changeset
    23
  val add_hook: hook -> theory -> theory
haftmann
parents: 20597
diff changeset
    24
  val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
haftmann
parents: 20597
diff changeset
    25
  val get_cert: theory -> string -> thm
haftmann
parents: 20597
diff changeset
    26
  val get_eq: theory -> string -> thm
20426
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 data *)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    35
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    36
type info = {
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    37
  vs: (string * sort) list,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    38
  constr: string,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    39
  typ: typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    40
  inject: thm,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    41
  proj: string * typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    42
  proj_def: thm
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    43
};
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    44
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    45
type hook = string * info -> theory -> theory;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    46
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    47
structure TypecopyData = TheoryDataFun
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    48
(struct
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    49
  val name = "HOL/typecopy_package";
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    50
  type T = info Symtab.table * (serial * hook) list;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    51
  val empty = (Symtab.empty, []);
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    52
  val copy = I;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    53
  val extend = I;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    54
  fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    55
    (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    56
  fun print thy (tab, _) =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    57
    let
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    58
      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    59
        (Pretty.block o Pretty.breaks) [
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    60
          Sign.pretty_typ thy (Type (tyco, map TFree vs)),
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    61
          Pretty.str "=",
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    62
          (Pretty.str o Sign.extern_const thy) constr,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    63
          Sign.pretty_typ thy typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    64
          Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    65
        ];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    66
    in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    67
      (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    68
        Pretty.str "type copies:"
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    69
        :: map mk (Symtab.dest tab)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    70
      )
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    71
    end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    72
end);
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    73
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    74
val print = TypecopyData.print;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    75
val get_typecopies = Symtab.keys o fst o TypecopyData.get;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    76
val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    77
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    78
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    79
(* hook management *)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    80
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    81
fun add_hook hook =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    82
  (TypecopyData.map o apsnd o cons) (serial (), hook);
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    83
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    84
fun invoke_hooks tyco_info thy =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    85
  fold (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    86
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    87
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    88
(* add a type copy *)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    89
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    90
local
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    91
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
    92
fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    93
  let
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    94
    val ty = prep_typ thy raw_ty;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    95
    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
    96
    val tac = Tactic.rtac UNIV_witness 1;
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
    97
    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    98
      Rep_name = c_rep, Abs_inject = inject,
21708
45e7491bea47 reorganized structure Tactic vs. MetaSimplifier;
wenzelm
parents: 21675
diff changeset
    99
      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   100
        let
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   101
          val exists_thm =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   102
            UNIV_I
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   103
            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   104
          val inject' = inject OF [exists_thm, exists_thm];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   105
          val proj_def = inverse OF [exists_thm];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   106
          val info = {
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   107
            vs = vs,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   108
            constr = c_abs,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   109
            typ = ty_rep,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   110
            inject = inject',
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   111
            proj = (c_rep, ty_abs --> ty_rep),
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   112
            proj_def = proj_def
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   113
          };
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   114
        in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   115
          thy
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   116
          |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info)
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   117
          |> invoke_hooks (tyco, info)
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   118
          |> pair (tyco, info)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   119
        end
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   120
  in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   121
    thy
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   122
    |> setmp TypedefPackage.quiet_mode true
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   123
        (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   124
          (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   125
    |-> (fn (tyco, info) => add_info tyco info)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   126
  end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   127
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   128
in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   129
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   130
val add_typecopy = gen_add_typecopy Sign.certify_typ;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   131
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   132
end; (*local*)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   133
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   134
20835
haftmann
parents: 20597
diff changeset
   135
(* equality function equation *)
haftmann
parents: 20597
diff changeset
   136
haftmann
parents: 20597
diff changeset
   137
fun get_eq thy tyco =
haftmann
parents: 20597
diff changeset
   138
  (#inject o the o get_typecopy_info thy) tyco;
haftmann
parents: 20597
diff changeset
   139
haftmann
parents: 20597
diff changeset
   140
haftmann
parents: 20597
diff changeset
   141
(* datatype specification and certificate *)
haftmann
parents: 20597
diff changeset
   142
haftmann
parents: 20597
diff changeset
   143
fun get_spec thy tyco =
haftmann
parents: 20597
diff changeset
   144
  let
haftmann
parents: 20597
diff changeset
   145
    val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
haftmann
parents: 20597
diff changeset
   146
  in (vs, [(constr, [typ])]) end;
haftmann
parents: 20597
diff changeset
   147
haftmann
parents: 20597
diff changeset
   148
local
21708
45e7491bea47 reorganized structure Tactic vs. MetaSimplifier;
wenzelm
parents: 21675
diff changeset
   149
  val bool_eq_implies = iffD1;
20835
haftmann
parents: 20597
diff changeset
   150
  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
haftmann
parents: 20597
diff changeset
   151
in fun get_cert thy tyco =
21708
45e7491bea47 reorganized structure Tactic vs. MetaSimplifier;
wenzelm
parents: 21675
diff changeset
   152
  MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
20835
haftmann
parents: 20597
diff changeset
   153
end; (*local*)
haftmann
parents: 20597
diff changeset
   154
haftmann
parents: 20597
diff changeset
   155
haftmann
parents: 20597
diff changeset
   156
(* hook for projection function code *)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   157
21708
45e7491bea47 reorganized structure Tactic vs. MetaSimplifier;
wenzelm
parents: 21675
diff changeset
   158
fun add_project (_ , {proj_def, ...} : info) =
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20483
diff changeset
   159
  CodegenData.add_func proj_def;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   160
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   161
val setup =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   162
  TypecopyData.init
20597
65fe827aa595 code generation 2 adjustments
haftmann
parents: 20483
diff changeset
   163
  #> add_hook add_project;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   164
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   165
end; (*struct*)