src/Tools/try.ML
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (18 months ago)
changeset 67835 c8e4ee2b5482
parent 67149 e61557884799
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned imports;
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@63690
     9
  type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
blanchet@43020
    10
blanchet@63690
    11
  val tryN: string
blanchet@33561
    12
blanchet@63690
    13
  val serial_commas: string -> string list -> string list
blanchet@63690
    14
  val subgoal_count: Proof.state -> int
blanchet@63690
    15
  val get_tools: theory -> tool list
blanchet@63690
    16
  val try_tools: Proof.state -> (string * string) option
blanchet@63690
    17
  val tool_setup: tool -> unit
blanchet@33561
    18
end;
blanchet@33561
    19
blanchet@43018
    20
structure Try : TRY =
blanchet@33561
    21
struct
blanchet@33561
    22
blanchet@63690
    23
type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)));
blanchet@43020
    24
blanchet@63690
    25
val tryN = "try";
blanchet@43020
    26
blanchet@43020
    27
blanchet@43028
    28
(* helpers *)
blanchet@43028
    29
blanchet@43028
    30
fun serial_commas _ [] = ["??"]
blanchet@43028
    31
  | serial_commas _ [s] = [s]
blanchet@43028
    32
  | serial_commas conj [s1, s2] = [s1, conj, s2]
blanchet@43028
    33
  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
blanchet@63690
    34
  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
blanchet@43028
    35
blanchet@63690
    36
val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
blanchet@43028
    37
blanchet@43028
    38
blanchet@33561
    39
(* configuration *)
blanchet@33561
    40
blanchet@43061
    41
fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
blanchet@63690
    42
  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2));
blanchet@43028
    43
wenzelm@33600
    44
structure Data = Theory_Data
wenzelm@33600
    45
(
blanchet@63690
    46
  type T = tool list;
blanchet@63690
    47
  val empty = [];
blanchet@63690
    48
  val extend = I;
blanchet@63690
    49
  fun merge data : T = Ord_List.merge tool_ord data;
blanchet@63690
    50
);
blanchet@33561
    51
blanchet@63690
    52
val get_tools = Data.get;
blanchet@43020
    53
blanchet@63690
    54
val register_tool = Data.map o Ord_List.insert tool_ord;
blanchet@33561
    55
wenzelm@52641
    56
blanchet@43020
    57
(* try command *)
blanchet@43020
    58
blanchet@43020
    59
fun try_tools state =
blanchet@43028
    60
  if subgoal_count state = 0 then
wenzelm@58843
    61
    (writeln "No subgoal!"; NONE)
blanchet@43028
    62
  else
blanchet@43028
    63
    get_tools (Proof.theory_of state)
blanchet@43028
    64
    |> tap (fn tools =>
blanchet@43028
    65
               "Trying " ^ space_implode " "
blanchet@43028
    66
                    (serial_commas "and" (map (quote o fst) tools)) ^ "..."
wenzelm@58843
    67
               |> writeln)
blanchet@43028
    68
    |> Par_List.get_some
blanchet@43028
    69
           (fn (name, (_, _, tool)) =>
blanchet@43028
    70
               case try (tool false) state of
blanchet@43028
    71
                 SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
blanchet@43028
    72
               | _ => NONE)
blanchet@63690
    73
    |> tap (fn NONE => writeln "Tried in vain" | _ => ());
blanchet@43020
    74
blanchet@43020
    75
val _ =
wenzelm@67149
    76
  Outer_Syntax.command \<^command_keyword>\<open>try\<close>
wenzelm@46961
    77
    "try a combination of automatic proving and disproving tools"
blanchet@63690
    78
    (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)));
blanchet@43020
    79
blanchet@33561
    80
wenzelm@52641
    81
(* automatic try (TTY) *)
blanchet@33561
    82
blanchet@43020
    83
fun auto_try state =
blanchet@43020
    84
  get_tools (Proof.theory_of state)
wenzelm@52639
    85
  |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
blanchet@43020
    86
  |> Par_List.get_some (fn tool =>
blanchet@63690
    87
    (case try (tool true) state of
blanchet@63690
    88
      SOME (true, (_, outcome)) => SOME outcome
blanchet@63690
    89
    | _ => NONE))
blanchet@63690
    90
  |> the_default [];
blanchet@40931
    91
wenzelm@52641
    92
wenzelm@52641
    93
(* asynchronous print function (PIDE) *)
wenzelm@52641
    94
wenzelm@52641
    95
fun print_function ((name, (weight, auto, tool)): tool) =
wenzelm@53839
    96
  Command.print_function ("auto_" ^ name)
wenzelm@58923
    97
    (fn {keywords, command_name, ...} =>
wenzelm@58923
    98
      if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
wenzelm@52651
    99
        SOME
wenzelm@56467
   100
         {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
wenzelm@52651
   101
          pri = ~ weight,
wenzelm@52651
   102
          persistent = true,
wenzelm@52953
   103
          strict = true,
wenzelm@52651
   104
          print_fn = fn _ => fn st =>
wenzelm@52651
   105
            let
wenzelm@52651
   106
              val state = Toplevel.proof_of st
wenzelm@52652
   107
                |> Proof.map_context (Context_Position.set_visible false)
wenzelm@56467
   108
              val auto_time_limit = Options.default_real @{system_option auto_time_limit}
wenzelm@52651
   109
            in
wenzelm@52651
   110
              if auto_time_limit > 0.0 then
wenzelm@62519
   111
                (case Timeout.apply (seconds auto_time_limit) (fn () => tool true state) () of
wenzelm@59184
   112
                  (true, (_, outcome)) => List.app Output.information outcome
wenzelm@52651
   113
                | _ => ())
wenzelm@52651
   114
              else ()
wenzelm@62505
   115
            end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
blanchet@63690
   116
      else NONE);
wenzelm@52641
   117
wenzelm@52641
   118
wenzelm@52641
   119
(* hybrid tool setup *)
wenzelm@52641
   120
blanchet@63690
   121
fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool);
wenzelm@52641
   122
blanchet@33561
   123
end;