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