# HG changeset patch
# User boehmes
# Date 1251575913 -7200
# Node ID d84edd022efe1a9641afbbc00a9e848b85e329d0
# Parent  8f0dc876fb1b76aed35ea7acc01a4d7f2d6cab25
apply metis with found theorems in case sledgehammer was successful

diff -r 8f0dc876fb1b -r d84edd022efe src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 21:57:06 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 21:58:33 2009 +0200
@@ -5,6 +5,32 @@
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
 struct
 
+local
+val valid = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
+  member (op =) (explode "_.")
+val name = Scan.many1 valid >> (rpair Position.none o implode)
+
+val digit = (fn
+  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
+  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
+  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
+fun join d n = 10 * n + d
+val number = Scan.repeat1 (Scan.some digit) >> (fn ds => fold join ds 0)
+val interval = Scan.option (Scan.$$ "(" |-- number --| Scan.$$ ")" >>
+  (single o Facts.Single))
+
+val fact_ref = name -- interval >> Facts.Named
+
+in
+
+fun thm_of_name ctxt s =
+  (case try (Scan.read Symbol.stopper fact_ref) (explode s) of
+    SOME (SOME r) => ProofContext.get_fact ctxt r
+  | _ => [])
+
+end
+
+
 fun sledgehammer_action args {pre=st, ...} =
   let
     val prover_name =
@@ -16,16 +42,25 @@
     val prover = the (AtpManager.get_prover prover_name thy)
     val timeout = AtpManager.get_timeout () 
 
-    val (success, message) =
+    (* run sledgehammer *)
+    val (success, message, thm_names) =
       let
-        val (success, message, _, _, _) =
+        val (success, (message, thm_names), _, _, _) =
           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 (success, message, SOME thm_names) end
+      handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
+           | ERROR msg => (false, "error: " ^ msg, NONE)
+
+    (* try metis *)
+    val thms = maps (thm_of_name (Proof.context_of st)) (these thm_names)
+    fun metis ctxt = MetisTools.metis_tac ctxt thms
+    val msg = if not (AList.defined (op =) args "metis") then "" else
+      if try (Mirabelle.can_apply metis) st = SOME true
+        then "\nMETIS: success"
+        else "\nMETIS: failure"
   in
     if success
-    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")")
+    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
     else NONE
   end