# HG changeset patch
# User boehmes
# Date 1251703730 -7200
# Node ID a1a5589207adab75249798772864a529aa7570f1
# Parent  6084b36a195f993b84ee79c57bedc38be454b3c9
Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names

diff -r 6084b36a195f -r a1a5589207ad src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Aug 29 22:01:55 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 31 09:28:50 2009 +0200
@@ -5,31 +5,18 @@
 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 thms_of_name ctxt name =
+  let
+    val lex = OuterKeyword.get_lexicons
+    val get = maps (ProofContext.get_fact ctxt o fst)
+  in
+    Source.of_string name
+    |> Symbol.source {do_recover=false}
+    |> OuterLex.source {do_recover=SOME false} lex Position.start
+    |> OuterLex.source_proper
+    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
+    |> Source.exhaust
+  end
 
 fun sledgehammer_action args {pre=st, ...} =
   let
@@ -52,12 +39,13 @@
            | 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"
+    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 try (Mirabelle.can_apply (metis thms)) st = SOME true
+      then "success"
+      else "failure")
+    val msg = apply_metis (get_thms (Proof.context_of st) (these thm_names))
   in
     if success
     then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
diff -r 6084b36a195f -r a1a5589207ad src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Sat Aug 29 22:01:55 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 31 09:28:50 2009 +0200
@@ -26,10 +26,10 @@
 my $thy_file = $ARGV[1];
 my $start_line = "0";
 my $end_line = "~1";
-if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) { # FIXME
-  my $thy_file = $1;
-  my $start_line = $2;
-  my $end_line = $3;
+if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
+  $thy_file = $1;
+  $start_line = $2;
+  $end_line = $3;
 }
 my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
 my $new_thy_name = $thy_name . "_Mirabelle";