Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)
(* Title: mirabelle.ML
Author: Jasmin Blanchette and Sascha Boehme
*)
signature MIRABELLE =
sig
(* configuration *)
val logfile : string Config.T
val timeout : int Config.T
val start_line : int Config.T
val end_line : int Config.T
val setup : theory -> theory
(* core *)
type action
val register : string * action -> theory -> theory
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
unit
(* utility functions *)
val goal_thm_of : Proof.state -> thm
val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
Proof.state -> bool
val theorems_in_proof_term : Thm.thm -> Thm.thm list
val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list
val get_setting : (string * string) list -> string * string -> string
val get_int_setting : (string * string) list -> string * int -> int
val cpu_time : ('a -> 'b) -> 'a -> 'b * int
end
structure Mirabelle : MIRABELLE =
struct
(* Mirabelle configuration *)
val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0
val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1
val setup = setup1 #> setup2 #> setup3 #> setup4
(* Mirabelle core *)
type action = {pre: Proof.state, post: Toplevel.state option,
timeout: Time.time, log: string -> unit} -> unit
structure Actions = TheoryDataFun
(
type T = action Symtab.table
val empty = Symtab.empty
val copy = I
val extend = I
fun merge _ = Symtab.merge (K true)
)
val register = Actions.map o Symtab.update_new
local
fun log thy s =
let fun append_to n = if n = "" then K () else File.append (Path.explode n)
in append_to (Config.get_thy thy logfile) (s ^ "\n") end
(* FIXME: with multithreading and parallel proofs enabled, we might need to
encapsulate this inside a critical section *)
fun log_sep thy = log thy "------------------"
fun try_with f NONE = SOME ()
| try_with f (SOME e) = (f e; try (fn () => reraise e) ())
fun capture_exns thy name f x =
(case try_with I (Exn.get_exn (Exn.capture f x)) of
NONE => (log thy ("Unhandled exception in " ^ quote name); log_sep thy)
| SOME _ => log_sep thy)
fun apply_actions thy info (pre, post, time) actions =
let
fun apply (name, action) =
{pre=pre, post=post, timeout=time, log=log thy}
|> capture_exns thy name action
in (log thy info; log_sep thy; List.app apply actions) end
fun in_range _ _ NONE = true
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
fun only_within_range thy pos f x =
let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
in if in_range l r (Position.line_of pos) then f x else () end
in
fun basic_hook tr pre post =
let
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
val name = Toplevel.name_of tr
val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
val str0 = string_of_int o the_default 0
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
in
Actions.get thy
|> Symtab.dest
|> only_within_range thy pos (apply_actions thy info st)
end
end
val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"]
fun step_hook tr pre post =
(* FIXME: might require wrapping into "interruptible" *)
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
not (member (op =) blacklist (Toplevel.name_of tr))
then basic_hook tr (Toplevel.proof_of pre) (SOME post)
else () (* FIXME: add theory_hook here *)
(* Mirabelle utility functions *)
val goal_thm_of = snd o snd o Proof.get_goal
fun can_apply time tac st =
let
val (ctxt, (facts, goal)) = Proof.get_goal st
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
in
(case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
SOME (thm, _) => true
| NONE => false)
end
local
fun fold_body_thms f =
let
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
fn (x, seen) =>
if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body
val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
(x, Inttab.update (i, ()) seen)
in (x' |> n = 0 ? f (name, prop, body'), seen') end)
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
in
fun theorems_in_proof_term thm =
let
val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
fun collect (s, _, _) = if s <> "" then insert (op =) s else I
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
fun resolve_thms names = map_filter (member_of names) all_thms
in
resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
end
end
fun theorems_of_sucessful_proof state =
(case state of
NONE => []
| SOME st =>
if not (Toplevel.is_proof st) then []
else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
fun get_setting settings (key, default) =
the_default default (AList.lookup (op =) settings key)
fun get_int_setting settings (key, default) =
(case Option.map Int.fromString (AList.lookup (op =) settings key) of
SOME (SOME i) => i
| SOME NONE => error ("bad option: " ^ key)
| NONE => default)
fun cpu_time f x =
let
val start = start_timing ()
val result = Exn.capture (fn () => f x) ()
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, time) end
end