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