src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
author blanchet
Wed, 18 Jul 2012 08:44:04 +0200
changeset 48311 3c4e10606567
parent 48309 42c05a6c6c1e
child 48312 b40722a81ac9
permissions -rw-r--r--
implemented MaSh QUERY operation
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
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    18
  val escape_meta : string -> string
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    19
  val escape_metas : string list -> string
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    20
  val unescape_meta : string -> string
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    21
  val unescape_metas : string -> string list
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    22
  val extract_query : string -> string * string list
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    23
  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48298
diff changeset
    24
  val all_non_tautological_facts_of :
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48298
diff changeset
    25
    theory -> status Termtab.table -> fact list
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    26
  val theory_ord : theory * theory -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    27
  val thm_ord : thm * thm -> order
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    28
  val thy_facts_from_thms : ('a * thm) list -> string list Symtab.table
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    29
  val has_thy : theory -> thm -> bool
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    30
  val parent_facts : theory -> string list Symtab.table -> string list
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
    31
  val features_of : theory -> status -> term list -> string list
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    32
  val isabelle_dependencies_of : string list -> thm -> string list
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    33
  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
    34
  val run_prover : Proof.context -> params -> fact list -> thm -> prover_result
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
    35
  val thy_name_of_fact : string -> string
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    36
  val mash_RESET : Proof.context -> unit
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    37
  val mash_ADD :
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    38
    Proof.context -> (string * string list * string list * string list) list
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    39
    -> unit
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    40
  val mash_DEL : Proof.context -> string list -> string list -> unit
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    41
  val mash_QUERY : Proof.context -> string list * string list -> string list
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    42
  val mash_reset : Proof.context -> unit
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    43
  val mash_can_suggest_facts : Proof.context -> bool
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
    44
  val mash_suggest_facts :
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    45
    Proof.context -> params -> string -> term list -> term -> fact list
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    46
    -> fact list
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    47
  val mash_can_learn_thy : Proof.context -> theory -> bool
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    48
  val mash_learn_thy : Proof.context -> theory -> real -> unit
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
    49
  val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
    50
  val relevant_facts :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    51
    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
    52
    -> term -> fact list -> fact list
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    53
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    54
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    55
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    56
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
    57
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    58
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    59
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    60
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    61
open Sledgehammer_Fact
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    62
open Sledgehammer_Filter_Iter
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    63
open Sledgehammer_Provers
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    64
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    65
val trace =
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    66
  Attrib.setup_config_bool @{binding sledgehammer_filter_mash_trace} (K false)
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    67
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    68
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
    69
fun mash_dir () =
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
    70
  getenv "ISABELLE_HOME_USER" ^ "/mash"
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
    71
  |> tap (fn dir => Isabelle_System.mkdir (Path.explode dir))
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
    72
fun mash_state_path () = mash_dir () ^ "/state" |> Path.explode
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    73
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    74
(*** Isabelle helpers ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    75
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    76
fun meta_char c =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    77
  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
    78
     c = #")" orelse c = #"," then
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    79
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    80
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    81
    (* fixed width, in case more digits follow *)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    82
    "\\" ^ stringN_of_int 3 (Char.ord c)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    83
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    84
fun unmeta_chars accum [] = String.implode (rev accum)
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    85
  | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    86
    (case Int.fromString (String.implode [d1, d2, d3]) of
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    87
       SOME n => unmeta_chars (Char.chr n :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    88
     | NONE => "" (* error *))
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    89
  | unmeta_chars _ (#"\\" :: _) = "" (* error *)
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    90
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    91
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    92
val escape_meta = String.translate meta_char
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    93
val escape_metas = map escape_meta #> space_implode " "
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    94
val unescape_meta = unmeta_chars [] o String.explode
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    95
val unescape_metas = map unescape_meta o space_explode " "
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    96
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    97
val explode_suggs =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    98
  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    99
fun extract_query line =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   100
  case space_explode ":" line of
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   101
    [goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   102
  | _ => ("", explode_suggs line)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   103
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   104
fun find_suggested facts sugg =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   105
  find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   106
fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   107
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   108
val thy_feature_prefix = "y_"
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   109
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   110
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
   111
val const_name_of = prefix const_prefix
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   112
val type_name_of = prefix type_const_prefix
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   113
val class_name_of = prefix class_prefix
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   114
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   115
local
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   116
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   117
fun has_bool @{typ bool} = true
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   118
  | has_bool (Type (_, Ts)) = exists has_bool Ts
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   119
  | has_bool _ = false
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   120
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   121
fun has_fun (Type (@{type_name fun}, _)) = true
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   122
  | has_fun (Type (_, Ts)) = exists has_fun Ts
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   123
  | has_fun _ = false
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   124
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   125
val is_conn = member (op =)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   126
  [@{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
   127
   @{const_name HOL.implies}, @{const_name Not},
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   128
   @{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
   129
   @{const_name HOL.eq}]
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   130
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   131
val has_bool_arg_const =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   132
  exists_Const (fn (c, T) =>
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   133
                   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
   134
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   135
fun higher_inst_const thy (c, T) =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   136
  case binder_types T of
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   137
    [] => false
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   138
  | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   139
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   140
val binders = [@{const_name All}, @{const_name Ex}]
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   141
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   142
in
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
fun is_fo_term thy t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   145
  let
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   146
    val t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   147
      t |> Envir.beta_eta_contract
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   148
        |> transform_elim_prop
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   149
        |> Object_Logic.atomize_term thy
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   150
  in
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   151
    Term.is_first_order binders t andalso
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   152
    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
   153
                          | _ => false) t orelse
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   154
         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
   155
  end
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   156
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   157
end
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   158
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   159
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
   160
  let
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   161
    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
   162
    val bad_consts = atp_widely_irrelevant_consts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   163
    fun add_classes @{sort type} = I
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   164
      | 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
   165
    fun do_add_type (Type (s, Ts)) =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   166
        (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
   167
        #> fold do_add_type Ts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   168
      | do_add_type (TFree (_, S)) = add_classes S
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   169
      | do_add_type (TVar (_, S)) = add_classes S
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   170
    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
   171
    fun mk_app s args =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   172
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   173
      else s
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   174
    fun patternify ~1 _ = ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   175
      | patternify depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   176
        case strip_comb t of
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   177
          (Const (s, _), args) =>
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   178
          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
   179
        | _ => ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   180
    fun add_term_patterns ~1 _ = I
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   181
      | add_term_patterns depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   182
        insert (op =) (patternify depth t)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   183
        #> add_term_patterns (depth - 1) t
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   184
    val add_term = add_term_patterns term_max_depth
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   185
    fun add_patterns t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   186
      let val (head, args) = strip_comb t in
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   187
        (case head of
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   188
           Const (s, T) =>
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   189
           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
   190
         | Free (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   191
         | Var (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   192
         | Abs (_, T, body) => add_type T #> add_patterns body
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   193
         | _ => I)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   194
        #> fold add_patterns args
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   195
      end
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   196
  in [] |> fold add_patterns ts |> sort string_ord end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   197
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   198
fun is_likely_tautology th =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   199
  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
   200
  not (Thm.eq_thm_prop (@{thm ext}, th))
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   201
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   202
fun is_too_meta thy th =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   203
  fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   204
48299
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48298
diff changeset
   205
fun all_non_tautological_facts_of thy css_table =
5e5c6616f0fe centrally construct expensive data structures
blanchet
parents: 48298
diff changeset
   206
  all_facts_of thy css_table
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   207
  |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   208
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   209
fun theory_ord p =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   210
  if Theory.eq_thy p then EQUAL
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   211
  else if Theory.subthy p then LESS
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   212
  else if Theory.subthy (swap p) then GREATER
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   213
  else EQUAL
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   214
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   215
val thm_ord = theory_ord o pairself theory_of_thm
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   216
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   217
(* ### FIXME: optimize *)
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   218
fun thy_facts_from_thms ths =
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   219
  ths |> map (snd #> `(theory_of_thm #> Context.theory_name))
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   220
      |> AList.group (op =)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   221
      |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   222
                                   o hd o snd))
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   223
      |> map (apsnd (sort (rev_order o thm_ord) #> map Thm.get_name_hint))
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   224
      |> Symtab.make
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   225
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   226
fun has_thy thy th =
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   227
  Context.theory_name thy = Context.theory_name (theory_of_thm th)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   228
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   229
fun parent_facts thy thy_facts =
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   230
  let
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   231
    fun add_last thy =
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   232
      case Symtab.lookup thy_facts (Context.theory_name thy) of
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   233
        SOME (last_fact :: _) => insert (op =) last_fact
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   234
      | _ => add_parent thy
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   235
    and add_parent thy = fold add_last (Theory.parents_of thy)
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   236
  in add_parent thy [] end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   237
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   238
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
   239
48297
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   240
val term_max_depth = 1
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   241
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   242
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   243
(* TODO: Generate type classes for types? *)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   244
fun features_of thy status ts =
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   245
  thy_feature_name_of (Context.theory_name thy) ::
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   246
  interesting_terms_types_and_classes term_max_depth type_max_depth ts
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   247
  |> exists (not o is_lambda_free) ts ? cons "lambdas"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   248
  |> exists (exists_Const is_exists) ts ? cons "skolems"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   249
  |> exists (not o is_fo_term thy) ts ? cons "ho"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   250
  |> (case status of
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   251
        General => I
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   252
      | Induction => cons "induction"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   253
      | Intro => cons "intro"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   254
      | Inductive => cons "inductive"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   255
      | Elim => cons "elim"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   256
      | Simp => cons "simp"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   257
      | Def => cons "def")
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   258
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   259
fun isabelle_dependencies_of all_facts =
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   260
  thms_in_proof (SOME all_facts) #> sort string_ord
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   261
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   262
val freezeT = Type.legacy_freeze_type
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   263
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   264
fun freeze (t $ u) = freeze t $ freeze u
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   265
  | 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
   266
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   267
  | freeze (Const (s, T)) = Const (s, freezeT T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   268
  | freeze (Free (s, T)) = Free (s, freezeT T)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   269
  | freeze t = t
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 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
   272
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   273
fun run_prover ctxt (params as {provers, ...}) facts goal =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   274
  let
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   275
    val problem =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   276
      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   277
       facts = facts |> map (apfst (apfst (fn name => name ())))
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   278
                     |> map Sledgehammer_Provers.Untranslated_Fact}
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   279
    val prover =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   280
      Sledgehammer_Minimize.get_minimizing_prover ctxt
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   281
          Sledgehammer_Provers.Normal (hd provers)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   282
  in prover params (K (K (K ""))) problem end
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   283
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   284
fun accessibility_of thy thy_facts =
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   285
  case Symtab.lookup thy_facts (Context.theory_name thy) of
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   286
    SOME (fact :: _) => [fact]
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   287
  | _ => parent_facts thy thy_facts
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   288
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   289
val thy_name_of_fact = hd o Long_Name.explode
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   290
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   291
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   292
(*** Low-level communication with MaSh ***)
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   293
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   294
fun run_mash ctxt save write_cmds read_preds =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   295
  let
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   296
    val temp_dir = getenv "ISABELLE_TMP"
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   297
    val serial = serial_string ()
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   298
    val cmd_file = temp_dir ^ "/mash_commands." ^ serial
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   299
    val cmd_path = Path.explode cmd_file
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   300
    val pred_file = temp_dir ^ "/mash_preds." ^ serial
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   301
    val log_file = temp_dir ^ "/mash_log." ^ serial
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   302
    val command =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   303
      getenv "MASH_HOME" ^ "/mash.py --inputFile " ^ cmd_file ^
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   304
      " --outputDir " ^ mash_dir () ^ " --predictions " ^ pred_file ^
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   305
      " --log " ^ log_file ^ (if save then " --saveModel" else "") ^
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   306
      " > /dev/null"
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   307
    val _ = File.write cmd_path ""
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   308
    val _ = write_cmds (File.append cmd_path)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   309
    val _ = trace_msg ctxt (fn () => "  running " ^ command)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   310
    val _ = Isabelle_System.bash command
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   311
  in read_preds (fn () => File.read_lines (Path.explode pred_file)) end
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   312
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   313
fun str_of_update (fact, access, feats, deps) =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   314
  "! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   315
  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   316
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   317
fun str_of_query (access, feats) =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   318
  "? " ^ escape_metas access ^ "; " ^ escape_metas feats
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   319
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   320
fun mash_RESET ctxt =
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   321
  let val path = mash_dir () |> Path.explode in
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   322
    trace_msg ctxt (K "MaSh RESET");
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   323
    File.fold_dir (fn file => fn () =>
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   324
                      File.rm (Path.append path (Path.basic file)))
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   325
                  path ()
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   326
  end
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   327
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   328
fun mash_ADD _ [] = ()
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   329
  | mash_ADD ctxt upds =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   330
    (trace_msg ctxt (fn () => "MaSh ADD " ^ space_implode " " (map #1 upds));
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   331
     run_mash ctxt true (fn append => List.app (append o str_of_update) upds)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   332
              (K ()))
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   333
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   334
fun mash_DEL ctxt facts feats =
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   335
  trace_msg ctxt (fn () =>
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   336
      "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   337
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   338
fun mash_QUERY ctxt (query as (_, feats)) =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   339
  (trace_msg ctxt (fn () => "MaSh SUGGEST " ^ space_implode " " feats);
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   340
   run_mash ctxt false (fn append => append (str_of_query query))
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   341
                 (fn preds => snd (extract_query (List.last (preds ()))))
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   342
   handle List.Empty => [])
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   343
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   344
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   345
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   346
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   347
type mash_state =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   348
  {dirty_thys : unit Symtab.table,
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   349
   thy_facts : string list Symtab.table}
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   350
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   351
val empty_state =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   352
  {dirty_thys = Symtab.empty,
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   353
   thy_facts = Symtab.empty}
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   354
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   355
local
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   356
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   357
fun mash_load (state as (true, _)) = state
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   358
  | mash_load _ =
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   359
    let val path = mash_state_path () in
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   360
      (true,
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   361
       case try File.read_lines path of
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   362
         SOME (dirty_line :: facts_lines) =>
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   363
         let
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   364
           fun dirty_thys_of_line line =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   365
             Symtab.make (line |> unescape_metas |> map (rpair ()))
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   366
           fun add_facts_line line =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   367
             case unescape_metas line of
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   368
               thy :: facts => Symtab.update_new (thy, facts)
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   369
             | _ => I (* shouldn't happen *)
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   370
         in
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   371
           {dirty_thys = dirty_thys_of_line dirty_line,
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   372
            thy_facts = fold add_facts_line facts_lines Symtab.empty}
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   373
         end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   374
       | _ => empty_state)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   375
    end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   376
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   377
fun mash_save ({dirty_thys, thy_facts} : mash_state) =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   378
  let
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   379
    val path = mash_state_path ()
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   380
    val dirty_line = (escape_metas (Symtab.keys dirty_thys)) ^ "\n"
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   381
    fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n"
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   382
  in
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   383
    File.write path dirty_line;
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   384
    Symtab.fold (fn thy_fact => fn () =>
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   385
                    File.append path (fact_line_for thy_fact)) thy_facts ()
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   386
  end
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   387
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   388
val global_state =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   389
  Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   390
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   391
in
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   392
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   393
fun mash_map f =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   394
  Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   395
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   396
fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   397
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   398
fun mash_reset ctxt =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   399
  Synchronized.change global_state (fn _ =>
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   400
      (mash_RESET ctxt; File.write (mash_state_path ()) "";
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   401
       (true, empty_state)))
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   402
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   403
end
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   404
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   405
fun mash_can_suggest_facts (_ : Proof.context) =
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   406
  not (Symtab.is_empty (#thy_facts (mash_get ())))
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   407
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   408
fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   409
  let
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   410
    val thy = Proof_Context.theory_of ctxt
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   411
    val thy_facts = #thy_facts (mash_get ())
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   412
    val access = accessibility_of thy thy_facts
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   413
    val feats = features_of thy General (concl_t :: hyp_ts)
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   414
    val suggs = mash_QUERY ctxt (access, feats)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   415
  in suggested_facts suggs facts end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   416
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   417
fun mash_can_learn_thy (_ : Proof.context) thy =
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   418
  not (Symtab.defined (#dirty_thys (mash_get ())) (Context.theory_name thy))
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   419
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   420
fun is_fact_in_thy_facts thy_facts fact =
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   421
  case Symtab.lookup thy_facts (thy_name_of_fact fact) of
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   422
    SOME facts => member (op =) facts fact
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   423
  | NONE => false
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   424
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   425
fun zip_facts news [] = news
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   426
  | zip_facts [] olds = olds
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   427
  | zip_facts (new :: news) (old :: olds) =
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   428
    if new = old then
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   429
      new :: zip_facts news olds
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   430
    else if member (op =) news old then
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   431
      old :: zip_facts (filter_out (curry (op =) old) news) olds
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   432
    else if member (op =) olds new then
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   433
      new :: zip_facts news (filter_out (curry (op =) new) olds)
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   434
    else
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   435
      new :: old :: zip_facts news olds
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   436
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   437
fun add_thy_facts_from_thys new old =
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   438
  let
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   439
    fun add_thy (thy, new_facts) =
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   440
      case Symtab.lookup old thy of
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   441
        SOME old_facts => Symtab.update (thy, zip_facts old_facts new_facts)
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   442
      | NONE => Symtab.update_new (thy, new_facts)
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   443
  in old |> Symtab.fold add_thy new end
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   444
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   445
fun mash_learn_thy ctxt thy timeout =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   446
  let
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   447
    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   448
    val facts = all_non_tautological_facts_of thy css_table
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   449
    val {thy_facts, ...} = mash_get ()
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   450
    fun is_old (_, th) = is_fact_in_thy_facts thy_facts (Thm.get_name_hint th)
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   451
    val (old_facts, new_facts) =
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   452
      facts |> List.partition is_old ||> sort (thm_ord o pairself snd)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   453
  in
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   454
    if null new_facts then
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   455
      ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   456
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   457
      let
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   458
        val ths = facts |> map snd
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   459
        val all_names = ths |> map Thm.get_name_hint
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   460
        fun do_fact ((_, (_, status)), th) (prevs, upds) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   461
          let
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   462
            val name = Thm.get_name_hint th
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   463
            val feats = features_of thy status [prop_of th]
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   464
            val deps = isabelle_dependencies_of all_names th
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   465
            val upd = (name, prevs, feats, deps)
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   466
          in ([name], upd :: upds) end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   467
        val parents = parent_facts thy thy_facts
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   468
        val (_, upds) = (parents, []) |> fold do_fact new_facts
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   469
        val new_thy_facts = new_facts |> thy_facts_from_thms
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   470
        fun trans {dirty_thys, thy_facts} =
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   471
          (mash_ADD ctxt (rev upds);
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   472
           {dirty_thys = dirty_thys,
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   473
            thy_facts = thy_facts |> add_thy_facts_from_thys new_thy_facts})
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   474
      in mash_map trans end
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   475
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   476
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   477
fun mash_learn_proof ctxt thy t ths =
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   478
  mash_map (fn state as {dirty_thys, thy_facts} =>
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   479
    let val deps = ths |> map Thm.get_name_hint in
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   480
      if forall (is_fact_in_thy_facts thy_facts) deps then
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   481
        let
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   482
          val fact = ATP_Util.timestamp () (* should be fairly fresh *)
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   483
          val access = accessibility_of thy thy_facts
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   484
          val feats = features_of thy General [t]
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   485
        in
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   486
          mash_ADD ctxt [(fact, access, feats, deps)];
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   487
          {dirty_thys = dirty_thys, thy_facts = thy_facts}
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   488
        end
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   489
      else
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   490
        state
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   491
    end)
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   492
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   493
fun relevant_facts ctxt params prover max_facts
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   494
        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   495
  if only then
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   496
    facts
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   497
  else if max_facts <= 0 then
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   498
    []
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   499
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   500
    let
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   501
      val add_ths = Attrib.eval_thms ctxt add
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   502
      fun prepend_facts ths accepts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   503
        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   504
         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   505
        |> take max_facts
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   506
      val iter_facts =
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   507
        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   508
                                 concl_t facts
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   509
      val (mash_facts, mash_antifacts) =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   510
        facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   511
              |> chop max_facts
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   512
      val mesh_facts = iter_facts (* ### *)
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   513
    in
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   514
      mesh_facts
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   515
      |> not (null add_ths) ? prepend_facts add_ths
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   516
    end
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   517
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
   518
end;