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