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