src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Thu, 26 Jun 2014 16:41:30 +0200
changeset 57382 6c6a0ac70eac
parent 57381 98fb25b9e578
child 57383 ba0fe0639bc8
permissions -rw-r--r--
incremental learning when learing several facts
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
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
     3
    Author:     Cezary Kaliszyk, University of Innsbruck
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
     4
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
     5
Sledgehammer's machine-learning-based relevance filter (MaSh).
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
     6
*)
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
     7
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
     8
signature SLEDGEHAMMER_MASH =
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
     9
sig
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    10
  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
    11
  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
    12
  type fact = Sledgehammer_Fact.fact
e7f01b7e244e gracefully handle the case of empty theories when going up the accessibility chain
blanchet
parents: 48293
diff changeset
    13
  type fact_override = Sledgehammer_Fact.fact_override
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    14
  type params = Sledgehammer_Prover.params
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    15
  type prover_result = Sledgehammer_Prover.prover_result
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    16
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
    17
  val trace : bool Config.T
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
    18
  val duplicates : bool Config.T
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
    19
  val MePoN : string
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    20
  val MaShN : string
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
    21
  val MeShN : string
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    22
  val mepoN : string
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
    23
  val mashN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    24
  val meshN : string
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    25
  val unlearnN : string
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    26
  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
    27
  val learn_proverN : string
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
    28
  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
    29
  val relearn_proverN : string
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
    30
  val fact_filters : string list
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    31
  val encode_str : string -> string
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
    32
  val encode_strs : string list -> string
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
    33
  val decode_str : string -> string
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
    34
  val decode_strs : string -> string list
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
    35
  val encode_features : (string * real) list -> string
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
    36
  val extract_suggestions : string -> string * (string * real) list
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    37
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
    38
  datatype mash_engine =
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
    39
    MaSh_Py
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
    40
  | MaSh_SML_kNN
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
    41
  | MaSh_SML_kNN_Ext
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
    42
  | MaSh_SML_NB
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
    43
  | MaSh_SML_NB_Ext
57106
52e1e424eec1 export more ML functions, for experimentation
blanchet
parents: 57104
diff changeset
    44
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    45
  val is_mash_enabled : unit -> bool
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    46
  val the_mash_engine : unit -> mash_engine
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    47
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
    48
  val mash_unlearn : Proof.context -> params -> unit
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
    49
  val nickname_of_thm : thm -> string
57006
blanchet
parents: 57005
diff changeset
    50
  val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
blanchet
parents: 57005
diff changeset
    51
  val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
    52
  val crude_thm_ord : thm * thm -> order
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
    53
  val thm_less : thm * thm -> bool
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    54
  val goal_of_thm : theory -> thm -> thm
57006
blanchet
parents: 57005
diff changeset
    55
  val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
blanchet
parents: 57005
diff changeset
    56
    prover_result
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
    57
  val features_of : Proof.context -> theory -> int -> int Symtab.table -> stature -> term list ->
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
    58
    (string * real) list
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
    59
  val trim_dependencies : string list -> string list option
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
    60
  val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
57006
blanchet
parents: 57005
diff changeset
    61
  val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
blanchet
parents: 57005
diff changeset
    62
    string Symtab.table * string Symtab.table -> thm -> bool * string list
blanchet
parents: 57005
diff changeset
    63
  val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
blanchet
parents: 57005
diff changeset
    64
    (string list * ('a * thm)) list
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    65
  val num_extra_feature_facts : int
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
    66
  val extra_feature_factor : real
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    67
  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
    68
  val weight_facts_steeply : 'a list -> ('a * real) list
57006
blanchet
parents: 57005
diff changeset
    69
  val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
blanchet
parents: 57005
diff changeset
    70
    ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
53127
60801776d8af weight MaSh constants by frequency
blanchet
parents: 53121
diff changeset
    71
  val add_const_counts : term -> int Symtab.table -> int Symtab.table
57006
blanchet
parents: 57005
diff changeset
    72
  val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list ->
blanchet
parents: 57005
diff changeset
    73
    fact list * fact list
54503
blanchet
parents: 54432
diff changeset
    74
  val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    75
  val mash_learn_facts : Proof.context -> params -> string -> bool -> int -> bool -> Time.time ->
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    76
    raw_fact list -> string
57006
blanchet
parents: 57005
diff changeset
    77
  val mash_learn : 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
    78
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
    79
  val mash_can_suggest_facts : Proof.context -> bool -> bool
57108
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57107
diff changeset
    80
  val generous_max_suggestions : int -> int
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    81
  val mepo_weight : real
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    82
  val mash_weight : real
57006
blanchet
parents: 57005
diff changeset
    83
  val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
blanchet
parents: 57005
diff changeset
    84
    term -> raw_fact list -> (string * fact list) list
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
    85
  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
    86
  val running_learners : unit -> unit
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    87
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    88
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    89
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    90
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
    91
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    92
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    93
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    94
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    95
open Sledgehammer_Fact
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    96
open Sledgehammer_Prover
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    97
open Sledgehammer_Prover_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    98
open Sledgehammer_MePo
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    99
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   100
val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
   101
val duplicates = Attrib.setup_config_bool @{binding sledgehammer_fact_duplicates} (K false)
51032
69da236d7838 added option to use SNoW as machine learning algo
blanchet
parents: 51029
diff changeset
   102
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   103
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   104
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
   105
fun gen_eq_thm ctxt = if Config.get ctxt duplicates then Thm.eq_thm_strict else Thm.eq_thm_prop
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
   106
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   107
val MePoN = "MePo"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   108
val MaShN = "MaSh"
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   109
val MeShN = "MeSh"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   110
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   111
val mepoN = "mepo"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   112
val mashN = "mash"
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   113
val meshN = "mesh"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   114
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   115
val fact_filters = [meshN, mepoN, mashN]
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   116
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   117
val unlearnN = "unlearn"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   118
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
   119
val learn_proverN = "learn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   120
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
   121
val relearn_proverN = "relearn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   122
57368
blanchet
parents: 57367
diff changeset
   123
fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
blanchet
parents: 57367
diff changeset
   124
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   125
type xtab = int * int Symtab.table
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   126
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   127
val empty_xtab = (0, Symtab.empty)
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   128
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   129
fun add_to_xtab key (next, tab) = (next + 1, Symtab.update_new (key, next) tab)
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   130
fun maybe_add_to_xtab key = perhaps (try (add_to_xtab key))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   131
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   132
fun mash_state_dir () = Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir
50310
b00eeb8e352e proper quoting of paths in MaSh
blanchet
parents: 50229
diff changeset
   133
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
   134
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   135
fun wipe_out_mash_state_dir () =
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   136
  let val path = mash_state_dir () in
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   137
    try (File.fold_dir (fn file => fn _ => try File.rm (Path.append path (Path.basic file))) path)
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   138
      NONE;
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   139
    ()
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   140
  end
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   141
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   142
datatype mash_engine =
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   143
  MaSh_Py
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   144
| MaSh_SML_kNN
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
   145
| MaSh_SML_kNN_Ext
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   146
| MaSh_SML_NB
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
   147
| MaSh_SML_NB_Ext
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   148
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   149
fun mash_engine () =
57089
353652f47974 renamed 'MaSh' option
blanchet
parents: 57076
diff changeset
   150
  let val flag1 = Options.default_string @{system_option MaSh} in
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   151
    (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   152
      "yes" => SOME MaSh_SML_NB
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   153
    | "py" => SOME MaSh_Py
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   154
    | "sml" => SOME MaSh_SML_NB
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   155
    | "sml_knn" => SOME MaSh_SML_kNN
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
   156
    | "sml_knn_ext" => SOME MaSh_SML_kNN_Ext
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   157
    | "sml_nb" => SOME MaSh_SML_NB
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
   158
    | "sml_nb_ext" => SOME MaSh_SML_NB_Ext
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   159
    | _ => NONE)
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   160
  end
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
   161
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   162
val is_mash_enabled = is_some o mash_engine
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   163
val the_mash_engine = the_default MaSh_SML_NB o mash_engine
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
   164
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   165
57107
2d502370ee99 changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
blanchet
parents: 57106
diff changeset
   166
(*** Low-level communication with the Python version of MaSh ***)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   167
53117
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   168
val save_models_arg = "--saveModels"
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   169
val shutdown_server_arg = "--shutdownServer"
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   170
57122
5f69b8c3af5a more work on exporter
blanchet
parents: 57120
diff changeset
   171
fun wipe_out_file file = ignore (try (File.rm o Path.explode) file)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   172
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   173
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
   174
  (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
   175
   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
   176
  handle IO.Io _ => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   177
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   178
fun run_mash_tool ctxt overlord extra_args background write_cmds read_suggs =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   179
  let
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   180
    val (temp_dir, serial) =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   181
      if overlord then (getenv "ISABELLE_HOME_USER", "")
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   182
      else (getenv "ISABELLE_TMP", serial_string ())
53129
f92b24047fc7 improved support for MaSh server
blanchet
parents: 53128
diff changeset
   183
    val log_file = temp_dir ^ "/mash_log" ^ serial
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   184
    val err_file = temp_dir ^ "/mash_err" ^ serial
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   185
    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
   186
    val sugg_path = Path.explode sugg_file
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   187
    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
   188
    val cmd_path = Path.explode cmd_file
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   189
    val model_dir = File.shell_path (mash_state_dir ())
57130
f810d15ae625 added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
blanchet
parents: 57125
diff changeset
   190
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   191
    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
   192
      "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
53790
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   193
      \PYTHONDONTWRITEBYTECODE=y ./mash.py\
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   194
      \ --quiet\
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   195
      \ --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
   196
      \ --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
   197
      " --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
   198
      \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
53790
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   199
      \ --log " ^ log_file ^
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   200
      " --inputFile " ^ cmd_file ^
298774dbdde0 provide a way to override MaSh's port from configuration file
blanchet
parents: 53757
diff changeset
   201
      " --predictions " ^ sugg_file ^
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   202
      (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^ " >& " ^ err_file ^
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   203
      (if background then " &" else "")
57130
f810d15ae625 added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
blanchet
parents: 57125
diff changeset
   204
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   205
    fun run_on () =
50750
518f0b5ef3d9 tap after, not before command invocation
blanchet
parents: 50735
diff changeset
   206
      (Isabelle_System.bash command
54100
6fefbaeccb63 more prominent MaSh errors
blanchet
parents: 54096
diff changeset
   207
       |> tap (fn _ =>
57006
blanchet
parents: 57005
diff changeset
   208
         (case try File.read (Path.explode err_file) |> the_default "" of
blanchet
parents: 57005
diff changeset
   209
           "" => trace_msg ctxt (K "Done")
blanchet
parents: 57005
diff changeset
   210
         | 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
   211
       read_suggs (fn () => try File.read_lines sugg_path |> these))
57130
f810d15ae625 added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
blanchet
parents: 57125
diff changeset
   212
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   213
    fun clean_up () =
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   214
      if overlord then () else List.app wipe_out_file [err_file, sugg_file, cmd_file]
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   215
  in
50335
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   216
    write_file (SOME "") ([], K "") sugg_path;
b17b05c8d4a4 proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)
blanchet
parents: 50319
diff changeset
   217
    write_file (SOME "") write_cmds cmd_path;
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   218
    trace_msg ctxt (fn () => "Running " ^ command);
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   219
    with_cleanup clean_up run_on ()
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   220
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   221
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   222
fun meta_char c =
57006
blanchet
parents: 57005
diff changeset
   223
  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
blanchet
parents: 57005
diff changeset
   224
     c = #"," then
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   225
    String.str c
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   226
  else
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   227
    (* fixed width, in case more digits follow *)
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   228
    "%" ^ stringN_of_int 3 (Char.ord c)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   229
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   230
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
   231
  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   232
    (case Int.fromString (String.implode [d1, d2, d3]) of
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   233
      SOME n => unmeta_chars (Char.chr n :: accum) cs
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   234
    | NONE => "" (* error *))
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
   235
  | unmeta_chars _ (#"%" :: _) = "" (* error *)
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   236
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   237
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   238
val encode_str = String.translate meta_char
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   239
val decode_str = String.explode #> unmeta_chars []
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   240
50826
18ace05656cf start using MaSh hints
blanchet
parents: 50825
diff changeset
   241
val encode_strs = map encode_str #> space_implode " "
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   242
val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   243
53558
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   244
(* Avoid scientific notation *)
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   245
fun safe_str_of_real r =
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   246
  if r < 0.00001 then "0.00001"
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   247
  else if r >= 1000000.0 then "1000000"
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   248
  else Markup.print_real r
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   249
54695
a9efdf970720 generate problems with type classes
blanchet
parents: 54693
diff changeset
   250
fun encode_feature (names, weight) =
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   251
  encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
54695
a9efdf970720 generate problems with type classes
blanchet
parents: 54693
diff changeset
   252
50356
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   253
val encode_features = map encode_feature #> space_implode " "
41f8f1f2e15d added feature weights in MaSh
blanchet
parents: 50355
diff changeset
   254
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   255
fun str_of_learn (name, parents, feats, deps) =
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   256
  "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs feats ^ "; " ^
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   257
  encode_strs deps ^ "\n"
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
   258
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   259
fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   260
53099
5c7780d21d24 adapted to new MaSh syntax
blanchet
parents: 53098
diff changeset
   261
fun str_of_query max_suggs (learns, hints, parents, feats) =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   262
  implode (map str_of_learn learns) ^
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   263
  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   264
  (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   265
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   266
(* The suggested weights do not make much sense. *)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   267
fun extract_suggestion sugg =
55286
blanchet
parents: 55202
diff changeset
   268
  (case space_explode "=" sugg of
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   269
    [name, weight] => SOME (decode_str name, Real.fromString weight |> the_default 1.0)
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   270
  | [name] => SOME (decode_str name, 1.0)
55286
blanchet
parents: 55202
diff changeset
   271
  | _ => NONE)
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
   272
50633
87961472b404 tuned ML function name
blanchet
parents: 50632
diff changeset
   273
fun extract_suggestions line =
55286
blanchet
parents: 55202
diff changeset
   274
  (case space_explode ":" line of
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   275
    [goal, suggs] => (decode_str goal, map_filter extract_suggestion (space_explode " " suggs))
55286
blanchet
parents: 55202
diff changeset
   276
  | _ => ("", []))
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   277
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   278
structure MaSh_Py =
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   279
struct
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   280
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   281
fun shutdown ctxt overlord =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   282
  (trace_msg ctxt (K "MaSh_Py shutdown");
53756
be91786f2419 MaSh tweaks to facilitate debugging
blanchet
parents: 53564
diff changeset
   283
   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
   284
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
   285
fun save ctxt overlord =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   286
  (trace_msg ctxt (K "MaSh_Py save");
53153
1e9735cd27aa better tracing + honor blocking better
blanchet
parents: 53152
diff changeset
   287
   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
   288
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   289
fun unlearn ctxt overlord =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   290
  (trace_msg ctxt (K "MaSh_Py unlearn");
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   291
   shutdown ctxt overlord;
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   292
   wipe_out_mash_state_dir ())
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   293
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   294
fun learn _ _ _ [] = ()
57006
blanchet
parents: 57005
diff changeset
   295
  | learn ctxt overlord save learns =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   296
    (trace_msg ctxt (fn () =>
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   297
       "MaSh_Py learn {" ^ elide_string 1000 (space_implode " " (map #1 learns)) ^ "}");
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   298
     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false (learns, str_of_learn)
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   299
       (K ()))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   300
53757
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   301
fun relearn _ _ _ [] = ()
8d1a059ebcdb reduce the number of emitted MaSh commands (among others to facilitate debugging)
blanchet
parents: 53756
diff changeset
   302
  | relearn ctxt overlord save relearns =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   303
    (trace_msg ctxt (fn () => "MaSh_Py relearn " ^
57006
blanchet
parents: 57005
diff changeset
   304
       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
   305
     run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
57006
blanchet
parents: 57005
diff changeset
   306
       (relearns, str_of_relearn) (K ()))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   307
53117
2381bdf47ba5 use new MaSh command-line arguments
blanchet
parents: 53116
diff changeset
   308
fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   309
  (trace_msg ctxt (fn () => "MaSh_Py query " ^ encode_features feats);
55286
blanchet
parents: 55202
diff changeset
   310
   run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs =>
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   311
     (case suggs () of [] => [] | suggs => snd (extract_suggestions (List.last suggs))))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   312
   handle List.Empty => [])
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   313
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   314
end;
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
   315
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   316
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   317
(*** Standard ML version of MaSh ***)
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   318
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   319
structure MaSh_SML =
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   320
struct
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   321
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   322
exception BOTTOM of int
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   323
57355
blanchet
parents: 57354
diff changeset
   324
fun heap cmp bnd al a =
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   325
  let
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   326
    fun maxson l i =
57017
blanchet
parents: 57014
diff changeset
   327
      let val i31 = i + i + i + 1 in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   328
        if i31 + 2 < l then
57017
blanchet
parents: 57014
diff changeset
   329
          let val x = Unsynchronized.ref i31 in
blanchet
parents: 57014
diff changeset
   330
            if cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS then x := i31 + 1 else ();
blanchet
parents: 57014
diff changeset
   331
            if cmp (Array.sub (a, !x), Array.sub (a, i31 + 2)) = LESS then x := i31 + 2 else ();
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   332
            !x
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   333
          end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   334
        else
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   335
          if i31 + 1 < l andalso cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   336
          then i31 + 1 else if i31 < l then i31 else raise BOTTOM i
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   337
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   338
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   339
    fun trickledown l i e =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   340
      let val j = maxson l i in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   341
        if cmp (Array.sub (a, j), e) = GREATER then
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   342
          (Array.update (a, i, Array.sub (a, j)); trickledown l j e)
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   343
        else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   344
          Array.update (a, i, e)
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   345
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   346
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   347
    fun trickle l i e = trickledown l i e handle BOTTOM i => Array.update (a, i, e)
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   348
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   349
    fun bubbledown l i =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   350
      let val j = maxson l i in
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   351
        Array.update (a, i, Array.sub (a, j));
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   352
        bubbledown l j
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   353
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   354
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   355
    fun bubble l i = bubbledown l i handle BOTTOM i => i
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   356
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   357
    fun trickleup i e =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   358
      let val father = (i - 1) div 3 in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   359
        if cmp (Array.sub (a, father), e) = LESS then
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   360
          (Array.update (a, i, Array.sub (a, father));
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   361
           if father > 0 then trickleup father e else Array.update (a, 0, e))
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   362
        else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   363
          Array.update (a, i, e)
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   364
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   365
57355
blanchet
parents: 57354
diff changeset
   366
    fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1))
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   367
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   368
    fun for2 i =
57355
blanchet
parents: 57354
diff changeset
   369
      if i < Integer.max 2 (al - bnd) then
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   370
        ()
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   371
      else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   372
        let val e = Array.sub (a, i) in
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   373
          Array.update (a, i, Array.sub (a, 0));
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   374
          trickleup (bubble i 0) e;
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   375
          for2 (i - 1)
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   376
        end
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   377
  in
57355
blanchet
parents: 57354
diff changeset
   378
    for (((al + 1) div 3) - 1);
blanchet
parents: 57354
diff changeset
   379
    for2 (al - 1);
blanchet
parents: 57354
diff changeset
   380
    if al > 1 then
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   381
      let val e = Array.sub (a, 1) in
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   382
        Array.update (a, 1, Array.sub (a, 0));
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   383
        Array.update (a, 0, e)
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   384
      end
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   385
    else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   386
      ()
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   387
  end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   388
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   389
val number_of_nearest_neighbors = 10 (* FUDGE *)
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   390
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   391
fun select_visible_facts big_number recommends =
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   392
  List.app (fn at =>
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   393
    let val (j, ov) = Array.sub (recommends, at) in
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   394
      Array.update (recommends, at, (j, big_number + ov))
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   395
    end)
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   396
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   397
exception EXIT of unit
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   398
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   399
fun k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts goal_feats =
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   400
  let
57357
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   401
    val ln_afreq = Math.ln (Real.fromInt num_facts)
57374
blanchet
parents: 57373
diff changeset
   402
    fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
57017
blanchet
parents: 57014
diff changeset
   403
57102
blanchet
parents: 57101
diff changeset
   404
    val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
57017
blanchet
parents: 57014
diff changeset
   405
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   406
    fun inc_overlap j v =
57361
blanchet
parents: 57360
diff changeset
   407
      let val ov = snd (Array.sub (overlaps_sqr, j)) in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   408
        Array.update (overlaps_sqr, j, (j, v + ov))
57017
blanchet
parents: 57014
diff changeset
   409
      end
blanchet
parents: 57014
diff changeset
   410
57357
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   411
    fun do_feat s =
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   412
      let
57357
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   413
        val sw = tfidf s
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   414
        val w2 = sw * sw
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   415
        fun do_th j = if j < num_facts then inc_overlap j w2 else ()
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   416
      in
57374
blanchet
parents: 57373
diff changeset
   417
        List.app do_th (Array.sub (feat_facts, s))
57017
blanchet
parents: 57014
diff changeset
   418
      end
blanchet
parents: 57014
diff changeset
   419
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   420
    val _ = List.app do_feat goal_feats
57355
blanchet
parents: 57354
diff changeset
   421
    val _ = heap (Real.compare o pairself snd) num_facts num_facts overlaps_sqr
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   422
    val no_recommends = Unsynchronized.ref 0
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   423
    val recommends = Array.tabulate (num_facts, rpair 0.0)
57363
a6a6472a2536 honor visibility in SML k-NN
blanchet
parents: 57362
diff changeset
   424
    val age = Unsynchronized.ref 500000000.0
57017
blanchet
parents: 57014
diff changeset
   425
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   426
    fun inc_recommend j v =
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   427
      let val ov = snd (Array.sub (recommends, j)) in
57374
blanchet
parents: 57373
diff changeset
   428
        if ov <= 0.0 then
blanchet
parents: 57373
diff changeset
   429
          (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
blanchet
parents: 57373
diff changeset
   430
        else if ov < !age + 1000.0 then
blanchet
parents: 57373
diff changeset
   431
          Array.update (recommends, j, (j, v + ov))
blanchet
parents: 57373
diff changeset
   432
        else
blanchet
parents: 57373
diff changeset
   433
          ()
blanchet
parents: 57373
diff changeset
   434
      end
57017
blanchet
parents: 57014
diff changeset
   435
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   436
    val k = Unsynchronized.ref 0
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   437
    fun do_k k =
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   438
      if k >= num_facts then
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   439
        raise EXIT ()
57017
blanchet
parents: 57014
diff changeset
   440
      else
blanchet
parents: 57014
diff changeset
   441
        let
57102
blanchet
parents: 57101
diff changeset
   442
          val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
57017
blanchet
parents: 57014
diff changeset
   443
          val o1 = Math.sqrt o2
blanchet
parents: 57014
diff changeset
   444
          val _ = inc_recommend j o1
57374
blanchet
parents: 57373
diff changeset
   445
          val ds = Vector.sub (depss, j)
57017
blanchet
parents: 57014
diff changeset
   446
          val l = Real.fromInt (length ds)
blanchet
parents: 57014
diff changeset
   447
        in
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   448
          List.app (fn d => inc_recommend d (o1 / l)) ds
57017
blanchet
parents: 57014
diff changeset
   449
        end
blanchet
parents: 57014
diff changeset
   450
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   451
    fun while1 () =
57361
blanchet
parents: 57360
diff changeset
   452
      if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   453
      handle EXIT () => ()
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   454
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   455
    fun while2 () =
57361
blanchet
parents: 57360
diff changeset
   456
      if !no_recommends >= max_suggs then ()
blanchet
parents: 57360
diff changeset
   457
      else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   458
      handle EXIT () => ()
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
   459
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   460
    fun ret acc at =
57363
a6a6472a2536 honor visibility in SML k-NN
blanchet
parents: 57362
diff changeset
   461
      if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   462
  in
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   463
    while1 ();
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   464
    while2 ();
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   465
    select_visible_facts 1000000000.0 recommends visible_facts;
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   466
    heap (Real.compare o pairself snd) max_suggs num_facts recommends;
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   467
    ret [] (Integer.max 0 (num_facts - max_suggs))
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   468
  end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   469
57374
blanchet
parents: 57373
diff changeset
   470
fun wider_array_of_vector init vec =
blanchet
parents: 57373
diff changeset
   471
  let val ary = Array.array init in
blanchet
parents: 57373
diff changeset
   472
    Array.copyVec {src = vec, dst = ary, di = 0};
blanchet
parents: 57373
diff changeset
   473
    ary
blanchet
parents: 57373
diff changeset
   474
  end
blanchet
parents: 57373
diff changeset
   475
57132
4ddf5a8f8f38 make SML code closer to Python code when 'nb_kuehlwein_style' is true
blanchet
parents: 57130
diff changeset
   476
val nb_def_prior_weight = 21 (* FUDGE *)
57095
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
   477
57374
blanchet
parents: 57373
diff changeset
   478
fun learn_facts (tfreq0, sfreq0, dffreq0) num_facts0 num_facts num_feats depss featss =
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   479
  let
57374
blanchet
parents: 57373
diff changeset
   480
    val tfreq = wider_array_of_vector (num_facts, 0) tfreq0
blanchet
parents: 57373
diff changeset
   481
    val sfreq = wider_array_of_vector (num_facts, Inttab.empty) sfreq0
blanchet
parents: 57373
diff changeset
   482
    val dffreq = wider_array_of_vector (num_feats, 0) dffreq0
blanchet
parents: 57373
diff changeset
   483
blanchet
parents: 57373
diff changeset
   484
    fun learn_one th feats deps =
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   485
      let
57355
blanchet
parents: 57354
diff changeset
   486
        fun add_th weight t =
blanchet
parents: 57354
diff changeset
   487
          let
blanchet
parents: 57354
diff changeset
   488
            val im = Array.sub (sfreq, t)
57374
blanchet
parents: 57373
diff changeset
   489
            fun fold_fn s = Inttab.map_default (s, 0) (Integer.add weight)
57355
blanchet
parents: 57354
diff changeset
   490
          in
57368
blanchet
parents: 57367
diff changeset
   491
            map_array_at tfreq (Integer.add weight) t;
57355
blanchet
parents: 57354
diff changeset
   492
            Array.update (sfreq, t, fold fold_fn feats im)
blanchet
parents: 57354
diff changeset
   493
          end
blanchet
parents: 57354
diff changeset
   494
57368
blanchet
parents: 57367
diff changeset
   495
        val add_sym = map_array_at dffreq (Integer.add 1)
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   496
      in
57355
blanchet
parents: 57354
diff changeset
   497
        add_th nb_def_prior_weight th;
blanchet
parents: 57354
diff changeset
   498
        List.app (add_th 1) deps;
blanchet
parents: 57354
diff changeset
   499
        List.app add_sym feats
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   500
      end
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   501
57102
blanchet
parents: 57101
diff changeset
   502
    fun for i =
57374
blanchet
parents: 57373
diff changeset
   503
      if i = num_facts then
blanchet
parents: 57373
diff changeset
   504
        ()
blanchet
parents: 57373
diff changeset
   505
      else
blanchet
parents: 57373
diff changeset
   506
        (learn_one (num_facts0 + i) (Vector.sub (featss, i)) (Vector.sub (depss, i));
blanchet
parents: 57373
diff changeset
   507
         for (i + 1))
57102
blanchet
parents: 57101
diff changeset
   508
  in
57374
blanchet
parents: 57373
diff changeset
   509
    for 0;
blanchet
parents: 57373
diff changeset
   510
    (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq)
57102
blanchet
parents: 57101
diff changeset
   511
  end
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   512
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   513
fun naive_bayes (tfreq, sfreq, dffreq) num_facts max_suggs visible_facts goal_feats =
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   514
  let
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   515
    val tau = 0.05 (* FUDGE *)
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   516
    val pos_weight = 10.0 (* FUDGE *)
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   517
    val def_val = ~15.0 (* FUDGE *)
57124
e4c2c792226f make SML naive Bayes closer to Python version
blanchet
parents: 57122
diff changeset
   518
57366
blanchet
parents: 57365
diff changeset
   519
    val ln_afreq = Math.ln (Real.fromInt num_facts)
57374
blanchet
parents: 57373
diff changeset
   520
    val idf = Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) dffreq
57366
blanchet
parents: 57365
diff changeset
   521
57359
dd89d0ec8e41 avoid subscripting array with ~1
blanchet
parents: 57358
diff changeset
   522
    fun tfidf feat = Vector.sub (idf, feat)
57102
blanchet
parents: 57101
diff changeset
   523
blanchet
parents: 57101
diff changeset
   524
    fun log_posterior i =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   525
      let
57374
blanchet
parents: 57373
diff changeset
   526
        val tfreq = Real.fromInt (Vector.sub (tfreq, i))
57097
blanchet
parents: 57096
diff changeset
   527
57357
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   528
        fun fold_feats f (res, sfh) =
57102
blanchet
parents: 57101
diff changeset
   529
          (case Inttab.lookup sfh f of
blanchet
parents: 57101
diff changeset
   530
            SOME sf =>
57298
2502adc3c3f6 enable TF-IDF
blanchet
parents: 57297
diff changeset
   531
            (res + tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
57102
blanchet
parents: 57101
diff changeset
   532
             Inttab.delete f sfh)
57298
2502adc3c3f6 enable TF-IDF
blanchet
parents: 57297
diff changeset
   533
          | NONE => (res + tfidf f * def_val, sfh))
57097
blanchet
parents: 57096
diff changeset
   534
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   535
        val (res, sfh) = fold fold_feats goal_feats (Math.ln tfreq, Vector.sub (sfreq, i))
57097
blanchet
parents: 57096
diff changeset
   536
57362
3ae07451a9f5 got rid of a few experimental options
blanchet
parents: 57361
diff changeset
   537
        fun fold_sfh (f, sf) sow = sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
57097
blanchet
parents: 57096
diff changeset
   538
57102
blanchet
parents: 57101
diff changeset
   539
        val sum_of_weights = Inttab.fold fold_sfh sfh 0.0
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   540
      in
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   541
        res + tau * sum_of_weights
57097
blanchet
parents: 57096
diff changeset
   542
      end
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   543
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   544
    val posterior = Array.tabulate (num_facts, (fn j => (j, log_posterior j)))
57102
blanchet
parents: 57101
diff changeset
   545
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   546
    fun ret at acc =
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   547
      if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   548
  in
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   549
    select_visible_facts 100000.0 posterior visible_facts;
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   550
    heap (Real.compare o pairself snd) max_suggs num_facts posterior;
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   551
    ret (Integer.max 0 (num_facts - max_suggs)) []
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   552
  end
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   553
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   554
(* experimental *)
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   555
fun naive_bayes_py ctxt overlord num_facts depss featss max_suggs goal_feats =
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   556
  let
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   557
    fun name_of_fact j = "f" ^ string_of_int j
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   558
    fun fact_of_name s = the (Int.fromString (unprefix "f" s))
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   559
    fun name_of_feature j = "F" ^ string_of_int j
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   560
    fun parents_of j = if j = 0 then [] else [name_of_fact (j - 1)]
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   561
57373
e9d47cd3239b refactoring
blanchet
parents: 57372
diff changeset
   562
    val learns = map (fn j => (name_of_fact j, parents_of j,
e9d47cd3239b refactoring
blanchet
parents: 57372
diff changeset
   563
      map name_of_feature (Vector.sub (featss, j)),
e9d47cd3239b refactoring
blanchet
parents: 57372
diff changeset
   564
      map name_of_fact (Vector.sub (depss, j)))) (0 upto num_facts - 1)
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   565
    val parents' = parents_of num_facts
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   566
    val goal_feats' = map (rpair 1.0 o name_of_feature) goal_feats
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   567
  in
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   568
    MaSh_Py.unlearn ctxt overlord;
57130
f810d15ae625 added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
blanchet
parents: 57125
diff changeset
   569
    OS.Process.sleep (seconds 2.0); (* hack *)
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   570
    MaSh_Py.query ctxt overlord max_suggs (learns, [], parents', goal_feats')
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   571
    |> map (apfst fact_of_name)
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   572
  end
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   573
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   574
(* experimental *)
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   575
fun external_tool tool max_suggs learns goal_feats =
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   576
  let
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   577
    val ser = string_of_int (serial ()) (* poor person's attempt at thread-safety *)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   578
    val ocs = TextIO.openOut ("adv_syms" ^ ser)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   579
    val ocd = TextIO.openOut ("adv_deps" ^ ser)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   580
    val ocq = TextIO.openOut ("adv_seq" ^ ser)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   581
    val occ = TextIO.openOut ("adv_conj" ^ ser)
57296
8a98f08a0523 tweaked experimental setup
blanchet
parents: 57294
diff changeset
   582
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   583
    fun os oc s = TextIO.output (oc, s)
57296
8a98f08a0523 tweaked experimental setup
blanchet
parents: 57294
diff changeset
   584
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   585
    fun ol _ _ _ [] = ()
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   586
      | ol _ f _ [e] = f e
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   587
      | ol oc f sep (h :: t) = (f h; os oc sep; ol oc f sep t)
57296
8a98f08a0523 tweaked experimental setup
blanchet
parents: 57294
diff changeset
   588
57294
ef9d4e1ceb00 use strings to communicate with external process, to ease debugging
blanchet
parents: 57291
diff changeset
   589
    fun do_learn (name, feats, deps) =
57357
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   590
      (os ocs name; os ocs ":"; ol ocs (os ocs o quote) ", " feats; os ocs "\n";
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   591
       os ocd name; os ocd ":"; ol ocd (os ocd) " " deps; os ocd "\n"; os ocq name; os ocq "\n")
57296
8a98f08a0523 tweaked experimental setup
blanchet
parents: 57294
diff changeset
   592
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   593
    fun forkexec no =
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   594
      let
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   595
        val cmd =
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   596
          "~/misc/" ^ tool ^ " adv_syms" ^ ser ^ " adv_deps" ^ ser ^ " " ^ string_of_int no ^
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   597
          " adv_seq" ^ ser ^ " < adv_conj" ^ ser
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   598
      in
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   599
        fst (Isabelle_System.bash_output cmd)
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   600
        |> space_explode " "
57294
ef9d4e1ceb00 use strings to communicate with external process, to ease debugging
blanchet
parents: 57291
diff changeset
   601
        |> filter_out (curry (op =) "")
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   602
      end
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   603
  in
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   604
    (List.app do_learn learns; ol occ (os occ o quote) ", " goal_feats;
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   605
     TextIO.closeOut ocs; TextIO.closeOut ocd; TextIO.closeOut ocq; TextIO.closeOut occ;
57294
ef9d4e1ceb00 use strings to communicate with external process, to ease debugging
blanchet
parents: 57291
diff changeset
   606
     forkexec max_suggs)
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   607
  end
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   608
57375
b75438e23925 renamed experimental learning engines
blanchet
parents: 57374
diff changeset
   609
val k_nearest_neighbors_ext =
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   610
  external_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   611
val naive_bayes_ext = external_tool "predict/nbayes"
57374
blanchet
parents: 57373
diff changeset
   612
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   613
fun query_external ctxt engine max_suggs learns goal_feats =
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   614
  (trace_msg ctxt (fn () => "MaSh_SML query external " ^ encode_strs goal_feats);
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   615
   (case engine of
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   616
     MaSh_SML_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   617
   | MaSh_SML_NB_Ext => naive_bayes_ext max_suggs learns goal_feats))
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   618
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   619
fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   620
    (freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   621
  (trace_msg ctxt (fn () => "MaSh_SML query internal " ^ encode_strs goal_feats ^ " from {" ^
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   622
     elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   623
   (case engine of
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   624
     MaSh_SML_kNN =>
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   625
     let
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   626
       val feat_facts = Array.array (num_feats, [])
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   627
       val _ =
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   628
         Vector.foldl (fn (feats, fact) =>
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   629
             (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1))
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   630
           0 featss
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   631
     in
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   632
       k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts int_goal_feats
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   633
     end
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   634
   | MaSh_SML_NB => naive_bayes freqs num_facts max_suggs visible_facts int_goal_feats)
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   635
   |> map (curry Vector.sub fact_names o fst))
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   636
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   637
end;
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   638
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   639
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   640
(*** Middle-level communication with MaSh ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   641
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   642
datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   643
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   644
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
   645
  | 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
   646
  | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   647
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   648
fun proof_kind_of_str "a" = Automatic_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
   649
  | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   650
  | proof_kind_of_str _ (* "i" *) = Isar_Proof
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   651
57011
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   652
fun add_edge_to name parent =
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   653
  Graph.default_node (parent, (Isar_Proof, [], []))
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   654
  #> Graph.add_edge (parent, name)
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   655
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   656
fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) =
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   657
  ((Graph.new_node (name, (kind, feats, deps)) access_G
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   658
    handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   659
   |> fold (add_edge_to name) parents,
57374
blanchet
parents: 57373
diff changeset
   660
  (maybe_add_to_xtab name fact_xtab,
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   661
   fold maybe_add_to_xtab feats feat_xtab),
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   662
  (name, feats, deps) :: learns)
57011
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   663
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   664
fun try_graph ctxt when def f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   665
  f ()
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   666
  handle
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   667
    Graph.CYCLES (cycle :: _) =>
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   668
    (trace_msg ctxt (fn () => "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   669
  | Graph.DUP name =>
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   670
    (trace_msg ctxt (fn () => "Duplicate fact " ^ quote name ^ " when " ^ when); def)
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   671
  | Graph.UNDEF name =>
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   672
    (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   673
  | exn =>
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   674
    if Exn.is_interrupt exn then
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   675
      reraise exn
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   676
    else
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   677
      (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   678
       def)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   679
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   680
fun graph_info G =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   681
  string_of_int (length (Graph.keys G)) ^ " node(s), " ^
57006
blanchet
parents: 57005
diff changeset
   682
  string_of_int (fold (Integer.add o length o snd) (Graph.dest G) 0) ^ " edge(s), " ^
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   683
  string_of_int (length (Graph.maximals G)) ^ " maximal"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   684
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   685
type mash_state =
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   686
  {access_G : (proof_kind * string list * string list) Graph.T,
57374
blanchet
parents: 57373
diff changeset
   687
   xtabs : xtab * xtab,
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   688
   ffds : string vector * int list vector * int list vector,
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   689
   freqs : int vector * int Inttab.table vector * int vector,
57365
blanchet
parents: 57364
diff changeset
   690
   dirty_facts : string list option}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   691
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   692
val empty_xtabs = (empty_xtab, empty_xtab)
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   693
val empty_ffds = (Vector.fromList [], Vector.fromList [], Vector.fromList [])
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   694
val empty_freqs = (Vector.fromList [], Vector.fromList [], Vector.fromList [])
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   695
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   696
val empty_state =
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   697
  {access_G = Graph.empty,
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   698
   xtabs = empty_xtabs,
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   699
   ffds = empty_ffds,
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   700
   freqs = empty_freqs,
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   701
   dirty_facts = SOME []} : mash_state
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   702
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   703
fun recompute_ffds_freqs_from_learns learns ((num_facts, fact_tab), (num_feats, feat_tab))
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   704
    num_facts0 (fact_names0, featss0, depss0) freqs0 =
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   705
  let
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   706
    val fact_names = Vector.concat [fact_names0, Vector.fromList (map #1 learns)]
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   707
    val featss = Vector.concat [featss0,
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   708
      Vector.fromList (map (map_filter (Symtab.lookup feat_tab) o #2) learns)]
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   709
    val depss = Vector.concat [depss0,
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   710
      Vector.fromList (map (map_filter (Symtab.lookup fact_tab) o #3) learns)]
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   711
  in
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   712
    ((fact_names, featss, depss),
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   713
     MaSh_SML.learn_facts freqs0 num_facts0 num_facts num_feats depss featss)
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   714
  end
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   715
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   716
fun reorder_learns (num_facts, fact_tab) learns =
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   717
  let val ary = Array.array (num_facts, ("", [], [])) in
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   718
    List.app (fn learn as (fact, _, _) =>
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   719
        Array.update (ary, the (Symtab.lookup fact_tab fact), learn))
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   720
      learns;
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   721
    Array.foldr (op ::) [] ary
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   722
  end
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   723
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   724
fun recompute_ffds_freqs_from_access_G access_G (xtabs as (fact_xtab, _)) =
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   725
  let
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   726
    val learns =
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   727
      Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   728
      |> reorder_learns fact_xtab
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   729
  in
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   730
    recompute_ffds_freqs_from_learns learns xtabs 0 empty_ffds empty_freqs
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   731
  end
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   732
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   733
local
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   734
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   735
val version = "*** MaSh version 20140625 ***"
50357
187ae76a1757 more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions
blanchet
parents: 50356
diff changeset
   736
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   737
exception FILE_VERSION_TOO_NEW of unit
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   738
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   739
fun extract_node line =
55286
blanchet
parents: 55202
diff changeset
   740
  (case space_explode ":" line of
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   741
    [head, tail] =>
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   742
    (case (space_explode " " head, map (unprefix " ") (space_explode ";" tail)) of
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   743
      ([kind, name], [parents, feats, deps]) =>
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   744
      SOME (proof_kind_of_str kind, decode_str name, decode_strs parents, decode_strs feats,
57010
121b63d7bcdb take weights into consideration in knn
blanchet
parents: 57009
diff changeset
   745
        decode_strs deps)
55286
blanchet
parents: 55202
diff changeset
   746
    | _ => NONE)
blanchet
parents: 55202
diff changeset
   747
  | _ => NONE)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   748
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   749
fun load_state ctxt overlord (time_state as (memory_time, _)) =
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   750
  let val path = mash_state_file () in
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   751
    (case try OS.FileSys.modTime (Path.implode (Path.expand path)) of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   752
      NONE => time_state
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   753
    | SOME disk_time =>
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   754
      if Time.>= (memory_time, disk_time) then
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   755
        time_state
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   756
      else
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   757
        (disk_time,
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   758
         (case try File.read_lines path of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   759
           SOME (version' :: node_lines) =>
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   760
           let
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   761
             fun extract_line_and_add_node line =
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   762
               (case extract_node line of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   763
                 NONE => I (* should not happen *)
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   764
               | SOME (kind, name, parents, feats, deps) => add_node kind name parents feats deps)
57011
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   765
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   766
             val empty_G_etc = (Graph.empty, empty_xtabs, [])
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   767
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   768
             val (access_G, xtabs, rev_learns) =
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   769
               (case string_ord (version', version) of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   770
                 EQUAL =>
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   771
                 try_graph ctxt "loading state" empty_G_etc
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   772
                   (fn () => fold extract_line_and_add_node node_lines empty_G_etc)
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   773
               | LESS =>
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   774
                 (* cannot parse old file *)
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   775
                 (if the_mash_engine () = MaSh_Py then MaSh_Py.unlearn ctxt overlord
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   776
                  else wipe_out_mash_state_dir ();
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   777
                  empty_G_etc)
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   778
               | GREATER => raise FILE_VERSION_TOO_NEW ())
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   779
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   780
             val (ffds, freqs) =
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   781
               recompute_ffds_freqs_from_learns (rev rev_learns) xtabs 0 empty_ffds empty_freqs
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   782
           in
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   783
             trace_msg ctxt (fn () => "Loaded fact graph (" ^ graph_info access_G ^ ")");
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   784
             {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []}
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   785
           end
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   786
         | _ => empty_state)))
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   787
  end
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   788
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   789
fun str_of_entry (kind, name, parents, feats, deps) =
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   790
  str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   791
  encode_strs feats ^ "; " ^ encode_strs deps ^ "\n"
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   792
57365
blanchet
parents: 57364
diff changeset
   793
fun save_state _ (time_state as (_, {dirty_facts = SOME [], ...})) = time_state
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   794
  | save_state ctxt (memory_time, {access_G, xtabs, ffds, freqs, dirty_facts}) =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   795
    let
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   796
      fun append_entry (name, ((kind, feats, deps), (parents, _))) =
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   797
        cons (kind, name, Graph.Keys.dest parents, feats, deps)
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   798
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   799
      val path = mash_state_file ()
57365
blanchet
parents: 57364
diff changeset
   800
      val dirty_facts' =
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   801
        (case try OS.FileSys.modTime (Path.implode path) of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   802
          NONE => NONE
57365
blanchet
parents: 57364
diff changeset
   803
        | SOME disk_time => if Time.< (disk_time, memory_time) then dirty_facts else NONE)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   804
      val (banner, entries) =
57365
blanchet
parents: 57364
diff changeset
   805
        (case dirty_facts' of
55286
blanchet
parents: 55202
diff changeset
   806
          SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
blanchet
parents: 55202
diff changeset
   807
        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   808
    in
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   809
      write_file banner (entries, str_of_entry) path;
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   810
      trace_msg ctxt (fn () =>
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   811
        "Saved fact graph (" ^ graph_info access_G ^
57365
blanchet
parents: 57364
diff changeset
   812
        (case dirty_facts of
blanchet
parents: 57364
diff changeset
   813
          SOME dirty_facts => "; " ^ string_of_int (length dirty_facts) ^ " dirty fact(s)"
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   814
        | _ => "") ^  ")");
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   815
      (Time.now (),
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   816
       {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []})
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   817
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   818
57365
blanchet
parents: 57364
diff changeset
   819
val global_state = Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   820
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   821
in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   822
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   823
fun map_state ctxt overlord f =
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   824
  Synchronized.change global_state (load_state ctxt overlord ##> f #> save_state ctxt)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   825
  handle FILE_VERSION_TOO_NEW () => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   826
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   827
fun peek_state ctxt overlord f =
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   828
  Synchronized.change_result global_state (perhaps (try (load_state ctxt overlord)) #> `snd #>> f)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   829
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   830
fun clear_state ctxt overlord =
57017
blanchet
parents: 57014
diff changeset
   831
  (* "MaSh_Py.unlearn" also removes the state file *)
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   832
  Synchronized.change global_state (fn _ =>
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   833
    (if the_mash_engine () = MaSh_Py then MaSh_Py.unlearn ctxt overlord
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   834
     else wipe_out_mash_state_dir ();
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   835
     (Time.zeroTime, empty_state)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   836
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   837
end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   838
53558
f9682fdfd47b minor fixes
blanchet
parents: 53556
diff changeset
   839
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
   840
  (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")
50570
blanchet
parents: 50557
diff changeset
   841
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   842
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   843
(*** Isabelle helpers ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   844
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   845
val local_prefix = "local" ^ Long_Name.separator
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   846
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   847
fun elided_backquote_thm threshold th =
57006
blanchet
parents: 57005
diff changeset
   848
  elide_string threshold (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
   849
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   850
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
   851
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   852
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
   853
  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
   854
    let val hint = Thm.get_name_hint th in
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   855
      (* There must be a better way to detect local facts. *)
55286
blanchet
parents: 55202
diff changeset
   856
      (case try (unprefix local_prefix) hint of
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
   857
        SOME suf =>
55286
blanchet
parents: 55202
diff changeset
   858
        thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
blanchet
parents: 55202
diff changeset
   859
        elided_backquote_thm 50 th
blanchet
parents: 55202
diff changeset
   860
      | NONE => hint)
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
   861
    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
   862
  else
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   863
    elided_backquote_thm 200 th
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   864
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   865
fun find_suggested_facts ctxt facts =
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   866
  let
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   867
    fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   868
    val tab = fold add facts Symtab.empty
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   869
    fun lookup nick =
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   870
      Symtab.lookup tab nick
57006
blanchet
parents: 57005
diff changeset
   871
      |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ())
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   872
  in map_filter lookup end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   873
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   874
fun scaled_avg [] = 0
57006
blanchet
parents: 57005
diff changeset
   875
  | scaled_avg xs = 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
   876
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   877
fun avg [] = 0.0
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   878
  | 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
   879
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   880
fun normalize_scores _ [] = []
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   881
  | normalize_scores max_facts xs =
57006
blanchet
parents: 57005
diff changeset
   882
    map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   883
57096
e4074b91b2a6 always remove duplicates in meshing + use weights for Naive Bayes
blanchet
parents: 57095
diff changeset
   884
fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
e4074b91b2a6 always remove duplicates in meshing + use weights for Naive Bayes
blanchet
parents: 57095
diff changeset
   885
    distinct fact_eq (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
   886
  | mesh_facts fact_eq max_facts mess =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   887
    let
51029
211a9240b1e3 killed deadcode
blanchet
parents: 51025
diff changeset
   888
      val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
57006
blanchet
parents: 57005
diff changeset
   889
51029
211a9240b1e3 killed deadcode
blanchet
parents: 51025
diff changeset
   890
      fun score_in fact (global_weight, (sels, unks)) =
57006
blanchet
parents: 57005
diff changeset
   891
        let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
55286
blanchet
parents: 55202
diff changeset
   892
          (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
   893
            ~1 => if member fact_eq unks fact then NONE else SOME 0.0
55286
blanchet
parents: 55202
diff changeset
   894
          | rank => score_at rank)
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   895
        end
57006
blanchet
parents: 57005
diff changeset
   896
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
   897
      fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   898
    in
57006
blanchet
parents: 57005
diff changeset
   899
      fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
blanchet
parents: 57005
diff changeset
   900
      |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
blanchet
parents: 57005
diff changeset
   901
      |> map snd |> take max_facts
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   902
    end
48312
b40722a81ac9 implemented meshing of Iter and MaSh results
blanchet
parents: 48311
diff changeset
   903
54693
dd5874e4553f more reasonable default weight
blanchet
parents: 54503
diff changeset
   904
val default_weight = 1.0
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   905
fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *))
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   906
fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *))
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   907
fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *))
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   908
fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *))
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   909
val local_feature = ("local", 16.0 (* FUDGE *))
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   910
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   911
fun crude_theory_ord p =
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   912
  if Theory.subthy p then
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   913
    if Theory.eq_thy p then EQUAL else LESS
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   914
  else if Theory.subthy (swap p) then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   915
    GREATER
55286
blanchet
parents: 55202
diff changeset
   916
  else
blanchet
parents: 55202
diff changeset
   917
    (case int_ord (pairself (length o Theory.ancestors_of) p) of
blanchet
parents: 55202
diff changeset
   918
      EQUAL => string_ord (pairself Context.theory_name p)
blanchet
parents: 55202
diff changeset
   919
    | order => order)
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   920
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   921
fun crude_thm_ord p =
55286
blanchet
parents: 55202
diff changeset
   922
  (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
   923
    EQUAL =>
57039
1ddd1f75fb40 added comment
blanchet
parents: 57029
diff changeset
   924
    (* The hack below is necessary because of odd dependencies that are not reflected in the theory
1ddd1f75fb40 added comment
blanchet
parents: 57029
diff changeset
   925
       comparison. *)
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   926
    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
   927
      (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
55286
blanchet
parents: 55202
diff changeset
   928
      (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   929
        EQUAL => string_ord q
55286
blanchet
parents: 55202
diff changeset
   930
      | ord => ord)
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   931
    end
55286
blanchet
parents: 55202
diff changeset
   932
  | ord => ord)
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   933
51136
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   934
val thm_less_eq = Theory.subthy o pairself theory_of_thm
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   935
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
   936
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   937
val freezeT = Type.legacy_freeze_type
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   938
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   939
fun freeze (t $ u) = freeze t $ freeze u
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   940
  | 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
   941
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   942
  | freeze (Const (s, T)) = Const (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   943
  | freeze (Free (s, T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   944
  | freeze t = t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   945
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   946
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
   947
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
   948
fun run_prover_for_mash ctxt params prover goal_name facts goal =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   949
  let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   950
    val problem =
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
   951
      {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
   952
       subgoal_count = 1, factss = [("", facts)]}
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   953
  in
54503
blanchet
parents: 54432
diff changeset
   954
    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   955
  end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   956
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   957
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   958
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   959
val pat_tvar_prefix = "_"
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   960
val pat_var_prefix = "_"
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   961
53089
a58b3b8631c6 keep long names to stay on the safe side
blanchet
parents: 53086
diff changeset
   962
(* try "Long_Name.base_name" for shorter names *)
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   963
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
   964
57006
blanchet
parents: 57005
diff changeset
   965
val crude_str_of_sort = space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   966
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   967
fun crude_str_of_typ (Type (s, [])) = massage_long_name s
57006
blanchet
parents: 57005
diff changeset
   968
  | crude_str_of_typ (Type (s, Ts)) = 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
   969
  | 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
   970
  | 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
   971
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   972
fun maybe_singleton_str _ "" = []
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   973
  | maybe_singleton_str pref s = [pref ^ s]
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   974
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   975
val max_pat_breadth = 10 (* FUDGE *)
50585
306c7b807e13 contain exponential explosion of term patterns
blanchet
parents: 50584
diff changeset
   976
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   977
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
   978
  let
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   979
    val thy = Proof_Context.theory_of ctxt
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   980
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   981
    val fixes = map snd (Variable.dest_fixes ctxt)
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   982
    val classes = Sign.classes_of thy
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   983
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   984
    fun add_classes @{sort type} = I
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   985
      | add_classes S =
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   986
        fold (`(Sorts.super_classes classes)
57006
blanchet
parents: 57005
diff changeset
   987
          #> swap #> op ::
blanchet
parents: 57005
diff changeset
   988
          #> subtract (op =) @{sort type} #> map massage_long_name
blanchet
parents: 57005
diff changeset
   989
          #> map class_feature_of
blanchet
parents: 57005
diff changeset
   990
          #> union (eq_fst (op =))) S
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   991
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   992
    fun pattify_type 0 _ = []
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   993
      | pattify_type _ (Type (s, [])) =
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   994
        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
   995
      | pattify_type depth (Type (s, U :: Ts)) =
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   996
        let
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   997
          val T = Type (s, Ts)
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   998
          val ps = take max_pat_breadth (pattify_type depth T)
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   999
          val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U)
57006
blanchet
parents: 57005
diff changeset
  1000
        in
blanchet
parents: 57005
diff changeset
  1001
          map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
blanchet
parents: 57005
diff changeset
  1002
        end
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
  1003
      | pattify_type _ (TFree (_, S)) =
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
  1004
        maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
  1005
      | pattify_type _ (TVar (_, S)) =
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
  1006
        maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
57006
blanchet
parents: 57005
diff changeset
  1007
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
  1008
    fun add_type_pat depth T =
53159
a5805fe4e91c repaired num_extra_feature_facts + tuning
blanchet
parents: 53156
diff changeset
  1009
      union (eq_fst (op =)) (map type_feature_of (pattify_type depth T))
57006
blanchet
parents: 57005
diff changeset
  1010
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
  1011
    fun add_type_pats 0 _ = I
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
  1012
      | add_type_pats depth t =
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
  1013
        add_type_pat depth t #> add_type_pats (depth - 1) t
57006
blanchet
parents: 57005
diff changeset
  1014
53083
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
  1015
    fun add_type T =
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
  1016
      add_type_pats type_max_depth T
53156
f79f4693868b minor MaSh fix
blanchet
parents: 53155
diff changeset
  1017
      #> fold_atyps_sorts (add_classes o snd) T
57006
blanchet
parents: 57005
diff changeset
  1018
53084
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
  1019
    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
  1020
      | add_subtypes T = add_type T
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
  1021
57099
blanchet
parents: 57098
diff changeset
  1022
    val base_weight_of_const = 16.0 (* FUDGE *)
blanchet
parents: 57098
diff changeset
  1023
    val weight_of_const =
blanchet
parents: 57098
diff changeset
  1024
      (if num_facts = 0 orelse Symtab.is_empty const_tab then
blanchet
parents: 57098
diff changeset
  1025
         K base_weight_of_const
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1026
       else
57099
blanchet
parents: 57098
diff changeset
  1027
         fn s =>
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1028
         let val count = Symtab.lookup const_tab s |> the_default 1 in
57099
blanchet
parents: 57098
diff changeset
  1029
           base_weight_of_const + Real.fromInt num_facts / Real.fromInt count
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1030
         end)
57006
blanchet
parents: 57005
diff changeset
  1031
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1032
    fun pattify_term _ 0 _ = []
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1033
      | pattify_term _ _ (Const (s, _)) =
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1034
        if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)]
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
  1035
      | pattify_term _ _ (Free (s, T)) =
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
  1036
        maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1037
        |> map (rpair 1.0)
53090
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
  1038
        |> (if member (op =) fixes s then
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1039
              cons (free_feature_of (massage_long_name
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1040
                  (thy_name ^ Long_Name.separator ^ s)))
53090
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
  1041
            else
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
  1042
              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
  1043
      | pattify_term _ _ (Var (_, T)) =
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1044
        maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight)
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
  1045
      | pattify_term Ts _ (Bound j) =
54695
a9efdf970720 generate problems with type classes
blanchet
parents: 54693
diff changeset
  1046
        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1047
        |> map (rpair default_weight)
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
  1048
      | pattify_term Ts depth (t $ u) =
50339
d8dae91f3107 MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents: 50338
diff changeset
  1049
        let
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1050
          val ps = take max_pat_breadth (pattify_term Ts depth t)
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1051
          val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u)
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1052
        in
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1053
          map_product (fn ppw as (p, pw) =>
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1054
            fn ("", _) => ppw
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1055
             | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1056
        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
  1057
      | pattify_term _ _ _ = []
57006
blanchet
parents: 57005
diff changeset
  1058
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
  1059
    fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts
57006
blanchet
parents: 57005
diff changeset
  1060
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1061
    fun add_term_pats _ 0 _ = I
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1062
      | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t
57006
blanchet
parents: 57005
diff changeset
  1063
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1064
    fun add_term Ts = add_term_pats Ts term_max_depth
57006
blanchet
parents: 57005
diff changeset
  1065
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
  1066
    fun add_subterms Ts t =
55286
blanchet
parents: 55202
diff changeset
  1067
      (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
  1068
        (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
  1069
        (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
  1070
        #> 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
  1071
        #> fold (add_subterms Ts) args
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
  1072
      | (head, args) =>
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1073
        (case head of
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
  1074
           Free (_, T) => add_term Ts t #> add_subtypes T
53084
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
  1075
         | Var (_, T) => add_subtypes T
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
  1076
         | 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
  1077
         | _ => I)
55286
blanchet
parents: 55202
diff changeset
  1078
        #> fold (add_subterms Ts) args)
57006
blanchet
parents: 57005
diff changeset
  1079
  in
blanchet
parents: 57005
diff changeset
  1080
    fold (add_subterms []) ts []
blanchet
parents: 57005
diff changeset
  1081
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1082
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
  1083
val term_max_depth = 2
53155
2c585fdbe197 eliminated some needless MaSh features
blanchet
parents: 53154
diff changeset
  1084
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1085
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1086
(* TODO: Generate type classes for types? *)
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1087
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
  1088
  let val thy_name = Context.theory_name thy in
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
  1089
    thy_feature_of thy_name ::
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1090
    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
  1091
    |> scope <> Global ? cons local_feature
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
  1092
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1093
57006
blanchet
parents: 57005
diff changeset
  1094
(* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
blanchet
parents: 57005
diff changeset
  1095
   from such proofs. *)
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
  1096
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
  1097
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
  1098
val prover_default_max_facts = 25
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1099
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
  1100
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
  1101
val typedef_dep = nickname_of_thm @{thm CollectI}
57006
blanchet
parents: 57005
diff changeset
  1102
(* Mysterious parts of the class machinery create lots of proofs that refer exclusively to
blanchet
parents: 57005
diff changeset
  1103
   "someI_ex" (and to some internal constructions). *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
  1104
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
  1105
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
  1106
val fundef_ths =
57006
blanchet
parents: 57005
diff changeset
  1107
  @{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value}
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
  1108
  |> map nickname_of_thm
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
  1109
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
  1110
(* "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
  1111
val typedef_ths =
57006
blanchet
parents: 57005
diff changeset
  1112
  @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep
blanchet
parents: 57005
diff changeset
  1113
      type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases
blanchet
parents: 57005
diff changeset
  1114
      type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct
blanchet
parents: 57005
diff changeset
  1115
      type_definition.Rep_range type_definition.Abs_image}
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1116
  |> map nickname_of_thm
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
  1117
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
  1118
fun is_size_def [dep] th =
55642
63beb38e9258 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents: 55286
diff changeset
  1119
    (case first_field ".rec" dep of
57006
blanchet
parents: 57005
diff changeset
  1120
      SOME (pref, _) =>
blanchet
parents: 57005
diff changeset
  1121
      (case first_field ".size" (nickname_of_thm th) of
blanchet
parents: 57005
diff changeset
  1122
        SOME (pref', _) => pref = pref'
blanchet
parents: 57005
diff changeset
  1123
      | NONE => false)
blanchet
parents: 57005
diff changeset
  1124
    | NONE => false)
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
  1125
  | is_size_def _ _ = false
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
  1126
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1127
fun trim_dependencies deps =
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
  1128
  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
  1129
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
  1130
fun isar_dependencies_of name_tabs th =
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
  1131
  thms_in_proof max_dependencies (SOME name_tabs) th
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
  1132
  |> Option.map (fn deps =>
57006
blanchet
parents: 57005
diff changeset
  1133
    if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
blanchet
parents: 57005
diff changeset
  1134
       exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
  1135
       is_size_def deps th then
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
  1136
      []
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
  1137
    else
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
  1138
      deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1139
57006
blanchet
parents: 57005
diff changeset
  1140
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
blanchet
parents: 57005
diff changeset
  1141
    name_tabs th =
55286
blanchet
parents: 55202
diff changeset
  1142
  (case isar_dependencies_of name_tabs th of
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
  1143
    SOME [] => (false, [])
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
  1144
  | isar_deps0 =>
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1145
    let
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
  1146
      val isar_deps = these isar_deps0
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1147
      val thy = Proof_Context.theory_of ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1148
      val goal = goal_of_thm thy th
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
  1149
      val name = nickname_of_thm 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
  1150
      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
51136
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
  1151
      val facts = facts |> filter (fn (_, th') => thm_less (th', th))
57006
blanchet
parents: 57005
diff changeset
  1152
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
  1153
      fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
57006
blanchet
parents: 57005
diff changeset
  1154
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1155
      fun is_dep dep (_, th) = nickname_of_thm th = dep
57006
blanchet
parents: 57005
diff changeset
  1156
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1157
      fun add_isar_dep facts dep accum =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1158
        if exists (is_dep dep) accum then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1159
          accum
55286
blanchet
parents: 55202
diff changeset
  1160
        else
blanchet
parents: 55202
diff changeset
  1161
          (case find_first (is_dep dep) facts of
blanchet
parents: 55202
diff changeset
  1162
            SOME ((_, status), th) => accum @ [(("", status), th)]
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1163
          | NONE => accum (* should not happen *))
57006
blanchet
parents: 57005
diff changeset
  1164
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
  1165
      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
  1166
        facts
54095
d80743f28fec simplify fudge factor code
blanchet
parents: 54091
diff changeset
  1167
        |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
d80743f28fec simplify fudge factor code
blanchet
parents: 54091
diff changeset
  1168
             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
  1169
      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
  1170
        mepo_facts
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
  1171
        |> 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
  1172
        |> 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
  1173
      val num_isar_deps = length isar_deps
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1174
    in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1175
      if verbose andalso auto_level = 0 then
57017
blanchet
parents: 57014
diff changeset
  1176
        Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
blanchet
parents: 57014
diff changeset
  1177
          string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
blanchet
parents: 57014
diff changeset
  1178
          " facts.")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1179
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1180
        ();
55286
blanchet
parents: 55202
diff changeset
  1181
      (case run_prover_for_mash ctxt params prover name facts goal of
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1182
        {outcome = NONE, used_facts, ...} =>
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1183
        (if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1184
           let val num_facts = length used_facts in
57017
blanchet
parents: 57014
diff changeset
  1185
             Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
blanchet
parents: 57014
diff changeset
  1186
               plural_s num_facts ^ ".")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1187
           end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1188
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1189
           ();
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
  1190
         (true, map fst used_facts))
55286
blanchet
parents: 55202
diff changeset
  1191
      | _ => (false, isar_deps))
blanchet
parents: 55202
diff changeset
  1192
    end)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1193
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1194
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1195
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1196
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1197
(* 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
  1198
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1199
fun chunks_and_parents_for chunks th =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1200
  let
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1201
    fun insert_parent new parents =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1202
      let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in
57096
e4074b91b2a6 always remove duplicates in meshing + use weights for Naive Bayes
blanchet
parents: 57095
diff changeset
  1203
        parents |> forall (fn p => not (thm_less_eq (new, p))) parents ? cons new
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1204
      end
57006
blanchet
parents: 57005
diff changeset
  1205
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1206
    fun rechunk seen (rest as th' :: ths) =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1207
      if thm_less_eq (th', th) then (rev seen, rest)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1208
      else rechunk (th' :: seen) ths
57006
blanchet
parents: 57005
diff changeset
  1209
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1210
    fun do_chunk [] accum = accum
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1211
      | do_chunk (chunk as hd_chunk :: _) (chunks, parents) =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1212
        if thm_less_eq (hd_chunk, th) then
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1213
          (chunk :: chunks, insert_parent hd_chunk parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1214
        else if thm_less_eq (List.last chunk, th) then
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1215
          let val (front, back as hd_back :: _) = rechunk [] chunk in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1216
            (front :: back :: chunks, insert_parent hd_back parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1217
          end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1218
        else
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1219
          (chunk :: chunks, parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1220
  in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1221
    fold_rev do_chunk chunks ([], [])
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1222
    |>> cons []
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1223
    ||> map nickname_of_thm
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1224
  end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1225
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1226
fun attach_parents_to_facts _ [] = []
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1227
  | 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
  1228
    let
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1229
      fun do_facts _ [] = []
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1230
        | do_facts (_, parents) [fact] = [(parents, fact)]
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1231
        | do_facts (chunks, parents)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1232
                   ((fact as (_, th)) :: (facts as (_, th') :: _)) =
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1233
          let
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1234
            val chunks = app_hd (cons th) chunks
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1235
            val chunks_and_parents' =
57370
9d420da6c7e2 disable 'extra' feature tainting for now
blanchet
parents: 57369
diff changeset
  1236
              if thm_less_eq (th, th') andalso thy_name_of_thm th = thy_name_of_thm th' then
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1237
                (chunks, [nickname_of_thm th])
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1238
              else
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1239
                chunks_and_parents_for chunks th'
57006
blanchet
parents: 57005
diff changeset
  1240
          in
blanchet
parents: 57005
diff changeset
  1241
            (parents, fact) :: do_facts chunks_and_parents' facts
blanchet
parents: 57005
diff changeset
  1242
          end
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1243
    in
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1244
      old_facts @ facts
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1245
      |> do_facts (chunks_and_parents_for [[]] th)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1246
      |> drop (length old_facts)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1247
    end
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1248
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1249
fun maximal_wrt_graph G keys =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1250
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1251
    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
57006
blanchet
parents: 57005
diff changeset
  1252
57012
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1253
    fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name
57006
blanchet
parents: 57005
diff changeset
  1254
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1255
    fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
57006
blanchet
parents: 57005
diff changeset
  1256
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1257
    fun find_maxes _ (maxs, []) = map snd maxs
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1258
      | find_maxes seen (maxs, new :: news) =
57012
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1259
        find_maxes (seen |> num_keys (Graph.imm_succs G new) > 1 ? Symtab.default (new, ()))
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1260
          (if Symtab.defined tab new then
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1261
             let
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1262
               val newp = Graph.all_preds G [new]
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1263
               fun is_ancestor x yp = member (op =) yp x
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1264
               val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp))
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1265
             in
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1266
               if exists (is_ancestor new o fst) maxs then (maxs, news)
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1267
               else ((newp, new) :: filter_out (fn (_, max) => is_ancestor max newp) maxs, news)
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1268
             end
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1269
           else
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1270
             (maxs, Graph.Keys.fold (insert_new seen) (Graph.imm_preds G new) news))
57006
blanchet
parents: 57005
diff changeset
  1271
  in
blanchet
parents: 57005
diff changeset
  1272
    find_maxes Symtab.empty ([], Graph.maximals G)
blanchet
parents: 57005
diff changeset
  1273
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1274
57012
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1275
fun maximal_wrt_access_graph access_G facts =
57013
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1276
  map (nickname_of_thm o snd) facts
57012
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1277
  |> maximal_wrt_graph access_G
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1278
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1279
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
  1280
53197
6c5e7143e1f6 tuned fudge factor in light of evaluation
blanchet
parents: 53159
diff changeset
  1281
val chained_feature_factor = 0.5 (* FUDGE *)
6c5e7143e1f6 tuned fudge factor in light of evaluation
blanchet
parents: 53159
diff changeset
  1282
val extra_feature_factor = 0.1 (* FUDGE *)
57370
9d420da6c7e2 disable 'extra' feature tainting for now
blanchet
parents: 57369
diff changeset
  1283
val num_extra_feature_facts = 0 (* FUDGE *) (* TODO: keep or eliminate? *)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1284
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1285
(* FUDGE *)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1286
fun weight_of_proximity_fact rank =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1287
  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
  1288
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1289
fun weight_facts_smoothly facts =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1290
  facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1291
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1292
(* FUDGE *)
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1293
fun steep_weight_of_fact rank =
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1294
  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
  1295
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1296
fun weight_facts_steeply facts =
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1297
  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
  1298
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1299
val max_proximity_facts = 100
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1300
54060
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1301
fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1302
  let
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1303
    val inter_fact = inter (eq_snd Thm.eq_thm_prop)
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1304
    val raw_mash = find_suggested_facts ctxt facts suggs
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1305
    val proximate = take max_proximity_facts facts
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1306
    val unknown_chained = inter_fact raw_unknown chained
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1307
    val unknown_proximate = inter_fact raw_unknown proximate
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1308
    val mess =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1309
      [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1310
       (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1311
       (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
  1312
    val unknown = raw_unknown
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
  1313
      |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate]
57006
blanchet
parents: 57005
diff changeset
  1314
  in
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1315
    (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
57006
blanchet
parents: 57005
diff changeset
  1316
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1317
53127
60801776d8af weight MaSh constants by frequency
blanchet
parents: 53121
diff changeset
  1318
fun add_const_counts t =
57006
blanchet
parents: 57005
diff changeset
  1319
  fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t [])
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1320
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1321
fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1322
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1323
    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
  1324
    val thy_name = Context.theory_name thy
57052
ea5912e3b008 until naive Bayes supports weights, don't incorporate 'extra' low-weight features
blanchet
parents: 57039
diff changeset
  1325
    val engine = the_mash_engine ()
ea5912e3b008 until naive Bayes supports weights, don't incorporate 'extra' low-weight features
blanchet
parents: 57039
diff changeset
  1326
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
  1327
    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
  1328
    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
  1329
    val num_facts = length facts
57060
7a1167331c8c disable weights that cause more harm than they help in kNN
blanchet
parents: 57059
diff changeset
  1330
57096
e4074b91b2a6 always remove duplicates in meshing + use weights for Naive Bayes
blanchet
parents: 57095
diff changeset
  1331
    (* Weights appear to hurt kNN more than they help. *)
57104
b93e0680a5b3 disabled IDF for now -- empirical evidence points the wrong way (as usual)
blanchet
parents: 57103
diff changeset
  1332
    val const_tab = Symtab.empty |> engine <> MaSh_SML_kNN
b93e0680a5b3 disabled IDF for now -- empirical evidence points the wrong way (as usual)
blanchet
parents: 57103
diff changeset
  1333
      ? fold (add_const_counts o prop_of o snd) facts
54085
b6b41e1d5689 optimized built-in const check
blanchet
parents: 54064
diff changeset
  1334
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
  1335
    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
  1336
      thy_name = Context.theory_name (theory_of_thm th)
56995
61855ade6c7e hide more consts to beautify documentation
blanchet
parents: 56303
diff changeset
  1337
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
  1338
    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
  1339
      [prop_of th]
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1340
      |> 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
  1341
      |> map (apsnd (fn r => weight * factor * r))
54085
b6b41e1d5689 optimized built-in const check
blanchet
parents: 54064
diff changeset
  1342
57017
blanchet
parents: 57014
diff changeset
  1343
    fun query_args access_G =
blanchet
parents: 57014
diff changeset
  1344
      let
blanchet
parents: 57014
diff changeset
  1345
        val parents = maximal_wrt_access_graph access_G facts
blanchet
parents: 57014
diff changeset
  1346
        val hints = chained
blanchet
parents: 57014
diff changeset
  1347
          |> filter (is_fact_in_graph access_G o snd)
blanchet
parents: 57014
diff changeset
  1348
          |> map (nickname_of_thm o snd)
blanchet
parents: 57014
diff changeset
  1349
blanchet
parents: 57014
diff changeset
  1350
        val goal_feats =
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
  1351
          features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
57017
blanchet
parents: 57014
diff changeset
  1352
        val chained_feats = chained
blanchet
parents: 57014
diff changeset
  1353
          |> map (rpair 1.0)
blanchet
parents: 57014
diff changeset
  1354
          |> map (chained_or_extra_features_of chained_feature_factor)
blanchet
parents: 57014
diff changeset
  1355
          |> rpair [] |-> fold (union (eq_fst (op =)))
57052
ea5912e3b008 until naive Bayes supports weights, don't incorporate 'extra' low-weight features
blanchet
parents: 57039
diff changeset
  1356
        val extra_feats =
57095
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
  1357
          facts
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
  1358
          |> take (Int.max (0, num_extra_feature_facts - length chained))
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
  1359
          |> filter fact_has_right_theory
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
  1360
          |> weight_facts_steeply
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
  1361
          |> map (chained_or_extra_features_of extra_feature_factor)
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
  1362
          |> rpair [] |-> fold (union (eq_fst (op =)))
57017
blanchet
parents: 57014
diff changeset
  1363
        val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
blanchet
parents: 57014
diff changeset
  1364
          |> debug ? sort (Real.compare o swap o pairself snd)
blanchet
parents: 57014
diff changeset
  1365
      in
blanchet
parents: 57014
diff changeset
  1366
        (parents, hints, feats)
blanchet
parents: 57014
diff changeset
  1367
      end
blanchet
parents: 57014
diff changeset
  1368
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1369
    val ((access_G, ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs), py_suggs) =
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1370
      peek_state ctxt overlord (fn {access_G, xtabs, ffds, freqs, ...} =>
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1371
        ((access_G, xtabs, ffds, freqs),
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1372
         if Graph.is_empty access_G then
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1373
           (trace_msg ctxt (K "Nothing has been learned yet"); [])
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1374
         else if engine = MaSh_Py then
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1375
           let val (parents, hints, feats) = query_args access_G in
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1376
             MaSh_Py.query ctxt overlord max_suggs ([], hints, parents, feats)
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1377
             |> map fst
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1378
           end
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1379
         else
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1380
           []))
57017
blanchet
parents: 57014
diff changeset
  1381
blanchet
parents: 57014
diff changeset
  1382
    val sml_suggs =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1383
      if engine = MaSh_Py then
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1384
        []
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1385
      else
57103
blanchet
parents: 57102
diff changeset
  1386
        let
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1387
          val (parents, hints, goal_feats0) = query_args access_G
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1388
          val goal_feats = map fst goal_feats0
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1389
          val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
57103
blanchet
parents: 57102
diff changeset
  1390
        in
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1391
          if engine = MaSh_SML_kNN_Ext orelse engine = MaSh_SML_NB_Ext then
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1392
            let
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1393
              val learns =
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1394
                Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1395
            in
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1396
              MaSh_SML.query_external ctxt engine max_suggs learns goal_feats
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1397
            end
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1398
          else
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1399
            let
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1400
              val int_goal_feats = map_filter (Symtab.lookup feat_tab) goal_feats
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1401
            in
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1402
              MaSh_SML.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1403
                max_suggs goal_feats int_goal_feats
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1404
            end
57017
blanchet
parents: 57014
diff changeset
  1405
        end
blanchet
parents: 57014
diff changeset
  1406
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1407
    val unknown = filter_out (is_fact_in_graph access_G o snd) facts
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1408
  in
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
  1409
    find_mash_suggestions ctxt max_suggs (py_suggs @ sml_suggs) facts chained unknown
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1410
    |> pairself (map fact_of_raw_fact)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1411
  end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1412
57381
blanchet
parents: 57380
diff changeset
  1413
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (access_G, (fact_xtab, feat_xtab)) =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1414
  let
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1415
    fun maybe_learn_from from (accum as (parents, access_G)) =
57013
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1416
      try_graph ctxt "updating graph" accum (fn () =>
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1417
        (from :: parents, Graph.add_edge_acyclic (from, name) access_G))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1418
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1419
    val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1420
    val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1421
    val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1422
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1423
    val fact_xtab = maybe_add_to_xtab name fact_xtab
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1424
    val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
57006
blanchet
parents: 57005
diff changeset
  1425
  in
57381
blanchet
parents: 57380
diff changeset
  1426
    ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
57006
blanchet
parents: 57005
diff changeset
  1427
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1428
57381
blanchet
parents: 57380
diff changeset
  1429
fun relearn_wrt_access_graph ctxt (name, deps) access_G =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1430
  let
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1431
    fun maybe_relearn_from from (accum as (parents, access_G)) =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1432
      try_graph ctxt "updating graph" accum (fn () =>
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1433
        (from :: parents, Graph.add_edge_acyclic (from, name) access_G))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1434
    val access_G =
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1435
      access_G |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1436
    val (deps, _) = ([], access_G) |> fold maybe_relearn_from deps
57006
blanchet
parents: 57005
diff changeset
  1437
  in
57381
blanchet
parents: 57380
diff changeset
  1438
    ((name, deps), access_G)
57006
blanchet
parents: 57005
diff changeset
  1439
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1440
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1441
fun flop_wrt_access_graph name =
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1442
  Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps))
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1443
57273
01b68f625550 automatically learn MaSh facts also in 'blocking' mode
blanchet
parents: 57150
diff changeset
  1444
val learn_timeout_slack = 20.0
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1445
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1446
fun launch_thread timeout task =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1447
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1448
    val hard_timeout = time_mult learn_timeout_slack timeout
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1449
    val birth_time = Time.now ()
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1450
    val death_time = Time.+ (birth_time, hard_timeout)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1451
    val desc = ("Machine learner for Sledgehammer", "")
57006
blanchet
parents: 57005
diff changeset
  1452
  in
blanchet
parents: 57005
diff changeset
  1453
    Async_Manager.thread MaShN birth_time death_time desc task
blanchet
parents: 57005
diff changeset
  1454
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1455
57013
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1456
fun learned_proof_name () =
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1457
  Date.fmt ".%Y%m%d.%H%M%S." (Date.fromTimeLocal (Time.now ())) ^ serial_string ()
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1458
54503
blanchet
parents: 54432
diff changeset
  1459
fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths =
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1460
  if is_mash_enabled () then
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1461
    launch_thread timeout (fn () =>
57006
blanchet
parents: 57005
diff changeset
  1462
      let
blanchet
parents: 57005
diff changeset
  1463
        val thy = Proof_Context.theory_of ctxt
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
  1464
        val feats = map fst (features_of ctxt thy 0 Symtab.empty (Local, General) [t])
57006
blanchet
parents: 57005
diff changeset
  1465
      in
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1466
        map_state ctxt overlord
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
  1467
          (fn state as {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1468
             let
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1469
               val parents = maximal_wrt_access_graph access_G facts
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1470
               val deps = used_ths
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1471
                 |> filter (is_fact_in_graph access_G)
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1472
                 |> map nickname_of_thm
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1473
             in
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1474
               if the_mash_engine () = MaSh_Py then
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1475
                 (MaSh_Py.learn ctxt overlord true [("", parents, feats, deps)]; state)
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1476
               else
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1477
                 let
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1478
                   val name = learned_proof_name ()
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
  1479
                   val (access_G', xtabs', rev_learns) =
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
  1480
                     add_node Automatic_Proof name parents feats deps (access_G, xtabs, [])
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1481
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
  1482
                   val (ffds', freqs') =
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
  1483
                     recompute_ffds_freqs_from_learns (rev rev_learns) xtabs' num_facts0 ffds freqs
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1484
                 in
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1485
                   {access_G = access_G', xtabs = xtabs', ffds = ffds', freqs = freqs',
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1486
                    dirty_facts = Option.map (cons name) dirty_facts}
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1487
                 end
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1488
             end);
57006
blanchet
parents: 57005
diff changeset
  1489
        (true, "")
blanchet
parents: 57005
diff changeset
  1490
      end)
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1491
  else
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1492
    ()
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1493
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
  1494
fun sendback sub = 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
  1495
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1496
val commit_timeout = seconds 30.0
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
  1497
50485
3c6ac2da2f45 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents: 50484
diff changeset
  1498
(* The timeout is understood in a very relaxed fashion. *)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1499
fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover save auto_level
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1500
    run_prover learn_timeout facts =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1501
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1502
    val timer = Timer.startRealTimer ()
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1503
    fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1504
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1505
    val engine = the_mash_engine ()
57372
24738b4f8c6b removed experimental machine learning engine
blanchet
parents: 57371
diff changeset
  1506
    val {access_G, ...} = peek_state ctxt overlord I
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1507
    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
  1508
    val no_new_facts = forall is_in_access_G facts
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1509
  in
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1510
    if no_new_facts andalso not run_prover then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1511
      if auto_level < 2 then
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1512
        "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^
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
  1513
        (if auto_level = 0 andalso not run_prover then
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1514
           "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1515
         else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1516
           "")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1517
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1518
        ""
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1519
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1520
      let
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1521
        val name_tabs = build_name_tables nickname_of_thm facts
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1522
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1523
        fun deps_of status th =
57017
blanchet
parents: 57014
diff changeset
  1524
          if status = Non_Rec_Def orelse status = Rec_Def then
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1525
            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
  1526
          else if run_prover then
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1527
            prover_dependencies_of ctxt params prover auto_level facts name_tabs th
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1528
            |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1529
          else
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1530
            isar_dependencies_of name_tabs th
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1531
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1532
        fun do_commit [] [] [] state = state
57382
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1533
          | do_commit learns relearns flops
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1534
              {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1535
            let
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1536
              val was_empty = Graph.is_empty access_G
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1537
57374
blanchet
parents: 57373
diff changeset
  1538
              val (learns, (access_G, xtabs)) =
57381
blanchet
parents: 57380
diff changeset
  1539
                fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1540
              val (relearns, access_G) =
57381
blanchet
parents: 57380
diff changeset
  1541
                fold_map (relearn_wrt_access_graph ctxt) relearns access_G
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1542
50610
d9c4fbbb0c11 name tuning
blanchet
parents: 50608
diff changeset
  1543
              val access_G = access_G |> fold flop_wrt_access_graph flops
57365
blanchet
parents: 57364
diff changeset
  1544
              val dirty_facts =
blanchet
parents: 57364
diff changeset
  1545
                (case (was_empty, dirty_facts) of
57062
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1546
                  (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
55286
blanchet
parents: 55202
diff changeset
  1547
                | _ => NONE)
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1548
57382
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1549
              val (ffds', freqs') =
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1550
                if null relearns then
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1551
                  recompute_ffds_freqs_from_learns
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1552
                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs num_facts0
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1553
                    ffds freqs
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1554
                else
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1555
                  recompute_ffds_freqs_from_access_G access_G xtabs
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1556
            in
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1557
              if engine = MaSh_Py then
57381
blanchet
parents: 57380
diff changeset
  1558
                (MaSh_Py.learn ctxt overlord (save andalso null relearns) learns;
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1559
                 MaSh_Py.relearn ctxt overlord save relearns)
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
  1560
              else
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1561
                ();
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1562
              {access_G = access_G, xtabs = xtabs, ffds = ffds', freqs = freqs',
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1563
               dirty_facts = dirty_facts}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1564
            end
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1565
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1566
        fun commit last learns relearns flops =
57017
blanchet
parents: 57014
diff changeset
  1567
          (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
  1568
           map_state ctxt overlord (do_commit (rev learns) relearns flops);
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1569
           if not last andalso auto_level = 0 then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1570
             let val num_proofs = length learns + length relearns in
57017
blanchet
parents: 57014
diff changeset
  1571
               Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
blanchet
parents: 57014
diff changeset
  1572
                 (if run_prover then "automatic" else "Isar") ^ " proof" ^
blanchet
parents: 57014
diff changeset
  1573
                 plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1574
             end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1575
           else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1576
             ())
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1577
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1578
        fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1579
          | learn_new_fact (parents, ((_, stature as (_, status)), th))
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1580
              (learns, (n, next_commit, _)) =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1581
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1582
              val name = nickname_of_thm th
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
  1583
              val feats =
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
  1584
                map fst (features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th])
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1585
              val deps = deps_of status th |> these
48394
82fc8c956cdc fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
blanchet
parents: 48392
diff changeset
  1586
              val n = n |> not (null deps) ? Integer.add 1
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1587
              val learns = (name, parents, feats, deps) :: learns
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1588
              val (learns, next_commit) =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1589
                if Time.> (Timer.checkRealTimer timer, next_commit) then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1590
                  (commit false learns [] []; ([], next_commit_time ()))
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1591
                else
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1592
                  (learns, next_commit)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1593
              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1594
            in
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1595
              (learns, (n, next_commit, timed_out))
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1596
            end
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1597
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1598
        val n =
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1599
          if no_new_facts then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1600
            0
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1601
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1602
            let
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1603
              val new_facts = facts
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1604
                |> sort (crude_thm_ord o pairself snd)
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1605
                |> attach_parents_to_facts []
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1606
                |> filter_out (is_in_access_G o snd)
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1607
              val (learns, (n, _, _)) =
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1608
                ([], (0, next_commit_time (), false))
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1609
                |> fold learn_new_fact new_facts
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1610
            in
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1611
              commit true learns [] []; n
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1612
            end
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1613
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1614
        fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1615
          | relearn_old_fact ((_, (_, status)), th) ((relearns, flops), (n, next_commit, _)) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1616
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1617
              val name = nickname_of_thm th
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1618
              val (n, relearns, flops) =
55286
blanchet
parents: 55202
diff changeset
  1619
                (case deps_of status th of
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1620
                  SOME deps => (n + 1, (name, deps) :: relearns, flops)
55286
blanchet
parents: 55202
diff changeset
  1621
                | NONE => (n, relearns, name :: flops))
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1622
              val (relearns, flops, next_commit) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1623
                if Time.> (Timer.checkRealTimer timer, next_commit) then
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1624
                  (commit false [] relearns flops; ([], [], next_commit_time ()))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1625
                else
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1626
                  (relearns, flops, next_commit)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1627
              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1628
            in
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1629
              ((relearns, flops), (n, next_commit, timed_out))
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1630
            end
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1631
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1632
        val n =
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1633
          if not run_prover then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1634
            n
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1635
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1636
            let
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
  1637
              val max_isar = 1000 * max_dependencies
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1638
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1639
              fun priority_of th =
57062
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1640
                random_range 0 max_isar +
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1641
                (case try (Graph.get_node access_G) (nickname_of_thm th) of
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1642
                  SOME (Isar_Proof, _, deps) => ~100 * length deps
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1643
                | SOME (Automatic_Proof, _, _) => 2 * max_isar
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1644
                | SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1645
                | NONE => 0)
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1646
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1647
              val old_facts = facts
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1648
                |> filter is_in_access_G
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1649
                |> map (`(priority_of o snd))
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1650
                |> sort (int_ord o pairself fst)
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1651
                |> map snd
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1652
              val ((relearns, flops), (n, _, _)) =
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1653
                (([], []), (n, next_commit_time (), false))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1654
                |> fold relearn_old_fact old_facts
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1655
            in
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1656
              commit true [] relearns flops; n
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1657
            end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1658
      in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1659
        if verbose orelse auto_level < 2 then
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1660
          "Learned " ^ string_of_int n ^ " nontrivial " ^
54140
564b8adb0952 clarified message
blanchet
parents: 54131
diff changeset
  1661
          (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
57006
blanchet
parents: 57005
diff changeset
  1662
          (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") ^ "."
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1663
        else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1664
          ""
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1665
      end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1666
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1667
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
  1668
fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1669
  let
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
  1670
    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
48395
85a7fb65507a learning should honor the fact override and the chained facts
blanchet
parents: 48394
diff changeset
  1671
    val ctxt = ctxt |> Config.put instantiate_inducts false
57006
blanchet
parents: 57005
diff changeset
  1672
    val facts = nearly_all_facts ctxt false fact_override Symtab.empty css chained [] @{prop True}
54115
2b7e063c7abc improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance
blanchet
parents: 54100
diff changeset
  1673
      |> sort (crude_thm_ord o pairself snd o swap)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1674
    val num_facts = length facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1675
    val prover = hd provers
57006
blanchet
parents: 57005
diff changeset
  1676
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
  1677
    fun learn auto_level run_prover =
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1678
      mash_learn_facts ctxt params prover true auto_level run_prover one_year facts
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1679
      |> Output.urgent_message
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1680
  in
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
  1681
    if run_prover then
57017
blanchet
parents: 57014
diff changeset
  1682
      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
blanchet
parents: 57014
diff changeset
  1683
         plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
blanchet
parents: 57014
diff changeset
  1684
         string_of_time timeout ^ ").\n\nCollecting Isar proofs first...");
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1685
       learn 1 false;
57017
blanchet
parents: 57014
diff changeset
  1686
       Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
blanchet
parents: 57014
diff changeset
  1687
         \can safely stop the learning process at any point.";
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1688
       learn 0 true)
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1689
    else
57006
blanchet
parents: 57005
diff changeset
  1690
      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
blanchet
parents: 57005
diff changeset
  1691
         plural_s num_facts ^ " for Isar proofs...");
50340
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1692
       learn 0 false)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1693
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
  1694
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
  1695
fun mash_can_suggest_facts ctxt overlord =
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
  1696
  not (Graph.is_empty (#access_G (peek_state ctxt overlord I)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
  1697
57274
0acfdb151e52 more generous formula -- there are lots of duplicates out there
blanchet
parents: 57273
diff changeset
  1698
(* Generate more suggestions than requested, because some might be thrown out later for various
0acfdb151e52 more generous formula -- there are lots of duplicates out there
blanchet
parents: 57273
diff changeset
  1699
   reasons (e.g., duplicates). *)
0acfdb151e52 more generous formula -- there are lots of duplicates out there
blanchet
parents: 57273
diff changeset
  1700
fun generous_max_suggestions max_facts = 3 * max_facts div 2 + 25
50383
4274b25ff4e7 take proximity into account for MaSh + fix a debilitating bug in feature generation
blanchet
parents: 50382
diff changeset
  1701
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1702
val mepo_weight = 0.5
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1703
val mash_weight = 0.5
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1704
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1705
val max_facts_to_learn_before_query = 100
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1706
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1707
(* The threshold should be large enough so that MaSh does not get activated for Auto Sledgehammer
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1708
   and Try. *)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1709
val min_secs_for_learning = 15
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1710
57361
blanchet
parents: 57360
diff changeset
  1711
fun relevant_facts ctxt (params as {overlord, learn, fact_filter, timeout, ...}) prover max_facts
blanchet
parents: 57360
diff changeset
  1712
    ({add, only, ...} : fact_override) hyp_ts concl_t facts =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1713
  if not (subset (op =) (the_list fact_filter, fact_filters)) then
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1714
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1715
  else if only then
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1716
    [("", map fact_of_raw_fact facts)]
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
  1717
  else if max_facts <= 0 orelse null facts then
51010
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
  1718
    [("", [])]
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1719
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1720
    let
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1721
      fun maybe_launch_thread () =
57273
01b68f625550 automatically learn MaSh facts also in 'blocking' mode
blanchet
parents: 57150
diff changeset
  1722
        if not (Async_Manager.has_running_threads MaShN) andalso
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1723
           Time.toSeconds timeout >= min_secs_for_learning then
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1724
          let val timeout = time_mult learn_timeout_slack timeout in
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1725
            launch_thread timeout
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1726
              (fn () => (true, mash_learn_facts ctxt params prover true 2 false timeout facts))
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1727
          end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1728
        else
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1729
          ()
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1730
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1731
      fun maybe_learn () =
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1732
        if is_mash_enabled () andalso learn then
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1733
          let
57377
73e9b858ec8d imported patch killed_num_known_facts0
blanchet
parents: 57376
diff changeset
  1734
            val {access_G, xtabs = ((num_facts0, _), _), ...} = peek_state ctxt overlord I
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1735
            val is_in_access_G = is_fact_in_graph access_G o snd
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1736
          in
57377
73e9b858ec8d imported patch killed_num_known_facts0
blanchet
parents: 57376
diff changeset
  1737
            if length facts - num_facts0 <= max_facts_to_learn_before_query then
55286
blanchet
parents: 55202
diff changeset
  1738
              (case length (filter_out is_in_access_G facts) of
54012
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1739
                0 => false
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1740
              | num_facts_to_learn =>
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1741
                if num_facts_to_learn <= max_facts_to_learn_before_query then
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1742
                  (mash_learn_facts ctxt params prover false 2 false timeout facts
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1743
                   |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s));
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1744
                   true)
7a8263843acb removed spurious save if nothing needs to bee learned
blanchet
parents: 53819
diff changeset
  1745
                else
55286
blanchet
parents: 55202
diff changeset
  1746
                  (maybe_launch_thread (); false))
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1747
            else
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1748
              (maybe_launch_thread (); false)
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1749
          end
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1750
        else
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1751
          false
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1752
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1753
      val (save, effective_fact_filter) =
55286
blanchet
parents: 55202
diff changeset
  1754
        (case fact_filter of
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1755
          SOME ff => (ff <> mepoN andalso maybe_learn (), ff)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1756
        | NONE =>
51024
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51020
diff changeset
  1757
          if is_mash_enabled () then
57107
2d502370ee99 changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
blanchet
parents: 57106
diff changeset
  1758
            (maybe_learn (), if mash_can_suggest_facts ctxt overlord then meshN else mepoN)
48407
47fe0ca12fc2 faster maximal node computation
blanchet
parents: 48406
diff changeset
  1759
          else
55286
blanchet
parents: 55202
diff changeset
  1760
            (false, mepoN))
54143
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1761
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1762
      val unique_facts = drop_duplicate_facts facts
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1763
      val add_ths = Attrib.eval_thms ctxt add
54143
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1764
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
  1765
      fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1766
51003
198cb05fb35b report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents: 51001
diff changeset
  1767
      fun add_and_take accepts =
198cb05fb35b report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents: 51001
diff changeset
  1768
        (case add_ths of
198cb05fb35b report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents: 51001
diff changeset
  1769
           [] => accepts
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1770
         | _ =>
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1771
           (unique_facts |> filter in_add |> map fact_of_raw_fact) @ (accepts |> filter_out in_add))
48293
914ca0827804 renamed Sledgehammer options
blanchet
parents: 48292
diff changeset
  1772
        |> take max_facts
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1773
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
  1774
      fun mepo () =
54143
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1775
        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
54091
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1776
         |> weight_facts_steeply, [])
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1777
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1778
      fun mash () =
57108
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57107
diff changeset
  1779
        mash_suggested_facts ctxt params (generous_max_suggestions max_facts) hyp_ts concl_t facts
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1780
        |>> weight_facts_steeply
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1781
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1782
      val mess =
51003
198cb05fb35b report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents: 51001
diff changeset
  1783
        (* the order is important for the "case" expression below *)
54091
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1784
        [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1785
           |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo)
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1786
           |> Par_List.map (apsnd (fn f => f ()))
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1787
      val mesh = mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess |> add_and_take
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1788
    in
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1789
      if the_mash_engine () = MaSh_Py andalso save then MaSh_Py.save ctxt overlord else ();
55286
blanchet
parents: 55202
diff changeset
  1790
      (case (fact_filter, mess) of
51024
98fb341d32e3 distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
blanchet
parents: 51020
diff changeset
  1791
        (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
51010
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
  1792
        [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
  1793
         (mashN, mash |> map fst |> add_and_take)]
55286
blanchet
parents: 55202
diff changeset
  1794
      | _ => [(effective_fact_filter, mesh)])
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1795
    end
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1796
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
  1797
fun kill_learners ctxt ({overlord, ...} : params) =
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
  1798
  (Async_Manager.kill_threads MaShN "learner";
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
  1799
   if the_mash_engine () = MaSh_Py then MaSh_Py.shutdown ctxt overlord else ())
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1800
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1801
fun running_learners () = Async_Manager.running_threads MaShN "learner"
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1802
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
  1803
end;