src/HOL/Import/import_data.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 59936 b8ffc3dc9e24
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Import/import_data.ML
     2     Author:     Cezary Kaliszyk, University of Innsbruck
     3     Author:     Alexander Krauss, QAware GmbH
     4 
     5 Importer data.
     6 *)
     7 
     8 signature IMPORT_DATA =
     9 sig
    10   val get_const_map : string -> theory -> string option
    11   val get_typ_map : string -> theory -> string option
    12   val get_const_def : string -> theory -> thm option
    13   val get_typ_def : string -> theory -> thm option
    14 
    15   val add_const_map : string -> string -> theory -> theory
    16   val add_const_map_cmd : string -> string -> theory -> theory
    17   val add_typ_map : string -> string -> theory -> theory
    18   val add_typ_map_cmd : string -> string -> theory -> theory
    19   val add_const_def : string -> thm -> string option -> theory -> theory
    20   val add_typ_def : string -> string -> string -> thm -> theory -> theory
    21 end
    22 
    23 structure Import_Data: IMPORT_DATA =
    24 struct
    25 
    26 structure Data = Theory_Data
    27 (
    28   type T = {const_map: string Symtab.table, ty_map: string Symtab.table,
    29             const_def: thm Symtab.table, ty_def: thm Symtab.table}
    30   val empty = {const_map = Symtab.empty, ty_map = Symtab.empty,
    31                const_def = Symtab.empty, ty_def = Symtab.empty}
    32   val extend = I
    33   fun merge
    34    ({const_map = cm1, ty_map = tm1, const_def = cd1, ty_def = td1},
    35     {const_map = cm2, ty_map = tm2, const_def = cd2, ty_def = td2}) : T =
    36     {const_map = Symtab.merge (K true) (cm1, cm2), ty_map = Symtab.merge (K true) (tm1, tm2),
    37      const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)
    38     }
    39 )
    40 
    41 fun get_const_map s thy = Symtab.lookup (#const_map (Data.get thy)) s
    42 
    43 fun get_typ_map s thy = Symtab.lookup (#ty_map (Data.get thy)) s
    44 
    45 fun get_const_def s thy = Symtab.lookup (#const_def (Data.get thy)) s
    46 
    47 fun get_typ_def s thy = Symtab.lookup (#ty_def (Data.get thy)) s
    48 
    49 fun add_const_map s1 s2 thy =
    50   Data.map (fn {const_map, ty_map, const_def, ty_def} =>
    51     {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
    52      const_def = const_def, ty_def = ty_def}) thy
    53 
    54 fun add_const_map_cmd s1 raw_s2 thy =
    55   let
    56     val ctxt = Proof_Context.init_global thy
    57     val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
    58   in add_const_map s1 s2 thy end
    59 
    60 fun add_typ_map s1 s2 thy =
    61   Data.map (fn {const_map, ty_map, const_def, ty_def} =>
    62     {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
    63      const_def = const_def, ty_def = ty_def}) thy
    64 
    65 fun add_typ_map_cmd s1 raw_s2 thy =
    66   let
    67     val ctxt = Proof_Context.init_global thy
    68     val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
    69   in add_typ_map s1 s2 thy end
    70 
    71 fun add_const_def s th name_opt thy =
    72   let
    73     val th = Thm.legacy_freezeT th
    74     val name = case name_opt of
    75          NONE => (fst o dest_Const o fst o HOLogic.dest_eq o
    76            HOLogic.dest_Trueprop o Thm.prop_of) th
    77        | SOME n => n
    78     val thy' = add_const_map s name thy
    79   in
    80     Data.map (fn {const_map, ty_map, const_def, ty_def} =>
    81       {const_map = const_map, ty_map = ty_map,
    82        const_def = (Symtab.update (s, th) const_def), ty_def = ty_def}) thy'
    83   end
    84 
    85 fun add_typ_def tyname absname repname th thy =
    86   let
    87     val th = Thm.legacy_freezeT th
    88     val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th))
    89     val (l, abst) = dest_comb l
    90     val (_, rept) = dest_comb l
    91     val (absn, _) = dest_Const abst
    92     val (repn, _) = dest_Const rept
    93     val nty = domain_type (fastype_of rept)
    94     val ntyn = fst (dest_Type nty)
    95     val thy2 = add_typ_map tyname ntyn thy
    96     val thy3 = add_const_map absname absn thy2
    97     val thy4 = add_const_map repname repn thy3
    98   in
    99     Data.map (fn {const_map, ty_map, const_def, ty_def} =>
   100       {const_map = const_map, ty_map = ty_map,
   101        const_def = const_def, ty_def = (Symtab.update (tyname, th) ty_def)}) thy4
   102   end
   103 
   104 val _ = Theory.setup
   105   (Attrib.setup @{binding import_const}
   106     (Scan.lift Parse.name --
   107       Scan.option (Scan.lift @{keyword ":"} |-- Args.const {proper = true, strict = false}) >>
   108       (fn (s1, s2) => Thm.declaration_attribute
   109         (fn th => Context.mapping (add_const_def s1 th s2) I)))
   110   "declare a theorem as an equality that maps the given constant")
   111 
   112 val _ = Theory.setup
   113   (Attrib.setup @{binding import_type}
   114     (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
   115       (fn ((tyname, absname), repname) => Thm.declaration_attribute
   116         (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
   117   "declare a type_definition theorem as a map for an imported type with abs and rep")
   118 
   119 val _ =
   120   Outer_Syntax.command @{command_keyword import_type_map}
   121     "map external type name to existing Isabelle/HOL type name"
   122     ((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
   123       (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
   124 
   125 val _ =
   126   Outer_Syntax.command @{command_keyword import_const_map}
   127     "map external const name to existing Isabelle/HOL const name"
   128     ((Parse.name --| @{keyword ":"}) -- Parse.const >>
   129       (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
   130 
   131 (* Initial type and constant maps, for types and constants that are not
   132    defined, which means their definitions do not appear in the proof dump *)
   133 val _ = Theory.setup
   134   (add_typ_map "bool" @{type_name bool} #>
   135   add_typ_map "fun" @{type_name fun} #>
   136   add_typ_map "ind" @{type_name ind} #>
   137   add_const_map "=" @{const_name HOL.eq} #>
   138   add_const_map "@" @{const_name "Eps"})
   139 
   140 end