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