src/Pure/Thy/thm_database.ML
author clasohm
Mon May 29 13:55:06 1995 +0200 (1995-05-29)
changeset 1132 dfb29abcf3c2
child 1134 5e9775c196e8
permissions -rw-r--r--
added theorem database which contains axioms and theorems indexed by the
constants they contain
clasohm@1132
     1
(*  Title:      Pure/Thy/thm_database.ML
clasohm@1132
     2
    ID:         $Id$
clasohm@1132
     3
    Author:     Carsten Clasohm
clasohm@1132
     4
    Copyright   1995 TU Muenchen
clasohm@1132
     5
*)
clasohm@1132
     6
clasohm@1132
     7
signature THMDB =
clasohm@1132
     8
sig
clasohm@1132
     9
  val thm_db: (int * (string * thm)) list Symtab.table ref
clasohm@1132
    10
  val thm_num: int ref
clasohm@1132
    11
  val store_thm_db: string * thm -> thm
clasohm@1132
    12
  val thms_containing: string list -> (string * thm) list
clasohm@1132
    13
end;
clasohm@1132
    14
clasohm@1132
    15
clasohm@1132
    16
functor ThmdbFUN(val ignore: string list): THMDB =
clasohm@1132
    17
               (*ignore: constants that must not be used for theorem indexing*)
clasohm@1132
    18
struct
clasohm@1132
    19
clasohm@1132
    20
(*Symtab which associates a constant with a list of theorems that contain the
clasohm@1132
    21
  constant (theorems are represented as numbers)*)
clasohm@1132
    22
val thm_db =
clasohm@1132
    23
      ref (Symtab.make ([] : (string * ((int * (string * thm)) list)) list));
clasohm@1132
    24
val thm_num = ref 0;                                 (*number of next theorem*)
clasohm@1132
    25
clasohm@1132
    26
(*list all relevant constants a theorem contains*)
clasohm@1132
    27
fun list_consts t =
clasohm@1132
    28
  let val {prop, hyps, ...} = rep_thm t;
clasohm@1132
    29
clasohm@1132
    30
      fun consts (Const (c, _)) = if c mem ignore then [] else [c]
clasohm@1132
    31
        | consts (Free _) = []
clasohm@1132
    32
        | consts (Var _) = []
clasohm@1132
    33
        | consts (Bound _) = []
clasohm@1132
    34
        | consts (Abs (_, _, t)) = consts t
clasohm@1132
    35
        | consts (t1$t2) = (consts t1) union (consts t2);
clasohm@1132
    36
  in distinct (flat (map consts (prop :: hyps))) end;
clasohm@1132
    37
clasohm@1132
    38
(*store a theorem in database*)
clasohm@1132
    39
fun store_thm_db (thm as (name, t)) =
clasohm@1132
    40
  let val consts = list_consts t;
clasohm@1132
    41
clasohm@1132
    42
      val tagged_thm = (!thm_num + 1, thm);
clasohm@1132
    43
clasohm@1132
    44
      fun update_db [] = ()
clasohm@1132
    45
        | update_db (c :: cs) =
clasohm@1132
    46
            let val old_thms = Symtab.lookup_multi (!thm_db, c);
clasohm@1132
    47
            in thm_db := Symtab.update ((c, tagged_thm :: old_thms), !thm_db);
clasohm@1132
    48
               update_db cs
clasohm@1132
    49
            end;
clasohm@1132
    50
  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
clasohm@1132
    51
                                  " cannot be stored in ThmDB because it \
clasohm@1132
    52
                                  \contains no constants.")
clasohm@1132
    53
                    else ();
clasohm@1132
    54
     update_db consts;
clasohm@1132
    55
     thm_num := !thm_num+1;
clasohm@1132
    56
     t
clasohm@1132
    57
  end;
clasohm@1132
    58
clasohm@1132
    59
(*intersection of two descending theorem lists*)
clasohm@1132
    60
infix desc_inter;
clasohm@1132
    61
fun ([] : (int*'a) list) desc_inter (ys : (int*'a) list) = []
clasohm@1132
    62
  | xs desc_inter [] = []
clasohm@1132
    63
  | (xss as ((x as (xi,_)) :: xs)) desc_inter (yss as ((yi,_) :: ys)) =
clasohm@1132
    64
      if xi = yi then x :: (xs desc_inter ys)
clasohm@1132
    65
      else if xi > yi then xs desc_inter yss
clasohm@1132
    66
      else xss desc_inter ys;
clasohm@1132
    67
clasohm@1132
    68
(*get all theorems from database that contain a list of constants*)
clasohm@1132
    69
fun thms_containing constants =
clasohm@1132
    70
  let fun collect [] _ result = map snd result
clasohm@1132
    71
        | collect (c :: cs) first result =
clasohm@1132
    72
            let val new_thms = Symtab.lookup_multi (!thm_db, c);
clasohm@1132
    73
            in collect cs false (if first then new_thms
clasohm@1132
    74
                                          else (result desc_inter new_thms))
clasohm@1132
    75
            end;
clasohm@1132
    76
clasohm@1132
    77
      val ignored = constants inter ignore;
clasohm@1132
    78
  in if null ignored then () else
clasohm@1132
    79
       error ("The following constant(s) must not be used for searching the \
clasohm@1132
    80
              \theorem database:\n  " ^ commas (map quote ignored));
clasohm@1132
    81
     collect constants true [] end;
clasohm@1132
    82
end;