src/Pure/Thy/thm_database.ML

changed error message in thms_containing

(*  Title:      Pure/Thy/thm_database.ML
    ID:         $Id$
    Author:     Carsten Clasohm
    Copyright   1995 TU Muenchen
*)

signature THMDB =
sig
  val thm_db: (int * (string * thm)) list Symtab.table ref
  val thm_num: int ref
  val store_thm_db: string * thm -> thm
  val thms_containing: string list -> (string * thm) list
end;


functor ThmdbFUN(val ignore: string list): THMDB =
               (*ignore: constants that must not be used for theorem indexing*)
struct

(*Symtab which associates a constant with a list of theorems that contain the
  constant (theorems are represented as numbers)*)
val thm_db =
      ref (Symtab.make ([] : (string * ((int * (string * thm)) list)) list));
val thm_num = ref 0;                                 (*number of next theorem*)

(*list all relevant constants a theorem contains*)
fun list_consts t =
  let val {prop, hyps, ...} = rep_thm t;

      fun consts (Const (c, _)) = if c mem ignore then [] else [c]
        | consts (Free _) = []
        | consts (Var _) = []
        | consts (Bound _) = []
        | consts (Abs (_, _, t)) = consts t
        | consts (t1$t2) = (consts t1) union (consts t2);
  in distinct (flat (map consts (prop :: hyps))) end;

(*store a theorem in database*)
fun store_thm_db (thm as (name, t)) =
  let val consts = list_consts t;

      val tagged_thm = (!thm_num + 1, thm);

      fun update_db [] = ()
        | update_db (c :: cs) =
            let val old_thms = Symtab.lookup_multi (!thm_db, c);
            in thm_db := Symtab.update ((c, tagged_thm :: old_thms), !thm_db);
               update_db cs
            end;
  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
                                  " cannot be stored in ThmDB because it \
                                  \contains no constants.")
                    else ();
     update_db consts;
     thm_num := !thm_num+1;
     t
  end;

(*intersection of two descending theorem lists*)
infix desc_inter;
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
  | xs desc_inter [] = []
  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
      if xi = yi then x :: (xs desc_inter ys)
      else if xi > yi then xs desc_inter yss
      else xss desc_inter ys;

(*get all theorems from database that contain a list of constants*)
fun thms_containing constants =
  let fun collect [] _ result = map snd result
        | collect (c :: cs) first result =
            let val new_thms = Symtab.lookup_multi (!thm_db, c);
            in collect cs false (if first then new_thms
                                          else (result desc_inter new_thms))
            end;

      val look_for = constants \\ ignore;
  in if null look_for then
       error ("Only ignored constants specified for theorem database search:\n"
              ^ commas (map quote ignored))
     else ();
     collect look_for true [] end;
end;