src/Pure/Thy/README

documentation on theories

    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.