src/HOL/TPTP/mash_export.ML
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 65458 cf504b7a7aa7
child 69597 ff784d5a5bfb
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
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@55201
    10
  type params = Sledgehammer_Prover.params
blanchet@48235
    11
blanchet@57431
    12
  val in_range : int * int option -> int -> bool
blanchet@57431
    13
  val extract_suggestions : string -> string * (string * real) list
blanchet@57431
    14
blanchet@57121
    15
  val generate_accessibility : Proof.context -> theory list -> string -> unit
blanchet@55212
    16
  val generate_features : Proof.context -> theory list -> string -> unit
blanchet@57121
    17
  val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> string ->
blanchet@57121
    18
    unit
blanchet@57121
    19
  val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list ->
blanchet@55212
    20
    string -> unit
blanchet@55212
    21
  val generate_isar_commands : Proof.context -> string -> (int * int option) * int -> theory list ->
blanchet@57121
    22
    int -> string -> unit
blanchet@55212
    23
  val generate_prover_commands : Proof.context -> params -> (int * int option) * int ->
blanchet@57121
    24
    theory list -> int -> string -> unit
blanchet@55212
    25
  val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
blanchet@57121
    26
    theory list -> int -> string -> unit
blanchet@57457
    27
  val generate_mash_suggestions : string -> Proof.context -> params -> (int * int option) * int ->
blanchet@57121
    28
    theory list -> int -> string -> unit
blanchet@50814
    29
  val generate_mesh_suggestions : int -> string -> string -> string -> unit
blanchet@48234
    30
end;
blanchet@48234
    31
blanchet@48234
    32
structure MaSh_Export : MASH_EXPORT =
blanchet@48234
    33
struct
blanchet@48234
    34
blanchet@50485
    35
open Sledgehammer_Fact
blanchet@55212
    36
open Sledgehammer_Prover_ATP
blanchet@48381
    37
open Sledgehammer_MePo
blanchet@48381
    38
open Sledgehammer_MaSh
blanchet@48245
    39
blanchet@50559
    40
fun in_range (from, to) j =
blanchet@50559
    41
  j >= from andalso (to = NONE orelse j <= the to)
blanchet@50559
    42
blanchet@57432
    43
fun encode_feature (names, weight) =
blanchet@57432
    44
  encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
blanchet@57432
    45
blanchet@57432
    46
val encode_features = map encode_feature #> space_implode " "
blanchet@57432
    47
blanchet@57431
    48
(* The suggested weights do not make much sense. *)
blanchet@57431
    49
fun extract_suggestion sugg =
blanchet@57431
    50
  (case space_explode "=" sugg of
blanchet@57431
    51
    [name, weight] => SOME (decode_str name, Real.fromString weight |> the_default 1.0)
blanchet@57431
    52
  | [name] => SOME (decode_str name, 1.0)
blanchet@57431
    53
  | _ => NONE)
blanchet@57431
    54
blanchet@57431
    55
fun extract_suggestions line =
blanchet@57431
    56
  (case space_explode ":" line of
blanchet@57431
    57
    [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs))
blanchet@57431
    58
  | _ => ("", []))
blanchet@57431
    59
blanchet@50349
    60
fun has_thm_thy th thy =
wenzelm@65458
    61
  Context.theory_name thy = Thm.theory_name th
blanchet@48316
    62
blanchet@50349
    63
fun has_thys thys th = exists (has_thm_thy th) thys
blanchet@50349
    64
blanchet@50349
    65
fun all_facts ctxt =
blanchet@48531
    66
  let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
wenzelm@58922
    67
    Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css
wenzelm@60641
    68
    |> sort (crude_thm_ord ctxt o apply2 snd)
blanchet@48531
    69
  end
blanchet@48531
    70
blanchet@51182
    71
fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
blanchet@51182
    72
blanchet@57121
    73
fun generate_accessibility ctxt thys file_name =
blanchet@48304
    74
  let
blanchet@57121
    75
    val path = Path.explode file_name
blanchet@57055
    76
blanchet@57406
    77
    fun do_fact (parents, fact) =
blanchet@57122
    78
      let val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" in
blanchet@57406
    79
        File.append path s
blanchet@57122
    80
      end
blanchet@57055
    81
blanchet@50611
    82
    val facts =
blanchet@50349
    83
      all_facts ctxt
blanchet@51182
    84
      |> filter_out (has_thys thys o snd)
blanchet@61321
    85
      |> attach_parents_to_facts []
blanchet@61321
    86
      |> map (apsnd (nickname_of_thm o snd))
blanchet@57055
    87
  in
blanchet@57122
    88
    File.write path "";
blanchet@57406
    89
    List.app do_fact facts
blanchet@57055
    90
  end
blanchet@48304
    91
blanchet@55212
    92
fun generate_features ctxt thys file_name =
blanchet@48304
    93
  let
blanchet@57388
    94
    val path = Path.explode file_name
blanchet@48304
    95
    val _ = File.write path ""
blanchet@51182
    96
    val facts = all_facts ctxt |> filter_out (has_thys thys o snd)
blanchet@57122
    97
blanchet@48385
    98
    fun do_fact ((_, stature), th) =
blanchet@48304
    99
      let
blanchet@61321
   100
        val name = nickname_of_thm th
wenzelm@65458
   101
        val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
blanchet@57055
   102
        val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
blanchet@57122
   103
      in
blanchet@57122
   104
        File.append path s
blanchet@57122
   105
      end
blanchet@57055
   106
  in
blanchet@57055
   107
    List.app do_fact facts
blanchet@57055
   108
  end
blanchet@48304
   109
blanchet@51034
   110
val prover_marker = "$a"
blanchet@51033
   111
val isar_marker = "$i"
blanchet@51033
   112
val omitted_marker = "$o"
blanchet@51034
   113
val unprovable_marker = "$u" (* axiom or definition or characteristic theorem *)
blanchet@51033
   114
val prover_failed_marker = "$x"
blanchet@51033
   115
blanchet@51033
   116
fun smart_dependencies_of ctxt params_opt facts name_tabs th isar_deps_opt =
blanchet@51033
   117
  let
blanchet@51033
   118
    val (marker, deps) =
blanchet@57055
   119
      (case params_opt of
blanchet@51033
   120
        SOME (params as {provers = prover :: _, ...}) =>
blanchet@51033
   121
        prover_dependencies_of ctxt params prover 0 facts name_tabs th
blanchet@51033
   122
        |>> (fn true => prover_marker | false => prover_failed_marker)
blanchet@51033
   123
      | NONE =>
blanchet@51033
   124
        let
blanchet@51033
   125
          val deps =
blanchet@57055
   126
            (case isar_deps_opt of
blanchet@61321
   127
              NONE => isar_dependencies_of name_tabs th
blanchet@57306
   128
            | deps => deps)
blanchet@57306
   129
        in
blanchet@57351
   130
          (case deps of
blanchet@57351
   131
            NONE => (omitted_marker, [])
blanchet@57351
   132
          | SOME [] => (unprovable_marker, [])
blanchet@57351
   133
          | SOME deps => (isar_marker, deps))
blanchet@57306
   134
        end)
blanchet@51033
   135
  in
blanchet@57055
   136
    (case trim_dependencies deps of
blanchet@51033
   137
      SOME deps => (marker, deps)
blanchet@57055
   138
    | NONE => (omitted_marker, []))
blanchet@51033
   139
  end
blanchet@50411
   140
blanchet@57121
   141
fun generate_isar_or_prover_dependencies ctxt params_opt range thys file_name =
blanchet@48304
   142
  let
blanchet@57121
   143
    val path = Path.explode file_name
blanchet@57121
   144
    val facts = filter_out (has_thys thys o snd) (all_facts ctxt)
blanchet@61321
   145
    val name_tabs = build_name_tables nickname_of_thm facts
blanchet@57055
   146
blanchet@50559
   147
    fun do_fact (j, (_, th)) =
blanchet@50559
   148
      if in_range range j then
blanchet@50559
   149
        let
blanchet@61321
   150
          val name = nickname_of_thm th
blanchet@50561
   151
          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
blanchet@57121
   152
          val access_facts = filter_accessible_from th facts
blanchet@57121
   153
          val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
blanchet@57121
   154
        in
blanchet@57121
   155
          encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n"
blanchet@57121
   156
        end
blanchet@50559
   157
      else
blanchet@50559
   158
        ""
blanchet@57055
   159
blanchet@57352
   160
    val lines = map do_fact (tag_list 1 facts)
blanchet@57055
   161
  in
blanchet@57055
   162
    File.write_list path lines
blanchet@57055
   163
  end
blanchet@48304
   164
blanchet@50411
   165
fun generate_isar_dependencies ctxt =
blanchet@54118
   166
  generate_isar_or_prover_dependencies ctxt NONE
blanchet@50411
   167
blanchet@50484
   168
fun generate_prover_dependencies ctxt params =
blanchet@50484
   169
  generate_isar_or_prover_dependencies ctxt (SOME params)
blanchet@50411
   170
blanchet@50954
   171
fun is_bad_query ctxt ho_atp step j th isar_deps =
blanchet@50954
   172
  j mod step <> 0 orelse
blanchet@58253
   173
  Thm.legacy_get_kind th = "" orelse
blanchet@57306
   174
  null (the_list isar_deps) orelse
blanchet@50523
   175
  is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
blanchet@50515
   176
blanchet@57121
   177
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
blanchet@48234
   178
  let
blanchet@55212
   179
    val ho_atp = is_ho_atp ctxt prover
blanchet@57388
   180
    val path = Path.explode file_name
blanchet@50349
   181
    val facts = all_facts ctxt
blanchet@50485
   182
    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
blanchet@61321
   183
    val name_tabs = build_name_tables nickname_of_thm facts
blanchet@57055
   184
blanchet@57407
   185
    fun do_fact (j, (name, (parents, ((_, stature), th)))) =
blanchet@50559
   186
      if in_range range j then
blanchet@50559
   187
        let
blanchet@50561
   188
          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
blanchet@61321
   189
          val isar_deps = isar_dependencies_of name_tabs th
blanchet@53127
   190
          val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
wenzelm@65458
   191
          val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
blanchet@57121
   192
          val access_facts = filter_accessible_from th new_facts @ old_facts
blanchet@51033
   193
          val (marker, deps) =
blanchet@57306
   194
            smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
blanchet@57122
   195
blanchet@53140
   196
          fun extra_features_of (((_, stature), th), weight) =
wenzelm@59582
   197
            [Thm.prop_of th]
wenzelm@65458
   198
            |> features_of ctxt (Thm.theory_name th) stature
blanchet@57406
   199
            |> map (rpair (weight * extra_feature_factor))
blanchet@57122
   200
blanchet@50559
   201
          val query =
blanchet@53127
   202
            if do_query then
blanchet@53140
   203
              let
blanchet@53141
   204
                val query_feats =
blanchet@53140
   205
                  new_facts
blanchet@53140
   206
                  |> drop (j - num_extra_feature_facts)
blanchet@53140
   207
                  |> take num_extra_feature_facts
blanchet@53140
   208
                  |> rev
blanchet@53140
   209
                  |> weight_facts_steeply
blanchet@53140
   210
                  |> map extra_features_of
blanchet@57406
   211
                  |> rpair (map (rpair 1.0) goal_feats)
blanchet@57406
   212
                  |-> fold (union (eq_fst (op =)))
blanchet@53140
   213
              in
blanchet@57122
   214
                "? " ^ string_of_int max_suggs ^ " # " ^ encode_str name ^ ": " ^
blanchet@57122
   215
                encode_strs parents ^ "; " ^ encode_features query_feats ^ "\n"
blanchet@53140
   216
              end
blanchet@53127
   217
            else
blanchet@53127
   218
              ""
blanchet@50754
   219
          val update =
blanchet@57406
   220
            "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs goal_feats ^
blanchet@57406
   221
            "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
blanchet@50559
   222
        in query ^ update end
blanchet@50559
   223
      else
blanchet@50559
   224
        ""
blanchet@57122
   225
blanchet@51182
   226
    val new_facts =
wenzelm@60641
   227
      new_facts
blanchet@61321
   228
      |> attach_parents_to_facts old_facts
blanchet@61321
   229
      |> map (`(nickname_of_thm o snd o snd))
blanchet@57407
   230
    val lines = map do_fact (tag_list 1 new_facts)
blanchet@57055
   231
  in
blanchet@57055
   232
    File.write_list path lines
blanchet@57055
   233
  end
blanchet@48239
   234
blanchet@50411
   235
fun generate_isar_commands ctxt prover =
blanchet@50954
   236
  generate_isar_or_prover_commands ctxt prover NONE
blanchet@50411
   237
blanchet@50484
   238
fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
blanchet@50484
   239
  generate_isar_or_prover_commands ctxt prover (SOME params)
blanchet@50411
   240
blanchet@57120
   241
fun generate_mepo_or_mash_suggestions mepo_or_mash_suggested_facts ctxt
blanchet@57121
   242
    (params as {provers = prover :: _, ...}) (range, step) thys max_suggs file_name =
blanchet@48239
   243
  let
blanchet@55212
   244
    val ho_atp = is_ho_atp ctxt prover
blanchet@57388
   245
    val path = Path.explode file_name
blanchet@50349
   246
    val facts = all_facts ctxt
blanchet@50485
   247
    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
blanchet@61321
   248
    val name_tabs = build_name_tables nickname_of_thm facts
blanchet@57055
   249
blanchet@50814
   250
    fun do_fact (j, ((_, th), old_facts)) =
blanchet@50906
   251
      if in_range range j then
blanchet@50906
   252
        let
blanchet@61321
   253
          val name = nickname_of_thm th
blanchet@50906
   254
          val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
blanchet@50906
   255
          val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
blanchet@52196
   256
          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
blanchet@61321
   257
          val isar_deps = isar_dependencies_of name_tabs th
blanchet@50906
   258
        in
blanchet@50954
   259
          if is_bad_query ctxt ho_atp step j th isar_deps then
blanchet@50906
   260
            ""
blanchet@50906
   261
          else
blanchet@50906
   262
            let
blanchet@50906
   263
              val suggs =
blanchet@50906
   264
                old_facts
blanchet@57121
   265
                |> filter_accessible_from th
wenzelm@65458
   266
                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th)
wenzelm@60649
   267
                  params max_suggs hyp_ts concl_t
blanchet@61321
   268
                |> map (nickname_of_thm o snd)
blanchet@57120
   269
            in
blanchet@57120
   270
              encode_str name ^ ": " ^ encode_strs suggs ^ "\n"
blanchet@57120
   271
            end
blanchet@50906
   272
        end
blanchet@50906
   273
      else
blanchet@50906
   274
        ""
blanchet@57055
   275
blanchet@50519
   276
    fun accum x (yss as ys :: _) = (x :: ys) :: yss
blanchet@57295
   277
    val old_factss = tl (fold accum new_facts [rev old_facts])
blanchet@57352
   278
    val lines = map do_fact (tag_list 1 (new_facts ~~ rev (map rev old_factss)))
blanchet@57055
   279
  in
blanchet@57055
   280
    File.write_list path lines
blanchet@57055
   281
  end
blanchet@48234
   282
blanchet@57120
   283
val generate_mepo_suggestions =
blanchet@57120
   284
  generate_mepo_or_mash_suggestions
blanchet@57407
   285
    (fn ctxt => fn _ => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
blanchet@57150
   286
       not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
blanchet@57120
   287
       #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
blanchet@57120
   288
blanchet@64522
   289
fun generate_mash_suggestions algorithm ctxt =
blanchet@57532
   290
  (Options.put_default @{system_option MaSh} algorithm;
blanchet@64522
   291
   Sledgehammer_MaSh.mash_unlearn ctxt;
blanchet@57120
   292
   generate_mepo_or_mash_suggestions
wenzelm@60649
   293
     (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
wenzelm@60649
   294
          fn max_suggs => fn hyp_ts => fn concl_t =>
blanchet@57431
   295
        tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
blanchet@57120
   296
          Sledgehammer_Util.one_year)
wenzelm@60649
   297
        #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t
blanchet@64522
   298
        #> fst) ctxt)
blanchet@57120
   299
blanchet@57055
   300
fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
blanchet@50814
   301
  let
blanchet@50814
   302
    val mesh_path = Path.explode mesh_file_name
blanchet@50814
   303
    val _ = File.write mesh_path ""
blanchet@57055
   304
blanchet@50814
   305
    fun do_fact (mash_line, mepo_line) =
blanchet@50814
   306
      let
blanchet@50829
   307
        val (name, mash_suggs) =
blanchet@50814
   308
          extract_suggestions mash_line
blanchet@57125
   309
          ||> (map fst #> weight_facts_steeply)
blanchet@50829
   310
        val (name', mepo_suggs) =
blanchet@50814
   311
          extract_suggestions mepo_line
blanchet@57125
   312
          ||> (map fst #> weight_facts_steeply)
blanchet@63692
   313
        val _ = if name = name' then () else error "Input files out of sync"
blanchet@50814
   314
        val mess =
blanchet@50814
   315
          [(mepo_weight, (mepo_suggs, [])),
blanchet@50814
   316
           (mash_weight, (mash_suggs, []))]
blanchet@61322
   317
        val mesh_suggs = mesh_facts I (op =) max_suggs mess
blanchet@50829
   318
        val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n"
blanchet@50814
   319
      in File.append mesh_path mesh_line end
blanchet@57055
   320
blanchet@50814
   321
    val mash_lines = Path.explode mash_file_name |> File.read_lines
blanchet@50814
   322
    val mepo_lines = Path.explode mepo_file_name |> File.read_lines
blanchet@50907
   323
  in
blanchet@57122
   324
    if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines)
blanchet@63692
   325
    else warning "Skipped: MaSh file missing or out of sync with MePo file"
blanchet@50907
   326
  end
blanchet@50814
   327
blanchet@48234
   328
end;