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