start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
authorblanchet
Thu Mar 31 11:16:54 2011 +0200 (2011-03-31)
changeset 42182a630978fc967
parent 42181 8f25605e646c
child 42183 173b0f488428
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:53 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 31 11:16:54 2011 +0200
     1.3 @@ -341,15 +341,20 @@
     1.4           : params)
     1.5          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
     1.6    let
     1.7 +    val thy = Proof.theory_of state
     1.8      val ctxt = Proof.context_of state
     1.9      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    1.10      fun monomorphize_facts facts =
    1.11        let
    1.12          val facts = facts |> map untranslated_fact
    1.13 +        (* pseudo-theorem involving the same constants as the subgoal *)
    1.14 +        val subgoal_th =
    1.15 +          Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
    1.16          val indexed_facts =
    1.17 -          (~1, goal) :: (0 upto length facts - 1 ~~ map snd facts)
    1.18 +          (~1, subgoal_th) :: (0 upto length facts - 1 ~~ map snd facts)
    1.19          val (mono_facts, ctxt') =
    1.20 -          ctxt |> Config.put SMT_Config.monomorph_limit monomorphize_limit
    1.21 +          ctxt |> Config.put SMT_Config.verbose debug
    1.22 +               |> Config.put SMT_Config.monomorph_limit monomorphize_limit
    1.23                 |> SMT_Monomorph.monomorph indexed_facts
    1.24        in
    1.25          mono_facts