# HG changeset patch
# User blanchet
# Date 1403782512 -7200
# Node ID a6a6472a2536f5113d4d1267932ec0312045ca03
# Parent  3ae07451a9f5a385098223198d5aeef8fc381c5e
honor visibility in SML k-NN

diff -r 3ae07451a9f5 -r a6a6472a2536 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:07 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:12 2014 +0200
@@ -441,7 +441,7 @@
     val _ = heap (Real.compare o pairself snd) num_facts num_facts overlaps_sqr
     val no_recommends = Unsynchronized.ref 0
     val recommends = Array.tabulate (num_facts, rpair 0.0)
-    val age = Unsynchronized.ref 1000000000.0
+    val age = Unsynchronized.ref 500000000.0
 
     fun inc_recommend j v =
       let val ov = snd (Array.sub (recommends, j)) in
@@ -473,9 +473,14 @@
       handle EXIT () => ()
 
     fun ret acc at =
-      if at = Array.length recommends then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
+      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;
     heap (Real.compare o pairself snd) max_suggs num_facts recommends;
     ret [] (Integer.max 0 (num_facts - max_suggs))
   end
@@ -652,7 +657,7 @@
 
         val facts = rev rev_facts
         val fact_vec = Vector.fromList facts
-        val int_visible_facts = map (Symtab.lookup fact_tab) visible_facts
+        val int_visible_facts = map_filter (Symtab.lookup fact_tab) visible_facts
 
         val deps_vec = Vector.fromList (rev rev_depss)