src/Tools/try.ML
author wenzelm
Fri Aug 15 18:02:34 2014 +0200 (2014-08-15)
changeset 57944 fff8d328da56
parent 56467 8d7d6f17c6a7
child 58842 22b87ab47d3b
permissions -rw-r--r--
more informative Token.Name with history of morphisms;
tuned signature;
     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 * string * (bool -> Proof.state -> bool * (string * Proof.state)))
    11 
    12   val tryN : string
    13 
    14   val serial_commas : string -> string list -> string list
    15   val subgoal_count : Proof.state -> int
    16   val get_tools : theory -> tool list
    17   val try_tools : Proof.state -> (string * string) option
    18   val tool_setup : tool -> unit
    19 end;
    20 
    21 structure Try : TRY =
    22 struct
    23 
    24 type tool =
    25   string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
    26 
    27 val tryN = "try"
    28 
    29 
    30 (* preferences *)
    31 
    32 val _ =
    33   ProofGeneral.preference_option ProofGeneral.category_tracing
    34     (SOME "4.0")
    35     @{system_option auto_time_limit}
    36     "auto-try-time-limit"
    37     "Time limit for automatically tried tools (in seconds)"
    38 
    39 
    40 (* helpers *)
    41 
    42 fun serial_commas _ [] = ["??"]
    43   | serial_commas _ [s] = [s]
    44   | serial_commas conj [s1, s2] = [s1, conj, s2]
    45   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    46   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    47 
    48 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    49 
    50 
    51 (* configuration *)
    52 
    53 fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
    54   prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
    55 
    56 structure Data = Theory_Data
    57 (
    58   type T = tool list
    59   val empty = []
    60   val extend = I
    61   fun merge data : T = Ord_List.merge tool_ord data
    62 )
    63 
    64 val get_tools = Data.get
    65 
    66 val register_tool = Data.map o Ord_List.insert tool_ord
    67 
    68 
    69 (* try command *)
    70 
    71 fun try_tools state =
    72   if subgoal_count state = 0 then
    73     (Output.urgent_message "No subgoal!"; NONE)
    74   else
    75     get_tools (Proof.theory_of state)
    76     |> tap (fn tools =>
    77                "Trying " ^ space_implode " "
    78                     (serial_commas "and" (map (quote o fst) tools)) ^ "..."
    79                |> Output.urgent_message)
    80     |> Par_List.get_some
    81            (fn (name, (_, _, tool)) =>
    82                case try (tool false) state of
    83                  SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    84                | _ => NONE)
    85     |> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
    86 
    87 val _ =
    88   Outer_Syntax.improper_command @{command_spec "try"}
    89     "try a combination of automatic proving and disproving tools"
    90     (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
    91 
    92 
    93 (* automatic try (TTY) *)
    94 
    95 fun auto_try state =
    96   get_tools (Proof.theory_of state)
    97   |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
    98   |> Par_List.get_some (fn tool =>
    99                            case try (tool true) state of
   100                              SOME (true, (_, state)) => SOME state
   101                            | _ => NONE)
   102   |> the_default state
   103 
   104 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   105   let
   106     val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   107   in
   108     if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
   109       TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
   110       handle TimeLimit.TimeOut => state
   111     else
   112       state
   113   end))
   114 
   115 
   116 (* asynchronous print function (PIDE) *)
   117 
   118 fun print_function ((name, (weight, auto, tool)): tool) =
   119   Command.print_function ("auto_" ^ name)
   120     (fn {command_name, ...} =>
   121       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
   122         SOME
   123          {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
   124           pri = ~ weight,
   125           persistent = true,
   126           strict = true,
   127           print_fn = fn _ => fn st =>
   128             let
   129               val state = Toplevel.proof_of st
   130                 |> Proof.map_context (Context_Position.set_visible false)
   131               val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   132             in
   133               if auto_time_limit > 0.0 then
   134                 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
   135                   (true, (_, state')) =>
   136                     List.app Pretty.writeln (Proof.pretty_goal_messages state')
   137                 | _ => ())
   138               else ()
   139             end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
   140       else NONE)
   141 
   142 
   143 (* hybrid tool setup *)
   144 
   145 fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
   146 
   147 end;