|
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. |