# HG changeset patch
# User blanchet
# Date 1406220398 -7200
# Node ID 86b853448f08df6a11591d6c7621c7a136fc6048
# Parent  b246943b3aa33ac09c1e9b72527c585ee1c23fb9
fixed sorting (broken since 9cc802a8ab06)

diff -r b246943b3aa3 -r 86b853448f08 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
@@ -197,7 +197,7 @@
 fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1)
 fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
 
-fun rev_sort_array_prefix cmp bnd a =
+fun sort_array_suffix cmp needed a =
   let
     exception BOTTOM of int
 
@@ -246,7 +246,7 @@
     fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1))
 
     fun for2 i =
-      if i < Integer.max 2 (al - bnd) then
+      if i < Integer.max 2 (al - needed) then
         ()
       else
         let val e = Array.sub (a, i) in
@@ -266,10 +266,10 @@
       ()
   end
 
-fun rev_sort_list_prefix cmp bnd xs =
+fun rev_sort_list_prefix cmp needed xs =
   let val ary = Array.fromList xs in
-    rev_sort_array_prefix cmp bnd ary;
-    Array.foldr (op ::) [] ary
+    sort_array_suffix cmp needed ary;
+    Array.foldl (op ::) [] ary
   end
 
 
@@ -363,7 +363,7 @@
       if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
   in
     select_visible_facts 100000.0 posterior visible_facts;
-    rev_sort_array_prefix (Real.compare o pairself snd) max_suggs posterior;
+    sort_array_suffix (Real.compare o pairself snd) max_suggs posterior;
     ret (Integer.max 0 (num_facts - max_suggs)) []
   end
 
@@ -396,7 +396,7 @@
       end
 
     val _ = List.app do_feat goal_feats
-    val _ = rev_sort_array_prefix (Real.compare o pairself snd) num_facts overlaps_sqr
+    val _ = sort_array_suffix (Real.compare o pairself snd) num_facts overlaps_sqr
     val no_recommends = Unsynchronized.ref 0
     val recommends = Array.tabulate (num_facts, rpair 0.0)
     val age = Unsynchronized.ref 500000000.0
@@ -438,7 +438,7 @@
     while1 ();
     while2 ();
     select_visible_facts 1000000000.0 recommends visible_facts;
-    rev_sort_array_prefix (Real.compare o pairself snd) max_suggs recommends;
+    sort_array_suffix (Real.compare o pairself snd) max_suggs recommends;
     ret [] (Integer.max 0 (num_facts - max_suggs))
   end
 
@@ -1126,7 +1126,7 @@
 val extra_feature_factor = 0.1 (* FUDGE *)
 val num_extra_feature_facts = 10 (* FUDGE *)
 
-val max_proximity_facts = 100
+val max_proximity_facts = 100 (* FUDGE *)
 
 fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
   let