src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Sat, 01 Dec 2012 23:55:39 +0100
changeset 50311 c9d7ccd090e1
parent 50310 b00eeb8e352e
child 50319 dddcaeb92e11
permissions -rw-r--r--
tuned order of functions
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
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    31
  val extract_query : string -> string * (string * real) list
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    32
  val mash_CLEAR : Proof.context -> unit
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    33
  val mash_ADD :
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    34
    Proof.context -> bool
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    35
    -> (string * string list * string list * string list) list -> unit
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    36
  val mash_REPROVE :
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    37
    Proof.context -> bool -> (string * string list) list -> unit
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    38
  val mash_QUERY :
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    39
    Proof.context -> bool -> int -> string list * string list
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    40
    -> (string * real) list
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    41
  val mash_unlearn : Proof.context -> unit
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
    42
  val nickname_of : thm -> string
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    43
  val suggested_facts :
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    44
    (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    45
  val mesh_facts :
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    46
    int -> ((('a * thm) * real) list * ('a * thm) list) list -> ('a * thm) list
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    47
  val theory_ord : theory * theory -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    48
  val thm_ord : thm * thm -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    49
  val goal_of_thm : theory -> thm -> thm
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    50
  val run_prover_for_mash :
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    51
    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
    52
  val features_of :
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    53
    Proof.context -> string -> theory -> stature -> term list -> string list
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
    54
  val isar_dependencies_of : unit Symtab.table -> thm -> string list option
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    55
  val atp_dependencies_of :
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
    56
    Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
    57
    -> thm -> bool * string list option
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    58
  val mash_suggested_facts :
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    59
    Proof.context -> params -> string -> int -> term list -> term
48435
f30eb5eb7927 include unknown local facts in MaSh
blanchet
parents: 48434
diff changeset
    60
    -> fact list -> (fact * real) list * fact list
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
    61
  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
    62
    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
    63
    -> unit
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    64
  val mash_learn :
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    65
    Proof.context -> params -> fact_override -> thm list -> bool -> unit
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    66
  val is_mash_enabled : unit -> bool
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    67
  val mash_can_suggest_facts : Proof.context -> bool
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
50310
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   104
fun mash_script () = Path.explode "$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py"
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 () =
50310
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   106
  Path.explode "$ISABELLE_HOME_USER/mash"
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   107
  |> tap Isabelle_System.mkdir
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
50310
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   109
fun mash_state_file () = Path.append (mash_state_dir ()) (Path.explode "state")
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
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   112
(*** Low-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   113
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   114
fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   115
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   116
fun write_file banner (xs, f) file =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   117
  let val path = Path.explode file in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   118
    case banner of SOME s => File.write path s | NONE => ();
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   119
    xs |> chunk_list 500
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   120
       |> List.app (File.append path o space_implode "" o map f)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   121
  end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   122
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   123
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   124
  let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   125
    val (temp_dir, serial) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   126
      if overlord then (getenv "ISABELLE_HOME_USER", "")
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   127
      else (getenv "ISABELLE_TMP", serial_string ())
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   128
    val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   129
    val err_file = temp_dir ^ "/mash_err" ^ serial
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   130
    val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   131
    val cmd_file = temp_dir ^ "/mash_commands" ^ serial
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   132
    val core =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   133
      "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   134
      " --numberOfPredictions " ^ string_of_int max_suggs ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   135
      (if save then " --saveModel" else "")
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   136
    val command =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   137
      Path.implode (mash_script ()) ^ " --quiet --outputDir " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   138
      Path.implode (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   139
      " >& " ^ err_file
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   140
      |> tap (fn _ => trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   141
             case try File.read (Path.explode err_file) of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   142
               NONE => "Done"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   143
             | SOME "" => "Done"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   144
             | SOME s => "Error: " ^ elide_string 1000 s))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   145
    fun run_on () =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   146
      (Isabelle_System.bash command;
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   147
       read_suggs (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   148
           try File.read_lines (Path.explode sugg_file) |> these))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   149
    fun clean_up () =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   150
      if overlord then ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   151
      else List.app wipe_out_file [err_file, sugg_file, cmd_file]
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   152
  in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   153
    write_file (SOME "") ([], K "") sugg_file;
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   154
    write_file (SOME "") write_cmds cmd_file;
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   155
    trace_msg ctxt (fn () => "Running " ^ command);
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   156
    with_cleanup clean_up run_on ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   157
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   158
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   159
fun meta_char c =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   160
  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
   161
     c = #")" orelse c = #"," then
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   162
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   163
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   164
    (* fixed width, in case more digits follow *)
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   165
    "%" ^ stringN_of_int 3 (Char.ord c)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   166
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   167
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
   168
  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   169
    (case Int.fromString (String.implode [d1, d2, d3]) of
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   170
       SOME n => unmeta_chars (Char.chr n :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   171
     | NONE => "" (* error *))
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   172
  | unmeta_chars _ (#"%" :: _) = "" (* error *)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   173
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   174
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   175
val escape_meta = String.translate meta_char
48303
f1d135d0ea69 improved MaSh string escaping and make more operations string-based
blanchet
parents: 48302
diff changeset
   176
val escape_metas = map escape_meta #> space_implode " "
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   177
val unescape_meta = String.explode #> unmeta_chars []
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   178
val unescape_metas =
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   179
  space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   180
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   181
fun str_of_add (name, parents, feats, deps) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   182
  "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   183
  escape_metas feats ^ "; " ^ escape_metas deps ^ "\n"
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   184
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   185
fun str_of_reprove (name, deps) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   186
  "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   187
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   188
fun str_of_query (parents, feats) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   189
  "? " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "\n"
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   190
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   191
fun extract_suggestion sugg =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   192
  case space_explode "=" sugg of
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   193
    [name, weight] =>
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   194
    SOME (unescape_meta name, Real.fromString weight |> the_default 0.0)
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   195
  | _ => NONE
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   196
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   197
fun extract_query line =
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   198
  case space_explode ":" line of
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   199
    [goal, suggs] =>
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   200
    (unescape_meta goal,
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   201
     map_filter extract_suggestion (space_explode " " suggs))
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   202
  | _ => ("", [])
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   203
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   204
fun mash_CLEAR ctxt =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   205
  let val path = mash_model_dir () in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   206
    trace_msg ctxt (K "MaSh CLEAR");
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   207
    File.fold_dir (fn file => fn _ =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   208
                      try File.rm (Path.append path (Path.basic file)))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   209
                  path NONE;
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   210
    ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   211
  end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   212
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   213
fun mash_ADD _ _ [] = ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   214
  | mash_ADD ctxt overlord adds =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   215
    (trace_msg ctxt (fn () => "MaSh ADD " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   216
         elide_string 1000 (space_implode " " (map #1 adds)));
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   217
     run_mash_tool ctxt overlord true 0 (adds, str_of_add) (K ()))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   218
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   219
fun mash_REPROVE _ _ [] = ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   220
  | mash_REPROVE ctxt overlord reps =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   221
    (trace_msg ctxt (fn () => "MaSh REPROVE " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   222
         elide_string 1000 (space_implode " " (map #1 reps)));
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   223
     run_mash_tool ctxt overlord true 0 (reps, str_of_reprove) (K ()))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   224
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   225
fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   226
  (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   227
   run_mash_tool ctxt overlord false max_suggs
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   228
       ([query], str_of_query)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   229
       (fn suggs =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   230
           case suggs () of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   231
             [] => []
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   232
           | suggs => snd (extract_query (List.last suggs)))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   233
   handle List.Empty => [])
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   234
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   235
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   236
(*** Middle-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   237
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   238
datatype proof_kind = Isar_Proof | ATP_Proof | Isar_Proof_wegen_ATP_Flop
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   239
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   240
fun str_of_proof_kind Isar_Proof = "i"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   241
  | str_of_proof_kind ATP_Proof = "a"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   242
  | str_of_proof_kind Isar_Proof_wegen_ATP_Flop = "x"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   243
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   244
fun proof_kind_of_str "i" = Isar_Proof
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   245
  | proof_kind_of_str "a" = ATP_Proof
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   246
  | proof_kind_of_str "x" = Isar_Proof_wegen_ATP_Flop
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   247
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   248
(* FIXME: Here a "Graph.update_node" function would be useful *)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   249
fun update_fact_graph_node (name, kind) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   250
  Graph.default_node (name, Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   251
  #> kind <> Isar_Proof ? Graph.map_node name (K kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   252
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   253
fun try_graph ctxt when def f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   254
  f ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   255
  handle Graph.CYCLES (cycle :: _) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   256
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   257
              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   258
       | Graph.DUP name =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   259
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   260
              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   261
       | Graph.UNDEF name =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   262
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   263
              "Unknown fact " ^ quote name ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   264
       | exn =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   265
         if Exn.is_interrupt exn then
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   266
           reraise exn
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   267
         else
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   268
           (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   269
                "Internal error when " ^ when ^ ":\n" ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   270
                ML_Compiler.exn_message exn); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   271
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   272
fun graph_info G =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   273
  string_of_int (length (Graph.keys G)) ^ " node(s), " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   274
  string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   275
  " edge(s), " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   276
  string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   277
  string_of_int (length (Graph.maximals G)) ^ " maximal"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   278
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   279
type mash_state = {fact_G : unit Graph.T, dirty : string list option}
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   280
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   281
val empty_state = {fact_G = Graph.empty, dirty = SOME []}
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   282
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   283
local
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   284
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   285
val version = "*** MaSh 0.0 ***"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   286
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   287
fun extract_node line =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   288
  case space_explode ":" line of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   289
    [head, parents] =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   290
    (case space_explode " " head of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   291
       [kind, name] =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   292
       SOME (unescape_meta name, unescape_metas parents,
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   293
             try proof_kind_of_str kind |> the_default Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   294
     | _ => NONE)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   295
  | _ => NONE
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   296
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   297
fun load _ (state as (true, _)) = state
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   298
  | load ctxt _ =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   299
    let val path = mash_state_file () in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   300
      (true,
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   301
       case try File.read_lines path of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   302
         SOME (version' :: node_lines) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   303
         let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   304
           fun add_edge_to name parent =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   305
             Graph.default_node (parent, Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   306
             #> Graph.add_edge (parent, name)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   307
           fun add_node line =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   308
             case extract_node line of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   309
               NONE => I (* shouldn't happen *)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   310
             | SOME (name, parents, kind) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   311
               update_fact_graph_node (name, kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   312
               #> fold (add_edge_to name) parents
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   313
           val fact_G =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   314
             try_graph ctxt "loading state" Graph.empty (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   315
                 Graph.empty |> version' = version ? fold add_node node_lines)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   316
         in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   317
           trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   318
               "Loaded fact graph (" ^ graph_info fact_G ^ ")");
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   319
           {fact_G = fact_G, dirty = SOME []}
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   320
         end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   321
       | _ => empty_state)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   322
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   323
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   324
fun save _ (state as {dirty = SOME [], ...}) = state
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   325
  | save ctxt {fact_G, dirty} =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   326
    let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   327
      fun str_of_entry (name, parents, kind) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   328
        str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   329
        escape_metas parents ^ "\n"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   330
      fun append_entry (name, (kind, (parents, _))) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   331
        cons (name, Graph.Keys.dest parents, kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   332
      val (banner, entries) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   333
        case dirty of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   334
          SOME names =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   335
          (NONE, fold (append_entry o Graph.get_entry fact_G) names [])
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   336
        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G [])
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   337
    in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   338
      write_file banner (entries, str_of_entry)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   339
                 (Path.implode (mash_state_file ()));
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   340
      trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   341
          "Saved fact graph (" ^ graph_info fact_G ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   342
          (case dirty of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   343
             SOME dirty =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   344
             "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   345
           | _ => "") ^  ")");
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   346
      {fact_G = fact_G, dirty = SOME []}
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   347
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   348
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   349
val global_state =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   350
  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   351
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   352
in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   353
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   354
fun mash_map ctxt f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   355
  Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   356
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   357
fun mash_peek ctxt f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   358
  Synchronized.change_result global_state (load ctxt #> `snd #>> f)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   359
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   360
fun mash_get ctxt =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   361
  Synchronized.change_result global_state (load ctxt #> `snd)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   362
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   363
fun mash_unlearn ctxt =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   364
  Synchronized.change global_state (fn _ =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   365
      (mash_CLEAR ctxt; (* also removes the state file *)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   366
       (true, empty_state)))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   367
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   368
end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   369
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   370
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   371
(*** Isabelle helpers ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   372
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   373
fun parent_of_local_thm th =
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   374
  let
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   375
    val thy = th |> Thm.theory_of_thm
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   376
    val facts = thy |> Global_Theory.facts_of
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   377
    val space = facts |> Facts.space_of
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   378
    fun id_of s = #id (Name_Space.the_entry space s)
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   379
    fun max_id (s', _) (s, id) =
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   380
      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
   381
  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   382
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   383
val local_prefix = "local" ^ Long_Name.separator
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   384
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   385
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
   386
  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
   387
    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
   388
      (* 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
   389
      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
   390
        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
   391
        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
   392
      | 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
   393
    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
   394
  else
50047
45684acf0b94 thread context correctly when printing backquoted facts
blanchet
parents: 49997
diff changeset
   395
    backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   396
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   397
fun suggested_facts suggs facts =
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   398
  let
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   399
    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   400
    val tab = Symtab.empty |> fold add_fact facts
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   401
    fun find_sugg (name, weight) =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   402
      Symtab.lookup tab name |> Option.map (rpair weight)
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   403
  in map_filter find_sugg suggs end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   404
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   405
fun sum_avg [] = 0
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   406
  | sum_avg xs =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   407
    Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
48328
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   408
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   409
fun normalize_scores [] = []
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   410
  | normalize_scores ((fact, score) :: tail) =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   411
    (fact, 1.0) :: map (apsnd (curry Real.* (1.0 / score))) tail
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   412
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   413
fun mesh_facts max_facts [(sels, unks)] =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   414
    map fst (take max_facts sels) @ take (max_facts - length sels) unks
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   415
  | mesh_facts max_facts mess =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   416
    let
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   417
      val mess = mess |> map (apfst (normalize_scores #> `length))
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   418
      val fact_eq = Thm.eq_thm o pairself snd
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   419
      fun score_at sels = try (nth sels) #> Option.map 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
   420
      fun score_in fact ((sel_len, sels), unks) =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   421
        case find_index (curry fact_eq fact o fst) sels of
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   422
          ~1 => (case find_index (curry fact_eq fact) unks of
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   423
                   ~1 => score_at sels 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
   424
                 | _ => NONE)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   425
        | rank => score_at sels rank
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   426
      fun weight_of fact = mess |> map_filter (score_in fact) |> sum_avg
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   427
      val facts =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   428
        fold (union fact_eq o map fst 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
   429
    in
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   430
      facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
48328
ca0b7d19dd62 attempt at meshing according to more meaningful factors
blanchet
parents: 48327
diff changeset
   431
            |> map snd |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   432
    end
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   433
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   434
val thy_feature_name_of = prefix "y"
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   435
val const_name_of = prefix "c"
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   436
val type_name_of = prefix "t"
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   437
val class_name_of = prefix "s"
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   438
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   439
fun theory_ord p =
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   440
  if Theory.eq_thy p then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   441
    EQUAL
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   442
  else if Theory.subthy p then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   443
    LESS
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   444
  else if Theory.subthy (swap p) then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   445
    GREATER
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   446
  else case int_ord (pairself (length o Theory.ancestors_of) p) of
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   447
    EQUAL => string_ord (pairself Context.theory_name p)
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   448
  | order => order
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   449
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   450
val thm_ord = theory_ord o pairself theory_of_thm
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   451
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   452
val freezeT = Type.legacy_freeze_type
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   453
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   454
fun freeze (t $ u) = freeze t $ freeze u
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   455
  | 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
   456
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   457
  | freeze (Const (s, T)) = Const (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   458
  | freeze (Free (s, T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   459
  | freeze t = t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   460
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   461
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
   462
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   463
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
   464
  let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   465
    val problem =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   466
      {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
   467
       facts = facts |> map (apfst (apfst (fn name => name ())))
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   468
                     |> map Untranslated_Fact}
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   469
  in
48399
4bacc8983b3d learn from SMT proofs when they can be minimized by Metis
blanchet
parents: 48398
diff changeset
   470
    get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   471
                          problem
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   472
  end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   473
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   474
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   475
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   476
val logical_consts =
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   477
  [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   478
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   479
fun interesting_terms_types_and_classes ctxt prover term_max_depth
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   480
                                        type_max_depth ts =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   481
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   482
    fun is_bad_const (x as (s, _)) args =
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   483
      member (op =) logical_consts s orelse
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   484
      fst (is_built_in_const_for_prover ctxt prover x args)
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   485
    fun add_classes @{sort type} = I
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   486
      | 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
   487
    fun do_add_type (Type (s, Ts)) =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   488
        (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
   489
        #> fold do_add_type Ts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   490
      | do_add_type (TFree (_, S)) = add_classes S
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   491
      | do_add_type (TVar (_, S)) = add_classes S
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   492
    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
   493
    fun mk_app s args =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   494
      if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   495
      else s
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   496
    fun patternify ~1 _ = ""
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   497
      | patternify depth t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   498
        case strip_comb t of
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   499
          (Const (x as (s, _)), args) =>
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   500
          if is_bad_const x args then ""
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   501
          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
   502
        | _ => ""
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   503
    fun add_pattern depth t =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   504
      case patternify depth t of "" => I | s => insert (op =) s
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   505
    fun add_term_patterns ~1 _ = I
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   506
      | add_term_patterns depth t =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   507
        add_pattern depth t #> add_term_patterns (depth - 1) t
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   508
    val add_term = add_term_patterns term_max_depth
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   509
    fun add_patterns t =
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   510
      let val (head, args) = strip_comb t in
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   511
        (case head of
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   512
           Const (_, T) => add_term t #> add_type T
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   513
         | Free (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   514
         | Var (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   515
         | Abs (_, T, body) => add_type T #> add_patterns body
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   516
         | _ => I)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   517
        #> fold add_patterns args
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   518
      end
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   519
  in [] |> fold add_patterns ts end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   520
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   521
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
   522
48297
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   523
val term_max_depth = 1
dcf3160376ae compile
blanchet
parents: 48296
diff changeset
   524
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   525
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   526
(* TODO: Generate type classes for types? *)
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   527
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
   528
  thy_feature_name_of (Context.theory_name thy) ::
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   529
  interesting_terms_types_and_classes ctxt prover term_max_depth type_max_depth
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   530
                                      ts
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   531
  |> forall is_lambda_free ts ? cons "no_lams"
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   532
  |> forall (not o exists_Const is_exists) ts ? cons "no_skos"
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   533
  |> scope <> Global ? cons "local"
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   534
  |> (case string_of_status status of "" => I | s => cons s)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   535
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   536
(* Too many dependencies is a sign that a crazy decision procedure is at work.
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   537
   There isn't much to learn from such proofs. *)
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   538
val max_dependencies = 100
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   539
val atp_dependency_default_max_facts = 50
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   540
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   541
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   542
val typedef_deps = [@{thm CollectI} |> nickname_of]
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   543
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   544
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   545
val typedef_ths =
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   546
  @{thms type_definition.Abs_inverse type_definition.Rep_inverse
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   547
         type_definition.Rep type_definition.Rep_inject
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   548
         type_definition.Abs_inject type_definition.Rep_cases
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   549
         type_definition.Abs_cases type_definition.Rep_induct
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   550
         type_definition.Abs_induct type_definition.Rep_range
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   551
         type_definition.Abs_image}
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   552
  |> map nickname_of
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   553
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   554
fun is_size_def [dep] th =
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   555
    (case first_field ".recs" dep of
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   556
       SOME (pref, _) =>
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   557
       (case first_field ".size" (nickname_of th) of
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   558
          SOME (pref', _) => pref = pref'
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   559
        | NONE => false)
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   560
     | NONE => false)
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   561
  | is_size_def _ _ = false
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   562
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   563
fun trim_dependencies th deps =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   564
  if length deps > max_dependencies then
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   565
    NONE
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   566
  else
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   567
    SOME (if deps = typedef_deps orelse
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   568
             exists (member (op =) typedef_ths) deps orelse
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   569
             is_size_def deps th then
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   570
            []
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   571
          else
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   572
            deps)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   573
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   574
fun isar_dependencies_of all_names th =
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   575
  th |> thms_in_proof (SOME all_names) |> trim_dependencies th
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   576
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   577
fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   578
                        auto_level facts all_names th =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   579
  case isar_dependencies_of all_names th of
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   580
    SOME [] => (false, SOME [])
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   581
  | isar_deps =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   582
    let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   583
      val thy = Proof_Context.theory_of ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   584
      val goal = goal_of_thm thy th
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   585
      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
   586
      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
   587
      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
   588
      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
   589
      fun add_isar_dep facts dep accum =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   590
        if exists (is_dep dep) accum then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   591
          accum
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   592
        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
   593
          SOME ((name, status), th) => accum @ [((name, status), th)]
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   594
        | NONE => accum (* shouldn't happen *)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   595
      val facts =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   596
        facts |> mepo_suggested_facts ctxt params prover
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   597
                     (max_facts |> the_default atp_dependency_default_max_facts)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   598
                     NONE hyp_ts concl_t
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   599
              |> fold (add_isar_dep facts) (these isar_deps)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   600
              |> map fix_name
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   601
    in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   602
      if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   603
        let val num_facts = length facts in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   604
          "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   605
          " 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
   606
          "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   607
          |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   608
        end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   609
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   610
        ();
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   611
      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
   612
        {outcome = NONE, used_facts, ...} =>
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   613
        (if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   614
           let val num_facts = length used_facts in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   615
             "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
   616
             plural_s num_facts ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   617
             |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   618
           end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   619
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   620
           ();
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   621
         case used_facts |> map fst |> trim_dependencies th of
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   622
           NONE => (false, isar_deps)
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   623
         | atp_deps => (true, atp_deps))
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   624
      | _ => (false, isar_deps)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   625
    end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   626
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   627
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   628
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   629
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   630
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   631
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   632
fun maximal_in_graph fact_G facts =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   633
  let
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   634
    val facts = [] |> fold (cons o nickname_of o snd) facts
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   635
    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   636
    fun insert_new seen name =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   637
      not (Symtab.defined seen name) ? insert (op =) name
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   638
    fun find_maxes _ (maxs, []) = map snd maxs
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   639
      | find_maxes seen (maxs, new :: news) =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   640
        find_maxes
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   641
            (seen |> num_keys (Graph.imm_succs fact_G new) > 1
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   642
                     ? Symtab.default (new, ()))
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   643
            (if Symtab.defined tab new then
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   644
               let
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   645
                 val newp = Graph.all_preds fact_G [new]
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   646
                 fun is_ancestor x yp = member (op =) yp x
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   647
                 val maxs =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   648
                   maxs |> filter (fn (_, max) => not (is_ancestor max newp))
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   649
               in
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   650
                 if exists (is_ancestor new o fst) maxs then
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   651
                   (maxs, news)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   652
                 else
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   653
                   ((newp, new)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   654
                    :: filter_out (fn (_, max) => is_ancestor max newp) maxs,
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   655
                    news)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   656
               end
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   657
             else
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   658
               (maxs, Graph.Keys.fold (insert_new seen)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   659
                                      (Graph.imm_preds fact_G new) news))
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   660
  in find_maxes Symtab.empty ([], Graph.maximals fact_G) end
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   661
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   662
(* Generate more suggestions than requested, because some might be thrown out
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   663
   later for various reasons and "meshing" gives better results with some
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   664
   slack. *)
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   665
fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   666
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   667
fun is_fact_in_graph fact_G (_, th) =
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   668
  can (Graph.get_node fact_G) (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
   669
48442
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   670
fun interleave 0 _ _ = []
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   671
  | interleave n [] ys = take n ys
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   672
  | interleave n xs [] = take n xs
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   673
  | interleave 1 (x :: _) _ = [x]
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   674
  | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
48435
f30eb5eb7927 include unknown local facts in MaSh
blanchet
parents: 48434
diff changeset
   675
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   676
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   677
                         concl_t facts =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   678
  let
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   679
    val thy = Proof_Context.theory_of ctxt
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   680
    val (fact_G, suggs) =
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   681
      mash_peek ctxt (fn {fact_G, ...} =>
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   682
          if Graph.is_empty fact_G then
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   683
            (fact_G, [])
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   684
          else
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   685
            let
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   686
              val parents = maximal_in_graph fact_G facts
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   687
              val feats =
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   688
                features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   689
            in
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   690
              (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   691
                                  (parents, feats))
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   692
            end)
48435
f30eb5eb7927 include unknown local facts in MaSh
blanchet
parents: 48434
diff changeset
   693
    val sels =
48408
5493e67982ee tune Mesh filter
blanchet
parents: 48407
diff changeset
   694
      facts |> suggested_facts suggs
5493e67982ee tune Mesh filter
blanchet
parents: 48407
diff changeset
   695
            (* The weights currently returned by "mash.py" are too extreme to
5493e67982ee tune Mesh filter
blanchet
parents: 48407
diff changeset
   696
               make any sense. *)
48435
f30eb5eb7927 include unknown local facts in MaSh
blanchet
parents: 48434
diff changeset
   697
            |> map fst
f30eb5eb7927 include unknown local facts in MaSh
blanchet
parents: 48434
diff changeset
   698
    val (unk_global, unk_local) =
f30eb5eb7927 include unknown local facts in MaSh
blanchet
parents: 48434
diff changeset
   699
      facts |> filter_out (is_fact_in_graph fact_G)
48442
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   700
            |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   701
  in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   702
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   703
fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   704
  let
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   705
    fun maybe_add_from from (accum as (parents, graph)) =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   706
      try_graph ctxt "updating graph" accum (fn () =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   707
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   708
    val graph = graph |> Graph.default_node (name, Isar_Proof)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   709
    val (parents, graph) = ([], graph) |> fold maybe_add_from parents
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   710
    val (deps, _) = ([], graph) |> fold maybe_add_from deps
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   711
  in ((name, parents, feats, deps) :: adds, graph) end
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   712
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   713
fun reprove_wrt_fact_graph ctxt (name, deps) (reps, graph) =
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   714
  let
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   715
    fun maybe_rep_from from (accum as (parents, graph)) =
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   716
      try_graph ctxt "updating graph" accum (fn () =>
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   717
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   718
    val graph = graph |> update_fact_graph_node (name, ATP_Proof)
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   719
    val (deps, _) = ([], graph) |> fold maybe_rep_from deps
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   720
  in ((name, deps) :: reps, graph) end
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   721
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   722
fun flop_wrt_fact_graph name =
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   723
  update_fact_graph_node (name, Isar_Proof_wegen_ATP_Flop)
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   724
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
   725
val learn_timeout_slack = 2.0
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   726
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
   727
fun launch_thread timeout task =
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   728
  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
   729
    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
   730
    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
   731
    val death_time = Time.+ (birth_time, hard_timeout)
48442
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   732
    val desc = ("Machine learner for Sledgehammer", "")
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
   733
  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
   734
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   735
fun freshish_name () =
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   736
  Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   737
  serial_string ()
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   738
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
   739
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
   740
                     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
   741
  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
   742
    ()
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
   743
  else
48403
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   744
    launch_thread timeout (fn () =>
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   745
        let
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   746
          val thy = Proof_Context.theory_of ctxt
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   747
          val name = freshish_name ()
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   748
          val feats = features_of ctxt prover thy (Local, General) [t]
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   749
          val deps = used_ths |> map nickname_of
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   750
        in
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   751
          mash_peek ctxt (fn {fact_G, ...} =>
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   752
              let val parents = maximal_in_graph fact_G facts in
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   753
                mash_ADD ctxt overlord [(name, parents, feats, deps)]
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   754
              end);
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   755
          (true, "")
48403
1f214c653c80 don't store fresh names in fact graph, since these cannot be the parents of any other facts
blanchet
parents: 48401
diff changeset
   756
        end)
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   757
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents: 50047
diff changeset
   758
fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   759
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   760
val commit_timeout = seconds 30.0
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   761
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   762
(* The timeout is understood in a very slack fashion. *)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   763
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   764
                     auto_level atp learn_timeout facts =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   765
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   766
    val timer = Timer.startRealTimer ()
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   767
    fun next_commit_time () =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   768
      Time.+ (Timer.checkRealTimer timer, commit_timeout)
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   769
    val {fact_G, ...} = mash_get ctxt
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   770
    val (old_facts, new_facts) =
48667
ac58317ef11f rule out same "technical" theories for MePo as for MaSh
blanchet
parents: 48665
diff changeset
   771
      facts |> List.partition (is_fact_in_graph fact_G)
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   772
            ||> sort (thm_ord o pairself snd)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   773
  in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   774
    if null new_facts andalso (not atp orelse null old_facts) then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   775
      if auto_level < 2 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   776
        "No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   777
        (if auto_level = 0 andalso not atp then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   778
           "\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   779
         else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   780
           "")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   781
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   782
        ""
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   783
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   784
      let
48315
82d6e46c673f fixed order of accessibles + other tweaks to MaSh
blanchet
parents: 48314
diff changeset
   785
        val all_names =
49997
dbbf9578e712 made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
blanchet
parents: 48699
diff changeset
   786
          Symtab.empty
dbbf9578e712 made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)
blanchet
parents: 48699
diff changeset
   787
          |> fold Symtab.update (facts |> map (rpair () o nickname_of o snd))
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   788
        fun deps_of status th =
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   789
          if status = Non_Rec_Def orelse status = Rec_Def then
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   790
            SOME []
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   791
          else if atp then
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   792
            atp_dependencies_of ctxt params prover auto_level facts all_names th
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   793
            |> (fn (false, _) => NONE | (true, deps) => deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   794
          else
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   795
            isar_dependencies_of all_names th
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   796
        fun do_commit [] [] [] state = state
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   797
          | do_commit adds reps flops {fact_G, dirty} =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   798
            let
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   799
              val was_empty = Graph.is_empty fact_G
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   800
              val (adds, fact_G) =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   801
                ([], fact_G) |> fold (add_wrt_fact_graph ctxt) adds
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   802
              val (reps, fact_G) =
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   803
                ([], fact_G) |> fold (reprove_wrt_fact_graph ctxt) reps
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   804
              val fact_G = fact_G |> fold flop_wrt_fact_graph flops
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   805
              val dirty =
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   806
                case (was_empty, dirty, reps) of
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   807
                  (false, SOME names, []) => SOME (map #1 adds @ names)
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   808
                | _ => NONE
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   809
            in
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   810
              mash_ADD ctxt overlord (rev adds);
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   811
              mash_REPROVE ctxt overlord reps;
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   812
              {fact_G = fact_G, dirty = dirty}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   813
            end
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   814
        fun commit last adds reps flops =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   815
          (if debug andalso auto_level = 0 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   816
             Output.urgent_message "Committing..."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   817
           else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   818
             ();
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   819
           mash_map ctxt (do_commit (rev adds) reps flops);
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   820
           if not last andalso auto_level = 0 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   821
             let val num_proofs = length adds + length reps in
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   822
               "Learned " ^ string_of_int num_proofs ^ " " ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   823
               (if atp then "ATP" else "Isar") ^ " proof" ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   824
               plural_s num_proofs ^ " in the last " ^
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   825
               string_from_time commit_timeout ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   826
               |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   827
             end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   828
           else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   829
             ())
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   830
        fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   831
          | learn_new_fact ((_, stature as (_, status)), th)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   832
                           (adds, (parents, n, next_commit, _)) =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   833
            let
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   834
              val name = nickname_of th
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   835
              val feats =
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   836
                features_of ctxt prover (theory_of_thm th) stature [prop_of th]
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   837
              val deps = deps_of status th |> these
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
   838
              val n = n |> not (null deps) ? Integer.add 1
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   839
              val adds = (name, parents, feats, deps) :: adds
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   840
              val (adds, next_commit) =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   841
                if Time.> (Timer.checkRealTimer timer, next_commit) then
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   842
                  (commit false adds [] []; ([], next_commit_time ()))
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   843
                else
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   844
                  (adds, next_commit)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   845
              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   846
            in (adds, ([name], n, next_commit, timed_out)) end
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   847
        val n =
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   848
          if null new_facts then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   849
            0
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   850
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   851
            let
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   852
              val last_th = new_facts |> List.last |> snd
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   853
              (* crude approximation *)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   854
              val ancestors =
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   855
                old_facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   856
                |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   857
              val parents = maximal_in_graph fact_G ancestors
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   858
              val (adds, (_, n, _, _)) =
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   859
                ([], (parents, 0, next_commit_time (), false))
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   860
                |> fold learn_new_fact new_facts
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   861
            in commit true adds [] []; n end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   862
        fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   863
          | relearn_old_fact ((_, (_, status)), th)
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   864
                             ((reps, flops), (n, next_commit, _)) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   865
            let
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   866
              val name = nickname_of th
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   867
              val (n, reps, flops) =
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   868
                case deps_of status th of
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   869
                  SOME deps => (n + 1, (name, deps) :: reps, flops)
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   870
                | NONE => (n, reps, name :: flops)
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   871
              val (reps, flops, next_commit) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   872
                if Time.> (Timer.checkRealTimer timer, next_commit) then
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   873
                  (commit false [] reps flops; ([], [], next_commit_time ()))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   874
                else
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   875
                  (reps, flops, next_commit)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   876
              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   877
            in ((reps, flops), (n, next_commit, timed_out)) end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   878
        val n =
48433
9e9b6e363859 don't relearn old facts in Isar mode
blanchet
parents: 48408
diff changeset
   879
          if not atp orelse null old_facts then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   880
            n
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   881
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   882
            let
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   883
              val max_isar = 1000 * max_dependencies
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   884
              fun kind_of_proof th =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   885
                try (Graph.get_node fact_G) (nickname_of th)
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   886
                |> the_default Isar_Proof
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   887
              fun priority_of (_, th) =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   888
                random_range 0 max_isar
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   889
                + (case kind_of_proof th of
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   890
                     Isar_Proof => 0
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   891
                   | ATP_Proof => 2 * max_isar
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   892
                   | Isar_Proof_wegen_ATP_Flop => max_isar)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   893
                - 500 * (th |> isar_dependencies_of all_names
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   894
                            |> Option.map length
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   895
                            |> the_default max_dependencies)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   896
              val old_facts =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   897
                old_facts |> map (`priority_of)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   898
                          |> sort (int_ord o pairself fst)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   899
                          |> map snd
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   900
              val ((reps, flops), (n, _, _)) =
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   901
                (([], []), (n, next_commit_time (), false))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   902
                |> fold relearn_old_fact old_facts
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   903
            in commit true [] reps flops; n end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   904
      in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   905
        if verbose orelse auto_level < 2 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   906
          "Learned " ^ string_of_int n ^ " nontrivial " ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   907
          (if atp then "ATP" else "Isar") ^ " 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
   908
          (if verbose then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   909
             " 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
   910
           else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   911
             "") ^ "."
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   912
        else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   913
          ""
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   914
      end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   915
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   916
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   917
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   918
               atp =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   919
  let
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   920
    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
   921
    val ctxt = ctxt |> Config.put instantiate_inducts false
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   922
    val facts =
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   923
      nearly_all_facts ctxt false fact_override Symtab.empty css chained []
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
   924
                       @{prop True}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   925
    val num_facts = length facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   926
    val prover = hd provers
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   927
    fun learn auto_level atp =
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   928
      mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   929
      |> Output.urgent_message
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   930
  in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   931
    (if atp then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   932
       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   933
        plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   934
        string_from_time timeout ^ ").\n\nCollecting Isar proofs first..."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   935
        |> Output.urgent_message;
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   936
        learn 1 false;
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   937
        "Now collecting ATP proofs. This may take several hours. You can \
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   938
        \safely stop the learning process at any point."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   939
        |> Output.urgent_message;
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   940
        learn 0 true)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   941
     else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   942
       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   943
        plural_s num_facts ^ " for Isar proofs..."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   944
        |> Output.urgent_message;
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   945
        learn 0 false))
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   946
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   947
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   948
fun is_mash_enabled () = (getenv "MASH" = "yes")
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   949
fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   950
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   951
(* 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
   952
   Sledgehammer and Try. *)
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   953
val min_secs_for_learning = 15
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   954
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   955
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   956
        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
   957
  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
   958
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   959
  else if only then
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
   960
    facts
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   961
  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
   962
    []
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   963
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   964
    let
48327
568b3193e53e don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents: 48326
diff changeset
   965
      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
   966
        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
   967
           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
   968
          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
   969
            launch_thread timeout
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   970
                (fn () => (true, mash_learn_facts ctxt params prover 2 false
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   971
                                                  timeout facts))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   972
          end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   973
        else
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   974
          ()
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   975
      val fact_filter =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   976
        case fact_filter of
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   977
          SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   978
        | NONE =>
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   979
          if is_smt_prover ctxt prover then
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   980
            mepoN
50229
78f3be5e51d2 simplify code slightly
blanchet
parents: 50220
diff changeset
   981
          else if is_mash_enabled () then
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   982
            (maybe_learn ();
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   983
             if mash_can_suggest_facts ctxt then meshN else mepoN)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   984
          else
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   985
            mepoN
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   986
      val add_ths = Attrib.eval_thms ctxt add
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   987
      fun prepend_facts ths accepts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
   988
        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
   989
         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
   990
        |> take max_facts
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   991
      fun mepo () =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   992
        facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   993
                                      concl_t
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   994
              |> weight_mepo_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   995
      fun mash () =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   996
        mash_suggested_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
   997
      val mess =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   998
        [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   999
           |> (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
  1000
    in
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
  1001
      mesh_facts max_facts mess
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1002
      |> not (null add_ths) ? prepend_facts add_ths
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1003
    end
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1004
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1005
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
  1006
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
  1007
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
  1008
end;