optimized MaSh output by chunking it
authorblanchet
Wed Jul 18 08:44:04 2012 +0200 (2012-07-18 ago)
changeset 483237b5f7ca25d17
parent 48322 8a8d71e34297
child 48324 3ee5b5589402
optimized MaSh output by chunking it
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    val timestamp : unit -> string
     1.5    val hash_string : string -> int
     1.6    val hash_term : term -> int
     1.7 +  val chunk_list : int -> 'a list -> 'a list list
     1.8    val stringN_of_int : int -> int -> string
     1.9    val strip_spaces : bool -> (char -> bool) -> string -> string
    1.10    val strip_spaces_except_between_idents : string -> string
    1.11 @@ -67,6 +68,10 @@
    1.12  fun hash_string s = Word.toInt (hashw_string (s, 0w0))
    1.13  val hash_term = Word.toInt o hashw_term
    1.14  
    1.15 +fun chunk_list _ [] = []
    1.16 +  | chunk_list k xs =
    1.17 +    let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end
    1.18 +
    1.19  fun stringN_of_int 0 _ = ""
    1.20    | stringN_of_int k n =
    1.21      stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jul 18 08:44:04 2012 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Jul 18 08:44:04 2012 +0200
     2.3 @@ -1038,7 +1038,7 @@
     2.4            run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
     2.5          end
     2.6  
     2.7 -    val batches = batch_list batch_size (!scopes)
     2.8 +    val batches = chunk_list batch_size (!scopes)
     2.9      val outcome_code =
    2.10        run_batches 0 (length batches) batches
    2.11                    (false, max_potential, max_genuine, 0)
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 18 08:44:04 2012 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 18 08:44:04 2012 +0200
     3.3 @@ -619,7 +619,7 @@
     3.4          make_fun_or_set true T T1 T2 T'
     3.5              (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
     3.6              (map (term_for_rep true seen T2 T2 R o single)
     3.7 -                 (batch_list (arity_of_rep R) js))
     3.8 +                 (chunk_list (arity_of_rep R) js))
     3.9        end
    3.10      and term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
    3.11          if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jul 18 08:44:04 2012 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jul 18 08:44:04 2012 +0200
     4.3 @@ -1111,7 +1111,7 @@
     4.4      end
     4.5    | shape_tuple T (R as Vect (k, R')) us =
     4.6      Tuple (T, R, map (shape_tuple (pseudo_range_type T) R')
     4.7 -                     (batch_list (length us div k) us))
     4.8 +                     (chunk_list (length us div k) us))
     4.9    | shape_tuple T _ [u] =
    4.10      if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
    4.11    | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Jul 18 08:44:04 2012 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Jul 18 08:44:04 2012 +0200
     5.3 @@ -38,7 +38,7 @@
     5.4    val nth_combination : (int * int) list -> int -> int list
     5.5    val all_combinations : (int * int) list -> int list list
     5.6    val all_permutations : 'a list -> 'a list list
     5.7 -  val batch_list : int -> 'a list -> 'a list list
     5.8 +  val chunk_list : int -> 'a list -> 'a list list
     5.9    val chunk_list_unevenly : int list -> 'a list -> 'a list list
    5.10    val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    5.11    val double_lookup :
    5.12 @@ -192,15 +192,12 @@
    5.13      maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
    5.14           (index_seq 0 (length xs))
    5.15  
    5.16 -fun batch_list _ [] = []
    5.17 -  | batch_list k xs =
    5.18 -    if length xs <= k then [xs]
    5.19 -    else List.take (xs, k) :: batch_list k (List.drop (xs, k))
    5.20 +val chunk_list = ATP_Util.chunk_list
    5.21  
    5.22  fun chunk_list_unevenly _ [] = []
    5.23 -  | chunk_list_unevenly [] ys = map single ys
    5.24 -  | chunk_list_unevenly (k :: ks) ys =
    5.25 -    let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
    5.26 +  | chunk_list_unevenly [] xs = map single xs
    5.27 +  | chunk_list_unevenly (k :: ks) xs =
    5.28 +    let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end
    5.29  
    5.30  fun map3 _ [] [] [] = []
    5.31    | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     6.3 @@ -313,9 +313,11 @@
     6.4  
     6.5  (*** Low-level communication with MaSh ***)
     6.6  
     6.7 -fun write_file write file =
     6.8 +fun write_file (xs, f) file =
     6.9    let val path = Path.explode file in
    6.10 -    File.write path ""; write (File.append path)
    6.11 +    File.write path "";
    6.12 +    xs |> chunk_list 500
    6.13 +       |> List.app (File.append path o space_implode "" o map f)
    6.14    end
    6.15  
    6.16  fun mash_info overlord =
    6.17 @@ -331,8 +333,8 @@
    6.18        " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file
    6.19    in
    6.20      trace_msg ctxt (fn () => "Running " ^ command);
    6.21 -    write_file (K ()) log_file;
    6.22 -    write_file (K ()) err_file;
    6.23 +    write_file ([], K "") log_file;
    6.24 +    write_file ([], K "") err_file;
    6.25      Isabelle_System.bash command; ()
    6.26    end
    6.27  
    6.28 @@ -354,7 +356,7 @@
    6.29      val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
    6.30      val cmd_file = temp_dir ^ "/mash_commands" ^ serial
    6.31    in
    6.32 -    write_file (K ()) sugg_file;
    6.33 +    write_file ([], K "") sugg_file;
    6.34      write_file write_cmds cmd_file;
    6.35      run_mash ctxt info
    6.36               ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
    6.37 @@ -385,22 +387,19 @@
    6.38    | mash_INIT ctxt overlord upds =
    6.39      (trace_msg ctxt (fn () => "MaSh INIT " ^
    6.40           elide_string 1000 (space_implode " " (map #1 upds)));
    6.41 -     run_mash_init ctxt overlord
    6.42 -         (fn append => List.app (append o init_str_of_update #2) upds)
    6.43 -         (fn append => List.app (append o init_str_of_update #3) upds)
    6.44 -         (fn append => List.app (append o init_str_of_update #4) upds))
    6.45 +     run_mash_init ctxt overlord (upds, init_str_of_update #2)
    6.46 +                   (upds, init_str_of_update #3) (upds, init_str_of_update #4))
    6.47  
    6.48  fun mash_ADD _ _ [] = ()
    6.49    | mash_ADD ctxt overlord upds =
    6.50      (trace_msg ctxt (fn () => "MaSh ADD " ^
    6.51           elide_string 1000 (space_implode " " (map #1 upds)));
    6.52 -     run_mash_commands ctxt overlord true 0
    6.53 -         (fn append => List.app (append o str_of_update) upds) (K ()))
    6.54 +     run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
    6.55  
    6.56  fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
    6.57    (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
    6.58     run_mash_commands ctxt overlord false max_suggs
    6.59 -       (fn append => append (str_of_query query))
    6.60 +       ([query], str_of_query)
    6.61         (fn suggs => snd (extract_query (List.last (suggs ()))))
    6.62     handle List.Empty => [])
    6.63