src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 50867 48836c35d636
parent 50669 84c7cf36b2e0
child 50868 4b30d461b3a6
equal deleted inserted replaced
50866:e12ebcb859a7 50867:48836c35d636
   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