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