(*  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 HOL4DefThy = TheoryDataFun

(

  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)

)

structure ImportSegment = TheoryDataFun

(

  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"

)

val get_import_segment = ImportSegment.get

val set_import_segment = ImportSegment.put

structure HOL4UNames = TheoryDataFun

(

  type T = string list

  val empty = []

  val copy = I

  val extend = I

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

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

)

structure HOL4Dump = TheoryDataFun

(

  type T = string * string * string list

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

  val copy = I

  val extend = I

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

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

)

structure HOL4Moves = TheoryDataFun

(

  type T = string Symtab.table

  val empty = Symtab.empty

  val copy = I

  val extend = I

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

)

structure HOL4Imports = TheoryDataFun

(

  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 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 HOL4CMoves = TheoryDataFun

(

  type T = string Symtab.table

  val empty = Symtab.empty

  val copy = I

  val extend = I

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

)

structure HOL4Maps = TheoryDataFun

(

  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)

)

structure HOL4Thms = TheoryDataFun

(

  type T = holthm StringPair.table

  val empty = StringPair.empty

  val copy = I

  val extend = I

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

)

structure HOL4ConstMaps = TheoryDataFun

(

  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)

)

structure HOL4Rename = TheoryDataFun

(

  type T = string StringPair.table

  val empty = StringPair.empty

  val copy = I

  val extend = I

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

)

structure HOL4DefMaps = TheoryDataFun

(

  type T = string StringPair.table

  val empty = StringPair.empty

  val copy = I

  val extend = I

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

)

structure HOL4TypeMaps = TheoryDataFun

(

  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)

)

structure HOL4Pending = TheoryDataFun

(

  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)

)

structure HOL4Rewrites = TheoryDataFun

(

  type T = thm list

  val empty = []

  val copy = I

  val extend = I

  fun merge _ = Library.gen_union Thm.eq_thm

)

val hol4_debug = ref false

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

local

  val eq_reflection = thm "eq_reflection"

in

fun add_hol4_rewrite (Context.Theory thy, th) =

    let

	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

  | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);

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 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 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 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 =

  let

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

  in

    HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))

  end;

fun export_hol4_pending thy =

  let

    val rews = HOL4Rewrites.get thy;

    val pending = HOL4Pending.get thy;

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

      let

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

        val thm2 = standard thm1;

      in

        thy

        |> PureThy.store_thm (bthm, thm2)

        |> snd

        |> add_hol4_theorem bthy bthm hth

      end;

  in

    thy

    |> StringPair.fold process pending

    |> HOL4Pending.put StringPair.empty

  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 os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,

						      file=thyname ^ ".imp"})

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

    val (ignored, mapped) = StringPair.fold

      (fn ((bthy, bthm), v) => fn (ign, map) =>

        if bthy = thyname

        then case v

         of NONE => (bthm :: ign, map)

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

        else (ign, map)) (HOL4Maps.get thy) ([],[]);

    fun mk init = StringPair.fold

      (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];

    val constmaps = mk (HOL4ConstMaps.get thy);

    val constrenames = mk (HOL4Rename.get thy);

    val typemaps = mk (HOL4TypeMaps.get thy);

    val defmaps = mk (HOL4DefMaps.get thy);

	fun new_name internal isa =

	    if internal

	    then

		let

		    val paths = NameSpace.explode 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 thy 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.explode s

	    in

		if (hd ss = in_thy) then 

		    NameSpace.implode (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 [];

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 =

  initial_maps #>

  Attrib.add_attributes

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

end