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