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