143 fun write_file banner (xs, f) path = |
143 fun write_file banner (xs, f) path = |
144 (case banner of SOME s => File.write path s | NONE => (); |
144 (case banner of SOME s => File.write path s | NONE => (); |
145 xs |> chunk_list 500 |> List.app (File.append path o implode o map f)) |
145 xs |> chunk_list 500 |> List.app (File.append path o implode o map f)) |
146 handle IO.Io _ => () |
146 handle IO.Io _ => () |
147 |
147 |
148 fun run_mash_tool ctxt overlord save write_cmds read_suggs = |
148 fun run_mash_tool ctxt overlord write_cmds read_suggs = |
149 let |
149 let |
150 val (temp_dir, serial) = |
150 val (temp_dir, serial) = |
151 if overlord then (getenv "ISABELLE_HOME_USER", "") |
151 if overlord then (getenv "ISABELLE_HOME_USER", "") |
152 else (getenv "ISABELLE_TMP", serial_string ()) |
152 else (getenv "ISABELLE_TMP", serial_string ()) |
153 val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" |
153 val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" |
155 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
155 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
156 val sugg_path = Path.explode sugg_file |
156 val sugg_path = Path.explode sugg_file |
157 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
157 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
158 val cmd_path = Path.explode cmd_file |
158 val cmd_path = Path.explode cmd_file |
159 val model_dir = File.shell_path (mash_model_dir ()) |
159 val model_dir = File.shell_path (mash_model_dir ()) |
160 val core = |
160 val core = "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file |
161 "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
|
162 " --numberOfPredictions " ^ string_of_int max_suggs ^ |
|
163 (if save then " --saveModel" else "") |
|
164 val command = |
161 val command = |
165 "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^ |
162 "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^ |
166 "./mash.py --quiet" ^ |
163 "./mash.py --quiet" ^ |
167 " --outputDir " ^ model_dir ^ |
164 " --outputDir " ^ model_dir ^ |
168 " --modelFile=" ^ model_dir ^ "/model.pickle" ^ |
165 " --modelFile=" ^ model_dir ^ "/model.pickle" ^ |
260 |
257 |
261 fun learn _ _ [] = () |
258 fun learn _ _ [] = () |
262 | learn ctxt overlord learns = |
259 | learn ctxt overlord learns = |
263 (trace_msg ctxt (fn () => "MaSh learn " ^ |
260 (trace_msg ctxt (fn () => "MaSh learn " ^ |
264 elide_string 1000 (space_implode " " (map #1 learns))); |
261 elide_string 1000 (space_implode " " (map #1 learns))); |
265 run_mash_tool ctxt overlord true (learns, str_of_learn) (K ())) |
262 run_mash_tool ctxt overlord (learns, str_of_learn) (K ())) |
266 |
263 |
267 fun relearn _ _ [] = () |
264 fun relearn _ _ [] = () |
268 | relearn ctxt overlord relearns = |
265 | relearn ctxt overlord relearns = |
269 (trace_msg ctxt (fn () => "MaSh relearn " ^ |
266 (trace_msg ctxt (fn () => "MaSh relearn " ^ |
270 elide_string 1000 (space_implode " " (map #1 relearns))); |
267 elide_string 1000 (space_implode " " (map #1 relearns))); |
271 run_mash_tool ctxt overlord true (relearns, str_of_relearn) (K ())) |
268 run_mash_tool ctxt overlord (relearns, str_of_relearn) (K ())) |
272 |
269 |
273 fun query ctxt overlord max_suggs (query as (learns, hints, _, feats)) = |
270 fun query ctxt overlord max_suggs (query as (learns, hints, _, feats)) = |
274 (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); |
271 (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); |
275 run_mash_tool ctxt overlord false ([query], str_of_query max_suggs) |
272 run_mash_tool ctxt overlord ([query], str_of_query max_suggs) |
276 (fn suggs => |
273 (fn suggs => |
277 case suggs () of |
274 case suggs () of |
278 [] => [] |
275 [] => [] |
279 | suggs => snd (extract_suggestions (List.last suggs))) |
276 | suggs => snd (extract_suggestions (List.last suggs))) |
280 handle List.Empty => []) |
277 handle List.Empty => []) |