--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thm_database.ML Mon May 29 13:55:06 1995 +0200
@@ -0,0 +1,82 @@
+(* 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;