# HG changeset patch
# User boehmes
# Date 1252010851 -7200
# Node ID e7c0d3c0494a8f72c8948ce633c1aace181abf71
# Parent  43d2ac4aa2de8e73df4529a2a86023559ea192c8
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
removed PolyML.makestring (no strict dependency on PolyML anymore)

diff -r 43d2ac4aa2de -r e7c0d3c0494a src/HOL/Mirabelle/ROOT.ML
--- a/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -1,3 +1,1 @@
-if String.isPrefix "polyml" ml_system
-then use_thy "MirabelleTest"
-else ();
+use_thy "MirabelleTest";
diff -r 43d2ac4aa2de -r e7c0d3c0494a src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -13,7 +13,8 @@
 
   (* core *)
   type action
-  val register : string * action -> theory -> theory
+  val catch : string -> action -> action
+  val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
 
@@ -51,14 +52,22 @@
 
 structure Actions = TheoryDataFun
 (
-  type T = action Symtab.table
-  val empty = Symtab.empty
+  type T = action list
+  val empty = []
   val copy = I
   val extend = I
-  fun merge _ = Symtab.merge (K true)
+  fun merge _ = Library.merge (K true)
 )
 
-val register = Actions.map o Symtab.update_new
+
+fun app_with f g x = (g x; ())
+  handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
+
+fun catch tag f (st as {log, ...}) =
+  let fun log_exn e = log (tag ^ "exception:\n" ^ General.exnMessage e)
+  in app_with log_exn f st end
+
+val register = Actions.map o cons
 
 local
 
@@ -70,20 +79,11 @@
 
 fun log_sep thy = log thy "------------------"
 
-fun log_exn thy name (exn : exn) = log thy ("Unhandled exception in action " ^
-  quote name ^ ":\n" ^ PolyML.makestring exn)
-
-fun try_with f g x = SOME (g x)
-  handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; NONE)
-
-fun capture_exns thy name f x = (try_with (log_exn thy name) f x; log_sep thy)
-
 fun apply_actions thy info (pre, post, time) actions =
   let
-    fun apply (name, action) =
-      {pre=pre, post=post, timeout=time, log=log thy}
-      |> capture_exns thy name action
-  in (log thy info; log_sep thy; List.app apply actions) end
+    fun apply f = f {pre=pre, post=post, timeout=time, log=log thy}
+    fun run f = (apply f; log_sep thy)
+  in (log thy info; log_sep thy; List.app run actions) end
 
 fun in_range _ _ NONE = true
   | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
@@ -105,9 +105,7 @@
     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 (apply_actions thy info st)
+    only_within_range thy pos (apply_actions thy info st) (Actions.get thy)
   end
 
 end
diff -r 43d2ac4aa2de -r e7c0d3c0494a src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -11,6 +11,6 @@
   else ()
   handle TimeLimit.TimeOut => log "arith: time out"
 
-fun invoke _ = Mirabelle.register ("arith", arith_action)
+fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
 
 end
diff -r 43d2ac4aa2de -r e7c0d3c0494a src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -22,6 +22,6 @@
   end
   handle TimeLimit.TimeOut => log "metis: time out"
 
-fun invoke _ = Mirabelle.register ("metis", metis_action)
+fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
 
 end
diff -r 43d2ac4aa2de -r e7c0d3c0494a src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -16,6 +16,7 @@
   end
   handle TimeLimit.TimeOut => log "quickcheck: time out"
 
-fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
+fun invoke args =
+  Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
 
 end
diff -r 43d2ac4aa2de -r e7c0d3c0494a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 03 22:47:31 2009 +0200
@@ -30,6 +30,9 @@
 val metisK = "metis"
 val full_typesK = "full_types"
 
+val sh_tag = "sledgehammer: "
+val metis_tag = "metis (sledgehammer): "
+
 
 local
 
@@ -57,7 +60,7 @@
 
 in
 
-fun run_sledgehammer (args, st, timeout, log) =
+fun run_sledgehammer args thm_names {pre=st, timeout, log, ...} =
   let
     val prover_name =
       AList.lookup (op =) args proverK
@@ -66,10 +69,10 @@
     val (msg, result) = safe init done (run prover_name timeout st) dir
     val _ =
       if is_some result
-      then log ("sledgehammer: succeeded (" ^ string_of_int (fst (the result)) ^
+      then log (sh_tag ^ "succeeded (" ^ string_of_int (fst (the result)) ^
         ") [" ^ prover_name ^ "]:\n" ^ msg)
-      else log ("sledgehammer: failed: " ^ msg)
-  in Option.map snd result end
+      else log (sh_tag ^ "failed: " ^ msg)
+  in change thm_names (K (Option.map snd result)) end
 
 end
 
@@ -77,7 +80,7 @@
 fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
   | with_time false t = "failed (" ^ string_of_int t ^ ")"
 
-fun run_metis (args, st, timeout, log) thm_names =
+fun run_metis args thm_names {pre=st, timeout, log, ...} =
   let
     fun get_thms ctxt = maps (thms_of_name ctxt)
     fun metis thms ctxt = MetisTools.metis_tac ctxt thms
@@ -86,26 +89,29 @@
       uncurry with_time (Mirabelle.cpu_time apply_metis thms)
       handle TimeLimit.TimeOut => "time out"
            | ERROR msg => "error: " ^ msg
-    fun log_metis s = log ("metis (sledgehammer): " ^ s)
+    fun log_metis s = log (metis_tag ^ s)
   in
     if not (AList.defined (op =) args metisK) then ()
-    else if is_none thm_names then ()
+    else if is_none (!thm_names) then ()
     else
       log "-----"
-      |> K (these thm_names)
+      |> K (these (!thm_names))
       |> get_thms (Proof.context_of st)
       |> timed_metis
       |> log_metis
   end
 
 
-fun sledgehammer_action args {pre, timeout, log, ...} =
-  run_sledgehammer (args, pre, timeout, log)
-  |> run_metis (args, pre, timeout, log)
+fun sledgehammer_action args (st as {log, ...}) =
+  let
+    val thm_names = ref (NONE : string list option)
+    val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) st
+    val _ = Mirabelle.catch metis_tag (run_metis args thm_names) st
+  in () end
 
 fun invoke args =
-  let val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
-  in Mirabelle.register ("sledgehammer", sledgehammer_action args) end
+  let
+    val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
+  in Mirabelle.register (sledgehammer_action args) end
 
 end
-