author  wenzelm 
Tue, 06 Jul 1999 21:03:34 +0200  
changeset 6900  29060d9b60d4 
parent 6666  be06ed5d0b4c 
child 7066  febce8eee487 
permissions  rwrr 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

1 
(* Title: Pure/Thy/thy_info.ML 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

2 
ID: $Id$ 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

4 

6362  5 
Theory loader database, including theory and file dependencies. 
3976  6 
*) 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

7 

5209  8 
signature BASIC_THY_INFO = 
9 
sig 

10 
val theory: string > theory 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

11 
val theory_of_sign: Sign.sg > theory 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

12 
val theory_of_thm: thm > theory 
6241  13 
(*val use: string > unit*) (*exported later*) 
14 
val time_use: string > unit 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

15 
val touch_thy: string > unit 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

16 
val use_thy: string > unit 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

17 
val update_thy: string > unit 
6666  18 
val remove_thy: string > unit 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

19 
val time_use_thy: string > unit 
6527  20 
val use_thy_only: string > unit 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

21 
end; 
5209  22 

3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

23 
signature THY_INFO = 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

24 
sig 
5209  25 
include BASIC_THY_INFO 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

26 
val names: unit > string list 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

27 
val get_theory: string > theory 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

28 
val put_theory: theory > unit 
6654  29 
val get_preds: string > string list 
6241  30 
val loaded_files: string > (Path.T * File.info) list 
31 
val load_file: bool > Path.T > unit 

6329  32 
val use_path: Path.T > unit 
6241  33 
val use: string > unit 
6329  34 
val begin_theory: string > string list > (Path.T * bool) list > theory 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

35 
val end_theory: theory > theory 
6666  36 
val finish: unit > unit 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

37 
val register_theory: theory > unit 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

38 
end; 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

39 

6362  40 
structure ThyInfo: THY_INFO = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

41 
struct 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

42 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

43 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

44 
(** thy database **) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

45 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

46 
(* messages *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

47 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

48 
fun gen_msg txt [] = txt 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

49 
 gen_msg txt names = txt ^ " " ^ commas_quote names; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

50 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

51 
fun loader_msg txt names = gen_msg ("Theory loader: " ^ txt) names; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

52 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

53 
val show_path = space_implode " via " o map quote; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

54 
fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) []; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

55 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

56 

6666  57 
(* derived graph operations *) 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

58 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

59 
fun add_deps name parents G = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

60 
foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

61 
handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess)); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

62 

6666  63 
fun del_deps name G = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

64 
foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name); 
3976  65 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

66 
fun update_node name parents entry G = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

67 
add_deps name parents 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

68 
(if can (Graph.get_node G) name then del_deps name G else Graph.new_node (name, entry) G); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

69 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

70 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

71 
(* thy database *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

72 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

73 
type deps = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

74 
{present: bool, outdated: bool, 
6241  75 
master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list}; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

76 

6241  77 
fun make_deps present outdated master files = 
78 
{present = present, outdated = outdated, master = master, files = files}: deps; 

3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

79 

6362  80 
type thy = deps option * theory option; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

81 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

82 
local 
6362  83 
val database = ref (Graph.empty: thy Graph.T); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

84 
in 
6362  85 
fun get_thys () = ! database; 
86 
fun change_thys f = database := (f (! database)); 

3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

87 
end; 
5209  88 

89 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

90 
(* access thy graph *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

91 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

92 
fun thy_graph f x = f (get_thys ()) x; 
6666  93 
fun get_names () = Graph.keys (get_thys ()); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

94 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

95 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

96 
(* access thy *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

97 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

98 
fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

99 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

100 
fun get_thy name = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

101 
(case lookup_thy name of 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

102 
Some thy => thy 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

103 
 None => error (loader_msg "nothing known about theory" [name])); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

104 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

105 
fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f)); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

106 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

107 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

108 
(* access deps *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

109 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

110 
val lookup_deps = apsome #1 o lookup_thy; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

111 
val get_deps = #1 o get_thy; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

112 
fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x)); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

113 

6666  114 
fun is_finished name = is_none (get_deps name); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

115 
fun get_files name = (case get_deps name of Some {files, ...} => files  _ => []); 
6241  116 
val loaded_files = mapfilter #2 o get_files; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

117 

6654  118 
fun get_preds name = 
119 
(thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ => 

120 
error (loader_msg "nothing known about theory" [name]); 

121 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

122 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

123 
(* access theory *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

124 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

125 
fun get_theory name = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

126 
(case get_thy name of 
6362  127 
(_, Some theory) => theory 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

128 
 _ => error (loader_msg "undefined theory entry for" [name])); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

129 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

130 
val theory_of_sign = get_theory o Sign.name_of; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

131 
val theory_of_thm = theory_of_sign o Thm.sign_of_thm; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

132 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

133 
fun put_theory theory = 
6362  134 
change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, Some theory)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

135 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

136 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

137 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

138 
(** thy operations **) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

139 

6241  140 
(* maintain 'outdated' flag *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

141 

6241  142 
fun is_outdated name = 
143 
(case lookup_deps name of 

144 
Some (Some {outdated, ...}) => outdated 

145 
 _ => false); 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

146 

6241  147 
fun outdate_thy name = 
6666  148 
if is_finished name then () 
6241  149 
else change_deps name (apsome (fn {present, outdated = _, master, files} => 
150 
make_deps present true master files)); 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

151 

6241  152 
fun touch_thy name = 
153 
if is_outdated name then () 

6666  154 
else if is_finished name then warning (loader_msg "tried to touch finished theory" [name]) 
6241  155 
else 
156 
(case filter_out is_outdated (thy_graph Graph.all_succs [name]) \ name of 

157 
[] => outdate_thy name 

158 
 names => 

159 
(warning (loader_msg "the following theories become outofdate:" names); 

160 
seq outdate_thy names; outdate_thy name)); 

161 

162 
val untouch_deps = apsome (fn {present, outdated = _, master, files}: deps => 

163 
make_deps present false master files); 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

164 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

165 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

166 
(* load_thy *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

167 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

168 
fun required_by [] = "" 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

169 
 required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")"; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

170 

6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

171 
fun load_thy ml time initiators dir name parents = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

172 
let 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

173 
val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else (); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

174 
val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

175 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

176 
val _ = seq touch_thy (thy_graph Graph.all_succs [name]); 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

177 
val master = ThyLoad.load_thy dir name ml time; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

178 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

179 
val files = get_files name; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

180 
val missing_files = mapfilter (fn (path, None) => Some (Path.pack path)  _ => None) files; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

181 
in 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

182 
if null missing_files then () 
6263  183 
else warning (loader_msg "unresolved dependencies of theory" [name] ^ 
184 
"\nfile(s): " ^ commas_quote missing_files); 

6241  185 
change_deps name (fn _ => Some (make_deps true false master files)) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

186 
end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

187 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

188 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

189 
(* load_file *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

190 

6241  191 
fun run_file path = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

192 
let 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

193 
fun provide name info (deps as Some {present, outdated, master, files}) = 
6263  194 
if exists (equal path o #1) files then 
6241  195 
Some (make_deps present outdated master (overwrite (files, (path, Some info)))) 
196 
else (warning (loader_msg "undeclared dependency of theory" [name] ^ 

6389  197 
" on file: " ^ quote (Path.pack path)); deps) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

198 
 provide _ _ None = None; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

199 
in 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

200 
(case apsome PureThy.get_name (Context.get_context ()) of 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

201 
None => (ThyLoad.load_file path; ()) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

202 
 Some name => 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

203 
if is_some (lookup_thy name) then change_deps name (provide name (ThyLoad.load_file path)) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

204 
else (ThyLoad.load_file path; ())) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

205 
end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

206 

6241  207 
fun load_file false path = run_file path 
208 
 load_file true path = 

209 
let val name = Path.pack path in 

210 
timeit (fn () => 

211 
(writeln ("\n**** Starting file " ^ quote name ^ " ****"); 

212 
run_file path; 

213 
writeln ("**** Finished file " ^ quote name ^ " ****\n"))) 

214 
end; 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

215 

6329  216 
val use_path = load_file false; 
217 
val use = use_path o Path.unpack; 

6241  218 
val time_use = load_file true o Path.unpack; 
6233  219 

220 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

221 
(* require_thy *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

222 

6241  223 
fun init_deps master files = Some (make_deps false false master (map (rpair None) files)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

224 

6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

225 
fun load_deps dir name ml = 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

226 
let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml 
6233  227 
in (Some (init_deps master files), parents) end; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

228 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

229 
fun file_current (_, None) = false 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

230 
 file_current (path, info) = info = ThyLoad.check_file path; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

231 

6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

232 
fun current_deps ml strict dir name = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

233 
(case lookup_deps name of 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

234 
None => (false, load_deps dir name ml) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

235 
 Some deps => 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

236 
let val same_deps = (None, thy_graph Graph.imm_preds name) in 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

237 
(case deps of 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

238 
None => (true, same_deps) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

239 
 Some {present, outdated, master, files} => 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

240 
if present andalso not strict then (true, same_deps) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

241 
else 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

242 
let val master' = ThyLoad.check_thy dir name ml in 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

243 
if master <> master' then (false, load_deps dir name ml) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

244 
else (not outdated andalso forall file_current files, same_deps) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

245 
end) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

246 
end); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

247 

6487  248 
fun require_thy ml time strict keep_strict initiators prfx s = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

249 
let 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

250 
val path = Path.expand (Path.unpack s); 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

251 
val name = Path.pack (Path.base path); 
6487  252 
val dir = Path.append prfx (Path.dir path); 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

253 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

254 
val require_parent = 
6487  255 
#1 o require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators) dir; 
256 
val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR => 

6241  257 
error (loader_msg "The error(s) above occurred while examining theory" [name] ^ 
258 
(if null initiators then "" else "\n" ^ required_by initiators)); 

6233  259 
val parents_current = map require_parent parents; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

260 

6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

261 
val result = 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

262 
if current andalso forall I parents_current then true 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

263 
else 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

264 
((case new_deps of 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

265 
Some deps => change_thys (update_node name parents (untouch_deps deps, None)) 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

266 
 None => ()); 
6487  267 
load_thy ml time initiators dir name parents; 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

268 
false); 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

269 
in (result, name) end; 
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

270 

6487  271 
fun gen_use_thy f s = 
272 
let val (_, name) = f Path.current s in Context.context (get_theory name) end; 

6241  273 

274 
val weak_use_thy = gen_use_thy (require_thy true false false false []); 

275 
val use_thy = gen_use_thy (require_thy true false true false []); 

276 
val update_thy = gen_use_thy (require_thy true false true true []); 

277 
val time_use_thy = gen_use_thy (require_thy true true true false []); 

278 
val use_thy_only = gen_use_thy (require_thy false false true false []); 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

279 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

280 

6666  281 
(* remove_thy *) 
282 

283 
fun remove_thy name = 

284 
if is_finished name then error (loader_msg "cannot remove finished theory" [name]) 

285 
else 

286 
let val succs = thy_graph Graph.all_succs [name] in 

287 
writeln (loader_msg "removing" succs); 

288 
change_thys (Graph.del_nodes succs) 

289 
end; 

290 

291 

6329  292 
(* begin / end theory *) (* FIXME tune *) (* FIXME files vs. paths (!?!?) *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

293 

6329  294 
fun begin_theory name parents paths = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

295 
let 
6900  296 
val _ = 
297 
if is_some (lookup_thy name) andalso is_finished name then 

298 
error (loader_msg "cannot change finished theory" [name]) 

299 
else (); 

6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

300 
val _ = (map Path.basic parents; seq weak_use_thy parents); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

301 
val theory = PureThy.begin_theory name (map get_theory parents); 
6362  302 
val _ = change_thys (update_node name parents (init_deps [] [], Some theory)); 
6329  303 
val use_paths = mapfilter (fn (x, true) => Some x  _ => None) paths; 
304 
in Context.setmp (Some theory) (seq use_path) use_paths; theory end; 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

305 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

306 
fun end_theory theory = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

307 
let val theory' = PureThy.end_theory theory 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

308 
in put_theory theory'; theory' end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

309 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

310 

6666  311 
(* finish all theories *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

312 

6666  313 
fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

314 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

315 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

316 
(* register existing theories *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

317 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

318 
fun register_theory theory = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

319 
let 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

320 
val name = PureThy.get_name theory; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

321 
val parents = Theory.parents_of theory; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

322 
val parent_names = map PureThy.get_name parents; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

323 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

324 
fun err txt bads = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

325 
error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

326 

6666  327 
val nonfinished = filter_out is_finished parent_names; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

328 
fun get_variant (x, y_name) = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

329 
if Theory.eq_thy (x, get_theory y_name) then None 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

330 
else Some y_name; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

331 
val variants = mapfilter get_variant (parents ~~ parent_names); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

332 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

333 
fun register G = 
6362  334 
(Graph.new_node (name, (None, Some theory)) G 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

335 
handle Graph.DUPLICATE _ => err "duplicate theory entry" []) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

336 
> add_deps name parent_names; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

337 
in 
6666  338 
if not (null nonfinished) then err "nonfinished parent theories" nonfinished 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

339 
else if not (null variants) then err "different versions of parent theories" variants 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

340 
else change_thys register 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

341 
end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

342 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

343 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

344 
(*final declarations of this structure*) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

345 
val theory = get_theory; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

346 
val names = get_names; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

347 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

348 
end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

349 

5209  350 
structure BasicThyInfo: BASIC_THY_INFO = ThyInfo; 
351 
open BasicThyInfo; 