--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Fri Aug 21 09:49:10 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Fri Aug 21 13:21:19 2009 +0200
@@ -5,9 +5,7 @@
signature MIRABELLE =
sig
type action
- type settings
- val register : string -> action -> theory -> theory
- val invoke : string -> settings -> theory -> theory
+ val register : string * action -> theory -> theory
val timeout : int Config.T
val verbose : bool Config.T
@@ -15,37 +13,34 @@
val end_line : int Config.T
val set_logfile : string -> theory -> theory
- val setup : theory -> theory
-
- val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
- unit
-
val goal_thm_of : Proof.state -> thm
val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
val theorems_in_proof_term : Thm.thm -> Thm.thm list
- val theorems_of_sucessful_proof : Toplevel.state -> Thm.thm list
- val get_setting : settings -> string * string -> string
- val get_int_setting : settings -> string * int -> int
-
-(* FIXME val refute_action : action *)
- val quickcheck_action : action
- val arith_action : action
- val sledgehammer_action : action
- val metis_action : action
+ 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
-structure Mirabelle (*: MIRABELLE*) =
+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 settings = (string * string) list
-type invoked = {pre: Proof.state, post: Toplevel.state option} -> string option
-type action = settings -> invoked
+type action = {pre: Proof.state, post: Toplevel.state option} -> string option
-structure Registered = TheoryDataFun
+structure Actions = TheoryDataFun
(
type T = action Symtab.table
val empty = Symtab.empty
@@ -54,26 +49,7 @@
fun merge _ = Symtab.merge (K true)
)
-fun register name act = Registered.map (Symtab.update_new (name, act))
-
-
-structure Invoked = TheoryDataFun
-(
- type T = (string * invoked) list
- val empty = []
- val copy = I
- val extend = I
- fun merge _ = Library.merge (K true)
-)
-
-fun invoke name sts thy =
- let
- val act =
- (case Symtab.lookup (Registered.get thy) name of
- SOME act => act
- | NONE => error ("The invoked action " ^ quote name ^
- " is not registered."))
- in Invoked.map (cons (name, act sts)) thy end
+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
@@ -81,7 +57,7 @@
val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0
val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1
-val setup_config = setup1 #> setup2 #> setup3 #> setup4 #> setup5
+val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
fun set_logfile name =
let val _ = File.write (Path.explode name) "" (* erase file content *)
@@ -104,8 +80,8 @@
fun capture_exns verb f x =
(case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg)
-fun apply_action (c as (verb, _)) st (name, invoked) =
- Option.map (pair name) (capture_exns verb (with_time_limit c invoked) st)
+fun apply_action (c as (verb, _)) st (name, action) =
+ Option.map (pair name) (capture_exns verb (with_time_limit c action) st)
fun in_range _ _ NONE = true
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
@@ -140,7 +116,8 @@
val secs = Time.fromSeconds (Config.get_thy thy timeout)
val st = {pre=pre, post=post}
in
- Invoked.get thy
+ Actions.get thy
+ |> Symtab.dest
|> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
|> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
end
@@ -213,108 +190,4 @@
| SOME NONE => error ("bad option: " ^ key)
| NONE => default)
-
-
-(* Mirabelle actions *)
-
-(* FIXME
-fun refute_action settings {pre=st, ...} =
- let
- val params = [("minsize", "2") (*"maxsize", "2"*)]
- val subgoal = 0
- val thy = Proof.theory_of st
- val thm = goal_thm_of st
-
- val _ = Refute.refute_subgoal thy parms thm subgoal
- in
- val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
- val warn_log = Substring.full (the (Symtab.lookup tab "warning"))
-
- val r =
- if Substring.isSubstring "model found" writ_log
- then
- if Substring.isSubstring "spurious" warn_log
- then SOME "potential counterexample"
- else SOME "real counterexample (bug?)"
- else
- if Substring.isSubstring "time limit" writ_log
- then SOME "no counterexample (time out)"
- else if Substring.isSubstring "Search terminated" writ_log
- then SOME "no counterexample (normal termination)"
- else SOME "no counterexample (unknown)"
- in r end
-*)
-
-fun quickcheck_action settings {pre=st, ...} =
- let
- val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
- val args = filter has_valid_key settings
- in
- (case Quickcheck.quickcheck args 1 st of
- NONE => SOME "no counterexample"
- | SOME _ => SOME "counterexample found")
- end
-
-
-fun arith_action _ {pre=st, ...} =
- if can_apply Arith_Data.arith_tac st
- then SOME "succeeded"
- else NONE
-
-
-fun sledgehammer_action settings {pre=st, ...} =
- let
- val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
- val thy = Proof.theory_of st
-
- val prover = the (AtpManager.get_prover prover_name thy)
- val timeout = AtpManager.get_timeout ()
-
- val (success, message) =
- let
- val (success, message, _, _, _) =
- prover timeout NONE NONE prover_name 1 (Proof.get_goal st)
- in (success, message) end
- handle ResHolClause.TOO_TRIVIAL => (true, "trivial")
- | ERROR msg => (false, "error: " ^ msg)
- in
- if success
- then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
- else NONE
- end
-
-
-fun metis_action settings {pre, post} =
- let
- val thms = theorems_of_sucessful_proof post
- val names = map Thm.get_name thms
-
- val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
-
- fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
- in
- (if can_apply metis pre then "succeeded" else "failed")
- |> suffix (" (" ^ commas names ^ ")")
- |> SOME
- end
-
-
-
-(* Mirabelle setup *)
-
-val setup =
- setup_config #>
-(* FIXME register "refute" refute_action #> *)
- register "quickcheck" quickcheck_action #>
- register "arith" arith_action #>
- register "sledgehammer" sledgehammer_action #>
- register "metis" metis_action (* #> FIXME:
- Context.theory_map (Specification.add_theorem_hook theorem_hook) *)
-
end
-
-val _ = Toplevel.add_hook Mirabelle.step_hook
-
-(* no multithreading, no parallel proofs *)
-val _ = Multithreading.max_threads := 1
-val _ = Goal.parallel_proofs := 0