src/HOL/Tools/Mirabelle/Tools/mirabelle.ML

added "using" to blacklist

(* Title:  mirabelle.ML
   Author: Jasmin Blanchette and Sascha Boehme
*)

signature MIRABELLE =
sig
  type action
  val register : string * action -> theory -> theory

  val logfile : string Config.T
  val timeout : int Config.T
  val start_line : int Config.T
  val end_line : int Config.T

  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
end



signature MIRABELLE_EXT =
sig
  include MIRABELLE
  val setup : theory -> theory
  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
    unit
end



structure Mirabelle : MIRABELLE_EXT =
struct

(* 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

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

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_block thy msg = log thy (msg ^ "\n------------------")
fun log_action thy name msg = log_block thy (name ^ ": " ^ msg)

fun capture_exns logf f x =
  let
    fun f' x = f x
      handle TimeLimit.TimeOut => logf "time out"
           | ERROR msg => logf ("error: " ^ msg)
  in (case try f' x of NONE => logf "exception" | _ => ()) end

fun apply_actions thy info (pre, post, time) actions =
  let
    val _ = log_block thy info
    fun apply (name, action) =
      let val st = {pre=pre, post=post, timeout=time, log=log_action thy name}
      in capture_exns (log_action thy name) action st end
  in 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)

end