src/Tools/try.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58923 cb9b69cca999
child 59184 830bb7ddb3ab
permissions -rw-r--r--
proper context for match_tac etc.;
     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 * string list)))
    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 * string list)))
    26 
    27 val tryN = "try"
    28 
    29 
    30 (* helpers *)
    31 
    32 fun serial_commas _ [] = ["??"]
    33   | serial_commas _ [s] = [s]
    34   | serial_commas conj [s1, s2] = [s1, conj, s2]
    35   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    36   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    37 
    38 val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    39 
    40 
    41 (* configuration *)
    42 
    43 fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
    44   prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
    45 
    46 structure Data = Theory_Data
    47 (
    48   type T = tool list
    49   val empty = []
    50   val extend = I
    51   fun merge data : T = Ord_List.merge tool_ord data
    52 )
    53 
    54 val get_tools = Data.get
    55 
    56 val register_tool = Data.map o Ord_List.insert tool_ord
    57 
    58 
    59 (* try command *)
    60 
    61 fun try_tools state =
    62   if subgoal_count state = 0 then
    63     (writeln "No subgoal!"; NONE)
    64   else
    65     get_tools (Proof.theory_of state)
    66     |> tap (fn tools =>
    67                "Trying " ^ space_implode " "
    68                     (serial_commas "and" (map (quote o fst) tools)) ^ "..."
    69                |> writeln)
    70     |> Par_List.get_some
    71            (fn (name, (_, _, tool)) =>
    72                case try (tool false) state of
    73                  SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
    74                | _ => NONE)
    75     |> tap (fn NONE => writeln "Tried in vain." | _ => ())
    76 
    77 val _ =
    78   Outer_Syntax.command @{command_spec "try"}
    79     "try a combination of automatic proving and disproving tools"
    80     (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
    81 
    82 
    83 (* automatic try (TTY) *)
    84 
    85 fun auto_try state =
    86   get_tools (Proof.theory_of state)
    87   |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
    88   |> Par_List.get_some (fn tool =>
    89                            case try (tool true) state of
    90                              SOME (true, (_, outcome)) => SOME outcome
    91                            | _ => NONE)
    92   |> the_default []
    93 
    94 
    95 (* asynchronous print function (PIDE) *)
    96 
    97 fun print_function ((name, (weight, auto, tool)): tool) =
    98   Command.print_function ("auto_" ^ name)
    99     (fn {keywords, command_name, ...} =>
   100       if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
   101         SOME
   102          {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
   103           pri = ~ weight,
   104           persistent = true,
   105           strict = true,
   106           print_fn = fn _ => fn st =>
   107             let
   108               val state = Toplevel.proof_of st
   109                 |> Proof.map_context (Context_Position.set_visible false)
   110               val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   111             in
   112               if auto_time_limit > 0.0 then
   113                 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
   114                   (true, (_, outcome)) => List.app writeln outcome
   115                 | _ => ())
   116               else ()
   117             end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
   118       else NONE)
   119 
   120 
   121 (* hybrid tool setup *)
   122 
   123 fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
   124 
   125 end;