File ‹Subtool.ML›
signature SUBTOOL =
sig
val state_stttac : Proof.state Dynamic_Utils.stttac;
end;
signature SUBTOOLS =
sig
val quickcheck : Proof.state Dynamic_Utils.stttac;
val nitpick : Proof.state Dynamic_Utils.stttac;
val hammer : Proof.state Dynamic_Utils.stttac;
val is_solved : Proof.state Dynamic_Utils.stttac;
val defer : Proof.state Dynamic_Utils.stttac;
val subgoal : Proof.state Dynamic_Utils.stttac;
end;
structure Subtools =
struct
structure Quickcheck_Tactic : SUBTOOL =
struct
fun nontac (state:Proof.state) =
let
val do_trace = false;
fun show_trace text = if do_trace then tracing text else ();
val quickcheck = Quickcheck.quickcheck;
val single = Seq.single state;
fun trace_no_cexm _ = show_trace "Quickcheck.quickcheck found no counterexample";
fun trace_cexm _ = show_trace "Quickcheck.quickcheck found a counterexample";
fun trace_scexn _ = show_trace ("Quickcheck.quickcheck found a potentially spurious " ^
"counterexample due to underspecified functions");
fun get_result _ = (case quickcheck [] 1 state of
NONE => (trace_no_cexm (); single)
| SOME (genuine, _) => if genuine then (trace_cexm (); Seq.empty) else (trace_scexn (); single));
in
Utils.try_with single get_result state
end;
val state_stttac = Dynamic_Utils.log_n_nontac_to_stttac ([], nontac);
end;
structure Nitpick_Tactic : SUBTOOL =
struct
fun nontac (state:Proof.state) =
let
val single = Seq.single state;
val thy:theory = (Proof.theory_of state);
val params = Nitpick_Commands.default_params thy [];
val nitpick_result = Nitpick.pick_nits_in_subgoal state params Nitpick.Normal 1 1;
val nitpick_succeed = fst nitpick_result = "genuine";
val nitpick_tac_result = if nitpick_succeed then Seq.empty else single
in
nitpick_tac_result : Proof.state Seq.seq
end;
val state_stttac = Dynamic_Utils.log_n_nontac_to_stttac ([], nontac);
end;
structure Sledgehammer_Tacctic : SUBTOOL =
struct
local
type text = Method.text;
type text_range = Method.text_range;
type ctxt = Proof.context;
type T = Token.T;
type ref = Facts.ref;
type srcs = Token.src list;
type keywords = Keyword.keywords;
fun sh_output_to_sh_logtac (sh_output:string) (state:Proof.state) =
let
val thy = Proof.theory_of state : theory;
val ctxt = Proof.context_of state : ctxt;
val keywords = Thy_Header.get_keywords thy : keywords;
val op_w_stopper = sh_output ^ " parserStopsWithMe";
val tokens = Token.explode keywords Position.none op_w_stopper
|> filter_out (fn token:T => Token.is_kind Token.Space token) : T list;
val is_using = String.isPrefix "using " sh_output;
val parse_using = Parse.and_list1 Parse.thms1 : (ref * srcs) list list Token.parser;
val parse_method = Method.parse : text_range Token.parser;
val parse_one = Scan.one (K true) : T list -> T * T list;
val parser = if is_using
then (parse_one |-- parse_using) -- (parse_one |-- parse_method)
else (parse_one |-- parse_method) >> (fn x => ([], x));
val p_get_meth = (parse_one |-- parse_using) -- parse_one
: T list -> ((ref * srcs) list list * T) * T list;
fun get_str tkns = tkns
|> Utils.init
|> map Token.unparse |> String.concatWith " " : string;
val methN:string = if is_using
then p_get_meth tokens |> snd |> get_str
else parse_one tokens |> snd |> get_str;
val result = parser tokens
: ((ref * srcs) list list * text_range) * T list;
val using_raw = (#1 o #1) result : (ref * srcs) list list;
val text_range = (#2 o #1) result : text_range;
val check_text = Method.check_text ctxt;
val fail_trange = (Method.Basic (K Method.fail), Position.no_range) : Method.text_range;
val checked_range = (apfst check_text text_range handle ERROR _ => fail_trange) : text_range;
val using_strings = using_raw |> List.concat |> map (Facts.string_of_ref o #1) handle Empty =>
(if Utils.debug
then tracing "using_strings in sh_output_to_sh_logtac failed." else ();
["Failed constructing using_strings."])
: string list;
val node : Dynamic_Utils.node = Dynamic_Utils.Apply {using = using_strings, methN = methN, back = 0};
val _ =
let
val app = case node of
Dynamic_Utils.Apply app_node => app_node
| _ => error "app in Sledgehammer_Tactic panics.";
fun tracing1 _ = tracing ("methN in node is " ^ #methN app);
fun tracing2 _ = tracing "using_strings are ...";
fun tracing3 _ = map tracing using_strings;
in
if Utils.debug then (tracing1 (); tracing2 (); tracing3 (); ()) else ()
end;
val _ = Basics.try;
val state_w_using = Proof.using_cmd using_raw state : Proof.state;
val timeout = Timeout.apply (seconds 60.0)
val tac_results = timeout (Proof.apply checked_range) state_w_using
|> Seq.filter_results
|> Utils.try_with Seq.empty (Seq.try Seq.hd): Proof.state Seq.seq;
val results_w_log = Seq.map (fn x => ([node], x)) tac_results : (Dynamic_Utils.log * Proof.state) Seq.seq;
in
results_w_log : (Dynamic_Utils.log * Proof.state) Seq.seq
end;
fun hammer_logtac (pstate:Proof.state) =
let
infix <$>
fun x <$> f = Option.map f x;
val valOf = Option.valOf;
val omap = Option.map;
val thy = Proof.theory_of pstate : theory;
val params = Sledgehammer_Commands.default_params thy
[("isar_proofs", "false"),("smt_proofs", "false")]
val Auto_Try = Sledgehammer_Prover.Auto_Try;
val fact_override = Sledgehammer_Fact.no_fact_override;
val run_sledgehammer = (fn state =>
let
val string_of_outcome =
Sledgehammer.short_string_of_sledgehammer_outcome
in
Sledgehammer.run_sledgehammer params Auto_Try NONE 1 fact_override
state
|> apsnd (ATP_Util.map_prod string_of_outcome single)
end)
: Proof.state -> bool * (string * string list);
val result = SOME (run_sledgehammer pstate)
handle ERROR _ =>
(if Utils.debug then tracing "ERROR in result/hammer_logtac" else ();
NONE)
: (bool * (string * string list)) option;
val orig_string = result <$> snd <$> snd <$> hd handle Empty =>
(if Utils.debug then tracing "Empty in orig_string/hammer_logtac" else ();
NONE) : string option;
fun did_smt_timeout (out::timed::_) = (Utils.are_same ("out)", out)) andalso
(Utils.are_same ("timed", timed))
| did_smt_timeout _ = error "Something went wrong in Subtool.ML";
val one_line_apply = orig_string <$> space_explode " "
<$> drop 2
<$> rev <$> (fn tokens =>
if did_smt_timeout tokens then drop 5 tokens else drop 2 tokens)
<$> rev
<$> String.concatWith " " : string option;
val apply_script_cntnt = omap YXML.content_of one_line_apply : string option;
val sh_returned = if is_some apply_script_cntnt
then valOf result |> fst else false : bool;
in
if sh_returned
then
sh_output_to_sh_logtac (valOf apply_script_cntnt) pstate
else Seq.empty : (Dynamic_Utils.log * Proof.state) Seq.seq
end;
in
val state_stttac = Dynamic_Utils.logtac_to_stttac hammer_logtac : Proof.state Dynamic_Utils.stttac;
end;
end;
val quickcheck = Quickcheck_Tactic.state_stttac;
val nitpick = Nitpick_Tactic.state_stttac;
val hammer = Sledgehammer_Tacctic.state_stttac;
val to_stttac = Dynamic_Utils.log_n_nontac_to_stttac;
fun is_solved_nontac(state:Proof.state) =
let
val done = Proof.local_done_proof;
val goal = state |> Proof.goal |> #goal : thm;
val no_goal = Thm.nprems_of goal = 0 : bool;
val result = if no_goal then state |> done |> Seq.single
handle ERROR _ => Seq.single state else Seq.empty;
in
result : Proof.state Seq.seq
end;
val is_solved = to_stttac ([Dynamic_Utils.Done], is_solved_nontac);
val defer = to_stttac ([Dynamic_Utils.Defer], Seq.single o (Proof.defer 1));
val subgoal_nontac = Seq.single o #2 o Subgoal.subgoal (Binding.empty, []) NONE (false, []);
val subgoal = to_stttac ([Dynamic_Utils.Subgoal], subgoal_nontac);
end;