--- 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)
--- 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)
--- 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
--- 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)
--- 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
--- 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 => [])