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