src/HOL/TPTP/mash_export.ML
author blanchet
Fri Dec 21 15:22:57 2012 +0100 (2012-12-21)
changeset 50611 99af6b652b3a
parent 50582 001a0e12d7f1
child 50624 4d0997abce79
permissions -rw-r--r--
linearize eval driver, to work around horrible bug in previous implementation
blanchet@48234
     1
(*  Title:      HOL/TPTP/mash_export.ML
blanchet@48234
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48234
     3
    Copyright   2012
blanchet@48234
     4
blanchet@48234
     5
Export Isabelle theory information for MaSh (Machine-learning for Sledgehammer).
blanchet@48234
     6
*)
blanchet@48234
     7
blanchet@48234
     8
signature MASH_EXPORT =
blanchet@48234
     9
sig
blanchet@48251
    10
  type params = Sledgehammer_Provers.params
blanchet@48235
    11
blanchet@50349
    12
  val generate_accessibility :
blanchet@50349
    13
    Proof.context -> theory list -> bool -> string -> unit
blanchet@48318
    14
  val generate_features :
blanchet@50349
    15
    Proof.context -> string -> theory list -> bool -> string -> unit
blanchet@48333
    16
  val generate_isar_dependencies :
blanchet@50349
    17
    Proof.context -> theory list -> bool -> string -> unit
blanchet@50484
    18
  val generate_prover_dependencies :
blanchet@50559
    19
    Proof.context -> params -> int * int option -> theory list -> bool -> string
blanchet@50559
    20
    -> unit
blanchet@50411
    21
  val generate_isar_commands :
blanchet@50411
    22
    Proof.context -> string -> theory list -> string -> unit
blanchet@50484
    23
  val generate_prover_commands :
blanchet@50559
    24
    Proof.context -> params -> int * int option -> theory list -> string -> unit
blanchet@48379
    25
  val generate_mepo_suggestions :
blanchet@50349
    26
    Proof.context -> params -> theory list -> int -> string -> unit
blanchet@48234
    27
end;
blanchet@48234
    28
blanchet@48234
    29
structure MaSh_Export : MASH_EXPORT =
blanchet@48234
    30
struct
blanchet@48234
    31
blanchet@50485
    32
open Sledgehammer_Fact
blanchet@48381
    33
open Sledgehammer_MePo
blanchet@48381
    34
open Sledgehammer_MaSh
blanchet@48245
    35
blanchet@50559
    36
fun in_range (from, to) j =
blanchet@50559
    37
  j >= from andalso (to = NONE orelse j <= the to)
blanchet@50559
    38
blanchet@50349
    39
fun has_thm_thy th thy =
blanchet@48316
    40
  Context.theory_name thy = Context.theory_name (theory_of_thm th)
blanchet@48316
    41
blanchet@50349
    42
fun has_thys thys th = exists (has_thm_thy th) thys
blanchet@50349
    43
blanchet@50349
    44
fun all_facts ctxt =
blanchet@48531
    45
  let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
blanchet@50442
    46
    Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css
blanchet@50485
    47
    |> sort (thm_ord o pairself snd)
blanchet@48531
    48
  end
blanchet@48531
    49
blanchet@50349
    50
fun generate_accessibility ctxt thys include_thys file_name =
blanchet@48304
    51
  let
blanchet@48304
    52
    val path = file_name |> Path.explode
blanchet@48304
    53
    val _ = File.write path ""
blanchet@48304
    54
    fun do_fact fact prevs =
blanchet@48304
    55
      let
blanchet@48304
    56
        val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
blanchet@48304
    57
        val _ = File.append path s
blanchet@48304
    58
      in [fact] end
blanchet@50611
    59
    val facts =
blanchet@50349
    60
      all_facts ctxt
blanchet@50349
    61
      |> not include_thys ? filter_out (has_thys thys o snd)
blanchet@50611
    62
      |> map (snd #> nickname_of)
blanchet@50611
    63
  in fold do_fact facts []; () end
blanchet@48304
    64
blanchet@50349
    65
fun generate_features ctxt prover thys include_thys file_name =
blanchet@48304
    66
  let
blanchet@48304
    67
    val path = file_name |> Path.explode
blanchet@48304
    68
    val _ = File.write path ""
blanchet@48304
    69
    val facts =
blanchet@50349
    70
      all_facts ctxt
blanchet@50349
    71
      |> not include_thys ? filter_out (has_thys thys o snd)
blanchet@48385
    72
    fun do_fact ((_, stature), th) =
blanchet@48304
    73
      let
blanchet@48378
    74
        val name = nickname_of th
blanchet@48318
    75
        val feats =
blanchet@48385
    76
          features_of ctxt prover (theory_of_thm th) stature [prop_of th]
blanchet@50582
    77
        val s =
blanchet@50582
    78
          escape_meta name ^ ": " ^ encode_features (sort_wrt fst feats) ^ "\n"
blanchet@48304
    79
      in File.append path s end
blanchet@48304
    80
  in List.app do_fact facts end
blanchet@48304
    81
blanchet@50515
    82
fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th
blanchet@50515
    83
                                   isar_deps_opt =
blanchet@50411
    84
  (case params_opt of
blanchet@50411
    85
     SOME (params as {provers = prover :: _, ...}) =>
blanchet@50484
    86
     prover_dependencies_of ctxt params prover 0 facts all_names th |> snd
blanchet@50515
    87
   | NONE =>
blanchet@50515
    88
     case isar_deps_opt of
blanchet@50515
    89
       SOME deps => deps
blanchet@50515
    90
     | NONE => isar_dependencies_of all_names th)
blanchet@50411
    91
  |> these
blanchet@50411
    92
blanchet@50559
    93
fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
blanchet@50484
    94
                                         file_name =
blanchet@48304
    95
  let
blanchet@48304
    96
    val path = file_name |> Path.explode
blanchet@48304
    97
    val facts =
blanchet@50485
    98
      all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
blanchet@50485
    99
    val all_names = build_all_names nickname_of facts
blanchet@50559
   100
    fun do_fact (j, (_, th)) =
blanchet@50559
   101
      if in_range range j then
blanchet@50559
   102
        let
blanchet@50559
   103
          val name = nickname_of th
blanchet@50561
   104
          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
blanchet@50559
   105
          val deps =
blanchet@50559
   106
            isar_or_prover_dependencies_of ctxt params_opt facts all_names th
blanchet@50559
   107
                                           NONE
blanchet@50559
   108
        in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
blanchet@50559
   109
      else
blanchet@50559
   110
        ""
blanchet@50559
   111
    val lines = Par_List.map do_fact (tag_list 1 facts)
blanchet@50519
   112
  in File.write_list path lines end
blanchet@48304
   113
blanchet@50411
   114
fun generate_isar_dependencies ctxt =
blanchet@50559
   115
  generate_isar_or_prover_dependencies ctxt NONE (1, NONE)
blanchet@50411
   116
blanchet@50484
   117
fun generate_prover_dependencies ctxt params =
blanchet@50484
   118
  generate_isar_or_prover_dependencies ctxt (SOME params)
blanchet@50411
   119
blanchet@50515
   120
fun is_bad_query ctxt ho_atp th isar_deps =
blanchet@50515
   121
  Thm.legacy_get_kind th = "" orelse null isar_deps orelse
blanchet@50523
   122
  is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
blanchet@50515
   123
blanchet@50559
   124
fun generate_isar_or_prover_commands ctxt prover params_opt range thys
blanchet@50559
   125
                                     file_name =
blanchet@48234
   126
  let
blanchet@50511
   127
    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
blanchet@48234
   128
    val path = file_name |> Path.explode
blanchet@50349
   129
    val facts = all_facts ctxt
blanchet@50485
   130
    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
blanchet@50485
   131
    val all_names = build_all_names nickname_of facts
blanchet@50559
   132
    fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
blanchet@50559
   133
      if in_range range j then
blanchet@50559
   134
        let
blanchet@50561
   135
          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
blanchet@50559
   136
          val feats =
blanchet@50559
   137
            features_of ctxt prover (theory_of_thm th) stature [prop_of th]
blanchet@50559
   138
          val isar_deps = isar_dependencies_of all_names th
blanchet@50559
   139
          val deps =
blanchet@50559
   140
            isar_or_prover_dependencies_of ctxt params_opt facts all_names th
blanchet@50559
   141
                                           (SOME isar_deps)
blanchet@50559
   142
          val core =
blanchet@50559
   143
            escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
blanchet@50582
   144
            encode_features (sort_wrt fst feats)
blanchet@50559
   145
          val query =
blanchet@50559
   146
            if is_bad_query ctxt ho_atp th (these isar_deps) then ""
blanchet@50559
   147
            else "? " ^ core ^ "\n"
blanchet@50559
   148
          val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
blanchet@50559
   149
        in query ^ update end
blanchet@50559
   150
      else
blanchet@50559
   151
        ""
blanchet@50611
   152
    val parents = map (nickname_of o snd) (the_list (try List.last old_facts))
blanchet@50519
   153
    val new_facts = new_facts |> map (`(nickname_of o snd))
blanchet@50519
   154
    val prevss = fst (split_last (parents :: map (single o fst) new_facts))
blanchet@50559
   155
    val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
blanchet@50519
   156
  in File.write_list path lines end
blanchet@48239
   157
blanchet@50411
   158
fun generate_isar_commands ctxt prover =
blanchet@50559
   159
  generate_isar_or_prover_commands ctxt prover NONE (1, NONE)
blanchet@50411
   160
blanchet@50484
   161
fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
blanchet@50484
   162
  generate_isar_or_prover_commands ctxt prover (SOME params)
blanchet@50411
   163
blanchet@50515
   164
fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys
blanchet@50515
   165
                              max_facts file_name =
blanchet@48239
   166
  let
blanchet@50515
   167
    val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
blanchet@48239
   168
    val path = file_name |> Path.explode
blanchet@50349
   169
    val facts = all_facts ctxt
blanchet@50485
   170
    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
blanchet@50515
   171
    val all_names = build_all_names nickname_of facts
blanchet@50523
   172
    fun do_fact ((_, th), old_facts) =
blanchet@48239
   173
      let
blanchet@48378
   174
        val name = nickname_of th
blanchet@50349
   175
        val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
blanchet@48292
   176
        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
blanchet@50515
   177
        val isar_deps = isar_dependencies_of all_names th
blanchet@50519
   178
      in
blanchet@50519
   179
        if is_bad_query ctxt ho_atp th (these isar_deps) then
blanchet@50519
   180
          ""
blanchet@50519
   181
        else
blanchet@50519
   182
          let
blanchet@50519
   183
            val suggs =
blanchet@50519
   184
              old_facts
blanchet@50519
   185
              |> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
blanchet@50519
   186
                     max_facts NONE hyp_ts concl_t
blanchet@50519
   187
              |> map (nickname_of o snd)
blanchet@50519
   188
          in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end
blanchet@50519
   189
      end
blanchet@50519
   190
    fun accum x (yss as ys :: _) = (x :: ys) :: yss
blanchet@50519
   191
    val old_factss = tl (fold accum new_facts [old_facts])
blanchet@50519
   192
    val lines = Par_List.map do_fact (new_facts ~~ rev old_factss)
blanchet@50519
   193
  in File.write_list path lines end
blanchet@48234
   194
blanchet@48234
   195
end;