src/HOL/Tools/typecopy_package.ML
author wenzelm
Wed, 31 Dec 2008 18:53:17 +0100
changeset 29272 fb3ccf499df5
parent 28965 1de908189869
child 29875 4a1510b5f886
permissions -rw-r--r--
use regular Term.add_XXX etc.;
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
    Author:     Florian Haftmann, TU Muenchen
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     3
20855
9f60d493c8fe clarified header comments
haftmann
parents: 20835
diff changeset
     4
Introducing copies of types using trivial typedefs; datatype-like abstraction.
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     5
*)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     6
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     7
signature TYPECOPY_PACKAGE =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     8
sig
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     9
  type info = {
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    10
    vs: (string * sort) list,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    11
    constr: string,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    12
    typ: typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    13
    inject: thm,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    14
    proj: string * typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    15
    proj_def: thm
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    16
  }
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    17
  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
    18
    -> theory -> (string * info) * theory
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    19
  val get_typecopies: theory -> string list
25506
haftmann
parents: 25489
diff changeset
    20
  val get_info: theory -> string -> info option
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
    21
  val interpretation: (string -> theory -> theory) -> theory -> theory
28664
haftmann
parents: 28423
diff changeset
    22
  val add_typecopy_default_code: string -> theory -> theory
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    23
  val print_typecopies: theory -> unit
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    24
  val setup: theory -> theory
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    25
end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    26
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    27
structure TypecopyPackage: TYPECOPY_PACKAGE =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    28
struct
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    29
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    30
(* theory data *)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    31
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    32
type info = {
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    33
  vs: (string * sort) list,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    34
  constr: string,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    35
  typ: typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    36
  inject: thm,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    37
  proj: string * typ,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    38
  proj_def: thm
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    39
};
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    40
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    41
structure TypecopyData = TheoryDataFun
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    42
(
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    43
  type T = info Symtab.table;
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    44
  val empty = Symtab.empty;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    45
  val copy = I;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    46
  val extend = I;
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    47
  fun merge _ = Symtab.merge (K true);
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    48
);
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    49
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    50
fun print_typecopies thy =
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    51
  let
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    52
    val tab = TypecopyData.get thy;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    53
    fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    54
      (Pretty.block o Pretty.breaks) [
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26732
diff changeset
    55
        Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    56
        Pretty.str "=",
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    57
        (Pretty.str o Sign.extern_const thy) constr,
26939
1035c89b4c02 moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents: 26732
diff changeset
    58
        Syntax.pretty_typ_global thy typ,
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    59
        Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    60
    in
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    61
      (Pretty.writeln o Pretty.block o Pretty.fbreaks)
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    62
        (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    63
    end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    64
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    65
val get_typecopies = Symtab.keys o TypecopyData.get;
25506
haftmann
parents: 25489
diff changeset
    66
val get_info = Symtab.lookup o TypecopyData.get;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    67
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    68
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
    69
(* interpretation of type copies *)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    70
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24626
diff changeset
    71
structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
    72
val interpretation = TypecopyInterpretation.interpretation;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    73
28664
haftmann
parents: 28423
diff changeset
    74
fun add_typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    75
  let
28664
haftmann
parents: 28423
diff changeset
    76
    val ty = Sign.certify_typ thy raw_ty;
29272
fb3ccf499df5 use regular Term.add_XXX etc.;
wenzelm
parents: 28965
diff changeset
    77
    val vs =
fb3ccf499df5 use regular Term.add_XXX etc.;
wenzelm
parents: 28965
diff changeset
    78
      AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    79
    val tac = Tactic.rtac UNIV_witness 1;
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
    80
    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
    81
      Rep_name = c_rep, Abs_inject = inject,
21708
45e7491bea47 reorganized structure Tactic vs. MetaSimplifier;
wenzelm
parents: 21675
diff changeset
    82
      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    83
        let
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    84
          val exists_thm =
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    85
            UNIV_I
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    86
            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    87
          val inject' = inject OF [exists_thm, exists_thm];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    88
          val proj_def = inverse OF [exists_thm];
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    89
          val info = {
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    90
            vs = vs,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    91
            constr = c_abs,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    92
            typ = ty_rep,
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    93
            inject = inject',
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    94
            proj = (c_rep, ty_abs --> ty_rep),
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    95
            proj_def = proj_def
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    96
          };
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    97
        in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    98
          thy
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    99
          |> (TypecopyData.map o Symtab.update_new) (tyco, info)
24711
e8bba7723858 simplified interpretation setup;
wenzelm
parents: 24626
diff changeset
   100
          |> TypecopyInterpretation.data tyco
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   101
          |> pair (tyco, info)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   102
        end
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   103
  in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   104
    thy
28664
haftmann
parents: 28423
diff changeset
   105
    |> TypedefPackage.add_typedef false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
26475
3cc1e48d0ce1 eliminated quiet_mode ref of some packages (avoid CRITICAL setmp!);
wenzelm
parents: 25864
diff changeset
   106
      (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
   107
    |-> (fn (tyco, info) => add_info tyco info)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   108
  end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   109
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   110
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   111
(* code generator setup *)
20835
haftmann
parents: 20597
diff changeset
   112
28664
haftmann
parents: 28423
diff changeset
   113
fun add_typecopy_default_code tyco thy =
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   114
  let
28664
haftmann
parents: 28423
diff changeset
   115
    val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
haftmann
parents: 28423
diff changeset
   116
      typ = raw_ty_rep, ... } =  get_info thy tyco;
haftmann
parents: 28423
diff changeset
   117
    val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy)
haftmann
parents: 28423
diff changeset
   118
      (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]);
haftmann
parents: 28423
diff changeset
   119
    val ty_inst = Logic.varifyT
haftmann
parents: 28423
diff changeset
   120
      #> inst_meet
haftmann
parents: 28423
diff changeset
   121
      #> Logic.unvarifyT;
haftmann
parents: 28423
diff changeset
   122
    val vs = (map dest_TFree o snd o dest_Type o ty_inst)
haftmann
parents: 28423
diff changeset
   123
      (Type (tyco, map TFree raw_vs));
haftmann
parents: 28423
diff changeset
   124
    val ty_rep = ty_inst raw_ty_rep;
haftmann
parents: 28423
diff changeset
   125
    val SOME { Rep_inject = proj_inject, ... } = TypedefPackage.get_info thy tyco;
haftmann
parents: 28423
diff changeset
   126
    val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr_name);
haftmann
parents: 28423
diff changeset
   127
    val constr = (constr_name, ty_constr)
28423
9fc3befd8191 clarified codegen interfaces
haftmann
parents: 28394
diff changeset
   128
    val ty = Type (tyco, map TFree vs);
28664
haftmann
parents: 28423
diff changeset
   129
    fun mk_eq ty t_x t_y = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
haftmann
parents: 28423
diff changeset
   130
      $ t_x $ t_y;
haftmann
parents: 28423
diff changeset
   131
    fun mk_proj t = Const (proj, ty --> ty_rep) $ t;
haftmann
parents: 28423
diff changeset
   132
    val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
haftmann
parents: 28423
diff changeset
   133
    val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
haftmann
parents: 28423
diff changeset
   134
      (mk_eq ty t_x t_y, mk_eq ty_rep (mk_proj t_x) (mk_proj t_y));
haftmann
parents: 28423
diff changeset
   135
    fun mk_eq_refl thy = @{thm HOL.eq_refl}
haftmann
parents: 28423
diff changeset
   136
      |> Thm.instantiate
haftmann
parents: 28423
diff changeset
   137
         ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], [])
haftmann
parents: 28423
diff changeset
   138
      |> AxClass.unoverload thy;
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   139
  in
25506
haftmann
parents: 25489
diff changeset
   140
    thy
28664
haftmann
parents: 28423
diff changeset
   141
    |> Code.add_datatype [constr]
haftmann
parents: 28423
diff changeset
   142
    |> Code.add_eqn proj_eq
28423
9fc3befd8191 clarified codegen interfaces
haftmann
parents: 28394
diff changeset
   143
    |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
28664
haftmann
parents: 28423
diff changeset
   144
    |> `(fn lthy => Syntax.check_term lthy def_eq)
haftmann
parents: 28423
diff changeset
   145
    |-> (fn def_eq => Specification.definition
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28664
diff changeset
   146
         (NONE, (Attrib.empty_binding, def_eq)))
28664
haftmann
parents: 28423
diff changeset
   147
    |-> (fn (_, (_, def_thm)) =>
haftmann
parents: 28423
diff changeset
   148
       Class.prove_instantiation_exit_result Morphism.thm
haftmann
parents: 28423
diff changeset
   149
         (fn _ => fn def_thm => Class.intro_classes_tac []
haftmann
parents: 28423
diff changeset
   150
            THEN (Simplifier.rewrite_goals_tac
haftmann
parents: 28423
diff changeset
   151
              (map Simpdata.mk_eq [def_thm, @{thm eq}, proj_inject]))
haftmann
parents: 28423
diff changeset
   152
                THEN ALLGOALS (rtac @{thm refl})) def_thm)
haftmann
parents: 28423
diff changeset
   153
    |-> (fn def_thm => Code.add_eqn def_thm)
haftmann
parents: 28423
diff changeset
   154
    |> `(fn thy => mk_eq_refl thy)
haftmann
parents: 28423
diff changeset
   155
    |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm)
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   156
  end;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   157
28664
haftmann
parents: 28423
diff changeset
   158
fun perhaps_add_typecopy_default_code tyco thy =
haftmann
parents: 28423
diff changeset
   159
  add_typecopy_default_code tyco thy handle Sorts.CLASS_ERROR _ => thy;
haftmann
parents: 28423
diff changeset
   160
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   161
val setup =
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   162
  TypecopyInterpretation.init
28664
haftmann
parents: 28423
diff changeset
   163
  #> interpretation perhaps_add_typecopy_default_code
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   164
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
   165
end;