src/HOL/Import/hol4rews.ML
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35021 c839a4c670c6
child 35250 92664dca6f20
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
skalberg@14620
     1
(*  Title:      HOL/Import/hol4rews.ML
skalberg@14620
     2
    Author:     Sebastian Skalberg (TU Muenchen)
skalberg@14620
     3
*)
skalberg@14620
     4
wenzelm@31971
     5
structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord);
skalberg@14516
     6
skalberg@14516
     7
type holthm = (term * term) list * thm
skalberg@14516
     8
skalberg@14516
     9
datatype ImportStatus =
wenzelm@32960
    10
         NoImport
skalberg@14516
    11
       | Generating of string
skalberg@14516
    12
       | Replaying of string
skalberg@14516
    13
wenzelm@33522
    14
structure HOL4DefThy = Theory_Data
wenzelm@22846
    15
(
wenzelm@22846
    16
  type T = ImportStatus
wenzelm@22846
    17
  val empty = NoImport
wenzelm@22846
    18
  val extend = I
wenzelm@33522
    19
  fun merge (NoImport, NoImport) = NoImport
wenzelm@33522
    20
    | merge _ = (warning "Import status set during merge"; NoImport)
wenzelm@22846
    21
)
skalberg@14516
    22
wenzelm@33522
    23
structure ImportSegment = Theory_Data
wenzelm@22846
    24
(
wenzelm@22846
    25
  type T = string
wenzelm@22846
    26
  val empty = ""
wenzelm@22846
    27
  val extend = I
wenzelm@33522
    28
  fun merge ("",arg) = arg
wenzelm@33522
    29
    | merge (arg,"") = arg
wenzelm@33522
    30
    | merge (s1,s2) =
wenzelm@22846
    31
      if s1 = s2
wenzelm@22846
    32
      then s1
wenzelm@22846
    33
      else error "Trying to merge two different import segments"
wenzelm@22846
    34
)
skalberg@14516
    35
skalberg@14516
    36
val get_import_segment = ImportSegment.get
skalberg@14516
    37
val set_import_segment = ImportSegment.put
skalberg@14516
    38
wenzelm@33522
    39
structure HOL4UNames = Theory_Data
wenzelm@22846
    40
(
wenzelm@22846
    41
  type T = string list
wenzelm@22846
    42
  val empty = []
wenzelm@22846
    43
  val extend = I
wenzelm@33522
    44
  fun merge ([], []) = []
wenzelm@33522
    45
    | merge _ = error "Used names not empty during merge"
wenzelm@22846
    46
)
skalberg@14516
    47
wenzelm@33522
    48
structure HOL4Dump = Theory_Data
wenzelm@22846
    49
(
wenzelm@22846
    50
  type T = string * string * string list
wenzelm@22846
    51
  val empty = ("","",[])
wenzelm@22846
    52
  val extend = I
wenzelm@33522
    53
  fun merge (("","",[]),("","",[])) = ("","",[])
wenzelm@33522
    54
    | merge _ = error "Dump data not empty during merge"
wenzelm@22846
    55
)
skalberg@14516
    56
wenzelm@33522
    57
structure HOL4Moves = Theory_Data
wenzelm@22846
    58
(
wenzelm@22846
    59
  type T = string Symtab.table
wenzelm@22846
    60
  val empty = Symtab.empty
wenzelm@22846
    61
  val extend = I
wenzelm@33522
    62
  fun merge data = Symtab.merge (K true) data
wenzelm@22846
    63
)
skalberg@14516
    64
wenzelm@33522
    65
structure HOL4Imports = Theory_Data
wenzelm@22846
    66
(
wenzelm@22846
    67
  type T = string Symtab.table
wenzelm@22846
    68
  val empty = Symtab.empty
wenzelm@22846
    69
  val extend = I
wenzelm@33522
    70
  fun merge data = Symtab.merge (K true) data
wenzelm@22846
    71
)
skalberg@14516
    72
skalberg@14516
    73
fun get_segment2 thyname thy =
wenzelm@17412
    74
  Symtab.lookup (HOL4Imports.get thy) thyname
skalberg@14516
    75
skalberg@14516
    76
fun set_segment thyname segname thy =
skalberg@14516
    77
    let
wenzelm@32960
    78
        val imps = HOL4Imports.get thy
wenzelm@32960
    79
        val imps' = Symtab.update_new (thyname,segname) imps
skalberg@14516
    80
    in
wenzelm@32960
    81
        HOL4Imports.put imps' thy
skalberg@14516
    82
    end
skalberg@14516
    83
wenzelm@33522
    84
structure HOL4CMoves = Theory_Data
wenzelm@22846
    85
(
wenzelm@22846
    86
  type T = string Symtab.table
wenzelm@22846
    87
  val empty = Symtab.empty
wenzelm@22846
    88
  val extend = I
wenzelm@33522
    89
  fun merge data = Symtab.merge (K true) data
wenzelm@22846
    90
)
skalberg@14516
    91
wenzelm@33522
    92
structure HOL4Maps = Theory_Data
wenzelm@22846
    93
(
wenzelm@33522
    94
  type T = string option StringPair.table
wenzelm@22846
    95
  val empty = StringPair.empty
wenzelm@22846
    96
  val extend = I
wenzelm@33522
    97
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
    98
)
skalberg@14516
    99
wenzelm@33522
   100
structure HOL4Thms = Theory_Data
wenzelm@22846
   101
(
wenzelm@22846
   102
  type T = holthm StringPair.table
wenzelm@22846
   103
  val empty = StringPair.empty
wenzelm@22846
   104
  val extend = I
wenzelm@33522
   105
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
   106
)
skalberg@14516
   107
wenzelm@33522
   108
structure HOL4ConstMaps = Theory_Data
wenzelm@22846
   109
(
wenzelm@22846
   110
  type T = (bool * string * typ option) StringPair.table
wenzelm@22846
   111
  val empty = StringPair.empty
wenzelm@22846
   112
  val extend = I
wenzelm@33522
   113
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
   114
)
skalberg@14516
   115
wenzelm@33522
   116
structure HOL4Rename = Theory_Data
wenzelm@22846
   117
(
wenzelm@22846
   118
  type T = string StringPair.table
wenzelm@22846
   119
  val empty = StringPair.empty
wenzelm@22846
   120
  val extend = I
wenzelm@33522
   121
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
   122
)
skalberg@14516
   123
wenzelm@33522
   124
structure HOL4DefMaps = Theory_Data
wenzelm@22846
   125
(
wenzelm@22846
   126
  type T = string StringPair.table
wenzelm@22846
   127
  val empty = StringPair.empty
wenzelm@22846
   128
  val extend = I
wenzelm@33522
   129
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
   130
)
skalberg@14516
   131
wenzelm@33522
   132
structure HOL4TypeMaps = Theory_Data
wenzelm@22846
   133
(
wenzelm@22846
   134
  type T = (bool * string) StringPair.table
wenzelm@22846
   135
  val empty = StringPair.empty
wenzelm@22846
   136
  val extend = I
wenzelm@33522
   137
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
   138
)
skalberg@14516
   139
wenzelm@33522
   140
structure HOL4Pending = Theory_Data
wenzelm@22846
   141
(
wenzelm@22846
   142
  type T = ((term * term) list * thm) StringPair.table
wenzelm@22846
   143
  val empty = StringPair.empty
wenzelm@22846
   144
  val extend = I
wenzelm@33522
   145
  fun merge data = StringPair.merge (K true) data
wenzelm@22846
   146
)
skalberg@14516
   147
wenzelm@33522
   148
structure HOL4Rewrites = Theory_Data
wenzelm@22846
   149
(
wenzelm@22846
   150
  type T = thm list
wenzelm@22846
   151
  val empty = []
wenzelm@22846
   152
  val extend = I
wenzelm@33522
   153
  val merge = Thm.merge_thms
wenzelm@22846
   154
)
skalberg@14516
   155
wenzelm@32740
   156
val hol4_debug = Unsynchronized.ref false
skalberg@14516
   157
fun message s = if !hol4_debug then writeln s else ()
skalberg@14516
   158
haftmann@21546
   159
local
haftmann@21546
   160
  val eq_reflection = thm "eq_reflection"
haftmann@21546
   161
in
wenzelm@20897
   162
fun add_hol4_rewrite (Context.Theory thy, th) =
skalberg@14516
   163
    let
wenzelm@32960
   164
        val _ = message "Adding HOL4 rewrite"
wenzelm@32960
   165
        val th1 = th RS eq_reflection
wenzelm@32960
   166
        val current_rews = HOL4Rewrites.get thy
wenzelm@32960
   167
        val new_rews = insert Thm.eq_thm th1 current_rews
wenzelm@32960
   168
        val updated_thy  = HOL4Rewrites.put new_rews thy
skalberg@14516
   169
    in
wenzelm@32960
   170
        (Context.Theory updated_thy,th1)
wenzelm@20897
   171
    end
haftmann@21546
   172
  | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
haftmann@21546
   173
end
skalberg@14516
   174
skalberg@14516
   175
fun ignore_hol4 bthy bthm thy =
skalberg@14516
   176
    let
wenzelm@32960
   177
        val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
wenzelm@32960
   178
        val curmaps = HOL4Maps.get thy
wenzelm@32960
   179
        val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
wenzelm@32960
   180
        val upd_thy = HOL4Maps.put newmaps thy
skalberg@14516
   181
    in
wenzelm@32960
   182
        upd_thy
skalberg@14516
   183
    end
skalberg@14516
   184
skalberg@14516
   185
val opt_get_output_thy = #2 o HOL4Dump.get
skalberg@14516
   186
skalberg@14516
   187
fun get_output_thy thy =
skalberg@14516
   188
    case #2 (HOL4Dump.get thy) of
wenzelm@32960
   189
        "" => error "No theory file being output"
skalberg@14516
   190
      | thyname => thyname
skalberg@14516
   191
skalberg@14516
   192
val get_output_dir = #1 o HOL4Dump.get
skalberg@14516
   193
skalberg@14516
   194
fun add_hol4_move bef aft thy =
skalberg@14516
   195
    let
wenzelm@32960
   196
        val curmoves = HOL4Moves.get thy
wenzelm@32960
   197
        val newmoves = Symtab.update_new (bef, aft) curmoves
skalberg@14516
   198
    in
wenzelm@32960
   199
        HOL4Moves.put newmoves thy
skalberg@14516
   200
    end
skalberg@14516
   201
skalberg@14516
   202
fun get_hol4_move bef thy =
wenzelm@17412
   203
  Symtab.lookup (HOL4Moves.get thy) bef
skalberg@14516
   204
skalberg@14516
   205
fun follow_name thmname thy =
skalberg@14516
   206
    let
wenzelm@32960
   207
        val moves = HOL4Moves.get thy
wenzelm@32960
   208
        fun F thmname =
wenzelm@32960
   209
            case Symtab.lookup moves thmname of
wenzelm@32960
   210
                SOME name => F name
wenzelm@32960
   211
              | NONE => thmname
skalberg@14516
   212
    in
wenzelm@32960
   213
        F thmname
skalberg@14516
   214
    end
skalberg@14516
   215
skalberg@14516
   216
fun add_hol4_cmove bef aft thy =
skalberg@14516
   217
    let
wenzelm@32960
   218
        val curmoves = HOL4CMoves.get thy
wenzelm@32960
   219
        val newmoves = Symtab.update_new (bef, aft) curmoves
skalberg@14516
   220
    in
wenzelm@32960
   221
        HOL4CMoves.put newmoves thy
skalberg@14516
   222
    end
skalberg@14516
   223
skalberg@14516
   224
fun get_hol4_cmove bef thy =
wenzelm@17412
   225
  Symtab.lookup (HOL4CMoves.get thy) bef
skalberg@14516
   226
skalberg@14516
   227
fun follow_cname thmname thy =
skalberg@14516
   228
    let
wenzelm@32960
   229
        val moves = HOL4CMoves.get thy
wenzelm@32960
   230
        fun F thmname =
wenzelm@32960
   231
            case Symtab.lookup moves thmname of
wenzelm@32960
   232
                SOME name => F name
wenzelm@32960
   233
              | NONE => thmname
skalberg@14516
   234
    in
wenzelm@32960
   235
        F thmname
skalberg@14516
   236
    end
skalberg@14516
   237
skalberg@14516
   238
fun add_hol4_mapping bthy bthm isathm thy =
wenzelm@32960
   239
    let 
obua@17644
   240
       (* val _ = writeln ("Before follow_name: "^isathm)  *)
obua@17644
   241
      val isathm = follow_name isathm thy
obua@17644
   242
       (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
wenzelm@32960
   243
        val curmaps = HOL4Maps.get thy
wenzelm@32960
   244
        val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
wenzelm@32960
   245
        val upd_thy = HOL4Maps.put newmaps thy
skalberg@14516
   246
    in
wenzelm@32960
   247
        upd_thy
skalberg@14516
   248
    end;
skalberg@14516
   249
skalberg@14516
   250
fun get_hol4_type_mapping bthy tycon thy =
skalberg@14516
   251
    let
wenzelm@32960
   252
        val maps = HOL4TypeMaps.get thy
skalberg@14516
   253
    in
wenzelm@32960
   254
        StringPair.lookup maps (bthy,tycon)
skalberg@14516
   255
    end
skalberg@14516
   256
skalberg@14516
   257
fun get_hol4_mapping bthy bthm thy =
skalberg@14516
   258
    let
wenzelm@32960
   259
        val curmaps = HOL4Maps.get thy
skalberg@14516
   260
    in
wenzelm@32960
   261
        StringPair.lookup curmaps (bthy,bthm)
skalberg@14516
   262
    end;
skalberg@14516
   263
skalberg@14516
   264
fun add_hol4_const_mapping bthy bconst internal isaconst thy =
skalberg@14516
   265
    let
wenzelm@32960
   266
        val thy = case opt_get_output_thy thy of
wenzelm@32960
   267
                      "" => thy
wenzelm@32960
   268
                    | output_thy => if internal
wenzelm@32960
   269
                                    then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
wenzelm@32960
   270
                                    else thy
wenzelm@32960
   271
        val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
wenzelm@32960
   272
        val curmaps = HOL4ConstMaps.get thy
wenzelm@32960
   273
        val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
wenzelm@32960
   274
        val upd_thy = HOL4ConstMaps.put newmaps thy
skalberg@14516
   275
    in
wenzelm@32960
   276
        upd_thy
skalberg@14516
   277
    end;
skalberg@14516
   278
skalberg@14516
   279
fun add_hol4_const_renaming bthy bconst newname thy =
skalberg@14516
   280
    let
wenzelm@32960
   281
        val currens = HOL4Rename.get thy
wenzelm@32960
   282
        val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
wenzelm@32960
   283
        val newrens = StringPair.update_new ((bthy,bconst),newname) currens
wenzelm@32960
   284
        val upd_thy = HOL4Rename.put newrens thy
skalberg@14516
   285
    in
wenzelm@32960
   286
        upd_thy
skalberg@14516
   287
    end;
skalberg@14516
   288
skalberg@14516
   289
fun get_hol4_const_renaming bthy bconst thy =
skalberg@14516
   290
    let
wenzelm@32960
   291
        val currens = HOL4Rename.get thy
skalberg@14516
   292
    in
wenzelm@32960
   293
        StringPair.lookup currens (bthy,bconst)
skalberg@14516
   294
    end;
skalberg@14516
   295
skalberg@14516
   296
fun get_hol4_const_mapping bthy bconst thy =
skalberg@14516
   297
    let
wenzelm@32960
   298
        val bconst = case get_hol4_const_renaming bthy bconst thy of
wenzelm@32960
   299
                         SOME name => name
wenzelm@32960
   300
                       | NONE => bconst
wenzelm@32960
   301
        val maps = HOL4ConstMaps.get thy
skalberg@14516
   302
    in
wenzelm@32960
   303
        StringPair.lookup maps (bthy,bconst)
skalberg@14516
   304
    end
skalberg@14516
   305
skalberg@14516
   306
fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
skalberg@14516
   307
    let
wenzelm@32960
   308
        val thy = case opt_get_output_thy thy of
wenzelm@32960
   309
                      "" => thy
wenzelm@32960
   310
                    | output_thy => if internal
wenzelm@32960
   311
                                    then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
wenzelm@32960
   312
                                    else thy
wenzelm@32960
   313
        val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
wenzelm@32960
   314
        val curmaps = HOL4ConstMaps.get thy
wenzelm@32960
   315
        val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
wenzelm@32960
   316
        val upd_thy = HOL4ConstMaps.put newmaps thy
skalberg@14516
   317
    in
wenzelm@32960
   318
        upd_thy
skalberg@14516
   319
    end;
skalberg@14516
   320
skalberg@14516
   321
fun add_hol4_type_mapping bthy bconst internal isaconst thy =
skalberg@14516
   322
    let
wenzelm@32960
   323
        val curmaps = HOL4TypeMaps.get thy
wenzelm@32960
   324
        val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
wenzelm@32960
   325
        val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
wenzelm@17412
   326
               handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
obua@17322
   327
                      warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
obua@17322
   328
        val upd_thy = HOL4TypeMaps.put newmaps thy
skalberg@14516
   329
    in
wenzelm@32960
   330
        upd_thy
skalberg@14516
   331
    end;
skalberg@14516
   332
skalberg@14516
   333
fun add_hol4_pending bthy bthm hth thy =
skalberg@14516
   334
    let
wenzelm@32960
   335
        val thmname = Sign.full_bname thy bthm
wenzelm@32960
   336
        val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
wenzelm@32960
   337
        val curpend = HOL4Pending.get thy
wenzelm@32960
   338
        val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
wenzelm@32960
   339
        val upd_thy = HOL4Pending.put newpend thy
wenzelm@32960
   340
        val thy' = case opt_get_output_thy upd_thy of
wenzelm@32960
   341
                       "" => add_hol4_mapping bthy bthm thmname upd_thy
wenzelm@32960
   342
                     | output_thy =>
wenzelm@32960
   343
                       let
wenzelm@32960
   344
                           val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
wenzelm@32960
   345
                       in
wenzelm@32960
   346
                           upd_thy |> add_hol4_move thmname new_thmname
wenzelm@32960
   347
                                   |> add_hol4_mapping bthy bthm new_thmname
wenzelm@32960
   348
                       end
skalberg@14516
   349
    in
wenzelm@32960
   350
        thy'
skalberg@14516
   351
    end;
skalberg@14516
   352
skalberg@14516
   353
fun get_hol4_theorem thyname thmname thy =
haftmann@21056
   354
  let
haftmann@21056
   355
    val isathms = HOL4Thms.get thy
haftmann@21056
   356
  in
haftmann@21056
   357
    StringPair.lookup isathms (thyname,thmname)
haftmann@21056
   358
  end;
skalberg@14516
   359
haftmann@21056
   360
fun add_hol4_theorem thyname thmname hth =
haftmann@21056
   361
  let
haftmann@21056
   362
    val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
haftmann@21056
   363
  in
haftmann@21056
   364
    HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
haftmann@21056
   365
  end;
skalberg@14516
   366
skalberg@14516
   367
fun export_hol4_pending thy =
haftmann@21056
   368
  let
haftmann@21056
   369
    val rews = HOL4Rewrites.get thy;
haftmann@21056
   370
    val pending = HOL4Pending.get thy;
haftmann@21056
   371
    fun process ((bthy,bthm), hth as (_,thm)) thy =
haftmann@21056
   372
      let
haftmann@21056
   373
        val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
wenzelm@35021
   374
        val thm2 = Drule.export_without_context thm1;
haftmann@21056
   375
      in
haftmann@21056
   376
        thy
haftmann@29585
   377
        |> PureThy.store_thm (Binding.name bthm, thm2)
haftmann@21056
   378
        |> snd
haftmann@21056
   379
        |> add_hol4_theorem bthy bthm hth
haftmann@21056
   380
      end;
haftmann@21056
   381
  in
haftmann@21056
   382
    thy
haftmann@21056
   383
    |> StringPair.fold process pending
haftmann@21056
   384
    |> HOL4Pending.put StringPair.empty
haftmann@21056
   385
  end;
skalberg@14516
   386
skalberg@14516
   387
fun setup_dump (dir,thyname) thy =
skalberg@15647
   388
    HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
skalberg@14516
   389
skalberg@14516
   390
fun add_dump str thy =
skalberg@14516
   391
    let
wenzelm@32960
   392
        val (dir,thyname,curdump) = HOL4Dump.get thy
skalberg@14516
   393
    in
wenzelm@32960
   394
        HOL4Dump.put (dir,thyname,str::curdump) thy
skalberg@14516
   395
    end
skalberg@14516
   396
skalberg@14516
   397
fun flush_dump thy =
skalberg@14516
   398
    let
wenzelm@32960
   399
        val (dir,thyname,dumpdata) = HOL4Dump.get thy
wenzelm@32960
   400
        val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
wenzelm@32960
   401
                                                      file=thyname ^ ".thy"})
wenzelm@32960
   402
        val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
wenzelm@32960
   403
        val  _ = TextIO.closeOut os
skalberg@14516
   404
    in
wenzelm@32960
   405
        HOL4Dump.put ("","",[]) thy
skalberg@14516
   406
    end
skalberg@14516
   407
skalberg@14516
   408
fun set_generating_thy thyname thy =
skalberg@14516
   409
    case HOL4DefThy.get thy of
wenzelm@32960
   410
        NoImport => HOL4DefThy.put (Generating thyname) thy
skalberg@14516
   411
      | _ => error "Import already in progess"
skalberg@14516
   412
skalberg@14516
   413
fun set_replaying_thy thyname thy =
skalberg@14516
   414
    case HOL4DefThy.get thy of
wenzelm@32960
   415
        NoImport => HOL4DefThy.put (Replaying thyname) thy
skalberg@14516
   416
      | _ => error "Import already in progess"
skalberg@14516
   417
skalberg@14516
   418
fun clear_import_thy thy =
skalberg@14516
   419
    case HOL4DefThy.get thy of
wenzelm@32960
   420
        NoImport => error "No import in progress"
skalberg@14516
   421
      | _ => HOL4DefThy.put NoImport thy
skalberg@14516
   422
skalberg@14516
   423
fun get_generating_thy thy =
skalberg@14516
   424
    case HOL4DefThy.get thy of
wenzelm@32960
   425
        Generating thyname => thyname
skalberg@14516
   426
      | _ => error "No theory being generated"
skalberg@14516
   427
skalberg@14516
   428
fun get_replaying_thy thy =
skalberg@14516
   429
    case HOL4DefThy.get thy of
wenzelm@32960
   430
        Replaying thyname => thyname
skalberg@14516
   431
      | _ => error "No theory being replayed"
skalberg@14516
   432
skalberg@14516
   433
fun get_import_thy thy =
skalberg@14516
   434
    case HOL4DefThy.get thy of
wenzelm@32960
   435
        Replaying thyname => thyname
skalberg@14516
   436
      | Generating thyname => thyname
skalberg@14516
   437
      | _ => error "No theory being imported"
skalberg@14516
   438
skalberg@14516
   439
fun should_ignore thyname thy thmname =
skalberg@14516
   440
    case get_hol4_mapping thyname thmname thy of
wenzelm@32960
   441
        SOME NONE => true 
skalberg@14516
   442
      | _ => false
skalberg@14516
   443
skalberg@14516
   444
val trans_string =
skalberg@14516
   445
    let
wenzelm@32960
   446
        fun quote s = "\"" ^ s ^ "\""
wenzelm@32960
   447
        fun F [] = []
wenzelm@32960
   448
          | F (#"\\" :: cs) = patch #"\\" cs
wenzelm@32960
   449
          | F (#"\"" :: cs) = patch #"\"" cs
wenzelm@32960
   450
          | F (c     :: cs) = c :: F cs
wenzelm@32960
   451
        and patch c rest = #"\\" :: c :: F rest
skalberg@14516
   452
    in
wenzelm@32960
   453
        quote o String.implode o F o String.explode
skalberg@14516
   454
    end
skalberg@14516
   455
skalberg@14516
   456
fun dump_import_thy thyname thy =
skalberg@14516
   457
    let
wenzelm@32960
   458
        val output_dir = get_output_dir thy
wenzelm@32960
   459
        val output_thy = get_output_thy thy
wenzelm@32960
   460
        val input_thy = Context.theory_name thy
wenzelm@32960
   461
        val import_segment = get_import_segment thy
wenzelm@32960
   462
        val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
wenzelm@32960
   463
                                                      file=thyname ^ ".imp"})
wenzelm@32960
   464
        fun out s = TextIO.output(os,s)
haftmann@21056
   465
    val (ignored, mapped) = StringPair.fold
haftmann@21056
   466
      (fn ((bthy, bthm), v) => fn (ign, map) =>
haftmann@21056
   467
        if bthy = thyname
haftmann@21056
   468
        then case v
haftmann@21056
   469
         of NONE => (bthm :: ign, map)
haftmann@21056
   470
          | SOME w => (ign, (bthm, w) :: map)
haftmann@21056
   471
        else (ign, map)) (HOL4Maps.get thy) ([],[]);
haftmann@21056
   472
    fun mk init = StringPair.fold
haftmann@21056
   473
      (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
haftmann@21056
   474
    val constmaps = mk (HOL4ConstMaps.get thy);
haftmann@21056
   475
    val constrenames = mk (HOL4Rename.get thy);
haftmann@21056
   476
    val typemaps = mk (HOL4TypeMaps.get thy);
haftmann@21056
   477
    val defmaps = mk (HOL4DefMaps.get thy);
wenzelm@32960
   478
        fun new_name internal isa =
wenzelm@32960
   479
            if internal
wenzelm@32960
   480
            then
wenzelm@32960
   481
                let
wenzelm@32960
   482
                    val paths = Long_Name.explode isa
haftmann@33955
   483
                    val i = drop (length paths - 2) paths
wenzelm@32960
   484
                in
wenzelm@32960
   485
                    case i of
wenzelm@32960
   486
                        [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
wenzelm@32960
   487
                      | _ => error "hol4rews.dump internal error"
wenzelm@32960
   488
                end
wenzelm@32960
   489
            else
wenzelm@32960
   490
                isa
skalberg@14516
   491
wenzelm@32960
   492
        val _ = out "import\n\n"
skalberg@14516
   493
wenzelm@32960
   494
        val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
wenzelm@32960
   495
        val _ = if null defmaps
wenzelm@32960
   496
                then ()
wenzelm@32960
   497
                else out "def_maps"
wenzelm@32960
   498
        val _ = app (fn (hol,isa) =>
wenzelm@32960
   499
                        out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
wenzelm@32960
   500
        val _ = if null defmaps
wenzelm@32960
   501
                then ()
wenzelm@32960
   502
                else out "\n\n"
skalberg@14516
   503
wenzelm@32960
   504
        val _ = if null typemaps
wenzelm@32960
   505
                then ()
wenzelm@32960
   506
                else out "type_maps"
wenzelm@32960
   507
        val _ = app (fn (hol,(internal,isa)) =>
wenzelm@32960
   508
                        out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
wenzelm@32960
   509
        val _ = if null typemaps
wenzelm@32960
   510
                then ()
wenzelm@32960
   511
                else out "\n\n"
skalberg@14516
   512
wenzelm@32960
   513
        val _ = if null constmaps
wenzelm@32960
   514
                then ()
wenzelm@32960
   515
                else out "const_maps"
wenzelm@32960
   516
        val _ = app (fn (hol,(internal,isa,opt_ty)) =>
wenzelm@32960
   517
                        (out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
wenzelm@32960
   518
                         case opt_ty of
wenzelm@32960
   519
                             SOME ty => out (" :: \"" ^ Syntax.string_of_typ_global thy ty ^ "\"")
wenzelm@32960
   520
                           | NONE => ())) constmaps
wenzelm@32960
   521
        val _ = if null constmaps
wenzelm@32960
   522
                then ()
wenzelm@32960
   523
                else out "\n\n"
skalberg@14516
   524
wenzelm@32960
   525
        val _ = if null constrenames
wenzelm@32960
   526
                then ()
wenzelm@32960
   527
                else out "const_renames"
wenzelm@32960
   528
        val _ = app (fn (old,new) =>
wenzelm@32960
   529
                        out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
wenzelm@32960
   530
        val _ = if null constrenames
wenzelm@32960
   531
                then ()
wenzelm@32960
   532
                else out "\n\n"
skalberg@14516
   533
wenzelm@32960
   534
        fun gen2replay in_thy out_thy s = 
wenzelm@32960
   535
            let
wenzelm@32960
   536
                val ss = Long_Name.explode s
wenzelm@32960
   537
            in
wenzelm@32960
   538
                if (hd ss = in_thy) then 
wenzelm@32960
   539
                    Long_Name.implode (out_thy::(tl ss))
wenzelm@32960
   540
                else
wenzelm@32960
   541
                    s
wenzelm@32960
   542
            end 
obua@17607
   543
wenzelm@32960
   544
        val _ = if null mapped
wenzelm@32960
   545
                then ()
wenzelm@32960
   546
                else out "thm_maps"
wenzelm@32960
   547
        val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
wenzelm@32960
   548
        val _ = if null mapped 
wenzelm@32960
   549
                then ()
wenzelm@32960
   550
                else out "\n\n"
skalberg@14516
   551
wenzelm@32960
   552
        val _ = if null ignored
wenzelm@32960
   553
                then ()
wenzelm@32960
   554
                else out "ignore_thms"
wenzelm@32960
   555
        val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored
wenzelm@32960
   556
        val _ = if null ignored
wenzelm@32960
   557
                then ()
wenzelm@32960
   558
                else out "\n\n"
skalberg@14516
   559
wenzelm@32960
   560
        val _ = out "end\n"
wenzelm@32960
   561
        val _ = TextIO.closeOut os
skalberg@14516
   562
    in
wenzelm@32960
   563
        thy
skalberg@14516
   564
    end
skalberg@14516
   565
skalberg@14516
   566
fun set_used_names names thy =
skalberg@14516
   567
    let
wenzelm@32960
   568
        val unames = HOL4UNames.get thy
skalberg@14516
   569
    in
wenzelm@32960
   570
        case unames of
wenzelm@32960
   571
            [] => HOL4UNames.put names thy
wenzelm@32960
   572
          | _ => error "hol4rews.set_used_names called on initialized data!"
skalberg@14516
   573
    end
skalberg@14516
   574
wenzelm@22846
   575
val clear_used_names = HOL4UNames.put [];
skalberg@14516
   576
skalberg@14516
   577
fun get_defmap thyname const thy =
skalberg@14516
   578
    let
wenzelm@32960
   579
        val maps = HOL4DefMaps.get thy
skalberg@14516
   580
    in
wenzelm@32960
   581
        StringPair.lookup maps (thyname,const)
skalberg@14516
   582
    end
skalberg@14516
   583
skalberg@14516
   584
fun add_defmap thyname const defname thy =
skalberg@14516
   585
    let
wenzelm@32960
   586
        val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
wenzelm@32960
   587
        val maps = HOL4DefMaps.get thy
wenzelm@32960
   588
        val maps' = StringPair.update_new ((thyname,const),defname) maps
wenzelm@32960
   589
        val thy' = HOL4DefMaps.put maps' thy
skalberg@14516
   590
    in
wenzelm@32960
   591
        thy'
skalberg@14516
   592
    end
skalberg@14516
   593
skalberg@14516
   594
fun get_defname thyname name thy =
skalberg@14516
   595
    let
wenzelm@32960
   596
        val maps = HOL4DefMaps.get thy
wenzelm@32960
   597
        fun F dname = (dname,add_defmap thyname name dname thy)
skalberg@14516
   598
    in
wenzelm@32960
   599
        case StringPair.lookup maps (thyname,name) of
wenzelm@32960
   600
            SOME thmname => (thmname,thy)
wenzelm@32960
   601
          | NONE =>
wenzelm@32960
   602
            let
wenzelm@32960
   603
                val used = HOL4UNames.get thy
wenzelm@32960
   604
                val defname = Thm.def_name name
wenzelm@32960
   605
                val pdefname = name ^ "_primdef"
wenzelm@32960
   606
            in
wenzelm@32960
   607
                if not (defname mem used)
wenzelm@32960
   608
                then F defname                 (* name_def *)
wenzelm@32960
   609
                else if not (pdefname mem used)
wenzelm@32960
   610
                then F pdefname                (* name_primdef *)
wenzelm@32960
   611
                else F (Name.variant used pdefname) (* last resort *)
wenzelm@32960
   612
            end
skalberg@14516
   613
    end
skalberg@14516
   614
skalberg@14516
   615
local
skalberg@14516
   616
    fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
skalberg@14516
   617
      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
skalberg@14516
   618
      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
skalberg@14516
   619
      | handle_meta [x] = Appl[Constant "Trueprop",x]
skalberg@14518
   620
      | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
skalberg@14516
   621
in
skalberg@14516
   622
val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
skalberg@14516
   623
end
skalberg@14516
   624
skalberg@14516
   625
local
skalberg@14516
   626
    fun initial_maps thy =
wenzelm@32960
   627
        thy |> add_hol4_type_mapping "min" "bool" false "bool"
wenzelm@32960
   628
            |> add_hol4_type_mapping "min" "fun" false "fun"
wenzelm@32960
   629
            |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
wenzelm@32960
   630
            |> add_hol4_const_mapping "min" "=" false "op ="
wenzelm@32960
   631
            |> add_hol4_const_mapping "min" "==>" false "op -->"
wenzelm@32960
   632
            |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
skalberg@14516
   633
in
skalberg@14516
   634
val hol4_setup =
wenzelm@18708
   635
  initial_maps #>
wenzelm@30528
   636
  Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
wenzelm@30528
   637
skalberg@14516
   638
end