--- a/src/Pure/Isar/attrib.ML Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Aug 16 12:53:47 2019 +0100
@@ -282,7 +282,7 @@
val atts = map (attribute_generic context) srcs;
val (ths', context') =
fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context;
- in (context', pick (name, Facts.pos_of_ref thmref) ths') end)
+ in (context', pick (name, Facts.ref_pos thmref) ths') end)
end);
in
--- a/src/Pure/Isar/generic_target.ML Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/Isar/generic_target.ML Fri Aug 16 12:53:47 2019 +0100
@@ -306,6 +306,8 @@
fun bind_name lthy b =
(Local_Theory.full_name lthy b, Binding.default_pos_of b);
+fun map_facts f = map (apsnd (map (apfst (map f))));
+
in
fun notes target_notes kind facts lthy =
@@ -313,9 +315,9 @@
val facts' = facts
|> map (fn (a, bs) =>
(a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs))
- |> Global_Theory.map_facts (import_export_proof lthy);
- val local_facts = Global_Theory.map_facts #1 facts';
- val global_facts = Global_Theory.map_facts #2 facts';
+ |> map_facts (import_export_proof lthy);
+ val local_facts = map_facts #1 facts';
+ val global_facts = map_facts #2 facts';
in
lthy
|> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
--- a/src/Pure/Tools/find_theorems.ML Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/Tools/find_theorems.ML Fri Aug 16 12:53:47 2019 +0100
@@ -125,7 +125,7 @@
(* filter_name *)
fun filter_name str_pat (thmref, _) =
- if match_string str_pat (Facts.name_of_ref thmref)
+ if match_string str_pat (Facts.ref_name thmref)
then SOME (0, 0, 0) else NONE;
--- a/src/Pure/facts.ML Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/facts.ML Fri Aug 16 12:53:47 2019 +0100
@@ -12,11 +12,11 @@
Named of (string * Position.T) * interval list option |
Fact of string
val named: string -> ref
+ val ref_name: ref -> string
+ val ref_pos: ref -> Position.T
+ val map_ref_name: (string -> string) -> ref -> ref
val string_of_selection: interval list option -> string
val string_of_ref: ref -> string
- val name_of_ref: ref -> string
- val pos_of_ref: ref -> Position.T
- val map_name_of_ref: (string -> string) -> ref -> ref
val select: ref -> thm list -> thm list
val selections: string * thm list -> (ref * thm) list
type T
@@ -44,6 +44,10 @@
val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
val del: string -> T -> T
val hide: bool -> string -> T -> T
+ type thm_name = string * int
+ val thm_name_ord: thm_name * thm_name -> order
+ val single_thm_name: string -> thm_name
+ val get_thm: Context.generic -> T -> thm_name * Position.T -> thm
end;
structure Facts: FACTS =
@@ -51,10 +55,18 @@
(** fact references **)
-fun the_single _ [th] : thm = th
- | the_single (name, pos) ths =
- error ("Expected singleton fact " ^ quote name ^
- " (length " ^ string_of_int (length ths) ^ ")" ^ Position.here pos);
+fun length_msg (thms: thm list) pos =
+ " (length " ^ string_of_int (length thms) ^ ")" ^ Position.here pos;
+
+fun err_single (name, pos) thms =
+ error ("Expected singleton fact " ^ quote name ^ length_msg thms pos);
+
+fun err_selection (name, pos) i thms =
+ error ("Bad fact selection " ^ quote (name ^ enclose "(" ")" (string_of_int i)) ^
+ length_msg thms pos);
+
+fun the_single _ [thm] = thm
+ | the_single name_pos thms = err_single name_pos thms;
(* datatype interval *)
@@ -85,14 +97,14 @@
fun named name = Named ((name, Position.none), NONE);
-fun name_of_ref (Named ((name, _), _)) = name
- | name_of_ref (Fact _) = raise Fail "Illegal literal fact";
+fun ref_name (Named ((name, _), _)) = name
+ | ref_name (Fact _) = raise Fail "Illegal literal fact";
-fun pos_of_ref (Named ((_, pos), _)) = pos
- | pos_of_ref (Fact _) = Position.none;
+fun ref_pos (Named ((_, pos), _)) = pos
+ | ref_pos (Fact _) = Position.none;
-fun map_name_of_ref f (Named ((name, pos), is)) = Named ((f name, pos), is)
- | map_name_of_ref _ r = r;
+fun map_ref_name f (Named ((name, pos), is)) = Named ((f name, pos), is)
+ | map_ref_name _ r = r;
fun string_of_selection NONE = ""
| string_of_selection (SOME is) = enclose "(" ")" (commas (map string_of_interval is));
@@ -108,12 +120,10 @@
| select (Named ((name, pos), SOME ivs)) ths =
let
val n = length ths;
- fun err msg =
- error (msg ^ " for fact " ^ quote name ^ " (length " ^ string_of_int n ^ ")" ^
- Position.here pos);
+ fun err msg = error (msg ^ " for fact " ^ quote name ^ length_msg ths pos);
fun sel i =
- if i < 1 orelse i > n then err ("Bad subscript " ^ string_of_int i)
- else nth ths (i - 1);
+ if i > 0 andalso i <= n then nth ths (i - 1)
+ else err_selection (name, pos) i ths;
val is = maps (interval n) ivs handle Fail msg => err msg;
in map sel is end;
@@ -288,4 +298,27 @@
fun hide fully name (Facts {facts, props}) =
make_facts (Name_Space.hide_table fully name facts) props;
+
+
+(** get individual theorems **)
+
+type thm_name = string * int;
+val thm_name_ord = prod_ord string_ord int_ord;
+
+fun single_thm_name name : thm_name = (name, 0);
+
+fun get_thm context facts ((name, i), pos) =
+ let
+ fun print_name () =
+ markup_extern (Context.proof_of context) facts name |-> Markup.markup;
+ in
+ (case (lookup context facts name, i) of
+ (NONE, _) => error ("Undefined fact " ^ quote (print_name ()) ^ Position.here pos)
+ | (SOME {thms = [thm], ...}, 0) => thm
+ | (SOME {thms, ...}, 0) => err_single (print_name (), pos) thms
+ | (SOME {thms, ...}, _) =>
+ if i > 0 andalso i <= length thms then nth thms (i - 1)
+ else err_selection (print_name (), pos) i thms)
+ end;
+
end;
--- a/src/Pure/global_theory.ML Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/global_theory.ML Fri Aug 16 12:53:47 2019 +0100
@@ -16,7 +16,6 @@
val get_thm: theory -> xstring -> thm
val transfer_theories: theory -> thm -> thm
val all_thms_of: theory -> bool -> (string * thm) list
- val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
val burrow_facts: ('a list -> 'b list) ->
('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
@@ -63,15 +62,16 @@
);
val facts_of = Data.get;
+fun map_facts f = Data.map f;
fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
val intern_fact = Facts.intern o facts_of;
val defined_fact = Facts.defined o facts_of;
fun alias_fact binding name thy =
- Data.map (Facts.alias (Sign.naming_of thy) binding name) thy;
+ map_facts (Facts.alias (Sign.naming_of thy) binding name) thy;
-fun hide_fact fully name = Data.map (Facts.hide fully name);
+fun hide_fact fully name = map_facts (Facts.hide fully name);
(* retrieve theorems *)
@@ -106,7 +106,6 @@
(* fact specifications *)
-fun map_facts f = map (apsnd (map (apfst (map f))));
fun burrow_fact f = split_list #>> burrow f #> op ~~;
fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~;
@@ -128,7 +127,7 @@
No_Name_Flags => thm
| Name_Flags {pre, official} =>
thm
- |> (official andalso (not pre orelse Thm.derivation_name thm = "")) ?
+ |> (official andalso (not pre orelse Thm.raw_derivation_name thm = "")) ?
Thm.name_derivation (name, pos)
|> (name <> "" andalso (not pre orelse not (Thm.has_name_hint thm))) ?
Thm.put_name_hint name));
@@ -176,7 +175,7 @@
end);
val arg = (b, Lazy.map_finished (tap check) fact);
in
- thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
+ thy |> map_facts (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2)
end;
fun check_thms_lazy (thms: thm list lazy) =
@@ -231,8 +230,8 @@
(* dynamic theorems *)
fun add_thms_dynamic' context arg thy =
- let val (name, facts') = Facts.add_dynamic context arg (Data.get thy)
- in (name, Data.put facts' thy) end;
+ let val (name, facts') = Facts.add_dynamic context arg (facts_of thy)
+ in (name, map_facts (K facts') thy) end;
fun add_thms_dynamic arg thy =
add_thms_dynamic' (Context.Theory thy) arg thy |> snd;
--- a/src/Pure/thm.ML Fri Aug 16 12:53:36 2019 +0100
+++ b/src/Pure/thm.ML Fri Aug 16 12:53:47 2019 +0100
@@ -106,6 +106,7 @@
val future: thm future -> cterm -> thm
val derivation_closed: thm -> bool
val derivation_name: thm -> string
+ val raw_derivation_name: thm -> string
val name_derivation: string * Position.T -> thm -> thm
val close_derivation: Position.T -> thm -> thm
val trim_context: thm -> thm
@@ -996,9 +997,13 @@
Proofterm.compact_proof (Proofterm.proof_of body);
(*non-deterministic, depends on unknown promises*)
-fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
+fun raw_derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
+(*deterministic name of finished proof*)
+fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
+ Proofterm.get_name shyps hyps prop (proof_of thm);
+
fun name_derivation name_pos =
solve_constraints #> (fn thm as Thm (der, args) =>
let