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