--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Tue Sep 01 21:44:19 2009 +0200
@@ -38,8 +38,8 @@
(* Mirabelle core *)
-type action = Time.time -> {pre: Proof.state, post: Toplevel.state option} ->
- string option
+type action = {pre: Proof.state, post: Toplevel.state option,
+ timeout: Time.time, log: string -> unit} -> unit
structure Actions = TheoryDataFun
(
@@ -67,33 +67,30 @@
(* FIXME: with multithreading and parallel proofs enabled, we might need to
encapsulate this inside a critical section *)
-fun capture_exns f x =
+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 => SOME "time out"
- | ERROR msg => SOME ("error: " ^ msg)
- in (case try f' x of NONE => SOME "exception" | SOME msg => msg) end
+ handle TimeLimit.TimeOut => logf "time out"
+ | ERROR msg => logf ("error: " ^ msg)
+ in (case try f' x of NONE => logf "exception" | _ => ()) end
-fun apply_action timeout st (name, action) =
- Option.map (pair name) (capture_exns (action timeout) st)
+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
-
-fun pretty_print pos name msgs =
- let
- val str0 = string_of_int o the_default 0
- val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
- val head = "at " ^ loc ^ " (" ^ name ^ "):"
-
- fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
- in
- Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
- end
+ in if in_range l r (Position.line_of pos) then f x else () end
in
@@ -102,18 +99,20 @@
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
val name = Toplevel.name_of tr
- val timeout = Time.fromSeconds (Config.get_thy thy timeout)
- val st = {pre=pre, post=post}
+ 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 (map_filter (apply_action timeout st))
- |> (fn [] => () | msgs => log thy (pretty_print pos name msgs))
+ |> only_within_range thy pos (apply_actions thy info st)
end
end
-val blacklist = ["disable_pr", "enable_pr", "done", "."]
+val blacklist = ["disable_pr", "enable_pr", "done", ".", "txt"]
fun step_hook tr pre post =
(* FIXME: might require wrapping into "interruptible" *)
@@ -128,12 +127,12 @@
val goal_thm_of = snd o snd o Proof.get_goal
-fun can_apply timeout tac st =
+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 timeout (Seq.pull o full_tac) goal of
+ (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
SOME (thm, _) => true
| NONE => false)
end
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Tue Sep 01 21:44:19 2009 +0200
@@ -5,10 +5,10 @@
structure Mirabelle_Arith : MIRABELLE_ACTION =
struct
-fun arith_action timeout {pre=st, ...} =
- if Mirabelle.can_apply timeout Arith_Data.arith_tac st
- then SOME "succeeded"
- else NONE
+fun arith_action {pre, timeout, log, ...} =
+ if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
+ then log "succeeded"
+ else ()
fun invoke _ = Mirabelle.register ("arith", arith_action)
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Tue Sep 01 21:44:19 2009 +0200
@@ -5,18 +5,19 @@
structure Mirabelle_Metis : MIRABELLE_ACTION =
struct
-fun metis_action timeout {pre, post} =
+fun metis_action {pre, post, timeout, log} =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
val names = map Thm.get_name thms
+ val add_info = if null names then I else suffix (":\n" ^ commas names)
val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> suffix (" (" ^ commas names ^ ")")
- |> SOME
+ |> add_info
+ |> log
end
fun invoke _ = Mirabelle.register ("metis", metis_action)
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 01 21:44:19 2009 +0200
@@ -29,7 +29,7 @@
val keepK = "keep"
val metisK = "metis"
-fun sledgehammer_action args timeout {pre=st, ...} =
+fun sledgehammer_action args {pre=st, timeout, log, ...} =
let
val prover_name =
AList.lookup (op =) args proverK
@@ -56,25 +56,28 @@
TimeLimit.timeLimit timeout atp (Proof.get_goal st)
in (success, message, SOME thm_names) end
handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
- | ERROR msg => (false, "error: " ^ msg, NONE)
val (success, message, thm_names) = safe init done sh
(AList.lookup (op =) args keepK)
+ val _ =
+ if success then log (quote prover_name ^ " succeeded:\n" ^ message)
+ else log (prover_name ^ " failed")
(* try metis *)
fun get_thms ctxt = maps (thms_of_name ctxt)
fun metis thms ctxt = MetisTools.metis_tac ctxt thms
- fun apply_metis thms = "\nApplying metis with these theorems: " ^
- (if Mirabelle.can_apply timeout (metis thms) st
- then "success"
- else "failure")
- val msg = if not (AList.defined (op =) args metisK) then ""
- else (apply_metis (get_thms (Proof.context_of st) (these thm_names))
- handle ERROR m => "\nException: " ^ m)
- in
- if success
- then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
- else NONE
- end
+ fun log_metis s =
+ log ("applying metis: " ^ s)
+ fun apply_metis thms =
+ if Mirabelle.can_apply timeout (metis thms) st
+ then "succeeded" else "failed"
+ val _ =
+ if not (AList.defined (op =) args metisK) then ()
+ else
+ these thm_names
+ |> get_thms (Proof.context_of st)
+ |> apply_metis
+ |> log_metis
+ in () end
fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Tue Sep 01 21:44:19 2009 +0200
@@ -120,7 +120,6 @@
foreach $name (@action_names) {
print LOG_FILE " $name\n";
}
-print LOG_FILE "\n\n";
close(LOG_FILE);
my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
--- a/src/Pure/Isar/isar_document.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML Tue Sep 01 21:44:19 2009 +0200
@@ -15,7 +15,7 @@
val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
end;
-structure IsarDocument: ISAR_DOCUMENT =
+structure Isar_Document: ISAR_DOCUMENT =
struct
(* unique identifiers *)
--- a/src/Pure/Isar/isar_document.scala Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala Tue Sep 01 21:44:19 2009 +0200
@@ -7,7 +7,7 @@
package isabelle
-object IsarDocument
+object Isar_Document
{
/* unique identifiers */
@@ -17,9 +17,9 @@
}
-trait IsarDocument extends Isabelle_Process
+trait Isar_Document extends Isabelle_Process
{
- import IsarDocument._
+ import Isar_Document._
/* commands */
--- a/src/Pure/Isar/isar_syn.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Sep 01 21:44:19 2009 +0200
@@ -30,7 +30,7 @@
val _ =
OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
- (ThyHeader.args >> (Toplevel.print oo IsarCmd.init_theory));
+ (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
val _ =
OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
--- a/src/Pure/ProofGeneral/pgip_parser.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Tue Sep 01 21:44:19 2009 +0200
@@ -20,7 +20,7 @@
fun badcmd text = [D.Badcmd {text = text}];
fun thy_begin text =
- (case try (ThyHeader.read Position.none) (Source.of_string text) of
+ (case try (Thy_Header.read Position.none) (Source.of_string text) of
NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
| SOME (name, imports, _) =>
D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
--- a/src/Pure/Thy/thy_header.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Thy/thy_header.ML Tue Sep 01 21:44:19 2009 +0200
@@ -11,7 +11,7 @@
val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
end;
-structure ThyHeader: THY_HEADER =
+structure Thy_Header: THY_HEADER =
struct
structure T = OuterLex;
--- a/src/Pure/Thy/thy_header.scala Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Sep 01 21:44:19 2009 +0200
@@ -7,7 +7,7 @@
package isabelle
-object ThyHeader
+object Thy_Header
{
val HEADER = "header"
val THEORY = "theory"
--- a/src/Pure/Thy/thy_load.ML Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML Tue Sep 01 21:44:19 2009 +0200
@@ -109,7 +109,7 @@
val master as (path, _) = check_thy dir name;
val text = explode (File.read path);
val (name', imports, uses) =
- ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
+ Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
val _ = check_name name name';
val uses = map (Path.explode o #1) uses;
in {master = master, text = text, imports = imports, uses = uses} end;