src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 42450 2765d4fb2b9c
parent 42449 494e4ac5b0f8
child 42451 a75fcd103cbb
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:18:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:32:00 2011 +0200
     1.3 @@ -401,7 +401,8 @@
     1.4                  |> filter_out (curry (op =) ~1 o fst)
     1.5                  |> map (Untranslated_Fact o apfst (fst o nth facts))
     1.6                end
     1.7 -            fun run_slice (slice, (time_frac, (complete, default_max_relevant)))
     1.8 +            fun run_slice type_sys
     1.9 +                          (slice, (time_frac, (complete, default_max_relevant)))
    1.10                            time_left =
    1.11                let
    1.12                  val num_facts =
    1.13 @@ -479,16 +480,22 @@
    1.14                   (output, msecs, atp_proof, outcome))
    1.15                end
    1.16              val timer = Timer.startRealTimer ()
    1.17 -            fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) =
    1.18 -                run_slice slice (Time.- (timeout, Timer.checkRealTimer timer))
    1.19 +            fun maybe_run_slice type_sys slice (_, (_, msecs0, _, SOME _)) =
    1.20 +                run_slice type_sys slice
    1.21 +                          (Time.- (timeout, Timer.checkRealTimer timer))
    1.22                  |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    1.23                         (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
    1.24                                  outcome)))
    1.25 -              | maybe_run_slice _ result = result
    1.26 +              | maybe_run_slice _ _ result = result
    1.27            in
    1.28              ((Symtab.empty, [], Vector.fromList []),
    1.29               ("", SOME 0, [], SOME InternalError))
    1.30 -            |> fold maybe_run_slice actual_slices
    1.31 +            |> fold (maybe_run_slice type_sys) actual_slices
    1.32 +               (* The ATP found an unsound proof? Automatically try again with
    1.33 +                  full types! *)
    1.34 +            |> (fn result as (_, (_, _, _, SOME UnsoundProof)) =>
    1.35 +                   result |> fold (maybe_run_slice (Tags true)) actual_slices
    1.36 +                 | result => result)
    1.37            end
    1.38          else
    1.39            error ("Bad executable: " ^ Path.print command ^ ".")