learn command in MaSh

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -35,9 +35,11 @@
 val supported_proversN = "supported_provers"
 val kill_proversN = "kill_provers"
 val running_proversN = "running_provers"
+val unlearnN = "unlearn"
+val learnN = "learn"
+val relearnN = "relearn"
 val kill_learnersN = "kill_learners"
 val running_learnersN = "running_learners"
-val unlearnN = "unlearn"
 val refresh_tptpN = "refresh_tptp"
 
 val auto = Unsynchronized.ref false
@@ -245,8 +247,7 @@
                          end)]
   end
 
-val infinity_time_in_secs = 60 * 60 * 24 * 365
-val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
+val the_timeout = the_default infinite_timeout
 
 fun extract_params mode default_params override_params =
   let
@@ -383,12 +384,16 @@
       kill_provers ()
     else if subcommand = running_proversN then
       running_provers ()
+    else if subcommand = unlearnN then
+      mash_unlearn ctxt
+    else if subcommand = learnN orelse subcommand = relearnN then
+      (if subcommand = relearnN then mash_unlearn ctxt else ();
+       mash_learn ctxt (get_params Normal ctxt
+                                   (("verbose", ["true"]) :: override_params)))
     else if subcommand = kill_learnersN then
       kill_learners ()
     else if subcommand = running_learnersN then
       running_learners ()
-    else if subcommand = unlearnN then
-      mash_unlearn ctxt
     else if subcommand = refresh_tptpN then
       refresh_systems_on_tptp ()
     else

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -53,10 +53,11 @@
   val mash_suggest_facts :
     Proof.context -> params -> string -> int -> term list -> term
     -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
+  val mash_learn_proof :
+    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
   val mash_learn_thy :
     Proof.context -> params -> theory -> Time.time -> fact list -> string
-  val mash_learn_proof :
-    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
+  val mash_learn : Proof.context -> params -> unit
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> fact list -> fact list
@@ -350,12 +351,12 @@
     write_file write_access (in_dir ^ "/mash_accessibility");
     write_file write_feats (in_dir ^ "/mash_features");
     write_file write_deps (in_dir ^ "/mash_dependencies");
-    run_mash ctxt overlord info true
+    run_mash ctxt overlord info false
              ("--init --inputDir " ^ in_dir ^
               and_rm_files overlord " -r" [in_dir])
   end
 
-fun run_mash_commands ctxt overlord async save max_suggs write_cmds read_suggs =
+fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
   let
     val info as (temp_dir, serial) = mash_info overlord
     val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
@@ -363,7 +364,7 @@
   in
     write_file ([], K "") sugg_file;
     write_file write_cmds cmd_file;
-    run_mash ctxt overlord info async
+    run_mash ctxt overlord info false
              ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
               " --numberOfPredictions " ^ string_of_int max_suggs ^
               (if save then " --saveModel" else "") ^
@@ -400,11 +401,11 @@
   | mash_ADD ctxt overlord upds =
     (trace_msg ctxt (fn () => "MaSh ADD " ^
          elide_string 1000 (space_implode " " (map #1 upds)));
-     run_mash_commands ctxt overlord true true 0 (upds, str_of_update) (K ()))
+     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
 
 fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
   (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
-   run_mash_commands ctxt overlord false false max_suggs
+   run_mash_commands ctxt overlord false  max_suggs
        ([query], str_of_query)
        (fn suggs => snd (extract_query (List.last (suggs ()))))
    handle List.Empty => [])
@@ -548,6 +549,26 @@
 
 val pass1_learn_timeout_factor = 0.5
 
+fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val prover = hd provers
+    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
+    val feats = features_of ctxt prover thy General [t]
+    val deps = used_ths |> map nickname_of
+  in
+    mash_map ctxt (fn {thys, fact_graph} =>
+        let
+          val parents = parents_wrt_facts facts fact_graph
+          val upds = [(name, parents, feats, deps)]
+          val (upds, fact_graph) =
+            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
+        in
+          mash_ADD ctxt overlord upds;
+          {thys = thys, fact_graph = fact_graph}
+        end)
+  end
+
 (* Too many dependencies is a sign that a decision procedure is at work. There
    isn't much too learn from such proofs. *)
 val max_dependencies = 10
@@ -596,13 +617,12 @@
               ([], fact_graph) |> fold (update_fact_graph ctxt) upds
           in
             (mash_INIT_or_ADD ctxt overlord (rev upds);
-             {thys = thys |> add_thys_for thy,
-              fact_graph = fact_graph})
+             {thys = thys |> add_thys_for thy, fact_graph = fact_graph})
           end
       in
         mash_map ctxt trans;
         if verbose then
-          "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
+          "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
           (if verbose then
              " in " ^ string_from_time (Timer.checkRealTimer timer)
            else
@@ -612,24 +632,16 @@
       end
   end
 
-fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
+fun mash_learn ctxt params =
   let
     val thy = Proof_Context.theory_of ctxt
-    val prover = hd provers
-    val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
-    val feats = features_of ctxt prover thy General [t]
-    val deps = used_ths |> map nickname_of
+    val _ = Output.urgent_message "MaShing..."
+    val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val facts = all_facts_of thy css_table
   in
-    mash_map ctxt (fn {thys, fact_graph} =>
-        let
-          val parents = parents_wrt_facts facts fact_graph
-          val upds = [(name, parents, feats, deps)]
-          val (upds, fact_graph) =
-            ([], fact_graph) |> fold (update_fact_graph ctxt) upds
-        in
-          mash_ADD ctxt overlord upds;
-          {thys = thys, fact_graph = fact_graph}
-        end)
+     mash_learn_thy ctxt params thy infinite_timeout facts
+     |> (fn "" => "Learned nothing." | msg => msg)
+     |> Output.urgent_message
   end
 
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -9,6 +9,7 @@
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
   val simplify_spaces : string -> string
+  val infinite_timeout : Time.time
   val time_mult : real -> Time.time -> Time.time
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
@@ -27,6 +28,8 @@
 val serial_commas = Try.serial_commas
 val simplify_spaces = strip_spaces false (K true)
 
+val infinite_timeout = seconds 31536000.0 (* one year *)
+
 fun time_mult k t =
   Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))