(*  Title:      HOL/Import/hol4rews.ML

     ID:         $Id$

     Author:     Sebastian Skalberg (TU Muenchen)

 *)

 structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);

 type holthm = (term * term) list * thm

 datatype ImportStatus =

 	 NoImport

        | Generating of string

        | Replaying of string

 structure HOL4DefThyArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/import_status"

 type T = ImportStatus

 val empty = NoImport

 val copy = I

 val extend = I

 fun merge _ (NoImport,NoImport) = NoImport

   | merge _ _ = (warning "Import status set during merge"; NoImport)

 fun print sg import_status =

     Pretty.writeln (Pretty.str (case import_status of NoImport => "No current import" | Generating thyname => ("Generating " ^ thyname) | Replaying thyname => ("Replaying " ^ thyname)))

 end;

 structure HOL4DefThy = TheoryDataFun(HOL4DefThyArgs);

 structure ImportSegmentArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/import_segment"

 type T = string

 val empty = ""

 val copy = I

 val extend = I

 fun merge _ ("",arg) = arg

   | merge _ (arg,"") = arg

   | merge _ (s1,s2) =

     if s1 = s2

     then s1

     else error "Trying to merge two different import segments"

 fun print sg import_segment =

     Pretty.writeln (Pretty.str ("Import segment: " ^ import_segment))

 end;

 structure ImportSegment = TheoryDataFun(ImportSegmentArgs);

 val get_import_segment = ImportSegment.get

 val set_import_segment = ImportSegment.put

 structure HOL4UNamesArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/used_names"

 type T = string list

 val empty = []

 val copy = I

 val extend = I

 fun merge _ ([],[]) = []

   | merge _ _ = error "Used names not empty during merge"

 fun print sg used_names =

     Pretty.writeln (Pretty.str "Printing of HOL4/used_names Not implemented")

 end;

 structure HOL4UNames = TheoryDataFun(HOL4UNamesArgs);

 structure HOL4DumpArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/dump_data"

 type T = string * string * string list

 val empty = ("","",[])

 val copy = I

 val extend = I

 fun merge _ (("","",[]),("","",[])) = ("","",[])

   | merge _ _ = error "Dump data not empty during merge"

 fun print sg dump_data =

     Pretty.writeln (Pretty.str "Printing of HOL4/dump_data Not implemented")

 end;

 structure HOL4Dump = TheoryDataFun(HOL4DumpArgs);

 structure HOL4MovesArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/moves"

 type T = string Symtab.table

 val empty = Symtab.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = Symtab.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 moves:"

 	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))

 end;

 structure HOL4Moves = TheoryDataFun(HOL4MovesArgs);

 structure HOL4ImportsArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/imports"

 type T = string Symtab.table

 val empty = Symtab.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = Symtab.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 imports:"

 	(Symtab.foldl (fn (xl,(thyname,segname)) => (Pretty.str (thyname ^ " imported from segment " ^ segname)::xl)) ([],tab)))

 end;

 structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs);

 fun get_segment2 thyname thy =

   Symtab.lookup (HOL4Imports.get thy) thyname

 fun set_segment thyname segname thy =

     let

 	val imps = HOL4Imports.get thy

 	val imps' = Symtab.update_new (thyname,segname) imps

     in

 	HOL4Imports.put imps' thy

     end

 structure HOL4CMovesArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/constant_moves"

 type T = string Symtab.table

 val empty = Symtab.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = Symtab.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 constant moves:"

 	(Symtab.foldl (fn (xl,(bef,aft)) => (Pretty.str (bef ^ " --> " ^ aft)::xl)) ([],tab)))

 end;

 structure HOL4CMoves = TheoryDataFun(HOL4CMovesArgs);

 structure HOL4MapsArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/mappings"

 type T = (string option) StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 mappings:"

 	(StringPair.foldl (fn (xl,((bthy,bthm),isathm)) => (Pretty.str (bthy ^ "." ^ bthm ^ (case isathm of SOME th => " --> " ^ th | NONE => "IGNORED"))::xl)) ([],tab)))

 end;

 structure HOL4Maps = TheoryDataFun(HOL4MapsArgs);

 structure HOL4ThmsArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/theorems"

 type T = holthm StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 mappings:"

 	(StringPair.foldl (fn (xl,((bthy,bthm),(_,thm))) => (Pretty.str (bthy ^ "." ^ bthm ^ ":")::(Display.pretty_thm thm)::xl)) ([],tab)))

 end;

 structure HOL4Thms = TheoryDataFun(HOL4ThmsArgs);

 structure HOL4ConstMapsArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/constmappings"

 type T = (bool * string * typ option) StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 constant mappings:"

 	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst,_))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))

 end;

 structure HOL4ConstMaps = TheoryDataFun(HOL4ConstMapsArgs);

 structure HOL4RenameArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/renamings"

 type T = string StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 constant renamings:"

 	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ newname)::xl)) ([],tab)))

 end;

 structure HOL4Rename = TheoryDataFun(HOL4RenameArgs);

 structure HOL4DefMapsArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/def_maps"

 type T = string StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 constant definitions:"

 	(StringPair.foldl (fn (xl,((bthy,bconst),newname)) => (Pretty.str (bthy ^ "." ^ bconst ^ ": " ^ newname)::xl)) ([],tab)))

 end;

 structure HOL4DefMaps = TheoryDataFun(HOL4DefMapsArgs);

 structure HOL4TypeMapsArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/typemappings"

 type T = (bool * string) StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 type mappings:"

 	(StringPair.foldl (fn (xl,((bthy,bconst),(internal,isaconst))) => (Pretty.str (bthy ^ "." ^ bconst ^ " --> " ^ isaconst ^ (if internal then " (*)" else ""))::xl)) ([],tab)))

 end;

 structure HOL4TypeMaps = TheoryDataFun(HOL4TypeMapsArgs);

 structure HOL4PendingArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/pending"

 type T = ((term * term) list * thm) StringPair.table

 val empty = StringPair.empty

 val copy = I

 val extend = I

 fun merge _ : T * T -> T = StringPair.merge (K true)

 fun print sg tab =

     Pretty.writeln (Pretty.big_list "HOL4 pending theorems:"

 	(StringPair.foldl (fn (xl,((bthy,bthm),(_,th))) => (Pretty.chunks [Pretty.str (bthy ^ "." ^ bthm ^ ":"),Display.pretty_thm th]::xl)) ([],tab)))

 end;

 structure HOL4Pending = TheoryDataFun(HOL4PendingArgs);

 structure HOL4RewritesArgs: THEORY_DATA_ARGS =

 struct

 val name = "HOL4/rewrites"

 type T = thm list

 val empty = []

 val copy = I

 val extend = I

 fun merge _ = Library.gen_union Thm.eq_thm

 fun print sg thms =

     Pretty.writeln (Pretty.big_list "HOL4 rewrite rules:"

 				    (map Display.pretty_thm thms))

 end;

 structure HOL4Rewrites = TheoryDataFun(HOL4RewritesArgs);

 val hol4_debug = ref false

 fun message s = if !hol4_debug then writeln s else ()

 fun add_hol4_rewrite (context, th) =

     let

         val thy = Context.the_theory context;

 	val _ = message "Adding HOL4 rewrite"

 	val th1 = th RS eq_reflection

 	val current_rews = HOL4Rewrites.get thy

 	val new_rews = insert Thm.eq_thm th1 current_rews

 	val updated_thy  = HOL4Rewrites.put new_rews thy

     in

 	(Context.Theory updated_thy,th1)

     end;

 fun ignore_hol4 bthy bthm thy =

     let

 	val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)

 	val curmaps = HOL4Maps.get thy

 	val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps

 	val upd_thy = HOL4Maps.put newmaps thy

     in

 	upd_thy

     end

 val opt_get_output_thy = #2 o HOL4Dump.get

 fun get_output_thy thy =

     case #2 (HOL4Dump.get thy) of

 	"" => error "No theory file being output"

       | thyname => thyname

 val get_output_dir = #1 o HOL4Dump.get

 fun add_hol4_move bef aft thy =

     let

 	val curmoves = HOL4Moves.get thy

 	val newmoves = Symtab.update_new (bef, aft) curmoves

     in

 	HOL4Moves.put newmoves thy

     end

 fun get_hol4_move bef thy =

   Symtab.lookup (HOL4Moves.get thy) bef

 fun follow_name thmname thy =

     let

 	val moves = HOL4Moves.get thy

 	fun F thmname =

 	    case Symtab.lookup moves thmname of

 		SOME name => F name

 	      | NONE => thmname

     in

 	F thmname

     end

 fun add_hol4_cmove bef aft thy =

     let

 	val curmoves = HOL4CMoves.get thy

 	val newmoves = Symtab.update_new (bef, aft) curmoves

     in

 	HOL4CMoves.put newmoves thy

     end

 fun get_hol4_cmove bef thy =

   Symtab.lookup (HOL4CMoves.get thy) bef

 fun follow_cname thmname thy =

     let

 	val moves = HOL4CMoves.get thy

 	fun F thmname =

 	    case Symtab.lookup moves thmname of

 		SOME name => F name

 	      | NONE => thmname

     in

 	F thmname

     end

 fun add_hol4_mapping bthy bthm isathm thy =

     let	

        (* val _ = writeln ("Before follow_name: "^isathm)  *)

       val isathm = follow_name isathm thy

        (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)

 	val curmaps = HOL4Maps.get thy

 	val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps

 	val upd_thy = HOL4Maps.put newmaps thy

     in

 	upd_thy

     end;

 fun get_hol4_type_mapping bthy tycon thy =

     let

 	val maps = HOL4TypeMaps.get thy

     in

 	StringPair.lookup maps (bthy,tycon)

     end

 fun get_hol4_mapping bthy bthm thy =

     let

 	val curmaps = HOL4Maps.get thy

     in

 	StringPair.lookup curmaps (bthy,bthm)

     end;

 fun add_hol4_const_mapping bthy bconst internal isaconst thy =

     let

 	val thy = case opt_get_output_thy thy of

 		      "" => thy

 		    | output_thy => if internal

 				    then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy

 				    else thy

 	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))

 	val curmaps = HOL4ConstMaps.get thy

 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps

 	val upd_thy = HOL4ConstMaps.put newmaps thy

     in

 	upd_thy

     end;

 fun add_hol4_const_renaming bthy bconst newname thy =

     let

 	val currens = HOL4Rename.get thy

 	val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)

 	val newrens = StringPair.update_new ((bthy,bconst),newname) currens

 	val upd_thy = HOL4Rename.put newrens thy

     in

 	upd_thy

     end;

 fun get_hol4_const_renaming bthy bconst thy =

     let

 	val currens = HOL4Rename.get thy

     in

 	StringPair.lookup currens (bthy,bconst)

     end;

 fun get_hol4_const_mapping bthy bconst thy =

     let

 	val bconst = case get_hol4_const_renaming bthy bconst thy of

 			 SOME name => name

 		       | NONE => bconst

 	val maps = HOL4ConstMaps.get thy

     in

 	StringPair.lookup maps (bthy,bconst)

     end

 fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =

     let

 	val thy = case opt_get_output_thy thy of

 		      "" => thy

 		    | output_thy => if internal

 				    then add_hol4_cmove (Sign.full_name (sign_of thy) bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy

 				    else thy

 	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))

 	val curmaps = HOL4ConstMaps.get thy

 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps

 	val upd_thy = HOL4ConstMaps.put newmaps thy

     in

 	upd_thy

     end;

 fun add_hol4_type_mapping bthy bconst internal isaconst thy =

     let

 	val curmaps = HOL4TypeMaps.get thy

 	val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))

 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps

                handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in

                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end

         val upd_thy = HOL4TypeMaps.put newmaps thy

     in

 	upd_thy

     end;

 fun add_hol4_pending bthy bthm hth thy =

     let

 	val thmname = Sign.full_name (sign_of thy) bthm

 	val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)

 	val curpend = HOL4Pending.get thy

 	val newpend = StringPair.update_new ((bthy,bthm),hth) curpend

 	val upd_thy = HOL4Pending.put newpend thy

 	val thy' = case opt_get_output_thy upd_thy of

 		       "" => add_hol4_mapping bthy bthm thmname upd_thy

 		     | output_thy =>

 		       let

 			   val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm

 		       in

 			   upd_thy |> add_hol4_move thmname new_thmname

 				   |> add_hol4_mapping bthy bthm new_thmname

 		       end

     in

 	thy'

     end;

 fun get_hol4_theorem thyname thmname thy =

     let

 	val isathms = HOL4Thms.get thy

     in

 	StringPair.lookup isathms (thyname,thmname)

     end

 fun add_hol4_theorem thyname thmname hth thy =

     let

 	val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)

 	val isathms = HOL4Thms.get thy

 	val isathms' = StringPair.update_new ((thyname,thmname),hth) isathms

 	val thy' = HOL4Thms.put isathms' thy

     in

 	thy'

     end

 fun export_hol4_pending thy =

     let

 	val rews    = HOL4Rewrites.get thy

 	val outthy  = get_output_thy thy

 	fun process (thy,((bthy,bthm),hth as (_,thm))) =

 	    let

 		val sg      = sign_of thy

 		val thm1 = rewrite_rule (map (Thm.transfer sg) rews) (Thm.transfer sg thm)

 		val thm2 = standard thm1

 		val thy2 = PureThy.store_thm ((bthm, thm2), []) thy |> snd

 		val thy5 = add_hol4_theorem bthy bthm hth thy2

 	    in

 		thy5

 	    end

 	val pending = HOL4Pending.get thy

 	val thy1    = StringPair.foldl process (thy,pending)

 	val thy2    = HOL4Pending.put (StringPair.empty) thy1

     in

 	thy2

     end;

 fun setup_dump (dir,thyname) thy =

     HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy

 fun add_dump str thy =

     let

 	val (dir,thyname,curdump) = HOL4Dump.get thy

     in

 	HOL4Dump.put (dir,thyname,str::curdump) thy

     end

 fun flush_dump thy =

     let

 	val (dir,thyname,dumpdata) = HOL4Dump.get thy

 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,

 						      file=thyname ^ ".thy"})

 	val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)

 	val  _ = TextIO.closeOut os

     in

 	HOL4Dump.put ("","",[]) thy

     end

 fun set_generating_thy thyname thy =

     case HOL4DefThy.get thy of

 	NoImport => HOL4DefThy.put (Generating thyname) thy

       | _ => error "Import already in progess"

 fun set_replaying_thy thyname thy =

     case HOL4DefThy.get thy of

 	NoImport => HOL4DefThy.put (Replaying thyname) thy

       | _ => error "Import already in progess"

 fun clear_import_thy thy =

     case HOL4DefThy.get thy of

 	NoImport => error "No import in progress"

       | _ => HOL4DefThy.put NoImport thy

 fun get_generating_thy thy =

     case HOL4DefThy.get thy of

 	Generating thyname => thyname

       | _ => error "No theory being generated"

 fun get_replaying_thy thy =

     case HOL4DefThy.get thy of

 	Replaying thyname => thyname

       | _ => error "No theory being replayed"

 fun get_import_thy thy =

     case HOL4DefThy.get thy of

 	Replaying thyname => thyname

       | Generating thyname => thyname

       | _ => error "No theory being imported"

 fun should_ignore thyname thy thmname =

     case get_hol4_mapping thyname thmname thy of

 	SOME NONE => true 

       | _ => false

 val trans_string =

     let

 	fun quote s = "\"" ^ s ^ "\""

 	fun F [] = []

 	  | F (#"\\" :: cs) = patch #"\\" cs

 	  | F (#"\"" :: cs) = patch #"\"" cs

 	  | F (c     :: cs) = c :: F cs

 	and patch c rest = #"\\" :: c :: F rest

     in

 	quote o String.implode o F o String.explode

     end

 fun dump_import_thy thyname thy =

     let

 	val output_dir = get_output_dir thy

 	val output_thy = get_output_thy thy

 	val input_thy = Context.theory_name thy

 	val import_segment = get_import_segment thy

 	val sg = sign_of thy

 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,

 						      file=thyname ^ ".imp"})

 	fun out s = TextIO.output(os,s)

 	val (ignored,mapped) =

 	    StringPair.foldl (fn ((ign,map),((bthy,bthm),v)) =>

 				 if bthy = thyname

 				 then (case v of

 					   NONE => (bthm::ign,map)

 					 | SOME w => (ign,(bthm,w)::map))

 				 else (ign,map))

 				 (([],[]),HOL4Maps.get thy)

 	val constmaps =

 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>

 				 if bthy = thyname

 				 then (bthm,v)::map

 				 else map)

 				 ([],HOL4ConstMaps.get thy)

 	val constrenames =

 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>

 				 if bthy = thyname

 				 then (bthm,v)::map

 				 else map)

 				 ([],HOL4Rename.get thy)

 	val typemaps =

 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>

 				 if bthy = thyname

 				 then (bthm,v)::map

 				 else map)

 				 ([],HOL4TypeMaps.get thy)

 	val defmaps =

 	    StringPair.foldl (fn (map,((bthy,bthm),v)) =>

 				 if bthy = thyname

 				 then (bthm,v)::map

 				 else map)

 				 ([],HOL4DefMaps.get thy)

 	fun new_name internal isa =

 	    if internal

 	    then

 		let

 		    val paths = NameSpace.unpack isa

 		    val i = Library.drop(length paths - 2,paths)

 		in

 		    case i of

 			[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con

 		      | _ => error "hol4rews.dump internal error"

 		end

 	    else

 		isa

 	val _ = out "import\n\n"

 	val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")

 	val _ = if null defmaps

 		then ()

 		else out "def_maps"

 	val _ = app (fn (hol,isa) =>

 			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps

 	val _ = if null defmaps

 		then ()

 		else out "\n\n"

 	val _ = if null typemaps

 		then ()

 		else out "type_maps"

 	val _ = app (fn (hol,(internal,isa)) =>

 			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps

 	val _ = if null typemaps

 		then ()

 		else out "\n\n"

 	val _ = if null constmaps

 		then ()

 		else out "const_maps"

 	val _ = app (fn (hol,(internal,isa,opt_ty)) =>

 			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));

 			 case opt_ty of

 			     SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of sg ty)) ^ "\"")

 			   | NONE => ())) constmaps

 	val _ = if null constmaps

 		then ()

 		else out "\n\n"

 	val _ = if null constrenames

 		then ()

 		else out "const_renames"

 	val _ = app (fn (old,new) =>

 			out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames

 	val _ = if null constrenames

 		then ()

 		else out "\n\n"

 	fun gen2replay in_thy out_thy s = 

 	    let

 		val ss = NameSpace.unpack s

 	    in

 		if (hd ss = in_thy) then 

 		    NameSpace.pack (out_thy::(tl ss))

 		else

 		    s

 	    end 

 	val _ = if null mapped

 		then ()

 		else out "thm_maps"

 	val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped

 	val _ = if null mapped 

 		then ()

 		else out "\n\n"

 	val _ = if null ignored

 		then ()

 		else out "ignore_thms"

 	val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored

 	val _ = if null ignored

 		then ()

 		else out "\n\n"

 	val _ = out "end\n"

 	val _ = TextIO.closeOut os

     in

 	thy

     end

 fun set_used_names names thy =

     let

 	val unames = HOL4UNames.get thy

     in

 	case unames of

 	    [] => HOL4UNames.put names thy

 	  | _ => error "hol4rews.set_used_names called on initialized data!"

     end

 val clear_used_names = HOL4UNames.put HOL4UNamesArgs.empty

 fun get_defmap thyname const thy =

     let

 	val maps = HOL4DefMaps.get thy

     in

 	StringPair.lookup maps (thyname,const)

     end

 fun add_defmap thyname const defname thy =

     let

 	val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)

 	val maps = HOL4DefMaps.get thy

 	val maps' = StringPair.update_new ((thyname,const),defname) maps

 	val thy' = HOL4DefMaps.put maps' thy

     in

 	thy'

     end

 fun get_defname thyname name thy =

     let

 	val maps = HOL4DefMaps.get thy

 	fun F dname = (dname,add_defmap thyname name dname thy)

     in

 	case StringPair.lookup maps (thyname,name) of

 	    SOME thmname => (thmname,thy)

 	  | NONE =>

 	    let

 		val used = HOL4UNames.get thy

 		val defname = def_name name

 		val pdefname = name ^ "_primdef"

 	    in

 		if not (defname mem used)

 		then F defname                 (* name_def *)

 		else if not (pdefname mem used)

 		then F pdefname                (* name_primdef *)

 		else F (Name.variant used pdefname) (* last resort *)

 	    end

     end

 local

     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x

       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x

       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x

       | handle_meta [x] = Appl[Constant "Trueprop",x]

       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"

 in

 val smarter_trueprop_parsing = [("Trueprop",handle_meta)]

 end

 local

     fun initial_maps thy =

 	thy |> add_hol4_type_mapping "min" "bool" false "bool"

 	    |> add_hol4_type_mapping "min" "fun" false "fun"

 	    |> add_hol4_type_mapping "min" "ind" false "Nat.ind"

 	    |> add_hol4_const_mapping "min" "=" false "op ="

 	    |> add_hol4_const_mapping "min" "==>" false "op -->"

 	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"

 in

 val hol4_setup =

   HOL4Rewrites.init #>

   HOL4Maps.init #>

   HOL4UNames.init #>

   HOL4DefMaps.init #>

   HOL4Moves.init #>

   HOL4CMoves.init #>

   HOL4ConstMaps.init #>

   HOL4Rename.init #>

   HOL4TypeMaps.init #>

   HOL4Pending.init #>

   HOL4Thms.init #>

   HOL4Dump.init #>

   HOL4DefThy.init #>

   HOL4Imports.init #>

   ImportSegment.init #>

   initial_maps #>

   Attrib.add_attributes

     [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]

 end