src/HOL/Import/hol4rews.ML

prefer polyml-5.2.1 over odd polyml-5.3.0-old;

(*  Title:      HOL/Import/hol4rews.ML
    Author:     Sebastian Skalberg (TU Muenchen)
*)

structure StringPair = Table(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 = Theory_Data
(
  type T = ImportStatus
  val empty = NoImport
  val extend = I
  fun merge (NoImport, NoImport) = NoImport
    | merge _ = (warning "Import status set during merge"; NoImport)
)

structure ImportSegment = Theory_Data
(
  type T = string
  val empty = ""
  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 = Theory_Data
(
  type T = string list
  val empty = []
  val extend = I
  fun merge ([], []) = []
    | merge _ = error "Used names not empty during merge"
)

structure HOL4Dump = Theory_Data
(
  type T = string * string * string list
  val empty = ("","",[])
  val extend = I
  fun merge (("","",[]),("","",[])) = ("","",[])
    | merge _ = error "Dump data not empty during merge"
)

structure HOL4Moves = Theory_Data
(
  type T = string Symtab.table
  val empty = Symtab.empty
  val extend = I
  fun merge data = Symtab.merge (K true) data
)

structure HOL4Imports = Theory_Data
(
  type T = string Symtab.table
  val empty = Symtab.empty
  val extend = I
  fun merge data = Symtab.merge (K true) data
)

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 = Theory_Data
(
  type T = string Symtab.table
  val empty = Symtab.empty
  val extend = I
  fun merge data = Symtab.merge (K true) data
)

structure HOL4Maps = Theory_Data
(
  type T = string option StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4Thms = Theory_Data
(
  type T = holthm StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4ConstMaps = Theory_Data
(
  type T = (bool * string * typ option) StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4Rename = Theory_Data
(
  type T = string StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4DefMaps = Theory_Data
(
  type T = string StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4TypeMaps = Theory_Data
(
  type T = (bool * string) StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4Pending = Theory_Data
(
  type T = ((term * term) list * thm) StringPair.table
  val empty = StringPair.empty
  val extend = I
  fun merge data = StringPair.merge (K true) data
)

structure HOL4Rewrites = Theory_Data
(
  type T = thm list
  val empty = []
  val extend = I
  val merge = Thm.merge_thms
)

val hol4_debug = Unsynchronized.ref false
fun message s = if !hol4_debug then writeln s else ()

fun add_hol4_rewrite (Context.Theory thy, th) =
    let
        val _ = message "Adding HOL4 rewrite"
        val th1 = th RS @{thm 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);

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_bname 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_bname 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
               (* FIXME avoid handle x *)
               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_bname 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 = Drule.export_without_context thm1;
      in
        thy
        |> Global_Theory.store_thm (Binding.name 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 = Long_Name.explode isa
                    val i = 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 (" :: \"" ^ Syntax.string_of_typ_global 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 = Long_Name.explode s
            in
                if (hd ss = in_thy) then 
                    Long_Name.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 = Thm.def_name name
                val pdefname = name ^ "_primdef"
            in
                if not (member (op =) used defname)
                then F defname                 (* name_def *)
                else if not (member (op =) used pdefname)
                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 @{const_syntax "=="}, _],_,_]] = x
      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
      | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
      | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
      | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
in
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
end

local
    fun initial_maps thy =
        thy |> add_hol4_type_mapping "min" "bool" false @{type_name bool}
            |> add_hol4_type_mapping "min" "fun" false "fun"
            |> add_hol4_type_mapping "min" "ind" false @{type_name ind}
            |> add_hol4_const_mapping "min" "=" false @{const_name HOL.eq}
            |> add_hol4_const_mapping "min" "==>" false @{const_name HOL.implies}
            |> add_hol4_const_mapping "min" "@" false @{const_name "Eps"}
in
val hol4_setup =
  initial_maps #>
  Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"

end