author  wenzelm 
Fri, 19 Aug 1994 15:39:19 +0200  
changeset 559  00365d2e0c50 
parent 476  836cad329311 
child 586  201e115d8031 
permissions  rwrr 
391  1 
(* Title: Pure/Thy/thy_read.ML 
2 
ID: $Id$ 

559  3 
Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and 
4 
Tobias Nipkow and L C Paulson 

5 
Copyright 1994 TU Muenchen 

391  6 

559  7 
(* FIXME !? *) 
391  8 
Reading and writing the theory definition files. 
9 

559  10 
(* FIXME !? *) 
391  11 
For theory XXX, the input file is called XXX.thy 
12 
the output file is called .XXX.thy.ML 

13 
and it then tries to read XXX.ML 

14 
*) 

15 

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

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

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

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

21 
thms: thm Symtab.table}; 
391  22 

412  23 
signature READTHY = 
391  24 
sig 
25 
datatype basetype = Thy of string 

26 
 File of string 

27 

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

28 
val loaded_thys : thy_info Symtab.table ref 
391  29 
val loadpath : string list ref 
30 
val delete_tmpfiles: bool ref 

31 

32 
val use_thy : string > unit 

33 
val update : unit > unit 

34 
val time_use_thy : string > unit 

35 
val unlink_thy : string > unit 

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

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

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

38 

559  39 
val theory_of_sign: Sign.sg > theory 
40 
val theory_of_thm: thm > theory 

41 
val store_thm: string * thm > thm 

42 
val qed: string > unit 

43 
val get_thm: theory > string > thm 

44 
val thms_of: theory > (string * thm) list 

391  45 
end; 
46 

47 

412  48 
functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY = 
391  49 
struct 
50 

51 
datatype basetype = Thy of string 

52 
 File of string; 

53 

559  54 
val loaded_thys = ref (Symtab.make [("Pure", ThyInfo {path = "", children = [], 
55 
thy_time = Some "", ml_time = Some "", 

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

56 
theory = Some pure_thy, 
559  57 
thms = Symtab.null})]); 
391  58 

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

60 

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

62 

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

64 
fun out_name tname = "." ^ tname ^ ".thy.ML"; 
391  65 

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

67 
fun read_thy tname thy_file = 
559  68 
let 
391  69 
val instream = open_in thy_file; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

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

72 
output (outstream, ThySyn.parse tname (input (instream, 999999))); 
391  73 
close_out outstream; 
74 
close_in instream 

75 
end; 

76 

77 
fun file_exists file = 

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

79 
handle Io _ => false; 

80 

81 
(*Get thy_info for a loaded theory *) 

559  82 
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); 
391  83 

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

85 
fun already_loaded thy = 

86 
let val t = get_thyinfo thy 

87 
in if is_none t then false 

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

88 
else let val ThyInfo {thy_time, ml_time, ...} = the t 
559  89 
in if is_none thy_time orelse is_none ml_time then false 
90 
else true 

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

91 
end 
391  92 
end; 
93 

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

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

559  96 
fun thy_unchanged thy thy_file ml_file = 
391  97 
let val t = get_thyinfo thy 
98 
in if is_some t then 

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

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

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

101 
val mn = is_none ml_time 
391  102 
in if not tn andalso not mn then 
559  103 
((file_info thy_file = the thy_time), 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

104 
(file_info ml_file = the ml_time)) 
391  105 
else if not tn andalso mn then (true, false) 
106 
else (false, false) 

107 
end 

108 
else (false, false) 

109 
end; 

110 

111 
exception FILE_NOT_FOUND; (*raised by find_file *) 

112 

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

114 
specified.*) 

115 
fun find_file "" name = 

116 
let fun find_it (curr :: paths) = 

117 
if file_exists (tack_on curr name) then 

118 
tack_on curr name 

559  119 
else 
391  120 
find_it paths 
121 
 find_it [] = "" 

122 
in find_it (!loadpath) end 

123 
 find_file path name = 

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

125 
else ""; 

126 

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

128 
fun get_filenames path name = 

129 
let fun make_absolute file = 

559  130 
if file = "" then "" else 
391  131 
if hd (explode file) = "/" then file else tack_on (pwd ()) file; 
132 

133 
fun new_filename () = 

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

135 
handle FILE_NOT_FOUND => ""; 

136 
val thy_file = make_absolute found; 

137 
val (thy_path, _) = split_filename thy_file; 

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

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

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

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

142 
else ""; 

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

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

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

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

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

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

149 
else (); 

559  150 
(thy_file, ml_file) 
391  151 
end; 
152 

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

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

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

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

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

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

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

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

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

163 
new_filename () 

164 
) 

165 
else (thy_file, ml_file) 

166 
end 

167 
else new_filename () 

168 
end; 

169 

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

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

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

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

175 
theory = theory, thms = thms} 
559  176 
in loaded_thys := Symtab.map remove (!loaded_thys) end; 
391  177 

178 
(*Remove a theory from loaded_thys *) 

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

179 
fun remove_thy tname = 
559  180 
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) 
181 
(Symtab.dest (!loaded_thys))); 

391  182 

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

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

184 
fun set_info thy_time ml_time tname = 
559  185 
let val ThyInfo {path, children, theory, thms, ...} = 
186 
the (Symtab.lookup (!loaded_thys, tname)); 

187 
in loaded_thys := Symtab.update ((tname, 

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

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

189 
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

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

191 
end; 
391  192 

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

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

195 
if already_loaded tname then set_info "" "" tname else (); 
391  196 

559  197 
(*Read .thy and .ML files that haven't been read yet or have changed since 
391  198 
they were last read; 
559  199 
loaded_thys is a thy_info list ref containing all theories that have 
391  200 
completly been read by this and preceeding use_thy calls. 
201 
If a theory changed since its last use its children are marked as changed *) 

202 
fun use_thy name = 

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

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

204 
val (thy_file, ml_file) = get_filenames path tname; 
391  205 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 
206 
else split_filename thy_file; 

559  207 
val (thy_uptodate, ml_uptodate) = thy_unchanged tname 
391  208 
thy_file ml_file; 
209 

210 
(*Set absolute path for loaded theory *) 

211 
fun set_path () = 

559  212 
let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} = 
213 
the (Symtab.lookup (!loaded_thys, tname)); 

214 
in loaded_thys := Symtab.update ((tname, 

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

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

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

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

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

219 
end; 
391  220 

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

222 
fun mark_children thy = 

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

224 
val loaded = filter already_loaded children 

225 
in if loaded <> [] then 

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

227 
^ " are now outofdate: " 

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

229 
seq mark_outdated loaded 

230 
) 

231 
else () 

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

232 
end; 
391  233 

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

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

235 
fun delete_thms () = 
559  236 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

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

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

239 
thy_time = thy_time, ml_time = ml_time, 
559  240 
theory = theory, thms = Symtab.null} 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

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

242 
thy_time = None, ml_time = None, 
559  243 
theory = None, thms = Symtab.null}; 
244 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; 

391  245 
in if thy_uptodate andalso ml_uptodate then () 
246 
else 

247 
( 

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

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

249 

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

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

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

253 
use (out_name tname) 
391  254 
); 
255 

559  256 
if ml_file = "" then () 
391  257 
else (writeln ("Reading \"" ^ name ^ ".ML\""); 
258 
use ml_file); 

259 

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

260 
use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; 
391  261 

262 
(*Now set the correct info*) 

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

263 
set_info (file_info thy_file) (file_info ml_file) tname; 
391  264 
set_path (); 
265 

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

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

267 
mark_children tname; 
391  268 

269 
(*Remove temporary files*) 

559  270 
if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 
391  271 
then () 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

272 
else delete_file (out_name tname) 
391  273 
) 
274 
end; 

275 

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

559  277 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
391  278 
use_thy tname; 
279 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

280 
); 

281 

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

283 
all theories that depend on them *) 

284 
fun update () = 

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

286 
fun load_order [] result = result 

287 
 load_order thys result = 

288 
let fun next_level (t :: ts) = 

289 
let val thy = get_thyinfo t 

290 
in if is_some thy then 

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

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

292 
in children union (next_level ts) end 
391  293 
else next_level ts 
294 
end 

295 
 next_level [] = []; 

559  296 

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

297 
val children = next_level thys; 
391  298 
in load_order children ((result \\ children) @ children) end; 
299 

300 
fun reload_changed (t :: ts) = 

301 
let val thy = get_thyinfo t; 

302 

303 
fun abspath () = 

304 
if is_some thy then 

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

306 
else ""; 

307 

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

309 
val (thy_uptodate, ml_uptodate) = 

310 
thy_unchanged t thy_file ml_file; 

311 
in if thy_uptodate andalso ml_uptodate then () 

312 
else use_thy t; 

313 
reload_changed ts 

314 
end 

315 
 reload_changed [] = (); 

316 

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

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

319 
schedule them for reloading *) 

320 
fun collect_garbage not_garbage = 

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

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

322 
if tname mem not_garbage then collect ts 
559  323 
else (writeln ("Theory \"" ^ tname 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

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

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

326 
seq mark_outdated children) 
391  327 
 collect [] = () 
328 

559  329 
in collect (Symtab.dest (!loaded_thys)) end; 
391  330 
in collect_garbage ("Pure" :: (load_order ["Pure"] [])); 
331 
reload_changed (load_order ["Pure"] []) 

332 
end; 

333 

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

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

424  336 
fun base_on bases child mk_draft = 
391  337 
let (*List all descendants of a theory list *) 
338 
fun list_descendants (t :: ts) = 

339 
let val tinfo = get_thyinfo t 

340 
in if is_some tinfo then 

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

342 
in children union (list_descendants (ts union children)) 

343 
end 

344 
else [] 

345 
end 

346 
 list_descendants [] = []; 

347 

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

349 
fun show_cycle base = 

350 
let fun find_it result curr = 

351 
let val tinfo = get_thyinfo curr 

559  352 
in if base = curr then 
391  353 
error ("Cyclic dependency of theories: " 
354 
^ child ^ ">" ^ base ^ result) 

355 
else if is_some tinfo then 

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

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

358 
end 

359 
else () 

360 
end 

361 
in find_it "" child end; 

559  362 

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

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

366 
else (); 

559  367 

391  368 
(*Add child to child list of base *) 
369 
fun add_child base = 

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

370 
let val tinfo = 
559  371 
case Symtab.lookup (!loaded_thys, base) of 
372 
Some (ThyInfo {path, children, thy_time, ml_time, 

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

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

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

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

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

377 
 None => ThyInfo {path = "", children = [child], 
559  378 
thy_time = None, ml_time = None, 
379 
theory = None, thms = Symtab.null}; 

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

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

382 
(*Load a base theory if not already done 

383 
and no cycle would be created *) 

384 
fun load base = 

385 
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

386 
(*test this before child is added *) 
391  387 
in 
388 
if child = base then 

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

390 
^ ">" ^ child) 

559  391 
else 
391  392 
(find_cycle base; 
393 
add_child base; 

394 
if thy_present then () 

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

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

397 
use_thy base) 

398 
) 

559  399 
end; 
391  400 

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

402 
fun load_base (Thy b :: bs) = 

403 
(load b; 

404 
b :: (load_base bs)) 

405 
 load_base (File b :: bs) = 

406 
(load b; 

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

408 
 load_base [] = []; 

409 

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

411 
fun get_theory name = 

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

413 
in the theory end; 

414 

415 
val mergelist = (unlink_thy child; 

416 
load_base bases); 

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

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

418 
merge_thy_list mk_draft (map get_theory mergelist) end; 
391  419 

559  420 
(*Change theory object for an existent item of loaded_thys 
391  421 
or create a new item *) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

422 
fun store_theory (thy, tname) = 
559  423 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

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

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

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

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

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

429 
thy_time = Some "", ml_time = Some "", 
559  430 
theory = Some thy, thms = Symtab.null}; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

431 
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

432 

559  433 

434 

435 
(** store and retrieve theorems **) 

436 

437 
(* thyinfo_of_sign *) 

438 

439 
fun thyinfo_of_sign sg = 

440 
let 

441 
val ref xname = hd (#stamps (Sign.rep_sg sg)); 

442 
val opt_info = get_thyinfo xname; 

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

443 

559  444 
fun eq_sg (ThyInfo {theory = None, ...}) = false 
445 
 eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg, sign_of thy); 

446 

447 
val show_sg = Pretty.str_of o Sign.pretty_sg; 

448 
in 

449 
if is_some opt_info andalso eq_sg (the opt_info) then 

450 
(xname, the opt_info) 

451 
else 

452 
(case Symtab.find_first (eq_sg o snd) (! loaded_thys) of 

453 
Some name_info => name_info 

454 
 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

455 
end; 
391  456 

559  457 

458 
(* theory_of_sign, theory_of_thm *) 

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

459 

559  460 
fun theory_of_sign sg = 
461 
(case thyinfo_of_sign sg of 

462 
(_, ThyInfo {theory = Some thy, ...}) => thy 

463 
 _ => sys_error "theory_of_sign"); 

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

464 

559  465 
val theory_of_thm = theory_of_sign o #sign o rep_thm; 
466 

467 

468 
(* store theorems *) 

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

469 

559  470 
(*store a theorem in the thy_info of its theory*) 
471 
fun store_thm (name, thm) = 

472 
let 

473 
val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms}) = 

474 
thyinfo_of_sign (#sign (rep_thm thm)); 

475 
val thms' = Symtab.update_new ((name, thm), thms) 

476 
handle Symtab.DUPLICATE s => error ("Duplicate theorem name " ^ quote s); 

477 
in 

478 
loaded_thys := Symtab.update 

479 
((thy_name, ThyInfo {path = path, children = children, 

480 
thy_time = thy_time, ml_time = ml_time, theory = theory, thms = thms'}), 

481 
! loaded_thys); 

482 
thm 

483 
end; 

484 

485 
(*store result of proof in loaded_thys and as ML value*) 

486 
fun qed name = 

487 
use_string ["val " ^ name ^ " = store_thm (" ^ quote name ^ ", result ());"]; 

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

488 

559  489 

490 
(* retrieve theorems *) 

491 

492 
fun thmtab thy = 

493 
let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy) 

494 
in thms end; 

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

495 

559  496 
(*get a stored theorem specified by theory and name*) 
497 
fun get_thm thy name = 

498 
(case Symtab.lookup (thmtab thy, name) of 

499 
Some thm => thm 

500 
 None => raise THEORY ("get_thm: no theorem " ^ quote name, [thy])); 

501 

502 
(*get stored theorems of a theory*) 

503 
val thms_of = Symtab.dest o thmtab; 

504 

505 

391  506 
end; 
559  507 