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