# HG changeset patch
# User blanchet
# Date 1403782517 -7200
# Node ID c1060d10089f54071dc3479714bd246caaf7edb3
# Parent  a6a6472a2536f5113d4d1267932ec0312045ca03
honor visible in SML naive Bayes

diff -r a6a6472a2536 -r c1060d10089f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:12 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:17 2014 +0200
@@ -406,6 +406,12 @@
 
 val number_of_nearest_neighbors = 10 (* FUDGE *)
 
+fun select_visible_facts recommends =
+  List.app (fn at =>
+    let val (j, ov) = Array.sub (recommends, at) in
+      Array.update (recommends, at, (j, 1000000000.0 + ov))
+    end)
+
 exception EXIT of unit
 
 fun k_nearest_neighbors num_facts get_deps get_sym_ths max_suggs visible_facts num_feats feats =
@@ -475,12 +481,9 @@
     fun ret acc at =
       if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
   in
-    while1 (); while2 ();
-    List.app (fn at =>
-        let val (j, ov) = Array.sub (recommends, at) in
-          Array.update (recommends, at, (j, 1000000000.0 + ov))
-        end)
-      visible_facts;
+    while1 ();
+    while2 ();
+    select_visible_facts recommends visible_facts;
     heap (Real.compare o pairself snd) max_suggs num_facts recommends;
     ret [] (Integer.max 0 (num_facts - max_suggs))
   end
@@ -556,11 +559,12 @@
 
     val posterior = Array.tabulate (num_facts, (fn j => (j, log_posterior j)))
 
-    fun ret acc at =
-      if at = num_facts then acc else ret (Array.sub (posterior, at) :: acc) (at + 1)
+    fun ret at acc =
+      if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
   in
+    select_visible_facts posterior visible_facts;
     heap (Real.compare o pairself snd) max_suggs num_facts posterior;
-    ret [] (Integer.max 0 (num_facts - max_suggs))
+    ret (Integer.max 0 (num_facts - max_suggs)) []
   end
 
 fun naive_bayes num_facts get_deps get_feats num_feats max_suggs visible_facts feats =