src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Thu, 17 Oct 2013 20:20:53 +0200
changeset 54140 564b8adb0952
parent 54131 18b23d787062
child 54141 f57f8e7a879f
permissions -rw-r--r--
clarified message
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
51004
5f2788c38127 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents: 51003
diff changeset
    10
  type raw_fact = Sledgehammer_Fact.raw_fact
48296
e7f01b7e244e gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents: 48293
diff changeset
    11
  type fact = Sledgehammer_Fact.fact
e7f01b7e244e gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents: 48293
diff changeset
    12
  type fact_override = Sledgehammer_Fact.fact_override
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    13
  type params = Sledgehammer_Provers.params
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
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
    17
  val MePoN : string
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    18
  val MaShN : string
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
    19
  val MeShN : string
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    20
  val mepoN : string
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    21
  val mashN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    22
  val meshN : string
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    23
  val unlearnN : string
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    24
  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
    25
  val learn_proverN : string
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    26
  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
    27
  val relearn_proverN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    28
  val fact_filters : string list
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    29
  val encode_str : string -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    30
  val encode_strs : string list -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    31
  val unencode_str : string -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    32
  val unencode_strs : string -> string list
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
    33
  val encode_features : (string * real) list -> string
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
    34
  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
    35
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    36
  structure MaSh:
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    37
  sig
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
    38
    val unlearn : Proof.context -> bool -> unit
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    39
    val learn :
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
    40
      Proof.context -> bool -> bool
53121
5f727525b1ac only generate feature weights for queries -- they're not used elsewhere
blanchet
parents: 53118
diff changeset
    41
      -> (string * string list * string list * string list) list -> unit
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    42
    val relearn :
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
    43
      Proof.context -> bool -> bool -> (string * string list) list -> unit
50969
blanchet
parents: 50967
diff changeset
    44
    val query :
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
    45
      Proof.context -> bool -> int
53121
5f727525b1ac only generate feature weights for queries -- they're not used elsewhere
blanchet
parents: 53118
diff changeset
    46
      -> (string * string list * string list * string list) list
53094
e33d77814a92 allow MaSh query to do some learning as well
blanchet
parents: 53090
diff changeset
    47
         * string list * string list * (string * real) list
e33d77814a92 allow MaSh query to do some learning as well
blanchet
parents: 53090
diff changeset
    48
      -> string list
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    49
  end
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    50
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
    51
  val mash_unlearn : Proof.context -> params -> unit
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
    52
  val is_mash_enabled : unit -> bool
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
    53
  val nickname_of_thm : thm -> string
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
    54
  val find_suggested_facts :
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
    55
    Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    56
  val mesh_facts :
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    57
    ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    58
    -> 'a list
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
    59
  val crude_thm_ord : thm * thm -> order
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
    60
  val thm_less : thm * thm -> bool
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    61
  val goal_of_thm : theory -> thm -> thm
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
    62
  val run_prover_for_mash :
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
    63
    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
    64
  val features_of :
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
    65
    Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
    66
    (string * real) list
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
    67
  val trim_dependencies : string list -> string list option
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
    68
  val isar_dependencies_of :
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
    69
    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
    70
  val prover_dependencies_of :
51004
5f2788c38127 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents: 51003
diff changeset
    71
    Proof.context -> params -> string -> int -> raw_fact list
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
    72
    -> string Symtab.table * string Symtab.table -> thm
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
    73
    -> bool * string list
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
    74
  val attach_parents_to_facts :
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
    75
    ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    76
  val num_extra_feature_facts : int
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
    77
  val extra_feature_factor : real
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    78
  val weight_facts_smoothly : 'a list -> ('a * real) list
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    79
  val weight_facts_steeply : 'a list -> ('a * real) list
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50401
diff changeset
    80
  val find_mash_suggestions :
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
    81
    Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
    82
    -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
53127
60801776d8af weight MaSh constants by frequency
blanchet
parents: 53121
diff changeset
    83
  val add_const_counts : term -> int Symtab.table -> int Symtab.table
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
    84
  val mash_suggested_facts :
51004
5f2788c38127 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents: 51003
diff changeset
    85
    Proof.context -> params -> string -> int -> term list -> term
5f2788c38127 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents: 51003
diff changeset
    86
    -> raw_fact list -> fact list * fact list
48383
df75b2d7e26a learn command in MaSh
blanchet
parents: 48382
diff changeset
    87
  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
    88
    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
    89
    -> unit
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    90
  val mash_learn :
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
    91
    Proof.context -> params -> fact_override -> thm list -> bool -> unit
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
    92
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
    93
  val mash_can_suggest_facts : Proof.context -> bool -> bool
50412
e83ab94e3e6e use proper entry point for MaSh in test driver
blanchet
parents: 50401
diff changeset
    94
  val generous_max_facts : int -> int
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    95
  val mepo_weight : real
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    96
  val mash_weight : real
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
    97
  val relevant_facts :
48292
7fcee834c7f5 more code rationalization in relevance filter
blanchet
parents: 48289
diff changeset
    98
    Proof.context -> params -> string -> int -> fact_override -> term list
51010
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
    99
    -> term -> raw_fact list -> (string * fact list) list
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   100
  val kill_learners : Proof.context -> params -> unit
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   101
  val running_learners : unit -> unit
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
   102
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
   103
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
   104
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
   105
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
   106
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   107
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   108
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   109
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   110
open Sledgehammer_Fact
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   111
open Sledgehammer_Provers
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
   112
open Sledgehammer_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
   113
open Sledgehammer_MePo
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   114
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   115
val trace =
48380
d4b7c7be3116 renamed ML files
blanchet
parents: 48379
diff changeset
   116
  Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
51032
69da236d7838 added option to use SNoW as machine learning algo
blanchet
parents: 51029
diff changeset
   117
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   118
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   119
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   120
val MePoN = "MePo"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   121
val MaShN = "MaSh"
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   122
val MeShN = "MeSh"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   123
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   124
val mepoN = "mepo"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   125
val mashN = "mash"
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   126
val meshN = "mesh"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   127
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   128
val fact_filters = [meshN, mepoN, mashN]
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   129
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   130
val unlearnN = "unlearn"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   131
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
   132
val learn_proverN = "learn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   133
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
   134
val relearn_proverN = "relearn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   135
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
   136
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
   137
  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
   138
val mash_state_dir = mash_model_dir
50310
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   139
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
   140
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   141
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   142
(*** Low-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   143
53117
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   144
val save_models_arg = "--saveModels"
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   145
val shutdown_server_arg = "--shutdownServer"
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   146
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   147
fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   148
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   149
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
   150
  (case banner of SOME s => File.write path s | NONE => ();
53094
e33d77814a92 allow MaSh query to do some learning as well
blanchet
parents: 53090
diff changeset
   151
   xs |> chunk_list 500 |> List.app (File.append path o 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
   152
  handle IO.Io _ => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   153
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   154
fun run_mash_tool ctxt overlord extra_args background write_cmds read_suggs =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   155
  let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   156
    val (temp_dir, serial) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   157
      if overlord then (getenv "ISABELLE_HOME_USER", "")
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   158
      else (getenv "ISABELLE_TMP", serial_string ())
53129
f92b24047fc7 improved support for MaSh server
blanchet
parents: 53128
diff changeset
   159
    val log_file = temp_dir ^ "/mash_log" ^ serial
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   160
    val err_file = temp_dir ^ "/mash_err" ^ serial
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   161
    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
   162
    val sugg_path = Path.explode sugg_file
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   163
    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
   164
    val cmd_path = Path.explode cmd_file
51001
461fdbbdb912 adapted to new MaSh interface
blanchet
parents: 50985
diff changeset
   165
    val model_dir = File.shell_path (mash_model_dir ())
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   166
    val command =
53556
347f743e8336 invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents: 53201
diff changeset
   167
      "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
53790
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   168
      \PYTHONDONTWRITEBYTECODE=y ./mash.py\
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   169
      \ --quiet\
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   170
      \ --port=$MASH_PORT\
53556
347f743e8336 invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents: 53201
diff changeset
   171
      \ --outputDir " ^ model_dir ^
347f743e8336 invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents: 53201
diff changeset
   172
      " --modelFile=" ^ model_dir ^ "/model.pickle\
347f743e8336 invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
blanchet
parents: 53201
diff changeset
   173
      \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
53790
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   174
      \ --log " ^ log_file ^
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   175
      " --inputFile " ^ cmd_file ^
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   176
      " --predictions " ^ sugg_file ^
53117
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   177
      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   178
      " >& " ^ err_file ^
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   179
      (if background then " &" else "")
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   180
    fun run_on () =
50750
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   181
      (Isabelle_System.bash command
54100
6fefbaeccb63 more prominent MaSh errors
blanchet
parents: 54096
diff changeset
   182
       |> tap (fn _ =>
6fefbaeccb63 more prominent MaSh errors
blanchet
parents: 54096
diff changeset
   183
            case try File.read (Path.explode err_file) |> the_default "" of
6fefbaeccb63 more prominent MaSh errors
blanchet
parents: 54096
diff changeset
   184
              "" => trace_msg ctxt (K "Done")
6fefbaeccb63 more prominent MaSh errors
blanchet
parents: 54096
diff changeset
   185
            | s => warning ("MaSh error: " ^ elide_string 1000 s));
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   186
       read_suggs (fn () => try File.read_lines sugg_path |> these))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   187
    fun clean_up () =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   188
      if overlord then ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   189
      else List.app wipe_out_file [err_file, sugg_file, cmd_file]
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   190
  in
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   191
    write_file (SOME "") ([], K "") sugg_path;
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   192
    write_file (SOME "") write_cmds cmd_path;
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   193
    trace_msg ctxt (fn () => "Running " ^ command);
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   194
    with_cleanup clean_up run_on ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   195
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   196
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   197
fun meta_char c =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   198
  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
   199
     c = #")" orelse c = #"," then
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   200
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   201
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   202
    (* fixed width, in case more digits follow *)
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   203
    "%" ^ stringN_of_int 3 (Char.ord c)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   204
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   205
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
   206
  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   207
    (case Int.fromString (String.implode [d1, d2, d3]) of
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   208
       SOME n => unmeta_chars (Char.chr n :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   209
     | NONE => "" (* error *))
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   210
  | unmeta_chars _ (#"%" :: _) = "" (* error *)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   211
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   212
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   213
val encode_str = String.translate meta_char
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   214
val encode_strs = map encode_str #> space_implode " "
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   215
val unencode_str = String.explode #> unmeta_chars []
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   216
val unencode_strs =
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   217
  space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   218
50858
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   219
fun freshish_name () =
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   220
  Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   221
  serial_string ()
42c5fcc6f28f cleaned up hint handling
blanchet
parents: 50857
diff changeset
   222
53558
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   223
(* Avoid scientific notation *)
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   224
fun safe_str_of_real r =
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   225
  if r < 0.00001 then "0.00001"
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   226
  else if r >= 1000000.0 then "1000000"
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   227
  else Markup.print_real r
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   228
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   229
fun encode_feature (name, weight) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   230
  encode_str name ^
53558
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   231
  (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   232
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   233
val encode_features = map encode_feature #> space_implode " "
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   234
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   235
fun str_of_learn (name, parents, feats, deps) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   236
  "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
53121
5f727525b1ac only generate feature weights for queries -- they're not used elsewhere
blanchet
parents: 53118
diff changeset
   237
  encode_strs feats ^ "; " ^ encode_strs deps ^ "\n"
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   238
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   239
fun str_of_relearn (name, deps) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   240
  "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   241
53099
5c7780d21d24 adapted to new MaSh syntax
blanchet
parents: 53098
diff changeset
   242
fun str_of_query max_suggs (learns, hints, parents, feats) =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   243
  implode (map str_of_learn learns) ^
53099
5c7780d21d24 adapted to new MaSh syntax
blanchet
parents: 53098
diff changeset
   244
  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^
5c7780d21d24 adapted to new MaSh syntax
blanchet
parents: 53098
diff changeset
   245
  encode_features feats ^
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   246
  (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   247
53098
blanchet
parents: 53095
diff changeset
   248
(* The suggested weights don't make much sense. *)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   249
fun extract_suggestion sugg =
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   250
  case space_explode "=" sugg of
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
   251
    [name, _ (* weight *)] =>
50965
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   252
    SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *))
7a7d1418301e use correct weights in MeSh driver
blanchet
parents: 50952
diff changeset
   253
  | [name] => SOME (unencode_str name (* , 1.0 *))
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   254
  | _ => NONE
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   255
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
   256
fun extract_suggestions line =
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   257
  case space_explode ":" line of
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   258
    [goal, suggs] =>
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   259
    (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   260
  | _ => ("", [])
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   261
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   262
structure MaSh =
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   263
struct
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   264
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   265
fun shutdown ctxt overlord =
53153
1e9735cd27aa better tracing + honor blocking better
blanchet
parents: 53152
diff changeset
   266
  (trace_msg ctxt (K "MaSh shutdown");
53756
be91786f2419 MaSh tweaks to facilitate debugging
blanchet
parents: 53564
diff changeset
   267
   run_mash_tool ctxt overlord [shutdown_server_arg] false ([], K "") (K ()))
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   268
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   269
fun save ctxt overlord =
53153
1e9735cd27aa better tracing + honor blocking better
blanchet
parents: 53152
diff changeset
   270
  (trace_msg ctxt (K "MaSh save");
1e9735cd27aa better tracing + honor blocking better
blanchet
parents: 53152
diff changeset
   271
   run_mash_tool ctxt overlord [save_models_arg] true ([], K "") (K ()))
53142
966a251efd16 have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
blanchet
parents: 53141
diff changeset
   272
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   273
fun unlearn ctxt overlord =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   274
  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
   275
    trace_msg ctxt (K "MaSh unlearn");
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   276
    shutdown ctxt overlord;
50319
dddcaeb92e11 robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer
blanchet
parents: 50311
diff changeset
   277
    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
   278
                           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
   279
                       path) NONE;
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   280
    ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   281
  end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   282
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   283
fun learn _ _ _ [] = ()
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   284
  | learn ctxt overlord save learns =
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   285
    (trace_msg ctxt (fn () => "MaSh learn " ^
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   286
         elide_string 1000 (space_implode " " (map #1 learns)));
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   287
     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   288
                   (learns, str_of_learn) (K ()))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   289
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   290
fun relearn _ _ _ [] = ()
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   291
  | relearn ctxt overlord save relearns =
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   292
    (trace_msg ctxt (fn () => "MaSh relearn " ^
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
   293
         elide_string 1000 (space_implode " " (map #1 relearns)));
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   294
     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   295
                   (relearns, str_of_relearn) (K ()))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   296
53117
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   297
fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
50969
blanchet
parents: 50967
diff changeset
   298
  (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   299
   run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   300
       (fn suggs =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   301
           case suggs () of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   302
             [] => []
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
   303
           | suggs => snd (extract_suggestions (List.last suggs)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   304
   handle List.Empty => [])
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   305
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   306
end;
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   307
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   308
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   309
(*** Middle-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   310
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
   311
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
   312
  Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   313
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   314
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
   315
  | 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
   316
  | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   317
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   318
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
   319
  | 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
   320
  | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   321
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   322
(* FIXME: Here a "Graph.update_node" function would be useful *)
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   323
fun update_access_graph_node (name, kind) =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   324
  Graph.default_node (name, Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   325
  #> kind <> Isar_Proof ? Graph.map_node name (K kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   326
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   327
fun try_graph ctxt when def f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   328
  f ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   329
  handle Graph.CYCLES (cycle :: _) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   330
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   331
              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   332
       | Graph.DUP name =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   333
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   334
              "Duplicate fact " ^ quote name ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   335
       | Graph.UNDEF name =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   336
         (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   337
              "Unknown fact " ^ quote name ^ " when " ^ when); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   338
       | exn =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   339
         if Exn.is_interrupt exn then
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   340
           reraise exn
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   341
         else
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   342
           (trace_msg ctxt (fn () =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   343
                "Internal error when " ^ when ^ ":\n" ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   344
                ML_Compiler.exn_message exn); def)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   345
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   346
fun graph_info G =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   347
  string_of_int (length (Graph.keys G)) ^ " node(s), " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   348
  string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   349
  " edge(s), " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   350
  string_of_int (length (Graph.minimals G)) ^ " minimal, " ^
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   351
  string_of_int (length (Graph.maximals G)) ^ " maximal"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   352
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   353
type mash_state =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   354
  {access_G : unit Graph.T,
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   355
   num_known_facts : int,
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   356
   dirty : string list option}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   357
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   358
val empty_state = {access_G = Graph.empty, num_known_facts = 0, dirty = SOME []}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   359
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   360
local
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   361
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   362
val version = "*** MaSh version 20130820 ***"
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   363
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   364
exception FILE_VERSION_TOO_NEW of unit
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   365
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   366
fun extract_node line =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   367
  case space_explode ":" line of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   368
    [head, parents] =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   369
    (case space_explode " " head of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   370
       [kind, name] =>
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   371
       SOME (unencode_str name, unencode_strs parents,
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   372
             try proof_kind_of_str kind |> the_default Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   373
     | _ => NONE)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   374
  | _ => NONE
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   375
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   376
fun load_state _ _ (state as (true, _)) = state
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   377
  | load_state ctxt overlord _ =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   378
    let val path = mash_state_file () in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   379
      (true,
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   380
       case try File.read_lines path of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   381
         SOME (version' :: node_lines) =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   382
         let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   383
           fun add_edge_to name parent =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   384
             Graph.default_node (parent, Isar_Proof)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   385
             #> Graph.add_edge (parent, name)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   386
           fun add_node line =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   387
             case extract_node line of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   388
               NONE => I (* shouldn't happen *)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   389
             | SOME (name, parents, kind) =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   390
               update_access_graph_node (name, kind)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   391
               #> fold (add_edge_to name) parents
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   392
           val (access_G, num_known_facts) =
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   393
             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
   394
               EQUAL =>
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   395
               (try_graph ctxt "loading state" Graph.empty (fn () =>
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   396
                    fold add_node node_lines Graph.empty),
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   397
                length node_lines)
50860
e32a283b8ce0 remove obsolete MaSh files
blanchet
parents: 50858
diff changeset
   398
             | LESS =>
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   399
               (* can't parse old file *)
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   400
               (MaSh.unlearn ctxt overlord; (Graph.empty, 0))
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   401
             | GREATER => raise FILE_VERSION_TOO_NEW ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   402
         in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   403
           trace_msg ctxt (fn () =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   404
               "Loaded fact graph (" ^ graph_info access_G ^ ")");
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   405
           {access_G = access_G, num_known_facts = num_known_facts,
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   406
            dirty = SOME []}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   407
         end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   408
       | _ => empty_state)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   409
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   410
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   411
fun save_state _ (state as {dirty = SOME [], ...}) = state
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   412
  | save_state ctxt {access_G, num_known_facts, dirty} =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   413
    let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   414
      fun str_of_entry (name, parents, kind) =
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   415
        str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   416
        encode_strs parents ^ "\n"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   417
      fun append_entry (name, (kind, (parents, _))) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   418
        cons (name, Graph.Keys.dest parents, kind)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   419
      val (banner, entries) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   420
        case dirty of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   421
          SOME names =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   422
          (NONE, fold (append_entry o Graph.get_entry access_G) names [])
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   423
        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G [])
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   424
    in
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   425
      write_file banner (entries, str_of_entry) (mash_state_file ());
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   426
      trace_msg ctxt (fn () =>
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
   427
          "Saved fact graph (" ^ graph_info access_G ^
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   428
          (case dirty of
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   429
             SOME dirty =>
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   430
             "; " ^ string_of_int (length dirty) ^ " dirty fact(s)"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   431
           | _ => "") ^  ")");
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   432
      {access_G = access_G, num_known_facts = num_known_facts, dirty = SOME []}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   433
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   434
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   435
val global_state =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   436
  Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   437
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   438
in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   439
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   440
fun map_state ctxt overlord f =
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   441
  Synchronized.change global_state
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   442
                      (load_state ctxt overlord ##> (f #> save_state ctxt))
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   443
  handle FILE_VERSION_TOO_NEW () => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   444
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   445
fun peek_state ctxt overlord 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
   446
  Synchronized.change_result global_state
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   447
      (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   448
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   449
fun clear_state ctxt overlord =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   450
  Synchronized.change global_state (fn _ =>
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   451
      (MaSh.unlearn ctxt overlord; (* also removes the state file *)
53142
966a251efd16 have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
blanchet
parents: 53141
diff changeset
   452
       (false, empty_state)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   453
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   454
end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   455
53558
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   456
fun mash_unlearn ctxt ({overlord, ...} : params) =
53559
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   457
  (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")
50570
blanchet
parents: 50557
diff changeset
   458
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   459
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   460
(*** Isabelle helpers ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   461
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
   462
fun is_mash_enabled () = (getenv "MASH" = "yes")
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
   463
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   464
val local_prefix = "local" ^ Long_Name.separator
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   465
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   466
fun elided_backquote_thm threshold th =
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   467
  elide_string threshold
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   468
    (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
   469
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   470
val thy_name_of_thm = Context.theory_name o Thm.theory_of_thm
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   471
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   472
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
   473
  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
   474
    let val hint = Thm.get_name_hint th in
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   475
      (* 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
   476
      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
   477
        SOME suf =>
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   478
        thy_name_of_thm th ^ Long_Name.separator ^ suf ^
50732
b2e7490a1b3d tweaked nicknames
blanchet
parents: 50722
diff changeset
   479
        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
   480
      | 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
   481
    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
   482
  else
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   483
    elided_backquote_thm 200 th
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   484
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   485
fun find_suggested_facts ctxt facts =
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   486
  let
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   487
    fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   488
    val tab = fold add facts Symtab.empty
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   489
    fun lookup nick =
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   490
      Symtab.lookup tab nick
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   491
      |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick)
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   492
               | _ => ())
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   493
  in map_filter lookup end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   494
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   495
fun scaled_avg [] = 0
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   496
  | scaled_avg xs =
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
   497
    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
   498
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   499
fun avg [] = 0.0
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   500
  | 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
   501
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   502
fun normalize_scores _ [] = []
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   503
  | normalize_scores max_facts xs =
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   504
    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
   505
      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
   506
    end
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   507
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
   508
fun mesh_facts _ max_facts [(_, (sels, unks))] =
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   509
    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
   510
  | mesh_facts fact_eq max_facts mess =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   511
    let
51029
211a9240b1e3 killed deadcode
blanchet
parents: 51025
diff changeset
   512
      val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
211a9240b1e3 killed deadcode
blanchet
parents: 51025
diff changeset
   513
      fun score_in fact (global_weight, (sels, unks)) =
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   514
        let
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   515
          val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score)
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   516
        in
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   517
          case find_index (curry fact_eq fact o fst) sels of
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   518
            ~1 => if member fact_eq unks fact then NONE else SOME 0.0
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   519
          | rank => score_at rank
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   520
        end
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   521
      fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   522
      val facts = fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   523
    in
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   524
      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
   525
            |> map snd |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   526
    end
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   527
53155
2c585fdbe197 eliminated some needless MaSh features
blanchet
parents: 53154
diff changeset
   528
fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
50874
2eae85887282 adjust weights -- sorts are prolific, so tone them down even more
blanchet
parents: 50869
diff changeset
   529
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
   530
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
   531
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
53155
2c585fdbe197 eliminated some needless MaSh features
blanchet
parents: 53154
diff changeset
   532
val local_feature = ("local", 16.0 (* FUDGE *))
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   533
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   534
fun crude_theory_ord p =
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   535
  if Theory.subthy p then
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   536
    if Theory.eq_thy p then EQUAL else LESS
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   537
  else if Theory.subthy (swap p) then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   538
    GREATER
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   539
  else case int_ord (pairself (length o Theory.ancestors_of) p) of
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   540
    EQUAL => string_ord (pairself Context.theory_name p)
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   541
  | order => order
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   542
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   543
fun crude_thm_ord p =
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   544
  case crude_theory_ord (pairself theory_of_thm p) of
50359
da395f0e7dea tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents: 50357
diff changeset
   545
    EQUAL =>
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   546
    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
   547
      (* 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
   548
      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
   549
        EQUAL => string_ord q
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   550
      | ord => ord
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   551
    end
50359
da395f0e7dea tweaked order of theorems to avoid forward dependencies (MaSh)
blanchet
parents: 50357
diff changeset
   552
  | ord => ord
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   553
51136
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   554
val thm_less_eq = Theory.subthy o pairself theory_of_thm
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   555
fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   556
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   557
val freezeT = Type.legacy_freeze_type
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   558
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   559
fun freeze (t $ u) = freeze t $ freeze u
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   560
  | 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
   561
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   562
  | freeze (Const (s, T)) = Const (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   563
  | freeze (Free (s, T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   564
  | freeze t = t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   565
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   566
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
   567
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   568
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
   569
  let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   570
    val problem =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   571
      {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
51010
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
   572
       factss = [("", facts)]}
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   573
  in
51187
c344cf148e8f avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents: 51184
diff changeset
   574
    get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
c344cf148e8f avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents: 51184
diff changeset
   575
                          problem
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   576
  end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   577
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   578
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   579
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   580
val pat_tvar_prefix = "_"
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   581
val pat_var_prefix = "_"
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   582
53089
a58b3b8631c6 keep long names to stay on the safe side
blanchet
parents: 53086
diff changeset
   583
(* try "Long_Name.base_name" for shorter names *)
a58b3b8631c6 keep long names to stay on the safe side
blanchet
parents: 53086
diff changeset
   584
fun massage_long_name s = s
53083
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   585
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   586
val crude_str_of_sort =
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   587
  space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   588
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   589
fun crude_str_of_typ (Type (s, [])) = massage_long_name s
53083
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   590
  | crude_str_of_typ (Type (s, Ts)) =
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   591
    massage_long_name s ^ implode (map crude_str_of_typ Ts)
53083
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   592
  | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   593
  | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   594
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   595
fun maybe_singleton_str _ "" = []
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   596
  | maybe_singleton_str pref s = [pref ^ s]
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   597
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   598
val max_pat_breadth = 10 (* FUDGE *)
50585
306c7b807e13 contain exponential explosion of term patterns
blanchet
parents: 50584
diff changeset
   599
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   600
fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   601
  let
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   602
    val thy = Proof_Context.theory_of ctxt
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   603
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   604
    val fixes = map snd (Variable.dest_fixes ctxt)
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   605
    val classes = Sign.classes_of thy
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   606
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   607
    fun add_classes @{sort type} = I
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   608
      | add_classes S =
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   609
        fold (`(Sorts.super_classes classes)
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   610
              #> swap #> op ::
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   611
              #> subtract (op =) @{sort type} #> map massage_long_name
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   612
              #> map class_feature_of
53159
a5805fe4e91c repaired num_extra_feature_facts + tuning
blanchet
parents: 53156
diff changeset
   613
              #> union (eq_fst (op =))) S
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   614
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   615
    fun pattify_type 0 _ = []
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   616
      | pattify_type _ (Type (s, [])) =
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   617
        if member (op =) bad_types s then [] else [massage_long_name s]
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   618
      | pattify_type depth (Type (s, U :: Ts)) =
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   619
        let
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   620
          val T = Type (s, Ts)
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   621
          val ps = take max_pat_breadth (pattify_type depth T)
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   622
          val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U)
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   623
        in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   624
      | pattify_type _ (TFree (_, S)) =
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   625
        maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   626
      | pattify_type _ (TVar (_, S)) =
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   627
        maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   628
    fun add_type_pat depth T =
53159
a5805fe4e91c repaired num_extra_feature_facts + tuning
blanchet
parents: 53156
diff changeset
   629
      union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   630
    fun add_type_pats 0 _ = I
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   631
      | add_type_pats depth t =
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   632
        add_type_pat depth t #> add_type_pats (depth - 1) t
53083
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   633
    fun add_type T =
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   634
      add_type_pats type_max_depth T
53156
f79f4693868b minor MaSh fix
blanchet
parents: 53155
diff changeset
   635
      #> fold_atyps_sorts (add_classes o snd) T
53084
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
   636
    fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
   637
      | add_subtypes T = add_type T
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   638
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   639
    fun weight_of_const s =
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   640
      16.0 +
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   641
      (if num_facts = 0 then
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   642
         0.0
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   643
       else
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   644
         let val count = Symtab.lookup const_tab s |> the_default 1 in
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   645
           Real.fromInt num_facts / Real.fromInt count (* FUDGE *)
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   646
         end)
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   647
    fun pattify_term _ 0 _ = []
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   648
      | pattify_term _ _ (Const (s, _)) =
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   649
        if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   650
      | pattify_term _ _ (Free (s, T)) =
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   651
        maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   652
        |> map (rpair 0.0)
53090
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
   653
        |> (if member (op =) fixes s then
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   654
              cons (free_feature_of (massage_long_name
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   655
                  (thy_name ^ Long_Name.separator ^ s)))
53090
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
   656
            else
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
   657
              I)
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   658
      | pattify_term _ _ (Var (_, T)) =
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   659
        maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair 0.0)
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   660
      | pattify_term Ts _ (Bound j) =
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   661
        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) |> map (rpair 0.0)
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   662
      | pattify_term Ts depth (t $ u) =
50339
d8dae91f3107 MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents: 50338
diff changeset
   663
        let
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   664
          val ps = take max_pat_breadth (pattify_term Ts depth t)
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   665
          val qs = take max_pat_breadth (("", 0.0) :: pattify_term Ts (depth - 1) u)
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   666
        in
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   667
          map_product (fn ppw as (p, pw) =>
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   668
              fn ("", _) => ppw
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   669
               | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   670
        end
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   671
      | pattify_term _ _ _ = []
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   672
    fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   673
    fun add_term_pats _ 0 _ = I
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   674
      | add_term_pats Ts depth t =
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   675
        add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   676
    fun add_term Ts = add_term_pats Ts term_max_depth
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   677
    fun add_subterms Ts t =
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   678
      case strip_comb t of
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   679
        (Const (s, T), args) =>
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   680
        (not (is_widely_irrelevant_const s) ? add_term Ts t)
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   681
        #> add_subtypes T
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   682
        #> fold (add_subterms Ts) args
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   683
      | (head, args) =>
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   684
        (case head of
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   685
           Free (_, T) => add_term Ts t #> add_subtypes T
53084
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
   686
         | Var (_, T) => add_subtypes T
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   687
         | Abs (_, T, body) => add_subtypes T #> add_subterms (T :: Ts) body
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   688
         | _ => I)
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   689
        #> fold (add_subterms Ts) args
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   690
  in [] |> fold (add_subterms []) ts end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   691
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   692
val term_max_depth = 2
53155
2c585fdbe197 eliminated some needless MaSh features
blanchet
parents: 53154
diff changeset
   693
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   694
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   695
(* TODO: Generate type classes for types? *)
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   696
fun features_of ctxt thy num_facts const_tab (scope, _) ts =
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   697
  let val thy_name = Context.theory_name thy in
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   698
    thy_feature_of thy_name ::
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   699
    term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   700
    |> scope <> Global ? cons local_feature
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   701
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   702
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
   703
(* 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
   704
   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
   705
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
   706
54125
420b876ff1e2 if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
blanchet
parents: 54123
diff changeset
   707
val prover_default_max_facts = 25
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   708
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   709
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   710
val typedef_dep = nickname_of_thm @{thm CollectI}
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   711
(* Mysterious parts of the class machinery create lots of proofs that refer
52071
0e70511cbba9 made "completish" mode a bit more complete
blanchet
parents: 52048
diff changeset
   712
   exclusively to "someI_ex" (and to some internal constructions). *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   713
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
   714
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   715
val fundef_ths =
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   716
  @{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
   717
         fundef_default_value}
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   718
  |> map nickname_of_thm
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   719
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   720
(* "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
   721
val typedef_ths =
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   722
  @{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
   723
         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
   724
         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
   725
         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
   726
         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
   727
         type_definition.Abs_image}
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   728
  |> map nickname_of_thm
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   729
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   730
fun is_size_def [dep] th =
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   731
    (case first_field ".recs" dep of
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   732
       SOME (pref, _) =>
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   733
       (case first_field ".size" (nickname_of_thm th) of
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   734
          SOME (pref', _) => pref = pref'
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   735
        | NONE => false)
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   736
     | NONE => false)
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   737
  | is_size_def _ _ = false
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   738
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   739
fun no_dependencies_for_status status =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   740
  status = Non_Rec_Def orelse status = Rec_Def
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   741
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
   742
fun trim_dependencies deps =
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   743
  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
   744
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   745
fun isar_dependencies_of name_tabs th =
51020
242cd1632b0b removed spurious trimming
blanchet
parents: 51010
diff changeset
   746
  let val deps = thms_in_proof (SOME name_tabs) th in
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   747
    if deps = [typedef_dep] orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   748
       deps = [class_some_dep] orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   749
       exists (member (op =) fundef_ths) deps orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   750
       exists (member (op =) typedef_ths) deps orelse
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   751
       is_size_def deps th then
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   752
      []
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   753
    else
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   754
      deps
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   755
  end
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   756
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
   757
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
   758
                           auto_level facts name_tabs th =
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
   759
  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
   760
    [] => (false, [])
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   761
  | isar_deps =>
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   762
    let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   763
      val thy = Proof_Context.theory_of ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   764
      val goal = goal_of_thm thy th
52196
2281f33e8da6 redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
blanchet
parents: 52125
diff changeset
   765
      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
51136
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   766
      val facts = facts |> filter (fn (_, th') => thm_less (th', th))
51004
5f2788c38127 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents: 51003
diff changeset
   767
      fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   768
      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
   769
      fun add_isar_dep facts dep accum =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   770
        if exists (is_dep dep) accum then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   771
          accum
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   772
        else case find_first (is_dep dep) facts of
51004
5f2788c38127 distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
blanchet
parents: 51003
diff changeset
   773
          SOME ((_, status), th) => accum @ [(("", status), th)]
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   774
        | NONE => accum (* shouldn't happen *)
54123
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   775
      val mepo_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
   776
        facts
54095
d80743f28fec simplify fudge factor code
blanchet
parents: 54091
diff changeset
   777
        |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
d80743f28fec simplify fudge factor code
blanchet
parents: 54091
diff changeset
   778
             hyp_ts concl_t
54123
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   779
      val facts =
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   780
        mepo_facts
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   781
        |> 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
   782
        |> map nickify
54123
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   783
      val num_isar_deps = length isar_deps
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   784
    in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   785
      if verbose andalso auto_level = 0 then
54123
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   786
        "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   787
        " with " ^ string_of_int num_isar_deps ^ " + " ^
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   788
        string_of_int (length facts - num_isar_deps) ^ " facts."
271a8377656f remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
blanchet
parents: 54115
diff changeset
   789
        |> Output.urgent_message
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   790
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   791
        ();
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   792
      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
   793
        {outcome = NONE, used_facts, ...} =>
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   794
        (if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   795
           let val num_facts = length used_facts in
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   796
             "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
   797
             plural_s num_facts ^ "."
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   798
             |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   799
           end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   800
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   801
           ();
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
   802
         (true, map fst used_facts))
48665
14b0732c72f7 crank up max number of dependencies
blanchet
parents: 48656
diff changeset
   803
      | _ => (false, isar_deps)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   804
    end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   805
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   806
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   807
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   808
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   809
(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   810
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   811
fun chunks_and_parents_for chunks th =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   812
  let
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   813
    fun insert_parent new parents =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   814
      let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   815
        parents |> forall (fn p => not (thm_less_eq (new, p))) parents
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   816
                   ? cons new
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   817
      end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   818
    fun rechunk seen (rest as th' :: ths) =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   819
      if thm_less_eq (th', th) then (rev seen, rest)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   820
      else rechunk (th' :: seen) ths
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   821
    fun do_chunk [] accum = accum
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   822
      | do_chunk (chunk as hd_chunk :: _) (chunks, parents) =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   823
        if thm_less_eq (hd_chunk, th) then
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   824
          (chunk :: chunks, insert_parent hd_chunk parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   825
        else if thm_less_eq (List.last chunk, th) then
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   826
          let val (front, back as hd_back :: _) = rechunk [] chunk in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   827
            (front :: back :: chunks, insert_parent hd_back parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   828
          end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   829
        else
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   830
          (chunk :: chunks, parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   831
  in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   832
    fold_rev do_chunk chunks ([], [])
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   833
    |>> cons []
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   834
    ||> map nickname_of_thm
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   835
  end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   836
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   837
fun attach_parents_to_facts _ [] = []
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   838
  | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   839
    let
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   840
      fun do_facts _ [] = []
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   841
        | do_facts (_, parents) [fact] = [(parents, fact)]
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   842
        | do_facts (chunks, parents)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   843
                   ((fact as (_, th)) :: (facts as (_, th') :: _)) =
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   844
          let
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   845
            val chunks = app_hd (cons th) chunks
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   846
            val chunks_and_parents' =
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   847
              if thm_less_eq (th, th') andalso
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   848
                 thy_name_of_thm th = thy_name_of_thm th' then
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   849
                (chunks, [nickname_of_thm th])
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   850
              else
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   851
                chunks_and_parents_for chunks th'
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   852
          in (parents, fact) :: do_facts chunks_and_parents' facts end
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   853
    in
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   854
      old_facts @ facts
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   855
      |> do_facts (chunks_and_parents_for [[]] th)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   856
      |> drop (length old_facts)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
   857
    end
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
   858
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   859
fun maximal_wrt_graph G keys =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   860
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   861
    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   862
    fun insert_new seen name =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   863
      not (Symtab.defined seen name) ? insert (op =) name
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   864
    fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   865
    fun find_maxes _ (maxs, []) = map snd maxs
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   866
      | find_maxes seen (maxs, new :: news) =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   867
        find_maxes
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   868
            (seen |> num_keys (Graph.imm_succs G new) > 1
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   869
                     ? Symtab.default (new, ()))
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   870
            (if Symtab.defined tab new then
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   871
               let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   872
                 val newp = Graph.all_preds G [new]
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   873
                 fun is_ancestor x yp = member (op =) yp x
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   874
                 val maxs =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   875
                   maxs |> filter (fn (_, max) => not (is_ancestor max newp))
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   876
               in
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   877
                 if exists (is_ancestor new o fst) maxs then
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   878
                   (maxs, news)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   879
                 else
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   880
                   ((newp, new)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   881
                    :: filter_out (fn (_, max) => is_ancestor max newp) maxs,
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   882
                    news)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   883
               end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   884
             else
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   885
               (maxs, Graph.Keys.fold (insert_new seen)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   886
                                      (Graph.imm_preds G new) news))
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   887
  in find_maxes Symtab.empty ([], Graph.maximals G) end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   888
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   889
fun maximal_wrt_access_graph access_G =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   890
  map (nickname_of_thm o snd)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   891
  #> maximal_wrt_graph access_G
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   892
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   893
fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   894
53197
6c5e7143e1f6 tuned fudge factor in light of evaluation
blanchet
parents: 53159
diff changeset
   895
val chained_feature_factor = 0.5 (* FUDGE *)
6c5e7143e1f6 tuned fudge factor in light of evaluation
blanchet
parents: 53159
diff changeset
   896
val extra_feature_factor = 0.1 (* FUDGE *)
53201
2a2dc18f3e10 reverted 6c5e7143e1f6; took a better look at evaluation data this time
blanchet
parents: 53197
diff changeset
   897
val num_extra_feature_facts = 10 (* FUDGE *)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   898
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   899
(* FUDGE *)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   900
fun weight_of_proximity_fact rank =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   901
  Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   902
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   903
fun weight_facts_smoothly facts =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   904
  facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   905
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   906
(* FUDGE *)
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   907
fun steep_weight_of_fact rank =
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   908
  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   909
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   910
fun weight_facts_steeply facts =
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   911
  facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
   912
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   913
val max_proximity_facts = 100
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   914
54060
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   915
fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   916
  let
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   917
    val inter_fact = inter (eq_snd Thm.eq_thm_prop)
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   918
    val raw_mash = find_suggested_facts ctxt facts suggs
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   919
    val proximate = take max_proximity_facts facts
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   920
    val unknown_chained = inter_fact raw_unknown chained
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   921
    val unknown_proximate = inter_fact raw_unknown proximate
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   922
    val mess =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   923
      [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   924
       (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   925
       (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   926
    val unknown =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   927
      raw_unknown
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   928
      |> fold (subtract (eq_snd Thm.eq_thm_prop))
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   929
              [unknown_chained, unknown_proximate]
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
   930
  in (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown) end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   931
53127
60801776d8af weight MaSh constants by frequency
blanchet
parents: 53121
diff changeset
   932
fun add_const_counts t =
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   933
  fold (fn s => Symtab.map_default (s, 0) (Integer.add 1))
53127
60801776d8af weight MaSh constants by frequency
blanchet
parents: 53121
diff changeset
   934
       (Term.add_const_names t [])
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   935
53559
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   936
fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) prover max_facts
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   937
                         hyp_ts concl_t facts =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   938
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   939
    val thy = Proof_Context.theory_of ctxt
53559
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   940
    val thy_name = Context.theory_name thy
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   941
    val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   942
    val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   943
    val num_facts = length facts
53127
60801776d8af weight MaSh constants by frequency
blanchet
parents: 53121
diff changeset
   944
    val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty
54085
b6b41e1d5689 optimized built-in const check
blanchet
parents: 54064
diff changeset
   945
53559
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   946
    fun fact_has_right_theory (_, th) =
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   947
      thy_name = Context.theory_name (theory_of_thm th)
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   948
    fun chained_or_extra_features_of factor (((_, stature), th), weight) =
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   949
      [prop_of th]
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   950
      |> features_of ctxt (theory_of_thm th) num_facts const_tab stature
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   951
      |> map (apsnd (fn r => weight * factor * r))
54085
b6b41e1d5689 optimized built-in const check
blanchet
parents: 54064
diff changeset
   952
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   953
    val (access_G, suggs) =
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   954
      peek_state ctxt overlord (fn {access_G, ...} =>
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   955
          if Graph.is_empty access_G then
54064
183cfce3f827 more tracing
blanchet
parents: 54063
diff changeset
   956
            (trace_msg ctxt (K "Nothing has been learned yet"); (access_G, []))
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   957
          else
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   958
            let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   959
              val parents = maximal_wrt_access_graph access_G facts
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   960
              val goal_feats =
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
   961
                features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   962
              val chained_feats =
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   963
                chained
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   964
                |> map (rpair 1.0)
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   965
                |> map (chained_or_extra_features_of chained_feature_factor)
53159
a5805fe4e91c repaired num_extra_feature_facts + tuning
blanchet
parents: 53156
diff changeset
   966
                |> rpair [] |-> fold (union (eq_fst (op =)))
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   967
              val extra_feats =
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   968
                facts
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   969
                |> take (Int.max (0, num_extra_feature_facts - length chained))
53559
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   970
                |> filter fact_has_right_theory
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   971
                |> weight_facts_steeply
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   972
                |> map (chained_or_extra_features_of extra_feature_factor)
53159
a5805fe4e91c repaired num_extra_feature_facts + tuning
blanchet
parents: 53156
diff changeset
   973
                |> rpair [] |-> fold (union (eq_fst (op =)))
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   974
              val feats =
53159
a5805fe4e91c repaired num_extra_feature_facts + tuning
blanchet
parents: 53156
diff changeset
   975
                fold (union (eq_fst (op =))) [chained_feats, extra_feats]
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
   976
                     goal_feats
53559
3858246c7c8f when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
blanchet
parents: 53558
diff changeset
   977
                |> debug ? sort (Real.compare o swap o pairself snd)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   978
              val hints =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   979
                chained |> filter (is_fact_in_graph access_G o snd)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   980
                        |> map (nickname_of_thm o snd)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   981
            in
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   982
              (access_G, MaSh.query ctxt overlord max_facts
53118
3f290031bd9e take out dangerous feature, now that all updates are permanent
blanchet
parents: 53117
diff changeset
   983
                                    ([], hints, parents, feats))
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   984
            end)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   985
    val unknown = facts |> filter_out (is_fact_in_graph access_G o snd)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   986
  in
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   987
    find_mash_suggestions ctxt max_facts suggs facts chained unknown
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   988
    |> pairself (map fact_of_raw_fact)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   989
  end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   990
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   991
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   992
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   993
    fun maybe_learn_from from (accum as (parents, graph)) =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   994
      try_graph ctxt "updating graph" accum (fn () =>
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   995
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   996
    val graph = graph |> Graph.default_node (name, Isar_Proof)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   997
    val (parents, graph) = ([], graph) |> fold maybe_learn_from parents
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   998
    val (deps, _) = ([], graph) |> fold maybe_learn_from deps
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   999
  in ((name, parents, feats, deps) :: learns, graph) end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1000
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1001
fun relearn_wrt_access_graph ctxt (name, deps) (relearns, graph) =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1002
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1003
    fun maybe_relearn_from from (accum as (parents, graph)) =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1004
      try_graph ctxt "updating graph" accum (fn () =>
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1005
          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1006
    val graph = graph |> update_access_graph_node (name, Automatic_Proof)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1007
    val (deps, _) = ([], graph) |> fold maybe_relearn_from deps
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1008
  in ((name, deps) :: relearns, graph) end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1009
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1010
fun flop_wrt_access_graph name =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1011
  update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1012
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1013
val learn_timeout_slack = 2.0
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1014
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1015
fun launch_thread timeout task =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1016
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1017
    val hard_timeout = time_mult learn_timeout_slack timeout
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1018
    val birth_time = Time.now ()
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1019
    val death_time = Time.+ (birth_time, hard_timeout)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1020
    val desc = ("Machine learner for Sledgehammer", "")
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1021
  in Async_Manager.thread MaShN birth_time death_time desc task end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1022
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1023
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) prover t facts
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1024
                     used_ths =
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1025
  if is_mash_enabled () then
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1026
    launch_thread (timeout |> the_default one_day) (fn () =>
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1027
        let
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1028
          val thy = Proof_Context.theory_of ctxt
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1029
          val name = freshish_name ()
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
  1030
          val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] |> map fst
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1031
        in
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1032
          peek_state ctxt overlord (fn {access_G, ...} =>
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1033
              let
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1034
                val parents = maximal_wrt_access_graph access_G facts
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1035
                val deps =
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1036
                  used_ths |> filter (is_fact_in_graph access_G)
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1037
                           |> map nickname_of_thm
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1038
              in
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1039
                MaSh.learn ctxt overlord true [(name, parents, feats, deps)]
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1040
              end);
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1041
          (true, "")
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1042
        end)
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1043
  else
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1044
    ()
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1045
52697
6fb98a20c349 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents: 52196
diff changeset
  1046
fun sendback sub =
6fb98a20c349 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents: 52196
diff changeset
  1047
  Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1048
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1049
val commit_timeout = seconds 30.0
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
  1050
50485
3c6ac2da2f45 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents: 50484
diff changeset
  1051
(* The timeout is understood in a very relaxed fashion. *)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1052
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1053
                     save auto_level run_prover learn_timeout facts =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1054
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1055
    val timer = Timer.startRealTimer ()
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1056
    fun next_commit_time () =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1057
      Time.+ (Timer.checkRealTimer timer, commit_timeout)
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
  1058
    val {access_G, ...} = peek_state ctxt overlord I
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1059
    val is_in_access_G = is_fact_in_graph access_G o snd
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1060
    val no_new_facts = forall is_in_access_G facts
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1061
  in
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1062
    if no_new_facts andalso not run_prover then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1063
      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
  1064
        "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
  1065
        " 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
  1066
        (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
  1067
           "\n\nHint: Try " ^ sendback learn_proverN ^
50751
d3111134973d tuned message
blanchet
parents: 50750
diff changeset
  1068
           " to learn from an automatic prover."
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1069
         else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1070
           "")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1071
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1072
        ""
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1073
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1074
      let
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1075
        val name_tabs = build_name_tables nickname_of_thm facts
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1076
        fun deps_of status th =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1077
          if no_dependencies_for_status status then
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1078
            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
  1079
          else if run_prover then
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1080
            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
  1081
                                   th
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
  1082
            |> (fn (false, _) => NONE
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1083
                 | (true, deps) => trim_dependencies deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1084
          else
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1085
            isar_dependencies_of name_tabs th
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1086
            |> trim_dependencies
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1087
        fun do_commit [] [] [] state = state
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1088
          | do_commit learns relearns flops {access_G, num_known_facts, dirty} =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1089
            let
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
  1090
              val was_empty = Graph.is_empty access_G
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1091
              val (learns, access_G) =
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1092
                ([], access_G) |> fold (learn_wrt_access_graph ctxt) learns
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1093
              val (relearns, access_G) =
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1094
                ([], access_G) |> fold (relearn_wrt_access_graph ctxt) relearns
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
  1095
              val access_G = access_G |> fold flop_wrt_access_graph flops
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1096
              val num_known_facts = num_known_facts + length learns
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
  1097
              val dirty =
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1098
                case (was_empty, dirty, relearns) of
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1099
                  (false, SOME names, []) => SOME (map #1 learns @ names)
48699
a89b83204c24 optimized saving
blanchet
parents: 48669
diff changeset
  1100
                | _ => NONE
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1101
            in
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
  1102
              MaSh.learn ctxt overlord (save andalso null relearns) (rev learns);
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
  1103
              MaSh.relearn ctxt overlord save relearns;
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1104
              {access_G = access_G, num_known_facts = num_known_facts,
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1105
               dirty = dirty}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1106
            end
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1107
        fun commit last learns relearns flops =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1108
          (if debug andalso auto_level = 0 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1109
             Output.urgent_message "Committing..."
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1110
           else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1111
             ();
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
  1112
           map_state ctxt overlord (do_commit (rev learns) relearns flops);
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1113
           if not last andalso auto_level = 0 then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1114
             let val num_proofs = length learns + length relearns in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1115
               "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
  1116
               (if run_prover then "automatic" else "Isar") ^ " proof" ^
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1117
               plural_s num_proofs ^ " in the last " ^
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51998
diff changeset
  1118
               string_of_time commit_timeout ^ "."
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1119
               |> Output.urgent_message
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1120
             end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1121
           else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1122
             ())
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1123
        fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1124
          | learn_new_fact (parents, ((_, stature as (_, status)), th))
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1125
                           (learns, (n, next_commit, _)) =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1126
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1127
              val name = nickname_of_thm th
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
  1128
              val feats =
54089
b13f6731f873 use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
blanchet
parents: 54085
diff changeset
  1129
                features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1130
              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