475 hyp_ts concl_t |
475 hyp_ts concl_t |
476 |> filter (is_appropriate_prop o prop_of o snd) |
476 |> filter (is_appropriate_prop o prop_of o snd) |
477 |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name |
477 |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name |
478 (the_default default_max_facts max_facts) |
478 (the_default default_max_facts max_facts) |
479 Sledgehammer_Fact.no_fact_override hyp_ts concl_t |
479 Sledgehammer_Fact.no_fact_override hyp_ts concl_t |
|
480 |> map (apfst (apfst (fn name => name ()))) |
|
481 |> tap (fn facts => |
|
482 (if null facts then |
|
483 "Found no relevant facts." |
|
484 else |
|
485 "Including " ^ string_of_int (length facts) ^ |
|
486 " relevant fact(s):\n" ^ |
|
487 (facts |> map (fst o fst) |> space_implode " ") ^ ".") |
|
488 |> Output.urgent_message) |
480 val prover = get_prover ctxt prover_name params goal facts |
489 val prover = get_prover ctxt prover_name params goal facts |
481 val problem = |
490 val problem = |
482 {state = st', goal = goal, subgoal = i, |
491 {state = st', goal = goal, subgoal = i, |
483 subgoal_count = Sledgehammer_Util.subgoal_count st, |
492 subgoal_count = Sledgehammer_Util.subgoal_count st, |
484 facts = facts |> map (apfst (apfst (fn name => name ()))) |
493 facts = facts |> map Sledgehammer_Provers.Untranslated_Fact} |
485 |> map Sledgehammer_Provers.Untranslated_Fact} |
|
486 in prover params (K (K (K ""))) problem end)) () |
494 in prover params (K (K (K ""))) problem end)) () |
487 handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut |
495 handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut |
488 | Fail "inappropriate" => failed ATP_Proof.Inappropriate |
496 | Fail "inappropriate" => failed ATP_Proof.Inappropriate |
489 val time_prover = run_time |> Time.toMilliseconds |
497 val time_prover = run_time |> Time.toMilliseconds |
490 val msg = message (Lazy.force preplay) ^ message_tail |
498 val msg = message (Lazy.force preplay) ^ message_tail |