(*  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 ignored = constants inter ignore;

  in if null ignored then () else

       error ("The following constant(s) must not be used for searching the \

              \theorem database:\n  " ^ commas (map quote ignored));

     collect constants true [] end;

end;