author | clasohm |
Tue, 07 Nov 1995 13:15:04 +0100 | |
changeset 1323 | ae24fa249266 |
parent 1320 | b94ef890dbf2 |
child 1332 | a60d1abb06c0 |
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 |
|
1242 | 7 |
Functions for reading theory files, and storing and retrieving theories, |
8 |
theorems and the global simplifier set. |
|
391 | 9 |
*) |
10 |
||
1157 | 11 |
(*Type for theory storage*) |
1291 | 12 |
datatype thy_info = |
13 |
ThyInfo of {path: string, |
|
14 |
children: string list, parents: string list, |
|
15 |
thy_time: string option, ml_time: string option, |
|
16 |
theory: theory option, thms: thm Symtab.table, |
|
17 |
thy_ss: Simplifier.simpset option, |
|
18 |
simpset: Simplifier.simpset option}; |
|
1157 | 19 |
(*meaning of special values: |
20 |
thy_time, ml_time = None theory file has not been read yet |
|
21 |
= Some "" theory was read but has either been marked |
|
22 |
as outdated or there is no such file for |
|
23 |
this theory (see e.g. 'virtual' theories |
|
24 |
like Pure or theories without a ML file) |
|
25 |
theory = None theory has not been read yet |
|
1291 | 26 |
|
27 |
parents: While 'children' contains all theories the theory depends |
|
28 |
on (i.e. also ones quoted in the .thy file), |
|
29 |
'parents' only contains the theories which were used to form |
|
30 |
the base of this theory. |
|
31 |
||
32 |
origin of the simpsets: |
|
33 |
thy_ss: snapshot of !Simpset.simpset after .thy file was read |
|
34 |
simpset: snapshot of !Simpset.simpset after .ML file was read |
|
1157 | 35 |
*) |
391 | 36 |
|
412 | 37 |
signature READTHY = |
391 | 38 |
sig |
39 |
datatype basetype = Thy of string |
|
40 |
| File of string |
|
41 |
||
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
42 |
val loaded_thys : thy_info Symtab.table ref |
391 | 43 |
val loadpath : string list ref |
44 |
val delete_tmpfiles: bool ref |
|
45 |
||
46 |
val use_thy : string -> unit |
|
47 |
val update : unit -> unit |
|
48 |
val time_use_thy : string -> unit |
|
49 |
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
|
50 |
val mk_base : basetype list -> string -> bool -> theory |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
51 |
val store_theory : theory * string -> unit |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
52 |
|
559 | 53 |
val theory_of_sign: Sign.sg -> theory |
54 |
val theory_of_thm: thm -> theory |
|
1291 | 55 |
val children_of: string -> string list |
56 |
val parents_of: string -> string list |
|
57 |
||
559 | 58 |
val store_thm: string * thm -> thm |
758 | 59 |
val bind_thm: string * thm -> unit |
559 | 60 |
val qed: string -> unit |
758 | 61 |
val qed_thm: thm ref |
746 | 62 |
val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
63 |
val qed_goalw: string -> theory->thm list->string->(thm list->tactic list) |
|
64 |
-> unit |
|
559 | 65 |
val get_thm: theory -> string -> thm |
66 |
val thms_of: theory -> (string * thm) list |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
67 |
val simpset_of: string -> Simplifier.simpset |
778 | 68 |
val print_theory: theory -> unit |
1291 | 69 |
|
70 |
val gif_path : string ref |
|
1313 | 71 |
val index_path : string ref |
1291 | 72 |
val make_html : bool ref |
73 |
val init_html: unit -> unit |
|
74 |
val make_chart: unit -> unit |
|
391 | 75 |
end; |
76 |
||
77 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
78 |
functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = |
391 | 79 |
struct |
1242 | 80 |
|
81 |
open ThmDB Simplifier; |
|
391 | 82 |
|
83 |
datatype basetype = Thy of string |
|
84 |
| File of string; |
|
85 |
||
1291 | 86 |
val loaded_thys = |
87 |
ref (Symtab.make [("ProtoPure", |
|
88 |
ThyInfo {path = "", |
|
89 |
children = ["Pure", "CPure"], parents = [], |
|
90 |
thy_time = Some "", ml_time = Some "", |
|
91 |
theory = Some proto_pure_thy, thms = Symtab.null, |
|
92 |
thy_ss = None, simpset = None}), |
|
93 |
("Pure", |
|
94 |
ThyInfo {path = "", children = [], |
|
95 |
parents = ["ProtoPure"], |
|
96 |
thy_time = Some "", ml_time = Some "", |
|
97 |
theory = Some pure_thy, thms = Symtab.null, |
|
98 |
thy_ss = None, simpset = None}), |
|
99 |
("CPure", |
|
100 |
ThyInfo {path = "", |
|
101 |
children = [], parents = ["ProtoPure"], |
|
102 |
thy_time = Some "", ml_time = Some "", |
|
103 |
theory = Some cpure_thy, |
|
104 |
thms = Symtab.null, |
|
105 |
thy_ss = None, simpset = None}) |
|
106 |
]); |
|
391 | 107 |
|
1291 | 108 |
val loadpath = ref ["."]; (*default search path for theory files*) |
109 |
||
110 |
val delete_tmpfiles = ref true; (*remove temporary files after use*) |
|
111 |
||
391 | 112 |
|
1291 | 113 |
(*Set location of graphics for HTML files |
114 |
(When this is executed for the first time we are in $ISABELLE/Pure/Thy. |
|
115 |
This path is converted to $ISABELLE/Tools by removing the last two |
|
116 |
directories and appending "Tools". All subsequently made ReadThy |
|
117 |
structures inherit this value.) |
|
118 |
*) |
|
119 |
val gif_path = ref (tack_on ("/" ^ |
|
120 |
space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ()))))))) |
|
121 |
"Tools"); |
|
122 |
||
1313 | 123 |
(*Location of theory-list.txt and index.html (normally set by init_html)*) |
124 |
val index_path = ref ""; |
|
1291 | 125 |
|
126 |
val make_html = ref false; (*don't make HTML versions of loaded theories*) |
|
127 |
||
128 |
(*HTML file of theory currently being read |
|
129 |
(Initialized by thyfile2html; used by use_thy and store_thm)*) |
|
130 |
val cur_htmlfile = ref None : outstream option ref; |
|
131 |
||
391 | 132 |
|
133 |
(*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
|
134 |
fun out_name tname = "." ^ tname ^ ".thy.ML"; |
391 | 135 |
|
136 |
(*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
|
137 |
fun read_thy tname thy_file = |
559 | 138 |
let |
391 | 139 |
val instream = open_in thy_file; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
140 |
val outstream = open_out (out_name tname); |
559 | 141 |
in |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
142 |
output (outstream, ThySyn.parse tname (input (instream, 999999))); |
391 | 143 |
close_out outstream; |
144 |
close_in instream |
|
145 |
end; |
|
146 |
||
147 |
fun file_exists file = |
|
148 |
let val instream = open_in file in close_in instream; true end |
|
149 |
handle Io _ => false; |
|
150 |
||
151 |
(*Get thy_info for a loaded theory *) |
|
559 | 152 |
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); |
391 | 153 |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
154 |
(*Check if a theory was completly loaded *) |
391 | 155 |
fun already_loaded thy = |
156 |
let val t = get_thyinfo thy |
|
157 |
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
|
158 |
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
|
159 |
in is_some thy_time andalso is_some ml_time end |
391 | 160 |
end; |
161 |
||
162 |
(*Check if a theory file has changed since its last use. |
|
163 |
Return a pair of boolean values for .thy and for .ML *) |
|
559 | 164 |
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
|
165 |
case get_thyinfo thy of |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
166 |
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
|
167 |
let val tn = is_none thy_time; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
168 |
val mn = is_none ml_time |
391 | 169 |
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
|
170 |
((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
|
171 |
(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
|
172 |
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
|
173 |
(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
|
174 |
else |
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
175 |
(false, false) |
391 | 176 |
end |
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset
|
177 |
| None => (false, false) |
391 | 178 |
|
1291 | 179 |
(*Get all direct descendants of a theory*) |
180 |
fun children_of t = |
|
181 |
case get_thyinfo t of Some (ThyInfo {children, ...}) => children |
|
182 |
| _ => []; |
|
183 |
||
1242 | 184 |
(*Get all direct ancestors of a theory*) |
1291 | 185 |
fun parents_of t = |
186 |
case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents |
|
187 |
| _ => []; |
|
1242 | 188 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
189 |
(*Get all descendants of a theory list *) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
190 |
fun get_descendants [] = [] |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
191 |
| get_descendants (t :: ts) = |
1291 | 192 |
let val children = children_of t |
193 |
in children union (get_descendants (children union ts)) end; |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
194 |
|
1242 | 195 |
(*Get theory object for a loaded theory *) |
1291 | 196 |
fun theory_of name = |
1242 | 197 |
let val ThyInfo {theory, ...} = the (get_thyinfo name) |
198 |
in the theory end; |
|
199 |
||
1291 | 200 |
(*Get path where theory's files are located*) |
201 |
fun path_of tname = |
|
202 |
let val ThyInfo {path, ...} = the (get_thyinfo tname) |
|
203 |
in path end; |
|
204 |
||
391 | 205 |
exception FILE_NOT_FOUND; (*raised by find_file *) |
206 |
||
207 |
(*Find a file using a list of paths if no absolute or relative path is |
|
208 |
specified.*) |
|
209 |
fun find_file "" name = |
|
1291 | 210 |
let fun find_it (cur :: paths) = |
211 |
if file_exists (tack_on cur name) then |
|
212 |
(if cur = "." then name else tack_on cur name) |
|
559 | 213 |
else |
1291 | 214 |
find_it paths |
391 | 215 |
| find_it [] = "" |
216 |
in find_it (!loadpath) end |
|
217 |
| find_file path name = |
|
218 |
if file_exists (tack_on path name) then tack_on path name |
|
219 |
else ""; |
|
220 |
||
221 |
(*Get absolute pathnames for a new or already loaded theory *) |
|
222 |
fun get_filenames path name = |
|
223 |
let fun make_absolute file = |
|
559 | 224 |
if file = "" then "" else |
391 | 225 |
if hd (explode file) = "/" then file else tack_on (pwd ()) file; |
226 |
||
227 |
fun new_filename () = |
|
228 |
let val found = find_file path (name ^ ".thy") |
|
229 |
handle FILE_NOT_FOUND => ""; |
|
230 |
val thy_file = make_absolute found; |
|
231 |
val (thy_path, _) = split_filename thy_file; |
|
232 |
val found = find_file path (name ^ ".ML"); |
|
233 |
val ml_file = if thy_file = "" then make_absolute found |
|
234 |
else if file_exists (tack_on thy_path (name ^ ".ML")) |
|
235 |
then tack_on thy_path (name ^ ".ML") |
|
236 |
else ""; |
|
237 |
val searched_dirs = if path = "" then (!loadpath) else [path] |
|
238 |
in if thy_file = "" andalso ml_file = "" then |
|
239 |
error ("Could not find file \"" ^ name ^ ".thy\" or \"" |
|
240 |
^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" |
|
241 |
^ "in the following directories: \"" ^ |
|
242 |
(space_implode "\", \"" searched_dirs) ^ "\"") |
|
243 |
else (); |
|
559 | 244 |
(thy_file, ml_file) |
391 | 245 |
end; |
246 |
||
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
247 |
val tinfo = get_thyinfo name; |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
248 |
in if is_some tinfo andalso path = "" then |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
249 |
let val ThyInfo {path = abs_path, ...} = the tinfo; |
391 | 250 |
val (thy_file, ml_file) = if abs_path = "" then new_filename () |
251 |
else (find_file abs_path (name ^ ".thy"), |
|
252 |
find_file abs_path (name ^ ".ML")) |
|
253 |
in if thy_file = "" andalso ml_file = "" then |
|
254 |
(writeln ("Warning: File \"" ^ (tack_on path name) |
|
255 |
^ ".thy\"\ncontaining theory \"" ^ name |
|
256 |
^ "\" no longer exists."); |
|
257 |
new_filename () |
|
258 |
) |
|
259 |
else (thy_file, ml_file) |
|
260 |
end |
|
261 |
else new_filename () |
|
262 |
end; |
|
263 |
||
264 |
(*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
|
265 |
fun unlink_thy tname = |
1291 | 266 |
let fun remove (ThyInfo {path, children, parents, thy_time, ml_time, |
267 |
theory, thms, thy_ss, simpset}) = |
|
268 |
ThyInfo {path = path, children = children \ tname, parents = parents, |
|
1242 | 269 |
thy_time = thy_time, ml_time = ml_time, theory = theory, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
270 |
thms = thms, thy_ss = thy_ss, simpset = simpset} |
559 | 271 |
in loaded_thys := Symtab.map remove (!loaded_thys) end; |
391 | 272 |
|
273 |
(*Remove a theory from loaded_thys *) |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
274 |
fun remove_thy tname = |
559 | 275 |
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) |
276 |
(Symtab.dest (!loaded_thys))); |
|
391 | 277 |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
278 |
(*Change thy_time and ml_time for an existent item *) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
279 |
fun set_info tname thy_time ml_time = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
280 |
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
1291 | 281 |
Some (ThyInfo {path, children, parents, theory, thms, |
282 |
thy_ss, simpset,...}) => |
|
283 |
ThyInfo {path = path, children = children, parents = parents, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
284 |
thy_time = thy_time, ml_time = ml_time, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
285 |
theory = theory, thms = thms, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
286 |
thy_ss = thy_ss, simpset = simpset} |
1291 | 287 |
| None => error ("set_info: theory " ^ tname ^ " not found"); |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
288 |
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
289 |
end; |
391 | 290 |
|
291 |
(*Mark theory as changed since last read if it has been completly read *) |
|
559 | 292 |
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
|
293 |
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
|
294 |
in if is_none t then () |
1291 | 295 |
else |
296 |
let val ThyInfo {thy_time, ml_time, ...} = the t |
|
297 |
in set_info tname (if is_none thy_time then None else Some "") |
|
298 |
(if is_none ml_time then None else Some "") |
|
299 |
end |
|
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset
|
300 |
end; |
391 | 301 |
|
1291 | 302 |
(*Make head of HTML dependency charts |
303 |
Parameters are: |
|
304 |
file: HTML file |
|
305 |
tname: theory name |
|
306 |
suffix: suffix of complementary chart |
|
307 |
(sup if this head is for a sub-chart, sub if it is for a sup-chart; |
|
308 |
empty for Pure and CPure sub-charts) |
|
309 |
gif_path: relative path to directory containing GIFs |
|
1313 | 310 |
index_path: relative path to directory containing main theory chart |
1291 | 311 |
*) |
1317 | 312 |
fun mk_charthead file tname title repeats gif_path index_path package = |
1291 | 313 |
output (file, |
314 |
"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ |
|
315 |
"</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^ |
|
316 |
"</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^ |
|
317 |
"<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ |
|
318 |
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
|
319 |
\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
|
320 |
\\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^ |
|
1317 | 321 |
(if not repeats then "" else |
322 |
"<BR><TT>...</TT> stands for repeated subtrees") ^ |
|
1313 | 323 |
"<P><A HREF = \"" ^ tack_on index_path "index.html\ |
1291 | 324 |
\\">Back</A> to the main theory chart of " ^ package ^ ".\n<HR>\n<PRE>"); |
325 |
||
326 |
(*Convert .thy file to HTML and make chart of its super-theories*) |
|
327 |
fun thyfile2html tpath tname = |
|
328 |
let |
|
329 |
val gif_path = relative_path tpath (!gif_path); |
|
1317 | 330 |
val package = |
331 |
case rev (space_explode "/" (!index_path)) of |
|
332 |
x::xs => x |
|
333 |
| _ => error "index_path is empty. \ |
|
334 |
\Please use 'init_html()' instead of \ |
|
335 |
\'make_html := true'"; |
|
1313 | 336 |
val index_path = relative_path tpath (!index_path); |
1291 | 337 |
|
338 |
(*Make list of all theories and all theories that own a .thy file*) |
|
339 |
fun list_theories [] theories thy_files = (theories, thy_files) |
|
340 |
| list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) |
|
341 |
theories thy_files = |
|
342 |
list_theories ts (tname :: theories) |
|
343 |
(if is_some thy_time andalso the thy_time <> "" then |
|
344 |
tname :: thy_files |
|
345 |
else thy_files); |
|
346 |
||
347 |
val (theories, thy_files) = |
|
348 |
list_theories (Symtab.dest (!loaded_thys)) [] []; |
|
349 |
||
350 |
(*Do the conversion*) |
|
351 |
fun gettext thy_file = |
|
352 |
let |
|
353 |
(*Convert special HTML characters ('&', '>', and '<')*) |
|
354 |
val file = |
|
355 |
explode (execute ("sed -e 's/\\&/\\&/g' -e 's/>/\\>/g' \ |
|
356 |
\-e 's/</\\</g' " ^ thy_file)); |
|
357 |
||
358 |
(*Isolate first (possibly nested) comment; |
|
359 |
skip all leading whitespaces*) |
|
360 |
val (comment, file') = |
|
361 |
let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs) |
|
362 |
| first_comment ("*" :: ")" :: cs) co d = |
|
363 |
first_comment cs (co ^ "*)") (d-1) |
|
364 |
| first_comment ("(" :: "*" :: cs) co d = |
|
365 |
first_comment cs (co ^ "(*") (d+1) |
|
366 |
| first_comment (" " :: cs) "" 0 = first_comment cs "" 0 |
|
367 |
| first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0 |
|
368 |
| first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0 |
|
369 |
| first_comment cs "" 0 = ("", cs) |
|
370 |
| first_comment (c :: cs) co d = |
|
371 |
first_comment cs (co ^ implode [c]) d |
|
372 |
| first_comment [] co _ = |
|
373 |
error ("Unexpected end of file " ^ tname ^ ".thy."); |
|
374 |
in first_comment file "" 0 end; |
|
375 |
||
376 |
(*Process line defining theory's ancestors; |
|
377 |
convert valid theory names to links to their HTML file*) |
|
378 |
val (ancestors, body) = |
|
379 |
let |
|
380 |
fun make_links l result = |
|
381 |
let val (pre, letter) = take_prefix (not o is_letter) l; |
|
382 |
||
383 |
val (id, rest) = |
|
384 |
take_prefix (is_quasi_letter orf is_digit) letter; |
|
385 |
||
386 |
val id = implode id; |
|
387 |
||
388 |
(*Make a HTML link out of a theory name*) |
|
389 |
fun make_link t = |
|
390 |
let val path = path_of t; |
|
391 |
in "<A HREF = \"" ^ |
|
1323 | 392 |
tack_on (relative_path tpath path) ("." ^ t) ^ |
1291 | 393 |
".html\">" ^ t ^ "</A>" end; |
394 |
in if not (id mem theories) then (result, implode l) |
|
395 |
else if id mem thy_files then |
|
396 |
make_links rest (result ^ implode pre ^ make_link id) |
|
397 |
else make_links rest (result ^ implode pre ^ id) |
|
398 |
end; |
|
399 |
||
400 |
val (pre, rest) = take_prefix (fn c => c <> "=") file'; |
|
401 |
||
402 |
val (ancestors, body) = |
|
403 |
if null rest then |
|
404 |
error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\ |
|
405 |
\(Make sure that the last line ends with a linebreak.)") |
|
406 |
else |
|
407 |
make_links rest ""; |
|
408 |
in (implode pre ^ ancestors, body) end; |
|
409 |
in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^ |
|
410 |
"<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^ |
|
1313 | 411 |
tack_on index_path "index.html\ |
1291 | 412 |
\\">Back</A> to the main theory chart of " ^ package ^ |
413 |
".\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^ |
|
414 |
"</PRE>\n<HR><H2>Theorems proved in <A HREF = \"" ^ tname ^ |
|
415 |
".ML\">" ^ tname ^ ".ML</A>:</H2>\n" |
|
416 |
end; |
|
417 |
||
418 |
(** Make chart of super-theories **) |
|
419 |
||
1323 | 420 |
val sup_out = open_out (tack_on tpath ("." ^ tname ^ "_sup.html")); |
421 |
val sub_out = open_out (tack_on tpath ("." ^ tname ^ "_sub.html")); |
|
1291 | 422 |
|
423 |
(*Theories that already have been listed in this chart*) |
|
424 |
val listed = ref []; |
|
425 |
||
426 |
val wanted_theories = |
|
427 |
filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure") |
|
428 |
theories; |
|
429 |
||
430 |
(*Make nested list of theories*) |
|
431 |
fun list_ancestors tname level continued = |
|
432 |
let |
|
433 |
fun mk_entry [] = () |
|
434 |
| mk_entry (t::ts) = |
|
435 |
let |
|
436 |
val is_pure = t = "Pure" orelse t = "CPure"; |
|
437 |
val path = path_of t; |
|
1313 | 438 |
val rel_path = if is_pure then index_path |
1291 | 439 |
else relative_path tpath path; |
1317 | 440 |
val repeated = t mem (!listed) andalso not (null (parents_of t)); |
1291 | 441 |
|
442 |
fun mk_offset [] cur = |
|
443 |
if level < cur then error "Error in mk_offset" |
|
444 |
else implode (replicate (level - cur) " ") |
|
445 |
| mk_offset (l::ls) cur = |
|
446 |
implode (replicate (l - cur) " ") ^ "| " ^ |
|
447 |
mk_offset ls (l+1); |
|
448 |
in output (sup_out, |
|
449 |
" " ^ mk_offset continued 0 ^ |
|
1323 | 450 |
"\\__" ^ (if is_pure then t else |
451 |
"<A HREF=\"" ^ tack_on rel_path ("." ^ t) ^ |
|
452 |
".html\">" ^ t ^ "</A>") ^ |
|
1317 | 453 |
(if repeated then "..." else " ") ^ |
1323 | 454 |
"<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ |
1317 | 455 |
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
1291 | 456 |
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^ |
457 |
(if is_pure then "" |
|
1323 | 458 |
else "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ |
1317 | 459 |
"_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
1291 | 460 |
tack_on gif_path "blue_arrow.gif\ |
1317 | 461 |
\\" ALT = /\\></A>") ^ |
462 |
"\n"); |
|
463 |
if repeated then () |
|
464 |
else (listed := t :: (!listed); |
|
1291 | 465 |
list_ancestors t (level+1) (if null ts then continued |
466 |
else continued @ [level]); |
|
467 |
mk_entry ts) |
|
468 |
end; |
|
469 |
||
470 |
val relatives = |
|
471 |
filter (fn s => s mem wanted_theories) (parents_of tname); |
|
472 |
in mk_entry relatives end; |
|
473 |
in if is_some (!cur_htmlfile) then |
|
1323 | 474 |
error "thyfile2html: Last theory's HTML file has not been closed." |
1291 | 475 |
else (); |
1323 | 476 |
cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html"))); |
1291 | 477 |
output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); |
478 |
||
1313 | 479 |
mk_charthead sup_out tname "Ancestors" true gif_path index_path package; |
1291 | 480 |
output(sup_out, |
1323 | 481 |
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
482 |
\<A HREF = \"." ^ tname ^ |
|
1317 | 483 |
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
1291 | 484 |
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n"); |
485 |
list_ancestors tname 0 []; |
|
486 |
output (sup_out, "</PRE><HR></BODY></HTML>"); |
|
487 |
close_out sup_out; |
|
488 |
||
1313 | 489 |
mk_charthead sub_out tname "Children" false gif_path index_path package; |
1291 | 490 |
output(sub_out, |
1323 | 491 |
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ |
492 |
\<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ |
|
1317 | 493 |
tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n"); |
1291 | 494 |
close_out sub_out |
495 |
end; |
|
496 |
||
497 |
||
559 | 498 |
(*Read .thy and .ML files that haven't been read yet or have changed since |
391 | 499 |
they were last read; |
559 | 500 |
loaded_thys is a thy_info list ref containing all theories that have |
391 | 501 |
completly been read by this and preceeding use_thy calls. |
502 |
If a theory changed since its last use its children are marked as changed *) |
|
503 |
fun use_thy name = |
|
1242 | 504 |
let |
505 |
val (path, tname) = split_filename name; |
|
506 |
val (thy_file, ml_file) = get_filenames path tname; |
|
507 |
val (abs_path, _) = if thy_file = "" then split_filename ml_file |
|
508 |
else split_filename thy_file; |
|
509 |
val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file; |
|
1291 | 510 |
val old_parents = parents_of tname; |
391 | 511 |
|
1242 | 512 |
(*Set absolute path for loaded theory *) |
513 |
fun set_path () = |
|
1291 | 514 |
let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, |
515 |
thy_ss, simpset, ...} = |
|
1242 | 516 |
the (Symtab.lookup (!loaded_thys, tname)); |
517 |
in loaded_thys := Symtab.update ((tname, |
|
1291 | 518 |
ThyInfo {path = abs_path, |
519 |
children = children, parents = parents, |
|
1242 | 520 |
thy_time = thy_time, ml_time = ml_time, |
521 |
theory = theory, thms = thms, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
522 |
thy_ss = thy_ss, simpset = simpset}), |
1242 | 523 |
!loaded_thys) |
524 |
end; |
|
525 |
||
526 |
(*Mark all direct descendants of a theory as changed *) |
|
527 |
fun mark_children thy = |
|
1291 | 528 |
let val children = children_of thy; |
1242 | 529 |
val present = filter (is_some o get_thyinfo) children; |
530 |
val loaded = filter already_loaded present; |
|
531 |
in if loaded <> [] then |
|
532 |
writeln ("The following children of theory " ^ (quote thy) |
|
533 |
^ " are now out-of-date: " |
|
534 |
^ (quote (space_implode "\",\"" loaded))) |
|
535 |
else (); |
|
536 |
seq mark_outdated present |
|
537 |
end; |
|
391 | 538 |
|
1242 | 539 |
(*Remove theorems associated with a theory*) |
540 |
fun delete_thms () = |
|
541 |
let |
|
542 |
val tinfo = case get_thyinfo tname of |
|
1291 | 543 |
Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, |
544 |
thy_ss, simpset, ...}) => |
|
545 |
ThyInfo {path = path, children = children, parents = parents, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
546 |
thy_time = thy_time, ml_time = ml_time, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
547 |
theory = theory, thms = Symtab.null, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
548 |
thy_ss = thy_ss, simpset = simpset} |
1291 | 549 |
| None => ThyInfo {path = "", children = [], parents = [], |
1242 | 550 |
thy_time = None, ml_time = None, |
551 |
theory = None, thms = Symtab.null, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
552 |
thy_ss = None, simpset = None}; |
1242 | 553 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
554 |
val ThyInfo {theory, ...} = tinfo; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
555 |
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
556 |
case theory of |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
557 |
Some t => delete_thm_db t |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
558 |
| None => () |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
559 |
end; |
391 | 560 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
561 |
fun save_thy_ss () = |
1291 | 562 |
let val ThyInfo {path, children, parents, thy_time, ml_time, |
563 |
theory, thms, simpset, ...} = the (get_thyinfo tname); |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
564 |
in loaded_thys := Symtab.update |
1291 | 565 |
((tname, ThyInfo {path = path, |
566 |
children = children, parents = parents, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
567 |
thy_time = thy_time, ml_time = ml_time, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
568 |
theory = theory, thms = thms, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
569 |
thy_ss = Some (!Simplifier.simpset), |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
570 |
simpset = simpset}), |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
571 |
!loaded_thys) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
572 |
end; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
573 |
|
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
574 |
fun save_simpset () = |
1291 | 575 |
let val ThyInfo {path, children, parents, thy_time, ml_time, |
576 |
theory, thms, thy_ss, ...} = the (get_thyinfo tname); |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
577 |
in loaded_thys := Symtab.update |
1291 | 578 |
((tname, ThyInfo {path = path, |
579 |
children = children, parents = parents, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
580 |
thy_time = thy_time, ml_time = ml_time, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
581 |
theory = theory, thms = thms, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
582 |
thy_ss = thy_ss, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
583 |
simpset = Some (!Simplifier.simpset)}), |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
584 |
!loaded_thys) |
1242 | 585 |
end; |
586 |
||
1313 | 587 |
(*Add theory to file listing all loaded theories (for index.html) |
1291 | 588 |
and to the sub-charts of its parents*) |
589 |
fun mk_html () = |
|
590 |
let val new_parents = parents_of tname \\ old_parents; |
|
591 |
||
592 |
(*Add child to parents' sub-theory charts*) |
|
593 |
fun add_to_parents t = |
|
594 |
let val is_pure = t = "Pure" orelse t = "CPure"; |
|
1313 | 595 |
val path = if is_pure then (!index_path) else path_of t; |
1291 | 596 |
|
597 |
val gif_path = relative_path path (!gif_path); |
|
598 |
val rel_path = relative_path path abs_path; |
|
1323 | 599 |
val tpath = tack_on rel_path ("." ^ tname); |
1291 | 600 |
|
1323 | 601 |
val out = open_append (tack_on path ("." ^ t ^ "_sub.html")); |
1291 | 602 |
in output (out, |
1323 | 603 |
" |\n \\__<A HREF=\"" ^ |
604 |
tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^ |
|
605 |
"</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\ |
|
606 |
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
|
1291 | 607 |
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ |
1323 | 608 |
\<A HREF = \"" ^ tpath ^ "_sup.html\">\ |
1317 | 609 |
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ |
610 |
tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); |
|
1291 | 611 |
close_out out |
612 |
end; |
|
613 |
||
614 |
val theory_list = |
|
1323 | 615 |
open_append (tack_on (!index_path) ".theory_list.txt"); |
1291 | 616 |
in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); |
617 |
close_out theory_list; |
|
618 |
||
619 |
seq add_to_parents new_parents |
|
620 |
end |
|
1242 | 621 |
in if thy_uptodate andalso ml_uptodate then () |
622 |
else |
|
1291 | 623 |
(if thy_file = "" then () |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
624 |
else if thy_uptodate then |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
625 |
simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
626 |
in the thy_ss end |
391 | 627 |
else |
1242 | 628 |
(writeln ("Reading \"" ^ name ^ ".thy\""); |
1291 | 629 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
630 |
delete_thms (); |
1242 | 631 |
read_thy tname thy_file; |
632 |
use (out_name tname); |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
633 |
save_thy_ss (); |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
634 |
|
1308 | 635 |
(*Store axioms of theory |
636 |
(but only if it's not a copy of an older theory)*) |
|
637 |
let val parents = parents_of tname; |
|
638 |
val this_thy = theory_of tname; |
|
639 |
val axioms = |
|
640 |
if length parents = 1 |
|
641 |
andalso Sign.eq_sg (sign_of (theory_of (hd parents)), |
|
642 |
sign_of this_thy) then [] |
|
643 |
else axioms_of this_thy; |
|
644 |
in map store_thm_db axioms end; |
|
645 |
||
1242 | 646 |
if not (!delete_tmpfiles) then () |
1291 | 647 |
else delete_file (out_name tname); |
648 |
||
649 |
if not (!make_html) then () |
|
650 |
else thyfile2html abs_path tname |
|
1242 | 651 |
); |
652 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
653 |
set_info tname (Some (file_info thy_file)) None; |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
654 |
(*mark thy_file as successfully loaded*) |
391 | 655 |
|
1242 | 656 |
if ml_file = "" then () |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
657 |
else (writeln ("Reading \"" ^ name ^ ".ML\""); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
658 |
use ml_file); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
659 |
save_simpset (); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
660 |
|
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
661 |
(*Store theory again because it could have been redefined*) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
662 |
use_string |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
663 |
["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; |
391 | 664 |
|
1313 | 665 |
(*Add theory to list of all loaded theories (for index.html) |
1291 | 666 |
and add it to its parents' sub-charts*) |
667 |
if !make_html then |
|
668 |
let val path = path_of tname; |
|
669 |
in if path = "" then mk_html () (*first time theory has been read*) |
|
670 |
else () |
|
671 |
end |
|
672 |
else (); |
|
673 |
||
1242 | 674 |
(*Now set the correct info*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
675 |
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); |
1242 | 676 |
set_path (); |
677 |
||
678 |
(*Mark theories that have to be reloaded*) |
|
1291 | 679 |
mark_children tname; |
680 |
||
681 |
(*Close HTML file*) |
|
682 |
case !cur_htmlfile of |
|
683 |
Some out => (output (out, "<HR></BODY></HTML>\n"); |
|
684 |
close_out out; |
|
685 |
cur_htmlfile := None) |
|
686 |
| None => () |
|
1242 | 687 |
) |
688 |
end; |
|
391 | 689 |
|
690 |
fun time_use_thy tname = timeit(fn()=> |
|
559 | 691 |
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); |
391 | 692 |
use_thy tname; |
693 |
writeln("\n**** Finished Theory " ^ tname ^ " ****")) |
|
694 |
); |
|
695 |
||
696 |
(*Load all thy or ML files that have been changed and also |
|
697 |
all theories that depend on them *) |
|
698 |
fun update () = |
|
699 |
let (*List theories in the order they have to be loaded *) |
|
700 |
fun load_order [] result = result |
|
701 |
| load_order thys result = |
|
1291 | 702 |
let fun next_level [] = [] |
703 |
| next_level (t :: ts) = |
|
704 |
let val children = children_of t |
|
705 |
in children union (next_level ts) end; |
|
559 | 706 |
|
1291 | 707 |
val descendants = next_level thys; |
708 |
in load_order descendants ((result \\ descendants) @ descendants) |
|
709 |
end; |
|
391 | 710 |
|
711 |
fun reload_changed (t :: ts) = |
|
1291 | 712 |
let fun abspath () = case get_thyinfo t of |
713 |
Some (ThyInfo {path, ...}) => path |
|
714 |
| None => ""; |
|
391 | 715 |
|
716 |
val (thy_file, ml_file) = get_filenames (abspath ()) t; |
|
717 |
val (thy_uptodate, ml_uptodate) = |
|
718 |
thy_unchanged t thy_file ml_file; |
|
719 |
in if thy_uptodate andalso ml_uptodate then () |
|
720 |
else use_thy t; |
|
721 |
reload_changed ts |
|
722 |
end |
|
723 |
| reload_changed [] = (); |
|
724 |
||
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
725 |
(*Remove all theories that are no descendants of ProtoPure. |
391 | 726 |
If there are still children in the deleted theory's list |
727 |
schedule them for reloading *) |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
728 |
fun collect_garbage no_garbage = |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
729 |
let fun collect ((tname, ThyInfo {children, ...}) :: ts) = |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
730 |
if tname mem no_garbage then collect ts |
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
731 |
else (writeln ("Theory \"" ^ tname ^ |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
732 |
"\" is no longer linked with ProtoPure - removing it."); |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
733 |
remove_thy tname; |
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
734 |
seq mark_outdated children) |
391 | 735 |
| collect [] = () |
559 | 736 |
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
|
737 |
in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] [])); |
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset
|
738 |
reload_changed (load_order ["Pure", "CPure"] []) |
391 | 739 |
end; |
740 |
||
741 |
(*Merge theories to build a base for a new theory. |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
742 |
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
|
743 |
fun mk_base bases child mk_draft = |
1291 | 744 |
let (*Show the cycle that would be created by add_child*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
745 |
fun show_cycle base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
746 |
let fun find_it result curr = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
747 |
let val tinfo = get_thyinfo curr |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
748 |
in if base = curr then |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
749 |
error ("Cyclic dependency of theories: " |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
750 |
^ child ^ "->" ^ base ^ result) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
751 |
else if is_some tinfo then |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
752 |
let val ThyInfo {children, ...} = the tinfo |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
753 |
in seq (find_it ("->" ^ curr ^ result)) children |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
754 |
end |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
755 |
else () |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
756 |
end |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
757 |
in find_it "" child end; |
391 | 758 |
|
1291 | 759 |
(*Check if a cycle would be created by add_child*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
760 |
fun find_cycle base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
761 |
if base mem (get_descendants [child]) then show_cycle base |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
762 |
else (); |
559 | 763 |
|
1291 | 764 |
(*Add child to child list of base*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
765 |
fun add_child base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
766 |
let val tinfo = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
767 |
case Symtab.lookup (!loaded_thys, base) of |
1291 | 768 |
Some (ThyInfo {path, children, parents, thy_time, ml_time, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
769 |
theory, thms, thy_ss, simpset}) => |
1291 | 770 |
ThyInfo {path = path, |
771 |
children = child ins children, parents = parents, |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
772 |
thy_time = thy_time, ml_time = ml_time, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
773 |
theory = theory, thms = thms, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
774 |
thy_ss = thy_ss, simpset = simpset} |
1291 | 775 |
| None => ThyInfo {path = "", children = [child], parents = [], |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
776 |
thy_time = None, ml_time = None, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
777 |
theory = None, thms = Symtab.null, |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
778 |
thy_ss = None, simpset = None}; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
779 |
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; |
559 | 780 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
781 |
(*Load a base theory if not already done |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
782 |
and no cycle would be created *) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
783 |
fun load base = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
784 |
let val thy_loaded = already_loaded base |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
785 |
(*test this before child is added *) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
786 |
in |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
787 |
if child = base then |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
788 |
error ("Cyclic dependency of theories: " ^ child |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
789 |
^ "->" ^ child) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
790 |
else |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
791 |
(find_cycle base; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
792 |
add_child base; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
793 |
if thy_loaded then () |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
794 |
else (writeln ("Autoloading theory " ^ (quote base) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
795 |
^ " (used by " ^ (quote child) ^ ")"); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
796 |
use_thy base) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
797 |
) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
798 |
end; |
391 | 799 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
800 |
(*Get simpset for a theory*) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
801 |
fun get_simpset tname = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
802 |
let val ThyInfo {simpset, ...} = the (get_thyinfo tname); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
803 |
in simpset end; |
391 | 804 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
805 |
(*Load all needed files and make a list of all real theories *) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
806 |
fun load_base (Thy b :: bs) = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
807 |
(load b; |
1291 | 808 |
b :: load_base bs) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
809 |
| load_base (File b :: bs) = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
810 |
(load b; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
811 |
load_base bs) (*don't add it to mergelist *) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
812 |
| load_base [] = []; |
391 | 813 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
814 |
val dummy = unlink_thy child; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
815 |
val mergelist = load_base bases; |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
816 |
|
1291 | 817 |
val dummy = |
818 |
let val tinfo = case Symtab.lookup (!loaded_thys, child) of |
|
819 |
Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, |
|
820 |
thy_ss, simpset, ...}) => |
|
821 |
ThyInfo {path = path, |
|
822 |
children = children, parents = mergelist, |
|
823 |
thy_time = thy_time, ml_time = ml_time, |
|
824 |
theory = theory, thms = thms, |
|
825 |
thy_ss = thy_ss, simpset = simpset} |
|
826 |
| None => error ("set_parents: theory " ^ child ^ " not found"); |
|
827 |
in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; |
|
828 |
||
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
829 |
val base_thy = (writeln ("Loading theory " ^ (quote child)); |
1291 | 830 |
merge_thy_list mk_draft (map theory_of mergelist)); |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
831 |
in simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss); |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
832 |
base_thy |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
833 |
end; |
391 | 834 |
|
1291 | 835 |
(*Change theory object for an existent item of loaded_thys*) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
836 |
fun store_theory (thy, tname) = |
559 | 837 |
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of |
1291 | 838 |
Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
839 |
thy_ss, simpset, ...}) => |
1291 | 840 |
ThyInfo {path = path, children = children, parents = parents, |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
841 |
thy_time = thy_time, ml_time = ml_time, |
1242 | 842 |
theory = Some thy, thms = thms, |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
843 |
thy_ss = thy_ss, simpset = simpset} |
1291 | 844 |
| None => error ("store_theory: theory " ^ tname ^ " not found"); |
1132
dfb29abcf3c2
added theorem database which contains axioms and theorems indexed by the
clasohm
parents:
1098
diff
changeset
|
845 |
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
|
846 |
end; |
559 | 847 |
|
848 |
||
849 |
(** store and retrieve theorems **) |
|
850 |
||
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
851 |
(*Guess to which theory a signature belongs and return it's thy_info*) |
559 | 852 |
fun thyinfo_of_sign sg = |
853 |
let |
|
854 |
val ref xname = hd (#stamps (Sign.rep_sg sg)); |
|
855 |
val opt_info = get_thyinfo xname; |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
856 |
|
559 | 857 |
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
|
858 |
| eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy); |
559 | 859 |
|
860 |
val show_sg = Pretty.str_of o Sign.pretty_sg; |
|
861 |
in |
|
862 |
if is_some opt_info andalso eq_sg (the opt_info) then |
|
863 |
(xname, the opt_info) |
|
864 |
else |
|
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
865 |
(case Symtab.find_first (eq_sg o snd) (!loaded_thys) of |
559 | 866 |
Some name_info => name_info |
867 |
| 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
|
868 |
end; |
391 | 869 |
|
559 | 870 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
871 |
(*Try to get the theory object corresponding to a given signature*) |
559 | 872 |
fun theory_of_sign sg = |
873 |
(case thyinfo_of_sign sg of |
|
874 |
(_, ThyInfo {theory = Some thy, ...}) => thy |
|
875 |
| _ => sys_error "theory_of_sign"); |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
876 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
877 |
(*Try to get the theory object corresponding to a given theorem*) |
559 | 878 |
val theory_of_thm = theory_of_sign o #sign o rep_thm; |
879 |
||
880 |
||
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
881 |
(* Store theorems *) |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
882 |
|
1291 | 883 |
(*Store a theorem in the thy_info of its theory, |
884 |
and in the theory's HTML file*) |
|
559 | 885 |
fun store_thm (name, thm) = |
886 |
let |
|
1291 | 887 |
val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, |
888 |
theory, thms, thy_ss, simpset}) = |
|
559 | 889 |
thyinfo_of_sign (#sign (rep_thm thm)); |
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset
|
890 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
891 |
val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) |
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
892 |
handle Symtab.DUPLICATE s => |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
893 |
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then |
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset
|
894 |
(writeln ("Warning: Theory database already contains copy of\ |
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset
|
895 |
\ theorem " ^ quote name); |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
896 |
(thms, true)) |
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset
|
897 |
else error ("Duplicate theorem name " ^ quote s |
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset
|
898 |
^ " used in theory database")); |
1291 | 899 |
|
900 |
fun thm_to_html () = |
|
901 |
let fun escape [] = "" |
|
902 |
| escape ("<"::s) = "<" ^ escape s |
|
903 |
| escape (">"::s) = ">" ^ escape s |
|
904 |
| escape ("&"::s) = "&" ^ escape s |
|
905 |
| escape (c::s) = c ^ escape s; |
|
906 |
in case !cur_htmlfile of |
|
907 |
Some out => |
|
908 |
output (out, "<EM>" ^ name ^ "</EM>\n<PRE>" ^ |
|
909 |
escape (explode (string_of_thm (freeze thm))) ^ |
|
910 |
"</PRE><P>\n") |
|
911 |
| None => () |
|
912 |
end; |
|
559 | 913 |
in |
914 |
loaded_thys := Symtab.update |
|
1291 | 915 |
((thy_name, ThyInfo {path = path, children = children, parents = parents, |
1242 | 916 |
thy_time = thy_time, ml_time = ml_time, |
917 |
theory = theory, thms = thms', |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
918 |
thy_ss = thy_ss, simpset = simpset}), |
1242 | 919 |
!loaded_thys); |
1291 | 920 |
thm_to_html (); |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
921 |
if duplicate then thm else store_thm_db (name, thm) |
559 | 922 |
end; |
923 |
||
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
924 |
(*Store result of proof in loaded_thys and as ML value*) |
758 | 925 |
|
926 |
val qed_thm = ref flexpair_def(*dummy*); |
|
927 |
||
928 |
fun bind_thm (name, thm) = |
|
1291 | 929 |
(qed_thm := standard thm; |
930 |
store_thm (name, standard thm); |
|
931 |
use_string ["val " ^ name ^ " = !qed_thm;"]); |
|
758 | 932 |
|
559 | 933 |
fun qed name = |
1291 | 934 |
(qed_thm := result (); |
935 |
store_thm (name, !qed_thm); |
|
936 |
use_string ["val " ^ name ^ " = !qed_thm;"]); |
|
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
937 |
|
746 | 938 |
fun qed_goal name thy agoal tacsf = |
1291 | 939 |
(qed_thm := prove_goal thy agoal tacsf; |
940 |
store_thm (name, !qed_thm); |
|
941 |
use_string ["val " ^ name ^ " = !qed_thm;"]); |
|
746 | 942 |
|
943 |
fun qed_goalw name thy rths agoal tacsf = |
|
1291 | 944 |
(qed_thm := prove_goalw thy rths agoal tacsf; |
945 |
store_thm (name, !qed_thm); |
|
946 |
use_string ["val " ^ name ^ " = !qed_thm;"]); |
|
559 | 947 |
|
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
948 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
949 |
(* Retrieve theorems *) |
559 | 950 |
|
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
951 |
(*Get all theorems belonging to a given theory*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
952 |
fun thmtab_of_thy thy = |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
953 |
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
|
954 |
in thms end; |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
955 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
956 |
fun thmtab_of_name name = |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
957 |
let val ThyInfo {thms, ...} = the (get_thyinfo name); |
559 | 958 |
in thms end; |
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset
|
959 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
960 |
(*Get a stored theorem specified by theory and name*) |
559 | 961 |
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
|
962 |
let fun get [] [] searched = |
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
963 |
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
|
964 |
| get [] ng searched = |
871 | 965 |
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
|
966 |
| get (t::ts) ng searched = |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
967 |
(case Symtab.lookup (thmtab_of_name t, name) of |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
968 |
Some thm => thm |
1291 | 969 |
| None => get ts (ng union (parents_of t)) (t::searched)); |
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
970 |
|
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset
|
971 |
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
|
972 |
in get [tname] [] [] end; |
559 | 973 |
|
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset
|
974 |
(*Get stored theorems of a theory*) |
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
975 |
val thms_of = Symtab.dest o thmtab_of_thy; |
559 | 976 |
|
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
977 |
(*Get simpset of a theory*) |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
978 |
fun simpset_of tname = |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
979 |
case get_thyinfo tname of |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
980 |
Some (ThyInfo {simpset, ...}) => |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
981 |
if is_some simpset then the simpset |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
982 |
else error ("Simpset of theory " ^ tname ^ " has not been stored yet") |
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset
|
983 |
| None => error ("Theory " ^ tname ^ " not stored by loader"); |
559 | 984 |
|
778 | 985 |
(* print theory *) |
986 |
||
987 |
fun print_thms thy = |
|
988 |
let |
|
989 |
val thms = thms_of thy; |
|
990 |
fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1, |
|
991 |
Pretty.quote (pretty_thm th)]; |
|
992 |
in |
|
993 |
Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms)) |
|
994 |
end; |
|
995 |
||
996 |
fun print_theory thy = (Drule.print_theory thy; print_thms thy); |
|
997 |
||
1291 | 998 |
|
999 |
(* Misc HTML functions *) |
|
1000 |
||
1001 |
(*Init HTML generator by setting paths and creating new files*) |
|
1002 |
fun init_html () = |
|
1323 | 1003 |
let val pure_out = open_out ".Pure_sub.html"; |
1004 |
val cpure_out = open_out ".CPure_sub.html"; |
|
1005 |
val theory_list = close_out (open_out ".theory_list.txt"); |
|
1291 | 1006 |
|
1007 |
val rel_gif_path = relative_path (pwd ()) (!gif_path); |
|
1008 |
val package = hd (rev (space_explode "/" (pwd ()))); |
|
1009 |
in make_html := true; |
|
1313 | 1010 |
index_path := pwd(); |
1011 |
writeln ("Setting path for index.html to " ^ quote (!index_path) ^ |
|
1291 | 1012 |
"\nGIF path has been set to " ^ quote (!gif_path)); |
1013 |
||
1014 |
mk_charthead pure_out "Pure" "Children" false rel_gif_path "" package; |
|
1015 |
mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" package; |
|
1016 |
output (pure_out, "Pure\n"); |
|
1017 |
output (cpure_out, "CPure\n"); |
|
1018 |
close_out pure_out; |
|
1019 |
close_out cpure_out |
|
1020 |
end; |
|
1021 |
||
1313 | 1022 |
(*Generate index.html*) |
1291 | 1023 |
fun make_chart () = if not (!make_html) then () else |
1323 | 1024 |
let val theory_list = open_in (tack_on (!index_path) ".theory_list.txt"); |
1291 | 1025 |
val theories = space_explode "\n" (input (theory_list, 999999)); |
1026 |
val dummy = close_in theory_list; |
|
1027 |
||
1028 |
(*Path to Isabelle's main directory = $gif_path/.. *) |
|
1029 |
val base_path = "/" ^ |
|
1030 |
space_implode "/" (rev (tl (rev (space_explode "/" (!gif_path))))); |
|
1031 |
||
1313 | 1032 |
val gif_path = relative_path (!index_path) (!gif_path); |
1291 | 1033 |
|
1034 |
(*Make entry for main chart of all theories.*) |
|
1035 |
fun main_entries [] curdir = |
|
1036 |
implode (replicate (length curdir -1) "</UL>\n") |
|
1037 |
| main_entries (t::ts) curdir = |
|
1038 |
let |
|
1039 |
val (name, path) = take_prefix (not_equal " ") (explode t); |
|
1040 |
||
1041 |
val tname = implode name |
|
1042 |
val tpath = |
|
1313 | 1043 |
tack_on (relative_path (!index_path) (implode (tl path))) |
1323 | 1044 |
("." ^ tname); |
1291 | 1045 |
val subdir = space_explode "/" |
1046 |
(relative_path base_path (implode (tl path))); |
|
1047 |
val level_diff = length subdir - length curdir; |
|
1048 |
in "\n" ^ |
|
1049 |
(if subdir <> curdir then |
|
1050 |
(implode (if level_diff > 0 then |
|
1051 |
replicate level_diff "<UL>\n" |
|
1052 |
else if level_diff < 0 then |
|
1053 |
replicate (~level_diff) "</UL>\n" |
|
1054 |
else []) ^ |
|
1055 |
"<H3>" ^ space_implode "/" subdir ^ "</H3>\n") |
|
1056 |
else "") ^ |
|
1057 |
"<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^ |
|
1320 | 1058 |
tack_on gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^ |
1291 | 1059 |
"<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^ |
1060 |
tack_on gif_path "blue_arrow.gif\ |
|
1320 | 1061 |
\\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^ |
1291 | 1062 |
".html\">" ^ tname ^ "</A><BR>\n" ^ |
1063 |
main_entries ts subdir |
|
1064 |
end; |
|
1065 |
||
1313 | 1066 |
val out = open_out (tack_on (!index_path) "index.html"); |
1067 |
val subdir = relative_path base_path (!index_path); |
|
1291 | 1068 |
in output (out, |
1069 |
"<HTML><HEAD><TITLE>Isabelle/" ^ subdir ^ "</TITLE></HEAD>\n\ |
|
1070 |
\<H2>Isabelle/" ^ subdir ^ "</H2>\n\ |
|
1071 |
\The name of every theory is linked to its theory file<BR>\n\ |
|
1072 |
\<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ |
|
1073 |
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
|
1074 |
\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
|
1075 |
\\" ALT = /\\></A> stands for supertheories (parent theories)\n\ |
|
1076 |
\<P><A HREF = \"" ^ |
|
1313 | 1077 |
tack_on (relative_path (!index_path) base_path) "index.html\">\ |
1291 | 1078 |
\Back</A> to the index of Isabelle logics.\n<HR>" ^ |
1079 |
main_entries theories (space_explode "/" base_path) ^ |
|
1080 |
"</BODY></HTML>\n"); |
|
1081 |
close_out out |
|
1082 |
end; |
|
391 | 1083 |
end; |