allow diagnostic proof commands with skip_proofs;
authorwenzelm
Wed Apr 22 20:14:43 2015 +0200 (2015-04-22 ago)
changeset 60190906de96ba68a
parent 60189 0d3a62127057
child 60191 46a353f6aa39
allow diagnostic proof commands with skip_proofs;
src/HOL/Library/refute.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/try0.ML
src/Pure/Isar/toplevel.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/src/HOL/Library/refute.ML	Wed Apr 22 19:48:32 2015 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Wed Apr 22 20:14:43 2015 +0200
     1.3 @@ -2969,7 +2969,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.keep (fn state =>
     1.8 +        Toplevel.keep_proof (fn state =>
     1.9            let
    1.10              val ctxt = Toplevel.context_of state;
    1.11              val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Apr 22 19:48:32 2015 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Apr 22 20:14:43 2015 +0200
     2.3 @@ -377,7 +377,7 @@
     2.4    Outer_Syntax.command @{command_keyword nitpick}
     2.5      "try to find a counterexample for a given subgoal using Nitpick"
     2.6      (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
     2.7 -      Toplevel.keep (fn state =>
     2.8 +      Toplevel.keep_proof (fn state =>
     2.9          ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
    2.10            (Toplevel.proof_of state)))))
    2.11  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 22 19:48:32 2015 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Apr 22 20:14:43 2015 +0200
     3.3 @@ -359,7 +359,7 @@
     3.4    end
     3.5  
     3.6  fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
     3.7 -  Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
     3.8 +  Toplevel.keep_proof (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
     3.9  
    3.10  fun string_of_raw_param (key, values) =
    3.11    key ^ (case implode_param values of "" => "" | value => " = " ^ value)
     4.1 --- a/src/HOL/Tools/try0.ML	Wed Apr 22 19:48:32 2015 +0200
     4.2 +++ b/src/HOL/Tools/try0.ML	Wed Apr 22 20:14:43 2015 +0200
     4.3 @@ -154,7 +154,8 @@
     4.4  fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
     4.5  
     4.6  fun try0_trans quad =
     4.7 -  Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
     4.8 +  Toplevel.keep_proof
     4.9 +    (ignore o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
    4.10  
    4.11  fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
    4.12  
     5.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 22 19:48:32 2015 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 22 20:14:43 2015 +0200
     5.3 @@ -40,6 +40,7 @@
     5.4    val exit: transition -> transition
     5.5    val keep: (state -> unit) -> transition -> transition
     5.6    val keep': (bool -> state -> unit) -> transition -> transition
     5.7 +  val keep_proof: (state -> unit) -> transition -> transition
     5.8    val ignored: Position.T -> transition
     5.9    val is_ignored: transition -> bool
    5.10    val malformed: Position.T -> string -> transition
    5.11 @@ -345,6 +346,12 @@
    5.12  
    5.13  fun keep f = add_trans (Keep (fn _ => f));
    5.14  
    5.15 +fun keep_proof f =
    5.16 +  keep (fn st =>
    5.17 +    if is_proof st then f st
    5.18 +    else if is_skipped_proof st then ()
    5.19 +    else warning "No proof state");
    5.20 +
    5.21  fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ());
    5.22  fun is_ignored tr = name_of tr = "<ignored>";
    5.23  
     6.1 --- a/src/Tools/quickcheck.ML	Wed Apr 22 19:48:32 2015 +0200
     6.2 +++ b/src/Tools/quickcheck.ML	Wed Apr 22 20:14:43 2015 +0200
     6.3 @@ -510,8 +510,8 @@
     6.4  fun quickcheck args i state =
     6.5    Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state));
     6.6  
     6.7 -fun quickcheck_cmd args i state =
     6.8 -  gen_quickcheck args i (Toplevel.proof_of state)
     6.9 +fun quickcheck_cmd args i st =
    6.10 +  gen_quickcheck args i (Toplevel.proof_of st)
    6.11    |> apfst (Option.map (the o get_first response_of))
    6.12    |> (fn (r, state) =>
    6.13        writeln (Pretty.string_of
    6.14 @@ -534,7 +534,7 @@
    6.15    Outer_Syntax.command @{command_keyword quickcheck}
    6.16      "try to find counterexample for subgoal"
    6.17      (parse_args -- Scan.optional Parse.nat 1 >>
    6.18 -      (fn (args, i) => Toplevel.keep (quickcheck_cmd args i)));
    6.19 +      (fn (args, i) => Toplevel.keep_proof (quickcheck_cmd args i)));
    6.20  
    6.21  
    6.22  (* automatic testing *)
     7.1 --- a/src/Tools/solve_direct.ML	Wed Apr 22 19:48:32 2015 +0200
     7.2 +++ b/src/Tools/solve_direct.ML	Wed Apr 22 20:14:43 2015 +0200
     7.3 @@ -94,7 +94,7 @@
     7.4  val _ =
     7.5    Outer_Syntax.command @{command_keyword solve_direct}
     7.6      "try to solve conjectures directly with existing theorems"
     7.7 -    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
     7.8 +    (Scan.succeed (Toplevel.keep_proof (ignore o solve_direct o Toplevel.proof_of)));
     7.9  
    7.10  
    7.11  (* hook *)
     8.1 --- a/src/Tools/try.ML	Wed Apr 22 19:48:32 2015 +0200
     8.2 +++ b/src/Tools/try.ML	Wed Apr 22 20:14:43 2015 +0200
     8.3 @@ -77,7 +77,7 @@
     8.4  val _ =
     8.5    Outer_Syntax.command @{command_keyword try}
     8.6      "try a combination of automatic proving and disproving tools"
     8.7 -    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
     8.8 +    (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)))
     8.9  
    8.10  
    8.11  (* automatic try (TTY) *)