# HG changeset patch
# User blanchet
# Date 1403807551 -7200
# Node ID 2b6fe2a483528e633f1311120e4ee9c2c23b17c7
# Parent  5980ee29dbf6fdea1d4cc998abeadc452829282c
reintroduced MaSh hints, this time as persistent creatures

diff -r 5980ee29dbf6 -r 2b6fe2a48352 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jun 26 19:40:58 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jun 26 20:32:31 2014 +0200
@@ -264,9 +264,10 @@
                   if outcome_code = someN then accum else launch problem prover)
                 provers
             else
-              provers
-              |> (if blocking then Par_List.map else map) (launch problem #> fst)
-              |> max_outcome_code |> rpair state
+              (learn chained;
+               provers
+               |> (if blocking then Par_List.map else map) (launch problem #> fst)
+               |> max_outcome_code |> rpair state)
           end
       in
         (if blocking then launch_provers state
diff -r 5980ee29dbf6 -r 2b6fe2a48352 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 19:40:58 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 20:32:31 2014 +0200
@@ -260,10 +260,9 @@
 
 fun str_of_relearn (name, deps) = "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
 
-fun str_of_query max_suggs (learns, hints, parents, feats) =
+fun str_of_query max_suggs (learns, parents, feats) =
   implode (map str_of_learn learns) ^
-  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^
-  (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
+  "? " ^ string_of_int max_suggs ^ " # " ^ encode_strs parents ^ "; " ^ encode_features feats ^ "\n"
 
 (* The suggested weights do not make much sense. *)
 fun extract_suggestion sugg =
@@ -307,7 +306,7 @@
      run_mash_tool ctxt overlord ([] |> save ? cons save_models_arg) false
        (relearns, str_of_relearn) (K ()))
 
-fun query ctxt overlord max_suggs (query as (_, _, _, feats)) =
+fun query ctxt overlord max_suggs (query as (_, _, feats)) =
   (trace_msg ctxt (fn () => "MaSh_Py query " ^ encode_features feats);
    run_mash_tool ctxt overlord [] false ([query], str_of_query max_suggs) (fn suggs =>
      (case suggs () of [] => [] | suggs => snd (extract_suggestions (List.last suggs))))
@@ -566,7 +565,7 @@
   in
     MaSh_Py.unlearn ctxt overlord;
     OS.Process.sleep (seconds 2.0); (* hack *)
-    MaSh_Py.query ctxt overlord max_suggs (learns, [], parents', goal_feats')
+    MaSh_Py.query ctxt overlord max_suggs (learns, parents', goal_feats')
     |> map (apfst fact_of_name)
   end
 
@@ -1341,9 +1340,6 @@
     fun query_args access_G =
       let
         val parents = maximal_wrt_access_graph access_G facts
-        val hints = chained
-          |> filter (is_fact_in_graph access_G o snd)
-          |> map (nickname_of_thm o snd)
 
         val goal_feats =
           features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts)
@@ -1361,7 +1357,7 @@
         val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats
           |> debug ? sort (Real.compare o swap o pairself snd)
       in
-        (parents, hints, feats)
+        (parents, feats)
       end
 
     val ((access_G, ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs), py_suggs) =
@@ -1370,8 +1366,8 @@
          if Graph.is_empty access_G then
            (trace_msg ctxt (K "Nothing has been learned yet"); [])
          else if engine = MaSh_Py then
-           let val (parents, hints, feats) = query_args access_G in
-             MaSh_Py.query ctxt overlord max_suggs ([], hints, parents, feats)
+           let val (parents, feats) = query_args access_G in
+             MaSh_Py.query ctxt overlord max_suggs ([], parents, feats)
              |> map fst
            end
          else
@@ -1382,7 +1378,7 @@
         []
       else
         let
-          val (parents, hints, goal_feats0) = query_args access_G
+          val (parents, goal_feats0) = query_args access_G
           val goal_feats = map fst goal_feats0
           val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
         in
@@ -1455,7 +1451,7 @@
   Date.fmt ".%Y%m%d.%H%M%S." (Date.fromTimeLocal (Time.now ())) ^ serial_string ()
 
 fun mash_learn_proof ctxt ({overlord, timeout, ...} : params) t facts used_ths =
-  if is_mash_enabled () then
+  if not (null used_ths) andalso is_mash_enabled () then
     launch_thread timeout (fn () =>
       let
         val thy = Proof_Context.theory_of ctxt