ID: $Id$
Directory: Pure/Thy
Author: Carsten Clasohm
Copyright 1994 TU Muenchen
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.