# HG changeset patch # User clasohm # Date 801748506 -7200 # Node ID dfb29abcf3c26f67537f24b0c1d1e714814ccc51 # Parent 8e81ad0c6f12833b73dc07c461dc38eede5acfc7 added theorem database which contains axioms and theorems indexed by the constants they contain diff -r 8e81ad0c6f12 -r dfb29abcf3c2 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Sun May 28 17:18:06 1995 +0200 +++ b/src/Pure/Thy/ROOT.ML Mon May 29 13:55:06 1995 +0200 @@ -13,22 +13,21 @@ structure ThyParse = ThyParseFun(structure Symtab = Symtab and ThyScan = ThyScan); -(* hide functors; saves space in PolyML *) -functor ThyScanFun() = struct end; -functor ThyParseFun() = struct end; - use "thy_syn.ML"; +use "thm_database.ML"; use "thy_read.ML"; structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []); -structure Readthy = ReadthyFUN(structure ThySyn = ThySyn); -open Readthy; -(* Do not hide ThySynFun and ReadthyFUN; they are still used *) +(* hide functors; saves space in PolyML *) +functor ThyScanFun() = struct end; +functor ThyParseFun() = struct end; +functor ThySynFun() = struct end; fun init_thy_reader () = use_string - ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);", - "Readthy.loaded_thys := ! loaded_thys;", - "open Readthy;"]; - + ["structure ThmDB = \ + \ThmdbFUN(val ignore = [\"Trueprop\",\"All\",\"==>\",\"==\"]);", + "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \ + \and ThmDB = ThmDB);", + "open Readthy ThmDB;"]; diff -r 8e81ad0c6f12 -r dfb29abcf3c2 src/Pure/Thy/thm_database.ML --- /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; diff -r 8e81ad0c6f12 -r dfb29abcf3c2 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Sun May 28 17:18:06 1995 +0200 +++ b/src/Pure/Thy/thy_read.ML Mon May 29 13:55:06 1995 +0200 @@ -51,8 +51,9 @@ end; -functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY = +functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = struct +local open ThmDB in datatype basetype = Thy of string | File of string; @@ -284,7 +285,8 @@ else (writeln ("Reading \"" ^ name ^ ".ML\""); use ml_file); - use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; + use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");", + "map store_thm_db (axioms_of " ^ tname ^ ".thy);"]; (*Store theory again because it could have been redefined*) (*Now set the correct info*) @@ -441,7 +443,7 @@ merge_thy_list mk_draft (map get_theory mergelist) end; (*Change theory object for an existent item of loaded_thys - or create a new item *) + or create a new item; also store axioms in Thm database*) fun store_theory (thy, tname) = let val tinfo = case Symtab.lookup (!loaded_thys, tname) of Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) => @@ -451,8 +453,8 @@ | None => ThyInfo {path = "", children = [], thy_time = None, ml_time = None, theory = Some thy, thms = Symtab.null}; - in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; - + in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) + end; (** store and retrieve theorems **) @@ -506,7 +508,7 @@ ((thy_name, ThyInfo {path = path, children = children, thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}), ! loaded_thys); - thm + store_thm_db (name, thm) end; (*Store result of proof in loaded_thys and as ML value*) @@ -578,5 +580,5 @@ fun print_theory thy = (Drule.print_theory thy; print_thms thy); - +end end;