# HG changeset patch
# User blanchet
# Date 1283352371 -7200
# Node ID 6905ba37376c7f5953990d8433cf44eabc0a590c
# Parent  54b81258c831a61e78a75f8a39ec9f936957dbd1
generalize theorem argument parsing syntax

diff -r 54b81258c831 -r 6905ba37376c src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 16:11:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 16:46:11 2010 +0200
@@ -8,8 +8,8 @@
   datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
   type relevance_override =
-    {add: Facts.ref list,
-     del: Facts.ref list,
+    {add: (Facts.ref * Attrib.src list) list,
+     del: (Facts.ref * Attrib.src list) list,
      only: bool}
 
   val trace : bool Unsynchronized.ref
@@ -31,8 +31,8 @@
   val threshold_divisor : real Unsynchronized.ref
   val ridiculous_threshold : real Unsynchronized.ref
   val name_thm_pairs_from_ref :
-    Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-    -> ((string * locality) * thm) list
+    Proof.context -> unit Symtab.table -> thm list
+    -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val relevant_facts :
     Proof.context -> bool -> real * real -> int -> bool -> relevance_override
     -> thm list -> term list -> term -> ((string * locality) * thm) list
@@ -54,8 +54,8 @@
 datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
 
 type relevance_override =
-  {add: Facts.ref list,
-   del: Facts.ref list,
+  {add: (Facts.ref * Attrib.src list) list,
+   del: (Facts.ref * Attrib.src list) list,
    only: bool}
 
 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
@@ -67,10 +67,18 @@
   (name |> Symtab.defined reserved name ? quote) ^
   (if multi then "(" ^ Int.toString j ^ ")" else "")
 
-fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
+fun name_thm_pairs_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
   let
-    val ths = ProofContext.get_fact ctxt xref
-    val name = Facts.string_of_ref xref
+    val ths = Attrib.eval_thms ctxt [xthm]
+    val bracket =
+      implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
+                               ^ "]") args)
+    val space_bracket = if bracket = "" then "" else " " ^ bracket
+    val name =
+      case xref of
+        Facts.Fact s => "`" ^ s ^ "`" ^ space_bracket
+      | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
+      | _ => Facts.string_of_ref xref ^ space_bracket
     val multi = length ths > 1
   in
     (ths, (1, []))
@@ -437,8 +445,8 @@
       pconsts_in_terms thy false (SOME false) goal_ts
       |> fold (if_empty_replace_with_locality thy axioms)
               [Chained, Assum, Local]
-    val add_thms = maps (ProofContext.get_fact ctxt) add
-    val del_thms = maps (ProofContext.get_fact ctxt) del
+    val add_thms = Attrib.eval_thms ctxt add
+    val del_thms = Attrib.eval_thms ctxt del
     fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
       let
         fun game_over rejects =
@@ -788,7 +796,7 @@
   let
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
                           1.0 / Real.fromInt (max_relevant + 1))
-    val add_thms = maps (ProofContext.get_fact ctxt) add
+    val add_thms = Attrib.eval_thms ctxt add
     val reserved = reserved_isar_keyword_table ()
     val axioms =
       (if only then
diff -r 54b81258c831 -r 6905ba37376c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 01 16:11:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 01 16:46:11 2010 +0200
@@ -272,10 +272,7 @@
 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
 val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
-                            (Parse.xname -- Scan.option Attrib.thm_sel)
-                >> (fn (name, interval) =>
-                       Facts.Named ((name, Position.none), interval)))
+  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
 val parse_relevance_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs
diff -r 54b81258c831 -r 6905ba37376c src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 16:11:48 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Sep 01 16:46:11 2010 +0200
@@ -13,7 +13,8 @@
   val minimize_theorems :
     params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
     -> ((string * locality) * thm list) list option * string
-  val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
+  val run_minimize :
+    params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
 end;
 
 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =