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