1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 23:18:39 2010 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Dec 18 12:46:58 2010 +0100
1.3 @@ -11,7 +11,12 @@
1.4 type relevance_override = Sledgehammer_Filter.relevance_override
1.5 type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
1.6 type params = Sledgehammer_Provers.params
1.7 + type prover_problem = Sledgehammer_Provers.prover_problem
1.8 + type prover_result = Sledgehammer_Provers.prover_result
1.9
1.10 + val run_prover :
1.11 + params -> bool -> (string -> minimize_command) -> prover_problem -> string
1.12 + -> prover_result
1.13 val run_sledgehammer :
1.14 params -> bool -> int -> relevance_override -> (string -> minimize_command)
1.15 -> Proof.state -> bool * Proof.state
1.16 @@ -41,9 +46,50 @@
1.17
1.18 val implicit_minimization_threshold = 50
1.19
1.20 -fun run_prover (params as {debug, blocking, max_relevant, timeout, expect, ...})
1.21 - auto minimize_command only
1.22 - {state, goal, subgoal, subgoal_count, facts, smt_head} name =
1.23 +fun run_prover (params as {debug, verbose, ...}) auto minimize_command
1.24 + (problem as {state, subgoal, subgoal_count, facts, ...}) name =
1.25 + let val ctxt = Proof.context_of state in
1.26 + get_prover ctxt auto name params (minimize_command name) problem
1.27 + |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
1.28 + if is_some outcome then
1.29 + result
1.30 + else
1.31 + let
1.32 + val (used_facts, message) =
1.33 + if length used_facts >= implicit_minimization_threshold then
1.34 + minimize_facts params (not verbose) subgoal subgoal_count
1.35 + state
1.36 + (filter_used_facts used_facts
1.37 + (map (apsnd single o untranslated_fact) facts))
1.38 + |>> Option.map (map fst)
1.39 + else
1.40 + (SOME used_facts, message)
1.41 + in
1.42 + case used_facts of
1.43 + SOME used_facts =>
1.44 + (if debug andalso not (null used_facts) then
1.45 + facts ~~ (0 upto length facts - 1)
1.46 + |> map (fn (fact, j) =>
1.47 + fact |> untranslated_fact |> apsnd (K j))
1.48 + |> filter_used_facts used_facts
1.49 + |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
1.50 + |> commas
1.51 + |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^
1.52 + quote name ^ " proof (of " ^
1.53 + string_of_int (length facts) ^ "): ") "."
1.54 + |> Output.urgent_message
1.55 + else
1.56 + ();
1.57 + {outcome = NONE, used_facts = used_facts,
1.58 + run_time_in_msecs = run_time_in_msecs, message = message})
1.59 + | NONE => result
1.60 + end)
1.61 + end
1.62 +
1.63 +fun launch_prover
1.64 + (params as {debug, blocking, max_relevant, timeout, expect, ...})
1.65 + auto minimize_command only
1.66 + {state, goal, subgoal, subgoal_count, facts, smt_head} name =
1.67 let
1.68 val ctxt = Proof.context_of state
1.69 val birth_time = Time.now ()
1.70 @@ -53,41 +99,14 @@
1.71 val num_facts = length facts |> not only ? Integer.min max_relevant
1.72 val desc =
1.73 prover_description ctxt params name num_facts subgoal subgoal_count goal
1.74 - val prover = get_prover ctxt auto name
1.75 val problem =
1.76 {state = state, goal = goal, subgoal = subgoal,
1.77 subgoal_count = subgoal_count, facts = take num_facts facts,
1.78 smt_head = smt_head}
1.79 fun really_go () =
1.80 - prover params (minimize_command name) problem
1.81 - |> (fn {outcome, used_facts, message, ...} =>
1.82 - if is_some outcome then
1.83 - ("none", message)
1.84 - else
1.85 - let
1.86 - val (used_facts, message) =
1.87 - if length used_facts >= implicit_minimization_threshold then
1.88 - minimize_facts params true subgoal subgoal_count state
1.89 - (filter_used_facts used_facts
1.90 - (map (apsnd single o untranslated_fact) facts))
1.91 - |>> Option.map (map fst)
1.92 - else
1.93 - (SOME used_facts, message)
1.94 - val _ =
1.95 - case (debug, used_facts) of
1.96 - (true, SOME (used_facts as _ :: _)) =>
1.97 - facts ~~ (0 upto length facts - 1)
1.98 - |> map (fn (fact, j) =>
1.99 - fact |> untranslated_fact |> apsnd (K j))
1.100 - |> filter_used_facts used_facts
1.101 - |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
1.102 - |> commas
1.103 - |> enclose ("Fact" ^ plural_s num_facts ^ " in " ^
1.104 - quote name ^ " proof (of " ^
1.105 - string_of_int num_facts ^ "): ") "."
1.106 - |> Output.urgent_message
1.107 - | _ => ()
1.108 - in ("some", message) end)
1.109 + run_prover params auto minimize_command problem name
1.110 + |> (fn {outcome, message, ...} =>
1.111 + (if is_some outcome then "none" else "some" (* sic *), message))
1.112 fun go () =
1.113 let
1.114 val (outcome_code, message) =
1.115 @@ -171,7 +190,7 @@
1.116 | NONE => ()
1.117 val _ = if auto then () else Output.urgent_message "Sledgehammering..."
1.118 val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
1.119 - fun run_provers state get_facts translate maybe_smt_head provers =
1.120 + fun launch_provers state get_facts translate maybe_smt_head provers =
1.121 let
1.122 val facts = get_facts ()
1.123 val num_facts = length facts
1.124 @@ -182,16 +201,15 @@
1.125 facts = facts,
1.126 smt_head = maybe_smt_head
1.127 (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
1.128 - val run_prover = run_prover params auto minimize_command only
1.129 + val launch = launch_prover params auto minimize_command only
1.130 in
1.131 if auto then
1.132 fold (fn prover => fn (true, state) => (true, state)
1.133 - | (false, _) => run_prover problem prover)
1.134 + | (false, _) => launch problem prover)
1.135 provers (false, state)
1.136 else
1.137 provers
1.138 - |> (if blocking then smart_par_list_map else map)
1.139 - (run_prover problem)
1.140 + |> (if blocking then smart_par_list_map else map) (launch problem)
1.141 |> exists fst |> rpair state
1.142 end
1.143 fun get_facts label no_dangerous_types relevance_fudge provers =
1.144 @@ -222,15 +240,15 @@
1.145 else
1.146 ())
1.147 end
1.148 - fun run_atps (accum as (success, _)) =
1.149 + fun launch_atps (accum as (success, _)) =
1.150 if success orelse null atps then
1.151 accum
1.152 else
1.153 - run_provers state
1.154 + launch_provers state
1.155 (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
1.156 (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
1.157 (K (K NONE)) atps
1.158 - fun run_smts (accum as (success, _)) =
1.159 + fun launch_smts (accum as (success, _)) =
1.160 if success orelse null smts then
1.161 accum
1.162 else
1.163 @@ -242,17 +260,17 @@
1.164 in
1.165 smts |> map (`(class_of_smt_solver ctxt))
1.166 |> AList.group (op =)
1.167 - |> map (run_provers state (K facts) weight smt_head o snd)
1.168 + |> map (launch_provers state (K facts) weight smt_head o snd)
1.169 |> exists fst |> rpair state
1.170 end
1.171 - fun run_atps_and_smt_solvers () =
1.172 - [run_atps, run_smts]
1.173 + fun launch_atps_and_smt_solvers () =
1.174 + [launch_atps, launch_smts]
1.175 |> smart_par_list_map (fn f => f (false, state) |> K ())
1.176 handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
1.177 in
1.178 (false, state)
1.179 - |> (if blocking then run_atps #> not auto ? run_smts
1.180 - else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
1.181 + |> (if blocking then launch_atps #> not auto ? launch_smts
1.182 + else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
1.183 end
1.184
1.185 end;