# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID 7b5f7ca25d17317c5f8fdd7b9e0b6c04365951d9
# Parent  8a8d71e34297f8c4b2cb1837343c23d3a78182e8
optimized MaSh output by chunking it

diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -9,6 +9,7 @@
   val timestamp : unit -> string
   val hash_string : string -> int
   val hash_term : term -> int
+  val chunk_list : int -> 'a list -> 'a list list
   val stringN_of_int : int -> int -> string
   val strip_spaces : bool -> (char -> bool) -> string -> string
   val strip_spaces_except_between_idents : string -> string
@@ -67,6 +68,10 @@
 fun hash_string s = Word.toInt (hashw_string (s, 0w0))
 val hash_term = Word.toInt o hashw_term
 
+fun chunk_list _ [] = []
+  | chunk_list k xs =
+    let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end
+
 fun stringN_of_int 0 _ = ""
   | stringN_of_int k n =
     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -1038,7 +1038,7 @@
           run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
         end
 
-    val batches = batch_list batch_size (!scopes)
+    val batches = chunk_list batch_size (!scopes)
     val outcome_code =
       run_batches 0 (length batches) batches
                   (false, max_potential, max_genuine, 0)
diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -619,7 +619,7 @@
         make_fun_or_set true T T1 T2 T'
             (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
             (map (term_for_rep true seen T2 T2 R o single)
-                 (batch_list (arity_of_rep R) js))
+                 (chunk_list (arity_of_rep R) js))
       end
     and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
         if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -1111,7 +1111,7 @@
     end
   | shape_tuple T (R as Vect (k, R')) us =
     Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
-                     (batch_list (length us div k) us))
+                     (chunk_list (length us div k) us))
   | shape_tuple T _ [u] =
     if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
   | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -38,7 +38,7 @@
   val nth_combination : (int * int) list -> int -> int list
   val all_combinations : (int * int) list -> int list list
   val all_permutations : 'a list -> 'a list list
-  val batch_list : int -> 'a list -> 'a list list
+  val chunk_list : int -> 'a list -> 'a list list
   val chunk_list_unevenly : int list -> 'a list -> 'a list list
   val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val double_lookup :
@@ -192,15 +192,12 @@
     maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
          (index_seq 0 (length xs))
 
-fun batch_list _ [] = []
-  | batch_list k xs =
-    if length xs <= k then [xs]
-    else List.take (xs, k) :: batch_list k (List.drop (xs, k))
+val chunk_list = ATP_Util.chunk_list
 
 fun chunk_list_unevenly _ [] = []
-  | chunk_list_unevenly [] ys = map single ys
-  | chunk_list_unevenly (k :: ks) ys =
-    let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
+  | chunk_list_unevenly [] xs = map single xs
+  | chunk_list_unevenly (k :: ks) xs =
+    let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end
 
 fun map3 _ [] [] [] = []
   | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
diff -r 8a8d71e34297 -r 7b5f7ca25d17 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -313,9 +313,11 @@
 
 (*** Low-level communication with MaSh ***)
 
-fun write_file write file =
+fun write_file (xs, f) file =
   let val path = Path.explode file in
-    File.write path ""; write (File.append path)
+    File.write path "";
+    xs |> chunk_list 500
+       |> List.app (File.append path o space_implode "" o map f)
   end
 
 fun mash_info overlord =
@@ -331,8 +333,8 @@
       " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
   in
     trace_msg ctxt (fn () => "Running " ^ command);
-    write_file (K ()) log_file;
-    write_file (K ()) err_file;
+    write_file ([], K "") log_file;
+    write_file ([], K "") err_file;
     Isabelle_System.bash command; ()
   end
 
@@ -354,7 +356,7 @@
     val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
   in
-    write_file (K ()) sugg_file;
+    write_file ([], K "") sugg_file;
     write_file write_cmds cmd_file;
     run_mash ctxt info
              ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
@@ -385,22 +387,19 @@
   | mash_INIT ctxt overlord upds =
     (trace_msg ctxt (fn () => "MaSh INIT " ^
          elide_string 1000 (space_implode " " (map #1 upds)));
-     run_mash_init ctxt overlord
-         (fn append => List.app (append o init_str_of_update #2) upds)
-         (fn append => List.app (append o init_str_of_update #3) upds)
-         (fn append => List.app (append o init_str_of_update #4) upds))
+     run_mash_init ctxt overlord (upds, init_str_of_update #2)
+                   (upds, init_str_of_update #3) (upds, init_str_of_update #4))
 
 fun mash_ADD _ _ [] = ()
   | 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 0
-         (fn append => List.app (append o str_of_update) upds) (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 max_suggs
-       (fn append => append (str_of_query query))
+       ([query], str_of_query)
        (fn suggs => snd (extract_query (List.last (suggs ()))))
    handle List.Empty => [])