src/Tools/try.ML
author wenzelm
Fri Mar 16 18:20:12 2012 +0100 (2012-03-16)
changeset 46961 5c6955f487e5
parent 43061 8096eec997a9
child 51557 4e4b56b7a3a5
permissions -rw-r--r--
outer syntax command definitions based on formal command_spec derived from theory header declarations;
blanchet@43018
     1
(*  Title:      Tools/try.ML
blanchet@33561
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@33561
     3
blanchet@43018
     4
Manager for tools that should be tried on conjectures.
blanchet@33561
     5
*)
blanchet@33561
     6
blanchet@43018
     7
signature TRY =
blanchet@33561
     8
sig
blanchet@43020
     9
  type tool =
blanchet@43024
    10
    string * (int * bool Unsynchronized.ref
blanchet@43020
    11
              * (bool -> Proof.state -> bool * (string * Proof.state)))
blanchet@43020
    12
blanchet@43020
    13
  val tryN : string
blanchet@43018
    14
  val auto_time_limit: real Unsynchronized.ref
blanchet@33561
    15
blanchet@43028
    16
  val serial_commas : string -> string list -> string list
blanchet@43028
    17
  val subgoal_count : Proof.state -> int
blanchet@43020
    18
  val register_tool : tool -> theory -> theory
blanchet@43020
    19
  val get_tools : theory -> tool list
blanchet@43020
    20
  val try_tools : Proof.state -> (string * string) option
blanchet@33561
    21
end;
blanchet@33561
    22
blanchet@43018
    23
structure Try : TRY =
blanchet@33561
    24
struct
blanchet@33561
    25
blanchet@43020
    26
type tool =
blanchet@43024
    27
  string * (int * bool Unsynchronized.ref
blanchet@43020
    28
            * (bool -> Proof.state -> bool * (string * Proof.state)))
blanchet@43020
    29
blanchet@43020
    30
val tryN = "try"
blanchet@43020
    31
blanchet@43020
    32
blanchet@33561
    33
(* preferences *)
blanchet@33561
    34
blanchet@43018
    35
val auto_time_limit = Unsynchronized.ref 4.0
blanchet@33561
    36
blanchet@43018
    37
val auto_try_time_limitN = "auto-try-time-limit"
blanchet@33561
    38
val _ =
blanchet@33561
    39
  ProofGeneralPgip.add_preference Preferences.category_tracing
blanchet@43018
    40
    (Preferences.real_pref auto_time_limit
blanchet@43018
    41
      auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")
blanchet@33561
    42
blanchet@33561
    43
blanchet@43028
    44
(* helpers *)
blanchet@43028
    45
blanchet@43028
    46
fun serial_commas _ [] = ["??"]
blanchet@43028
    47
  | serial_commas _ [s] = [s]
blanchet@43028
    48
  | serial_commas conj [s1, s2] = [s1, conj, s2]
blanchet@43028
    49
  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
blanchet@43028
    50
  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
blanchet@43028
    51
blanchet@43028
    52
val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
blanchet@43028
    53
blanchet@43028
    54
blanchet@33561
    55
(* configuration *)
blanchet@33561
    56
blanchet@43061
    57
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
blanchet@43061
    58
  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
blanchet@43028
    59
wenzelm@33600
    60
structure Data = Theory_Data
wenzelm@33600
    61
(
blanchet@43020
    62
  type T = tool list
blanchet@33561
    63
  val empty = []
blanchet@33561
    64
  val extend = I
blanchet@43028
    65
  fun merge data : T = Ord_List.merge tool_ord data
blanchet@33561
    66
)
blanchet@33561
    67
blanchet@43020
    68
val get_tools = Data.get
blanchet@43020
    69
blanchet@43028
    70
val register_tool = Data.map o Ord_List.insert tool_ord
blanchet@33561
    71
blanchet@43020
    72
(* try command *)
blanchet@43020
    73
blanchet@43020
    74
fun try_tools state =
blanchet@43028
    75
  if subgoal_count state = 0 then
blanchet@43028
    76
    (Output.urgent_message "No subgoal!"; NONE)
blanchet@43028
    77
  else
blanchet@43028
    78
    get_tools (Proof.theory_of state)
blanchet@43028
    79
    |> tap (fn tools =>
blanchet@43028
    80
               "Trying " ^ space_implode " "
blanchet@43028
    81
                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
blanchet@43028
    82
               |> Output.urgent_message)
blanchet@43028
    83
    |> Par_List.get_some
blanchet@43028
    84
           (fn (name, (_, _, tool)) =>
blanchet@43028
    85
               case try (tool false) state of
blanchet@43028
    86
                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
blanchet@43028
    87
               | _ => NONE)
blanchet@43028
    88
    |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
blanchet@43020
    89
blanchet@43020
    90
val _ =
wenzelm@46961
    91
  Outer_Syntax.improper_command @{command_spec "try"}
wenzelm@46961
    92
    "try a combination of automatic proving and disproving tools"
wenzelm@46961
    93
    (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
blanchet@43020
    94
blanchet@33561
    95
blanchet@43020
    96
(* automatic try *)
blanchet@33561
    97
blanchet@43020
    98
fun auto_try state =
blanchet@43020
    99
  get_tools (Proof.theory_of state)
blanchet@43024
   100
  |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
blanchet@43020
   101
  |> Par_List.get_some (fn tool =>
blanchet@43020
   102
                           case try (tool true) state of
blanchet@43020
   103
                             SOME (true, (_, state)) => SOME state
blanchet@43020
   104
                           | _ => NONE)
blanchet@43020
   105
  |> the_default state
blanchet@40931
   106
blanchet@40931
   107
(* Too large values are understood as milliseconds, ensuring compatibility with
blanchet@40931
   108
   old setting files. No users can possibly in their right mind want the user
blanchet@40931
   109
   interface to block for more than 100 seconds. *)
blanchet@40931
   110
fun smart_seconds r =
blanchet@40931
   111
  seconds (if r >= 100.0 then
blanchet@43018
   112
             (legacy_feature (quote auto_try_time_limitN ^
blanchet@40931
   113
                " expressed in milliseconds -- use seconds instead"); 0.001 * r)
blanchet@40931
   114
           else
blanchet@40931
   115
             r)
blanchet@40931
   116
blanchet@33561
   117
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
blanchet@43018
   118
  if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
blanchet@43020
   119
    TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state
blanchet@40931
   120
    handle TimeLimit.TimeOut => state
blanchet@40931
   121
  else
blanchet@40931
   122
    state))
blanchet@33561
   123
blanchet@33561
   124
end;