# HG changeset patch # User blanchet # Date 1292672818 -3600 # Node ID 095ecb0c687f5b781bd2a35d9ad19d9d57ed50e2 # Parent ffae1d9bad06e9e4f384afd2cb7bafac892be4a2 factored out running a prover with (optionally) an implicit minimizer phrase diff -r ffae1d9bad06 -r 095ecb0c687f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 23:18:39 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 18 12:46:58 2010 +0100 @@ -11,7 +11,12 @@ type relevance_override = Sledgehammer_Filter.relevance_override type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command type params = Sledgehammer_Provers.params + type prover_problem = Sledgehammer_Provers.prover_problem + type prover_result = Sledgehammer_Provers.prover_result + val run_prover : + params -> bool -> (string -> minimize_command) -> prover_problem -> string + -> prover_result val run_sledgehammer : params -> bool -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> bool * Proof.state @@ -41,9 +46,50 @@ val implicit_minimization_threshold = 50 -fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...}) - auto minimize_command only - {state, goal, subgoal, subgoal_count, facts, smt_head} name = +fun run_prover (params as {debug, verbose, ...}) auto minimize_command + (problem as {state, subgoal, subgoal_count, facts, ...}) name = + let val ctxt = Proof.context_of state in + get_prover ctxt auto name params (minimize_command name) problem + |> (fn result as {outcome, used_facts, run_time_in_msecs, message} => + if is_some outcome then + result + else + let + val (used_facts, message) = + if length used_facts >= implicit_minimization_threshold then + minimize_facts params (not verbose) subgoal subgoal_count + state + (filter_used_facts used_facts + (map (apsnd single o untranslated_fact) facts)) + |>> Option.map (map fst) + else + (SOME used_facts, message) + in + case used_facts of + SOME used_facts => + (if debug andalso not (null used_facts) then + facts ~~ (0 upto length facts - 1) + |> map (fn (fact, j) => + fact |> untranslated_fact |> apsnd (K j)) + |> filter_used_facts used_facts + |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) + |> commas + |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ + quote name ^ " proof (of " ^ + string_of_int (length facts) ^ "): ") "." + |> Output.urgent_message + else + (); + {outcome = NONE, used_facts = used_facts, + run_time_in_msecs = run_time_in_msecs, message = message}) + | NONE => result + end) + end + +fun launch_prover + (params as {debug, blocking, max_relevant, timeout, expect, ...}) + auto minimize_command only + {state, goal, subgoal, subgoal_count, facts, smt_head} name = let val ctxt = Proof.context_of state val birth_time = Time.now () @@ -53,41 +99,14 @@ val num_facts = length facts |> not only ? Integer.min max_relevant val desc = prover_description ctxt params name num_facts subgoal subgoal_count goal - val prover = get_prover ctxt auto name val problem = {state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, facts = take num_facts facts, smt_head = smt_head} fun really_go () = - prover params (minimize_command name) problem - |> (fn {outcome, used_facts, message, ...} => - if is_some outcome then - ("none", message) - else - let - val (used_facts, message) = - if length used_facts >= implicit_minimization_threshold then - minimize_facts params true subgoal subgoal_count state - (filter_used_facts used_facts - (map (apsnd single o untranslated_fact) facts)) - |>> Option.map (map fst) - else - (SOME used_facts, message) - val _ = - case (debug, used_facts) of - (true, SOME (used_facts as _ :: _)) => - facts ~~ (0 upto length facts - 1) - |> map (fn (fact, j) => - fact |> untranslated_fact |> apsnd (K j)) - |> filter_used_facts used_facts - |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) - |> commas - |> enclose ("Fact" ^ plural_s num_facts ^ " in " ^ - quote name ^ " proof (of " ^ - string_of_int num_facts ^ "): ") "." - |> Output.urgent_message - | _ => () - in ("some", message) end) + run_prover params auto minimize_command problem name + |> (fn {outcome, message, ...} => + (if is_some outcome then "none" else "some" (* sic *), message)) fun go () = let val (outcome_code, message) = @@ -171,7 +190,7 @@ | NONE => () val _ = if auto then () else Output.urgent_message "Sledgehammering..." val (smts, atps) = provers |> List.partition (is_smt_prover ctxt) - fun run_provers state get_facts translate maybe_smt_head provers = + fun launch_provers state get_facts translate maybe_smt_head provers = let val facts = get_facts () val num_facts = length facts @@ -182,16 +201,15 @@ facts = facts, smt_head = maybe_smt_head (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} - val run_prover = run_prover params auto minimize_command only + val launch = launch_prover params auto minimize_command only in if auto then fold (fn prover => fn (true, state) => (true, state) - | (false, _) => run_prover problem prover) + | (false, _) => launch problem prover) provers (false, state) else provers - |> (if blocking then smart_par_list_map else map) - (run_prover problem) + |> (if blocking then smart_par_list_map else map) (launch problem) |> exists fst |> rpair state end fun get_facts label no_dangerous_types relevance_fudge provers = @@ -222,15 +240,15 @@ else ()) end - fun run_atps (accum as (success, _)) = + fun launch_atps (accum as (success, _)) = if success orelse null atps then accum else - run_provers state + launch_provers state (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps) (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst)) (K (K NONE)) atps - fun run_smts (accum as (success, _)) = + fun launch_smts (accum as (success, _)) = if success orelse null smts then accum else @@ -242,17 +260,17 @@ in smts |> map (`(class_of_smt_solver ctxt)) |> AList.group (op =) - |> map (run_provers state (K facts) weight smt_head o snd) + |> map (launch_provers state (K facts) weight smt_head o snd) |> exists fst |> rpair state end - fun run_atps_and_smt_solvers () = - [run_atps, run_smts] + fun launch_atps_and_smt_solvers () = + [launch_atps, launch_smts] |> smart_par_list_map (fn f => f (false, state) |> K ()) handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg) in (false, state) - |> (if blocking then run_atps #> not auto ? run_smts - else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p)) + |> (if blocking then launch_atps #> not auto ? launch_smts + else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p)) end end;