1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Mirabelle/mirabelle.ML Mon Aug 17 10:59:12 2009 +0200
1.3 @@ -0,0 +1,318 @@
1.4 +(* Title: mirabelle.ML
1.5 + Author: Jasmin Blanchette and Sascha Boehme
1.6 +*)
1.7 +
1.8 +signature MIRABELLE =
1.9 +sig
1.10 + type action
1.11 + type settings
1.12 + val register : string -> action -> theory -> theory
1.13 + val invoke : string -> settings -> theory -> theory
1.14 +
1.15 + val timeout : int Config.T
1.16 + val verbose : bool Config.T
1.17 + val set_logfile : string -> theory -> theory
1.18 +
1.19 + val setup : theory -> theory
1.20 +
1.21 + val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
1.22 + unit
1.23 +
1.24 + val goal_thm_of : Proof.state -> thm
1.25 + val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
1.26 + val theorems_in_proof_term : Thm.thm -> Thm.thm list
1.27 + val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
1.28 + val get_setting : settings -> string * string -> string
1.29 + val get_int_setting : settings -> string * int -> int
1.30 +
1.31 +(* FIXME val refute_action : action *)
1.32 + val quickcheck_action : action
1.33 + val arith_action : action
1.34 + val sledgehammer_action : action
1.35 + val metis_action : action
1.36 +end
1.37 +
1.38 +
1.39 +
1.40 +structure Mirabelle (*: MIRABELLE*) =
1.41 +struct
1.42 +
1.43 +(* Mirabelle core *)
1.44 +
1.45 +type settings = (string * string) list
1.46 +type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
1.47 +type action = settings -> invoked
1.48 +
1.49 +structure Registered = TheoryDataFun
1.50 +(
1.51 + type T = action Symtab.table
1.52 + val empty = Symtab.empty
1.53 + val copy = I
1.54 + val extend = I
1.55 + fun merge _ = Symtab.merge (K true)
1.56 +)
1.57 +
1.58 +fun register name act = Registered.map (Symtab.update_new (name, act))
1.59 +
1.60 +
1.61 +structure Invoked = TheoryDataFun
1.62 +(
1.63 + type T = (string * invoked) list
1.64 + val empty = []
1.65 + val copy = I
1.66 + val extend = I
1.67 + fun merge _ = Library.merge (K true)
1.68 +)
1.69 +
1.70 +fun invoke name sts thy =
1.71 + let
1.72 + val act =
1.73 + (case Symtab.lookup (Registered.get thy) name of
1.74 + SOME act => act
1.75 + | NONE => error ("The invoked action " ^ quote name ^
1.76 + " is not registered."))
1.77 + in Invoked.map (cons (name, act sts)) thy end
1.78 +
1.79 +val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" ""
1.80 +val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30
1.81 +val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true
1.82 +val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
1.83 +val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
1.84 +
1.85 +val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
1.86 +
1.87 +fun set_logfile name =
1.88 + let val _ = File.write (Path.explode name) "" (* erase file content *)
1.89 + in Config.put_thy logfile name end
1.90 +
1.91 +local
1.92 +
1.93 +fun log thy s =
1.94 + let fun append_to n = if n = "" then K () else File.append (Path.explode n)
1.95 + in append_to (Config.get_thy thy logfile) (s ^ "\n") end
1.96 + (* FIXME: with multithreading and parallel proofs enabled, we might need to
1.97 + encapsulate this inside a critical section *)
1.98 +
1.99 +fun verbose_msg verbose msg = if verbose then SOME msg else NONE
1.100 +
1.101 +fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x
1.102 + handle TimeLimit.TimeOut => verbose_msg verb "time out"
1.103 + | ERROR msg => verbose_msg verb ("error: " ^ msg)
1.104 +
1.105 +fun capture_exns verb f x =
1.106 + (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
1.107 +
1.108 +fun apply_action (c as (verb, _)) st (name, invoked) =
1.109 + Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
1.110 +
1.111 +fun in_range _ _ NONE = true
1.112 + | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
1.113 +
1.114 +fun only_within_range thy pos f x =
1.115 + let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
1.116 + in if in_range l r (Position.line_of pos) then f x else [] end
1.117 +
1.118 +fun pretty_print verbose pos name msgs =
1.119 + let
1.120 + val file = the_default "unknown file" (Position.file_of pos)
1.121 +
1.122 + val str0 = string_of_int o the_default 0
1.123 + val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
1.124 +
1.125 + val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
1.126 + val head = full_loc ^ " (" ^ name ^ "):"
1.127 +
1.128 + fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
1.129 + in
1.130 + Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
1.131 + end
1.132 +
1.133 +in
1.134 +
1.135 +fun basic_hook tr pre post =
1.136 + let
1.137 + val thy = Proof.theory_of pre
1.138 + val pos = Toplevel.pos_of tr
1.139 + val name = Toplevel.name_of tr
1.140 + val verb = Config.get_thy thy verbose
1.141 + val secs = Time.fromSeconds (Config.get_thy thy timeout)
1.142 + val st = {pre=pre, post=post}
1.143 + in
1.144 + Invoked.get thy
1.145 + |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
1.146 + |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
1.147 + end
1.148 +
1.149 +end
1.150 +
1.151 +fun step_hook tr pre post =
1.152 + (* FIXME: might require wrapping into "interruptible" *)
1.153 + if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
1.154 + not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
1.155 + then basic_hook tr (Toplevel.proof_of pre) (SOME post)
1.156 + else () (* FIXME: add theory_hook here *)
1.157 +
1.158 +
1.159 +
1.160 +(* Mirabelle utility functions *)
1.161 +
1.162 +val goal_thm_of = snd o snd o Proof.get_goal
1.163 +
1.164 +fun can_apply tac st =
1.165 + let val (ctxt, (facts, goal)) = Proof.get_goal st
1.166 + in
1.167 + (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of
1.168 + SOME (thm, _) => true
1.169 + | NONE => false)
1.170 + end
1.171 +
1.172 +local
1.173 +
1.174 +fun fold_body_thms f =
1.175 + let
1.176 + fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) =>
1.177 + fn (x, seen) =>
1.178 + if Inttab.defined seen i then (x, seen)
1.179 + else
1.180 + let
1.181 + val body' = Future.join body
1.182 + val (x', seen') = app (n + (if name = "" then 0 else 1)) body'
1.183 + (x, Inttab.update (i, ()) seen)
1.184 + in (x' |> n = 0 ? f (name, prop, body'), seen') end)
1.185 + in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end
1.186 +
1.187 +in
1.188 +
1.189 +fun theorems_in_proof_term thm =
1.190 + let
1.191 + val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm)
1.192 + fun collect (s, _, _) = if s <> "" then insert (op =) s else I
1.193 + fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE
1.194 + fun resolve_thms names = map_filter (member_of names) all_thms
1.195 + in
1.196 + resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] [])
1.197 + end
1.198 +
1.199 +end
1.200 +
1.201 +fun theorems_of_sucessful_proof state =
1.202 + (case state of
1.203 + NONE => []
1.204 + | SOME st =>
1.205 + if not (Toplevel.is_proof st) then []
1.206 + else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
1.207 +
1.208 +fun get_setting settings (key, default) =
1.209 + the_default default (AList.lookup (op =) settings key)
1.210 +
1.211 +fun get_int_setting settings (key, default) =
1.212 + (case Option.map Int.fromString (AList.lookup (op =) settings key) of
1.213 + SOME (SOME i) => i
1.214 + | SOME NONE => error ("bad option: " ^ key)
1.215 + | NONE => default)
1.216 +
1.217 +
1.218 +
1.219 +(* Mirabelle actions *)
1.220 +
1.221 +(* FIXME
1.222 +fun refute_action settings {pre=st, ...} =
1.223 + let
1.224 + val params = [("minsize", "2") (*"maxsize", "2"*)]
1.225 + val subgoal = 0
1.226 + val thy = Proof.theory_of st
1.227 + val thm = goal_thm_of st
1.228 +
1.229 + val _ = Refute.refute_subgoal thy parms thm subgoal
1.230 + in
1.231 + val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
1.232 + val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
1.233 +
1.234 + val r =
1.235 + if Substring.isSubstring "model found" writ_log
1.236 + then
1.237 + if Substring.isSubstring "spurious" warn_log
1.238 + then SOME "potential counterexample"
1.239 + else SOME "real counterexample (bug?)"
1.240 + else
1.241 + if Substring.isSubstring "time limit" writ_log
1.242 + then SOME "no counterexample (time out)"
1.243 + else if Substring.isSubstring "Search terminated" writ_log
1.244 + then SOME "no counterexample (normal termination)"
1.245 + else SOME "no counterexample (unknown)"
1.246 + in r end
1.247 +*)
1.248 +
1.249 +fun quickcheck_action settings {pre=st, ...} =
1.250 + let
1.251 + val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
1.252 + val args = filter has_valid_key settings
1.253 + in
1.254 + (case Quickcheck.quickcheck args 1 st of
1.255 + NONE => SOME "no counterexample"
1.256 + | SOME _ => SOME "counterexample found")
1.257 + end
1.258 +
1.259 +
1.260 +fun arith_action _ {pre=st, ...} =
1.261 + if can_apply Arith_Data.arith_tac st
1.262 + then SOME "succeeded"
1.263 + else NONE
1.264 +
1.265 +
1.266 +fun sledgehammer_action settings {pre=st, ...} =
1.267 + let
1.268 + val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
1.269 + val thy = Proof.theory_of st
1.270 +
1.271 + val prover = the (AtpManager.get_prover prover_name thy)
1.272 + val timeout = AtpManager.get_timeout ()
1.273 +
1.274 + val (success, message) =
1.275 + let
1.276 + val (success, message, _, _, _) =
1.277 + prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
1.278 + in (success, message) end
1.279 + handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
1.280 + | ERROR msg => (false, "error: " ^ msg)
1.281 + in
1.282 + if success
1.283 + then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
1.284 + else NONE
1.285 + end
1.286 +
1.287 +
1.288 +fun metis_action settings {pre, post} =
1.289 + let
1.290 + val thms = theorems_of_sucessful_proof post
1.291 + val names = map Thm.get_name thms
1.292 +
1.293 + val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
1.294 +
1.295 + fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
1.296 + in
1.297 + (if can_apply metis pre then "succeeded" else "failed")
1.298 + |> suffix (" (" ^ commas names ^ ")")
1.299 + |> SOME
1.300 + end
1.301 +
1.302 +
1.303 +
1.304 +(* Mirabelle setup *)
1.305 +
1.306 +val setup =
1.307 + setup_config #>
1.308 +(* FIXME register "refute" refute_action #> *)
1.309 + register "quickcheck" quickcheck_action #>
1.310 + register "arith" arith_action #>
1.311 + register "sledgehammer" sledgehammer_action #>
1.312 + register "metis" metis_action (* #> FIXME:
1.313 + Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
1.314 +
1.315 +end
1.316 +
1.317 +val _ = Toplevel.add_hook Mirabelle.step_hook
1.318 +
1.319 +(* no multithreading, no parallel proofs *)
1.320 +val _ = Multithreading.max_threads := 1
1.321 +val _ = Goal.parallel_proofs := 0