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