src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
author blanchet
Thu, 24 Jul 2014 18:46:38 +0200
changeset 57658 f55c173a3cbc
parent 57574 e4ddd52e1b96
child 57660 86b853448f08
permissions -rw-r--r--
beware of duplicate fact names
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
50632
12c097ff3241 slightly more elegant naming convention (to keep low-level and high-level APIs separated)
blanchet
parents: 50631
diff changeset
    35
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
    36
  datatype mash_algorithm =
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
    37
    MaSh_NB
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
    38
  | MaSh_kNN
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
    39
  | MaSh_NB_kNN
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
    40
  | MaSh_NB_Ext
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
    41
  | MaSh_kNN_Ext
57106
52e1e424eec1 export more ML functions, for experimentation
blanchet
parents: 57104
diff changeset
    42
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    43
  val is_mash_enabled : unit -> bool
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
    44
  val the_mash_algorithm : unit -> mash_algorithm
57557
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
    45
  val str_of_mash_algorithm : mash_algorithm -> string
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    46
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
    47
  val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
    48
  val nickname_of_thm : thm -> string
57006
blanchet
parents: 57005
diff changeset
    49
  val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
    50
  val crude_thm_ord : thm * thm -> order
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
    51
  val thm_less : thm * thm -> bool
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    52
  val goal_of_thm : theory -> thm -> thm
57006
blanchet
parents: 57005
diff changeset
    53
  val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
blanchet
parents: 57005
diff changeset
    54
    prover_result
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
    55
  val features_of : Proof.context -> theory -> stature -> term list -> string list
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
    56
  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
    57
  val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
57006
blanchet
parents: 57005
diff changeset
    58
  val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
blanchet
parents: 57005
diff changeset
    59
    string Symtab.table * string Symtab.table -> thm -> bool * string list
blanchet
parents: 57005
diff changeset
    60
  val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
blanchet
parents: 57005
diff changeset
    61
    (string list * ('a * thm)) list
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    62
  val num_extra_feature_facts : int
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
    63
  val extra_feature_factor : real
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
    64
  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
    65
  val weight_facts_steeply : 'a list -> ('a * real) list
57432
blanchet
parents: 57431
diff changeset
    66
  val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list ->
blanchet
parents: 57431
diff changeset
    67
    ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
57407
140e16bc2a40 use right theory name for theorems in evaluation driver
blanchet
parents: 57406
diff changeset
    68
  val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term ->
140e16bc2a40 use right theory name for theorems in evaluation driver
blanchet
parents: 57406
diff changeset
    69
    raw_fact list -> fact list * fact list
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
    70
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
    71
  val mash_unlearn : unit -> unit
54503
blanchet
parents: 54432
diff changeset
    72
  val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
    73
  val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time ->
57120
f8112c4b9cb8 extend exporter with new versions of MaSh
blanchet
parents: 57108
diff changeset
    74
    raw_fact list -> string
57006
blanchet
parents: 57005
diff changeset
    75
  val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
57432
blanchet
parents: 57431
diff changeset
    76
  val mash_can_suggest_facts : Proof.context -> bool
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
    77
57108
dc0b4f50e288 more generous max number of suggestions, for more safety
blanchet
parents: 57107
diff changeset
    78
  val generous_max_suggestions : int -> int
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    79
  val mepo_weight : real
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
    80
  val mash_weight : real
57006
blanchet
parents: 57005
diff changeset
    81
  val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
blanchet
parents: 57005
diff changeset
    82
    term -> raw_fact list -> (string * fact list) list
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
    83
  val kill_learners : unit -> unit
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
    84
  val running_learners : unit -> unit
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    85
end;
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    86
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    87
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
    88
struct
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
    89
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    90
open ATP_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    91
open ATP_Problem_Generate
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    92
open Sledgehammer_Util
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    93
open Sledgehammer_Fact
55201
1ee776da8da7 renamed ML file
blanchet
parents: 54816
diff changeset
    94
open Sledgehammer_Prover
55202
824c48a539c9 renamed many Sledgehammer ML files to clarify structure
blanchet
parents: 55201
diff changeset
    95
open Sledgehammer_Prover_Minimize
48381
1b7d798460bb renamed ML structures
blanchet
parents: 48380
diff changeset
    96
open Sledgehammer_MePo
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
    97
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
    98
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
    99
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
   100
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   101
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
   102
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
   103
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
   104
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   105
val MePoN = "MePo"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   106
val MaShN = "MaSh"
51008
e096c0dc538b more precise output of selected facts
blanchet
parents: 51007
diff changeset
   107
val MeShN = "MeSh"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
   108
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   109
val mepoN = "mepo"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   110
val mashN = "mash"
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   111
val meshN = "mesh"
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   112
48379
2b5ad61e2ccc renamed "iter" fact filter to "MePo" (Meng--Paulson)
blanchet
parents: 48378
diff changeset
   113
val fact_filters = [meshN, mepoN, mashN]
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
   114
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   115
val unlearnN = "unlearn"
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   116
val learn_isarN = "learn_isar"
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   117
val learn_proverN = "learn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   118
val relearn_isarN = "relearn_isar"
50484
8ec31bdb9d36 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
blanchet
parents: 50450
diff changeset
   119
val relearn_proverN = "relearn_prover"
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   120
57368
blanchet
parents: 57367
diff changeset
   121
fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
blanchet
parents: 57367
diff changeset
   122
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   123
type xtab = int * int Symtab.table
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   124
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   125
val empty_xtab = (0, Symtab.empty)
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
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
   128
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
   129
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   130
fun state_file () = Path.expand (Path.explode "$ISABELLE_HOME_USER/mash_state")
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   131
val remove_state_file = try File.rm o state_file
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   132
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   133
datatype mash_algorithm =
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   134
  MaSh_NB
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   135
| MaSh_kNN
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   136
| MaSh_NB_kNN
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   137
| MaSh_NB_Ext
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   138
| MaSh_kNN_Ext
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   139
57554
12fb55fc11a6 no warning in case MaSh is disabled
blanchet
parents: 57552
diff changeset
   140
(* TODO: eliminate "MASH" environment variable after Isabelle2014 release *)
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   141
fun mash_algorithm () =
57089
353652f47974 renamed 'MaSh' option
blanchet
parents: 57076
diff changeset
   142
  let val flag1 = Options.default_string @{system_option MaSh} in
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   143
    (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
57462
dabd4516450d changed default MaSh engine
blanchet
parents: 57461
diff changeset
   144
      "yes" => SOME MaSh_NB_kNN
dabd4516450d changed default MaSh engine
blanchet
parents: 57461
diff changeset
   145
    | "sml" => SOME MaSh_NB_kNN
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   146
    | "nb" => SOME MaSh_NB
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   147
    | "knn" => SOME MaSh_kNN
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   148
    | "nb_knn" => SOME MaSh_NB_kNN
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   149
    | "nb_ext" => SOME MaSh_NB_Ext
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   150
    | "knn_ext" => SOME MaSh_kNN_Ext
57554
12fb55fc11a6 no warning in case MaSh is disabled
blanchet
parents: 57552
diff changeset
   151
    | "" => NONE
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   152
    | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
57028
e5466055e94f added Isabelle system option 'mash'
blanchet
parents: 57018
diff changeset
   153
  end
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
   154
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   155
val is_mash_enabled = is_some o mash_algorithm
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   156
val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
   157
57557
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
   158
fun str_of_mash_algorithm MaSh_NB = "nb"
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
   159
  | str_of_mash_algorithm MaSh_kNN = "knn"
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
   160
  | str_of_mash_algorithm MaSh_NB_kNN = "nb_knn"
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
   161
  | str_of_mash_algorithm MaSh_NB_Ext = "nb_ext"
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
   162
  | str_of_mash_algorithm MaSh_kNN_Ext = "knn_ext"
242ce8d3d16b record MaSh algorithm in spying data
blanchet
parents: 57555
diff changeset
   163
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   164
fun scaled_avg [] = 0
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   165
  | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   166
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   167
fun avg [] = 0.0
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   168
  | avg xs = fold (curry (op +)) xs 0.0 / Real.fromInt (length xs)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   169
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   170
fun normalize_scores _ [] = []
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   171
  | normalize_scores max_facts xs =
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   172
    map (apsnd (curry Real.* (1.0 / avg (map snd (take max_facts xs))))) xs
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   173
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   174
fun mesh_facts fact_eq max_facts [(_, (sels, unks))] =
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   175
    distinct fact_eq (map fst (take max_facts sels) @ take (max_facts - length sels) unks)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   176
  | mesh_facts fact_eq max_facts mess =
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   177
    let
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   178
      val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   179
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   180
      fun score_in fact (global_weight, (sels, unks)) =
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   181
        let val score_at = try (nth sels) #> Option.map (fn (_, score) => global_weight * score) in
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   182
          (case find_index (curry fact_eq fact o fst) sels of
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   183
            ~1 => if member fact_eq unks fact then NONE else SOME 0.0
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   184
          | rank => score_at rank)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   185
        end
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   186
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   187
      fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   188
    in
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   189
      fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   190
      |> map (`weight_of) |> sort (int_ord o pairself fst o swap)
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   191
      |> map snd |> take max_facts
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   192
    end
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   193
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   194
fun smooth_weight_of_fact rank = Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 (* FUDGE *)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   195
fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   196
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   197
fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   198
fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   199
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   200
fun rev_sort_array_prefix cmp bnd a =
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   201
  let
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
   202
    exception BOTTOM of int
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
   203
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   204
    val al = Array.length a
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   205
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   206
    fun maxson l i =
57017
blanchet
parents: 57014
diff changeset
   207
      let val i31 = i + i + i + 1 in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   208
        if i31 + 2 < l then
57017
blanchet
parents: 57014
diff changeset
   209
          let val x = Unsynchronized.ref i31 in
blanchet
parents: 57014
diff changeset
   210
            if cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS then x := i31 + 1 else ();
blanchet
parents: 57014
diff changeset
   211
            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
   212
            !x
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   213
          end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   214
        else
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   215
          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
   216
          then i31 + 1 else if i31 < l then i31 else raise BOTTOM i
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   217
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   218
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   219
    fun trickledown l i e =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   220
      let val j = maxson l i in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   221
        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
   222
          (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
   223
        else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   224
          Array.update (a, i, e)
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   225
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   226
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   227
    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
   228
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   229
    fun bubbledown l i =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   230
      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
   231
        Array.update (a, i, Array.sub (a, j));
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   232
        bubbledown l j
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   233
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   234
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   235
    fun bubble l i = bubbledown l i handle BOTTOM i => i
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   236
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   237
    fun trickleup i e =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   238
      let val father = (i - 1) div 3 in
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   239
        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
   240
          (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
   241
           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
   242
        else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   243
          Array.update (a, i, e)
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   244
      end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   245
57355
blanchet
parents: 57354
diff changeset
   246
    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
   247
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   248
    fun for2 i =
57355
blanchet
parents: 57354
diff changeset
   249
      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
   250
        ()
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   251
      else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   252
        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
   253
          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
   254
          trickleup (bubble i 0) e;
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   255
          for2 (i - 1)
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   256
        end
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   257
  in
57355
blanchet
parents: 57354
diff changeset
   258
    for (((al + 1) div 3) - 1);
blanchet
parents: 57354
diff changeset
   259
    for2 (al - 1);
blanchet
parents: 57354
diff changeset
   260
    if al > 1 then
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   261
      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
   262
        Array.update (a, 1, Array.sub (a, 0));
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   263
        Array.update (a, 0, e)
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   264
      end
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   265
    else
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   266
      ()
57009
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   267
  end
8cb6a5f1ae84 added SML implementation of MaSh
blanchet
parents: 57007
diff changeset
   268
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   269
fun rev_sort_list_prefix cmp bnd xs =
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   270
  let val ary = Array.fromList xs in
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   271
    rev_sort_array_prefix cmp bnd ary;
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   272
    Array.foldr (op ::) [] ary
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   273
  end
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   274
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   275
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   276
(*** Isabelle-agnostic machine learning ***)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   277
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   278
structure MaSh =
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   279
struct
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   280
57574
e4ddd52e1b96 made SML/NJ happier
blanchet
parents: 57561
diff changeset
   281
fun select_visible_facts (big_number : real) recommends =
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   282
  List.app (fn at =>
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   283
    let val (j, ov) = Array.sub (recommends, at) in
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   284
      Array.update (recommends, at, (j, big_number + ov))
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   285
    end)
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   286
57374
blanchet
parents: 57373
diff changeset
   287
fun wider_array_of_vector init vec =
blanchet
parents: 57373
diff changeset
   288
  let val ary = Array.array init in
blanchet
parents: 57373
diff changeset
   289
    Array.copyVec {src = vec, dst = ary, di = 0};
blanchet
parents: 57373
diff changeset
   290
    ary
blanchet
parents: 57373
diff changeset
   291
  end
blanchet
parents: 57373
diff changeset
   292
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   293
val nb_def_prior_weight = 1000 (* FUDGE *)
57095
001ec97c3e59 updated naive Bayes
blanchet
parents: 57089
diff changeset
   294
57374
blanchet
parents: 57373
diff changeset
   295
fun learn_facts (tfreq0, sfreq0, dffreq0) num_facts0 num_facts num_feats depss featss =
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   296
  let
57374
blanchet
parents: 57373
diff changeset
   297
    val tfreq = wider_array_of_vector (num_facts, 0) tfreq0
blanchet
parents: 57373
diff changeset
   298
    val sfreq = wider_array_of_vector (num_facts, Inttab.empty) sfreq0
blanchet
parents: 57373
diff changeset
   299
    val dffreq = wider_array_of_vector (num_feats, 0) dffreq0
blanchet
parents: 57373
diff changeset
   300
blanchet
parents: 57373
diff changeset
   301
    fun learn_one th feats deps =
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   302
      let
57355
blanchet
parents: 57354
diff changeset
   303
        fun add_th weight t =
blanchet
parents: 57354
diff changeset
   304
          let
blanchet
parents: 57354
diff changeset
   305
            val im = Array.sub (sfreq, t)
57374
blanchet
parents: 57373
diff changeset
   306
            fun fold_fn s = Inttab.map_default (s, 0) (Integer.add weight)
57355
blanchet
parents: 57354
diff changeset
   307
          in
57368
blanchet
parents: 57367
diff changeset
   308
            map_array_at tfreq (Integer.add weight) t;
57355
blanchet
parents: 57354
diff changeset
   309
            Array.update (sfreq, t, fold fold_fn feats im)
blanchet
parents: 57354
diff changeset
   310
          end
blanchet
parents: 57354
diff changeset
   311
57368
blanchet
parents: 57367
diff changeset
   312
        val add_sym = map_array_at dffreq (Integer.add 1)
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   313
      in
57355
blanchet
parents: 57354
diff changeset
   314
        add_th nb_def_prior_weight th;
blanchet
parents: 57354
diff changeset
   315
        List.app (add_th 1) deps;
blanchet
parents: 57354
diff changeset
   316
        List.app add_sym feats
57354
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   317
      end
ded92100ffd7 refactoring
blanchet
parents: 57353
diff changeset
   318
57102
blanchet
parents: 57101
diff changeset
   319
    fun for i =
57383
ba0fe0639bc8 right array indexing
blanchet
parents: 57382
diff changeset
   320
      if i = num_facts then ()
ba0fe0639bc8 right array indexing
blanchet
parents: 57382
diff changeset
   321
      else (learn_one i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1))
57102
blanchet
parents: 57101
diff changeset
   322
  in
57383
ba0fe0639bc8 right array indexing
blanchet
parents: 57382
diff changeset
   323
    for num_facts0;
57374
blanchet
parents: 57373
diff changeset
   324
    (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq)
57102
blanchet
parents: 57101
diff changeset
   325
  end
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   326
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   327
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
   328
  let
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   329
    val tau = 0.2 (* FUDGE *)
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   330
    val pos_weight = 5.0 (* FUDGE *)
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   331
    val def_val = ~18.0 (* FUDGE *)
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   332
    val init_val = 30.0 (* FUDGE *)
57124
e4c2c792226f make SML naive Bayes closer to Python version
blanchet
parents: 57122
diff changeset
   333
57366
blanchet
parents: 57365
diff changeset
   334
    val ln_afreq = Math.ln (Real.fromInt num_facts)
57374
blanchet
parents: 57373
diff changeset
   335
    val idf = Vector.map (fn i => ln_afreq - Math.ln (Real.fromInt i)) dffreq
57366
blanchet
parents: 57365
diff changeset
   336
57359
dd89d0ec8e41 avoid subscripting array with ~1
blanchet
parents: 57358
diff changeset
   337
    fun tfidf feat = Vector.sub (idf, feat)
57102
blanchet
parents: 57101
diff changeset
   338
blanchet
parents: 57101
diff changeset
   339
    fun log_posterior i =
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   340
      let
57374
blanchet
parents: 57373
diff changeset
   341
        val tfreq = Real.fromInt (Vector.sub (tfreq, i))
57097
blanchet
parents: 57096
diff changeset
   342
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   343
        fun add_feat (f, fw0) (res, sfh) =
57102
blanchet
parents: 57101
diff changeset
   344
          (case Inttab.lookup sfh f of
blanchet
parents: 57101
diff changeset
   345
            SOME sf =>
57401
02f56126b4e4 reintroduced 'extra features' but with lower weight than before (to account for tfidf)
blanchet
parents: 57387
diff changeset
   346
            (res + fw0 * tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
57102
blanchet
parents: 57101
diff changeset
   347
             Inttab.delete f sfh)
57409
c9e8cd8ec9e2 correctly take weights into consideration
blanchet
parents: 57407
diff changeset
   348
          | NONE => (res + fw0 * tfidf f * def_val, sfh))
57097
blanchet
parents: 57096
diff changeset
   349
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   350
        val (res, sfh) = fold add_feat goal_feats (init_val * Math.ln tfreq, Vector.sub (sfreq, i))
57097
blanchet
parents: 57096
diff changeset
   351
57409
c9e8cd8ec9e2 correctly take weights into consideration
blanchet
parents: 57407
diff changeset
   352
        fun fold_sfh (f, sf) sow =
c9e8cd8ec9e2 correctly take weights into consideration
blanchet
parents: 57407
diff changeset
   353
          sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
57097
blanchet
parents: 57096
diff changeset
   354
57102
blanchet
parents: 57101
diff changeset
   355
        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
   356
      in
57278
8f7d6f01a775 more MaSh engine variations, for evaluations
blanchet
parents: 57277
diff changeset
   357
        res + tau * sum_of_weights
57097
blanchet
parents: 57096
diff changeset
   358
      end
57029
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   359
57356
9816f692b0ca refactoring
blanchet
parents: 57355
diff changeset
   360
    val posterior = Array.tabulate (num_facts, (fn j => (j, log_posterior j)))
57102
blanchet
parents: 57101
diff changeset
   361
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   362
    fun ret at acc =
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   363
      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
   364
  in
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   365
    select_visible_facts 100000.0 posterior visible_facts;
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   366
    rev_sort_array_prefix (Real.compare o pairself snd) max_suggs posterior;
57364
c1060d10089f honor visible in SML naive Bayes
blanchet
parents: 57363
diff changeset
   367
    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
   368
  end
75cc30d2b83f added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
blanchet
parents: 57028
diff changeset
   369
57546
blanchet
parents: 57545
diff changeset
   370
val initial_number_of_nearest_neighbors = 1
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   371
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   372
fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats =
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   373
  let
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   374
    exception EXIT of unit
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   375
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   376
    val ln_afreq = Math.ln (Real.fromInt num_facts)
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   377
    fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat)))
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   378
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   379
    val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   380
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   381
    val feat_facts = Array.array (num_feats, [])
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   382
    val _ = Vector.foldl (fn (feats, fact) =>
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   383
      (List.app (map_array_at feat_facts (cons fact)) feats; fact + 1)) 0 featss
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   384
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   385
    fun do_feat (s, sw0) =
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   386
      let
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   387
        val sw = sw0 * tfidf s
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   388
        val w6 = Math.pow (sw, 6.0)
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   389
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   390
        fun inc_overlap j =
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   391
          let val (_, ov) = Array.sub (overlaps_sqr, j) in
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   392
            Array.update (overlaps_sqr, j, (j, w6 + ov))
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   393
          end
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   394
      in
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   395
        List.app inc_overlap (Array.sub (feat_facts, s))
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   396
      end
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   397
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   398
    val _ = List.app do_feat goal_feats
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   399
    val _ = rev_sort_array_prefix (Real.compare o pairself snd) num_facts overlaps_sqr
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   400
    val no_recommends = Unsynchronized.ref 0
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   401
    val recommends = Array.tabulate (num_facts, rpair 0.0)
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   402
    val age = Unsynchronized.ref 500000000.0
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   403
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   404
    fun inc_recommend v j =
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   405
      let val (_, ov) = Array.sub (recommends, j) in
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   406
        if ov <= 0.0 then
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   407
          (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   408
        else Array.update (recommends, j, (j, v + ov))
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   409
      end
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   410
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   411
    val k = Unsynchronized.ref 0
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   412
    fun do_k k =
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   413
      if k >= num_facts then
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   414
        raise EXIT ()
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   415
      else
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   416
        let
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   417
          val deps_factor = 2.7 (* FUDGE *)
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   418
          val (j, o2) = Array.sub (overlaps_sqr, num_facts - k - 1)
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   419
          val _ = inc_recommend o2 j
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   420
          val ds = Vector.sub (depss, j)
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   421
          val l = Real.fromInt (length ds)
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   422
        in
57531
4d9895d39b59 improvements to the machine learning algos (due to Cezary K.)
blanchet
parents: 57462
diff changeset
   423
          List.app (inc_recommend (deps_factor * o2 / l)) ds
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   424
        end
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   425
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   426
    fun while1 () =
57546
blanchet
parents: 57545
diff changeset
   427
      if !k = initial_number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   428
      handle EXIT () => ()
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   429
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   430
    fun while2 () =
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   431
      if !no_recommends >= max_suggs then ()
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   432
      else (do_k (!k); k := !k + 1; age := !age - 10000.0; while2 ())
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   433
      handle EXIT () => ()
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   434
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   435
    fun ret acc at =
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   436
      if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   437
  in
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   438
    while1 ();
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   439
    while2 ();
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   440
    select_visible_facts 1000000000.0 recommends visible_facts;
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
   441
    rev_sort_array_prefix (Real.compare o pairself snd) max_suggs recommends;
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   442
    ret [] (Integer.max 0 (num_facts - max_suggs))
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   443
  end
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   444
57125
2f620ef839ee added another way of invoking Python code, for experiments
blanchet
parents: 57124
diff changeset
   445
(* experimental *)
57376
f40ac83d076c refactoring
blanchet
parents: 57375
diff changeset
   446
fun external_tool tool max_suggs learns goal_feats =
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   447
  let
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   448
    val ser = string_of_int (serial ()) (* poor person's attempt at thread-safety *)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   449
    val ocs = TextIO.openOut ("adv_syms" ^ ser)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   450
    val ocd = TextIO.openOut ("adv_deps" ^ ser)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   451
    val ocq = TextIO.openOut ("adv_seq" ^ ser)
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   452
    val occ = TextIO.openOut ("adv_conj" ^ ser)
57296
8a98f08a0523 tweaked experimental setup
blanchet
parents: 57294
diff changeset
   453
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   454
    fun os oc s = TextIO.output (oc, s)
57296
8a98f08a0523 tweaked experimental setup
blanchet
parents: 57294
diff changeset
   455
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   456
    fun ol _ _ _ [] = ()
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   457
      | ol _ f _ [e] = f e
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   458
      | 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
   459
57294
ef9d4e1ceb00 use strings to communicate with external process, to ease debugging
blanchet
parents: 57291
diff changeset
   460
    fun do_learn (name, feats, deps) =
57357
30ee18eb23ac new version of adaptive k-NN with TFIDF
blanchet
parents: 57356
diff changeset
   461
      (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
   462
       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
   463
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   464
    fun forkexec no =
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   465
      let
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   466
        val cmd =
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   467
          "~/misc/" ^ tool ^ " adv_syms" ^ ser ^ " adv_deps" ^ ser ^ " " ^ string_of_int no ^
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   468
          " adv_seq" ^ ser ^ " < adv_conj" ^ ser
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   469
      in
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   470
        fst (Isabelle_System.bash_output cmd)
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   471
        |> space_explode " "
57294
ef9d4e1ceb00 use strings to communicate with external process, to ease debugging
blanchet
parents: 57291
diff changeset
   472
        |> filter_out (curry (op =) "")
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   473
      end
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   474
  in
57401
02f56126b4e4 reintroduced 'extra features' but with lower weight than before (to account for tfidf)
blanchet
parents: 57387
diff changeset
   475
    (List.app do_learn learns; ol occ (os occ o quote) ", " (map fst goal_feats);
57297
3d4647ea3e57 added another experimental engine
blanchet
parents: 57296
diff changeset
   476
     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
   477
     forkexec max_suggs)
57291
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   478
  end
1bac14e0a728 added experimental MaSh engine
blanchet
parents: 57281
diff changeset
   479
57561
8200e1eb367f made SML/NJ happier
blanchet
parents: 57557
diff changeset
   480
fun k_nearest_neighbors_ext max_suggs =
8200e1eb367f made SML/NJ happier
blanchet
parents: 57557
diff changeset
   481
  external_tool ("newknn/knn" ^ " " ^ string_of_int initial_number_of_nearest_neighbors) max_suggs
8200e1eb367f made SML/NJ happier
blanchet
parents: 57557
diff changeset
   482
fun naive_bayes_ext max_suggs = external_tool "predict/nbayes" max_suggs
57374
blanchet
parents: 57373
diff changeset
   483
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   484
fun query_external ctxt algorithm max_suggs learns goal_feats =
57432
blanchet
parents: 57431
diff changeset
   485
  (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   486
   (case algorithm of
57458
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   487
     MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats
419180c354c0 tuned (reordered) code
blanchet
parents: 57432
diff changeset
   488
   | MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats))
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   489
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   490
fun query_internal ctxt algorithm num_facts num_feats (fact_names, featss, depss)
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   491
    (freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   492
  let
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   493
    fun nb () =
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   494
      naive_bayes freqs num_facts max_suggs visible_facts int_goal_feats
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   495
      |> map fst
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   496
    fun knn () =
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   497
      k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   498
        int_goal_feats
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   499
      |> map fst
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   500
  in
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   501
    (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   502
       elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
   503
     (case algorithm of
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   504
       MaSh_NB => nb ()
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   505
     | MaSh_kNN => knn ()
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   506
     | MaSh_NB_kNN =>
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   507
       mesh_facts (op =) max_suggs
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   508
         [(0.5 (* FUDGE *), (weight_facts_steeply (nb ()), [])),
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   509
          (0.5 (* FUDGE *), (weight_facts_steeply (knn ()), []))])
57459
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   510
     |> map (curry Vector.sub fact_names))
22023ab4df3c mix NB and kNN
blanchet
parents: 57458
diff changeset
   511
   end
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   512
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   513
end;
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   514
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
   515
57432
blanchet
parents: 57431
diff changeset
   516
(*** Persistent, stringly-typed state ***)
blanchet
parents: 57431
diff changeset
   517
blanchet
parents: 57431
diff changeset
   518
fun meta_char c =
blanchet
parents: 57431
diff changeset
   519
  if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
blanchet
parents: 57431
diff changeset
   520
     c = #"," then
blanchet
parents: 57431
diff changeset
   521
    String.str c
blanchet
parents: 57431
diff changeset
   522
  else
blanchet
parents: 57431
diff changeset
   523
    (* fixed width, in case more digits follow *)
blanchet
parents: 57431
diff changeset
   524
    "%" ^ stringN_of_int 3 (Char.ord c)
blanchet
parents: 57431
diff changeset
   525
blanchet
parents: 57431
diff changeset
   526
fun unmeta_chars accum [] = String.implode (rev accum)
blanchet
parents: 57431
diff changeset
   527
  | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
blanchet
parents: 57431
diff changeset
   528
    (case Int.fromString (String.implode [d1, d2, d3]) of
blanchet
parents: 57431
diff changeset
   529
      SOME n => unmeta_chars (Char.chr n :: accum) cs
blanchet
parents: 57431
diff changeset
   530
    | NONE => "" (* error *))
blanchet
parents: 57431
diff changeset
   531
  | unmeta_chars _ (#"%" :: _) = "" (* error *)
blanchet
parents: 57431
diff changeset
   532
  | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
blanchet
parents: 57431
diff changeset
   533
blanchet
parents: 57431
diff changeset
   534
val encode_str = String.translate meta_char
blanchet
parents: 57431
diff changeset
   535
val decode_str = String.explode #> unmeta_chars []
blanchet
parents: 57431
diff changeset
   536
blanchet
parents: 57431
diff changeset
   537
val encode_strs = map encode_str #> space_implode " "
57461
29efe682335b removed needless code
blanchet
parents: 57460
diff changeset
   538
val decode_strs = space_explode " " #> map decode_str
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   539
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   540
datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   541
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   542
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
   543
  | 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
   544
  | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x"
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   545
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   546
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
   547
  | 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
   548
  | proof_kind_of_str _ (* "i" *) = Isar_Proof
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   549
57011
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   550
fun add_edge_to name parent =
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   551
  Graph.default_node (parent, (Isar_Proof, [], []))
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   552
  #> Graph.add_edge (parent, name)
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   553
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   554
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
   555
  ((Graph.new_node (name, (kind, feats, deps)) access_G
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   556
    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
   557
   |> fold (add_edge_to name) parents,
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
   558
  (maybe_add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   559
  (name, feats, deps) :: learns)
57011
a4428f517f46 implemented learning of single proofs in SML MaSh
blanchet
parents: 57010
diff changeset
   560
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   561
fun try_graph ctxt when def f =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   562
  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
   563
  handle
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   564
    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
   565
    (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
   566
  | 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
   567
    (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
   568
  | 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
   569
    (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
   570
  | exn =>
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   571
    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
   572
      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
   573
    else
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   574
      (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
   575
       def)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   576
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   577
fun graph_info G =
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   578
  string_of_int (length (Graph.keys G)) ^ " node(s), " ^
57006
blanchet
parents: 57005
diff changeset
   579
  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
   580
  string_of_int (length (Graph.maximals G)) ^ " maximal"
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   581
57545
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   582
type ffds = string vector * int list vector * int list vector
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   583
type freqs = int vector * int Inttab.table vector * int vector
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   584
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   585
type mash_state =
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   586
  {access_G : (proof_kind * string list * string list) Graph.T,
57374
blanchet
parents: 57373
diff changeset
   587
   xtabs : xtab * xtab,
57545
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   588
   ffds : ffds,
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   589
   freqs : freqs,
57365
blanchet
parents: 57364
diff changeset
   590
   dirty_facts : string list option}
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   591
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   592
val empty_xtabs = (empty_xtab, empty_xtab)
57545
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   593
val empty_ffds = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : ffds
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   594
val empty_freqs = (Vector.fromList [], Vector.fromList [], Vector.fromList []) : freqs
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   595
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   596
val empty_state =
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   597
  {access_G = Graph.empty,
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   598
   xtabs = empty_xtabs,
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   599
   ffds = empty_ffds,
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   600
   freqs = empty_freqs,
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   601
   dirty_facts = SOME []} : mash_state
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
   602
57545
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   603
fun recompute_ffds_freqs_from_learns (learns : (string * string list * string list) list)
2126b355f0ca made SML/NJ happier
blanchet
parents: 57532
diff changeset
   604
    ((num_facts, fact_tab), (num_feats, feat_tab)) num_facts0 (fact_names0, featss0, depss0) freqs0 =
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   605
  let
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   606
    val fact_names = Vector.concat [fact_names0, Vector.fromList (map #1 learns)]
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   607
    val featss = Vector.concat [featss0,
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   608
      Vector.fromList (map (map_filter (Symtab.lookup feat_tab) o #2) learns)]
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   609
    val depss = Vector.concat [depss0,
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   610
      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
   611
  in
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   612
    ((fact_names, featss, depss),
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   613
     MaSh.learn_facts freqs0 num_facts0 num_facts num_feats depss featss)
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   614
  end
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   615
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   616
fun reorder_learns (num_facts, fact_tab) learns =
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   617
  let val ary = Array.array (num_facts, ("", [], [])) in
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   618
    List.app (fn learn as (fact, _, _) =>
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   619
        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
   620
      learns;
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   621
    Array.foldr (op ::) [] ary
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   622
  end
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   623
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   624
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
   625
  let
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   626
    val learns =
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   627
      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
   628
      |> reorder_learns fact_xtab
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   629
  in
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   630
    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
   631
  end
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   632
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   633
local
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   634
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   635
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
   636
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   637
exception FILE_VERSION_TOO_NEW of unit
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   638
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   639
fun extract_node line =
55286
blanchet
parents: 55202
diff changeset
   640
  (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
   641
    [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
   642
    (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
   643
      ([kind, name], [parents, feats, deps]) =>
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   644
      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
   645
        decode_strs deps)
55286
blanchet
parents: 55202
diff changeset
   646
    | _ => NONE)
blanchet
parents: 55202
diff changeset
   647
  | _ => NONE)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   648
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   649
fun load_state ctxt (time_state as (memory_time, _)) =
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   650
  let val path = state_file () in
57386
5980ee29dbf6 always expand all paths
blanchet
parents: 57385
diff changeset
   651
    (case try OS.FileSys.modTime (Path.implode path) of
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   652
      NONE => time_state
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   653
    | SOME disk_time =>
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   654
      if Time.>= (memory_time, disk_time) then
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   655
        time_state
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   656
      else
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   657
        (disk_time,
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   658
         (case try File.read_lines path of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   659
           SOME (version' :: node_lines) =>
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   660
           let
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   661
             fun extract_line_and_add_node line =
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   662
               (case extract_node line of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   663
                 NONE => I (* should not happen *)
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   664
               | 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
   665
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   666
             val empty_G_etc = (Graph.empty, empty_xtabs, [])
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   667
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   668
             val (access_G, xtabs, rev_learns) =
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   669
               (case string_ord (version', version) of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   670
                 EQUAL =>
57379
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   671
                 try_graph ctxt "loading state" empty_G_etc
dcaf04545de2 avoid needless (trivial) reordering on load
blanchet
parents: 57378
diff changeset
   672
                   (fn () => fold extract_line_and_add_node node_lines empty_G_etc)
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   673
               | LESS => (remove_state_file (); empty_G_etc) (* cannot parse old file *)
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   674
               | GREATER => raise FILE_VERSION_TOO_NEW ())
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   675
57380
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   676
             val (ffds, freqs) =
a212bee30bba more incremental learning of single fact
blanchet
parents: 57379
diff changeset
   677
               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
   678
           in
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   679
             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
   680
             {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
   681
           end
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   682
         | _ => empty_state)))
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   683
  end
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   684
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
   685
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
   686
  str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
57358
545d02691b32 killed dead data
blanchet
parents: 57357
diff changeset
   687
  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
   688
57365
blanchet
parents: 57364
diff changeset
   689
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
   690
  | save_state ctxt (memory_time, {access_G, xtabs, ffds, freqs, dirty_facts}) =
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   691
    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
   692
      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
   693
        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
   694
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   695
      val path = state_file ()
57365
blanchet
parents: 57364
diff changeset
   696
      val dirty_facts' =
57076
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   697
        (case try OS.FileSys.modTime (Path.implode path) of
3d4b172d2209 automatically reload state file when it changes on disk
blanchet
parents: 57062
diff changeset
   698
          NONE => NONE
57365
blanchet
parents: 57364
diff changeset
   699
        | 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
   700
      val (banner, entries) =
57365
blanchet
parents: 57364
diff changeset
   701
        (case dirty_facts' of
55286
blanchet
parents: 55202
diff changeset
   702
          SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])
blanchet
parents: 55202
diff changeset
   703
        | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   704
    in
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   705
      (case banner of SOME s => File.write path s | NONE => ();
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   706
       entries |> chunk_list 500 |> List.app (File.append path o implode o map str_of_entry))
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   707
      handle IO.Io _ => ();
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   708
      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
   709
        "Saved fact graph (" ^ graph_info access_G ^
57365
blanchet
parents: 57364
diff changeset
   710
        (case dirty_facts of
blanchet
parents: 57364
diff changeset
   711
          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
   712
        | _ => "") ^  ")");
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   713
      (Time.now (),
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
   714
       {access_G = access_G, xtabs = xtabs, ffds = ffds, freqs = freqs, dirty_facts = SOME []})
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   715
    end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   716
57365
blanchet
parents: 57364
diff changeset
   717
val global_state = Synchronized.var "Sledgehammer_MaSh.global_state" (Time.zeroTime, empty_state)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   718
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   719
in
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   720
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   721
fun map_state ctxt f =
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   722
  Synchronized.change global_state (load_state ctxt ##> f #> save_state ctxt)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
   723
  handle FILE_VERSION_TOO_NEW () => ()
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   724
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   725
fun peek_state ctxt =
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   726
  Synchronized.change_result global_state (perhaps (try (load_state ctxt)) #> `snd)
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   727
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
   728
fun clear_state () =
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   729
  Synchronized.change global_state (fn _ => (remove_state_file (); (Time.zeroTime, empty_state)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   730
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   731
end
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   732
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   733
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   734
(*** Isabelle helpers ***)
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
   735
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   736
val local_prefix = "local" ^ Long_Name.separator
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   737
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   738
fun elided_backquote_thm threshold th =
57006
blanchet
parents: 57005
diff changeset
   739
  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
   740
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
   741
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
   742
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   743
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
   744
  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
   745
    let val hint = Thm.get_name_hint th in
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   746
      (* There must be a better way to detect local facts. *)
55286
blanchet
parents: 55202
diff changeset
   747
      (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
   748
        SOME suf =>
55286
blanchet
parents: 55202
diff changeset
   749
        thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
blanchet
parents: 55202
diff changeset
   750
        elided_backquote_thm 50 th
blanchet
parents: 55202
diff changeset
   751
      | 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
   752
    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
   753
  else
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   754
    elided_backquote_thm 200 th
48378
9e96486d53ad handle local facts smoothly in MaSh
blanchet
parents: 48377
diff changeset
   755
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   756
fun find_suggested_facts ctxt facts =
48330
192444b53e86 speed up MaSh queries
blanchet
parents: 48329
diff changeset
   757
  let
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   758
    fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   759
    val tab = fold add facts Symtab.empty
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   760
    fun lookup nick =
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   761
      Symtab.lookup tab nick
57006
blanchet
parents: 57005
diff changeset
   762
      |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick) | _ => ())
51134
d03ded5dcf65 more MaSh tracing
blanchet
parents: 51133
diff changeset
   763
  in map_filter lookup end
48311
3c4e10606567 implemented MaSh QUERY operation
blanchet
parents: 48309
diff changeset
   764
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   765
fun free_feature_of s = "f" ^ s
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   766
fun thy_feature_of s = "y" ^ s
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   767
fun type_feature_of s = "t" ^ s
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   768
fun class_feature_of s = "s" ^ s
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   769
val local_feature = "local"
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   770
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   771
fun crude_theory_ord p =
50722
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   772
  if Theory.subthy p then
b422a48adc2d speed up generation of local theorem nicknames
blanchet
parents: 50718
diff changeset
   773
    if Theory.eq_thy p then EQUAL else LESS
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   774
  else if Theory.subthy (swap p) then
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   775
    GREATER
55286
blanchet
parents: 55202
diff changeset
   776
  else
blanchet
parents: 55202
diff changeset
   777
    (case int_ord (pairself (length o Theory.ancestors_of) p) of
blanchet
parents: 55202
diff changeset
   778
      EQUAL => string_ord (pairself Context.theory_name p)
blanchet
parents: 55202
diff changeset
   779
    | order => order)
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   780
51135
e32114b25551 tuned code
blanchet
parents: 51134
diff changeset
   781
fun crude_thm_ord p =
55286
blanchet
parents: 55202
diff changeset
   782
  (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
   783
    EQUAL =>
57039
1ddd1f75fb40 added comment
blanchet
parents: 57029
diff changeset
   784
    (* The hack below is necessary because of odd dependencies that are not reflected in the theory
1ddd1f75fb40 added comment
blanchet
parents: 57029
diff changeset
   785
       comparison. *)
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   786
    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
   787
      (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
55286
blanchet
parents: 55202
diff changeset
   788
      (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
   789
        EQUAL => string_ord q
55286
blanchet
parents: 55202
diff changeset
   790
      | ord => ord)
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   791
    end
55286
blanchet
parents: 55202
diff changeset
   792
  | ord => ord)
48324
3ee5b5589402 speed up tautology/metaness check
blanchet
parents: 48323
diff changeset
   793
51136
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   794
val thm_less_eq = Theory.subthy o pairself theory_of_thm
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   795
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
   796
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   797
val freezeT = Type.legacy_freeze_type
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   798
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   799
fun freeze (t $ u) = freeze t $ freeze u
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   800
  | 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
   801
  | freeze (Var ((s, _), T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   802
  | freeze (Const (s, T)) = Const (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   803
  | freeze (Free (s, T)) = Free (s, freezeT T)
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   804
  | freeze t = t
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   805
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   806
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
   807
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
   808
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
   809
  let
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   810
    val problem =
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
   811
      {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
   812
       subgoal_count = 1, factss = [("", facts)]}
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   813
  in
54503
blanchet
parents: 54432
diff changeset
   814
    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
   815
  end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   816
48326
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   817
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
ef800e91d072 removed debugging output
blanchet
parents: 48325
diff changeset
   818
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   819
val pat_tvar_prefix = "_"
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   820
val pat_var_prefix = "_"
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   821
53089
a58b3b8631c6 keep long names to stay on the safe side
blanchet
parents: 53086
diff changeset
   822
(* 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
   823
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
   824
57006
blanchet
parents: 57005
diff changeset
   825
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
   826
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   827
fun crude_str_of_typ (Type (s, [])) = massage_long_name s
57006
blanchet
parents: 57005
diff changeset
   828
  | 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
   829
  | 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
   830
  | 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
   831
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   832
fun maybe_singleton_str _ "" = []
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   833
  | maybe_singleton_str pref s = [pref ^ s]
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   834
53148
c898409d8630 fixed subtle bug with "take" + thread overlord through
blanchet
parents: 53142
diff changeset
   835
val max_pat_breadth = 10 (* FUDGE *)
50585
306c7b807e13 contain exponential explosion of term patterns
blanchet
parents: 50584
diff changeset
   836
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
   837
fun term_features_of ctxt thy_name term_max_depth type_max_depth ts =
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   838
  let
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   839
    val thy = Proof_Context.theory_of ctxt
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   840
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   841
    val fixes = map snd (Variable.dest_fixes ctxt)
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   842
    val classes = Sign.classes_of thy
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   843
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
   844
    fun add_classes @{sort type} = I
50392
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   845
      | add_classes S =
190053ee24ed expand type classes into their ancestors for MaSh
blanchet
parents: 50391
diff changeset
   846
        fold (`(Sorts.super_classes classes)
57006
blanchet
parents: 57005
diff changeset
   847
          #> swap #> op ::
blanchet
parents: 57005
diff changeset
   848
          #> subtract (op =) @{sort type} #> map massage_long_name
blanchet
parents: 57005
diff changeset
   849
          #> map class_feature_of
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   850
          #> union (op =)) S
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   851
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   852
    fun pattify_type 0 _ = []
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   853
      | pattify_type _ (Type (s, [])) =
53086
15fe0ca088b3 MaSh tweaking: shorter names + killed (broken) SNoW
blanchet
parents: 53085
diff changeset
   854
        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
   855
      | pattify_type depth (Type (s, U :: Ts)) =
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   856
        let
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   857
          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
   858
          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
   859
          val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U)
57006
blanchet
parents: 57005
diff changeset
   860
        in
blanchet
parents: 57005
diff changeset
   861
          map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
blanchet
parents: 57005
diff changeset
   862
        end
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   863
      | pattify_type _ (TFree (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
   864
      | pattify_type _ (TVar (_, S)) = maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S)
57006
blanchet
parents: 57005
diff changeset
   865
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   866
    fun add_type_pat depth T =
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   867
      union (op =) (map type_feature_of (pattify_type depth T))
57006
blanchet
parents: 57005
diff changeset
   868
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   869
    fun add_type_pats 0 _ = I
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   870
      | add_type_pats depth t = add_type_pat depth t #> add_type_pats (depth - 1) t
57006
blanchet
parents: 57005
diff changeset
   871
53083
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   872
    fun add_type T =
019ecbb18e3f generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
blanchet
parents: 53082
diff changeset
   873
      add_type_pats type_max_depth T
53156
f79f4693868b minor MaSh fix
blanchet
parents: 53155
diff changeset
   874
      #> fold_atyps_sorts (add_classes o snd) T
57006
blanchet
parents: 57005
diff changeset
   875
53084
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
   876
    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
   877
      | add_subtypes T = add_type T
53082
369e39511555 generate deep type patterns in MaSh
blanchet
parents: 52697
diff changeset
   878
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   879
    fun pattify_term _ 0 _ = []
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   880
      | pattify_term _ _ (Const (s, _)) =
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   881
        if is_widely_irrelevant_const s then [] else [massage_long_name 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
   882
      | pattify_term _ _ (Free (s, T)) =
53128
ea1b62ed5a54 get rid of some silly MaSh features
blanchet
parents: 53127
diff changeset
   883
        maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
53090
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
   884
        |> (if member (op =) fixes s then
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   885
              cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
53090
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
   886
            else
1426c97311f2 treat frees as both consts and vars, for more hits
blanchet
parents: 53089
diff changeset
   887
              I)
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   888
      | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
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
   889
      | pattify_term Ts _ (Bound j) =
54695
a9efdf970720 generate problems with type classes
blanchet
parents: 54693
diff changeset
   890
        maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j))
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
   891
      | pattify_term Ts depth (t $ u) =
50339
d8dae91f3107 MaSh improvements: deeper patterns + more respect for chained facts
blanchet
parents: 50338
diff changeset
   892
        let
57055
df3a26987a8d reverted '|' features in MaSh -- these sounded like a good idea but never really worked
blanchet
parents: 57052
diff changeset
   893
          val ps = take max_pat_breadth (pattify_term Ts depth t)
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   894
          val qs = take max_pat_breadth ("" :: pattify_term Ts (depth - 1) u)
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   895
        in
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   896
          map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   897
        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
   898
      | pattify_term _ _ _ = []
57006
blanchet
parents: 57005
diff changeset
   899
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   900
    fun add_term_pat Ts = union (op =) oo pattify_term Ts
57006
blanchet
parents: 57005
diff changeset
   901
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   902
    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
   903
      | 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
   904
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   905
    fun add_term Ts = add_term_pats Ts term_max_depth
57006
blanchet
parents: 57005
diff changeset
   906
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   907
    fun add_subterms Ts t =
55286
blanchet
parents: 55202
diff changeset
   908
      (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
   909
        (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
   910
        (not (is_widely_irrelevant_const s) ? add_term Ts t)
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
   911
        #> add_subtypes T #> fold (add_subterms Ts) args
50857
80768e28c9ee better handlig of built-ins -- at the top-level, not in subterms
blanchet
parents: 50841
diff changeset
   912
      | (head, args) =>
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   913
        (case head of
53130
6741ba8d5c6d improve weight computation for complex terms
blanchet
parents: 53129
diff changeset
   914
           Free (_, T) => add_term Ts t #> add_subtypes T
53084
877f5c28016f add subtypes as well as features in MaSh
blanchet
parents: 53083
diff changeset
   915
         | Var (_, T) => add_subtypes T
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   916
         | 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
   917
         | _ => I)
55286
blanchet
parents: 55202
diff changeset
   918
        #> fold (add_subterms Ts) args)
57006
blanchet
parents: 57005
diff changeset
   919
  in
blanchet
parents: 57005
diff changeset
   920
    fold (add_subterms []) ts []
blanchet
parents: 57005
diff changeset
   921
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   922
53085
15483854c83e handle Bounds as well in MaSh features
blanchet
parents: 53084
diff changeset
   923
val term_max_depth = 2
53155
2c585fdbe197 eliminated some needless MaSh features
blanchet
parents: 53154
diff changeset
   924
val type_max_depth = 1
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   925
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   926
(* TODO: Generate type classes for types? *)
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
   927
fun features_of ctxt thy (scope, _) ts =
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   928
  let val thy_name = Context.theory_name thy in
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   929
    thy_feature_of thy_name ::
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
   930
    term_features_of ctxt thy_name term_max_depth type_max_depth ts
50393
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   931
    |> scope <> Global ? cons local_feature
d8aa26c78327 record free variables as a MaSh feature
blanchet
parents: 50392
diff changeset
   932
  end
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   933
57006
blanchet
parents: 57005
diff changeset
   934
(* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn
blanchet
parents: 57005
diff changeset
   935
   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
   936
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
   937
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
   938
val prover_default_max_facts = 25
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
   939
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   940
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   941
val typedef_dep = nickname_of_thm @{thm CollectI}
57006
blanchet
parents: 57005
diff changeset
   942
(* Mysterious parts of the class machinery create lots of proofs that refer exclusively to
blanchet
parents: 57005
diff changeset
   943
   "someI_ex" (and to some internal constructions). *)
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   944
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
   945
50828
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   946
val fundef_ths =
57006
blanchet
parents: 57005
diff changeset
   947
  @{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
   948
  |> map nickname_of_thm
91e6836bb68b don't learn from the proof of "psimps" etc.
blanchet
parents: 50827
diff changeset
   949
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   950
(* "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
   951
val typedef_ths =
57006
blanchet
parents: 57005
diff changeset
   952
  @{thms type_definition.Abs_inverse type_definition.Rep_inverse type_definition.Rep
blanchet
parents: 57005
diff changeset
   953
      type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases
blanchet
parents: 57005
diff changeset
   954
      type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct
blanchet
parents: 57005
diff changeset
   955
      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
   956
  |> map nickname_of_thm
48438
3e45c98fe127 distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
blanchet
parents: 48436
diff changeset
   957
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   958
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
   959
    (case first_field ".rec" dep of
57006
blanchet
parents: 57005
diff changeset
   960
      SOME (pref, _) =>
blanchet
parents: 57005
diff changeset
   961
      (case first_field ".size" (nickname_of_thm th) of
blanchet
parents: 57005
diff changeset
   962
        SOME (pref', _) => pref = pref'
blanchet
parents: 57005
diff changeset
   963
      | NONE => false)
blanchet
parents: 57005
diff changeset
   964
    | NONE => false)
48441
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   965
  | is_size_def _ _ = false
2d2f009ca8eb remove MaSh junk associated with size functions
blanchet
parents: 48440
diff changeset
   966
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
   967
fun trim_dependencies deps =
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   968
  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
   969
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   970
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
   971
  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
   972
  |> Option.map (fn deps =>
57006
blanchet
parents: 57005
diff changeset
   973
    if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
blanchet
parents: 57005
diff changeset
   974
       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
   975
       is_size_def deps th then
50755
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   976
      []
4c781d65c0d6 get rid of spurious "Isar" proofs
blanchet
parents: 50754
diff changeset
   977
    else
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
   978
      deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
   979
57006
blanchet
parents: 57005
diff changeset
   980
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
blanchet
parents: 57005
diff changeset
   981
    name_tabs th =
55286
blanchet
parents: 55202
diff changeset
   982
  (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
   983
    SOME [] => (false, [])
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
   984
  | isar_deps0 =>
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   985
    let
57306
ff10067b2248 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
blanchet
parents: 57305
diff changeset
   986
      val isar_deps = these isar_deps0
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   987
      val thy = Proof_Context.theory_of ctxt
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   988
      val goal = goal_of_thm thy th
54141
f57f8e7a879f generate a comment storing the goal nickname in "learn_prover"
blanchet
parents: 54140
diff changeset
   989
      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
   990
      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
51136
fdcc06013f2d avoid crude/wrong theorem comparision
blanchet
parents: 51135
diff changeset
   991
      val facts = facts |> filter (fn (_, th') => thm_less (th', th))
57006
blanchet
parents: 57005
diff changeset
   992
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
   993
      fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
57006
blanchet
parents: 57005
diff changeset
   994
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
   995
      fun is_dep dep (_, th) = nickname_of_thm th = dep
57006
blanchet
parents: 57005
diff changeset
   996
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   997
      fun add_isar_dep facts dep accum =
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   998
        if exists (is_dep dep) accum then
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
   999
          accum
55286
blanchet
parents: 55202
diff changeset
  1000
        else
blanchet
parents: 55202
diff changeset
  1001
          (case find_first (is_dep dep) facts of
blanchet
parents: 55202
diff changeset
  1002
            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
  1003
          | NONE => accum (* should not happen *))
57006
blanchet
parents: 57005
diff changeset
  1004
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
  1005
      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
  1006
        facts
54095
d80743f28fec simplify fudge factor code
blanchet
parents: 54091
diff changeset
  1007
        |> mepo_suggested_facts ctxt params (max_facts |> the_default prover_default_max_facts) NONE
d80743f28fec simplify fudge factor code
blanchet
parents: 54091
diff changeset
  1008
             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
  1009
      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
  1010
        mepo_facts
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
  1011
        |> 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
  1012
        |> 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
  1013
      val num_isar_deps = length isar_deps
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1014
    in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1015
      if verbose andalso auto_level = 0 then
57017
blanchet
parents: 57014
diff changeset
  1016
        Output.urgent_message ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^
blanchet
parents: 57014
diff changeset
  1017
          string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^
blanchet
parents: 57014
diff changeset
  1018
          " facts.")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1019
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1020
        ();
55286
blanchet
parents: 55202
diff changeset
  1021
      (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
  1022
        {outcome = NONE, used_facts, ...} =>
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1023
        (if verbose andalso auto_level = 0 then
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1024
           let val num_facts = length used_facts in
57017
blanchet
parents: 57014
diff changeset
  1025
             Output.urgent_message ("Found proof with " ^ string_of_int num_facts ^ " fact" ^
blanchet
parents: 57014
diff changeset
  1026
               plural_s num_facts ^ ".")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1027
           end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1028
         else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1029
           ();
50754
74a6adcb96ac also generate queries for goals with too many Isar dependencies
blanchet
parents: 50751
diff changeset
  1030
         (true, map fst used_facts))
55286
blanchet
parents: 55202
diff changeset
  1031
      | _ => (false, isar_deps))
blanchet
parents: 55202
diff changeset
  1032
    end)
48251
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1033
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1034
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1035
(*** High-level communication with MaSh ***)
6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer
blanchet
parents: 48249
diff changeset
  1036
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1037
(* 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
  1038
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1039
fun chunks_and_parents_for chunks th =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1040
  let
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1041
    fun insert_parent new parents =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1042
      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
  1043
        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
  1044
      end
57006
blanchet
parents: 57005
diff changeset
  1045
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1046
    fun rechunk seen (rest as th' :: ths) =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1047
      if thm_less_eq (th', th) then (rev seen, rest)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1048
      else rechunk (th' :: seen) ths
57006
blanchet
parents: 57005
diff changeset
  1049
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1050
    fun do_chunk [] accum = accum
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1051
      | do_chunk (chunk as hd_chunk :: _) (chunks, parents) =
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1052
        if thm_less_eq (hd_chunk, th) then
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1053
          (chunk :: chunks, insert_parent hd_chunk parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1054
        else if thm_less_eq (List.last chunk, th) then
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1055
          let val (front, back as hd_back :: _) = rechunk [] chunk in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1056
            (front :: back :: chunks, insert_parent hd_back parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1057
          end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1058
        else
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1059
          (chunk :: chunks, parents)
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1060
  in
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1061
    fold_rev do_chunk chunks ([], [])
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1062
    |>> cons []
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1063
    ||> map nickname_of_thm
51181
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1064
  end
d0fa18638478 implement (more) accurate computation of parents
blanchet
parents: 51180
diff changeset
  1065
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1066
fun attach_parents_to_facts _ [] = []
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1067
  | 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
  1068
    let
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1069
      fun do_facts _ [] = []
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1070
        | do_facts (_, parents) [fact] = [(parents, fact)]
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1071
        | do_facts (chunks, parents)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1072
                   ((fact as (_, th)) :: (facts as (_, th') :: _)) =
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1073
          let
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1074
            val chunks = app_hd (cons th) chunks
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1075
            val chunks_and_parents' =
57370
9d420da6c7e2 disable 'extra' feature tainting for now
blanchet
parents: 57369
diff changeset
  1076
              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
  1077
                (chunks, [nickname_of_thm th])
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1078
              else
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1079
                chunks_and_parents_for chunks th'
57006
blanchet
parents: 57005
diff changeset
  1080
          in
blanchet
parents: 57005
diff changeset
  1081
            (parents, fact) :: do_facts chunks_and_parents' facts
blanchet
parents: 57005
diff changeset
  1082
          end
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1083
    in
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1084
      old_facts @ facts
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1085
      |> do_facts (chunks_and_parents_for [[]] th)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1086
      |> drop (length old_facts)
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1087
    end
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1088
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1089
fun maximal_wrt_graph G keys =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1090
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1091
    val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) keys
57006
blanchet
parents: 57005
diff changeset
  1092
57012
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1093
    fun insert_new seen name = not (Symtab.defined seen name) ? insert (op =) name
57006
blanchet
parents: 57005
diff changeset
  1094
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1095
    fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0
57006
blanchet
parents: 57005
diff changeset
  1096
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1097
    fun find_maxes _ (maxs, []) = map snd maxs
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1098
      | find_maxes seen (maxs, new :: news) =
57012
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1099
        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
  1100
          (if Symtab.defined tab new then
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1101
             let
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1102
               val newp = Graph.all_preds G [new]
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1103
               fun is_ancestor x yp = member (op =) yp x
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1104
               val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp))
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1105
             in
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1106
               if exists (is_ancestor new o fst) maxs then (maxs, news)
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1107
               else ((newp, new) :: filter_out (fn (_, max) => is_ancestor max newp) maxs, news)
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1108
             end
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1109
           else
43fd82a537a3 cleaner handling of learned proofs
blanchet
parents: 57011
diff changeset
  1110
             (maxs, Graph.Keys.fold (insert_new seen) (Graph.imm_preds G new) news))
57006
blanchet
parents: 57005
diff changeset
  1111
  in
blanchet
parents: 57005
diff changeset
  1112
    find_maxes Symtab.empty ([], Graph.maximals G)
blanchet
parents: 57005
diff changeset
  1113
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1114
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1115
fun maximal_wrt_access_graph _ [] = []
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1116
  | maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) =
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1117
    let val thy = theory_of_thm th in
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1118
      fact :: filter_out (fn (_, th') => Theory.subthy (theory_of_thm th', thy)) facts
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1119
      |> map (nickname_of_thm o snd)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1120
      |> maximal_wrt_graph access_G
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1121
    end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1122
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1123
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
  1124
53197
6c5e7143e1f6 tuned fudge factor in light of evaluation
blanchet
parents: 53159
diff changeset
  1125
val chained_feature_factor = 0.5 (* FUDGE *)
57405
1f49da059947 reintroduced 'extra features' + only print message in verbose mode
blanchet
parents: 57404
diff changeset
  1126
val extra_feature_factor = 0.1 (* FUDGE *)
1f49da059947 reintroduced 'extra features' + only print message in verbose mode
blanchet
parents: 57404
diff changeset
  1127
val num_extra_feature_facts = 10 (* FUDGE *)
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1128
57386
5980ee29dbf6 always expand all paths
blanchet
parents: 57385
diff changeset
  1129
val max_proximity_facts = 100
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1130
54060
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1131
fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1132
  let
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1133
    val inter_fact = inter (eq_snd Thm.eq_thm_prop)
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1134
    val raw_mash = find_suggested_facts ctxt facts suggs
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1135
    val proximate = take max_proximity_facts facts
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1136
    val unknown_chained = inter_fact raw_unknown chained
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1137
    val unknown_proximate = inter_fact raw_unknown proximate
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1138
    val mess =
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1139
      [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1140
       (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
5f96d29fb7c2 removed pointless special case
blanchet
parents: 54012
diff changeset
  1141
       (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
57007
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
  1142
    val unknown = raw_unknown
d3eed0518882 started work on MaSh/SML
blanchet
parents: 57006
diff changeset
  1143
      |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate]
57006
blanchet
parents: 57005
diff changeset
  1144
  in
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1145
    (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
57006
blanchet
parents: 57005
diff changeset
  1146
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1147
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1148
fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1149
  let
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
  1150
    val thy_name = Context.theory_name thy
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
  1151
    val algorithm = the_mash_algorithm ()
57052
ea5912e3b008 until naive Bayes supports weights, don't incorporate 'extra' low-weight features
blanchet
parents: 57039
diff changeset
  1152
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1153
    val facts = facts
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1154
      |> rev_sort_list_prefix (crude_thm_ord o pairself snd)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1155
        (Int.max (num_extra_feature_facts, max_proximity_facts))
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1156
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1157
    val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
54085
b6b41e1d5689 optimized built-in const check
blanchet
parents: 54064
diff changeset
  1158
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
  1159
    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
  1160
      thy_name = Context.theory_name (theory_of_thm th)
56995
61855ade6c7e hide more consts to beautify documentation
blanchet
parents: 56303
diff changeset
  1161
53141
d27e99a6a679 take chained and proximate facts into consideration when computing MaSh features
blanchet
parents: 53140
diff changeset
  1162
    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
  1163
      [prop_of th]
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
  1164
      |> features_of ctxt (theory_of_thm th) stature
57404
a68ae60c1504 got rid of hard-coded weights, now that we have TFIDF
blanchet
parents: 57403
diff changeset
  1165
      |> map (rpair (weight * factor))
54085
b6b41e1d5689 optimized built-in const check
blanchet
parents: 54064
diff changeset
  1166
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1167
    val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} =
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1168
      peek_state ctxt
57017
blanchet
parents: 57014
diff changeset
  1169
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1170
    val goal_feats0 = features_of ctxt thy (Local, General) (concl_t :: hyp_ts)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1171
    val chained_feats = chained
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1172
      |> map (rpair 1.0)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1173
      |> map (chained_or_extra_features_of chained_feature_factor)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1174
      |> rpair [] |-> fold (union (eq_fst (op =)))
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1175
    val extra_feats = facts
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1176
      |> take (Int.max (0, num_extra_feature_facts - length chained))
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1177
      |> filter fact_has_right_theory
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1178
      |> weight_facts_steeply
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1179
      |> map (chained_or_extra_features_of extra_feature_factor)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1180
      |> rpair [] |-> fold (union (eq_fst (op =)))
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1181
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1182
    val goal_feats =
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1183
      fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1184
      |> debug ? sort (Real.compare o swap o pairself snd)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1185
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1186
    val parents = maximal_wrt_access_graph access_G facts
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1187
    val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1188
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1189
    val suggs =
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
  1190
      if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1191
        let
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1192
          val learns =
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1193
            Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1194
        in
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
  1195
          MaSh.query_external ctxt algorithm max_suggs learns goal_feats
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1196
        end
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1197
      else
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1198
        let
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1199
          val int_goal_feats =
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1200
            map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1201
        in
57532
c7dc1f0a2b8a tuned terminology
blanchet
parents: 57531
diff changeset
  1202
          MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1203
            goal_feats int_goal_feats
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1204
        end
57017
blanchet
parents: 57014
diff changeset
  1205
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1206
    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
  1207
  in
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1208
    find_mash_suggestions ctxt max_suggs suggs facts chained unknown
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1209
    |> pairself (map fact_of_raw_fact)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1210
  end
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1211
57552
1072599c43f6 no need for 'mash' subdirectory after removal of Python program
blanchet
parents: 57546
diff changeset
  1212
fun mash_unlearn () = (clear_state (); Output.urgent_message "Reset MaSh.")
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1213
57381
blanchet
parents: 57380
diff changeset
  1214
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
  1215
  let
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1216
    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
  1217
      try_graph ctxt "updating graph" accum (fn () =>
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1218
        (from :: parents, Graph.add_edge_acyclic (from, name) access_G))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1219
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1220
    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
  1221
    val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1222
    val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1223
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1224
    val fact_xtab = maybe_add_to_xtab name fact_xtab
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1225
    val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
57006
blanchet
parents: 57005
diff changeset
  1226
  in
57381
blanchet
parents: 57380
diff changeset
  1227
    ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
57006
blanchet
parents: 57005
diff changeset
  1228
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1229
57381
blanchet
parents: 57380
diff changeset
  1230
fun relearn_wrt_access_graph ctxt (name, deps) access_G =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1231
  let
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1232
    fun maybe_relearn_from from (accum as (parents, access_G)) =
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1233
      try_graph ctxt "updating graph" accum (fn () =>
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1234
        (from :: parents, Graph.add_edge_acyclic (from, name) access_G))
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1235
    val access_G =
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1236
      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
  1237
    val (deps, _) = ([], access_G) |> fold maybe_relearn_from deps
57006
blanchet
parents: 57005
diff changeset
  1238
  in
57381
blanchet
parents: 57380
diff changeset
  1239
    ((name, deps), access_G)
57006
blanchet
parents: 57005
diff changeset
  1240
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1241
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1242
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
  1243
  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
  1244
57273
01b68f625550 automatically learn MaSh facts also in 'blocking' mode
blanchet
parents: 57150
diff changeset
  1245
val learn_timeout_slack = 20.0
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1246
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1247
fun launch_thread timeout task =
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1248
  let
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1249
    val hard_timeout = time_mult learn_timeout_slack timeout
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1250
    val birth_time = Time.now ()
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1251
    val death_time = Time.+ (birth_time, hard_timeout)
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1252
    val desc = ("Machine learner for Sledgehammer", "")
57006
blanchet
parents: 57005
diff changeset
  1253
  in
blanchet
parents: 57005
diff changeset
  1254
    Async_Manager.thread MaShN birth_time death_time desc task
blanchet
parents: 57005
diff changeset
  1255
  end
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1256
57013
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1257
fun learned_proof_name () =
ed95456499e6 better way to take invisible facts into account than 'island' business
blanchet
parents: 57012
diff changeset
  1258
  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
  1259
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1260
fun mash_learn_proof ctxt ({timeout, ...} : params) t facts used_ths =
57387
2b6fe2a48352 reintroduced MaSh hints, this time as persistent creatures
blanchet
parents: 57386
diff changeset
  1261
  if not (null used_ths) andalso is_mash_enabled () then
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1262
    launch_thread timeout (fn () =>
57006
blanchet
parents: 57005
diff changeset
  1263
      let
blanchet
parents: 57005
diff changeset
  1264
        val thy = Proof_Context.theory_of ctxt
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
  1265
        val feats = features_of ctxt thy (Local, General) [t]
57460
9cc802a8ab06 speed up MaSh a bit
blanchet
parents: 57459
diff changeset
  1266
        val facts = rev_sort_list_prefix (crude_thm_ord o pairself snd) 1 facts
57006
blanchet
parents: 57005
diff changeset
  1267
      in
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1268
        map_state ctxt
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1269
          (fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1270
             let
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1271
               val parents = maximal_wrt_access_graph access_G facts
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1272
               val deps = used_ths
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1273
                 |> filter (is_fact_in_graph access_G)
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1274
                 |> map nickname_of_thm
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1275
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1276
               val name = learned_proof_name ()
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1277
               val (access_G', xtabs', rev_learns) =
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1278
                 add_node Automatic_Proof name parents feats deps (access_G, xtabs, [])
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1279
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1280
               val (ffds', freqs') =
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1281
                 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
  1282
             in
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1283
               {access_G = access_G', xtabs = xtabs', ffds = ffds', freqs = freqs',
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1284
                dirty_facts = Option.map (cons name) dirty_facts}
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1285
             end);
57006
blanchet
parents: 57005
diff changeset
  1286
        (true, "")
blanchet
parents: 57005
diff changeset
  1287
      end)
53819
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1288
  else
e55d641d0a70 honor MaSh's zero-overhead policy -- no learning if the tool is disabled
blanchet
parents: 53790
diff changeset
  1289
    ()
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1290
57353
ee493eb30c7b adaptive k-NN
blanchet
parents: 57306
diff changeset
  1291
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
  1292
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1293
val commit_timeout = seconds 30.0
48332
271a4a6af734 optimize parent computation in MaSh + remove temporary files
blanchet
parents: 48330
diff changeset
  1294
50485
3c6ac2da2f45 merge aliased theorems in MaSh dependencies, modulo symmetry of equality
blanchet
parents: 50484
diff changeset
  1295
(* The timeout is understood in a very relaxed fashion. *)
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1296
fun mash_learn_facts ctxt (params as {debug, verbose, ...}) prover auto_level run_prover
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1297
    learn_timeout facts =
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1298
  let
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1299
    val timer = Timer.startRealTimer ()
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1300
    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
  1301
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1302
    val {access_G, ...} = peek_state ctxt
53095
667717a5ad80 learn MaSh facts on the fly
blanchet
parents: 53094
diff changeset
  1303
    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
  1304
    val no_new_facts = forall is_in_access_G facts
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1305
  in
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1306
    if no_new_facts andalso not run_prover then
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1307
      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
  1308
        "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
  1309
        (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
  1310
           "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover."
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1311
         else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1312
           "")
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1313
      else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1314
        ""
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1315
    else
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1316
      let
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1317
        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
  1318
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1319
        fun deps_of status th =
57017
blanchet
parents: 57014
diff changeset
  1320
          if status = Non_Rec_Def orelse status = Rec_Def then
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1321
            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
  1322
          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
  1323
            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
  1324
            |> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1325
          else
50735
6b232d76cbc9 refined class handling, to prevent cycles in fact graph
blanchet
parents: 50732
diff changeset
  1326
            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
  1327
48669
cdcdb0547f29 remember ATP flops to avoid repeating them too quickly
blanchet
parents: 48668
diff changeset
  1328
        fun do_commit [] [] [] state = state
57382
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1329
          | do_commit learns relearns flops
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1330
              {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
  1331
            let
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1332
              val was_empty = Graph.is_empty access_G
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1333
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1334
              val (learns, (access_G', xtabs')) =
57381
blanchet
parents: 57380
diff changeset
  1335
                fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1336
              val (relearns, access_G'') =
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1337
                fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
57371
0b2bce982afd store string-to-index tables in memory
blanchet
parents: 57370
diff changeset
  1338
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1339
              val access_G''' = access_G'' |> fold flop_wrt_access_graph flops
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1340
              val dirty_facts' =
57365
blanchet
parents: 57364
diff changeset
  1341
                (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
  1342
                  (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
55286
blanchet
parents: 55202
diff changeset
  1343
                | _ => NONE)
57378
fe96689f393b recompute learning data at learning time, not query time
blanchet
parents: 57377
diff changeset
  1344
57382
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1345
              val (ffds', freqs') =
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1346
                if null relearns then
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1347
                  recompute_ffds_freqs_from_learns
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1348
                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0
57382
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1349
                    ffds freqs
6c6a0ac70eac incremental learning when learing several facts
blanchet
parents: 57381
diff changeset
  1350
                else
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1351
                  recompute_ffds_freqs_from_access_G access_G''' xtabs'
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1352
            in
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1353
              {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1354
               dirty_facts = dirty_facts'}
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1355
            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
  1356
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1357
        fun commit last learns relearns flops =
57017
blanchet
parents: 57014
diff changeset
  1358
          (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1359
           map_state ctxt (do_commit (rev learns) relearns flops);
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1360
           if not last andalso auto_level = 0 then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1361
             let val num_proofs = length learns + length relearns in
57017
blanchet
parents: 57014
diff changeset
  1362
               Output.urgent_message ("Learned " ^ string_of_int num_proofs ^ " " ^
blanchet
parents: 57014
diff changeset
  1363
                 (if run_prover then "automatic" else "Isar") ^ " proof" ^
blanchet
parents: 57014
diff changeset
  1364
                 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
  1365
             end
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1366
           else
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1367
             ())
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1368
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1369
        fun learn_new_fact _ (accum as (_, (_, _, true))) = accum
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1370
          | learn_new_fact (parents, ((_, stature as (_, status)), th))
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1371
              (learns, (num_nontrivial, next_commit, _)) =
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1372
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1373
              val name = nickname_of_thm th
57406
e844dcf57deb killed dead code
blanchet
parents: 57405
diff changeset
  1374
              val feats = features_of ctxt (theory_of_thm th) stature [prop_of th]
48439
67a6bcbd3587 removed MaSh junk arising from primrec definitions
blanchet
parents: 48438
diff changeset
  1375
              val deps = deps_of status th |> these
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1376
              val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1377
              val learns = (name, parents, feats, deps) :: learns
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1378
              val (learns, next_commit) =
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1379
                if Time.> (Timer.checkRealTimer timer, next_commit) then
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1380
                  (commit false learns [] []; ([], next_commit_time ()))
48392
ca998fa08cd9 added "learn_from_atp" command to MaSh, for patient users
blanchet
parents: 48390
diff changeset
  1381
                else
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1382
                  (learns, next_commit)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1383
              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
  1384
            in
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1385
              (learns, (num_nontrivial, next_commit, timed_out))
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1386
            end
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1387
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1388
        val (num_new_facts, num_nontrivial) =
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1389
          if no_new_facts then
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1390
            (0, 0)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1391
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1392
            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
  1393
              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
  1394
                |> 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
  1395
                |> 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
  1396
                |> filter_out (is_in_access_G o snd)
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1397
              val (learns, (num_nontrivial, _, _)) =
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1398
                ([], (0, next_commit_time (), false))
51182
962190eab40d provide two modes for MaSh driver: linearized or real visibility
blanchet
parents: 51181
diff changeset
  1399
                |> 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
  1400
            in
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1401
              commit true learns [] []; (length new_facts, num_nontrivial)
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1402
            end
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1403
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1404
        fun relearn_old_fact _ (accum as (_, (_, _, true))) = accum
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1405
          | relearn_old_fact ((_, (_, status)), th)
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1406
              ((relearns, flops), (num_nontrivial, next_commit, _)) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1407
            let
50624
4d0997abce79 improved thm order hack, in case the default names are overridden
blanchet
parents: 50623
diff changeset
  1408
              val name = nickname_of_thm th
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1409
              val (num_nontrivial, relearns, flops) =
55286
blanchet
parents: 55202
diff changeset
  1410
                (case deps_of status th of
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1411
                  SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1412
                | NONE => (num_nontrivial, relearns, name :: flops))
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1413
              val (relearns, flops, next_commit) =
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1414
                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
  1415
                  (commit false [] relearns flops; ([], [], next_commit_time ()))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1416
                else
50631
b69079c14665 tuned ML function names
blanchet
parents: 50624
diff changeset
  1417
                  (relearns, flops, next_commit)
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1418
              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
  1419
            in
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1420
              ((relearns, flops), (num_nontrivial, next_commit, timed_out))
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1421
            end
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1422
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1423
        val num_nontrivial =
51177
e8c9755fd14e tuned code: factored out parent computation
blanchet
parents: 51176
diff changeset
  1424
          if not run_prover then
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1425
            num_nontrivial
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1426
          else
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1427
            let
48668
5d63c23b4042 remember which MaSh proofs were found using ATPs
blanchet
parents: 48667
diff changeset
  1428
              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
  1429
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1430
              fun priority_of th =
57062
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1431
                random_range 0 max_isar +
eb6777796782 avoid slow inspection of proof terms now that dependencies are stored in 'state'
blanchet
parents: 57061
diff changeset
  1432
                (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
  1433
                  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
  1434
                | 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
  1435
                | 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
  1436
                | 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
  1437
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1438
              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
  1439
                |> 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
  1440
                |> 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
  1441
                |> 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
  1442
                |> map snd
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1443
              val ((relearns, flops), (num_nontrivial, _, _)) =
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1444
                (([], []), (num_nontrivial, next_commit_time (), false))
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1445
                |> 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
  1446
            in
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1447
              commit true [] relearns flops; num_nontrivial
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1448
            end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1449
      in
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1450
        if verbose orelse auto_level < 2 then
57385
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1451
          "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1452
          string_of_int num_nontrivial ^ " nontrivial " ^
0eb0c7b93676 tuned output
blanchet
parents: 57384
diff changeset
  1453
          (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^
57006
blanchet
parents: 57005
diff changeset
  1454
          (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
  1455
        else
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1456
          ""
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1457
      end
48308
89674e5a4d35 make tracing an option
blanchet
parents: 48306
diff changeset
  1458
  end
48304
50e64af9c829 more work on MaSh
blanchet
parents: 48303
diff changeset
  1459
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
  1460
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
  1461
  let
48396
dd82d190c2af name tuning
blanchet
parents: 48395
diff changeset
  1462
    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
  1463
    val ctxt = ctxt |> Config.put instantiate_inducts false
57006
blanchet
parents: 57005
diff changeset
  1464
    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
  1465
      |> sort (crude_thm_ord o pairself snd o swap)
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1466
    val num_facts = length facts
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1467
    val prover = hd provers
57006
blanchet
parents: 57005
diff changeset
  1468
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
  1469
    fun learn auto_level run_prover =
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1470
      mash_learn_facts ctxt params prover auto_level run_prover one_year facts
48404
0a261b4aa093 relearn ATP proofs
blanchet
parents: 48403
diff changeset
  1471
      |> Output.urgent_message
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1472
  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
  1473
    if run_prover then
57017
blanchet
parents: 57014
diff changeset
  1474
      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
blanchet
parents: 57014
diff changeset
  1475
         plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^
blanchet
parents: 57014
diff changeset
  1476
         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
  1477
       learn 1 false;
57017
blanchet
parents: 57014
diff changeset
  1478
       Output.urgent_message "Now collecting automatic proofs. This may take several hours. You \
blanchet
parents: 57014
diff changeset
  1479
         \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
  1480
       learn 0 true)
72519bf5f135 simplify MaSh term patterns + add missing global facts if there aren't too many
blanchet
parents: 50339
diff changeset
  1481
    else
57006
blanchet
parents: 57005
diff changeset
  1482
      (Output.urgent_message ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
blanchet
parents: 57005
diff changeset
  1483
         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
  1484
       learn 0 false)
48316
252f45c04042 drastic overhaul of MaSh data structures + fixed a few performance issues
blanchet
parents: 48315
diff changeset
  1485
  end
48249
2bd242c56c90 dummy implementation
blanchet
parents: 48248
diff changeset
  1486
57555
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1487
fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#access_G (peek_state ctxt)))
50311
c9d7ccd090e1 tuned order of functions
blanchet
parents: 50310
diff changeset
  1488
57274
0acfdb151e52 more generous formula -- there are lots of duplicates out there
blanchet
parents: 57273
diff changeset
  1489
(* 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
  1490
   reasons (e.g., duplicates). *)
0acfdb151e52 more generous formula -- there are lots of duplicates out there
blanchet
parents: 57273
diff changeset
  1491
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
  1492
50814
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1493
val mepo_weight = 0.5
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1494
val mash_weight = 0.5
4247cbd78aaf export MeSh data as well
blanchet
parents: 50755
diff changeset
  1495
53152
cbd3c7c48d2c learn new facts on query if there aren't too many of them in MaSh
blanchet
parents: 53150
diff changeset
  1496
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
  1497
57005
33f3d2ea803d store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
blanchet
parents: 56995
diff changeset
  1498
(* 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
  1499
   and Try. *)
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1500
val min_secs_for_learning = 15
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1501
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1502
fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover
57405
1f49da059947 reintroduced 'extra features' + only print message in verbose mode
blanchet
parents: 57404
diff changeset
  1503
    max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1504
  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
  1505
    error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1506
  else if only then
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1507
    [("", map fact_of_raw_fact facts)]
48321
c552d7f1720b learn from minimized ATP proofs
blanchet
parents: 48320
diff changeset
  1508
  else if max_facts <= 0 orelse null facts then
51010
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
  1509
    [("", [])]
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1510
  else
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1511
    let
57407
140e16bc2a40 use right theory name for theorems in evaluation driver
blanchet
parents: 57406
diff changeset
  1512
      val thy = Proof_Context.theory_of ctxt
140e16bc2a40 use right theory name for theorems in evaluation driver
blanchet
parents: 57406
diff changeset
  1513
57555
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1514
      fun maybe_launch_thread exact min_num_facts_to_learn =
57273
01b68f625550 automatically learn MaSh facts also in 'blocking' mode
blanchet
parents: 57150
diff changeset
  1515
        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
  1516
           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
  1517
          let val timeout = time_mult learn_timeout_slack timeout in
57405
1f49da059947 reintroduced 'extra features' + only print message in verbose mode
blanchet
parents: 57404
diff changeset
  1518
            (if verbose then
57555
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1519
               Output.urgent_message ("Started MaShing through " ^
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1520
                 (if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1521
                 " fact" ^ plural_s min_num_facts_to_learn ^ " in the background.")
57405
1f49da059947 reintroduced 'extra features' + only print message in verbose mode
blanchet
parents: 57404
diff changeset
  1522
             else
1f49da059947 reintroduced 'extra features' + only print message in verbose mode
blanchet
parents: 57404
diff changeset
  1523
               ());
54816
10d48c2a3e32 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
blanchet
parents: 54799
diff changeset
  1524
            launch_thread timeout
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1525
              (fn () => (true, mash_learn_facts ctxt params prover 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
  1526
          end
48318
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1527
        else
325c8fd0d762 more consolidation of MaSh code
blanchet
parents: 48316
diff changeset
  1528
          ()
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1529
57555
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1530
      fun please_learn () =
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1531
        let
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1532
          val {access_G, xtabs = ((num_facts0, _), _), ...} = peek_state ctxt
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1533
          val is_in_access_G = is_fact_in_graph access_G o snd
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1534
          val min_num_facts_to_learn = length facts - num_facts0
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1535
        in
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1536
          if min_num_facts_to_learn <= max_facts_to_learn_before_query then
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1537
            (case length (filter_out is_in_access_G facts) of
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1538
              0 => ()
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1539
            | num_facts_to_learn =>
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1540
              if num_facts_to_learn <= max_facts_to_learn_before_query then
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1541
                mash_learn_facts ctxt params prover 2 false timeout facts
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1542
                |> (fn "" => () | s => Output.urgent_message (MaShN ^ ": " ^ s))
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1543
              else
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1544
                maybe_launch_thread true num_facts_to_learn)
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1545
          else
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1546
            maybe_launch_thread false min_num_facts_to_learn
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1547
        end
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1548
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1549
      val mash_enabled = is_mash_enabled ()
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1550
      val _ =
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1551
        if learn andalso mash_enabled andalso fact_filter <> SOME mepoN then please_learn () else ()
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1552
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1553
      val effective_fact_filter =
55286
blanchet
parents: 55202
diff changeset
  1554
        (case fact_filter of
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1555
          SOME ff => ff
57555
f60d70566525 also learn when 'fact_filter =' is set explicitly
blanchet
parents: 57554
diff changeset
  1556
        | NONE => if mash_enabled andalso mash_can_suggest_facts ctxt then meshN else mepoN)
54143
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1557
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1558
      val unique_facts = drop_duplicate_facts facts
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1559
      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
  1560
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
  1561
      fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1562
51003
198cb05fb35b report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents: 51001
diff changeset
  1563
      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
  1564
        (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
  1565
           [] => accepts
57150
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1566
         | _ =>
f591096a9c94 add option to keep duplicates, for more precise evaluation of relevance filters
blanchet
parents: 57133
diff changeset
  1567
           (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
  1568
        |> take max_facts
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1569
48406
b002cc16aa99 honor suggested MaSh weights
blanchet
parents: 48404
diff changeset
  1570
      fun mepo () =
54143
18def1c73c79 make sure add: doesn't add duplicates, and works for [no_atp] facts
blanchet
parents: 54141
diff changeset
  1571
        (mepo_suggested_facts ctxt params max_facts NONE hyp_ts concl_t unique_facts
54091
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1572
         |> weight_facts_steeply, [])
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1573
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1574
      fun mash () =
57407
140e16bc2a40 use right theory name for theorems in evaluation driver
blanchet
parents: 57406
diff changeset
  1575
        mash_suggested_facts ctxt thy params (generous_max_suggestions max_facts) hyp_ts concl_t
140e16bc2a40 use right theory name for theorems in evaluation driver
blanchet
parents: 57406
diff changeset
  1576
          facts
53140
a1235e90da5f pour extra features from proximate facts into goal, in exporter
blanchet
parents: 53137
diff changeset
  1577
        |>> weight_facts_steeply
57018
142950e9c7e2 more flexible environment variable
blanchet
parents: 57017
diff changeset
  1578
48314
ee33ba3c0e05 added option to control which fact filter is used
blanchet
parents: 48313
diff changeset
  1579
      val mess =
51003
198cb05fb35b report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
blanchet
parents: 51001
diff changeset
  1580
        (* the order is important for the "case" expression below *)
54091
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1581
        [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1582
           |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo)
4df62d7eae34 parallelize MeSh
blanchet
parents: 54089
diff changeset
  1583
           |> 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
  1584
      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
  1585
    in
55286
blanchet
parents: 55202
diff changeset
  1586
      (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
  1587
        (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
57658
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1588
        [(meshN, mesh),
f55c173a3cbc beware of duplicate fact names
blanchet
parents: 57574
diff changeset
  1589
         (mepoN, mepo |> map fst |> add_and_take),
51010
afd0213a3dab tuned data structure
blanchet
parents: 51008
diff changeset
  1590
         (mashN, mash |> map fst |> add_and_take)]
55286
blanchet
parents: 55202
diff changeset
  1591
      | _ => [(effective_fact_filter, mesh)])
48288
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1592
    end
255c6e1fd505 rationalize relevance filter, slowing moving code from Iter to MaSh
blanchet
parents: 48251
diff changeset
  1593
57431
02c408aed5ee killed Python version of MaSh, now that the SML version works adequately
blanchet
parents: 57409
diff changeset
  1594
fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
48319
340187063d84 use async manager to manage MaSh learners to make sure they get killed cleanly
blanchet
parents: 48318
diff changeset
  1595
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
  1596
48248
b6eb45a52c28 split relevance filter code into three files
blanchet
parents:
diff changeset
  1597
end;