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