--- 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
--- 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
--- 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 =