src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
author blanchet
Wed, 18 Jul 2012 08:44:04 +0200
changeset 49342 568b3193e53e
parent 49341 ef800e91d072
child 49343 ca0b7d19dd62
permissions -rw-r--r--
don't include hidden facts in relevance filter + tweak MaSh learning
blanchet@49263
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
blanchet@49263
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49263
     3
blanchet@49263
     4
Sledgehammer's machine-learning-based relevance filter (MaSh).
blanchet@49263
     5
*)
blanchet@49263
     6
blanchet@49263
     7
signature SLEDGEHAMMER_FILTER_MASH =
blanchet@49263
     8
sig
blanchet@49266
     9
  type status = ATP_Problem_Generate.status
blanchet@49266
    10
  type stature = ATP_Problem_Generate.stature
blanchet@49311
    11
  type fact = Sledgehammer_Fact.fact
blanchet@49311
    12
  type fact_override = Sledgehammer_Fact.fact_override
blanchet@49266
    13
  type params = Sledgehammer_Provers.params
blanchet@49303
    14
  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
blanchet@49266
    15
  type prover_result = Sledgehammer_Provers.prover_result
blanchet@49266
    16
blanchet@49323
    17
  val trace : bool Config.T
blanchet@49334
    18
  val MaShN : string
blanchet@49329
    19
  val meshN : string
blanchet@49329
    20
  val iterN : string
blanchet@49329
    21
  val mashN : string
blanchet@49329
    22
  val fact_filters : string list
blanchet@49318
    23
  val escape_meta : string -> string
blanchet@49318
    24
  val escape_metas : string list -> string
blanchet@49323
    25
  val unescape_meta : string -> string
blanchet@49323
    26
  val unescape_metas : string -> string list
blanchet@49326
    27
  val extract_query : string -> string * string list
blanchet@49336
    28
  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
blanchet@49336
    29
  val mesh_facts :
blanchet@49336
    30
    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
blanchet@49339
    31
  val is_likely_tautology_or_too_meta : thm -> bool
blanchet@49266
    32
  val theory_ord : theory * theory -> order
blanchet@49266
    33
  val thm_ord : thm * thm -> order
blanchet@49333
    34
  val features_of :
blanchet@49333
    35
    Proof.context -> string -> theory -> status -> term list -> string list
blanchet@49331
    36
  val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
blanchet@49266
    37
  val goal_of_thm : theory -> thm -> thm
blanchet@49336
    38
  val run_prover_for_mash :
blanchet@49333
    39
    Proof.context -> params -> string -> fact list -> thm -> prover_result
blanchet@49323
    40
  val mash_RESET : Proof.context -> unit
blanchet@49331
    41
  val mash_INIT :
blanchet@49331
    42
    Proof.context -> bool
blanchet@49331
    43
    -> (string * string list * string list * string list) list -> unit
blanchet@49323
    44
  val mash_ADD :
blanchet@49331
    45
    Proof.context -> bool
blanchet@49331
    46
    -> (string * string list * string list * string list) list -> unit
blanchet@49331
    47
  val mash_QUERY :
blanchet@49333
    48
    Proof.context -> bool -> int -> string list * string list -> string list
blanchet@49323
    49
  val mash_reset : Proof.context -> unit
blanchet@49333
    50
  val mash_could_suggest_facts : unit -> bool
blanchet@49336
    51
  val mash_can_suggest_facts : Proof.context -> bool
blanchet@49313
    52
  val mash_suggest_facts :
blanchet@49336
    53
    Proof.context -> params -> string -> int -> term list -> term
blanchet@49336
    54
    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
blanchet@49334
    55
  val mash_learn_thy :
blanchet@49334
    56
    Proof.context -> params -> theory -> Time.time -> fact list -> string
blanchet@49331
    57
  val mash_learn_proof :
blanchet@49336
    58
    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
blanchet@49303
    59
  val relevant_facts :
blanchet@49307
    60
    Proof.context -> params -> string -> int -> fact_override -> term list
blanchet@49311
    61
    -> term -> fact list -> fact list
blanchet@49334
    62
  val kill_learners : unit -> unit
blanchet@49334
    63
  val running_learners : unit -> unit
blanchet@49263
    64
end;
blanchet@49263
    65
blanchet@49263
    66
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
blanchet@49263
    67
struct
blanchet@49264
    68
blanchet@49266
    69
open ATP_Util
blanchet@49266
    70
open ATP_Problem_Generate
blanchet@49266
    71
open Sledgehammer_Util
blanchet@49266
    72
open Sledgehammer_Fact
blanchet@49266
    73
open Sledgehammer_Filter_Iter
blanchet@49266
    74
open Sledgehammer_Provers
blanchet@49333
    75
open Sledgehammer_Minimize
blanchet@49266
    76
blanchet@49323
    77
val trace =
blanchet@49323
    78
  Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
blanchet@49323
    79
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
blanchet@49323
    80
blanchet@49334
    81
val MaShN = "MaSh"
blanchet@49334
    82
blanchet@49329
    83
val meshN = "mesh"
blanchet@49329
    84
val iterN = "iter"
blanchet@49329
    85
val mashN = "mash"
blanchet@49329
    86
blanchet@49329
    87
val fact_filters = [meshN, iterN, mashN]
blanchet@49329
    88
blanchet@49329
    89
fun mash_home () = getenv "MASH_HOME"
blanchet@49329
    90
fun mash_state_dir () =
blanchet@49324
    91
  getenv "ISABELLE_HOME_USER" ^ "/mash"
blanchet@49331
    92
  |> tap (Isabelle_System.mkdir o Path.explode)
blanchet@49329
    93
fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
blanchet@49266
    94
blanchet@49266
    95
(*** Isabelle helpers ***)
blanchet@49266
    96
blanchet@49323
    97
fun meta_char c =
blanchet@49266
    98
  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse
blanchet@49266
    99
     c = #")" orelse c = #"," then
blanchet@49266
   100
    String.str c
blanchet@49266
   101
  else
blanchet@49266
   102
    (* fixed width, in case more digits follow *)
blanchet@49266
   103
    "\\" ^ stringN_of_int 3 (Char.ord c)
blanchet@49266
   104
blanchet@49323
   105
fun unmeta_chars accum [] = String.implode (rev accum)
blanchet@49323
   106
  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
blanchet@49323
   107
    (case Int.fromString (String.implode [d1, d2, d3]) of
blanchet@49323
   108
       SOME n => unmeta_chars (Char.chr n :: accum) cs
blanchet@49323
   109
     | NONE => "" (* error *))
blanchet@49323
   110
  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
blanchet@49323
   111
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
blanchet@49323
   112
blanchet@49323
   113
val escape_meta = String.translate meta_char
blanchet@49318
   114
val escape_metas = map escape_meta #> space_implode " "
blanchet@49330
   115
val unescape_meta = String.explode #> unmeta_chars []
blanchet@49330
   116
val unescape_metas =
blanchet@49330
   117
  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
blanchet@49266
   118
blanchet@49326
   119
fun extract_query line =
blanchet@49326
   120
  case space_explode ":" line of
blanchet@49330
   121
    [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
blanchet@49327
   122
  | _ => ("", [])
blanchet@49326
   123
blanchet@49326
   124
fun find_suggested facts sugg =
blanchet@49326
   125
  find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
blanchet@49326
   126
fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
blanchet@49326
   127
blanchet@49335
   128
fun sum_avg _ [] = 1000000000 (* big number *)
blanchet@49335
   129
  | sum_avg n xs = fold (Integer.add o Integer.mult n) xs 0 div (length xs)
blanchet@49328
   130
blanchet@49335
   131
fun mesh_facts max_facts [(selected, unknown)] =
blanchet@49335
   132
    take max_facts selected @ take (max_facts - length selected) unknown
blanchet@49329
   133
  | mesh_facts max_facts mess =
blanchet@49329
   134
    let
blanchet@49335
   135
      val mess = mess |> map (apfst (`length))
blanchet@49329
   136
      val n = length mess
blanchet@49329
   137
      val fact_eq = Thm.eq_thm o pairself snd
blanchet@49335
   138
      fun score_in fact ((sel_len, sels), unks) =
blanchet@49335
   139
        case find_index (curry fact_eq fact) sels of
blanchet@49335
   140
          ~1 => (case find_index (curry fact_eq fact) unks of
blanchet@49335
   141
                   ~1 => SOME sel_len
blanchet@49335
   142
                 | _ => NONE)
blanchet@49329
   143
        | j => SOME j
blanchet@49329
   144
      fun score_of fact = mess |> map_filter (score_in fact) |> sum_avg n
blanchet@49335
   145
      val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
blanchet@49329
   146
    in
blanchet@49329
   147
      facts |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
blanchet@49329
   148
            |> take max_facts
blanchet@49329
   149
    end
blanchet@49327
   150
blanchet@49318
   151
val thy_feature_prefix = "y_"
blanchet@49266
   152
blanchet@49318
   153
val thy_feature_name_of = prefix thy_feature_prefix
blanchet@49318
   154
val const_name_of = prefix const_prefix
blanchet@49318
   155
val type_name_of = prefix type_const_prefix
blanchet@49318
   156
val class_name_of = prefix class_prefix
blanchet@49266
   157
blanchet@49339
   158
fun is_likely_tautology_or_too_meta th =
blanchet@49339
   159
  let
blanchet@49339
   160
    val is_boring_const = member (op =) atp_widely_irrelevant_consts
blanchet@49339
   161
    fun is_boring_bool t =
blanchet@49339
   162
      not (exists_Const (not o is_boring_const o fst) t) orelse
blanchet@49339
   163
      exists_type (exists_subtype (curry (op =) @{typ prop})) t
blanchet@49339
   164
    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
blanchet@49339
   165
      | is_boring_prop (@{const "==>"} $ t $ u) =
blanchet@49339
   166
        is_boring_prop t andalso is_boring_prop u
blanchet@49339
   167
      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
blanchet@49339
   168
        is_boring_prop t andalso is_boring_prop u
blanchet@49339
   169
      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
blanchet@49339
   170
        is_boring_bool t andalso is_boring_bool u
blanchet@49339
   171
      | is_boring_prop _ = true
blanchet@49339
   172
  in
blanchet@49339
   173
    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
blanchet@49339
   174
  end
blanchet@49339
   175
blanchet@49339
   176
fun theory_ord p =
blanchet@49339
   177
  if Theory.eq_thy p then
blanchet@49339
   178
    EQUAL
blanchet@49339
   179
  else if Theory.subthy p then
blanchet@49339
   180
    LESS
blanchet@49339
   181
  else if Theory.subthy (swap p) then
blanchet@49339
   182
    GREATER
blanchet@49339
   183
  else case int_ord (pairself (length o Theory.ancestors_of) p) of
blanchet@49339
   184
    EQUAL => string_ord (pairself Context.theory_name p)
blanchet@49339
   185
  | order => order
blanchet@49339
   186
blanchet@49339
   187
val thm_ord = theory_ord o pairself theory_of_thm
blanchet@49339
   188
blanchet@49341
   189
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
blanchet@49341
   190
blanchet@49333
   191
fun interesting_terms_types_and_classes ctxt prover term_max_depth
blanchet@49333
   192
                                        type_max_depth ts =
blanchet@49266
   193
  let
blanchet@49333
   194
    fun is_bad_const (x as (s, _)) args =
blanchet@49333
   195
      member (op =) atp_logical_consts s orelse
blanchet@49333
   196
      fst (is_built_in_const_for_prover ctxt prover x args)
blanchet@49319
   197
    fun add_classes @{sort type} = I
blanchet@49319
   198
      | add_classes S = union (op =) (map class_name_of S)
blanchet@49266
   199
    fun do_add_type (Type (s, Ts)) =
blanchet@49266
   200
        (not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
blanchet@49266
   201
        #> fold do_add_type Ts
blanchet@49319
   202
      | do_add_type (TFree (_, S)) = add_classes S
blanchet@49319
   203
      | do_add_type (TVar (_, S)) = add_classes S
blanchet@49266
   204
    fun add_type T = type_max_depth >= 0 ? do_add_type T
blanchet@49266
   205
    fun mk_app s args =
blanchet@49266
   206
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
blanchet@49266
   207
      else s
blanchet@49266
   208
    fun patternify ~1 _ = ""
blanchet@49266
   209
      | patternify depth t =
blanchet@49266
   210
        case strip_comb t of
blanchet@49266
   211
          (Const (s, _), args) =>
blanchet@49266
   212
          mk_app (const_name_of s) (map (patternify (depth - 1)) args)
blanchet@49266
   213
        | _ => ""
blanchet@49266
   214
    fun add_term_patterns ~1 _ = I
blanchet@49266
   215
      | add_term_patterns depth t =
blanchet@49266
   216
        insert (op =) (patternify depth t)
blanchet@49266
   217
        #> add_term_patterns (depth - 1) t
blanchet@49266
   218
    val add_term = add_term_patterns term_max_depth
blanchet@49266
   219
    fun add_patterns t =
blanchet@49266
   220
      let val (head, args) = strip_comb t in
blanchet@49266
   221
        (case head of
blanchet@49333
   222
           Const (x as (_, T)) =>
blanchet@49333
   223
           not (is_bad_const x args) ? (add_term t #> add_type T)
blanchet@49266
   224
         | Free (_, T) => add_type T
blanchet@49266
   225
         | Var (_, T) => add_type T
blanchet@49266
   226
         | Abs (_, T, body) => add_type T #> add_patterns body
blanchet@49266
   227
         | _ => I)
blanchet@49266
   228
        #> fold add_patterns args
blanchet@49266
   229
      end
blanchet@49341
   230
  in [] |> fold add_patterns ts end
blanchet@49266
   231
blanchet@49266
   232
fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
blanchet@49266
   233
blanchet@49312
   234
val term_max_depth = 1
blanchet@49312
   235
val type_max_depth = 1
blanchet@49266
   236
blanchet@49266
   237
(* TODO: Generate type classes for types? *)
blanchet@49333
   238
fun features_of ctxt prover thy status ts =
blanchet@49318
   239
  thy_feature_name_of (Context.theory_name thy) ::
blanchet@49333
   240
  interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
blanchet@49333
   241
                                      ts
blanchet@49317
   242
  |> exists (not o is_lambda_free) ts ? cons "lambdas"
blanchet@49317
   243
  |> exists (exists_Const is_exists) ts ? cons "skolems"
blanchet@49317
   244
  |> (case status of
blanchet@49317
   245
        General => I
blanchet@49317
   246
      | Induction => cons "induction"
blanchet@49317
   247
      | Intro => cons "intro"
blanchet@49317
   248
      | Inductive => cons "inductive"
blanchet@49317
   249
      | Elim => cons "elim"
blanchet@49317
   250
      | Simp => cons "simp"
blanchet@49317
   251
      | Def => cons "def")
blanchet@49266
   252
blanchet@49341
   253
fun isabelle_dependencies_of all_facts = thms_in_proof (SOME all_facts)
blanchet@49266
   254
blanchet@49266
   255
val freezeT = Type.legacy_freeze_type
blanchet@49266
   256
blanchet@49266
   257
fun freeze (t $ u) = freeze t $ freeze u
blanchet@49266
   258
  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
blanchet@49266
   259
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
blanchet@49266
   260
  | freeze (Const (s, T)) = Const (s, freezeT T)
blanchet@49266
   261
  | freeze (Free (s, T)) = Free (s, freezeT T)
blanchet@49266
   262
  | freeze t = t
blanchet@49266
   263
blanchet@49266
   264
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
blanchet@49266
   265
blanchet@49336
   266
fun run_prover_for_mash ctxt params prover facts goal =
blanchet@49266
   267
  let
blanchet@49266
   268
    val problem =
blanchet@49266
   269
      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
blanchet@49304
   270
       facts = facts |> map (apfst (apfst (fn name => name ())))
blanchet@49333
   271
                     |> map Untranslated_Fact}
blanchet@49336
   272
    val prover = get_minimizing_prover ctxt Normal (K ()) prover
blanchet@49266
   273
  in prover params (K (K (K ""))) problem end
blanchet@49266
   274
blanchet@49266
   275
blanchet@49317
   276
(*** Low-level communication with MaSh ***)
blanchet@49317
   277
blanchet@49338
   278
fun write_file (xs, f) file =
blanchet@49333
   279
  let val path = Path.explode file in
blanchet@49338
   280
    File.write path "";
blanchet@49338
   281
    xs |> chunk_list 500
blanchet@49338
   282
       |> List.app (File.append path o space_implode "" o map f)
blanchet@49333
   283
  end
blanchet@49331
   284
blanchet@49331
   285
fun mash_info overlord =
blanchet@49331
   286
  if overlord then (getenv "ISABELLE_HOME_USER", "")
blanchet@49331
   287
  else (getenv "ISABELLE_TMP", serial_string ())
blanchet@49331
   288
blanchet@49331
   289
fun run_mash ctxt (temp_dir, serial) core =
blanchet@49326
   290
  let
blanchet@49331
   291
    val log_file = temp_dir ^ "/mash_log" ^ serial
blanchet@49331
   292
    val err_file = temp_dir ^ "/mash_err" ^ serial
blanchet@49326
   293
    val command =
blanchet@49331
   294
      mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^
blanchet@49331
   295
      " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
blanchet@49331
   296
  in
blanchet@49331
   297
    trace_msg ctxt (fn () => "Running " ^ command);
blanchet@49338
   298
    write_file ([], K "") log_file;
blanchet@49338
   299
    write_file ([], K "") err_file;
blanchet@49331
   300
    Isabelle_System.bash command; ()
blanchet@49331
   301
  end
blanchet@49326
   302
blanchet@49331
   303
fun run_mash_init ctxt overlord write_access write_feats write_deps =
blanchet@49331
   304
  let
blanchet@49331
   305
    val info as (temp_dir, serial) = mash_info overlord
blanchet@49331
   306
    val in_dir = temp_dir ^ "/mash_init" ^ serial
blanchet@49331
   307
                 |> tap (Isabelle_System.mkdir o Path.explode)
blanchet@49331
   308
  in
blanchet@49331
   309
    write_file write_access (in_dir ^ "/mash_accessibility");
blanchet@49331
   310
    write_file write_feats (in_dir ^ "/mash_features");
blanchet@49331
   311
    write_file write_deps (in_dir ^ "/mash_dependencies");
blanchet@49331
   312
    run_mash ctxt info ("--init --inputDir " ^ in_dir)
blanchet@49331
   313
  end
blanchet@49331
   314
blanchet@49333
   315
fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
blanchet@49331
   316
  let
blanchet@49331
   317
    val info as (temp_dir, serial) = mash_info overlord
blanchet@49333
   318
    val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
blanchet@49331
   319
    val cmd_file = temp_dir ^ "/mash_commands" ^ serial
blanchet@49331
   320
  in
blanchet@49338
   321
    write_file ([], K "") sugg_file;
blanchet@49331
   322
    write_file write_cmds cmd_file;
blanchet@49331
   323
    run_mash ctxt info
blanchet@49333
   324
             ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
blanchet@49333
   325
              " --numberOfPredictions " ^ string_of_int max_suggs ^
blanchet@49331
   326
              (if save then " --saveModel" else ""));
blanchet@49333
   327
    read_suggs (fn () => File.read_lines (Path.explode sugg_file))
blanchet@49331
   328
  end
blanchet@49331
   329
blanchet@49331
   330
fun str_of_update (name, parents, feats, deps) =
blanchet@49331
   331
  "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
blanchet@49326
   332
  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
blanchet@49326
   333
blanchet@49331
   334
fun str_of_query (parents, feats) =
blanchet@49331
   335
  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
blanchet@49331
   336
blanchet@49331
   337
fun init_str_of_update get (upd as (name, _, _, _)) =
blanchet@49331
   338
  escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
blanchet@49326
   339
blanchet@49323
   340
fun mash_RESET ctxt =
blanchet@49329
   341
  let val path = mash_state_dir () |> Path.explode in
blanchet@49324
   342
    trace_msg ctxt (K "MaSh RESET");
blanchet@49324
   343
    File.fold_dir (fn file => fn () =>
blanchet@49324
   344
                      File.rm (Path.append path (Path.basic file)))
blanchet@49324
   345
                  path ()
blanchet@49324
   346
  end
blanchet@49317
   347
blanchet@49331
   348
fun mash_INIT ctxt _ [] = mash_RESET ctxt
blanchet@49331
   349
  | mash_INIT ctxt overlord upds =
blanchet@49331
   350
    (trace_msg ctxt (fn () => "MaSh INIT " ^
blanchet@49331
   351
         elide_string 1000 (space_implode " " (map #1 upds)));
blanchet@49338
   352
     run_mash_init ctxt overlord (upds, init_str_of_update #2)
blanchet@49338
   353
                   (upds, init_str_of_update #3) (upds, init_str_of_update #4))
blanchet@49317
   354
blanchet@49331
   355
fun mash_ADD _ _ [] = ()
blanchet@49331
   356
  | mash_ADD ctxt overlord upds =
blanchet@49331
   357
    (trace_msg ctxt (fn () => "MaSh ADD " ^
blanchet@49331
   358
         elide_string 1000 (space_implode " " (map #1 upds)));
blanchet@49338
   359
     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
blanchet@49317
   360
blanchet@49333
   361
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
blanchet@49329
   362
  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
blanchet@49333
   363
   run_mash_commands ctxt overlord false max_suggs
blanchet@49338
   364
       ([query], str_of_query)
blanchet@49333
   365
       (fn suggs => snd (extract_query (List.last (suggs ()))))
blanchet@49326
   366
   handle List.Empty => [])
blanchet@49317
   367
blanchet@49317
   368
blanchet@49266
   369
(*** High-level communication with MaSh ***)
blanchet@49266
   370
blanchet@49336
   371
fun try_graph ctxt when def f =
blanchet@49336
   372
  f ()
blanchet@49336
   373
  handle Graph.CYCLES (cycle :: _) =>
blanchet@49336
   374
         (trace_msg ctxt (fn () =>
blanchet@49336
   375
              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
blanchet@49336
   376
       | Graph.UNDEF name =>
blanchet@49336
   377
         (trace_msg ctxt (fn () =>
blanchet@49336
   378
              "Unknown fact " ^ quote name ^ " when " ^ when); def)
blanchet@49336
   379
blanchet@49316
   380
type mash_state =
blanchet@49331
   381
  {thys : bool Symtab.table,
blanchet@49331
   382
   fact_graph : unit Graph.T}
blanchet@49264
   383
blanchet@49331
   384
val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
blanchet@49316
   385
blanchet@49316
   386
local
blanchet@49316
   387
blanchet@49336
   388
fun mash_load _ (state as (true, _)) = state
blanchet@49336
   389
  | mash_load ctxt _ =
blanchet@49324
   390
    let val path = mash_state_path () in
blanchet@49317
   391
      (true,
blanchet@49317
   392
       case try File.read_lines path of
blanchet@49331
   393
         SOME (comp_thys :: incomp_thys :: fact_lines) =>
blanchet@49317
   394
         let
blanchet@49331
   395
           fun add_thy comp thy = Symtab.update (thy, comp)
blanchet@49337
   396
           fun add_edge_to name parent =
blanchet@49337
   397
             Graph.default_node (parent, ())
blanchet@49337
   398
             #> Graph.add_edge (parent, name)
blanchet@49331
   399
           fun add_fact_line line =
blanchet@49331
   400
             case extract_query line of
blanchet@49331
   401
               ("", _) => I (* shouldn't happen *)
blanchet@49331
   402
             | (name, parents) =>
blanchet@49331
   403
               Graph.default_node (name, ())
blanchet@49337
   404
               #> fold (add_edge_to name) parents
blanchet@49331
   405
           val thys =
blanchet@49331
   406
             Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
blanchet@49331
   407
                          |> fold (add_thy false) (unescape_metas incomp_thys)
blanchet@49336
   408
           val fact_graph =
blanchet@49337
   409
             try_graph ctxt "loading state" Graph.empty (fn () =>
blanchet@49336
   410
                 Graph.empty |> fold add_fact_line fact_lines)
blanchet@49331
   411
         in {thys = thys, fact_graph = fact_graph} end
blanchet@49319
   412
       | _ => empty_state)
blanchet@49317
   413
    end
blanchet@49316
   414
blanchet@49331
   415
fun mash_save ({thys, fact_graph, ...} : mash_state) =
blanchet@49316
   416
  let
blanchet@49324
   417
    val path = mash_state_path ()
blanchet@49331
   418
    val thys = Symtab.dest thys
blanchet@49333
   419
    val line_for_thys = escape_metas o AList.find (op =) thys
blanchet@49333
   420
    fun fact_line_for name parents =
blanchet@49333
   421
      escape_meta name ^ ": " ^ escape_metas parents
blanchet@49331
   422
    val append_fact = File.append path o suffix "\n" oo fact_line_for
blanchet@49316
   423
  in
blanchet@49331
   424
    File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n");
blanchet@49331
   425
    Graph.fold (fn (name, ((), (parents, _))) => fn () =>
blanchet@49331
   426
                   append_fact name (Graph.Keys.dest parents))
blanchet@49331
   427
        fact_graph ()
blanchet@49316
   428
  end
blanchet@49316
   429
blanchet@49317
   430
val global_state =
blanchet@49319
   431
  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
blanchet@49316
   432
blanchet@49316
   433
in
blanchet@49316
   434
blanchet@49336
   435
fun mash_map ctxt f =
blanchet@49336
   436
  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
blanchet@49316
   437
blanchet@49336
   438
fun mash_get ctxt =
blanchet@49336
   439
  Synchronized.change_result global_state (mash_load ctxt #> `snd)
blanchet@49317
   440
blanchet@49323
   441
fun mash_reset ctxt =
blanchet@49317
   442
  Synchronized.change global_state (fn _ =>
blanchet@49324
   443
      (mash_RESET ctxt; File.write (mash_state_path ()) "";
blanchet@49323
   444
       (true, empty_state)))
blanchet@49316
   445
blanchet@49316
   446
end
blanchet@49316
   447
blanchet@49333
   448
fun mash_could_suggest_facts () = mash_home () <> ""
blanchet@49336
   449
fun mash_can_suggest_facts ctxt =
blanchet@49336
   450
  not (Graph.is_empty (#fact_graph (mash_get ctxt)))
blanchet@49264
   451
blanchet@49336
   452
fun parents_wrt_facts ctxt facts fact_graph =
blanchet@49331
   453
  let
blanchet@49333
   454
    val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
blanchet@49331
   455
    val facts =
blanchet@49336
   456
      try_graph ctxt "when computing ancestor facts" [] (fn () =>
blanchet@49336
   457
          [] |> fold (cons o Thm.get_name_hint o snd) facts
blanchet@49336
   458
             |> filter (Symtab.defined graph_facts)
blanchet@49336
   459
             |> Graph.all_preds fact_graph)
blanchet@49333
   460
    val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
blanchet@49336
   461
  in
blanchet@49336
   462
    try_graph ctxt "when computing parent facts" [] (fn () =>
blanchet@49336
   463
        fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals)
blanchet@49336
   464
  end
blanchet@49331
   465
blanchet@49333
   466
(* Generate more suggestions than requested, because some might be thrown out
blanchet@49333
   467
   later for various reasons and "meshing" gives better results with some
blanchet@49333
   468
   slack. *)
blanchet@49333
   469
fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
blanchet@49333
   470
blanchet@49335
   471
fun is_fact_in_graph fact_graph (_, th) =
blanchet@49335
   472
  can (Graph.get_node fact_graph) (Thm.get_name_hint th)
blanchet@49335
   473
blanchet@49333
   474
fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
blanchet@49333
   475
                       concl_t facts =
blanchet@49316
   476
  let
blanchet@49317
   477
    val thy = Proof_Context.theory_of ctxt
blanchet@49336
   478
    val fact_graph = #fact_graph (mash_get ctxt)
blanchet@49336
   479
    val parents = parents_wrt_facts ctxt facts fact_graph
blanchet@49333
   480
    val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
blanchet@49333
   481
    val suggs =
blanchet@49335
   482
      if Graph.is_empty fact_graph then []
blanchet@49335
   483
      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
blanchet@49335
   484
    val selected = facts |> suggested_facts suggs
blanchet@49335
   485
    val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
blanchet@49335
   486
  in (selected, unknown) end
blanchet@49264
   487
blanchet@49331
   488
fun add_thys_for thy =
blanchet@49331
   489
  let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in
blanchet@49331
   490
    add false thy #> fold (add true) (Theory.ancestors_of thy)
blanchet@49331
   491
  end
blanchet@49319
   492
blanchet@49331
   493
fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
blanchet@49331
   494
  let
blanchet@49331
   495
    fun maybe_add_from from (accum as (parents, graph)) =
blanchet@49336
   496
      try_graph ctxt "updating graph" accum (fn () =>
blanchet@49336
   497
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
blanchet@49336
   498
    val graph = graph |> Graph.default_node (name, ())
blanchet@49331
   499
    val (parents, graph) = ([], graph) |> fold maybe_add_from parents
blanchet@49331
   500
    val (deps, graph) = ([], graph) |> fold maybe_add_from deps
blanchet@49331
   501
  in ((name, parents, feats, deps) :: upds, graph) end
blanchet@49321
   502
blanchet@49333
   503
val pass1_learn_timeout_factor = 0.5
blanchet@49333
   504
blanchet@49333
   505
(* The timeout is understood in a very slack fashion. *)
blanchet@49334
   506
fun mash_learn_thy ctxt ({provers, verbose, overlord, ...} : params) thy timeout
blanchet@49334
   507
                   facts =
blanchet@49319
   508
  let
blanchet@49333
   509
    val timer = Timer.startRealTimer ()
blanchet@49333
   510
    val prover = hd provers
blanchet@49333
   511
    fun timed_out frac =
blanchet@49333
   512
      Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
blanchet@49336
   513
    val {fact_graph, ...} = mash_get ctxt
blanchet@49335
   514
    val new_facts =
blanchet@49335
   515
      facts |> filter_out (is_fact_in_graph fact_graph)
blanchet@49335
   516
            |> sort (thm_ord o pairself snd)
blanchet@49323
   517
  in
blanchet@49323
   518
    if null new_facts then
blanchet@49334
   519
      ""
blanchet@49323
   520
    else
blanchet@49319
   521
      let
blanchet@49323
   522
        val ths = facts |> map snd
blanchet@49330
   523
        val all_names =
blanchet@49339
   524
          ths |> filter_out is_likely_tautology_or_too_meta
blanchet@49331
   525
              |> map (rpair () o Thm.get_name_hint)
blanchet@49331
   526
              |> Symtab.make
blanchet@49333
   527
        fun do_fact _ (accum as (_, true)) = accum
blanchet@49333
   528
          | do_fact ((_, (_, status)), th) ((parents, upds), false) =
blanchet@49333
   529
            let
blanchet@49333
   530
              val name = Thm.get_name_hint th
blanchet@49333
   531
              val feats = features_of ctxt prover thy status [prop_of th]
blanchet@49333
   532
              val deps = isabelle_dependencies_of all_names th
blanchet@49333
   533
              val upd = (name, parents, feats, deps)
blanchet@49333
   534
            in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
blanchet@49336
   535
        val parents = parents_wrt_facts ctxt facts fact_graph
blanchet@49333
   536
        val ((_, upds), _) =
blanchet@49333
   537
          ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
blanchet@49333
   538
        val n = length upds
blanchet@49331
   539
        fun trans {thys, fact_graph} =
blanchet@49331
   540
          let
blanchet@49331
   541
            val mash_INIT_or_ADD =
blanchet@49331
   542
              if Graph.is_empty fact_graph then mash_INIT else mash_ADD
blanchet@49331
   543
            val (upds, fact_graph) =
blanchet@49331
   544
              ([], fact_graph) |> fold (update_fact_graph ctxt) upds
blanchet@49331
   545
          in
blanchet@49331
   546
            (mash_INIT_or_ADD ctxt overlord (rev upds);
blanchet@49331
   547
             {thys = thys |> add_thys_for thy,
blanchet@49331
   548
              fact_graph = fact_graph})
blanchet@49331
   549
          end
blanchet@49333
   550
      in
blanchet@49336
   551
        mash_map ctxt trans;
blanchet@49334
   552
        if verbose then
blanchet@49334
   553
          "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
blanchet@49334
   554
          (if verbose then
blanchet@49334
   555
             " in " ^ string_from_time (Timer.checkRealTimer timer)
blanchet@49334
   556
           else
blanchet@49334
   557
             "") ^ "."
blanchet@49334
   558
        else
blanchet@49334
   559
          ""
blanchet@49333
   560
      end
blanchet@49323
   561
  end
blanchet@49319
   562
blanchet@49336
   563
fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
blanchet@49331
   564
  let
blanchet@49331
   565
    val thy = Proof_Context.theory_of ctxt
blanchet@49333
   566
    val prover = hd provers
blanchet@49342
   567
    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
blanchet@49333
   568
    val feats = features_of ctxt prover thy General [t]
blanchet@49331
   569
    val deps = used_ths |> map Thm.get_name_hint
blanchet@49331
   570
  in
blanchet@49336
   571
    mash_map ctxt (fn {thys, fact_graph} =>
blanchet@49324
   572
        let
blanchet@49336
   573
          val parents = parents_wrt_facts ctxt facts fact_graph
blanchet@49331
   574
          val upds = [(name, parents, feats, deps)]
blanchet@49331
   575
          val (upds, fact_graph) =
blanchet@49331
   576
            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
blanchet@49324
   577
        in
blanchet@49331
   578
          mash_ADD ctxt overlord upds;
blanchet@49331
   579
          {thys = thys, fact_graph = fact_graph}
blanchet@49331
   580
        end)
blanchet@49331
   581
  end
blanchet@49264
   582
blanchet@49333
   583
(* The threshold should be large enough so that MaSh doesn't kick in for Auto
blanchet@49333
   584
   Sledgehammer and Try. *)
blanchet@49333
   585
val min_secs_for_learning = 15
blanchet@49342
   586
val learn_timeout_factor = 2.0
blanchet@49333
   587
blanchet@49336
   588
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
blanchet@49336
   589
        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
blanchet@49329
   590
  if not (subset (op =) (the_list fact_filter, fact_filters)) then
blanchet@49329
   591
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
blanchet@49329
   592
  else if only then
blanchet@49304
   593
    facts
blanchet@49336
   594
  else if max_facts <= 0 orelse null facts then
blanchet@49303
   595
    []
blanchet@49303
   596
  else
blanchet@49303
   597
    let
blanchet@49333
   598
      val thy = Proof_Context.theory_of ctxt
blanchet@49342
   599
      fun maybe_learn () =
blanchet@49336
   600
        if not learn orelse Async_Manager.has_running_threads MaShN then
blanchet@49334
   601
          ()
blanchet@49334
   602
        else if Time.toSeconds timeout >= min_secs_for_learning then
blanchet@49334
   603
          let
blanchet@49342
   604
            val soft_timeout = time_mult learn_timeout_factor timeout
blanchet@49342
   605
            val hard_timeout = time_mult 4.0 soft_timeout
blanchet@49334
   606
            val birth_time = Time.now ()
blanchet@49334
   607
            val death_time = Time.+ (birth_time, hard_timeout)
blanchet@49334
   608
            val desc = ("machine learner for Sledgehammer", "")
blanchet@49334
   609
          in
blanchet@49334
   610
            Async_Manager.launch MaShN birth_time death_time desc
blanchet@49334
   611
                (fn () =>
blanchet@49334
   612
                    (true, mash_learn_thy ctxt params thy soft_timeout facts))
blanchet@49334
   613
          end
blanchet@49333
   614
        else
blanchet@49333
   615
          ()
blanchet@49329
   616
      val fact_filter =
blanchet@49329
   617
        case fact_filter of
blanchet@49342
   618
          SOME ff => (() |> ff <> iterN ? maybe_learn; ff)
blanchet@49333
   619
        | NONE =>
blanchet@49342
   620
          if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
blanchet@49342
   621
          else if mash_could_suggest_facts () then (maybe_learn (); iterN)
blanchet@49333
   622
          else iterN
blanchet@49303
   623
      val add_ths = Attrib.eval_thms ctxt add
blanchet@49307
   624
      fun prepend_facts ths accepts =
blanchet@49303
   625
        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
blanchet@49307
   626
         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
blanchet@49308
   627
        |> take max_facts
blanchet@49329
   628
      fun iter () =
blanchet@49313
   629
        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
blanchet@49313
   630
                                 concl_t facts
blanchet@49329
   631
      fun mash () =
blanchet@49335
   632
        mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
blanchet@49329
   633
      val mess =
blanchet@49335
   634
        [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
blanchet@49329
   635
           |> (if fact_filter <> iterN then cons (mash ()) else I)
blanchet@49303
   636
    in
blanchet@49328
   637
      mesh_facts max_facts mess
blanchet@49303
   638
      |> not (null add_ths) ? prepend_facts add_ths
blanchet@49303
   639
    end
blanchet@49303
   640
blanchet@49334
   641
fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
blanchet@49334
   642
fun running_learners () = Async_Manager.running_threads MaShN "learner"
blanchet@49334
   643
blanchet@49263
   644
end;