src/HOL/Mirabelle/Tools/mirabelle.ML
author wenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 39232 69c6d3e87660
parent 36787 f60e4dd6d76f
child 39377 9e544eb396dc
permissions -rw-r--r--
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm@32564
     1
(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
wenzelm@32564
     2
    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
boehmes@32381
     3
*)
boehmes@32381
     4
boehmes@32381
     5
signature MIRABELLE =
boehmes@32381
     6
sig
wenzelm@32564
     7
  (*configuration*)
boehmes@32396
     8
  val logfile : string Config.T
boehmes@32381
     9
  val timeout : int Config.T
boehmes@32382
    10
  val start_line : int Config.T
boehmes@32382
    11
  val end_line : int Config.T
boehmes@32495
    12
  val setup : theory -> theory
boehmes@32381
    13
wenzelm@32564
    14
  (*core*)
wenzelm@32567
    15
  type init_action = int -> theory -> theory
wenzelm@32567
    16
  type done_args = {last: Toplevel.state, log: string -> unit}
wenzelm@32567
    17
  type done_action = int -> done_args -> unit
wenzelm@32567
    18
  type run_args = {pre: Proof.state, post: Toplevel.state option,
nipkow@32676
    19
    timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
wenzelm@32567
    20
  type run_action = int -> run_args -> unit
wenzelm@32567
    21
  type action = init_action * run_action * done_action
boehmes@32521
    22
  val catch : (int -> string) -> run_action -> run_action
boehmes@34052
    23
  val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) ->
boehmes@34052
    24
    int -> run_args -> 'a
boehmes@32515
    25
  val register : action -> theory -> theory
boehmes@32495
    26
  val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
boehmes@32495
    27
    unit
boehmes@32495
    28
wenzelm@32564
    29
  (*utility functions*)
boehmes@32469
    30
  val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
boehmes@32469
    31
    Proof.state -> bool
wenzelm@33243
    32
  val theorems_in_proof_term : thm -> thm list
wenzelm@33243
    33
  val theorems_of_sucessful_proof : Toplevel.state option -> thm list
boehmes@32385
    34
  val get_setting : (string * string) list -> string * string -> string
boehmes@32385
    35
  val get_int_setting : (string * string) list -> string * int -> int
boehmes@32498
    36
  val cpu_time : ('a -> 'b) -> 'a -> 'b * int
boehmes@32381
    37
end
boehmes@32381
    38
boehmes@32381
    39
boehmes@32381
    40
boehmes@32497
    41
structure Mirabelle : MIRABELLE =
boehmes@32495
    42
struct
boehmes@32495
    43
boehmes@32495
    44
(* Mirabelle configuration *)
boehmes@32495
    45
wenzelm@36001
    46
val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" (K "")
wenzelm@36001
    47
val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" (K 30)
wenzelm@36001
    48
val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" (K 0)
wenzelm@36001
    49
val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" (K ~1)
boehmes@32495
    50
boehmes@32495
    51
val setup = setup1 #> setup2 #> setup3 #> setup4
boehmes@32385
    52
boehmes@32385
    53
boehmes@32381
    54
(* Mirabelle core *)
boehmes@32381
    55
boehmes@32521
    56
type init_action = int -> theory -> theory
wenzelm@32567
    57
type done_args = {last: Toplevel.state, log: string -> unit}
wenzelm@32567
    58
type done_action = int -> done_args -> unit
wenzelm@32567
    59
type run_args = {pre: Proof.state, post: Toplevel.state option,
nipkow@32676
    60
  timeout: Time.time, log: string -> unit, pos: Position.T, name: string}
wenzelm@32567
    61
type run_action = int -> run_args -> unit
boehmes@32521
    62
type action = init_action * run_action * done_action
boehmes@32381
    63
wenzelm@33522
    64
structure Actions = Theory_Data
boehmes@32381
    65
(
boehmes@32521
    66
  type T = (int * run_action * done_action) list
boehmes@32515
    67
  val empty = []
boehmes@32381
    68
  val extend = I
wenzelm@33522
    69
  fun merge data = Library.merge (K true) data  (* FIXME ?!? *)
boehmes@32381
    70
)
boehmes@32381
    71
boehmes@32515
    72
boehmes@34035
    73
fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
boehmes@34035
    74
boehmes@34052
    75
fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
wenzelm@39232
    76
  handle exn =>
wenzelm@39232
    77
    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
boehmes@34035
    78
boehmes@34052
    79
fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
wenzelm@39232
    80
  handle exn =>
wenzelm@39232
    81
    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
boehmes@32515
    82
boehmes@32521
    83
fun register (init, run, done) thy =
boehmes@32521
    84
  let val id = length (Actions.get thy) + 1
boehmes@32521
    85
  in
boehmes@32521
    86
    thy
boehmes@32521
    87
    |> init id
boehmes@32521
    88
    |> Actions.map (cons (id, run, done))
boehmes@32521
    89
  end
boehmes@32381
    90
boehmes@32381
    91
local
boehmes@32381
    92
boehmes@32381
    93
fun log thy s =
boehmes@32381
    94
  let fun append_to n = if n = "" then K () else File.append (Path.explode n)
wenzelm@36787
    95
  in append_to (Config.get_global thy logfile) (s ^ "\n") end
boehmes@32381
    96
  (* FIXME: with multithreading and parallel proofs enabled, we might need to
boehmes@32381
    97
     encapsulate this inside a critical section *)
boehmes@32381
    98
boehmes@32498
    99
fun log_sep thy = log thy "------------------"
boehmes@32498
   100
nipkow@32676
   101
fun apply_actions thy pos name info (pre, post, time) actions =
boehmes@32472
   102
  let
nipkow@32676
   103
    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name}
boehmes@32521
   104
    fun run (id, run, _) = (apply (run id); log_sep thy)
boehmes@32515
   105
  in (log thy info; log_sep thy; List.app run actions) end
boehmes@32381
   106
boehmes@32381
   107
fun in_range _ _ NONE = true
boehmes@32381
   108
  | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
boehmes@32381
   109
boehmes@32381
   110
fun only_within_range thy pos f x =
wenzelm@36787
   111
  let val l = Config.get_global thy start_line and r = Config.get_global thy end_line
boehmes@32472
   112
  in if in_range l r (Position.line_of pos) then f x else () end
boehmes@32381
   113
boehmes@32381
   114
in
boehmes@32381
   115
boehmes@32521
   116
fun run_actions tr pre post =
boehmes@32381
   117
  let
boehmes@32381
   118
    val thy = Proof.theory_of pre
boehmes@32381
   119
    val pos = Toplevel.pos_of tr
boehmes@32381
   120
    val name = Toplevel.name_of tr
wenzelm@36787
   121
    val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
boehmes@32472
   122
boehmes@32472
   123
    val str0 = string_of_int o the_default 0
boehmes@32472
   124
    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
boehmes@32472
   125
    val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
boehmes@32381
   126
  in
nipkow@32676
   127
    only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy)
boehmes@32381
   128
  end
boehmes@32381
   129
boehmes@32521
   130
fun done_actions st =
boehmes@32521
   131
  let
boehmes@32521
   132
    val thy = Toplevel.theory_of st
boehmes@32521
   133
    val _ = log thy "\n\n";
boehmes@32521
   134
  in
boehmes@32521
   135
    thy
boehmes@32521
   136
    |> Actions.get
boehmes@32521
   137
    |> List.app (fn (id, _, done) => done id {last=st, log=log thy})
boehmes@32521
   138
  end
boehmes@32521
   139
boehmes@32381
   140
end
boehmes@32381
   141
boehmes@32504
   142
val whitelist = ["apply", "by", "proof"]
boehmes@32468
   143
boehmes@32381
   144
fun step_hook tr pre post =
boehmes@32381
   145
 (* FIXME: might require wrapping into "interruptible" *)
boehmes@32381
   146
  if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
boehmes@32504
   147
     member (op =) whitelist (Toplevel.name_of tr)
boehmes@32521
   148
  then run_actions tr (Toplevel.proof_of pre) (SOME post)
boehmes@32521
   149
  else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post
boehmes@32521
   150
  then done_actions pre
boehmes@32381
   151
  else ()   (* FIXME: add theory_hook here *)
boehmes@32381
   152
boehmes@32381
   153
boehmes@32381
   154
boehmes@32381
   155
(* Mirabelle utility functions *)
boehmes@32381
   156
boehmes@32472
   157
fun can_apply time tac st =
boehmes@32469
   158
  let
wenzelm@35592
   159
    val {context = ctxt, facts, goal} = Proof.goal st
boehmes@32469
   160
    val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
boehmes@32381
   161
  in
boehmes@32472
   162
    (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
boehmes@32381
   163
      SOME (thm, _) => true
boehmes@32381
   164
    | NONE => false)
boehmes@32381
   165
  end
boehmes@32381
   166
boehmes@32381
   167
local
boehmes@32381
   168
boehmes@32381
   169
fun fold_body_thms f =
boehmes@32381
   170
  let
boehmes@32381
   171
    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
boehmes@32381
   172
      fn (x, seen) =>
boehmes@32381
   173
        if Inttab.defined seen i then (x, seen)
boehmes@32381
   174
        else
boehmes@32381
   175
          let
boehmes@32381
   176
            val body' = Future.join body
boehmes@32381
   177
            val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
boehmes@32381
   178
              (x, Inttab.update (i, ()) seen)
boehmes@32381
   179
        in (x' |> n = 0 ? f (name, prop, body'), seen') end)
boehmes@32381
   180
  in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
boehmes@32381
   181
boehmes@32381
   182
in
boehmes@32381
   183
boehmes@32381
   184
fun theorems_in_proof_term thm =
boehmes@32381
   185
  let
boehmes@32381
   186
    val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
boehmes@32381
   187
    fun collect (s, _, _) = if s <> "" then insert (op =) s else I
boehmes@32381
   188
    fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
boehmes@32381
   189
    fun resolve_thms names = map_filter (member_of names) all_thms
boehmes@32381
   190
  in
boehmes@32381
   191
    resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
boehmes@32381
   192
  end
boehmes@32381
   193
boehmes@32381
   194
end
boehmes@32381
   195
boehmes@32381
   196
fun theorems_of_sucessful_proof state =
boehmes@32381
   197
  (case state of
boehmes@32381
   198
    NONE => []
boehmes@32381
   199
  | SOME st =>
boehmes@32381
   200
      if not (Toplevel.is_proof st) then []
wenzelm@35592
   201
      else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
boehmes@32381
   202
boehmes@32381
   203
fun get_setting settings (key, default) =
boehmes@32381
   204
  the_default default (AList.lookup (op =) settings key)
boehmes@32381
   205
boehmes@32381
   206
fun get_int_setting settings (key, default) =
boehmes@32381
   207
  (case Option.map Int.fromString (AList.lookup (op =) settings key) of
boehmes@32381
   208
    SOME (SOME i) => i
boehmes@32381
   209
  | SOME NONE => error ("bad option: " ^ key)
boehmes@32381
   210
  | NONE => default)
boehmes@32381
   211
boehmes@32498
   212
fun cpu_time f x =
boehmes@32498
   213
  let
boehmes@32498
   214
    val start = start_timing ()
boehmes@32498
   215
    val result = Exn.capture (fn () => f x) ()
boehmes@32498
   216
    val time = Time.toMilliseconds (#cpu (end_timing start))
boehmes@32498
   217
  in (Exn.release result, time) end
boehmes@32498
   218
boehmes@32381
   219
end