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