# HG changeset patch
# User wenzelm
# Date 1025617444 -7200
# Node ID b62514fcbcab5ca977b7f1886b770cfe26d7ba8d
# Parent  ca2511db144dbe7e01768700e10aa3eef0b2545f
print_thms_containing: index variables, refer to local facts as well;

diff -r ca2511db144d -r b62514fcbcab src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 02 15:41:02 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 02 15:44:04 2002 +0200
@@ -114,6 +114,7 @@
   val pretty_sort: context -> sort -> Pretty.T
   val pretty_thm: context -> thm -> Pretty.T
   val pretty_thms: context -> thm list -> Pretty.T
+  val pretty_fact: context -> string * thm list -> Pretty.T
   val string_of_term: context -> term -> string
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
@@ -124,6 +125,7 @@
   val prems_limit: int ref
   val pretty_asms: context -> Pretty.T list
   val pretty_context: context -> Pretty.T list
+  val print_thms_containing: context -> string list -> unit
   val setup: (theory -> theory) list
 end;
 
@@ -155,7 +157,8 @@
         (string * thm list) list) *
       (string * string) list,                                 (*fixes: !!x. _*)
     binds: (term * typ) option Vartab.table,                  (*term bindings*)
-    thms: bool * NameSpace.T * thm list option Symtab.table,  (*local thms*)
+    thms: bool * NameSpace.T * thm list option Symtab.table
+      * FactIndex.T,                                          (*local thms*)
     cases: (string * RuleCases.T) list,                       (*local contexts*)
     defs:
       typ Vartab.table *                                      (*type constraints*)
@@ -180,6 +183,8 @@
 fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
 val fixed_names_of = map #2 o fixes_of;
 fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
+fun is_known (ctxt as Context {defs = (types, _, _, _), ...}) x =
+  is_some (Vartab.lookup (types, (x, ~1))) orelse is_fixed ctxt x;
 fun type_occs (Context {defs = (_, _, _, tab), ...}) = tab;
 
 fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms;
@@ -277,7 +282,8 @@
 fun init thy =
   let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
     make_context (thy, (Theory.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
-      (false, NameSpace.empty, Symtab.empty), [], (Vartab.empty, Vartab.empty, [], Symtab.empty))
+      (false, NameSpace.empty, Symtab.empty, FactIndex.empty), [],
+      (Vartab.empty, Vartab.empty, [], Symtab.empty))
   end;
 
 
@@ -657,6 +663,12 @@
 fun pretty_thms ctxt [th] = pretty_thm ctxt th
   | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
 
+fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
+  | pretty_fact ctxt (a, [th]) =
+      Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
+  | pretty_fact ctxt (a, ths) =
+      Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
+
 
 
 (** Hindley-Milner polymorphism **)
@@ -909,7 +921,7 @@
 (* get_thm(s) *)
 
 (*beware of proper order of evaluation!*)
-fun retrieve_thms f g (ctxt as Context {thy, thms = (_, space, tab), ...}) =
+fun retrieve_thms f g (ctxt as Context {thy, thms = (_, space, tab, _), ...}) =
   let
     val sg_ref = Sign.self_ref (Theory.sign_of thy);
     val get_from_thy = f thy;
@@ -928,10 +940,11 @@
 
 (* qualified names *)
 
-fun cond_extern (Context {thms = (_, space, _), ...}) = NameSpace.cond_extern space;
+fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space;
 
-fun set_qual q = map_context (fn (thy, syntax, data, asms, binds, (_, space, tab), cases, defs) =>
-  (thy, syntax, data, asms, binds, (q, space, tab), cases, defs));
+fun set_qual q = map_context (fn (thy, syntax, data, asms, binds,
+    (_, space, tab, index), cases, defs) =>
+  (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs));
 
 fun qualified_result f (ctxt as Context {thms, ...}) =
   ctxt |> set_qual true |> f |>> set_qual (#1 thms);
@@ -941,11 +954,12 @@
 
 fun put_thms ("", _) ctxt = ctxt
   | put_thms (name, ths) ctxt = ctxt |> map_context
-      (fn (thy, syntax, data, asms, binds, (q, space, tab), cases, defs) =>
+      (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
         if not q andalso NameSpace.is_qualified name then
           raise CONTEXT ("Attempt to declare qualified name " ^ quote name, ctxt)
         else (thy, syntax, data, asms, binds, (q, NameSpace.extend (space, [name]),
-          Symtab.update ((name, Some ths), tab)), cases, defs));
+          Symtab.update ((name, Some ths), tab),
+            FactIndex.add (is_known ctxt) (index, (name, ths))), cases, defs));
 
 fun put_thm (name, th) = put_thms (name, [th]);
 
@@ -956,8 +970,9 @@
 (* reset_thms *)
 
 fun reset_thms name =
-  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab), cases, defs) =>
-    (thy, syntax, data, asms, binds, (q, space, Symtab.update ((name, None), tab)), cases, defs));
+  map_context (fn (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs) =>
+    (thy, syntax, data, asms, binds, (q, space, Symtab.update ((name, None), tab), index),
+      cases, defs));
 
 
 (* have_thmss *)
@@ -1236,7 +1251,7 @@
 
 (* local theorems *)
 
-fun pretty_lthms (ctxt as Context {thms = (_, space, tab), ...}) =
+fun pretty_lthms (ctxt as Context {thms = (_, space, tab, _), ...}) =
   pretty_items (pretty_thm ctxt) "facts:"
     (mapfilter smash_option (NameSpace.cond_extern_table space tab));
 
@@ -1352,6 +1367,47 @@
   end;
 
 
+(* print_thms_containing *)
+
+fun lthms_containing (ctxt as Context {thms = (_, _, _, index), ...}) idx =
+  let
+    fun valid (name, ths) =
+      (case try (transform_error (fn () => get_thms ctxt name)) () of
+        None => false
+      | Some ths' => Library.equal_lists Thm.eq_thm (ths, ths'));
+  in gen_distinct eq_fst (filter valid (FactIndex.find idx index)) end;
+
+
+fun print_thms_containing ctxt ss =
+  let
+    val prt_term = pretty_term ctxt;
+    val prt_fact = pretty_fact ctxt o apsnd (map (#1 o Drule.freeze_thaw));
+    fun prt_consts [] = []
+      | prt_consts cs = [Pretty.block (Pretty.breaks (Pretty.str "constants" ::
+          map (Pretty.quote o prt_term o Syntax.const) cs))];
+    fun prt_frees [] = []
+      | prt_frees xs = [Pretty.block (Pretty.breaks (Pretty.str "variables" ::
+          map (Pretty.quote o prt_term o Syntax.free) xs))];
+
+    val (cs, xs) = foldl (FactIndex.index_term (is_known ctxt))
+      (([], []), map (read_term ctxt) ss);
+    val empty_idx = Library.null cs andalso Library.null xs;
+
+    val header =
+      if empty_idx then []
+      else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" ::
+        separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @
+          [Pretty.str ":", Pretty.fbrk])]
+    val globals = PureThy.thms_containing (theory_of ctxt) (cs, xs);
+    val locals = lthms_containing ctxt (cs, xs);
+  in
+    if empty_idx andalso not (Library.null ss) then
+      warning "thms_containing: no consts/frees in specification"
+    else (header @ map prt_fact (sort_wrt #1 (globals @ locals)))
+      |> Pretty.chunks |> Pretty.writeln
+  end;
+
+
 
 (** theory setup **)