more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
authorwenzelm
Wed Mar 27 17:58:07 2013 +0100 (2013-03-27)
changeset 515574e4b56b7a3a5
parent 51556 7ada6dfa9ab5
child 51558 91f8bed6d0a4
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
src/HOL/Library/refute.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/try0.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/Library/refute.ML	Wed Mar 27 17:55:21 2013 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Wed Mar 27 17:58:07 2013 +0100
     1.3 @@ -3202,6 +3202,7 @@
     1.4      "try to find a model that refutes a given subgoal"
     1.5      (scan_parms -- Scan.optional Parse.nat 1 >>
     1.6        (fn (parms, i) =>
     1.7 +        Toplevel.unknown_proof o
     1.8          Toplevel.keep (fn state =>
     1.9            let
    1.10              val ctxt = Toplevel.context_of state;
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Mar 27 17:55:21 2013 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Mar 27 17:58:07 2013 +0100
     2.3 @@ -368,11 +368,6 @@
     2.4    in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
     2.5    |> `(fn (outcome_code, _) => outcome_code = genuineN)
     2.6  
     2.7 -fun nitpick_trans (params, i) =
     2.8 -  Toplevel.keep (fn state =>
     2.9 -      pick_nits params Normal i (Toplevel.proof_position_of state)
    2.10 -                (Toplevel.proof_of state) |> K ())
    2.11 -
    2.12  fun string_for_raw_param (name, value) =
    2.13    name ^ " = " ^ stringify_raw_param_value value
    2.14  
    2.15 @@ -391,7 +386,11 @@
    2.16  val _ =
    2.17    Outer_Syntax.improper_command @{command_spec "nitpick"}
    2.18      "try to find a counterexample for a given subgoal using Nitpick"
    2.19 -    ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans)
    2.20 +    (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
    2.21 +      Toplevel.unknown_proof o
    2.22 +      Toplevel.keep (fn state =>
    2.23 +        ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
    2.24 +          (Toplevel.proof_of state)))))
    2.25  
    2.26  val _ =
    2.27    Outer_Syntax.command @{command_spec "nitpick_params"}
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 27 17:55:21 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 27 17:58:07 2013 +0100
     3.3 @@ -419,6 +419,7 @@
     3.4    end
     3.5  
     3.6  fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
     3.7 +  Toplevel.unknown_proof o
     3.8    Toplevel.keep (hammer_away params subcommand opt_i fact_override
     3.9                   o Toplevel.proof_of)
    3.10  
     4.1 --- a/src/HOL/Tools/try0.ML	Wed Mar 27 17:55:21 2013 +0100
     4.2 +++ b/src/HOL/Tools/try0.ML	Wed Mar 27 17:58:07 2013 +0100
     4.3 @@ -156,6 +156,7 @@
     4.4  fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt
     4.5  
     4.6  fun try0_trans quad =
     4.7 +  Toplevel.unknown_proof o
     4.8    Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad
     4.9                   o Toplevel.proof_of)
    4.10  
     5.1 --- a/src/Tools/quickcheck.ML	Wed Mar 27 17:55:21 2013 +0100
     5.2 +++ b/src/Tools/quickcheck.ML	Wed Mar 27 17:58:07 2013 +0100
     5.3 @@ -532,8 +532,8 @@
     5.4  val _ =
     5.5    Outer_Syntax.improper_command @{command_spec "quickcheck"}
     5.6      "try to find counterexample for subgoal"
     5.7 -    (parse_args -- Scan.optional Parse.nat 1
     5.8 -      >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
     5.9 +    (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
    5.10 +      Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
    5.11  
    5.12  
    5.13  (* automatic testing *)
     6.1 --- a/src/Tools/solve_direct.ML	Wed Mar 27 17:55:21 2013 +0100
     6.2 +++ b/src/Tools/solve_direct.ML	Wed Mar 27 17:58:07 2013 +0100
     6.3 @@ -109,7 +109,8 @@
     6.4  val _ =
     6.5    Outer_Syntax.improper_command @{command_spec "solve_direct"}
     6.6      "try to solve conjectures directly with existing theorems"
     6.7 -    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
     6.8 +    (Scan.succeed (Toplevel.unknown_proof o
     6.9 +      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
    6.10  
    6.11  
    6.12  (* hook *)
     7.1 --- a/src/Tools/try.ML	Wed Mar 27 17:55:21 2013 +0100
     7.2 +++ b/src/Tools/try.ML	Wed Mar 27 17:58:07 2013 +0100
     7.3 @@ -90,7 +90,7 @@
     7.4  val _ =
     7.5    Outer_Syntax.improper_command @{command_spec "try"}
     7.6      "try a combination of automatic proving and disproving tools"
     7.7 -    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
     7.8 +    (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
     7.9  
    7.10  
    7.11  (* automatic try *)