src/Pure/Thy/README
author wenzelm
Wed Jan 29 15:45:40 1997 +0100 (1997-01-29)
changeset 2564 9d66b758bce5
parent 592 9154d8410514
child 4273 c9b577c8f7a1
permissions -rw-r--r--
removed warning for unprintable chars in strings (functionality will
be put into administrative script);
lcp@592
     1
    ID:         $Id$
lcp@592
     2
    Directory:  Pure/Thy
lcp@592
     3
    Author:     Carsten Clasohm
lcp@592
     4
    Copyright   1994 TU Muenchen
lcp@592
     5
lcp@592
     6
lcp@592
     7
Conventions for theory- and filenames:
lcp@592
     8
lcp@592
     9
- Files for theory T are named T.thy and T.ML where only one of these two
lcp@592
    10
  must exist.
lcp@592
    11
- Either T.thy or T.ML must define a ML structure containing an element
lcp@592
    12
  named thy (the theory).
lcp@592
    13
lcp@592
    14
lcp@592
    15
Information stored about loaded theories:
lcp@592
    16
lcp@592
    17
- name of the theory
lcp@592
    18
- absolute path of the theory's files
lcp@592
    19
- time of last modification for .thy and .ML file
lcp@592
    20
  (updated when the files are read)
lcp@592
    21
- names of all read theories that depend on the theory
lcp@592
    22
- the theory as a ML object
lcp@592
    23
- theorems
lcp@592
    24
lcp@592
    25
lcp@592
    26
How to rebuild the theory hierarchy:
lcp@592
    27
lcp@592
    28
The database not only contains theories read from files but also the 
lcp@592
    29
'mother of all theories' - Pure. By retrieving this theory's child list
lcp@592
    30
(i.e. the names of all theories that are extensions of it) one can build the 
lcp@592
    31
hierarchy by recursively repeating this procedure.
lcp@592
    32
lcp@592
    33
lcp@592
    34
The datatype used:
lcp@592
    35
lcp@592
    36
Information is stored in the variable loaded_thys which has type
lcp@592
    37
"thy_info Symtab.table ref", i.e. as an unbalanced binary tree with
lcp@592
    38
the theory names as keys and entries of type thy_info:
lcp@592
    39
lcp@592
    40
datatype thy_info = ThyInfo of {path: string,
lcp@592
    41
                                children: string list,
lcp@592
    42
                                thy_time: string option,
lcp@592
    43
                                ml_time: string option,
lcp@592
    44
                                theory: theory option,
lcp@592
    45
                                thms: thm Symtab.table};
lcp@592
    46
lcp@592
    47
path: absolute path of directory where the files where located when the theory
lcp@592
    48
      was last read
lcp@592
    49
children: names of all read theories that are descendants of this theory
lcp@592
    50
thy_time: If T.thy existed this contains information about the file which
lcp@592
    51
  looks like this: Some "-rw-r--r--  1 clasohm       232 Aug 19 11:10 ".
lcp@592
    52
  Else it is 'None'.
lcp@592
    53
ml_time: same for T.ML
lcp@592
    54
theory: ML object containing the theory. As entries in loaded_thys are created
lcp@592
    55
  before the theory has been read this may be 'None' in case of an error
lcp@592
    56
  during use_thy "T".
lcp@592
    57
thms: theorems
lcp@592
    58
lcp@592
    59
lcp@592
    60
An entry may look like this:
lcp@592
    61
lcp@592
    62
   ("Fun",
lcp@592
    63
      ThyInfo
lcp@592
    64
         {path = "/disk1/usr/stud/clasohm/isabelle/HOL/./",
lcp@592
    65
            thms = ?,
lcp@592
    66
            theory = Some {Pure, HOL, Ord, Set},
lcp@592
    67
            ml_time = Some "-rw-r--r--  1 clasohm      6076 Aug 30 10:04 ",
lcp@592
    68
            children = ["Prod", "subset"],
lcp@592
    69
            thy_time =
lcp@592
    70
            Some "-rw-r--r--  1 clasohm       243 Aug 19 11:02 "})
lcp@592
    71
lcp@592
    72
lcp@592
    73
Notes:
lcp@592
    74
lcp@592
    75
In general all theories contained in loaded_thys are linked with Pure.
lcp@592
    76
Though stray theories are possible they are removed from loaded_thys 
lcp@592
    77
automatically as soon as update(); is used.
lcp@592
    78
lcp@592
    79
Cycles in the hierarchy are not allowed and it is guaranteed that
lcp@592
    80
loaded_thys doesn't contain one. On the other hand this is possible
lcp@592
    81
(with all lines representing downward arrows):
lcp@592
    82
lcp@592
    83
     A
lcp@592
    84
    / \
lcp@592
    85
   B   C
lcp@592
    86
   |   |
lcp@592
    87
   \   D
lcp@592
    88
    \ /
lcp@592
    89
     E
lcp@592
    90
lcp@592
    91
Isabelle first searches for theory files in the directory stored in
lcp@592
    92
thy_info's path component. But in case they have been moved meanwhile
lcp@592
    93
the variable load_path (string list ref) is used to find them.