src/HOL/TPTP/mash_export.ML

renamed "iter" fact filter to "MePo" (Meng--Paulson)

(*  Title:      HOL/TPTP/mash_export.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2012

Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer).
*)

signature MASH_EXPORT =
sig
  type params = Sledgehammer_Provers.params

  val generate_accessibility : theory -> bool -> string -> unit
  val generate_features :
    Proof.context -> string -> theory -> bool -> string -> unit
  val generate_isar_dependencies :
    theory -> bool -> string -> unit
  val generate_atp_dependencies :
    Proof.context -> params -> theory -> bool -> string -> unit
  val generate_commands : Proof.context -> string -> theory -> string -> unit
  val generate_mepo_suggestions :
    Proof.context -> params -> theory -> int -> string -> unit
end;

structure MaSh_Export : MASH_EXPORT =
struct

open Sledgehammer_Fact
open Sledgehammer_Filter_Iter
open Sledgehammer_Filter_MaSh

fun thy_map_from_facts ths =
  ths |> sort (thm_ord o swap o pairself snd)
      |> map (snd #> `(theory_of_thm #> Context.theory_name))
      |> AList.coalesce (op =)
      |> map (apsnd (map nickname_of))

fun has_thy thy th =
  Context.theory_name thy = Context.theory_name (theory_of_thm th)

fun parent_facts thy thy_map =
  let
    fun add_last thy =
      case AList.lookup (op =) thy_map (Context.theory_name thy) of
        SOME (last_fact :: _) => insert (op =) last_fact
      | _ => add_parent thy
    and add_parent thy = fold add_last (Theory.parents_of thy)
  in add_parent thy [] end

val thy_name_of_fact = hd o Long_Name.explode
fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact

val all_names =
  filter_out is_likely_tautology_or_too_meta
  #> map (rpair () o nickname_of) #> Symtab.make

fun generate_accessibility thy include_thy file_name =
  let
    val path = file_name |> Path.explode
    val _ = File.write path ""
    fun do_fact fact prevs =
      let
        val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
        val _ = File.append path s
      in [fact] end
    val thy_map =
      all_facts_of thy Termtab.empty
      |> not include_thy ? filter_out (has_thy thy o snd)
      |> thy_map_from_facts
    fun do_thy facts =
      let
        val thy = thy_of_fact thy (hd facts)
        val parents = parent_facts thy thy_map
      in fold do_fact facts parents; () end
  in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end

fun generate_features ctxt prover thy include_thy file_name =
  let
    val path = file_name |> Path.explode
    val _ = File.write path ""
    val css_table = clasimpset_rule_table_of ctxt
    val facts =
      all_facts_of thy css_table
      |> not include_thy ? filter_out (has_thy thy o snd)
    fun do_fact ((_, (_, status)), th) =
      let
        val name = nickname_of th
        val feats =
          features_of ctxt prover (theory_of_thm th) status [prop_of th]
        val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
      in File.append path s end
  in List.app do_fact facts end

fun generate_isar_dependencies thy include_thy file_name =
  let
    val path = file_name |> Path.explode
    val _ = File.write path ""
    val ths =
      all_facts_of thy Termtab.empty
      |> not include_thy ? filter_out (has_thy thy o snd)
      |> map snd
    val all_names = all_names ths
    fun do_thm th =
      let
        val name = nickname_of th
        val deps = isabelle_dependencies_of all_names th
        val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
      in File.append path s end
  in List.app do_thm ths end

fun generate_atp_dependencies ctxt (params as {provers, max_facts, ...}) thy
                              include_thy file_name =
  let
    val path = file_name |> Path.explode
    val _ = File.write path ""
    val prover = hd provers
    val facts =
      all_facts_of thy Termtab.empty
      |> not include_thy ? filter_out (has_thy thy o snd)
    val ths = facts |> map snd
    val all_names = all_names ths
    fun is_dep dep (_, th) = nickname_of th = dep
    fun add_isar_dep facts dep accum =
      if exists (is_dep dep) accum then
        accum
      else case find_first (is_dep dep) facts of
        SOME ((name, status), th) => accum @ [((name, status), th)]
      | NONE => accum (* shouldn't happen *)
    fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
    fun do_thm th =
      let
        val name = nickname_of th
        val goal = goal_of_thm thy th
        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
        val deps =
          case isabelle_dependencies_of all_names th of
            [] => []
          | isar_dep as [_] => isar_dep (* can hardly beat that *)
          | isar_deps =>
            let
              val facts =
                facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
              val facts =
                facts |> iterative_relevant_facts ctxt params prover
                             (the max_facts) NONE hyp_ts concl_t
                      |> fold (add_isar_dep facts) isar_deps
                      |> map fix_name
            in
              case run_prover_for_mash ctxt params prover facts goal of
                {outcome = NONE, used_facts, ...} =>
                used_facts |> map fst |> sort string_ord
              | _ => isar_deps
            end
        val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
      in File.append path s end
  in List.app do_thm ths end

fun generate_commands ctxt prover thy file_name =
  let
    val path = file_name |> Path.explode
    val _ = File.write path ""
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    val facts = all_facts_of thy css_table
    val (new_facts, old_facts) =
      facts |> List.partition (has_thy thy o snd)
            |>> sort (thm_ord o pairself snd)
    val ths = facts |> map snd
    val all_names = all_names ths
    fun do_fact ((_, (_, status)), th) prevs =
      let
        val name = nickname_of th
        val feats = features_of ctxt prover thy status [prop_of th]
        val deps = isabelle_dependencies_of all_names th
        val kind = Thm.legacy_get_kind th
        val core = escape_metas prevs ^ "; " ^ escape_metas feats
        val query = if kind <> "" then "? " ^ core ^ "\n" else ""
        val update =
          "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^
          escape_metas deps ^ "\n"
        val _ = File.append path (query ^ update)
      in [name] end
    val thy_map = old_facts |> thy_map_from_facts
    val parents = parent_facts thy thy_map
  in fold do_fact new_facts parents; () end

fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
                              file_name =
  let
    val path = file_name |> Path.explode
    val _ = File.write path ""
    val prover = hd provers
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    val facts = all_facts_of thy css_table
    val (new_facts, old_facts) =
      facts |> List.partition (has_thy thy o snd)
            |>> sort (thm_ord o pairself snd)
    fun do_fact (fact as (_, th)) old_facts =
      let
        val name = nickname_of th
        val goal = goal_of_thm thy th
        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
        val kind = Thm.legacy_get_kind th
        val _ =
          if kind <> "" then
            let
              val suggs =
                old_facts
                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
                                prover max_relevant NONE hyp_ts concl_t
                |> map (fn ((name, _), _) => name ())
                |> sort string_ord
              val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
            in File.append path s end
          else
            ()
      in fact :: old_facts end
  in fold do_fact new_facts old_facts; () end

end;