104 fun mash_home () = getenv "MASH_HOME" |
104 fun mash_home () = getenv "MASH_HOME" |
105 fun mash_model_dir () = |
105 fun mash_model_dir () = |
106 getenv "ISABELLE_HOME_USER" ^ "/mash" |
106 getenv "ISABELLE_HOME_USER" ^ "/mash" |
107 |> tap (Isabelle_System.mkdir o Path.explode) |
107 |> tap (Isabelle_System.mkdir o Path.explode) |
108 val mash_state_dir = mash_model_dir |
108 val mash_state_dir = mash_model_dir |
109 fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode |
109 fun mash_state_file () = mash_state_dir () ^ "/state" |
110 |
110 |
111 |
111 |
112 (*** Isabelle helpers ***) |
112 (*** Isabelle helpers ***) |
113 |
113 |
114 fun meta_char c = |
114 fun meta_char c = |
383 |
383 |
384 (*** Low-level communication with MaSh ***) |
384 (*** Low-level communication with MaSh ***) |
385 |
385 |
386 (* more friendly than "try o File.rm" for those who keep the files open in their |
386 (* more friendly than "try o File.rm" for those who keep the files open in their |
387 text editor *) |
387 text editor *) |
388 fun wipe_out file = File.write file "" |
388 fun wipe_out_file file = File.write (Path.explode file) "" |
389 |
389 |
390 fun write_file (xs, f) file = |
390 fun write_file heading (xs, f) file = |
391 let val path = Path.explode file in |
391 let val path = Path.explode file in |
392 wipe_out path; |
392 File.write path heading; |
393 xs |> chunk_list 500 |
393 xs |> chunk_list 500 |
394 |> List.app (File.append path o space_implode "" o map f) |
394 |> List.app (File.append path o space_implode "" o map f) |
395 end |
395 end |
396 |
396 |
397 fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = |
397 fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = |
409 (if save then " --saveModel" else "") |
409 (if save then " --saveModel" else "") |
410 val command = |
410 val command = |
411 mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^ |
411 mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^ |
412 " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file |
412 " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file |
413 in |
413 in |
414 write_file ([], K "") sugg_file; |
414 write_file "" ([], K "") sugg_file; |
415 write_file write_cmds cmd_file; |
415 write_file "" write_cmds cmd_file; |
416 trace_msg ctxt (fn () => "Running " ^ command); |
416 trace_msg ctxt (fn () => "Running " ^ command); |
417 Isabelle_System.bash command; |
417 Isabelle_System.bash command; |
418 read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these) |
418 read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these) |
419 |> tap (fn _ => trace_msg ctxt (fn () => |
419 |> tap (fn _ => trace_msg ctxt (fn () => |
420 case try File.read (Path.explode err_file) of |
420 case try File.read (Path.explode err_file) of |
421 NONE => "Done" |
421 NONE => "Done" |
422 | SOME "" => "Done" |
422 | SOME "" => "Done" |
423 | SOME s => "Error: " ^ elide_string 1000 s)) |
423 | SOME s => "Error: " ^ elide_string 1000 s)) |
424 |> not overlord |
424 |> not overlord |
425 ? tap (fn _ => List.app (wipe_out o Path.explode) |
425 ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file]) |
426 [err_file, sugg_file, cmd_file]) |
|
427 end |
426 end |
428 |
427 |
429 fun str_of_add (name, parents, feats, deps) = |
428 fun str_of_add (name, parents, feats, deps) = |
430 "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ |
429 "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ |
431 escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" |
430 escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" |
504 |
503 |
505 val version = "*** MaSh 0.0 ***" |
504 val version = "*** MaSh 0.0 ***" |
506 |
505 |
507 fun load _ (state as (true, _)) = state |
506 fun load _ (state as (true, _)) = state |
508 | load ctxt _ = |
507 | load ctxt _ = |
509 let val path = mash_state_path () in |
508 let val path = mash_state_file () |> Path.explode in |
510 (true, |
509 (true, |
511 case try File.read_lines path of |
510 case try File.read_lines path of |
512 SOME (version' :: node_lines) => |
511 SOME (version' :: node_lines) => |
513 let |
512 let |
514 fun add_edge_to name parent = |
513 fun add_edge_to name parent = |
529 | _ => empty_state) |
528 | _ => empty_state) |
530 end |
529 end |
531 |
530 |
532 fun save ctxt {fact_G} = |
531 fun save ctxt {fact_G} = |
533 let |
532 let |
534 val path = mash_state_path () |
533 fun str_of_entry (name, parents) = |
535 fun fact_line_for name parents = |
534 escape_meta name ^ ": " ^ escape_metas parents ^ "\n" |
536 escape_meta name ^ ": " ^ escape_metas parents |
535 fun append_entry (name, ((), (parents, _))) = |
537 val append_fact = File.append path o suffix "\n" oo fact_line_for |
536 cons (name, Graph.Keys.dest parents) |
538 fun append_entry (name, ((), (parents, _))) () = |
537 val entries = [] |> Graph.fold append_entry fact_G |
539 append_fact name (Graph.Keys.dest parents) |
|
540 in |
538 in |
541 File.write path (version ^ "\n"); |
539 write_file (version ^ "\n") (entries, str_of_entry) (mash_state_file ()); |
542 Graph.fold append_entry fact_G (); |
|
543 trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")") |
540 trace_msg ctxt (fn () => "Saved fact graph (" ^ graph_info fact_G ^ ")") |
544 end |
541 end |
545 |
542 |
546 val global_state = |
543 val global_state = |
547 Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) |
544 Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state) |
557 fun mash_get ctxt = |
554 fun mash_get ctxt = |
558 Synchronized.change_result global_state (load ctxt #> `snd) |
555 Synchronized.change_result global_state (load ctxt #> `snd) |
559 |
556 |
560 fun mash_unlearn ctxt = |
557 fun mash_unlearn ctxt = |
561 Synchronized.change global_state (fn _ => |
558 Synchronized.change global_state (fn _ => |
562 (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state))) |
559 (mash_CLEAR ctxt; |
|
560 wipe_out_file (mash_state_file ()); |
|
561 (true, empty_state))) |
563 |
562 |
564 end |
563 end |
565 |
564 |
566 fun mash_could_suggest_facts () = mash_home () <> "" |
565 fun mash_could_suggest_facts () = mash_home () <> "" |
567 fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) |
566 fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt))) |