36 val isabelle_dependencies_of : unit Symtab.table -> thm -> string list |
36 val isabelle_dependencies_of : unit Symtab.table -> thm -> string list |
37 val goal_of_thm : theory -> thm -> thm |
37 val goal_of_thm : theory -> thm -> thm |
38 val run_prover_for_mash : |
38 val run_prover_for_mash : |
39 Proof.context -> params -> string -> fact list -> thm -> prover_result |
39 Proof.context -> params -> string -> fact list -> thm -> prover_result |
40 val mash_CLEAR : Proof.context -> unit |
40 val mash_CLEAR : Proof.context -> unit |
41 val mash_INIT : |
|
42 Proof.context -> bool |
|
43 -> (string * string list * string list * string list) list -> unit |
|
44 val mash_ADD : |
41 val mash_ADD : |
45 Proof.context -> bool |
42 Proof.context -> bool |
46 -> (string * string list * string list * string list) list -> unit |
43 -> (string * string list * string list * string list) list -> unit |
47 val mash_QUERY : |
44 val mash_QUERY : |
48 Proof.context -> bool -> int -> string list * string list -> string list |
45 Proof.context -> bool -> int -> string list * string list -> string list |
339 write_file ([], K "") err_file; |
336 write_file ([], K "") err_file; |
340 Isabelle_System.bash command; |
337 Isabelle_System.bash command; |
341 if not async then trace_msg ctxt (K "Done") else () |
338 if not async then trace_msg ctxt (K "Done") else () |
342 end |
339 end |
343 |
340 |
344 (* TODO: Eliminate code once "mash.py" handles sequences of ADD commands as fast |
|
345 as a single INIT. *) |
|
346 fun run_mash_init ctxt overlord write_access write_feats write_deps = |
|
347 let |
|
348 val info as (temp_dir, serial) = mash_info overlord |
|
349 val in_dir = temp_dir ^ "/mash_init" ^ serial |
|
350 |> tap (Path.explode #> Isabelle_System.mkdir) |
|
351 in |
|
352 write_file write_access (in_dir ^ "/mash_accessibility"); |
|
353 write_file write_feats (in_dir ^ "/mash_features"); |
|
354 write_file write_deps (in_dir ^ "/mash_dependencies"); |
|
355 run_mash ctxt overlord info false |
|
356 ("--init --inputDir " ^ in_dir ^ |
|
357 and_rm_files overlord " -r" [in_dir]) |
|
358 end |
|
359 |
|
360 fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs = |
341 fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs = |
361 let |
342 let |
362 val info as (temp_dir, serial) = mash_info overlord |
343 val info as (temp_dir, serial) = mash_info overlord |
363 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
344 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial |
364 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
345 val cmd_file = temp_dir ^ "/mash_commands" ^ serial |
378 escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" |
359 escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" |
379 |
360 |
380 fun str_of_query (parents, feats) = |
361 fun str_of_query (parents, feats) = |
381 "? " ^ escape_metas parents ^ "; " ^ escape_metas feats |
362 "? " ^ escape_metas parents ^ "; " ^ escape_metas feats |
382 |
363 |
383 fun init_str_of_update get (upd as (name, _, _, _)) = |
|
384 escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n" |
|
385 |
|
386 fun mash_CLEAR ctxt = |
364 fun mash_CLEAR ctxt = |
387 let val path = mash_state_dir () |> Path.explode in |
365 let val path = mash_state_dir () |> Path.explode in |
388 trace_msg ctxt (K "MaSh CLEAR"); |
366 trace_msg ctxt (K "MaSh CLEAR"); |
389 File.fold_dir (fn file => fn () => |
367 File.fold_dir (fn file => fn () => |
390 File.rm (Path.append path (Path.basic file))) |
368 File.rm (Path.append path (Path.basic file))) |
391 path () |
369 path () |
392 end |
370 end |
393 |
|
394 fun mash_INIT ctxt _ [] = mash_CLEAR ctxt |
|
395 | mash_INIT ctxt overlord upds = |
|
396 (trace_msg ctxt (fn () => "MaSh INIT " ^ |
|
397 elide_string 1000 (space_implode " " (map #1 upds))); |
|
398 run_mash_init ctxt overlord (upds, init_str_of_update #2) |
|
399 (upds, init_str_of_update #3) (upds, init_str_of_update #4)) |
|
400 |
371 |
401 fun mash_ADD _ _ [] = () |
372 fun mash_ADD _ _ [] = () |
402 | mash_ADD ctxt overlord upds = |
373 | mash_ADD ctxt overlord upds = |
403 (trace_msg ctxt (fn () => "MaSh ADD " ^ |
374 (trace_msg ctxt (fn () => "MaSh ADD " ^ |
404 elide_string 1000 (space_implode " " (map #1 upds))); |
375 elide_string 1000 (space_implode " " (map #1 upds))); |
625 val ((_, upds), _) = |
596 val ((_, upds), _) = |
626 ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev |
597 ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev |
627 val n = length upds |
598 val n = length upds |
628 fun trans {thys, fact_graph} = |
599 fun trans {thys, fact_graph} = |
629 let |
600 let |
630 val mash_INIT_or_ADD = |
|
631 if Graph.is_empty fact_graph then mash_INIT else mash_ADD |
|
632 val (upds, fact_graph) = |
601 val (upds, fact_graph) = |
633 ([], fact_graph) |> fold (update_fact_graph ctxt) upds |
602 ([], fact_graph) |> fold (update_fact_graph ctxt) upds |
634 in |
603 in |
635 (mash_INIT_or_ADD ctxt overlord (rev upds); |
604 (mash_ADD ctxt overlord (rev upds); |
636 {thys = thys |> add_thys_for thy, fact_graph = fact_graph}) |
605 {thys = thys |> add_thys_for thy, fact_graph = fact_graph}) |
637 end |
606 end |
638 in |
607 in |
639 mash_map ctxt trans; |
608 mash_map ctxt trans; |
640 if verbose then |
609 if verbose then |