1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Time_Methods_Cmd imports
8  Main
9begin
10
11(* See Time_Methods_Cmd_Test for documentation *)
12
13ML \<open>
14structure Time_Methods = struct
15  (* Work around Isabelle running every apply method on a dummy proof state *)
16  fun skip_dummy_state (method: Method.method) : Method.method =
17    fn facts => fn (ctxt, st) =>
18      case Thm.prop_of st of
19          Const ("Pure.prop", _) $ (Const ("Pure.term", _) $ Const ("Pure.dummy_pattern", _)) =>
20            Seq.succeed (Seq.Result (ctxt, st))
21        | _ => method facts (ctxt, st);
22
23  (* ML interface. Takes a list of (possibly-named) methods, then calls the supplied
24   * callback with the method index (starting from 1), supplied name and timing.
25   * Also returns the list of timings at the end. *)
26  fun time_methods
27        (no_check: bool)
28        (skip_fail: bool)
29        (callback: (int * string option -> Timing.timing -> unit))
30        (maybe_named_methods: (string option * Method.method) list)
31        (* like Method.method but also returns timing list *)
32        : thm list -> context_state -> (Timing.timing list * context_state Seq.result Seq.seq)
33    = fn facts => fn (ctxt, st) => let
34        fun run method =
35              Timing.timing (fn () =>
36                case method facts (ctxt, st) |> Seq.pull of
37                  (* Peek at first result, then put it back *)
38                    NONE => (NONE, Seq.empty)
39                  | SOME (r as Seq.Result (_, st'), rs) => (SOME st', Seq.cons r rs)
40                  | SOME (r as Seq.Error _, rs) => (NONE, Seq.cons r rs)
41              ) ()
42
43        val results = tag_list 1 maybe_named_methods
44              |> map (fn (idx1, (maybe_name, method)) =>
45                  let val (time, (st', results)) = run method
46                      val _ =
47                        if Option.isSome st' orelse not skip_fail
48                        then callback (idx1, maybe_name) time
49                        else ()
50                      val name = Option.getOpt (maybe_name, "[method " ^ string_of_int idx1 ^ "]")
51                  in {name = name, state = st', results = results, time = time} end)
52
53        val canonical_result = hd results
54        val other_results = tl results
55        val return_val = (map #time results, #results canonical_result)
56        fun show_state NONE = @{thm FalseE[where P="METHOD_FAILED"]}
57          | show_state (SOME st) = st
58      in
59        if no_check then return_val else
60        (* Compare the proof states that we peeked at *)
61        case other_results
62              |> filter (fn result =>
63                    (* It's tempting to use aconv, etc., here instead of (<>), but
64                     * minute differences such as bound names in Pure.all can
65                     * break a proof script later on. *)
66                    Option.map Thm.full_prop_of (#state result) <>
67                    Option.map Thm.full_prop_of (#state canonical_result)) of
68            [] => return_val
69          | (bad_result::_) =>
70              raise THM ("methods \"" ^ #name canonical_result ^
71                         "\" and \"" ^ #name bad_result ^ "\" have different results",
72                         1, map (show_state o #state) [canonical_result, bad_result])
73      end
74end
75\<close>
76
77method_setup time_methods = \<open>
78let
79  fun scan_flag name = Scan.lift (Scan.optional (Args.parens (Parse.reserved name) >> K true) false)
80  val parse_no_check = scan_flag "no_check"
81  val parse_skip_fail = scan_flag "skip_fail"
82  val parse_maybe_name = Scan.option (Scan.lift (Parse.liberal_name --| Parse.$$$ ":"))
83  fun auto_name (idx1, maybe_name) =
84        Option.getOpt (maybe_name, "[method " ^ string_of_int idx1 ^ "]")
85in
86  parse_no_check -- parse_skip_fail --
87  Scan.repeat1 (parse_maybe_name -- Method.text_closure) >>
88  (fn ((no_check, skip_fail), maybe_named_methods_text) => fn ctxt =>
89      let
90        val max_length = tag_list 1 (map fst maybe_named_methods_text)
91                         |> map (String.size o auto_name)
92                         |> (fn ls => fold (curry Int.max) ls 0)
93        fun pad_name s =
94           let val pad_length = max_length + String.size ": " - String.size s
95           in s ^ replicate_string pad_length " " end
96        fun timing_callback id time = warning (pad_name (auto_name id ^ ": ") ^ Timing.message time)
97        val maybe_named_methods = maybe_named_methods_text
98              |> map (apsnd (fn method_text => Method.evaluate method_text ctxt))
99        val timed_method = Time_Methods.time_methods no_check skip_fail timing_callback maybe_named_methods
100        fun method_discard_times facts st = snd (timed_method facts st)
101      in
102        method_discard_times
103        |> Time_Methods.skip_dummy_state
104      end)
105end
106\<close> "Compare running time of several methods on the current proof state"
107
108end
109