src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Fri, 20 Jul 2012 22:19:46 +0200
changeset 48398 b86450f5b5cb
parent 48396 dd82d190c2af
child 48399 4bacc8983b3d
permissions -rw-r--r--
clean up interesting constants a bit
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48380
d4b7c7be3116 renamed ML files
blanchet
parents: 48379
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_mash.ML
48248
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
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
     7
signature SLEDGEHAMMER_MASH =
48248
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 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
    10
  type fact = Sledgehammer_Fact.fact
e7f01b7e244e gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents: 48293
diff changeset
    11
  type fact_override = Sledgehammer_Fact.fact_override
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    12
  type params = Sledgehammer_Provers.params
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
    13
  type relevance_fudge = Sledgehammer_Provers.relevance_fudge
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    14
  type prover_result = Sledgehammer_Provers.prover_result
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    15
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    16
  val trace : bool Config.T
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    17
  val MaShN : string
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    18
  val mepoN : string
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    19
  val mashN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    20
  val meshN : string
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    21
  val unlearnN : string
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    22
  val learn_isarN : string
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    23
  val learn_atpN : string
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    24
  val relearn_isarN : string
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    25
  val relearn_atpN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    26
  val fact_filters : string list
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    27
  val escape_meta : string -> string
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
    28
  val escape_metas : string list -> string
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    29
  val unescape_meta : string -> string
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    30
  val unescape_metas : string -> string list
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
    31
  val extract_query : string -> string * string list
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
    32
  val nickname_of : thm -> string
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    33
  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    34
  val mesh_facts :
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    35
    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
    36
  val is_likely_tautology_or_too_meta : thm -> bool
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    37
  val theory_ord : theory * theory -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    38
  val thm_ord : thm * thm -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    39
  val goal_of_thm : theory -> thm -> thm
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    40
  val run_prover_for_mash :
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    41
    Proof.context -> params -> string -> fact list -> thm -> prover_result
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    42
  val features_of :
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    43
    Proof.context -> string -> theory -> stature -> term list -> string list
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    44
  val isar_dependencies_of : unit Symtab.table -> thm -> string list
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    45
  val atp_dependencies_of :
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    46
    Proof.context -> params -> string -> bool -> fact list -> unit Symtab.table
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    47
    -> thm -> string list
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
    48
  val mash_CLEAR : Proof.context -> unit
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    49
  val mash_ADD :
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    50
    Proof.context -> bool
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    51
    -> (string * string list * string list * string list) list -> unit
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
    52
  val mash_QUERY :
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    53
    Proof.context -> bool -> int -> string list * string list -> string list
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
    54
  val mash_unlearn : Proof.context -> unit
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    55
  val mash_could_suggest_facts : unit -> bool
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    56
  val mash_can_suggest_facts : Proof.context -> bool
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
    57
  val mash_suggest_facts :
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    58
    Proof.context -> params -> string -> int -> term list -> term
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    59
    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
    60
  val mash_learn_proof :
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
    61
    Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
    62
    -> unit
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
    63
  val mash_learn_facts :
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    64
    Proof.context -> params -> string -> bool -> bool -> Time.time -> fact list
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    65
    -> string
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    66
  val mash_learn :
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    67
    Proof.context -> params -> fact_override -> thm list -> bool -> unit
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
    68
  val relevant_facts :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    69
    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
    70
    -> term -> fact list -> fact list
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    71
  val kill_learners : unit -> unit
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    72
  val running_learners : unit -> unit
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    73
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    74
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    75
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    76
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
    77
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    78
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    79
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    80
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    81
open Sledgehammer_Fact
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    82
open Sledgehammer_Provers
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    83
open Sledgehammer_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    84
open Sledgehammer_MePo
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    85
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    86
val trace =
48380
d4b7c7be3116 renamed ML files
blanchet
parents: 48379
diff changeset
    87
  Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    88
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    89
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    90
val MaShN = "MaSh"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    91
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    92
val mepoN = "mepo"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    93
val mashN = "mash"
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    94
val meshN = "mesh"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    95
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    96
val fact_filters = [meshN, mepoN, mashN]
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    97
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    98
val unlearnN = "unlearn"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    99
val learn_isarN = "learn_isar"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   100
val learn_atpN = "learn_atp"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   101
val relearn_isarN = "relearn_isar"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   102
val relearn_atpN = "relearn_atp"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   103
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   104
fun mash_home () = getenv "MASH_HOME"
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   105
fun mash_model_dir () =
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   106
  getenv "ISABELLE_HOME_USER" ^ "/mash"
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   107
  |> tap (Isabelle_System.mkdir o Path.explode)
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   108
val mash_state_dir = mash_model_dir
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   109
fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   110
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   111
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   112
(*** Isabelle helpers ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   113
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   114
fun meta_char c =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   115
  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
   116
     c = #")" orelse c = #"," then
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   117
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   118
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   119
    (* fixed width, in case more digits follow *)
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   120
    "%" ^ stringN_of_int 3 (Char.ord c)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   121
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   122
fun unmeta_chars accum [] = String.implode (rev accum)
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   123
  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   124
    (case Int.fromString (String.implode [d1, d2, d3]) of
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   125
       SOME n => unmeta_chars (Char.chr n :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   126
     | NONE => "" (* error *))
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   127
  | unmeta_chars _ (#"%" :: _) = "" (* error *)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   128
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   129
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   130
val escape_meta = String.translate meta_char
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   131
val escape_metas = map escape_meta #> space_implode " "
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   132
val unescape_meta = String.explode #> unmeta_chars []
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   133
val unescape_metas =
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   134
  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   135
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   136
fun extract_query line =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   137
  case space_explode ":" line of
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   138
    [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   139
  | _ => ("", [])
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   140
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   141
fun parent_of_local_thm th =
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   142
  let
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   143
    val thy = th |> Thm.theory_of_thm
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   144
    val facts = thy |> Global_Theory.facts_of
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   145
    val space = facts |> Facts.space_of
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   146
    fun id_of s = #id (Name_Space.the_entry space s)
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   147
    fun max_id (s', _) (s, id) =
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   148
      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   149
  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   150
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   151
val local_prefix = "local" ^ Long_Name.separator
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   152
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   153
fun nickname_of th =
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   154
  if Thm.has_name_hint th then
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   155
    let val hint = Thm.get_name_hint th in
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   156
      (* FIXME: There must be a better way to detect local facts. *)
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   157
      case try (unprefix local_prefix) hint of
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   158
        SOME suf =>
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   159
        parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   160
      | NONE => hint
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   161
    end
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   162
  else
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   163
    backquote_thm th
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   164
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   165
fun suggested_facts suggs facts =
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   166
  let
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   167
    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   168
    val tab = Symtab.empty |> fold add_fact facts
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   169
  in map_filter (Symtab.lookup tab) suggs end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   170
48329
5781c4620245 use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents: 48328
diff changeset
   171
(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
5781c4620245 use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents: 48328
diff changeset
   172
fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
48328
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   173
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   174
fun sum_sq_avg [] = 0
48329
5781c4620245 use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents: 48328
diff changeset
   175
  | sum_sq_avg xs =
5781c4620245 use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents: 48328
diff changeset
   176
    Real.ceil (100000.0 * fold (curry (op +) o score) xs 0.0) div length xs
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   177
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   178
fun mesh_facts max_facts [(selected, unknown)] =
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   179
    take max_facts selected @ take (max_facts - length selected) unknown
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   180
  | mesh_facts max_facts mess =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   181
    let
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   182
      val mess = mess |> map (apfst (`length))
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   183
      val fact_eq = Thm.eq_thm o pairself snd
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   184
      fun score_in fact ((sel_len, sels), unks) =
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   185
        case find_index (curry fact_eq fact) sels of
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   186
          ~1 => (case find_index (curry fact_eq fact) unks of
48329
5781c4620245 use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents: 48328
diff changeset
   187
                   ~1 => SOME sel_len
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   188
                 | _ => NONE)
48329
5781c4620245 use better score function, based on previous evaluation (cf. Deduct 2011 slides)
blanchet
parents: 48328
diff changeset
   189
        | j => SOME j
48328
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   190
      fun score_of fact = mess |> map_filter (score_in fact) |> sum_sq_avg
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   191
      val facts = fold (union fact_eq o take max_facts o snd o fst) mess []
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   192
    in
48328
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   193
      facts |> map (`score_of) |> sort (int_ord o swap o pairself fst)
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   194
            |> map snd |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   195
    end
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   196
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   197
val thy_feature_name_of = prefix "y"
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   198
val const_name_of = prefix "c"
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   199
val type_name_of = prefix "t"
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   200
val class_name_of = prefix "s"
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   201
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   202
fun is_likely_tautology_or_too_meta th =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   203
  let
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   204
    val is_boring_const = member (op =) atp_widely_irrelevant_consts
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   205
    fun is_boring_bool t =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   206
      not (exists_Const (not o is_boring_const o fst) t) orelse
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   207
      exists_type (exists_subtype (curry (op =) @{typ prop})) t
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   208
    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   209
      | is_boring_prop (@{const "==>"} $ t $ u) =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   210
        is_boring_prop t andalso is_boring_prop u
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   211
      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   212
        is_boring_prop t andalso is_boring_prop u
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   213
      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   214
        is_boring_bool t andalso is_boring_bool u
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   215
      | is_boring_prop _ = true
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   216
  in
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   217
    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   218
  end
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   219
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   220
fun theory_ord p =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   221
  if Theory.eq_thy p then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   222
    EQUAL
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   223
  else if Theory.subthy p then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   224
    LESS
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   225
  else if Theory.subthy (swap p) then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   226
    GREATER
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   227
  else case int_ord (pairself (length o Theory.ancestors_of) p) of
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   228
    EQUAL => string_ord (pairself Context.theory_name p)
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   229
  | order => order
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   230
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   231
val thm_ord = theory_ord o pairself theory_of_thm
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   232
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   233
val freezeT = Type.legacy_freeze_type
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   234
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   235
fun freeze (t $ u) = freeze t $ freeze u
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   236
  | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   237
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   238
  | freeze (Const (s, T)) = Const (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   239
  | freeze (Free (s, T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   240
  | freeze t = t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   241
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   242
fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   243
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   244
fun run_prover_for_mash ctxt params prover facts goal =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   245
  let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   246
    val problem =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   247
      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   248
       facts = facts |> map (apfst (apfst (fn name => name ())))
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   249
                     |> map Untranslated_Fact}
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   250
  in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   251
    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K "")))
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   252
                          problem
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   253
  end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   254
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   255
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   256
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   257
val logical_consts =
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   258
  [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   259
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   260
fun interesting_terms_types_and_classes ctxt prover term_max_depth
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   261
                                        type_max_depth ts =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   262
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   263
    fun is_bad_const (x as (s, _)) args =
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   264
      member (op =) logical_consts s orelse
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   265
      fst (is_built_in_const_for_prover ctxt prover x args)
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   266
    fun add_classes @{sort type} = I
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   267
      | 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
   268
    fun do_add_type (Type (s, Ts)) =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   269
        (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
   270
        #> fold do_add_type Ts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   271
      | do_add_type (TFree (_, S)) = add_classes S
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   272
      | do_add_type (TVar (_, S)) = add_classes S
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   273
    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
   274
    fun mk_app s args =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   275
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   276
      else s
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   277
    fun patternify ~1 _ = ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   278
      | patternify depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   279
        case strip_comb t of
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   280
          (Const (x as (s, _)), args) =>
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   281
          if is_bad_const x args then ""
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   282
          else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   283
        | _ => ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   284
    fun add_term_patterns ~1 _ = I
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   285
      | add_term_patterns depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   286
        insert (op =) (patternify depth t)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   287
        #> add_term_patterns (depth - 1) t
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   288
    val add_term = add_term_patterns term_max_depth
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   289
    fun add_patterns t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   290
      let val (head, args) = strip_comb t in
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   291
        (case head of
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   292
           Const (_, T) => add_term t #> add_type T
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   293
         | Free (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   294
         | Var (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   295
         | Abs (_, T, body) => add_type T #> add_patterns body
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   296
         | _ => I)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   297
        #> fold add_patterns args
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   298
      end
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   299
  in [] |> fold add_patterns ts end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   300
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   301
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
   302
48297
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   303
val term_max_depth = 1
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   304
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   305
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   306
(* TODO: Generate type classes for types? *)
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   307
fun features_of ctxt prover thy (scope, status) ts =
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   308
  thy_feature_name_of (Context.theory_name thy) ::
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   309
  interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   310
                                      ts
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   311
  |> forall is_lambda_free ts ? cons "no_lams"
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   312
  |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   313
  |> scope <> Global ? cons "local"
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   314
  |> (case status of
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   315
        General => I
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   316
      | Induction => cons "induction"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   317
      | Intro => cons "intro"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   318
      | Inductive => cons "inductive"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   319
      | Elim => cons "elim"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   320
      | Simp => cons "simp"
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   321
      | Def => cons "def")
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   322
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   323
fun isar_dependencies_of all_facts = thms_in_proof (SOME all_facts)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   324
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   325
val atp_dep_default_max_fact = 50
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   326
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   327
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   328
                        facts all_names th =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   329
  case isar_dependencies_of all_names th of
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   330
    [] => []
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   331
  | isar_deps =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   332
    let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   333
      val thy = Proof_Context.theory_of ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   334
      val goal = goal_of_thm thy th
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   335
      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   336
      val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   337
      fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   338
      fun is_dep dep (_, th) = nickname_of th = dep
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   339
      fun add_isar_dep facts dep accum =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   340
        if exists (is_dep dep) accum then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   341
          accum
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   342
        else case find_first (is_dep dep) facts of
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   343
          SOME ((name, status), th) => accum @ [((name, status), th)]
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   344
        | NONE => accum (* shouldn't happen *)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   345
      val facts =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   346
        facts |> iterative_relevant_facts ctxt params prover
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   347
                     (max_facts |> the_default atp_dep_default_max_fact) NONE
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   348
                     hyp_ts concl_t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   349
              |> fold (add_isar_dep facts) isar_deps
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   350
              |> map fix_name
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   351
    in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   352
      if verbose andalso not auto then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   353
        let val num_facts = length facts in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   354
          "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   355
          " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   356
          "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   357
          |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   358
        end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   359
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   360
        ();
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   361
      case run_prover_for_mash ctxt params prover facts goal of
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   362
        {outcome = NONE, used_facts, ...} =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   363
        (if verbose andalso not auto then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   364
           let val num_facts = length used_facts in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   365
             "Found proof with " ^ string_of_int num_facts ^ " fact" ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   366
             plural_s num_facts ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   367
             |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   368
           end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   369
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   370
           ();
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   371
         used_facts |> map fst)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   372
      | _ => isar_deps
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   373
    end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   374
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   375
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   376
(*** Low-level communication with MaSh ***)
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   377
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   378
(* more friendly than "try o File.rm" for those who keep the files open in their
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   379
   text editor *)
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   380
fun wipe_out file = File.write file ""
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   381
48323
7b5f7ca25d17 optimized MaSh output by chunking it
blanchet
parents: 48322
diff changeset
   382
fun write_file (xs, f) file =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   383
  let val path = Path.explode file in
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   384
    wipe_out path;
48323
7b5f7ca25d17 optimized MaSh output by chunking it
blanchet
parents: 48322
diff changeset
   385
    xs |> chunk_list 500
7b5f7ca25d17 optimized MaSh output by chunking it
blanchet
parents: 48322
diff changeset
   386
       |> List.app (File.append path o space_implode "" o map f)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   387
  end
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   388
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   389
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   390
  let
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   391
    val (temp_dir, serial) =
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   392
      if overlord then (getenv "ISABELLE_HOME_USER", "")
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   393
      else (getenv "ISABELLE_TMP", serial_string ())
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   394
    val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   395
    val err_file = temp_dir ^ "/mash_err" ^ serial
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   396
    val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   397
    val cmd_file = temp_dir ^ "/mash_commands" ^ serial
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   398
    val core =
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   399
      "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   400
      " --numberOfPredictions " ^ string_of_int max_suggs ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   401
      (if save then " --saveModel" else "")
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   402
    val command =
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   403
      mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   404
      " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   405
  in
48323
7b5f7ca25d17 optimized MaSh output by chunking it
blanchet
parents: 48322
diff changeset
   406
    write_file ([], K "") sugg_file;
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   407
    write_file write_cmds cmd_file;
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   408
    trace_msg ctxt (fn () => "Running " ^ command);
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   409
    Isabelle_System.bash command;
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   410
    read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   411
    |> tap (fn _ => trace_msg ctxt (fn () =>
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   412
           case try File.read (Path.explode err_file) of
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   413
             NONE => "Done"
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   414
           | SOME "" => "Done"
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   415
           | SOME s => "Error: " ^ elide_string 1000 s))
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   416
    |> not overlord
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   417
       ? tap (fn _ => List.app (wipe_out o Path.explode)
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   418
                               [err_file, sugg_file, cmd_file])
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   419
  end
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   420
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   421
fun str_of_update (name, parents, feats, deps) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   422
  "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   423
  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   424
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   425
fun str_of_query (parents, feats) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   426
  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   427
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   428
fun mash_CLEAR ctxt =
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   429
  let val path = mash_model_dir () |> Path.explode in
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   430
    trace_msg ctxt (K "MaSh CLEAR");
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   431
    File.fold_dir (fn file => fn _ =>
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   432
                      try File.rm (Path.append path (Path.basic file)))
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   433
                  path NONE;
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   434
    ()
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   435
  end
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   436
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   437
fun mash_ADD _ _ [] = ()
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   438
  | mash_ADD ctxt overlord upds =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   439
    (trace_msg ctxt (fn () => "MaSh ADD " ^
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   440
         elide_string 1000 (space_implode " " (map #1 upds)));
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   441
     run_mash_tool ctxt overlord true 0 (upds, str_of_update) (K ()))
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   442
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   443
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   444
  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   445
   run_mash_tool ctxt overlord false max_suggs
48323
7b5f7ca25d17 optimized MaSh output by chunking it
blanchet
parents: 48322
diff changeset
   446
       ([query], str_of_query)
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   447
       (fn suggs =>
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   448
           case suggs () of
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   449
             [] => []
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   450
           | suggs => snd (extract_query (List.last suggs)))
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   451
   handle List.Empty => [])
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   452
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   453
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   454
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   455
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   456
fun try_graph ctxt when def f =
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   457
  f ()
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   458
  handle Graph.CYCLES (cycle :: _) =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   459
         (trace_msg ctxt (fn () =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   460
              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   461
       | Graph.DUP name =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   462
         (trace_msg ctxt (fn () =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   463
              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   464
       | Graph.UNDEF name =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   465
         (trace_msg ctxt (fn () =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   466
              "Unknown fact " ^ quote name ^ " when " ^ when); def)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   467
       | exn =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   468
         if Exn.is_interrupt exn then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   469
           reraise exn
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   470
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   471
           (trace_msg ctxt (fn () =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   472
                "Internal error when " ^ when ^ ":\n" ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   473
                ML_Compiler.exn_message exn); def)
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   474
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   475
type mash_state = {fact_graph : unit Graph.T}
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   476
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   477
val empty_state = {fact_graph = Graph.empty}
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   478
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   479
local
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   480
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   481
val version = "*** MaSh 0.0 ***"
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   482
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   483
fun load _ (state as (true, _)) = state
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   484
  | load ctxt _ =
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   485
    let val path = mash_state_path () in
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   486
      (true,
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   487
       case try File.read_lines path of
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   488
         SOME (version' :: fact_lines) =>
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   489
         let
48322
8a8d71e34297 fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents: 48321
diff changeset
   490
           fun add_edge_to name parent =
8a8d71e34297 fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents: 48321
diff changeset
   491
             Graph.default_node (parent, ())
8a8d71e34297 fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents: 48321
diff changeset
   492
             #> Graph.add_edge (parent, name)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   493
           fun add_fact_line line =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   494
             case extract_query line of
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   495
               ("", _) => I (* shouldn't happen *)
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   496
             | (name, parents) =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   497
               Graph.default_node (name, ())
48322
8a8d71e34297 fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents: 48321
diff changeset
   498
               #> fold (add_edge_to name) parents
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   499
           val fact_graph =
48322
8a8d71e34297 fixed MaSh state load code so it works even if the facts are read in disorder
blanchet
parents: 48321
diff changeset
   500
             try_graph ctxt "loading state" Graph.empty (fn () =>
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   501
                 Graph.empty |> version' = version
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   502
                                ? fold add_fact_line fact_lines)
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   503
         in {fact_graph = fact_graph} end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   504
       | _ => empty_state)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   505
    end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   506
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   507
fun save {fact_graph} =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   508
  let
48309
42c05a6c6c1e implemented low-level MaSh ADD operation
blanchet
parents: 48308
diff changeset
   509
    val path = mash_state_path ()
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   510
    fun fact_line_for name parents =
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   511
      escape_meta name ^ ": " ^ escape_metas parents
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   512
    val append_fact = File.append path o suffix "\n" oo fact_line_for
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   513
  in
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   514
    File.write path (version ^ "\n");
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   515
    Graph.fold (fn (name, ((), (parents, _))) => fn () =>
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   516
                   append_fact name (Graph.Keys.dest parents))
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   517
        fact_graph ()
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   518
  end
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   519
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   520
val global_state =
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
   521
  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   522
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   523
in
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   524
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   525
fun mash_map ctxt f =
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   526
  Synchronized.change global_state (load ctxt ##> (f #> tap save))
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   527
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   528
fun mash_get ctxt =
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   529
  Synchronized.change_result global_state (load ctxt #> `snd)
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   530
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   531
fun mash_unlearn ctxt =
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   532
  Synchronized.change global_state (fn _ =>
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   533
      (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   534
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   535
end
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   536
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   537
fun mash_could_suggest_facts () = mash_home () <> ""
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   538
fun mash_can_suggest_facts ctxt =
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   539
  not (Graph.is_empty (#fact_graph (mash_get ctxt)))
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   540
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   541
fun parents_wrt_facts facts fact_graph =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   542
  let
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   543
    val facts = [] |> fold (cons o nickname_of o snd) facts
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   544
    val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
48377
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   545
    fun insert_not_seen seen name =
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   546
      not (member (op =) seen name) ? insert (op =) name
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   547
    fun parents_of _ parents [] = parents
48377
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   548
      | parents_of seen parents (name :: names) =
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   549
        if Symtab.defined tab name then
48377
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   550
          parents_of (name :: seen) (name :: parents) names
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   551
        else
48377
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   552
          parents_of (name :: seen) parents
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   553
                     (Graph.Keys.fold (insert_not_seen seen)
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   554
                                      (Graph.imm_preds fact_graph name) names)
4a11914fd530 fixed explosion when computing accessibility
blanchet
parents: 48332
diff changeset
   555
  in parents_of [] [] (Graph.maximals fact_graph) end
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   556
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   557
(* Generate more suggestions than requested, because some might be thrown out
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   558
   later for various reasons and "meshing" gives better results with some
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   559
   slack. *)
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   560
fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   561
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   562
fun is_fact_in_graph fact_graph (_, th) =
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   563
  can (Graph.get_node fact_graph) (nickname_of th)
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   564
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   565
fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   566
                       concl_t facts =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   567
  let
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   568
    val thy = Proof_Context.theory_of ctxt
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   569
    val fact_graph = #fact_graph (mash_get ctxt)
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   570
    val parents = parents_wrt_facts facts fact_graph
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   571
    val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   572
    val suggs =
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   573
      if Graph.is_empty fact_graph then []
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   574
      else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   575
    val selected = facts |> suggested_facts suggs
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   576
    val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   577
  in (selected, unknown) end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   578
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   579
fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   580
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   581
    fun maybe_add_from from (accum as (parents, graph)) =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   582
      try_graph ctxt "updating graph" accum (fn () =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   583
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   584
    val graph = graph |> Graph.default_node (name, ())
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   585
    val (parents, graph) = ([], graph) |> fold maybe_add_from parents
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   586
    val (deps, graph) = ([], graph) |> fold maybe_add_from deps
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   587
  in ((name, parents, feats, deps) :: upds, graph) end
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   588
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   589
val learn_timeout_slack = 2.0
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   590
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   591
fun launch_thread timeout task =
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   592
  let
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   593
    val hard_timeout = time_mult learn_timeout_slack timeout
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   594
    val birth_time = Time.now ()
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   595
    val death_time = Time.+ (birth_time, hard_timeout)
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   596
    val desc = ("machine learner for Sledgehammer", "")
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   597
  in Async_Manager.launch MaShN birth_time death_time desc task end
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   598
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   599
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   600
                     used_ths =
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   601
  if is_smt_prover ctxt prover then
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   602
    ()
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   603
  else
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   604
    launch_thread timeout
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   605
        (fn () =>
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   606
            let
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   607
              val thy = Proof_Context.theory_of ctxt
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   608
              val name = timestamp () ^ " " ^ serial_string () (* freshish *)
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   609
              val feats = features_of ctxt prover thy (Local, General) [t]
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   610
              val deps = used_ths |> map nickname_of
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   611
            in
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   612
              mash_map ctxt (fn {fact_graph} =>
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   613
                  let
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   614
                    val parents = parents_wrt_facts facts fact_graph
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   615
                    val upds = [(name, parents, feats, deps)]
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   616
                    val (upds, fact_graph) =
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   617
                      ([], fact_graph) |> fold (update_fact_graph ctxt) upds
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   618
                  in
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   619
                    mash_ADD ctxt overlord upds; {fact_graph = fact_graph}
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   620
                  end);
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   621
              (true, "")
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   622
            end)
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   623
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   624
fun sendback sub =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   625
  Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   626
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   627
(* Too many dependencies is a sign that a decision procedure is at work. There
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   628
   isn't much too learn from such proofs. *)
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   629
val max_dependencies = 10
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   630
val commit_timeout = seconds 30.0
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   631
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   632
(* The timeout is understood in a very slack fashion. *)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   633
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, timeout, ...})
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   634
                     prover auto atp learn_timeout facts =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   635
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   636
    val timer = Timer.startRealTimer ()
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   637
    fun next_commit_time () =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   638
      Time.+ (Timer.checkRealTimer timer, commit_timeout)
48390
4147f2bc4442 add versioning to MaSh state + cleanup dead code
blanchet
parents: 48389
diff changeset
   639
    val {fact_graph} = mash_get ctxt
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   640
    val new_facts =
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   641
      facts |> filter_out (is_fact_in_graph fact_graph)
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   642
            |> sort (thm_ord o pairself snd)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   643
    val num_new_facts = length new_facts
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   644
  in
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   645
    (if not auto then
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   646
       "MaShing" ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   647
       (if not auto then
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   648
          " " ^ string_of_int num_new_facts ^ " fact" ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   649
          plural_s num_new_facts ^
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   650
          (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")"
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   651
           else "")
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   652
        else
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   653
          "") ^ "..."
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   654
     else
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   655
       "")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   656
    |> Output.urgent_message;
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   657
    if null new_facts then
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   658
      if not auto then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   659
        "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   660
        sendback relearn_atpN ^ " to learn from scratch."
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   661
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   662
        ""
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   663
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   664
      let
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   665
        val ths = facts |> map snd
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   666
        val all_names =
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   667
          ths |> filter_out is_likely_tautology_or_too_meta
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   668
              |> map (rpair () o nickname_of)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   669
              |> Symtab.make
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   670
        fun do_commit [] state = state
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   671
          | do_commit upds {fact_graph} =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   672
            let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   673
              val (upds, fact_graph) =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   674
                ([], fact_graph) |> fold (update_fact_graph ctxt) upds
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   675
            in mash_ADD ctxt overlord (rev upds); {fact_graph = fact_graph} end
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   676
        fun trim_deps deps = if length deps > max_dependencies then [] else deps
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   677
        fun commit last upds =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   678
          (if debug andalso not auto then Output.urgent_message "Committing..."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   679
           else ();
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   680
           mash_map ctxt (do_commit (rev upds));
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   681
           if not last andalso not auto then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   682
             let val num_upds = length upds in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   683
               "Processed " ^ string_of_int num_upds ^ " fact" ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   684
               plural_s num_upds ^ " in the last " ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   685
               string_from_time commit_timeout ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   686
               |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   687
             end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   688
           else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   689
             ())
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   690
        fun do_fact _ (accum as (_, (_, _, _, true))) = accum
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   691
          | do_fact ((_, stature), th)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   692
                    (upds, (parents, n, next_commit, false)) =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   693
            let
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   694
              val name = nickname_of th
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   695
              val feats =
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   696
                features_of ctxt prover (theory_of_thm th) stature [prop_of th]
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   697
              val deps =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   698
                (if atp then atp_dependencies_of ctxt params prover auto facts
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   699
                 else isar_dependencies_of) all_names th
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   700
                |> trim_deps
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   701
              val n = n |> not (null deps) ? Integer.add 1
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   702
              val upds = (name, parents, feats, deps) :: upds
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   703
              val (upds, next_commit) =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   704
                if Time.> (Timer.checkRealTimer timer, next_commit) then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   705
                  (commit false upds; ([], next_commit_time ()))
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   706
                else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   707
                  (upds, next_commit)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   708
              val timed_out =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   709
                Time.> (Timer.checkRealTimer timer, learn_timeout)
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   710
            in (upds, ([name], n, next_commit, timed_out)) end
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   711
        val parents = parents_wrt_facts facts fact_graph
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   712
        val (upds, (_, n, _, _)) =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   713
          ([], (parents, 0, next_commit_time (), false))
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   714
          |> fold do_fact new_facts
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   715
      in
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   716
        commit true upds;
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   717
        if verbose orelse not auto then
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
   718
          "Learned " ^ string_of_int n ^ " nontrivial proof" ^ plural_s n ^
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   719
          (if verbose then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   720
             " in " ^ string_from_time (Timer.checkRealTimer timer)
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   721
           else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   722
             "") ^ "."
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   723
        else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   724
          ""
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   725
      end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   726
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   727
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   728
fun mash_learn ctxt (params as {provers, ...}) fact_override chained atp =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   729
  let
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   730
    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   731
    val ctxt = ctxt |> Config.put instantiate_inducts false
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   732
    val facts =
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   733
      nearly_all_facts ctxt false fact_override Symtab.empty css chained []
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   734
                       @{prop True}
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   735
  in
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   736
     mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   737
     |> Output.urgent_message
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   738
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   739
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   740
(* The threshold should be large enough so that MaSh doesn't kick in for Auto
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   741
   Sledgehammer and Try. *)
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   742
val min_secs_for_learning = 15
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   743
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   744
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   745
        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   746
  if not (subset (op =) (the_list fact_filter, fact_filters)) then
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   747
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   748
  else if only then
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   749
    facts
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   750
  else if max_facts <= 0 orelse null facts then
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   751
    []
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   752
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   753
    let
48327
568b3193e53e don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents: 48326
diff changeset
   754
      fun maybe_learn () =
48384
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   755
        if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   756
           Time.toSeconds timeout >= min_secs_for_learning then
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   757
          let val timeout = time_mult learn_timeout_slack timeout in
83dc102041e6 learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
blanchet
parents: 48383
diff changeset
   758
            launch_thread timeout
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   759
                (fn () => (true, mash_learn_facts ctxt params prover true false
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   760
                                                  timeout facts))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   761
          end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   762
        else
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   763
          ()
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   764
      val fact_filter =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   765
        case fact_filter of
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   766
          SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   767
        | NONE =>
48386
b903ea11b3bc use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
blanchet
parents: 48385
diff changeset
   768
          if is_smt_prover ctxt prover then mepoN
b903ea11b3bc use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
blanchet
parents: 48385
diff changeset
   769
          else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   770
          else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   771
          else mepoN
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   772
      val add_ths = Attrib.eval_thms ctxt add
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   773
      fun prepend_facts ths accepts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   774
        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   775
         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   776
        |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   777
      fun iter () =
48298
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   778
        iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
f5b160f9859e more work on MaSh
blanchet
parents: 48297
diff changeset
   779
                                 concl_t facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   780
      fun mash () =
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   781
        mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   782
      val mess =
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   783
        [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   784
           |> (if fact_filter <> mepoN then cons (mash ()) else I)
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   785
    in
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   786
      mesh_facts max_facts mess
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   787
      |> not (null add_ths) ? prepend_facts add_ths
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   788
    end
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   789
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   790
fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   791
fun running_learners () = Async_Manager.running_threads MaShN "learner"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   792
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
   793
end;