ID: $Id$ Directory: Pure/Thy Author: Carsten Clasohm Copyright 1994 TU Muenchen FIXME FIXME FIXME FIXME FIXME Warning: not quite up-to-date! Conventions for theory- and filenames: - Files for theory T are named T.thy and T.ML where only one of these two must exist. - Either T.thy or T.ML must define a ML structure containing an element named thy (the theory). Information stored about loaded theories: - name of the theory - absolute path of the theory's files - time of last modification for .thy and .ML file (updated when the files are read) - names of all read theories that depend on the theory - the theory as a ML object - theorems How to rebuild the theory hierarchy: The database not only contains theories read from files but also the 'mother of all theories' - Pure. By retrieving this theory's child list (i.e. the names of all theories that are extensions of it) one can build the hierarchy by recursively repeating this procedure. The datatype used: Information is stored in the variable loaded_thys which has type "thy_info Symtab.table ref", i.e. as an unbalanced binary tree with the theory names as keys and entries of type thy_info: datatype thy_info = ThyInfo of {path: string, children: string list, thy_time: string option, ml_time: string option, theory: theory option, thms: thm Symtab.table}; path: absolute path of directory where the files where located when the theory was last read children: names of all read theories that are descendants of this theory thy_time: If T.thy existed this contains information about the file which looks like this: Some "-rw-r--r-- 1 clasohm 232 Aug 19 11:10 ". Else it is 'None'. ml_time: same for T.ML theory: ML object containing the theory. As entries in loaded_thys are created before the theory has been read this may be 'None' in case of an error during use_thy "T". thms: theorems An entry may look like this: ("Fun", ThyInfo {path = "/disk1/usr/stud/clasohm/isabelle/HOL/./", thms = ?, theory = Some {Pure, HOL, Ord, Set}, ml_time = Some "-rw-r--r-- 1 clasohm 6076 Aug 30 10:04 ", children = ["Prod", "subset"], thy_time = Some "-rw-r--r-- 1 clasohm 243 Aug 19 11:02 "}) Notes: In general all theories contained in loaded_thys are linked with Pure. Though stray theories are possible they are removed from loaded_thys automatically as soon as update(); is used. Cycles in the hierarchy are not allowed and it is guaranteed that loaded_thys doesn't contain one. On the other hand this is possible (with all lines representing downward arrows): A / \ B C | | \ D \ / E Isabelle first searches for theory files in the directory stored in thy_info's path component. But in case they have been moved meanwhile the variable load_path (string list ref) is used to find them.