src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
author blanchet
Wed, 18 Jul 2012 08:44:04 +0200
changeset 48316 252f45c04042
parent 48315 82d6e46c673f
child 48318 325c8fd0d762
permissions -rw-r--r--
drastic overhaul of MaSh data structures + fixed a few performance issues
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
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    18
  val meshN : string
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    19
  val iterN : string
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    20
  val mashN : string
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    21
  val fact_filters : string list
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    22
  val escape_meta : string -> string
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    23
  val escape_metas : string list -> string
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    24
  val unescape_meta : string -> string
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    25
  val unescape_metas : string -> string list
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    26
  val extract_query : string -> string * string list
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
    27
  val suggested_facts : string list -> fact list -> fact list
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
    28
  val mesh_facts : int -> (fact list * int option) list -> fact list
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
    29
  val is_likely_tautology : thm -> bool
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
    30
  val is_too_meta : thm -> bool
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    31
  val theory_ord : theory * theory -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    32
  val thm_ord : thm * thm -> order
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
    33
  val features_of : theory -> status -> term list -> string list
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    34
  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
    35
  val goal_of_thm : theory -> thm -> thm
48296
e7f01b7e244e gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents: 48293
diff changeset
    36
  val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    37
  val mash_RESET : Proof.context -> unit
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    38
  val mash_INIT :
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    39
    Proof.context -> bool
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    40
    -> (string * string list * string list * string list) list -> unit
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    41
  val mash_ADD :
48316
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
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    44
  val mash_QUERY :
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    45
    Proof.context -> bool -> string list * string list -> string list
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    46
  val mash_reset : Proof.context -> unit
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    47
  val mash_can_suggest_facts : Proof.context -> bool
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
    48
  val mash_suggest_facts :
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    49
    Proof.context -> params -> string -> term list -> term -> fact list
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    50
    -> fact list
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    51
  val mash_learn_thy : Proof.context -> params -> theory -> real -> unit
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    52
  val mash_learn_proof :
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    53
    Proof.context -> params -> term -> thm list -> fact list -> unit
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
    54
  val relevant_facts :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    55
    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
    56
    -> term -> fact list -> fact list
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    57
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    58
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    59
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    60
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
    61
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    62
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    63
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    64
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    65
open Sledgehammer_Fact
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    66
open Sledgehammer_Filter_Iter
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    67
open Sledgehammer_Provers
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    68
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    69
val trace =
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    70
  Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    71
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    72
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    73
val meshN = "mesh"
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    74
val iterN = "iter"
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    75
val mashN = "mash"
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    76
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    77
val fact_filters = [meshN, iterN, mashN]
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    78
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    79
fun mash_home () = getenv "MASH_HOME"
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    80
fun mash_state_dir () =
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
    81
  getenv "ISABELLE_HOME_USER" ^ "/mash"
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    82
  |> tap (Isabelle_System.mkdir o Path.explode)
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    83
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
    84
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    85
(*** Isabelle helpers ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    86
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    87
fun meta_char c =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    88
  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
    89
     c = #")" orelse c = #"," then
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    90
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    91
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    92
    (* fixed width, in case more digits follow *)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    93
    "\\" ^ stringN_of_int 3 (Char.ord c)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    94
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    95
fun unmeta_chars accum [] = String.implode (rev accum)
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    96
  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    97
    (case Int.fromString (String.implode [d1, d2, d3]) of
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    98
       SOME n => unmeta_chars (Char.chr n :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    99
     | NONE => "" (* error *))
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   100
  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   101
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   102
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   103
val escape_meta = String.translate meta_char
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   104
val escape_metas = map escape_meta #> space_implode " "
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   105
val unescape_meta = String.explode #> unmeta_chars []
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   106
val unescape_metas =
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   107
  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   108
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   109
fun extract_query line =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   110
  case space_explode ":" line of
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   111
    [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   112
  | _ => ("", [])
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   113
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   114
fun find_suggested facts sugg =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   115
  find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   116
fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   117
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   118
fun sum_avg n xs =
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   119
  fold (Integer.add o Integer.mult n) xs 0 div (length xs)
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   120
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   121
fun mesh_facts max_facts [(facts, _)] = facts |> take max_facts
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   122
  | mesh_facts max_facts mess =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   123
    let
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   124
      val n = length mess
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   125
      val fact_eq = Thm.eq_thm o pairself snd
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   126
      fun score_in fact (facts, def) =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   127
        case find_index (curry fact_eq fact) facts of
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   128
          ~1 => def
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   129
        | j => SOME j
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   130
      fun score_of fact = mess |> map_filter (score_in fact) |> sum_avg n
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   131
      val facts = fold (union fact_eq o take max_facts o fst) mess []
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   132
    in
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   133
      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
   134
            |> take max_facts
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   135
    end
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   136
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   137
val thy_feature_prefix = "y_"
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   138
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   139
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
   140
val const_name_of = prefix const_prefix
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   141
val type_name_of = prefix type_const_prefix
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   142
val class_name_of = prefix class_prefix
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   143
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   144
local
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   145
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   146
fun has_bool @{typ bool} = true
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   147
  | has_bool (Type (_, Ts)) = exists has_bool Ts
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   148
  | has_bool _ = false
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   149
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   150
fun has_fun (Type (@{type_name fun}, _)) = true
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   151
  | has_fun (Type (_, Ts)) = exists has_fun Ts
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   152
  | has_fun _ = false
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   153
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   154
val is_conn = member (op =)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   155
  [@{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
   156
   @{const_name HOL.implies}, @{const_name Not},
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   157
   @{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
   158
   @{const_name HOL.eq}]
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
val has_bool_arg_const =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   161
  exists_Const (fn (c, T) =>
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   162
                   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
   163
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   164
fun higher_inst_const thy (s, T) =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   165
  case binder_types T of
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   166
    [] => false
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   167
  | 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
   168
  handle TYPE _ => false
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   169
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   170
val binders = [@{const_name All}, @{const_name Ex}]
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   171
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   172
in
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
fun is_fo_term thy t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   175
  let
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   176
    val t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   177
      t |> Envir.beta_eta_contract
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   178
        |> transform_elim_prop
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   179
        |> Object_Logic.atomize_term thy
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   180
  in
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   181
    Term.is_first_order binders t andalso
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   182
    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
   183
                          | _ => false) t orelse
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   184
         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
   185
  end
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   186
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   187
end
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   188
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   189
fun interesting_terms_types_and_classes term_max_depth type_max_depth ts =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   190
  let
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   191
    val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   192
    val bad_consts = atp_widely_irrelevant_consts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   193
    fun add_classes @{sort type} = I
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   194
      | 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
   195
    fun do_add_type (Type (s, Ts)) =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   196
        (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
   197
        #> fold do_add_type Ts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   198
      | do_add_type (TFree (_, S)) = add_classes S
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   199
      | do_add_type (TVar (_, S)) = add_classes S
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   200
    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
   201
    fun mk_app s args =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   202
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   203
      else s
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   204
    fun patternify ~1 _ = ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   205
      | patternify depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   206
        case strip_comb t of
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   207
          (Const (s, _), args) =>
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   208
          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
   209
        | _ => ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   210
    fun add_term_patterns ~1 _ = I
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   211
      | add_term_patterns depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   212
        insert (op =) (patternify depth t)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   213
        #> add_term_patterns (depth - 1) t
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   214
    val add_term = add_term_patterns term_max_depth
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   215
    fun add_patterns t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   216
      let val (head, args) = strip_comb t in
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   217
        (case head of
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   218
           Const (s, T) =>
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   219
           not (member (op =) bad_consts s) ? (add_term t #> add_type T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   220
         | Free (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   221
         | Var (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   222
         | Abs (_, T, body) => add_type T #> add_patterns body
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   223
         | _ => I)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   224
        #> fold add_patterns args
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   225
      end
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   226
  in [] |> fold add_patterns ts |> sort string_ord end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   227
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   228
fun is_likely_tautology th =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   229
  null (interesting_terms_types_and_classes 0 ~1 [prop_of th]) andalso
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   230
  not (Thm.eq_thm_prop (@{thm ext}, th))
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   231
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   232
(* ### FIXME: optimize *)
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   233
fun is_too_meta th =
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   234
  fastype_of (Object_Logic.atomize_term (theory_of_thm th) (prop_of th))
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   235
  <> @{typ bool}
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   236
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   237
fun theory_ord p =
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   238
  if Theory.eq_thy p then
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   239
    EQUAL
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   240
  else if Theory.subthy p then
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   241
    LESS
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   242
  else if Theory.subthy (swap p) then
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   243
    GREATER
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   244
  else case int_ord (pairself (length o Theory.ancestors_of) p) of
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   245
    EQUAL => string_ord (pairself Context.theory_name p)
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   246
  | order => order
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   247
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   248
val thm_ord = theory_ord o pairself theory_of_thm
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   249
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   250
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
   251
48297
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   252
val term_max_depth = 1
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   253
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   254
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   255
(* TODO: Generate type classes for types? *)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   256
fun features_of thy status ts =
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   257
  thy_feature_name_of (Context.theory_name thy) ::
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   258
  interesting_terms_types_and_classes term_max_depth type_max_depth ts
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   259
  |> exists (not o is_lambda_free) ts ? cons "lambdas"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   260
  |> exists (exists_Const is_exists) ts ? cons "skolems"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   261
  |> exists (not o is_fo_term thy) ts ? cons "ho"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   262
  |> (case status of
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   263
        General => I
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   264
      | Induction => cons "induction"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   265
      | Intro => cons "intro"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   266
      | Inductive => cons "inductive"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   267
      | Elim => cons "elim"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   268
      | Simp => cons "simp"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   269
      | Def => cons "def")
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   270
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   271
fun isabelle_dependencies_of all_facts =
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   272
  thms_in_proof (SOME all_facts) #> sort string_ord
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   273
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   274
val freezeT = Type.legacy_freeze_type
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 freeze (t $ u) = freeze t $ freeze u
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   277
  | 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
   278
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   279
  | freeze (Const (s, T)) = Const (s, freezeT T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   280
  | freeze (Free (s, T)) = Free (s, freezeT T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   281
  | freeze t = t
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   282
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   283
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
   284
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   285
fun run_prover ctxt (params as {provers, ...}) facts goal =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   286
  let
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   287
    val problem =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   288
      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   289
       facts = facts |> map (apfst (apfst (fn name => name ())))
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   290
                     |> map Sledgehammer_Provers.Untranslated_Fact}
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   291
    val prover =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   292
      Sledgehammer_Minimize.get_minimizing_prover ctxt
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   293
          Sledgehammer_Provers.Normal (hd provers)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   294
  in prover params (K (K (K ""))) problem end
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   295
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   296
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   297
(*** Low-level communication with MaSh ***)
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   298
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   299
val max_preds = 500
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   300
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   301
fun mash_info overlord =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   302
  if overlord then (getenv "ISABELLE_HOME_USER", "")
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   303
  else (getenv "ISABELLE_TMP", serial_string ())
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   304
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   305
fun run_mash ctxt (temp_dir, serial) core =
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   306
  let
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   307
    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
   308
    val err_file = temp_dir ^ "/mash_err" ^ serial
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   309
    val command =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   310
      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
   311
      " --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
   312
  in
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   313
    trace_msg ctxt (fn () => "Running " ^ command);
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   314
    Isabelle_System.bash command; ()
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   315
  end
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   317
fun write_file write file =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   318
  let val path = Path.explode file in
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   319
    File.write path ""; write (File.append path)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   320
  end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   321
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   322
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
   323
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   324
    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
   325
    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
   326
                 |> tap (Isabelle_System.mkdir o Path.explode)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   327
  in
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   328
    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
   329
    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
   330
    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
   331
    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
   332
  end
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   333
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   334
fun run_mash_commands ctxt overlord save write_cmds read_preds =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   335
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   336
    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
   337
    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
   338
    val pred_file = temp_dir ^ "/mash_preds" ^ serial
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   339
  in
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   340
    write_file write_cmds cmd_file;
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   341
    run_mash ctxt info
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   342
             ("--inputFile " ^ cmd_file ^ " --predictions " ^ pred_file ^
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   343
              " --numberOfPredictions " ^ string_of_int max_preds ^
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   344
              (if save then " --saveModel" else ""));
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   345
    read_preds (fn () => File.read_lines (Path.explode pred_file))
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   346
  end
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   347
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   348
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
   349
  "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   350
  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   351
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   352
fun str_of_query (parents, feats) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   353
  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   354
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   355
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
   356
  escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n"
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   357
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   358
fun mash_RESET ctxt =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   359
  let val path = mash_state_dir () |> Path.explode in
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   360
    trace_msg ctxt (K "MaSh RESET");
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   361
    File.fold_dir (fn file => fn () =>
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   362
                      File.rm (Path.append path (Path.basic file)))
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   363
                  path ()
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   364
  end
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   365
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   366
fun mash_INIT ctxt _ [] = mash_RESET ctxt
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   367
  | mash_INIT ctxt overlord upds =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   368
    (trace_msg ctxt (fn () => "MaSh INIT " ^
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   369
         elide_string 1000 (space_implode " " (map #1 upds)));
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   370
     run_mash_init ctxt overlord
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   371
         (fn append => List.app (append o init_str_of_update #2) upds)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   372
         (fn append => List.app (append o init_str_of_update #3) upds)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   373
         (fn append => List.app (append o init_str_of_update #4) upds))
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   374
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   375
fun mash_ADD _ _ [] = ()
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   376
  | mash_ADD ctxt overlord upds =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   377
    (trace_msg ctxt (fn () => "MaSh ADD " ^
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   378
         elide_string 1000 (space_implode " " (map #1 upds)));
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   379
     run_mash_commands ctxt overlord true
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   380
         (fn append => List.app (append o str_of_update) upds) (K ()))
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   381
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   382
fun mash_QUERY ctxt overlord (query as (_, feats)) =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   383
  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   384
   run_mash_commands ctxt overlord false
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   385
       (fn append => append (str_of_query query))
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   386
       (fn preds => snd (extract_query (List.last (preds ()))))
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   387
   handle List.Empty => [])
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   388
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   389
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   390
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   391
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   392
type mash_state =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   393
  {thys : bool Symtab.table,
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   394
   fact_graph : unit Graph.T}
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   395
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   396
val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty}
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   397
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   398
local
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   399
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   400
fun mash_load (state as (true, _)) = state
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   401
  | mash_load _ =
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   402
    let val path = mash_state_path () in
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   403
      (true,
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   404
       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
   405
         SOME (comp_thys :: incomp_thys :: fact_lines) =>
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   406
         let
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   407
           fun add_thy comp thy = Symtab.update (thy, comp)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   408
           fun add_fact_line line =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   409
             case extract_query line of
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   410
               ("", _) => I (* shouldn't happen *)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   411
             | (name, parents) =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   412
               Graph.default_node (name, ())
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   413
               #> fold (fn par => Graph.add_edge (par, name)) parents
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   414
           val thys =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   415
             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
   416
                          |> fold (add_thy false) (unescape_metas incomp_thys)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   417
           val fact_graph = Graph.empty |> fold add_fact_line fact_lines
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   418
         in {thys = thys, fact_graph = fact_graph} end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   419
       | _ => empty_state)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   420
    end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   421
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   422
fun mash_save ({thys, fact_graph, ...} : mash_state) =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   423
  let
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   424
    val path = mash_state_path ()
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   425
    val thys = Symtab.dest thys
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   426
    fun line_for_thys comp = AList.find (op =) thys comp |> escape_metas
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   427
    fun fact_line_for name parents = name :: parents |> escape_metas
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   428
    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
   429
  in
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   430
    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
   431
    Graph.fold (fn (name, ((), (parents, _))) => fn () =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   432
                   append_fact name (Graph.Keys.dest parents))
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   433
        fact_graph ()
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   434
  end
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   435
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   436
val global_state =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   437
  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   438
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   439
in
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   440
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   441
fun mash_map f =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   442
  Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   443
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   444
fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   445
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   446
fun mash_reset ctxt =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   447
  Synchronized.change global_state (fn _ =>
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   448
      (mash_RESET ctxt; File.write (mash_state_path ()) "";
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   449
       (true, empty_state)))
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   450
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   451
end
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   452
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   453
fun mash_can_suggest_facts (_ : Proof.context) =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   454
  mash_home () <> "" andalso not (Graph.is_empty (#fact_graph (mash_get ())))
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   455
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   456
fun parents_wrt facts fact_graph =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   457
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   458
    val facts =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   459
      Symtab.empty
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   460
      |> fold (fn (_, th) => Symtab.update (Thm.get_name_hint th, ())) facts
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   461
  in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   462
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   463
fun mash_suggest_facts ctxt ({overlord, ...} : params) prover hyp_ts concl_t
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   464
                       facts =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   465
  let
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   466
    val thy = Proof_Context.theory_of ctxt
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   467
    val fact_graph = #fact_graph (mash_get ())
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   468
    val parents = parents_wrt facts fact_graph
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   469
    val feats = features_of thy General (concl_t :: hyp_ts)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   470
    val suggs = mash_QUERY ctxt overlord (parents, feats)
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   471
  in suggested_facts suggs facts end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   472
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   473
fun add_thys_for thy =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   474
  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
   475
    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
   476
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   477
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   478
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
   479
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   480
    fun maybe_add_from from (accum as (parents, graph)) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   481
      (from :: parents, Graph.add_edge_acyclic (from, name) graph)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   482
      handle Graph.CYCLES _ =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   483
             (trace_msg ctxt (fn () =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   484
                  "Cycle between " ^ quote from ^ " and " ^ quote name); accum)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   485
           | Graph.UNDEF _ =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   486
             (trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   487
    val graph = graph |> Graph.new_node (name, ())
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   488
    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
   489
    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
   490
  in ((name, parents, feats, deps) :: upds, graph) end
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   491
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   492
fun mash_learn_thy ctxt ({overlord, ...} : params) thy timeout =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   493
  let
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   494
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   495
    val facts = all_facts_of thy css_table
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   496
    val {fact_graph, ...} = mash_get ()
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   497
    fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   498
    val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   499
  in
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   500
    if null new_facts then
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   501
      ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   502
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   503
      let
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   504
        val ths = facts |> map snd
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   505
        val all_names =
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   506
          ths |> filter_out (is_likely_tautology orf is_too_meta)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   507
              |> map (rpair () o Thm.get_name_hint)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   508
              |> Symtab.make
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   509
        fun do_fact ((_, (_, status)), th) (parents, upds) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   510
          let
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   511
            val name = Thm.get_name_hint th
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   512
            val feats = features_of thy status [prop_of th]
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   513
            val deps = isabelle_dependencies_of all_names th
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   514
            val upd = (name, parents, feats, deps)
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   515
          in ([name], upd :: upds) end
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   516
        val parents = parents_wrt facts fact_graph
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   517
        val (_, upds) = (parents, []) |> fold do_fact new_facts ||> rev
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   518
        fun trans {thys, fact_graph} =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   519
          let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   520
            val mash_INIT_or_ADD =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   521
              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
   522
            val (upds, fact_graph) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   523
              ([], fact_graph) |> fold (update_fact_graph ctxt) upds
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   524
          in
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   525
            (mash_INIT_or_ADD ctxt overlord (rev upds);
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   526
             {thys = thys |> add_thys_for thy,
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   527
              fact_graph = fact_graph})
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   528
          end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   529
      in mash_map trans end
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   530
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   531
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   532
fun mash_learn_proof ctxt ({overlord, ...} : params) t used_ths facts =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   533
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   534
    val thy = Proof_Context.theory_of ctxt
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   535
    val name = ATP_Util.timestamp () (* should be fairly fresh *)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   536
    val feats = features_of thy General [t]
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   537
    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
   538
  in
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   539
    mash_map (fn {thys, fact_graph} =>
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   540
        let
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   541
          val parents = parents_wrt facts fact_graph
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   542
          val upds = [(name, parents, feats, deps)]
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   543
          val (upds, fact_graph) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   544
            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   545
        in
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   546
          mash_ADD ctxt overlord upds;
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   547
          {thys = thys, fact_graph = fact_graph}
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   548
        end)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   549
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   550
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   551
fun relevant_facts ctxt (params as {fact_filter, ...}) prover max_facts
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   552
        ({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
   553
  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
   554
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   555
  else if only then
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   556
    facts
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   557
  else if max_facts <= 0 then
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   558
    []
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   559
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   560
    let
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   561
      val fact_filter =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   562
        case fact_filter of
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   563
          SOME ff => ff
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   564
        | NONE => if mash_can_suggest_facts ctxt then meshN else iterN
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   565
      val add_ths = Attrib.eval_thms ctxt add
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   566
      fun prepend_facts ths accepts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   567
        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   568
         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   569
        |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   570
      fun iter () =
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   571
        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   572
                                 concl_t facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   573
        |> (fn facts => (facts, SOME (length facts)))
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   574
      fun mash () =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   575
        (facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t, NONE)
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   576
      val mess =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   577
        [] |> (if fact_filter <> mashN then cons (iter ()) else I)
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   578
           |> (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
   579
    in
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   580
      mesh_facts max_facts mess
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   581
      |> not (null add_ths) ? prepend_facts add_ths
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   582
    end
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   583
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
   584
end;