src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Fri, 18 Jan 2013 00:18:11 +0100
changeset 50967 00d87ade2294
parent 50965 7a7d1418301e
child 50969 4179fa5c79fe
permissions -rw-r--r--
optimization -- evaluate conversion to table only once
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
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
    23
  val learn_proverN : string
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    24
  val relearn_isarN : string
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
    25
  val relearn_proverN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    26
  val fact_filters : string list
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    27
  val encode_str : string -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    28
  val encode_strs : string list -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    29
  val unencode_str : string -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    30
  val unencode_strs : string -> string list
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
    31
  val encode_features : (string * real) list -> string
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
    32
  val extract_suggestions : string -> string * string list
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    33
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    34
  structure MaSh:
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    35
  sig
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    36
    val unlearn : Proof.context -> unit
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    37
    val learn :
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    38
      Proof.context -> bool
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    39
      -> (string * string list * (string * real) list * string list) list -> unit
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    40
    val relearn :
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    41
      Proof.context -> bool -> (string * string list) list -> unit
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
    42
    val suggest :
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
    43
      Proof.context -> bool -> bool -> int
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
    44
      -> string list * (string * real) list * string list -> string list
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    45
  end
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    46
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    47
  val mash_unlearn : Proof.context -> unit
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
    48
  val nickname_of_thm : thm -> string
50967
00d87ade2294 optimization -- evaluate conversion to table only once
blanchet
parents: 50965
diff changeset
    49
  val find_suggested_facts : ('b * thm) list -> string list -> ('b * thm) list
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    50
  val mesh_facts :
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    51
    ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    52
    -> 'a list
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    53
  val theory_ord : theory * theory -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    54
  val thm_ord : thm * thm -> order
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    55
  val goal_of_thm : theory -> thm -> thm
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    56
  val run_prover_for_mash :
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    57
    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
    58
  val features_of :
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
    59
    Proof.context -> string -> theory -> stature -> term list
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
    60
    -> (string * real) list
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
    61
  val trim_dependencies : thm -> string list -> string list option
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
    62
  val isar_dependencies_of :
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
    63
    string Symtab.table * string Symtab.table -> thm -> string list
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
    64
  val prover_dependencies_of :
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
    65
    Proof.context -> params -> string -> int -> fact list
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
    66
    -> string Symtab.table * string Symtab.table -> thm
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
    67
    -> bool * string list
50608
5977de2993ac better weight functions for MePo/MaSh etc.
blanchet
parents: 50588
diff changeset
    68
  val weight_mash_facts : 'a list -> ('a * real) list
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50401
diff changeset
    69
  val find_mash_suggestions :
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
    70
    int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
    71
    -> ('b * thm) list * ('b * thm) list
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    72
  val mash_suggested_facts :
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
    73
    Proof.context -> params -> string -> int -> term list -> term -> fact list
50440
ca99c269ca3a don't have MaSh pretend it knows facts it doesn't know
blanchet
parents: 50438
diff changeset
    74
    -> fact list * fact list
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
    75
  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
    76
    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
    77
    -> unit
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    78
  val mash_learn :
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    79
    Proof.context -> params -> fact_override -> thm list -> bool -> unit
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    80
  val is_mash_enabled : unit -> bool
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
    81
  val mash_can_suggest_facts : Proof.context -> bool
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50401
diff changeset
    82
  val generous_max_facts : int -> int
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    83
  val mepo_weight : real
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    84
  val mash_weight : real
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
    85
  val relevant_facts :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    86
    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
    87
    -> 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
    88
  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
    89
  val running_learners : unit -> unit
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    90
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    91
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    92
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    93
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
    94
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    95
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    96
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    97
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    98
open Sledgehammer_Fact
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    99
open Sledgehammer_Provers
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   100
open Sledgehammer_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
   101
open Sledgehammer_MePo
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   102
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   103
val trace =
48380
d4b7c7be3116 renamed ML files
blanchet
parents: 48379
diff changeset
   104
  Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   105
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   106
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   107
val MaShN = "MaSh"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   108
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   109
val mepoN = "mepo"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   110
val mashN = "mash"
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   111
val meshN = "mesh"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   112
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   113
val fact_filters = [meshN, mepoN, mashN]
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   114
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   115
val unlearnN = "unlearn"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   116
val learn_isarN = "learn_isar"
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   117
val learn_proverN = "learn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   118
val relearn_isarN = "relearn_isar"
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   119
val relearn_proverN = "relearn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   120
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
   121
fun mash_model_dir () =
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
   122
  Path.explode "$ISABELLE_HOME_USER/mash" |> 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
   123
val mash_state_dir = mash_model_dir
50310
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   124
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
   125
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   126
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   127
(*** Low-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   128
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   129
fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   130
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   131
fun write_file banner (xs, f) path =
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   132
  (case banner of SOME s => File.write path s | NONE => ();
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   133
   xs |> chunk_list 500
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   134
      |> List.app (File.append path o space_implode "" o map f))
50319
dddcaeb92e11 robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents: 50311
diff changeset
   135
  handle IO.Io _ => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   136
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   137
fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   138
  let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   139
    val (temp_dir, serial) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   140
      if overlord then (getenv "ISABELLE_HOME_USER", "")
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   141
      else (getenv "ISABELLE_TMP", serial_string ())
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   142
    val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   143
    val err_file = temp_dir ^ "/mash_err" ^ serial
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   144
    val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   145
    val sugg_path = Path.explode sugg_file
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   146
    val cmd_file = temp_dir ^ "/mash_commands" ^ serial
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   147
    val cmd_path = Path.explode cmd_file
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   148
    val core =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   149
      "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   150
      " --numberOfPredictions " ^ string_of_int max_suggs ^
50951
e1cbaa7d5536 updated MaSh
blanchet
parents: 50874
diff changeset
   151
      (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   152
    val command =
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   153
      "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   154
      File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   155
      " >& " ^ err_file
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   156
    fun run_on () =
50750
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   157
      (Isabelle_System.bash command
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   158
       |> tap (fn _ => trace_msg ctxt (fn () =>
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   159
              case try File.read (Path.explode err_file) of
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   160
                NONE => "Done"
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   161
              | SOME "" => "Done"
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   162
              | SOME s => "Error: " ^ elide_string 1000 s));
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   163
       read_suggs (fn () => try File.read_lines sugg_path |> these))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   164
    fun clean_up () =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   165
      if overlord then ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   166
      else List.app wipe_out_file [err_file, sugg_file, cmd_file]
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   167
  in
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   168
    write_file (SOME "") ([], K "") sugg_path;
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   169
    write_file (SOME "") write_cmds cmd_path;
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   170
    trace_msg ctxt (fn () => "Running " ^ command);
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   171
    with_cleanup clean_up run_on ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   172
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   173
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   174
fun meta_char c =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   175
  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
   176
     c = #")" orelse c = #"," then
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   177
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   178
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   179
    (* fixed width, in case more digits follow *)
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   180
    "%" ^ stringN_of_int 3 (Char.ord c)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   181
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   182
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
   183
  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   184
    (case Int.fromString (String.implode [d1, d2, d3]) of
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   185
       SOME n => unmeta_chars (Char.chr n :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   186
     | NONE => "" (* error *))
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   187
  | unmeta_chars _ (#"%" :: _) = "" (* error *)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   188
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   189
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   190
val encode_str = String.translate meta_char
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   191
val encode_strs = map encode_str #> space_implode " "
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   192
val unencode_str = String.explode #> unmeta_chars []
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   193
val unencode_strs =
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   194
  space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   195
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   196
fun freshish_name () =
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   197
  Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   198
  serial_string ()
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   199
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   200
fun encode_feature (name, weight) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   201
  encode_str name ^
50389
ad0ac9112d2c simplify code now that "mash.py" supports weights
blanchet
parents: 50383
diff changeset
   202
  (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   203
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   204
val encode_features = map encode_feature #> space_implode " "
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   205
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   206
fun str_of_learn (name, parents, feats, deps) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   207
  "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   208
  encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   209
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   210
fun str_of_relearn (name, deps) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   211
  "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   212
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   213
fun str_of_query learn_hints (parents, feats, hints) =
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   214
  (if not learn_hints orelse null hints then ""
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   215
   else str_of_learn (freshish_name (), parents, feats, hints)) ^
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   216
  "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   217
  (if learn_hints orelse null hints then "" else "; " ^ encode_strs hints) ^
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   218
  "\n"
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   219
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   220
(* The weights currently returned by "mash.py" are too spaced out to make any
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   221
   sense. *)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   222
fun extract_suggestion sugg =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   223
  case space_explode "=" sugg of
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   224
    [name, weight] =>
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   225
    SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   226
  | [name] => SOME (unencode_str name (* , 1.0 *))
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   227
  | _ => NONE
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   228
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
   229
fun extract_suggestions line =
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   230
  case space_explode ":" line of
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   231
    [goal, suggs] =>
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   232
    (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   233
  | _ => ("", [])
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   234
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   235
structure MaSh =
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   236
struct
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   237
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   238
fun unlearn ctxt =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   239
  let val path = mash_model_dir () in
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   240
    trace_msg ctxt (K "MaSh unlearn");
50319
dddcaeb92e11 robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents: 50311
diff changeset
   241
    try (File.fold_dir (fn file => fn _ =>
dddcaeb92e11 robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents: 50311
diff changeset
   242
                           try File.rm (Path.append path (Path.basic file)))
dddcaeb92e11 robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents: 50311
diff changeset
   243
                       path) NONE;
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   244
    ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   245
  end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   246
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   247
fun learn _ _ [] = ()
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   248
  | learn ctxt overlord learns =
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   249
    (trace_msg ctxt (fn () => "MaSh learn " ^
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   250
         elide_string 1000 (space_implode " " (map #1 learns)));
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   251
     run_mash_tool ctxt overlord true 0 (learns, str_of_learn) (K ()))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   252
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   253
fun relearn _ _ [] = ()
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   254
  | relearn ctxt overlord relearns =
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   255
    (trace_msg ctxt (fn () => "MaSh relearn " ^
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   256
         elide_string 1000 (space_implode " " (map #1 relearns)));
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   257
     run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   258
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   259
fun suggest ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
   260
  (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   261
   run_mash_tool ctxt overlord (learn_hints andalso not (null hints))
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   262
       max_suggs ([query], str_of_query learn_hints)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   263
       (fn suggs =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   264
           case suggs () of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   265
             [] => []
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
   266
           | suggs => snd (extract_suggestions (List.last suggs)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   267
   handle List.Empty => [])
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   268
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   269
end;
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   270
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   271
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   272
(*** Middle-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   273
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   274
datatype proof_kind =
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   275
  Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   276
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   277
fun str_of_proof_kind Isar_Proof = "i"
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   278
  | str_of_proof_kind Automatic_Proof = "a"
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   279
  | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   280
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   281
fun proof_kind_of_str "i" = Isar_Proof
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   282
  | proof_kind_of_str "a" = Automatic_Proof
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   283
  | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   284
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   285
(* FIXME: Here a "Graph.update_node" function would be useful *)
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   286
fun update_access_graph_node (name, kind) =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   287
  Graph.default_node (name, Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   288
  #> kind <> Isar_Proof ? Graph.map_node name (K kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   289
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   290
fun try_graph ctxt when def f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   291
  f ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   292
  handle Graph.CYCLES (cycle :: _) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   293
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   294
              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   295
       | Graph.DUP name =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   296
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   297
              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   298
       | Graph.UNDEF name =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   299
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   300
              "Unknown fact " ^ quote name ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   301
       | exn =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   302
         if Exn.is_interrupt exn then
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   303
           reraise exn
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   304
         else
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   305
           (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   306
                "Internal error when " ^ when ^ ":\n" ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   307
                ML_Compiler.exn_message exn); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   308
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   309
fun graph_info G =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   310
  string_of_int (length (Graph.keys G)) ^ " node(s), " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   311
  string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   312
  " edge(s), " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   313
  string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   314
  string_of_int (length (Graph.maximals G)) ^ " maximal"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   315
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   316
type mash_state = {access_G : unit Graph.T, dirty : string list option}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   317
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   318
val empty_state = {access_G = Graph.empty, dirty = SOME []}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   319
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   320
local
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   321
50874
2eae85887282 adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents: 50869
diff changeset
   322
val version = "*** MaSh version 20130113a ***"
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   323
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   324
exception Too_New of unit
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   325
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   326
fun extract_node line =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   327
  case space_explode ":" line of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   328
    [head, parents] =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   329
    (case space_explode " " head of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   330
       [kind, name] =>
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   331
       SOME (unencode_str name, unencode_strs parents,
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   332
             try proof_kind_of_str kind |> the_default Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   333
     | _ => NONE)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   334
  | _ => NONE
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   335
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   336
fun load _ (state as (true, _)) = state
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   337
  | load ctxt _ =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   338
    let val path = mash_state_file () in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   339
      (true,
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   340
       case try File.read_lines path of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   341
         SOME (version' :: node_lines) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   342
         let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   343
           fun add_edge_to name parent =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   344
             Graph.default_node (parent, Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   345
             #> Graph.add_edge (parent, name)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   346
           fun add_node line =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   347
             case extract_node line of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   348
               NONE => I (* shouldn't happen *)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   349
             | SOME (name, parents, kind) =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   350
               update_access_graph_node (name, kind)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   351
               #> fold (add_edge_to name) parents
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   352
           val access_G =
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   353
             case string_ord (version', version) of
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   354
               EQUAL =>
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   355
               try_graph ctxt "loading state" Graph.empty (fn () =>
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   356
                   fold add_node node_lines Graph.empty)
50860
e32a283b8ce0 remove obsolete MaSh files
blanchet
parents: 50858
diff changeset
   357
             | LESS =>
e32a283b8ce0 remove obsolete MaSh files
blanchet
parents: 50858
diff changeset
   358
               (MaSh.unlearn ctxt; Graph.empty) (* can't parse old file *)
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   359
             | GREATER => raise Too_New ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   360
         in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   361
           trace_msg ctxt (fn () =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   362
               "Loaded fact graph (" ^ graph_info access_G ^ ")");
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   363
           {access_G = access_G, dirty = SOME []}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   364
         end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   365
       | _ => empty_state)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   366
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   367
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   368
fun save _ (state as {dirty = SOME [], ...}) = state
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   369
  | save ctxt {access_G, dirty} =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   370
    let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   371
      fun str_of_entry (name, parents, kind) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   372
        str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   373
        encode_strs parents ^ "\n"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   374
      fun append_entry (name, (kind, (parents, _))) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   375
        cons (name, Graph.Keys.dest parents, kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   376
      val (banner, entries) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   377
        case dirty of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   378
          SOME names =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   379
          (NONE, fold (append_entry o Graph.get_entry access_G) names [])
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   380
        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   381
    in
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   382
      write_file banner (entries, str_of_entry) (mash_state_file ());
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   383
      trace_msg ctxt (fn () =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   384
          "Saved fact graph (" ^ graph_info access_G ^
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   385
          (case dirty of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   386
             SOME dirty =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   387
             "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   388
           | _ => "") ^  ")");
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   389
      {access_G = access_G, dirty = SOME []}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   390
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   391
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   392
val global_state =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   393
  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   394
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   395
in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   396
50570
blanchet
parents: 50557
diff changeset
   397
fun map_state ctxt f =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   398
  Synchronized.change global_state (load ctxt ##> (f #> save ctxt))
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   399
  handle Too_New () => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   400
50570
blanchet
parents: 50557
diff changeset
   401
fun peek_state ctxt f =
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   402
  Synchronized.change_result global_state
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   403
      (perhaps (try (load ctxt)) #> `snd #>> f)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   404
50570
blanchet
parents: 50557
diff changeset
   405
fun clear_state ctxt =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   406
  Synchronized.change global_state (fn _ =>
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   407
      (MaSh.unlearn ctxt; (* also removes the state file *)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   408
       (true, empty_state)))
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   409
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   410
end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   411
50570
blanchet
parents: 50557
diff changeset
   412
val mash_unlearn = clear_state
blanchet
parents: 50557
diff changeset
   413
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   414
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   415
(*** Isabelle helpers ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   416
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   417
val local_prefix = "local" ^ Long_Name.separator
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   418
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   419
fun elided_backquote_thm threshold th =
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   420
  elide_string threshold
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   421
    (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
   422
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   423
fun nickname_of_thm 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
   424
  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
   425
    let val hint = Thm.get_name_hint th in
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   426
      (* There must be a better way to detect local facts. *)
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
   427
      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
   428
        SOME suf =>
50732
b2e7490a1b3d tweaked nicknames
blanchet
parents: 50722
diff changeset
   429
        Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^ suf ^
b2e7490a1b3d tweaked nicknames
blanchet
parents: 50722
diff changeset
   430
        Long_Name.separator ^ elided_backquote_thm 50 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
   431
      | 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
   432
    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
   433
  else
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   434
    elided_backquote_thm 200 th
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   435
50967
00d87ade2294 optimization -- evaluate conversion to table only once
blanchet
parents: 50965
diff changeset
   436
fun find_suggested_facts facts =
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   437
  let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   438
    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   439
    val tab = fold add_fact facts Symtab.empty
50967
00d87ade2294 optimization -- evaluate conversion to table only once
blanchet
parents: 50965
diff changeset
   440
  in map_filter (Symtab.lookup tab) end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   441
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   442
fun scaled_avg [] = 0
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   443
  | scaled_avg xs =
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   444
    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
   445
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   446
fun avg [] = 0.0
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   447
  | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
48313
0faafdffa662 mesh facts by taking into consideration whether a fact is known to MeSh
blanchet
parents: 48312
diff changeset
   448
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   449
fun normalize_scores _ [] = []
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   450
  | normalize_scores max_facts xs =
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   451
    let val avg = avg (map snd (take max_facts xs)) in
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   452
      map (apsnd (curry Real.* (1.0 / avg))) xs
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   453
    end
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   454
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
   455
fun mesh_facts _ max_facts [(_, (sels, unks))] =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   456
    map fst (take max_facts sels) @ take (max_facts - length sels) unks
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   457
  | mesh_facts fact_eq max_facts mess =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   458
    let
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   459
      val mess =
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   460
        mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   461
      fun score_in fact (global_weight, ((sel_len, sels), unks)) =
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   462
        let
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   463
          fun score_at j =
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   464
            case try (nth sels) j of
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   465
              SOME (_, score) => SOME (global_weight * score)
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   466
            | NONE => NONE
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   467
        in
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   468
          case find_index (curry fact_eq fact o fst) sels of
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   469
            ~1 => (case find_index (curry fact_eq fact) unks of
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   470
                     ~1 => SOME 0.0
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   471
                   | _ => NONE)
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   472
          | rank => score_at rank
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   473
        end
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   474
      fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   475
      val facts =
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   476
        fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   477
             []
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   478
    in
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   479
      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
   480
            |> map snd |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   481
    end
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   482
50874
2eae85887282 adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents: 50869
diff changeset
   483
fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
2eae85887282 adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents: 50869
diff changeset
   484
fun const_feature_of s = ("c" ^ s, 32.0 (* FUDGE *))
2eae85887282 adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents: 50869
diff changeset
   485
fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
2eae85887282 adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents: 50869
diff changeset
   486
fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
50584
4fff0898cc0e tuned weights -- keep same relative values, but use 1.0 as the least weight
blanchet
parents: 50583
diff changeset
   487
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
4fff0898cc0e tuned weights -- keep same relative values, but use 1.0 as the least weight
blanchet
parents: 50583
diff changeset
   488
fun status_feature_of status = (string_of_status status, 2.0 (* FUDGE *))
4fff0898cc0e tuned weights -- keep same relative values, but use 1.0 as the least weight
blanchet
parents: 50583
diff changeset
   489
val local_feature = ("local", 8.0 (* FUDGE *))
4fff0898cc0e tuned weights -- keep same relative values, but use 1.0 as the least weight
blanchet
parents: 50583
diff changeset
   490
val lams_feature = ("lams", 2.0 (* FUDGE *))
4fff0898cc0e tuned weights -- keep same relative values, but use 1.0 as the least weight
blanchet
parents: 50583
diff changeset
   491
val skos_feature = ("skos", 2.0 (* FUDGE *))
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   492
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   493
fun theory_ord p =
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   494
  if Theory.subthy p then
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   495
    if Theory.eq_thy p then EQUAL else LESS
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   496
  else if Theory.subthy (swap p) then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   497
    GREATER
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   498
  else case int_ord (pairself (length o Theory.ancestors_of) p) of
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   499
    EQUAL => string_ord (pairself Context.theory_name p)
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   500
  | order => order
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   501
50382
blanchet
parents: 50359
diff changeset
   502
fun thm_ord p =
blanchet
parents: 50359
diff changeset
   503
  case theory_ord (pairself theory_of_thm p) of
50359
da395f0e7dea tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents: 50357
diff changeset
   504
    EQUAL =>
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   505
    let val q = pairself nickname_of_thm p in
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   506
      (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   507
      case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   508
        EQUAL => string_ord q
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   509
      | ord => ord
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   510
    end
50359
da395f0e7dea tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents: 50357
diff changeset
   511
  | ord => ord
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   512
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   513
val freezeT = Type.legacy_freeze_type
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   514
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   515
fun freeze (t $ u) = freeze t $ freeze u
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   516
  | 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
   517
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   518
  | freeze (Const (s, T)) = Const (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   519
  | freeze (Free (s, T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   520
  | freeze t = t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   521
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   522
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
   523
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   524
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
   525
  let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   526
    val problem =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   527
      {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
   528
       facts = facts |> map (apfst (apfst (fn name => name ())))
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   529
                     |> map Untranslated_Fact}
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   530
  in
50668
blanchet
parents: 50633
diff changeset
   531
    get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
blanchet
parents: 50633
diff changeset
   532
                               problem
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   533
  end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   534
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   535
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   536
48398
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   537
val logical_consts =
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   538
  [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
b86450f5b5cb clean up interesting constants a bit
blanchet
parents: 48396
diff changeset
   539
50585
306c7b807e13 contain exponential explosion of term patterns
blanchet
parents: 50584
diff changeset
   540
val max_pattern_breadth = 10
306c7b807e13 contain exponential explosion of term patterns
blanchet
parents: 50584
diff changeset
   541
50841
087e3c531e86 honor filtering out of arguments for built-in constants (e.g. representation of numerals)
blanchet
parents: 50840
diff changeset
   542
fun term_features_of ctxt prover thy_name term_max_depth type_max_depth ts =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   543
  let
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   544
    val thy = Proof_Context.theory_of ctxt
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   545
    fun is_built_in (x as (s, _)) args =
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   546
      if member (op =) logical_consts s then (true, args)
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   547
      else is_built_in_const_for_prover ctxt prover x args
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   548
    val fixes = map snd (Variable.dest_fixes ctxt)
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   549
    val classes = Sign.classes_of thy
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   550
    fun add_classes @{sort type} = I
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   551
      | add_classes S =
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   552
        fold (`(Sorts.super_classes classes)
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   553
              #> swap #> op ::
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   554
              #> subtract (op =) @{sort type}
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   555
              #> map class_feature_of
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   556
              #> union (op = o pairself fst)) S
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   557
    fun do_add_type (Type (s, Ts)) =
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   558
        (not (member (op =) bad_types s)
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   559
         ? insert (op = o pairself fst) (type_feature_of s))
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   560
        #> fold do_add_type Ts
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   561
      | do_add_type (TFree (_, S)) = add_classes S
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   562
      | do_add_type (TVar (_, S)) = add_classes S
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   563
    fun add_type T = type_max_depth >= 0 ? do_add_type T
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   564
    fun patternify_term _ 0 _ = []
50339
d8dae91f3107 MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents: 50338
diff changeset
   565
      | patternify_term args _ (Const (x as (s, _))) =
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   566
        if fst (is_built_in x args) then [] else [s]
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   567
      | patternify_term _ depth (Free (s, _)) =
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   568
        if depth = term_max_depth andalso member (op =) fixes s then
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   569
          [thy_name ^ Long_Name.separator ^ s]
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   570
        else
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   571
          []
50339
d8dae91f3107 MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents: 50338
diff changeset
   572
      | patternify_term args depth (t $ u) =
d8dae91f3107 MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents: 50338
diff changeset
   573
        let
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   574
          val ps =
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   575
            take max_pattern_breadth (patternify_term (u :: args) depth t)
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   576
          val qs =
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   577
            take max_pattern_breadth ("" :: patternify_term [] (depth - 1) u)
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   578
        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   579
      | patternify_term _ _ _ = []
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   580
    fun add_term_pattern feature_of =
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   581
      union (op = o pairself fst) o map feature_of oo patternify_term []
50583
681edd111e9b really honor pattern depth, and use 2 by default
blanchet
parents: 50570
diff changeset
   582
    fun add_term_patterns _ 0 _ = I
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   583
      | add_term_patterns feature_of depth t =
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   584
        add_term_pattern feature_of depth t
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   585
        #> add_term_patterns feature_of (depth - 1) t
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   586
    fun add_term feature_of = add_term_patterns feature_of term_max_depth
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   587
    fun add_patterns t =
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   588
      case strip_comb t of
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   589
        (Const (x as (_, T)), args) =>
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   590
        let val (built_in, args) = is_built_in x args in
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   591
          (not built_in ? add_term const_feature_of t)
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   592
          #> add_type T
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   593
          #> fold add_patterns args
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   594
        end
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   595
      | (head, args) =>
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   596
        (case head of
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   597
           Const (_, T) => add_term const_feature_of t #> add_type T
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   598
         | Free (_, T) => add_term free_feature_of t #> add_type T
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   599
         | Var (_, T) => add_type T
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   600
         | Abs (_, T, body) => add_type T #> add_patterns body
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   601
         | _ => I)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   602
        #> fold add_patterns args
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   603
  in [] |> fold add_patterns ts end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   604
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   605
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
   606
50583
681edd111e9b really honor pattern depth, and use 2 by default
blanchet
parents: 50570
diff changeset
   607
val term_max_depth = 2
681edd111e9b really honor pattern depth, and use 2 by default
blanchet
parents: 50570
diff changeset
   608
val type_max_depth = 2
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   609
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   610
(* TODO: Generate type classes for types? *)
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   611
fun features_of ctxt prover thy (scope, status) ts =
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   612
  let val thy_name = Context.theory_name thy in
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   613
    thy_feature_of thy_name ::
50841
087e3c531e86 honor filtering out of arguments for built-in constants (e.g. representation of numerals)
blanchet
parents: 50840
diff changeset
   614
    term_features_of ctxt prover thy_name term_max_depth type_max_depth ts
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   615
    |> status <> General ? cons (status_feature_of status)
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   616
    |> scope <> Global ? cons local_feature
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   617
    |> exists (not o is_lambda_free) ts ? cons lams_feature
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   618
    |> exists (exists_Const is_exists) ts ? cons skos_feature
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   619
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   620
50434
960a3429615c more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents: 50412
diff changeset
   621
(* Too many dependencies is a sign that a decision procedure is at work. There
960a3429615c more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents: 50412
diff changeset
   622
   isn't much to learn from such proofs. *)
960a3429615c more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
blanchet
parents: 50412
diff changeset
   623
val max_dependencies = 20
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   624
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   625
val prover_dependency_default_max_facts = 50
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   626
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   627
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   628
val typedef_dep = nickname_of_thm @{thm CollectI}
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   629
(* Mysterious parts of the class machinery create lots of proofs that refer
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   630
   exclusively to "someI_e" (and to some internal constructions). *)
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   631
val class_some_dep = nickname_of_thm @{thm someI_ex}
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   632
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   633
val fundef_ths =
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   634
  @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   635
         fundef_default_value}
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   636
  |> map nickname_of_thm
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   637
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   638
(* "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
   639
val typedef_ths =
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   640
  @{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
   641
         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
   642
         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
   643
         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
   644
         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
   645
         type_definition.Abs_image}
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   646
  |> map nickname_of_thm
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   647
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   648
fun is_size_def [dep] th =
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   649
    (case first_field ".recs" dep of
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   650
       SOME (pref, _) =>
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   651
       (case first_field ".size" (nickname_of_thm th) of
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   652
          SOME (pref', _) => pref = pref'
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   653
        | NONE => false)
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   654
     | NONE => false)
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   655
  | is_size_def _ _ = false
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   656
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   657
fun trim_dependencies th deps =
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   658
  if length deps > max_dependencies then NONE else SOME deps
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   659
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   660
fun isar_dependencies_of name_tabs th =
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   661
  let
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   662
    val deps = thms_in_proof (SOME name_tabs) th
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   663
  in
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   664
    if deps = [typedef_dep] orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   665
       deps = [class_some_dep] orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   666
       exists (member (op =) fundef_ths) deps orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   667
       exists (member (op =) typedef_ths) deps orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   668
       is_size_def deps th then
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   669
      []
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   670
    else
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   671
      deps
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   672
  end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   673
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   674
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
   675
                           auto_level facts name_tabs th =
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
   676
  case isar_dependencies_of name_tabs th of
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   677
    [] => (false, [])
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   678
  | isar_deps =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   679
    let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   680
      val thy = Proof_Context.theory_of ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   681
      val goal = goal_of_thm thy th
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   682
      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
   683
      val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   684
      fun nickify ((_, stature), th) =
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   685
        ((fn () => nickname_of_thm th, stature), th)
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   686
      fun is_dep dep (_, th) = nickname_of_thm th = dep
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   687
      fun add_isar_dep facts dep accum =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   688
        if exists (is_dep dep) accum then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   689
          accum
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   690
        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
   691
          SOME ((name, status), th) => accum @ [((name, status), th)]
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   692
        | NONE => accum (* shouldn't happen *)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   693
      val facts =
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   694
        facts
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   695
        |> mepo_suggested_facts ctxt params prover
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   696
               (max_facts |> the_default prover_dependency_default_max_facts)
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   697
               NONE hyp_ts concl_t
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   698
        |> fold (add_isar_dep facts) isar_deps
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   699
        |> map nickify
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   700
    in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   701
      if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   702
        let val num_facts = length facts in
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   703
          "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   704
          " 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
   705
          "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   706
          |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   707
        end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   708
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   709
        ();
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   710
      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
   711
        {outcome = NONE, used_facts, ...} =>
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   712
        (if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   713
           let val num_facts = length used_facts in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   714
             "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
   715
             plural_s num_facts ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   716
             |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   717
           end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   718
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   719
           ();
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   720
         (true, map fst used_facts))
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   721
      | _ => (false, isar_deps)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   722
    end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   723
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   724
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   725
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   726
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   727
fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   728
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   729
fun maximal_in_graph access_G facts =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   730
  let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   731
    val facts = [] |> fold (cons o nickname_of_thm o snd) facts
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   732
    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   733
    fun insert_new seen name =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   734
      not (Symtab.defined seen name) ? insert (op =) name
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   735
    fun find_maxes _ (maxs, []) = map snd maxs
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   736
      | find_maxes seen (maxs, new :: news) =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   737
        find_maxes
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   738
            (seen |> num_keys (Graph.imm_succs access_G new) > 1
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   739
                     ? Symtab.default (new, ()))
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   740
            (if Symtab.defined tab new then
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   741
               let
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   742
                 val newp = Graph.all_preds access_G [new]
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   743
                 fun is_ancestor x yp = member (op =) yp x
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   744
                 val maxs =
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   745
                   maxs |> filter (fn (_, max) => not (is_ancestor max newp))
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   746
               in
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   747
                 if exists (is_ancestor new o fst) maxs then
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   748
                   (maxs, news)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   749
                 else
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   750
                   ((newp, new)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   751
                    :: filter_out (fn (_, max) => is_ancestor max newp) maxs,
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   752
                    news)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   753
               end
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   754
             else
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   755
               (maxs, Graph.Keys.fold (insert_new seen)
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   756
                                      (Graph.imm_preds access_G new) news))
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   757
  in find_maxes Symtab.empty ([], Graph.maximals access_G) end
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   758
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   759
fun is_fact_in_graph access_G get_th fact =
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   760
  can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
48320
891a24a48155 improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
blanchet
parents: 48319
diff changeset
   761
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   762
val weight_raw_mash_facts = weight_mepo_facts
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   763
val weight_mash_facts = weight_raw_mash_facts
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   764
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   765
(* FUDGE *)
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   766
fun weight_of_proximity_fact rank =
50398
78c7b52dbadb tweaked MaSh proximity
blanchet
parents: 50397
diff changeset
   767
  Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   768
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   769
fun weight_proximity_facts facts =
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   770
  facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
50382
blanchet
parents: 50359
diff changeset
   771
50440
ca99c269ca3a don't have MaSh pretend it knows facts it doesn't know
blanchet
parents: 50438
diff changeset
   772
val max_proximity_facts = 100
ca99c269ca3a don't have MaSh pretend it knows facts it doesn't know
blanchet
parents: 50438
diff changeset
   773
50952
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   774
fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   775
  | find_mash_suggestions max_facts suggs facts chained raw_unknown =
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   776
    let
50967
00d87ade2294 optimization -- evaluate conversion to table only once
blanchet
parents: 50965
diff changeset
   777
      val raw_mash = find_suggested_facts facts suggs
50952
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   778
      val unknown_chained =
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   779
        inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   780
      val proximity =
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   781
        facts |> sort (thm_ord o pairself snd o swap)
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   782
              |> take max_proximity_facts
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   783
      val mess =
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   784
        [(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   785
         (0.08 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)),
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   786
         (0.02 (* FUDGE *), (weight_proximity_facts proximity, []))]
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   787
      val unknown =
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   788
        raw_unknown
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   789
        |> fold (subtract (Thm.eq_thm_prop o pairself snd))
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   790
                [unknown_chained, proximity]
3fd83a0cc4bd evaluate more cases (cf. paper)
blanchet
parents: 50951
diff changeset
   791
    in (mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess, unknown) end
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50401
diff changeset
   792
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   793
fun mash_suggested_facts ctxt ({overlord, learn, ...} : params) prover max_facts
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   794
                         hyp_ts concl_t facts =
48301
e5c5037a3104 started implementing MaSh client-side I/O
blanchet
parents: 48299
diff changeset
   795
  let
48302
6cf5e58f1185 more implementation work on MaSh
blanchet
parents: 48301
diff changeset
   796
    val thy = Proof_Context.theory_of ctxt
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   797
    val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   798
    val (access_G, suggs) =
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   799
      peek_state ctxt (fn {access_G, ...} =>
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   800
          if Graph.is_empty access_G then
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   801
            (access_G, [])
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   802
          else
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   803
            let
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   804
              val parents = maximal_in_graph access_G facts
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   805
              val feats =
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   806
                features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   807
              val hints =
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   808
                chained |> filter (is_fact_in_graph access_G snd)
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   809
                        |> map (nickname_of_thm o snd)
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   810
            in
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   811
              (access_G, MaSh.suggest ctxt overlord learn max_facts
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   812
                                      (parents, feats, hints))
48434
aaaec69db3db ensure all calls to "mash" program are synchronous
blanchet
parents: 48433
diff changeset
   813
            end)
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   814
    val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50401
diff changeset
   815
  in find_mash_suggestions max_facts suggs facts chained unknown end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   816
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   817
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
   818
  let
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   819
    fun maybe_learn_from from (accum as (parents, graph)) =
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   820
      try_graph ctxt "updating graph" accum (fn () =>
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
   821
          (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
   822
    val graph = graph |> Graph.default_node (name, Isar_Proof)
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   823
    val (parents, graph) = ([], graph) |> fold maybe_learn_from parents
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   824
    val (deps, _) = ([], graph) |> fold maybe_learn_from deps
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   825
  in ((name, parents, feats, deps) :: learns, graph) end
48306
e699f754d9f7 better zipping of MaSh facts
blanchet
parents: 48305
diff changeset
   826
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   827
fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   828
  let
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   829
    fun maybe_relearn_from from (accum as (parents, graph)) =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   830
      try_graph ctxt "updating graph" accum (fn () =>
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   831
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   832
    val graph = graph |> update_access_graph_node (name, Automatic_Proof)
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   833
    val (deps, _) = ([], graph) |> fold maybe_relearn_from deps
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   834
  in ((name, deps) :: relearns, graph) end
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
   835
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   836
fun flop_wrt_access_graph name =
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   837
  update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop)
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   838
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
   839
val learn_timeout_slack = 2.0
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   840
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
   841
fun launch_thread timeout task =
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   842
  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
   843
    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
   844
    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
   845
    val death_time = Time.+ (birth_time, hard_timeout)
48442
3c9890c19e90 cap the number of facts returned by MaSh
blanchet
parents: 48441
diff changeset
   846
    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
   847
  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
   848
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
   849
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
   850
                     used_ths =
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   851
  launch_thread (timeout |> the_default one_day) (fn () =>
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   852
      let
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   853
        val thy = Proof_Context.theory_of ctxt
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   854
        val name = freshish_name ()
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   855
        val feats = features_of ctxt prover thy (Local, General) [t]
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   856
      in
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   857
        peek_state ctxt (fn {access_G, ...} =>
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   858
            let
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   859
              val parents = maximal_in_graph access_G facts
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   860
              val deps =
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   861
                used_ths |> filter (is_fact_in_graph access_G I)
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   862
                         |> map nickname_of_thm
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   863
            in
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   864
              MaSh.learn ctxt overlord [(name, parents, feats, deps)]
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   865
            end);
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   866
        (true, "")
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   867
      end)
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
   868
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50440
diff changeset
   869
fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   870
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   871
val commit_timeout = seconds 30.0
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   872
50485
3c6ac2da2f45 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents: 50484
diff changeset
   873
(* The timeout is understood in a very relaxed fashion. *)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   874
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   875
                     auto_level run_prover learn_timeout facts =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   876
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   877
    val timer = Timer.startRealTimer ()
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   878
    fun next_commit_time () =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   879
      Time.+ (Timer.checkRealTimer timer, commit_timeout)
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   880
    val {access_G, ...} = peek_state ctxt I
50485
3c6ac2da2f45 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents: 50484
diff changeset
   881
    val facts = facts |> sort (thm_ord o pairself snd)
48400
f08425165cca minimal maxes + tuning
blanchet
parents: 48399
diff changeset
   882
    val (old_facts, new_facts) =
50861
fa4253914e98 honor unknown chained in MaSh and a few other tweaks
blanchet
parents: 50860
diff changeset
   883
      facts |> List.partition (is_fact_in_graph access_G snd)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   884
  in
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   885
    if null new_facts andalso (not run_prover orelse null old_facts) then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   886
      if auto_level < 2 then
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   887
        "No new " ^ (if run_prover then "automatic" else "Isar") ^
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   888
        " proofs to learn." ^
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   889
        (if auto_level = 0 andalso not run_prover then
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   890
           "\n\nHint: Try " ^ sendback learn_proverN ^
50751
d3111134973d tuned message
blanchet
parents: 50750
diff changeset
   891
           " to learn from an automatic prover."
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   892
         else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   893
           "")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   894
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   895
        ""
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   896
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   897
      let
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
   898
        val name_tabs = build_name_tables nickname_of_thm facts
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   899
        fun deps_of status th =
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   900
          if status = Non_Rec_Def orelse status = Rec_Def then
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   901
            SOME []
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   902
          else if run_prover then
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
   903
            prover_dependencies_of ctxt params prover auto_level facts name_tabs
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   904
                                   th
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   905
            |> (fn (false, _) => NONE
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   906
                 | (true, deps) => trim_dependencies th deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   907
          else
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
   908
            isar_dependencies_of name_tabs th
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   909
            |> trim_dependencies th
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   910
        fun do_commit [] [] [] state = state
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   911
          | do_commit learns relearns flops {access_G, dirty} =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   912
            let
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   913
              val was_empty = Graph.is_empty access_G
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   914
              val (learns, access_G) =
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   915
                ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   916
              val (relearns, access_G) =
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   917
                ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   918
              val access_G = access_G |> fold flop_wrt_access_graph flops
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   919
              val dirty =
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   920
                case (was_empty, dirty, relearns) of
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   921
                  (false, SOME names, []) => SOME (map #1 learns @ names)
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
   922
                | _ => NONE
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   923
            in
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   924
              MaSh.learn ctxt overlord (rev learns);
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   925
              MaSh.relearn ctxt overlord relearns;
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   926
              {access_G = access_G, dirty = dirty}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   927
            end
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   928
        fun commit last learns relearns flops =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   929
          (if debug andalso auto_level = 0 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   930
             Output.urgent_message "Committing..."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   931
           else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   932
             ();
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   933
           map_state ctxt (do_commit (rev learns) relearns flops);
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   934
           if not last andalso auto_level = 0 then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   935
             let val num_proofs = length learns + length relearns in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   936
               "Learned " ^ string_of_int num_proofs ^ " " ^
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   937
               (if run_prover then "automatic" else "Isar") ^ " proof" ^
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   938
               plural_s num_proofs ^ " in the last " ^
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   939
               string_from_time commit_timeout ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   940
               |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   941
             end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   942
           else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   943
             ())
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   944
        fun learn_new_fact _ (accum as (_, (_, _, _, true))) = accum
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   945
          | learn_new_fact ((_, stature as (_, status)), th)
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   946
                           (learns, (parents, n, next_commit, _)) =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   947
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   948
              val name = nickname_of_thm th
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
   949
              val feats =
48385
2779dea0b1e0 added locality as a MaSh feature
blanchet
parents: 48384
diff changeset
   950
                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
   951
              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
   952
              val n = n |> not (null deps) ? Integer.add 1
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   953
              val learns = (name, parents, feats, deps) :: learns
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   954
              val (learns, next_commit) =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   955
                if Time.> (Timer.checkRealTimer timer, next_commit) then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   956
                  (commit false learns [] []; ([], next_commit_time ()))
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   957
                else
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   958
                  (learns, next_commit)
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   959
              val timed_out =
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   960
                case learn_timeout of
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   961
                  SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   962
                | NONE => false
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   963
            in (learns, ([name], n, next_commit, timed_out)) end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   964
        val n =
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   965
          if null new_facts then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   966
            0
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   967
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   968
            let
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   969
              val last_th = new_facts |> List.last |> snd
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   970
              (* crude approximation *)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   971
              val ancestors =
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   972
                old_facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   973
                |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER)
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   974
              val parents = maximal_in_graph access_G ancestors
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   975
              val (learns, (_, n, _, _)) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   976
                ([], (parents, 0, next_commit_time (), false))
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   977
                |> fold learn_new_fact new_facts
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   978
            in commit true learns [] []; n end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   979
        fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   980
          | relearn_old_fact ((_, (_, status)), th)
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   981
                             ((relearns, flops), (n, next_commit, _)) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   982
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   983
              val name = nickname_of_thm th
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   984
              val (n, relearns, flops) =
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
   985
                case deps_of status th of
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   986
                  SOME deps => (n + 1, (name, deps) :: relearns, flops)
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   987
                | NONE => (n, relearns, name :: flops)
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   988
              val (relearns, flops, next_commit) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   989
                if Time.> (Timer.checkRealTimer timer, next_commit) then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   990
                  (commit false [] relearns flops;
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   991
                   ([], [], next_commit_time ()))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   992
                else
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   993
                  (relearns, flops, next_commit)
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   994
              val timed_out =
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   995
                case learn_timeout of
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   996
                  SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
   997
                | NONE => false
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   998
            in ((relearns, flops), (n, next_commit, timed_out)) end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   999
        val n =
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1000
          if not run_prover orelse null old_facts then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1001
            n
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1002
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1003
            let
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
  1004
              val max_isar = 1000 * max_dependencies
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1005
              fun kind_of_proof th =
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1006
                try (Graph.get_node access_G) (nickname_of_thm th)
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1007
                |> the_default Isar_Proof
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
  1008
              fun priority_of (_, th) =
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
  1009
                random_range 0 max_isar
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1010
                + (case kind_of_proof th of
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1011
                     Isar_Proof => 0
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1012
                   | Automatic_Proof => 2 * max_isar
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1013
                   | Isar_Proof_wegen_Prover_Flop => max_isar)
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
  1014
                - 500 * length (isar_dependencies_of name_tabs th)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1015
              val old_facts =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
  1016
                old_facts |> map (`priority_of)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1017
                          |> sort (int_ord o pairself fst)
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1018
                          |> map snd
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1019
              val ((relearns, flops), (n, _, _)) =
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1020
                (([], []), (n, next_commit_time (), false))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1021
                |> fold relearn_old_fact old_facts
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1022
            in commit true [] relearns flops; n end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1023
      in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1024
        if verbose orelse auto_level < 2 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1025
          "Learned " ^ string_of_int n ^ " nontrivial " ^
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1026
          (if run_prover then "automatic" 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
  1027
          (if verbose then
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1028
             " 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
  1029
           else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1030
             "") ^ "."
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1031
        else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1032
          ""
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1033
      end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1034
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1035
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1036
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1037
               run_prover =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1038
  let
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
  1039
    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
  1040
    val ctxt = ctxt |> Config.put instantiate_inducts false
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
  1041
    val facts =
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
  1042
      nearly_all_facts ctxt false fact_override Symtab.empty css chained []
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
  1043
                       @{prop True}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1044
    val num_facts = length facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1045
    val prover = hd provers
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1046
    fun learn auto_level run_prover =
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1047
      mash_learn_facts ctxt params prover auto_level run_prover NONE facts
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1048
      |> Output.urgent_message
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1049
  in
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1050
    if run_prover then
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1051
      ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1052
       plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1053
       (case timeout of
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1054
          SOME timeout => " timeout: " ^ string_from_time timeout
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1055
        | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1056
       |> Output.urgent_message;
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1057
       learn 1 false;
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1058
       "Now collecting automatic proofs. This may take several hours. You can \
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1059
       \safely stop the learning process at any point."
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1060
       |> Output.urgent_message;
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1061
       learn 0 true)
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1062
    else
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1063
      ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1064
       plural_s num_facts ^ " for Isar proofs..."
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1065
       |> Output.urgent_message;
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1066
       learn 0 false)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1067
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
  1068
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
  1069
fun is_mash_enabled () = (getenv "MASH" = "yes")
50570
blanchet
parents: 50557
diff changeset
  1070
fun mash_can_suggest_facts ctxt =
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
  1071
  not (Graph.is_empty (#access_G (peek_state ctxt I)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
  1072
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
  1073
(* Generate more suggestions than requested, because some might be thrown out
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
  1074
   later for various reasons. *)
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
  1075
fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
  1076
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1077
val mepo_weight = 0.5
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1078
val mash_weight = 0.5
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1079
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1080
(* 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
  1081
   Sledgehammer and Try. *)
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1082
val min_secs_for_learning = 15
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1083
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
  1084
fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
  1085
        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
  1086
  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
  1087
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1088
  else if only then
48289
6b65f1ad0e4b systematize lazy names in relevance filter
blanchet
parents: 48288
diff changeset
  1089
    facts
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
  1090
  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
  1091
    []
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1092
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1093
    let
48327
568b3193e53e don't include hidden facts in relevance filter + tweak MaSh learning
blanchet
parents: 48326
diff changeset
  1094
      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
  1095
        if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
50557
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1096
           (timeout = NONE orelse
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1097
            Time.toSeconds (the timeout) >= min_secs_for_learning) then
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1098
          let
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1099
            val timeout = Option.map (time_mult learn_timeout_slack) timeout
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1100
          in
31313171deb5 thread no timeout properly
blanchet
parents: 50485
diff changeset
  1101
            launch_thread (timeout |> the_default one_day)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1102
                (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
  1103
                                                  timeout facts))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1104
          end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1105
        else
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1106
          ()
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1107
      val fact_filter =
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1108
        case fact_filter of
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
  1109
          SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1110
        | NONE =>
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1111
          if is_smt_prover ctxt prover then
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1112
            mepoN
50229
78f3be5e51d2 simplify code slightly
blanchet
parents: 50220
diff changeset
  1113
          else if is_mash_enabled () then
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1114
            (maybe_learn ();
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1115
             if mash_can_suggest_facts ctxt then meshN else mepoN)
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1116
          else
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1117
            mepoN
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1118
      val add_ths = Attrib.eval_thms ctxt add
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
  1119
      fun prepend_facts ths accepts =
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1120
        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
  1121
         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
  1122
        |> take max_facts
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
  1123
      fun mepo () =
50382
blanchet
parents: 50359
diff changeset
  1124
        mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
blanchet
parents: 50359
diff changeset
  1125
                             facts
blanchet
parents: 50359
diff changeset
  1126
        |> weight_mepo_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1127
      fun mash () =
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
  1128
        mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
  1129
            hyp_ts concl_t facts
50440
ca99c269ca3a don't have MaSh pretend it know