src/HOL/Import/hol4rews.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18358 0a733e11021a
child 18728 6790126ab5f6
permissions -rw-r--r--
setup: theory -> theory;
     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 (thy,th) =
   262     let
   263 	val _ = message "Adding HOL4 rewrite"
   264 	val th1 = th RS eq_reflection
   265 	val current_rews = HOL4Rewrites.get thy
   266 	val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
   267 	val updated_thy  = HOL4Rewrites.put new_rews thy
   268     in
   269 	(updated_thy,th1)
   270     end;
   271 
   272 fun ignore_hol4 bthy bthm thy =
   273     let
   274 	val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
   275 	val curmaps = HOL4Maps.get thy
   276 	val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
   277 	val upd_thy = HOL4Maps.put newmaps thy
   278     in
   279 	upd_thy
   280     end
   281 
   282 val opt_get_output_thy = #2 o HOL4Dump.get
   283 
   284 fun get_output_thy thy =
   285     case #2 (HOL4Dump.get thy) of
   286 	"" => error "No theory file being output"
   287       | thyname => thyname
   288 
   289 val get_output_dir = #1 o HOL4Dump.get
   290 
   291 fun add_hol4_move bef aft thy =
   292     let
   293 	val curmoves = HOL4Moves.get thy
   294 	val newmoves = Symtab.update_new (bef, aft) curmoves
   295     in
   296 	HOL4Moves.put newmoves thy
   297     end
   298 
   299 fun get_hol4_move bef thy =
   300   Symtab.lookup (HOL4Moves.get thy) bef
   301 
   302 fun follow_name thmname thy =
   303     let
   304 	val moves = HOL4Moves.get thy
   305 	fun F thmname =
   306 	    case Symtab.lookup moves thmname of
   307 		SOME name => F name
   308 	      | NONE => thmname
   309     in
   310 	F thmname
   311     end
   312 
   313 fun add_hol4_cmove bef aft thy =
   314     let
   315 	val curmoves = HOL4CMoves.get thy
   316 	val newmoves = Symtab.update_new (bef, aft) curmoves
   317     in
   318 	HOL4CMoves.put newmoves thy
   319     end
   320 
   321 fun get_hol4_cmove bef thy =
   322   Symtab.lookup (HOL4CMoves.get thy) bef
   323 
   324 fun follow_cname thmname thy =
   325     let
   326 	val moves = HOL4CMoves.get thy
   327 	fun F thmname =
   328 	    case Symtab.lookup moves thmname of
   329 		SOME name => F name
   330 	      | NONE => thmname
   331     in
   332 	F thmname
   333     end
   334 
   335 fun add_hol4_mapping bthy bthm isathm thy =
   336     let	
   337        (* val _ = writeln ("Before follow_name: "^isathm)  *)
   338       val isathm = follow_name isathm thy
   339        (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
   340 	val curmaps = HOL4Maps.get thy
   341 	val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
   342 	val upd_thy = HOL4Maps.put newmaps thy
   343     in
   344 	upd_thy
   345     end;
   346 
   347 fun get_hol4_type_mapping bthy tycon thy =
   348     let
   349 	val maps = HOL4TypeMaps.get thy
   350     in
   351 	StringPair.lookup maps (bthy,tycon)
   352     end
   353 
   354 fun get_hol4_mapping bthy bthm thy =
   355     let
   356 	val curmaps = HOL4Maps.get thy
   357     in
   358 	StringPair.lookup curmaps (bthy,bthm)
   359     end;
   360 
   361 fun add_hol4_const_mapping bthy bconst internal isaconst thy =
   362     let
   363 	val thy = case opt_get_output_thy thy of
   364 		      "" => thy
   365 		    | output_thy => if internal
   366 				    then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   367 				    else thy
   368 	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   369 	val curmaps = HOL4ConstMaps.get thy
   370 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
   371 	val upd_thy = HOL4ConstMaps.put newmaps thy
   372     in
   373 	upd_thy
   374     end;
   375 
   376 fun add_hol4_const_renaming bthy bconst newname thy =
   377     let
   378 	val currens = HOL4Rename.get thy
   379 	val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
   380 	val newrens = StringPair.update_new ((bthy,bconst),newname) currens
   381 	val upd_thy = HOL4Rename.put newrens thy
   382     in
   383 	upd_thy
   384     end;
   385 
   386 fun get_hol4_const_renaming bthy bconst thy =
   387     let
   388 	val currens = HOL4Rename.get thy
   389     in
   390 	StringPair.lookup currens (bthy,bconst)
   391     end;
   392 
   393 fun get_hol4_const_mapping bthy bconst thy =
   394     let
   395 	val bconst = case get_hol4_const_renaming bthy bconst thy of
   396 			 SOME name => name
   397 		       | NONE => bconst
   398 	val maps = HOL4ConstMaps.get thy
   399     in
   400 	StringPair.lookup maps (bthy,bconst)
   401     end
   402 
   403 fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
   404     let
   405 	val thy = case opt_get_output_thy thy of
   406 		      "" => thy
   407 		    | output_thy => if internal
   408 				    then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   409 				    else thy
   410 	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   411 	val curmaps = HOL4ConstMaps.get thy
   412 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
   413 	val upd_thy = HOL4ConstMaps.put newmaps thy
   414     in
   415 	upd_thy
   416     end;
   417 
   418 fun add_hol4_type_mapping bthy bconst internal isaconst thy =
   419     let
   420 	val curmaps = HOL4TypeMaps.get thy
   421 	val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   422 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
   423                handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
   424                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
   425         val upd_thy = HOL4TypeMaps.put newmaps thy
   426     in
   427 	upd_thy
   428     end;
   429 
   430 fun add_hol4_pending bthy bthm hth thy =
   431     let
   432 	val thmname = Sign.full_name (sign_of thy) bthm
   433 	val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
   434 	val curpend = HOL4Pending.get thy
   435 	val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
   436 	val upd_thy = HOL4Pending.put newpend thy
   437 	val thy' = case opt_get_output_thy upd_thy of
   438 		       "" => add_hol4_mapping bthy bthm thmname upd_thy
   439 		     | output_thy =>
   440 		       let
   441 			   val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
   442 		       in
   443 			   upd_thy |> add_hol4_move thmname new_thmname
   444 				   |> add_hol4_mapping bthy bthm new_thmname
   445 		       end
   446     in
   447 	thy'
   448     end;
   449 
   450 fun get_hol4_theorem thyname thmname thy =
   451     let
   452 	val isathms = HOL4Thms.get thy
   453     in
   454 	StringPair.lookup isathms (thyname,thmname)
   455     end
   456 
   457 fun add_hol4_theorem thyname thmname hth thy =
   458     let
   459 	val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
   460 	val isathms = HOL4Thms.get thy
   461 	val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms
   462 	val thy' = HOL4Thms.put isathms' thy
   463     in
   464 	thy'
   465     end
   466 
   467 fun export_hol4_pending thy =
   468     let
   469 	val rews    = HOL4Rewrites.get thy
   470 	val outthy  = get_output_thy thy
   471 	fun process (thy,((bthy,bthm),hth as (_,thm))) =
   472 	    let
   473 		val sg      = sign_of thy
   474 		val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm)
   475 		val thm2 = standard thm1
   476 		val thy2 = PureThy.store_thm ((bthm, thm2), []) thy |> snd
   477 		val thy5 = add_hol4_theorem bthy bthm hth thy2
   478 	    in
   479 		thy5
   480 	    end
   481 
   482 	val pending = HOL4Pending.get thy
   483 	val thy1    = StringPair.foldl process (thy,pending)
   484 	val thy2    = HOL4Pending.put (StringPair.empty) thy1
   485     in
   486 	thy2
   487     end;
   488 
   489 fun setup_dump (dir,thyname) thy =
   490     HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
   491 
   492 fun add_dump str thy =
   493     let
   494 	val (dir,thyname,curdump) = HOL4Dump.get thy
   495     in
   496 	HOL4Dump.put (dir,thyname,str::curdump) thy
   497     end
   498 
   499 fun flush_dump thy =
   500     let
   501 	val (dir,thyname,dumpdata) = HOL4Dump.get thy
   502 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
   503 						      file=thyname ^ ".thy"})
   504 	val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
   505 	val  _ = TextIO.closeOut os
   506     in
   507 	HOL4Dump.put ("","",[]) thy
   508     end
   509 
   510 fun set_generating_thy thyname thy =
   511     case HOL4DefThy.get thy of
   512 	NoImport => HOL4DefThy.put (Generating thyname) thy
   513       | _ => error "Import already in progess"
   514 
   515 fun set_replaying_thy thyname thy =
   516     case HOL4DefThy.get thy of
   517 	NoImport => HOL4DefThy.put (Replaying thyname) thy
   518       | _ => error "Import already in progess"
   519 
   520 fun clear_import_thy thy =
   521     case HOL4DefThy.get thy of
   522 	NoImport => error "No import in progress"
   523       | _ => HOL4DefThy.put NoImport thy
   524 
   525 fun get_generating_thy thy =
   526     case HOL4DefThy.get thy of
   527 	Generating thyname => thyname
   528       | _ => error "No theory being generated"
   529 
   530 fun get_replaying_thy thy =
   531     case HOL4DefThy.get thy of
   532 	Replaying thyname => thyname
   533       | _ => error "No theory being replayed"
   534 
   535 fun get_import_thy thy =
   536     case HOL4DefThy.get thy of
   537 	Replaying thyname => thyname
   538       | Generating thyname => thyname
   539       | _ => error "No theory being imported"
   540 
   541 fun should_ignore thyname thy thmname =
   542     case get_hol4_mapping thyname thmname thy of
   543 	SOME NONE => true 
   544       | _ => false
   545 
   546 val trans_string =
   547     let
   548 	fun quote s = "\"" ^ s ^ "\""
   549 	fun F [] = []
   550 	  | F (#"\\" :: cs) = patch #"\\" cs
   551 	  | F (#"\"" :: cs) = patch #"\"" cs
   552 	  | F (c     :: cs) = c :: F cs
   553 	and patch c rest = #"\\" :: c :: F rest
   554     in
   555 	quote o String.implode o F o String.explode
   556     end
   557 
   558 fun dump_import_thy thyname thy =
   559     let
   560 	val output_dir = get_output_dir thy
   561 	val output_thy = get_output_thy thy
   562 	val input_thy = Context.theory_name thy
   563 	val import_segment = get_import_segment thy
   564 	val sg = sign_of thy
   565 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
   566 						      file=thyname ^ ".imp"})
   567 	fun out s = TextIO.output(os,s)
   568 	val (ignored,mapped) =
   569 	    StringPair.foldl (fn ((ign,map),((bthy,bthm),v)) =>
   570 				 if bthy = thyname
   571 				 then (case v of
   572 					   NONE => (bthm::ign,map)
   573 					 | SOME w => (ign,(bthm,w)::map))
   574 				 else (ign,map))
   575 				 (([],[]),HOL4Maps.get thy)
   576 	val constmaps =
   577 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
   578 				 if bthy = thyname
   579 				 then (bthm,v)::map
   580 				 else map)
   581 				 ([],HOL4ConstMaps.get thy)
   582 
   583 	val constrenames =
   584 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
   585 				 if bthy = thyname
   586 				 then (bthm,v)::map
   587 				 else map)
   588 				 ([],HOL4Rename.get thy)
   589 
   590 	val typemaps =
   591 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
   592 				 if bthy = thyname
   593 				 then (bthm,v)::map
   594 				 else map)
   595 				 ([],HOL4TypeMaps.get thy)
   596 
   597 	val defmaps =
   598 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>
   599 				 if bthy = thyname
   600 				 then (bthm,v)::map
   601 				 else map)
   602 				 ([],HOL4DefMaps.get thy)
   603 
   604 	fun new_name internal isa =
   605 	    if internal
   606 	    then
   607 		let
   608 		    val paths = NameSpace.unpack isa
   609 		    val i = Library.drop(length paths - 2,paths)
   610 		in
   611 		    case i of
   612 			[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
   613 		      | _ => error "hol4rews.dump internal error"
   614 		end
   615 	    else
   616 		isa
   617 
   618 	val _ = out "import\n\n"
   619 
   620 	val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
   621 	val _ = if null defmaps
   622 		then ()
   623 		else out "def_maps"
   624 	val _ = app (fn (hol,isa) =>
   625 			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
   626 	val _ = if null defmaps
   627 		then ()
   628 		else out "\n\n"
   629 
   630 	val _ = if null typemaps
   631 		then ()
   632 		else out "type_maps"
   633 	val _ = app (fn (hol,(internal,isa)) =>
   634 			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
   635 	val _ = if null typemaps
   636 		then ()
   637 		else out "\n\n"
   638 
   639 	val _ = if null constmaps
   640 		then ()
   641 		else out "const_maps"
   642 	val _ = app (fn (hol,(internal,isa,opt_ty)) =>
   643 			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
   644 			 case opt_ty of
   645 			     SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")
   646 			   | NONE => ())) constmaps
   647 	val _ = if null constmaps
   648 		then ()
   649 		else out "\n\n"
   650 
   651 	val _ = if null constrenames
   652 		then ()
   653 		else out "const_renames"
   654 	val _ = app (fn (old,new) =>
   655 			out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
   656 	val _ = if null constrenames
   657 		then ()
   658 		else out "\n\n"
   659 
   660 	fun gen2replay in_thy out_thy s = 
   661 	    let
   662 		val ss = NameSpace.unpack s
   663 	    in
   664 		if (hd ss = in_thy) then 
   665 		    NameSpace.pack (out_thy::(tl ss))
   666 		else
   667 		    s
   668 	    end 
   669 
   670 	val _ = if null mapped
   671 		then ()
   672 		else out "thm_maps"
   673 	val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
   674 	val _ = if null mapped 
   675 		then ()
   676 		else out "\n\n"
   677 
   678 	val _ = if null ignored
   679 		then ()
   680 		else out "ignore_thms"
   681 	val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored
   682 	val _ = if null ignored
   683 		then ()
   684 		else out "\n\n"
   685 
   686 	val _ = out "end\n"
   687 	val _ = TextIO.closeOut os
   688     in
   689 	thy
   690     end
   691 
   692 fun set_used_names names thy =
   693     let
   694 	val unames = HOL4UNames.get thy
   695     in
   696 	case unames of
   697 	    [] => HOL4UNames.put names thy
   698 	  | _ => error "hol4rews.set_used_names called on initialized data!"
   699     end
   700 
   701 val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty
   702 
   703 fun get_defmap thyname const thy =
   704     let
   705 	val maps = HOL4DefMaps.get thy
   706     in
   707 	StringPair.lookup maps (thyname,const)
   708     end
   709 
   710 fun add_defmap thyname const defname thy =
   711     let
   712 	val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
   713 	val maps = HOL4DefMaps.get thy
   714 	val maps' = StringPair.update_new ((thyname,const),defname) maps
   715 	val thy' = HOL4DefMaps.put maps' thy
   716     in
   717 	thy'
   718     end
   719 
   720 fun get_defname thyname name thy =
   721     let
   722 	val maps = HOL4DefMaps.get thy
   723 	fun F dname = (dname,add_defmap thyname name dname thy)
   724     in
   725 	case StringPair.lookup maps (thyname,name) of
   726 	    SOME thmname => (thmname,thy)
   727 	  | NONE =>
   728 	    let
   729 		val used = HOL4UNames.get thy
   730 		val defname = def_name name
   731 		val pdefname = name ^ "_primdef"
   732 	    in
   733 		if not (defname mem used)
   734 		then F defname                 (* name_def *)
   735 		else if not (pdefname mem used)
   736 		then F pdefname                (* name_primdef *)
   737 		else F (variant used pdefname) (* last resort *)
   738 	    end
   739     end
   740 
   741 local
   742     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
   743       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
   744       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
   745       | handle_meta [x] = Appl[Constant "Trueprop",x]
   746       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
   747 in
   748 val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
   749 end
   750 
   751 local
   752     fun initial_maps thy =
   753 	thy |> add_hol4_type_mapping "min" "bool" false "bool"
   754 	    |> add_hol4_type_mapping "min" "fun" false "fun"
   755 	    |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
   756 	    |> add_hol4_const_mapping "min" "=" false "op ="
   757 	    |> add_hol4_const_mapping "min" "==>" false "op -->"
   758 	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
   759 in
   760 val hol4_setup =
   761   HOL4Rewrites.init #>
   762   HOL4Maps.init #>
   763   HOL4UNames.init #>
   764   HOL4DefMaps.init #>
   765   HOL4Moves.init #>
   766   HOL4CMoves.init #>
   767   HOL4ConstMaps.init #>
   768   HOL4Rename.init #>
   769   HOL4TypeMaps.init #>
   770   HOL4Pending.init #>
   771   HOL4Thms.init #>
   772   HOL4Dump.init #>
   773   HOL4DefThy.init #>
   774   HOL4Imports.init #>
   775   ImportSegment.init #>
   776   initial_maps #>
   777   Attrib.add_attributes
   778     [("hol4rew",
   779       (Attrib.no_args add_hol4_rewrite,
   780        Attrib.no_args Attrib.undef_local_attribute),
   781       "HOL4 rewrite rule")]
   782 end