author | clasohm |
Thu, 22 Jun 1995 12:58:39 +0200 | |
changeset 1154 | bc295e3dc078 |
parent 1132 | dfb29abcf3c2 |
child 1157 | da78c293e8dc |
permissions | -rw-r--r-- |
391 | 1 |
(* Title: Pure/Thy/thy_read.ML |
2 |
ID: $Id$ |
|
559 | 3 |
Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and |
4 |
Tobias Nipkow and L C Paulson |
|
5 |
Copyright 1994 TU Muenchen |
|
391 | 6 |
|
559 | 7 |
(* FIXME !? *) |
391 | 8 |
Reading and writing the theory definition files. |
9 |
||
559 | 10 |
(* FIXME !? *) |
391 | 11 |
For theory XXX, the input file is called XXX.thy |
12 |
the output file is called .XXX.thy.ML |
|
13 |
and it then tries to read XXX.ML |
|
14 |
*) |
|
15 |
||
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
16 |
datatype thy_info = ThyInfo of {path: string, |
391 | 17 |
children: string list, |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
18 |
thy_time: string option, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
19 |
ml_time: string option, |
559 | 20 |
theory: theory option, |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
21 |
thms: thm Symtab.table}; |
391 | 22 |
|
412 | 23 |
signature READTHY = |
391 | 24 |
sig |
25 |
datatype basetype = Thy of string |
|
26 |
| File of string |
|
27 |
||
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
28 |
val loaded_thys : thy_info Symtab.table ref |
391 | 29 |
val loadpath : string list ref |
30 |
val delete_tmpfiles: bool ref |
|
31 |
||
32 |
val use_thy : string -> unit |
|
33 |
val update : unit -> unit |
|
34 |
val time_use_thy : string -> unit |
|
35 |
val unlink_thy : string -> unit |
|
586
201e115d8031
renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents:
559
diff
changeset
|
36 |
val mk_base : basetype list -> string -> bool -> theory |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
37 |
val store_theory : theory * string -> unit |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
38 |
|
559 | 39 |
val theory_of_sign: Sign.sg -> theory |
40 |
val theory_of_thm: thm -> theory |
|
41 |
val store_thm: string * thm -> thm |
|
758 | 42 |
val bind_thm: string * thm -> unit |
559 | 43 |
val qed: string -> unit |
758 | 44 |
val qed_thm: thm ref |
746 | 45 |
val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
46 |
val qed_goalw: string -> theory->thm list->string->(thm list->tactic list) |
|
47 |
-> unit |
|
559 | 48 |
val get_thm: theory -> string -> thm |
49 |
val thms_of: theory -> (string * thm) list |
|
778 | 50 |
val print_theory: theory -> unit |
391 | 51 |
end; |
52 |
||
53 |
||
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
54 |
functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = |
391 | 55 |
struct |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
56 |
local open ThmDB in |
391 | 57 |
|
58 |
datatype basetype = Thy of string |
|
59 |
| File of string; |
|
60 |
||
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
61 |
val loaded_thys = ref (Symtab.make [("ProtoPure", |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
62 |
ThyInfo {path = "", |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
63 |
children = ["Pure", "CPure"], |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
64 |
thy_time = Some "", ml_time = Some "", |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
65 |
theory = Some proto_pure_thy, |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
66 |
thms = Symtab.null}), |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
67 |
("Pure", ThyInfo {path = "", children = [], |
559 | 68 |
thy_time = Some "", ml_time = Some "", |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
69 |
theory = Some pure_thy, |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
70 |
thms = Symtab.null}), |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
71 |
("CPure", ThyInfo {path = "", |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
72 |
children = [], |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
73 |
thy_time = Some "", ml_time = Some "", |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
74 |
theory = Some cpure_thy, |
559 | 75 |
thms = Symtab.null})]); |
391 | 76 |
|
77 |
val loadpath = ref ["."]; (*default search path for theory files *) |
|
78 |
||
79 |
val delete_tmpfiles = ref true; (*remove temporary files after use *) |
|
80 |
||
81 |
(*Make name of the output ML file for a theory *) |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
82 |
fun out_name tname = "." ^ tname ^ ".thy.ML"; |
391 | 83 |
|
84 |
(*Read a file specified by thy_file containing theory thy *) |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
85 |
fun read_thy tname thy_file = |
559 | 86 |
let |
391 | 87 |
val instream = open_in thy_file; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
88 |
val outstream = open_out (out_name tname); |
559 | 89 |
in |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
90 |
output (outstream, ThySyn.parse tname (input (instream, 999999))); |
391 | 91 |
close_out outstream; |
92 |
close_in instream |
|
93 |
end; |
|
94 |
||
95 |
fun file_exists file = |
|
96 |
let val instream = open_in file in close_in instream; true end |
|
97 |
handle Io _ => false; |
|
98 |
||
99 |
(*Get thy_info for a loaded theory *) |
|
559 | 100 |
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); |
391 | 101 |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
102 |
(*Check if a theory was completly loaded *) |
391 | 103 |
fun already_loaded thy = |
104 |
let val t = get_thyinfo thy |
|
105 |
in if is_none t then false |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
106 |
else let val ThyInfo {thy_time, ml_time, ...} = the t |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
107 |
in is_some thy_time andalso is_some ml_time end |
391 | 108 |
end; |
109 |
||
110 |
(*Check if a theory file has changed since its last use. |
|
111 |
Return a pair of boolean values for .thy and for .ML *) |
|
559 | 112 |
fun thy_unchanged thy thy_file ml_file = |
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
113 |
case get_thyinfo thy of |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
114 |
Some (ThyInfo {thy_time, ml_time, ...}) => |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
115 |
let val tn = is_none thy_time; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
116 |
val mn = is_none ml_time |
391 | 117 |
in if not tn andalso not mn then |
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
118 |
((file_info thy_file = the thy_time), |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
119 |
(file_info ml_file = the ml_time)) |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
120 |
else if not tn andalso mn then |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
121 |
(file_info thy_file = the thy_time, false) |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
122 |
else |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
123 |
(false, false) |
391 | 124 |
end |
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
125 |
| None => (false, false) |
391 | 126 |
|
127 |
exception FILE_NOT_FOUND; (*raised by find_file *) |
|
128 |
||
129 |
(*Find a file using a list of paths if no absolute or relative path is |
|
130 |
specified.*) |
|
131 |
fun find_file "" name = |
|
132 |
let fun find_it (curr :: paths) = |
|
133 |
if file_exists (tack_on curr name) then |
|
134 |
tack_on curr name |
|
559 | 135 |
else |
391 | 136 |
find_it paths |
137 |
| find_it [] = "" |
|
138 |
in find_it (!loadpath) end |
|
139 |
| find_file path name = |
|
140 |
if file_exists (tack_on path name) then tack_on path name |
|
141 |
else ""; |
|
142 |
||
143 |
(*Get absolute pathnames for a new or already loaded theory *) |
|
144 |
fun get_filenames path name = |
|
145 |
let fun make_absolute file = |
|
559 | 146 |
if file = "" then "" else |
391 | 147 |
if hd (explode file) = "/" then file else tack_on (pwd ()) file; |
148 |
||
149 |
fun new_filename () = |
|
150 |
let val found = find_file path (name ^ ".thy") |
|
151 |
handle FILE_NOT_FOUND => ""; |
|
152 |
val thy_file = make_absolute found; |
|
153 |
val (thy_path, _) = split_filename thy_file; |
|
154 |
val found = find_file path (name ^ ".ML"); |
|
155 |
val ml_file = if thy_file = "" then make_absolute found |
|
156 |
else if file_exists (tack_on thy_path (name ^ ".ML")) |
|
157 |
then tack_on thy_path (name ^ ".ML") |
|
158 |
else ""; |
|
159 |
val searched_dirs = if path = "" then (!loadpath) else [path] |
|
160 |
in if thy_file = "" andalso ml_file = "" then |
|
161 |
error ("Could not find file \"" ^ name ^ ".thy\" or \"" |
|
162 |
^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" |
|
163 |
^ "in the following directories: \"" ^ |
|
164 |
(space_implode "\", \"" searched_dirs) ^ "\"") |
|
165 |
else (); |
|
559 | 166 |
(thy_file, ml_file) |
391 | 167 |
end; |
168 |
||
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
169 |
val tinfo = get_thyinfo name; |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
170 |
in if is_some tinfo andalso path = "" then |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
171 |
let val ThyInfo {path = abs_path, ...} = the tinfo; |
391 | 172 |
val (thy_file, ml_file) = if abs_path = "" then new_filename () |
173 |
else (find_file abs_path (name ^ ".thy"), |
|
174 |
find_file abs_path (name ^ ".ML")) |
|
175 |
in if thy_file = "" andalso ml_file = "" then |
|
176 |
(writeln ("Warning: File \"" ^ (tack_on path name) |
|
177 |
^ ".thy\"\ncontaining theory \"" ^ name |
|
178 |
^ "\" no longer exists."); |
|
179 |
new_filename () |
|
180 |
) |
|
181 |
else (thy_file, ml_file) |
|
182 |
end |
|
183 |
else new_filename () |
|
184 |
end; |
|
185 |
||
186 |
(*Remove theory from all child lists in loaded_thys *) |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
187 |
fun unlink_thy tname = |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
188 |
let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) = |
559 | 189 |
ThyInfo {path = path, children = children \ tname, |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
190 |
thy_time = thy_time, ml_time = ml_time, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
191 |
theory = theory, thms = thms} |
559 | 192 |
in loaded_thys := Symtab.map remove (!loaded_thys) end; |
391 | 193 |
|
194 |
(*Remove a theory from loaded_thys *) |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
195 |
fun remove_thy tname = |
559 | 196 |
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) |
197 |
(Symtab.dest (!loaded_thys))); |
|
391 | 198 |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
199 |
(*Change thy_time and ml_time for an existent item *) |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
200 |
fun set_info thy_time ml_time tname = |
559 | 201 |
let val ThyInfo {path, children, theory, thms, ...} = |
202 |
the (Symtab.lookup (!loaded_thys, tname)); |
|
203 |
in loaded_thys := Symtab.update ((tname, |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
204 |
ThyInfo {path = path, children = children, |
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
205 |
thy_time = thy_time, ml_time = ml_time, |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
206 |
theory = theory, thms = thms}), !loaded_thys) |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
207 |
end; |
391 | 208 |
|
209 |
(*Mark theory as changed since last read if it has been completly read *) |
|
559 | 210 |
fun mark_outdated tname = |
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
211 |
let val t = get_thyinfo tname; |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
212 |
in if is_none t then () |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
213 |
else let val ThyInfo {thy_time, ml_time, ...} = the t |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
214 |
in set_info (if is_none thy_time then None else Some "") |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
215 |
(if is_none ml_time then None else Some "") |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
216 |
tname |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
217 |
end |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
218 |
end; |
391 | 219 |
|
559 | 220 |
(*Read .thy and .ML files that haven't been read yet or have changed since |
391 | 221 |
they were last read; |
559 | 222 |
loaded_thys is a thy_info list ref containing all theories that have |
391 | 223 |
completly been read by this and preceeding use_thy calls. |
224 |
If a theory changed since its last use its children are marked as changed *) |
|
225 |
fun use_thy name = |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
226 |
let val (path, tname) = split_filename name; |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
227 |
val (thy_file, ml_file) = get_filenames path tname; |
391 | 228 |
val (abs_path, _) = if thy_file = "" then split_filename ml_file |
229 |
else split_filename thy_file; |
|
559 | 230 |
val (thy_uptodate, ml_uptodate) = thy_unchanged tname |
391 | 231 |
thy_file ml_file; |
232 |
||
233 |
(*Set absolute path for loaded theory *) |
|
234 |
fun set_path () = |
|
559 | 235 |
let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = |
236 |
the (Symtab.lookup (!loaded_thys, tname)); |
|
237 |
in loaded_thys := Symtab.update ((tname, |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
238 |
ThyInfo {path = abs_path, children = children, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
239 |
thy_time = thy_time, ml_time = ml_time, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
240 |
theory = theory, thms = thms}), |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
241 |
!loaded_thys) |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
242 |
end; |
391 | 243 |
|
244 |
(*Mark all direct descendants of a theory as changed *) |
|
245 |
fun mark_children thy = |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
246 |
let val ThyInfo {children, ...} = the (get_thyinfo thy); |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
247 |
val present = filter (is_some o get_thyinfo) children; |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
248 |
val loaded = filter already_loaded present; |
391 | 249 |
in if loaded <> [] then |
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
250 |
writeln ("The following children of theory " ^ (quote thy) |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
251 |
^ " are now out-of-date: " |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
252 |
^ (quote (space_implode "\",\"" loaded))) |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
253 |
else (); |
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
254 |
seq mark_outdated present |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
255 |
end; |
391 | 256 |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
257 |
(*Remove all theorems associated with a theory*) |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
258 |
fun delete_thms () = |
559 | 259 |
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
260 |
Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) => |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
261 |
ThyInfo {path = path, children = children, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
262 |
thy_time = thy_time, ml_time = ml_time, |
559 | 263 |
theory = theory, thms = Symtab.null} |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
264 |
| None => ThyInfo {path = "", children = [], |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
265 |
thy_time = None, ml_time = None, |
559 | 266 |
theory = None, thms = Symtab.null}; |
267 |
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; |
|
391 | 268 |
in if thy_uptodate andalso ml_uptodate then () |
269 |
else |
|
270 |
( |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
271 |
delete_thms (); |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
272 |
|
391 | 273 |
if thy_uptodate orelse thy_file = "" then () |
274 |
else (writeln ("Reading \"" ^ name ^ ".thy\""); |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
275 |
read_thy tname thy_file; |
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
276 |
use (out_name tname); |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
277 |
|
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
278 |
if not (!delete_tmpfiles) then () |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
279 |
else delete_file (out_name tname) |
391 | 280 |
); |
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
281 |
set_info (Some (file_info thy_file)) None tname; |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
282 |
(*mark thy_file as successfully loaded*) |
391 | 283 |
|
559 | 284 |
if ml_file = "" then () |
391 | 285 |
else (writeln ("Reading \"" ^ name ^ ".ML\""); |
286 |
use ml_file); |
|
287 |
||
1154
bc295e3dc078
changed call of store_thm_db so that it's result is not displayed
clasohm
parents:
1132
diff
changeset
|
288 |
use_string |
bc295e3dc078
changed call of store_thm_db so that it's result is not displayed
clasohm
parents:
1132
diff
changeset
|
289 |
["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\ |
bc295e3dc078
changed call of store_thm_db so that it's result is not displayed
clasohm
parents:
1132
diff
changeset
|
290 |
\map store_thm_db (axioms_of " ^ tname ^ ".thy));"]; |
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
291 |
(*Store theory again because it could have been redefined*) |
391 | 292 |
|
293 |
(*Now set the correct info*) |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
294 |
set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname; |
391 | 295 |
set_path (); |
296 |
||
297 |
(*Mark theories that have to be reloaded*) |
|
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
298 |
mark_children tname |
391 | 299 |
) |
300 |
end; |
|
301 |
||
302 |
fun time_use_thy tname = timeit(fn()=> |
|
559 | 303 |
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); |
391 | 304 |
use_thy tname; |
305 |
writeln("\n**** Finished Theory " ^ tname ^ " ****")) |
|
306 |
); |
|
307 |
||
308 |
(*Load all thy or ML files that have been changed and also |
|
309 |
all theories that depend on them *) |
|
310 |
fun update () = |
|
311 |
let (*List theories in the order they have to be loaded *) |
|
312 |
fun load_order [] result = result |
|
313 |
| load_order thys result = |
|
314 |
let fun next_level (t :: ts) = |
|
315 |
let val thy = get_thyinfo t |
|
316 |
in if is_some thy then |
|
317 |
let val ThyInfo {children, ...} = the thy |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
318 |
in children union (next_level ts) end |
391 | 319 |
else next_level ts |
320 |
end |
|
321 |
| next_level [] = []; |
|
559 | 322 |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
323 |
val children = next_level thys; |
391 | 324 |
in load_order children ((result \\ children) @ children) end; |
325 |
||
326 |
fun reload_changed (t :: ts) = |
|
327 |
let val thy = get_thyinfo t; |
|
328 |
||
329 |
fun abspath () = |
|
330 |
if is_some thy then |
|
331 |
let val ThyInfo {path, ...} = the thy in path end |
|
332 |
else ""; |
|
333 |
||
334 |
val (thy_file, ml_file) = get_filenames (abspath ()) t; |
|
335 |
val (thy_uptodate, ml_uptodate) = |
|
336 |
thy_unchanged t thy_file ml_file; |
|
337 |
in if thy_uptodate andalso ml_uptodate then () |
|
338 |
else use_thy t; |
|
339 |
reload_changed ts |
|
340 |
end |
|
341 |
| reload_changed [] = (); |
|
342 |
||
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
343 |
(*Remove all theories that are no descendants of ProtoPure. |
391 | 344 |
If there are still children in the deleted theory's list |
345 |
schedule them for reloading *) |
|
346 |
fun collect_garbage not_garbage = |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
347 |
let fun collect ((tname, ThyInfo {children, ...}) :: ts) = |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
348 |
if tname mem not_garbage then collect ts |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
349 |
else (writeln ("Theory \"" ^ tname ^ |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
350 |
"\" is no longer linked with ProtoPure - removing it."); |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
351 |
remove_thy tname; |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
352 |
seq mark_outdated children) |
391 | 353 |
| collect [] = () |
354 |
||
559 | 355 |
in collect (Symtab.dest (!loaded_thys)) end; |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
356 |
in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] [])); |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
357 |
reload_changed (load_order ["Pure", "CPure"] []) |
391 | 358 |
end; |
359 |
||
360 |
(*Merge theories to build a base for a new theory. |
|
361 |
Base members are only loaded if they are missing. *) |
|
586
201e115d8031
renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents:
559
diff
changeset
|
362 |
fun mk_base bases child mk_draft = |
391 | 363 |
let (*List all descendants of a theory list *) |
364 |
fun list_descendants (t :: ts) = |
|
365 |
let val tinfo = get_thyinfo t |
|
366 |
in if is_some tinfo then |
|
367 |
let val ThyInfo {children, ...} = the tinfo |
|
368 |
in children union (list_descendants (ts union children)) |
|
369 |
end |
|
370 |
else [] |
|
371 |
end |
|
372 |
| list_descendants [] = []; |
|
373 |
||
374 |
(*Show the cycle that would be created by add_child *) |
|
375 |
fun show_cycle base = |
|
376 |
let fun find_it result curr = |
|
377 |
let val tinfo = get_thyinfo curr |
|
559 | 378 |
in if base = curr then |
391 | 379 |
error ("Cyclic dependency of theories: " |
380 |
^ child ^ "->" ^ base ^ result) |
|
381 |
else if is_some tinfo then |
|
382 |
let val ThyInfo {children, ...} = the tinfo |
|
383 |
in seq (find_it ("->" ^ curr ^ result)) children |
|
384 |
end |
|
385 |
else () |
|
386 |
end |
|
387 |
in find_it "" child end; |
|
559 | 388 |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
389 |
(*Check if a cycle would be created by add_child *) |
391 | 390 |
fun find_cycle base = |
391 |
if base mem (list_descendants [child]) then show_cycle base |
|
392 |
else (); |
|
559 | 393 |
|
391 | 394 |
(*Add child to child list of base *) |
395 |
fun add_child base = |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
396 |
let val tinfo = |
559 | 397 |
case Symtab.lookup (!loaded_thys, base) of |
398 |
Some (ThyInfo {path, children, thy_time, ml_time, |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
399 |
theory, thms}) => |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
400 |
ThyInfo {path = path, children = child ins children, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
401 |
thy_time = thy_time, ml_time = ml_time, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
402 |
theory = theory, thms = thms} |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
403 |
| None => ThyInfo {path = "", children = [child], |
559 | 404 |
thy_time = None, ml_time = None, |
405 |
theory = None, thms = Symtab.null}; |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
406 |
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; |
391 | 407 |
|
408 |
(*Load a base theory if not already done |
|
409 |
and no cycle would be created *) |
|
410 |
fun load base = |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
411 |
let val thy_loaded = already_loaded base |
426
767367131b47
replaced "foldl merge_theories" by "merge_thy_list" in base_on
clasohm
parents:
424
diff
changeset
|
412 |
(*test this before child is added *) |
391 | 413 |
in |
414 |
if child = base then |
|
415 |
error ("Cyclic dependency of theories: " ^ child |
|
416 |
^ "->" ^ child) |
|
559 | 417 |
else |
391 | 418 |
(find_cycle base; |
419 |
add_child base; |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
420 |
if thy_loaded then () |
391 | 421 |
else (writeln ("Autoloading theory " ^ (quote base) |
422 |
^ " (used by " ^ (quote child) ^ ")"); |
|
423 |
use_thy base) |
|
424 |
) |
|
559 | 425 |
end; |
391 | 426 |
|
427 |
(*Load all needed files and make a list of all real theories *) |
|
428 |
fun load_base (Thy b :: bs) = |
|
429 |
(load b; |
|
430 |
b :: (load_base bs)) |
|
431 |
| load_base (File b :: bs) = |
|
432 |
(load b; |
|
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
433 |
load_base bs) (*don't add it to mergelist *) |
391 | 434 |
| load_base [] = []; |
435 |
||
436 |
(*Get theory object for a loaded theory *) |
|
437 |
fun get_theory name = |
|
438 |
let val ThyInfo {theory, ...} = the (get_thyinfo name) |
|
439 |
in the theory end; |
|
440 |
||
441 |
val mergelist = (unlink_thy child; |
|
442 |
load_base bases); |
|
443 |
in writeln ("Loading theory " ^ (quote child)); |
|
426
767367131b47
replaced "foldl merge_theories" by "merge_thy_list" in base_on
clasohm
parents:
424
diff
changeset
|
444 |
merge_thy_list mk_draft (map get_theory mergelist) end; |
391 | 445 |
|
559 | 446 |
(*Change theory object for an existent item of loaded_thys |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
447 |
or create a new item; also store axioms in Thm database*) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
448 |
fun store_theory (thy, tname) = |
559 | 449 |
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
450 |
Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) => |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
451 |
ThyInfo {path = path, children = children, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
452 |
thy_time = thy_time, ml_time = ml_time, |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
453 |
theory = Some thy, thms = thms} |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
454 |
| None => ThyInfo {path = "", children = [], |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
455 |
thy_time = None, ml_time = None, |
559 | 456 |
theory = Some thy, thms = Symtab.null}; |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
457 |
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) |
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
458 |
end; |
559 | 459 |
|
460 |
||
461 |
(** store and retrieve theorems **) |
|
462 |
||
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
463 |
(*Guess to which theory a signature belongs and return it's thy_info*) |
559 | 464 |
fun thyinfo_of_sign sg = |
465 |
let |
|
466 |
val ref xname = hd (#stamps (Sign.rep_sg sg)); |
|
467 |
val opt_info = get_thyinfo xname; |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
468 |
|
559 | 469 |
fun eq_sg (ThyInfo {theory = None, ...}) = false |
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
470 |
| eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy); |
559 | 471 |
|
472 |
val show_sg = Pretty.str_of o Sign.pretty_sg; |
|
473 |
in |
|
474 |
if is_some opt_info andalso eq_sg (the opt_info) then |
|
475 |
(xname, the opt_info) |
|
476 |
else |
|
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
477 |
(case Symtab.find_first (eq_sg o snd) (!loaded_thys) of |
559 | 478 |
Some name_info => name_info |
479 |
| None => error ("Theory " ^ show_sg sg ^ " not stored by loader")) |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
480 |
end; |
391 | 481 |
|
559 | 482 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
483 |
(*Try to get the theory object corresponding to a given signature*) |
559 | 484 |
fun theory_of_sign sg = |
485 |
(case thyinfo_of_sign sg of |
|
486 |
(_, ThyInfo {theory = Some thy, ...}) => thy |
|
487 |
| _ => sys_error "theory_of_sign"); |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
488 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
489 |
(*Try to get the theory object corresponding to a given theorem*) |
559 | 490 |
val theory_of_thm = theory_of_sign o #sign o rep_thm; |
491 |
||
492 |
||
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
493 |
(* Store theorems *) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
494 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
495 |
(*Store a theorem in the thy_info of its theory*) |
559 | 496 |
fun store_thm (name, thm) = |
497 |
let |
|
498 |
val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) = |
|
499 |
thyinfo_of_sign (#sign (rep_thm thm)); |
|
500 |
val thms' = Symtab.update_new ((name, thm), thms) |
|
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
501 |
handle Symtab.DUPLICATE s => |
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
502 |
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then |
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
503 |
(writeln ("Warning: Theorem database already contains copy of\ |
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
504 |
\ theorem " ^ quote name); |
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
505 |
thms) |
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
506 |
else error ("Duplicate theorem name " ^ quote s)); |
559 | 507 |
in |
508 |
loaded_thys := Symtab.update |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
509 |
((thy_name, ThyInfo {path = path, children = children, |
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
510 |
thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}), |
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
511 |
! loaded_thys); |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
512 |
store_thm_db (name, thm) |
559 | 513 |
end; |
514 |
||
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
515 |
(*Store result of proof in loaded_thys and as ML value*) |
758 | 516 |
|
517 |
val qed_thm = ref flexpair_def(*dummy*); |
|
518 |
||
519 |
fun bind_thm (name, thm) = |
|
520 |
(qed_thm := thm; |
|
521 |
use_string ["val " ^ name ^ " = standard (store_thm (" ^ quote name ^ |
|
522 |
", !qed_thm));"]); |
|
523 |
||
559 | 524 |
fun qed name = |
525 |
use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"]; |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
526 |
|
746 | 527 |
fun qed_goal name thy agoal tacsf = |
758 | 528 |
(qed_thm := prove_goal thy agoal tacsf; |
529 |
use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]); |
|
746 | 530 |
|
531 |
fun qed_goalw name thy rths agoal tacsf = |
|
758 | 532 |
(qed_thm := prove_goalw thy rths agoal tacsf; |
533 |
use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^", !qed_thm);"]); |
|
559 | 534 |
|
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
535 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
536 |
(* Retrieve theorems *) |
559 | 537 |
|
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
538 |
(*Get all direct ancestors of a theory*) |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
539 |
fun get_parents child = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
540 |
let fun has_child (tname, ThyInfo {children, theory, ...}) = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
541 |
if child mem children then Some tname else None; |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
542 |
in mapfilter has_child (Symtab.dest (!loaded_thys)) end; |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
543 |
|
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
544 |
(*Get all theorems belonging to a given theory*) |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
545 |
fun thmtab_ofthy thy = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
546 |
let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy); |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
547 |
in thms end; |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
548 |
|
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
549 |
fun thmtab_ofname name = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
550 |
let val ThyInfo {thms, ...} = the (get_thyinfo name); |
559 | 551 |
in thms end; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
552 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
553 |
(*Get a stored theorem specified by theory and name*) |
559 | 554 |
fun get_thm thy name = |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
555 |
let fun get [] [] searched = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
556 |
raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
557 |
| get [] ng searched = |
871 | 558 |
get (ng \\ searched) [] searched |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
559 |
| get (t::ts) ng searched = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
560 |
(case Symtab.lookup (thmtab_ofname t, name) of |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
561 |
Some thm => thm |
871 | 562 |
| None => get ts (ng union (get_parents t)) (t::searched)); |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
563 |
|
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
564 |
val (tname, _) = thyinfo_of_sign (sign_of thy); |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
565 |
in get [tname] [] [] end; |
559 | 566 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
567 |
(*Get stored theorems of a theory*) |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
568 |
val thms_of = Symtab.dest o thmtab_ofthy; |
559 | 569 |
|
570 |
||
778 | 571 |
(* print theory *) |
572 |
||
573 |
fun print_thms thy = |
|
574 |
let |
|
575 |
val thms = thms_of thy; |
|
576 |
fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1, |
|
577 |
Pretty.quote (pretty_thm th)]; |
|
578 |
in |
|
579 |
Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms)) |
|
580 |
end; |
|
581 |
||
582 |
fun print_theory thy = (Drule.print_theory thy; print_thms thy); |
|
583 |
||
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
584 |
end |
391 | 585 |
end; |