automatically retry with full-types upon unsound proof
authorblanchet
Thu Apr 21 22:32:00 2011 +0200 (2011-04-21)
changeset 424502765d4fb2b9c
parent 42449 494e4ac5b0f8
child 42451 a75fcd103cbb
automatically retry with full-types upon unsound proof
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 21 22:18:28 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 21 22:32:00 2011 +0200
     1.3 @@ -96,7 +96,7 @@
     1.4    | string_for_failure ProofMissing =
     1.5      "The prover claims the conjecture is a theorem but did not provide a proof."
     1.6    | string_for_failure UnsoundProof =
     1.7 -    "The prover found a type-incorrect proof. (Or, very unlikely, your axioms \
     1.8 +    "The prover found a type-unsound proof. (Or, very unlikely, your axioms \
     1.9      \are inconsistent.)"
    1.10    | string_for_failure CantConnect = "Cannot connect to remote server."
    1.11    | string_for_failure TimedOut = "Timed out."
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:18:28 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:32:00 2011 +0200
     2.3 @@ -401,7 +401,8 @@
     2.4                  |> filter_out (curry (op =) ~1 o fst)
     2.5                  |> map (Untranslated_Fact o apfst (fst o nth facts))
     2.6                end
     2.7 -            fun run_slice (slice, (time_frac, (complete, default_max_relevant)))
     2.8 +            fun run_slice type_sys
     2.9 +                          (slice, (time_frac, (complete, default_max_relevant)))
    2.10                            time_left =
    2.11                let
    2.12                  val num_facts =
    2.13 @@ -479,16 +480,22 @@
    2.14                   (output, msecs, atp_proof, outcome))
    2.15                end
    2.16              val timer = Timer.startRealTimer ()
    2.17 -            fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) =
    2.18 -                run_slice slice (Time.- (timeout, Timer.checkRealTimer timer))
    2.19 +            fun maybe_run_slice type_sys slice (_, (_, msecs0, _, SOME _)) =
    2.20 +                run_slice type_sys slice
    2.21 +                          (Time.- (timeout, Timer.checkRealTimer timer))
    2.22                  |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
    2.23                         (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
    2.24                                  outcome)))
    2.25 -              | maybe_run_slice _ result = result
    2.26 +              | maybe_run_slice _ _ result = result
    2.27            in
    2.28              ((Symtab.empty, [], Vector.fromList []),
    2.29               ("", SOME 0, [], SOME InternalError))
    2.30 -            |> fold maybe_run_slice actual_slices
    2.31 +            |> fold (maybe_run_slice type_sys) actual_slices
    2.32 +               (* The ATP found an unsound proof? Automatically try again with
    2.33 +                  full types! *)
    2.34 +            |> (fn result as (_, (_, _, _, SOME UnsoundProof)) =>
    2.35 +                   result |> fold (maybe_run_slice (Tags true)) actual_slices
    2.36 +                 | result => result)
    2.37            end
    2.38          else
    2.39            error ("Bad executable: " ^ Path.print command ^ ".")