author  clasohm 
Fri, 15 Jul 1994 13:30:42 +0200  
changeset 476  836cad329311 
parent 426  767367131b47 
child 559  00365d2e0c50 
permissions  rwrr 
391  1 
(* Title: Pure/Thy/thy_read.ML 
2 
ID: $Id$ 

412  3 
Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson / Carsten Clasohm 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

4 
Copyright 1994 TU Muenchen 
391  5 

6 
Reading and writing the theory definition files. 

7 

8 
For theory XXX, the input file is called XXX.thy 

9 
the output file is called .XXX.thy.ML 

10 
and it then tries to read XXX.ML 

11 
*) 

12 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

13 
datatype thy_info = ThyInfo of {path: string, 
391  14 
children: string list, 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

15 
thy_time: string option, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

16 
ml_time: string option, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

17 
theory: Thm.theory option, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

18 
thms: thm Symtab.table}; 
391  19 

412  20 
signature READTHY = 
391  21 
sig 
22 
datatype basetype = Thy of string 

23 
 File of string 

24 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

25 
val loaded_thys : thy_info Symtab.table ref 
391  26 
val loadpath : string list ref 
27 
val delete_tmpfiles: bool ref 

28 

29 
val use_thy : string > unit 

30 
val update : unit > unit 

31 
val time_use_thy : string > unit 

32 
val unlink_thy : string > unit 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

33 
val base_on : basetype list > string > bool > theory 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

34 
val store_theory : theory * string > unit 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

35 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

36 
val store_thm : thm * string > thm 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

37 
val qed : string > unit 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

38 
val get_thm : theory > string > thm 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

39 
val get_thms : theory > (string * thm) list 
391  40 
end; 
41 

42 

412  43 
functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY = 
391  44 
struct 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

45 
open Symtab; 
391  46 

47 
datatype basetype = Thy of string 

48 
 File of string; 

49 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

50 
val loaded_thys = ref (make [("Pure", ThyInfo {path = "", children = [], 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

51 
thy_time = Some "", ml_time = Some "", 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

52 
theory = Some pure_thy, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

53 
thms = null})]); 
391  54 

55 
val loadpath = ref ["."]; (*default search path for theory files *) 

56 

57 
val delete_tmpfiles = ref true; (*remove temporary files after use *) 

58 

59 
(*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

60 
fun out_name tname = "." ^ tname ^ ".thy.ML"; 
391  61 

62 
(*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

63 
fun read_thy tname thy_file = 
391  64 
let 
65 
val instream = open_in thy_file; 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

66 
val outstream = open_out (out_name tname); 
391  67 
in 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

68 
output (outstream, ThySyn.parse tname (input (instream, 999999))); 
391  69 
close_out outstream; 
70 
close_in instream 

71 
end; 

72 

73 
fun file_exists file = 

74 
let val instream = open_in file in close_in instream; true end 

75 
handle Io _ => false; 

76 

77 
(*Get thy_info for a loaded theory *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

78 
fun get_thyinfo tname = lookup (!loaded_thys, tname); 
391  79 

80 
(*Check if a theory was already loaded *) 

81 
fun already_loaded thy = 

82 
let val t = get_thyinfo thy 

83 
in if is_none t then false 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

84 
else let val ThyInfo {thy_time, ml_time, ...} = the t 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

85 
in if is_none thy_time orelse is_none ml_time then false 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

86 
else true 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

87 
end 
391  88 
end; 
89 

90 
(*Check if a theory file has changed since its last use. 

91 
Return a pair of boolean values for .thy and for .ML *) 

92 
fun thy_unchanged thy thy_file ml_file = 

93 
let val t = get_thyinfo thy 

94 
in if is_some t then 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

95 
let val ThyInfo {thy_time, ml_time, ...} = the t 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

96 
val tn = is_none thy_time; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

97 
val mn = is_none ml_time 
391  98 
in if not tn andalso not mn then 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

99 
((file_info thy_file = the thy_time), 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

100 
(file_info ml_file = the ml_time)) 
391  101 
else if not tn andalso mn then (true, false) 
102 
else (false, false) 

103 
end 

104 
else (false, false) 

105 
end; 

106 

107 
exception FILE_NOT_FOUND; (*raised by find_file *) 

108 

109 
(*Find a file using a list of paths if no absolute or relative path is 

110 
specified.*) 

111 
fun find_file "" name = 

112 
let fun find_it (curr :: paths) = 

113 
if file_exists (tack_on curr name) then 

114 
tack_on curr name 

115 
else 

116 
find_it paths 

117 
 find_it [] = "" 

118 
in find_it (!loadpath) end 

119 
 find_file path name = 

120 
if file_exists (tack_on path name) then tack_on path name 

121 
else ""; 

122 

123 
(*Get absolute pathnames for a new or already loaded theory *) 

124 
fun get_filenames path name = 

125 
let fun make_absolute file = 

126 
if file = "" then "" else 

127 
if hd (explode file) = "/" then file else tack_on (pwd ()) file; 

128 

129 
fun new_filename () = 

130 
let val found = find_file path (name ^ ".thy") 

131 
handle FILE_NOT_FOUND => ""; 

132 
val thy_file = make_absolute found; 

133 
val (thy_path, _) = split_filename thy_file; 

134 
val found = find_file path (name ^ ".ML"); 

135 
val ml_file = if thy_file = "" then make_absolute found 

136 
else if file_exists (tack_on thy_path (name ^ ".ML")) 

137 
then tack_on thy_path (name ^ ".ML") 

138 
else ""; 

139 
val searched_dirs = if path = "" then (!loadpath) else [path] 

140 
in if thy_file = "" andalso ml_file = "" then 

141 
error ("Could not find file \"" ^ name ^ ".thy\" or \"" 

142 
^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" 

143 
^ "in the following directories: \"" ^ 

144 
(space_implode "\", \"" searched_dirs) ^ "\"") 

145 
else (); 

146 
(thy_file, ml_file) 

147 
end; 

148 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

149 
val tinfo = get_thyinfo name; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

150 
in if is_some tinfo andalso path = "" then 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

151 
let val ThyInfo {path = abs_path, ...} = the tinfo; 
391  152 
val (thy_file, ml_file) = if abs_path = "" then new_filename () 
153 
else (find_file abs_path (name ^ ".thy"), 

154 
find_file abs_path (name ^ ".ML")) 

155 
in if thy_file = "" andalso ml_file = "" then 

156 
(writeln ("Warning: File \"" ^ (tack_on path name) 

157 
^ ".thy\"\ncontaining theory \"" ^ name 

158 
^ "\" no longer exists."); 

159 
new_filename () 

160 
) 

161 
else (thy_file, ml_file) 

162 
end 

163 
else new_filename () 

164 
end; 

165 

166 
(*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

167 
fun unlink_thy tname = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

168 
let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

169 
ThyInfo {path = path, children = children \ tname, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

170 
thy_time = thy_time, ml_time = ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

171 
theory = theory, thms = thms} 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

172 
in loaded_thys := mapst remove (!loaded_thys) end; 
391  173 

174 
(*Remove a theory from loaded_thys *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

175 
fun remove_thy tname = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

176 
loaded_thys := make (filter_out (fn (id, _) => id = tname) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

177 
(alist_of (!loaded_thys))); 
391  178 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

179 
(*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

180 
fun set_info thy_time ml_time tname = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

181 
let val ThyInfo {path, children, theory, thms, ...} = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

182 
the (lookup (!loaded_thys, tname)); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

183 
in loaded_thys := update ((tname, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

184 
ThyInfo {path = path, children = children, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

185 
thy_time = Some thy_time, ml_time = Some ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

186 
theory = theory, thms = thms}), !loaded_thys) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

187 
end; 
391  188 

189 
(*Mark theory as changed since last read if it has been completly read *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

190 
fun mark_outdated tname = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

191 
if already_loaded tname then set_info "" "" tname else (); 
391  192 

193 
(*Read .thy and .ML files that haven't been read yet or have changed since 

194 
they were last read; 

195 
loaded_thys is a thy_info list ref containing all theories that have 

196 
completly been read by this and preceeding use_thy calls. 

197 
If a theory changed since its last use its children are marked as changed *) 

198 
fun use_thy name = 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

199 
let val (path, tname) = split_filename name; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

200 
val (thy_file, ml_file) = get_filenames path tname; 
391  201 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 
202 
else split_filename thy_file; 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

203 
val (thy_uptodate, ml_uptodate) = thy_unchanged tname 
391  204 
thy_file ml_file; 
205 

206 
(*Set absolute path for loaded theory *) 

207 
fun set_path () = 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

208 
let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

209 
the (lookup (!loaded_thys, tname)); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

210 
in loaded_thys := update ((tname, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

211 
ThyInfo {path = abs_path, children = children, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

212 
thy_time = thy_time, ml_time = ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

213 
theory = theory, thms = thms}), 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

214 
!loaded_thys) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

215 
end; 
391  216 

217 
(*Mark all direct descendants of a theory as changed *) 

218 
fun mark_children thy = 

219 
let val ThyInfo {children, ...} = the (get_thyinfo thy) 

220 
val loaded = filter already_loaded children 

221 
in if loaded <> [] then 

222 
(writeln ("The following children of theory " ^ (quote thy) 

223 
^ " are now outofdate: " 

224 
^ (quote (space_implode "\",\"" loaded))); 

225 
seq mark_outdated loaded 

226 
) 

227 
else () 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

228 
end; 
391  229 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

230 
(*Remove all theorems associated with a theory*) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

231 
fun delete_thms () = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

232 
let val tinfo = case lookup (!loaded_thys, tname) of 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

233 
Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) => 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

234 
ThyInfo {path = path, children = children, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

235 
thy_time = thy_time, ml_time = ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

236 
theory = theory, thms = null} 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

237 
 None => ThyInfo {path = "", children = [], 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

238 
thy_time = None, ml_time = None, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

239 
theory = None, thms = null}; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

240 
in loaded_thys := update ((tname, tinfo), !loaded_thys) end; 
391  241 
in if thy_uptodate andalso ml_uptodate then () 
242 
else 

243 
( 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

244 
delete_thms (); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

245 

391  246 
if thy_uptodate orelse thy_file = "" then () 
247 
else (writeln ("Reading \"" ^ name ^ ".thy\""); 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

248 
read_thy tname thy_file; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

249 
use (out_name tname) 
391  250 
); 
251 

252 
if ml_file = "" then () 

253 
else (writeln ("Reading \"" ^ name ^ ".ML\""); 

254 
use ml_file); 

255 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

256 
use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; 
391  257 

258 
(*Now set the correct info*) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

259 
set_info (file_info thy_file) (file_info ml_file) tname; 
391  260 
set_path (); 
261 

262 
(*Mark theories that have to be reloaded*) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

263 
mark_children tname; 
391  264 

265 
(*Remove temporary files*) 

266 
if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 

267 
then () 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

268 
else delete_file (out_name tname) 
391  269 
) 
270 
end; 

271 

272 
fun time_use_thy tname = timeit(fn()=> 

273 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 

274 
use_thy tname; 

275 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

276 
); 

277 

278 
(*Load all thy or ML files that have been changed and also 

279 
all theories that depend on them *) 

280 
fun update () = 

281 
let (*List theories in the order they have to be loaded *) 

282 
fun load_order [] result = result 

283 
 load_order thys result = 

284 
let fun next_level (t :: ts) = 

285 
let val thy = get_thyinfo t 

286 
in if is_some thy then 

287 
let val ThyInfo {children, ...} = the thy 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

288 
in children union (next_level ts) end 
391  289 
else next_level ts 
290 
end 

291 
 next_level [] = []; 

292 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

293 
val children = next_level thys; 
391  294 
in load_order children ((result \\ children) @ children) end; 
295 

296 
fun reload_changed (t :: ts) = 

297 
let val thy = get_thyinfo t; 

298 

299 
fun abspath () = 

300 
if is_some thy then 

301 
let val ThyInfo {path, ...} = the thy in path end 

302 
else ""; 

303 

304 
val (thy_file, ml_file) = get_filenames (abspath ()) t; 

305 
val (thy_uptodate, ml_uptodate) = 

306 
thy_unchanged t thy_file ml_file; 

307 
in if thy_uptodate andalso ml_uptodate then () 

308 
else use_thy t; 

309 
reload_changed ts 

310 
end 

311 
 reload_changed [] = (); 

312 

313 
(*Remove all theories that are no descendants of Pure. 

314 
If there are still children in the deleted theory's list 

315 
schedule them for reloading *) 

316 
fun collect_garbage not_garbage = 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

317 
let fun collect ((tname, ThyInfo {children, ...}) :: ts) = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

318 
if tname mem not_garbage then collect ts 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

319 
else (writeln ("Theory \"" ^ tname 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

320 
^ "\" is no longer linked with Pure  removing it."); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

321 
remove_thy tname; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

322 
seq mark_outdated children) 
391  323 
 collect [] = () 
324 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

325 
in collect (alist_of (!loaded_thys)) end; 
391  326 
in collect_garbage ("Pure" :: (load_order ["Pure"] [])); 
327 
reload_changed (load_order ["Pure"] []) 

328 
end; 

329 

330 
(*Merge theories to build a base for a new theory. 

331 
Base members are only loaded if they are missing. *) 

424  332 
fun base_on bases child mk_draft = 
391  333 
let (*List all descendants of a theory list *) 
334 
fun list_descendants (t :: ts) = 

335 
let val tinfo = get_thyinfo t 

336 
in if is_some tinfo then 

337 
let val ThyInfo {children, ...} = the tinfo 

338 
in children union (list_descendants (ts union children)) 

339 
end 

340 
else [] 

341 
end 

342 
 list_descendants [] = []; 

343 

344 
(*Show the cycle that would be created by add_child *) 

345 
fun show_cycle base = 

346 
let fun find_it result curr = 

347 
let val tinfo = get_thyinfo curr 

348 
in if base = curr then 

349 
error ("Cyclic dependency of theories: " 

350 
^ child ^ ">" ^ base ^ result) 

351 
else if is_some tinfo then 

352 
let val ThyInfo {children, ...} = the tinfo 

353 
in seq (find_it (">" ^ curr ^ result)) children 

354 
end 

355 
else () 

356 
end 

357 
in find_it "" child end; 

358 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

359 
(*Check if a cycle would be created by add_child *) 
391  360 
fun find_cycle base = 
361 
if base mem (list_descendants [child]) then show_cycle base 

362 
else (); 

363 

364 
(*Add child to child list of base *) 

365 
fun add_child base = 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

366 
let val tinfo = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

367 
case lookup (!loaded_thys, base) of 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

368 
Some (ThyInfo {path, children, thy_time, ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

369 
theory, thms}) => 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

370 
ThyInfo {path = path, children = child ins children, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

371 
thy_time = thy_time, ml_time = ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

372 
theory = theory, thms = thms} 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

373 
 None => ThyInfo {path = "", children = [child], 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

374 
thy_time = None, ml_time = None, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

375 
theory = None, thms = null}; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

376 
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; 
391  377 

378 
(*Load a base theory if not already done 

379 
and no cycle would be created *) 

380 
fun load base = 

381 
let val thy_present = already_loaded base 

426
767367131b47
replaced "foldl merge_theories" by "merge_thy_list" in base_on
clasohm
parents:
424
diff
changeset

382 
(*test this before child is added *) 
391  383 
in 
384 
if child = base then 

385 
error ("Cyclic dependency of theories: " ^ child 

386 
^ ">" ^ child) 

387 
else 

388 
(find_cycle base; 

389 
add_child base; 

390 
if thy_present then () 

391 
else (writeln ("Autoloading theory " ^ (quote base) 

392 
^ " (used by " ^ (quote child) ^ ")"); 

393 
use_thy base) 

394 
) 

395 
end; 

396 

397 
(*Load all needed files and make a list of all real theories *) 

398 
fun load_base (Thy b :: bs) = 

399 
(load b; 

400 
b :: (load_base bs)) 

401 
 load_base (File b :: bs) = 

402 
(load b; 

403 
load_base bs) (*don't add it to merge_theories' parameter *) 

404 
 load_base [] = []; 

405 

406 
(*Get theory object for a loaded theory *) 

407 
fun get_theory name = 

408 
let val ThyInfo {theory, ...} = the (get_thyinfo name) 

409 
in the theory end; 

410 

411 
val mergelist = (unlink_thy child; 

412 
load_base bases); 

413 
in writeln ("Loading theory " ^ (quote child)); 

426
767367131b47
replaced "foldl merge_theories" by "merge_thy_list" in base_on
clasohm
parents:
424
diff
changeset

414 
merge_thy_list mk_draft (map get_theory mergelist) end; 
391  415 

416 
(*Change theory object for an existent item of loaded_thys 

417 
or create a new item *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

418 
fun store_theory (thy, tname) = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

419 
let val tinfo = case lookup (!loaded_thys, tname) of 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

420 
Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) => 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

421 
ThyInfo {path = path, children = children, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

422 
thy_time = thy_time, ml_time = ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

423 
theory = Some thy, thms = thms} 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

424 
 None => ThyInfo {path = "", children = [], 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

425 
thy_time = Some "", ml_time = Some "", 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

426 
theory = Some thy, thms = null}; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

427 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

428 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

429 
(*Store a theorem in the ThyInfo of the theory it is associated with*) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

430 
fun store_thm (thm, tname) = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

431 
let val thy_name = !(hd (stamps_of_thm thm)); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

432 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

433 
val ThyInfo {path, children, thy_time, ml_time, theory, thms} = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

434 
case get_thyinfo thy_name of 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

435 
Some tinfo => tinfo 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

436 
 None => error ("store_thm: Theory \"" ^ thy_name 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

437 
^ "\" is not stored in loaded_thys"); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

438 
in loaded_thys := 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

439 
Symtab.update ((thy_name, ThyInfo {path = path, children = children, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

440 
thy_time = thy_time, ml_time = ml_time, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

441 
theory = theory, 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

442 
thms = Symtab.update ((tname, thm), thms)}), 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

443 
!loaded_thys); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

444 
thm 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

445 
end; 
391  446 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

447 
(*Store theorem in loaded_thys and a ML variable*) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

448 
fun qed name = use_string ["val " ^ name ^ " = store_thm (result(), " 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

449 
^ quote name ^ ");"]; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

450 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

451 
fun name_of_thy thy = !(hd (stamps_of_thy thy)); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

452 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

453 
(*Retrieve a theorem specified by theory and name*) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

454 
fun get_thm thy tname = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

455 
let val thy_name = name_of_thy thy; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

456 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

457 
val ThyInfo {thms, ...} = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

458 
case get_thyinfo thy_name of 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

459 
Some tinfo => tinfo 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

460 
 None => error ("get_thm: Theory \"" ^ thy_name 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

461 
^ "\" is not stored in loaded_thys"); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

462 
in the (lookup (thms, tname)) end; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

463 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

464 
(*Retrieve all theorems belonging to the specified theory*) 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

465 
fun get_thms thy = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

466 
let val thy_name = name_of_thy thy; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

467 

836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

468 
val ThyInfo {thms, ...} = 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

469 
case get_thyinfo thy_name of 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

470 
Some tinfo => tinfo 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

471 
 None => error ("get_thms: Theory \"" ^ thy_name 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

472 
^ "\" is not stored in loaded_thys"); 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

473 
in alist_of thms end; 
391  474 
end; 