src/HOL/Tools/typecopy_package.ML
author wenzelm
Tue Sep 25 15:34:35 2007 +0200 (2007-09-25)
changeset 24711 e8bba7723858
parent 24626 85eceef2edc7
child 25489 5b0625f6e324
permissions -rw-r--r--
simplified interpretation setup;
     1 (*  Title:      HOL/Tools/typecopy_package.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Introducing copies of types using trivial typedefs; datatype-like abstraction.
     6 *)
     7 
     8 signature TYPECOPY_PACKAGE =
     9 sig
    10   type info = {
    11     vs: (string * sort) list,
    12     constr: string,
    13     typ: typ,
    14     inject: thm,
    15     proj: string * typ,
    16     proj_def: thm
    17   }
    18   val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
    19     -> theory -> (string * info) * theory
    20   val get_typecopies: theory -> string list
    21   val get_typecopy_info: theory -> string -> info option
    22   val interpretation: (string * info -> theory -> theory) -> theory -> theory
    23   val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    24   val get_eq: theory -> string -> thm
    25   val print_typecopies: theory -> unit
    26   val setup: theory -> theory
    27 end;
    28 
    29 structure TypecopyPackage: TYPECOPY_PACKAGE =
    30 struct
    31 
    32 (* theory data *)
    33 
    34 type info = {
    35   vs: (string * sort) list,
    36   constr: string,
    37   typ: typ,
    38   inject: thm,
    39   proj: string * typ,
    40   proj_def: thm
    41 };
    42 
    43 structure TypecopyData = TheoryDataFun
    44 (
    45   type T = info Symtab.table;
    46   val empty = Symtab.empty;
    47   val copy = I;
    48   val extend = I;
    49   fun merge _ = Symtab.merge (K true);
    50 );
    51 
    52 fun print_typecopies thy =
    53   let
    54     val tab = TypecopyData.get thy;
    55     fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
    56       (Pretty.block o Pretty.breaks) [
    57         Sign.pretty_typ thy (Type (tyco, map TFree vs)),
    58         Pretty.str "=",
    59         (Pretty.str o Sign.extern_const thy) constr,
    60         Sign.pretty_typ thy typ,
    61         Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
    62     in
    63       (Pretty.writeln o Pretty.block o Pretty.fbreaks)
    64         (Pretty.str "type copies:" :: map mk (Symtab.dest tab))
    65     end;
    66 
    67 val get_typecopies = Symtab.keys o TypecopyData.get;
    68 val get_typecopy_info = Symtab.lookup o TypecopyData.get;
    69 
    70 
    71 (* interpretation *)
    72 
    73 structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
    74 
    75 fun interpretation interp = TypecopyInterpretation.interpretation
    76   (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy);
    77 
    78 
    79 (* add a type copy *)
    80 
    81 local
    82 
    83 fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
    84   let
    85     val ty = prep_typ thy raw_ty;
    86     val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
    87     val tac = Tactic.rtac UNIV_witness 1;
    88     fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    89       Rep_name = c_rep, Abs_inject = inject,
    90       Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
    91         let
    92           val exists_thm =
    93             UNIV_I
    94             |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
    95           val inject' = inject OF [exists_thm, exists_thm];
    96           val proj_def = inverse OF [exists_thm];
    97           val info = {
    98             vs = vs,
    99             constr = c_abs,
   100             typ = ty_rep,
   101             inject = inject',
   102             proj = (c_rep, ty_abs --> ty_rep),
   103             proj_def = proj_def
   104           };
   105         in
   106           thy
   107           |> (TypecopyData.map o Symtab.update_new) (tyco, info)
   108           |> TypecopyInterpretation.data tyco
   109           |> pair (tyco, info)
   110         end
   111   in
   112     thy
   113     |> setmp TypedefPackage.quiet_mode true
   114         (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
   115           (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac
   116     |-> (fn (tyco, info) => add_info tyco info)
   117   end;
   118 
   119 in
   120 
   121 val add_typecopy = gen_add_typecopy Sign.certify_typ;
   122 
   123 end;
   124 
   125 
   126 (* equality function equation and datatype specification *)
   127 
   128 fun get_eq thy tyco =
   129   (#inject o the o get_typecopy_info thy) tyco;
   130 
   131 fun get_spec thy tyco =
   132   let
   133     val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
   134   in (vs, [(constr, [typ])]) end;
   135 
   136 
   137 (* interpretation for projection function code *)
   138 
   139 fun add_project (_, {proj_def, ...} : info) = Code.add_default_func proj_def;
   140 
   141 val setup = TypecopyInterpretation.init #> interpretation add_project;
   142 
   143 end;