author  wenzelm 
Mon, 24 Sep 2007 21:07:41 +0200  
changeset 24696  b5e68fe31eba 
parent 24563  f2edc70f8962 
child 25013  bf4f7571407f 
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 

15801  5 
Main part of theory loader database, including handling of theory and 
6 
file dependencies. 

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

8 

5209  9 
signature BASIC_THY_INFO = 
10 
sig 

11 
val theory: string > theory 

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

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

14 
end; 
5209  15 

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

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

17 
sig 
5209  18 
include BASIC_THY_INFO 
7099  19 
datatype action = Update  Outdate  Remove 
20 
val str_of_action: action > string 

21 
val add_hook: (action > string > unit) > unit 

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

22 
val names: unit > string list 
7910  23 
val known_thy: string > bool 
7935  24 
val check_known_thy: string > bool 
25 
val if_known_thy: (string > unit) > string > unit 

7288  26 
val lookup_theory: string > theory option 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

27 
val get_theory: string > theory 
19547  28 
val the_theory: string > theory > theory 
24563  29 
val is_finished: string > bool 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

30 
val loaded_files: string > Path.T list 
23871  31 
val get_parents: string > string list 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

32 
val pretty_theory: theory > Pretty.T 
7910  33 
val touch_child_thys: string > unit 
7941  34 
val load_file: bool > Path.T > unit 
6241  35 
val use: string > unit 
24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

36 
val time_use: string > unit 
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

37 
val use_thys: string list > unit 
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

38 
val use_thy: string > unit 
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

39 
val time_use_thy: string > unit 
24563  40 
val thy_ord: theory * theory > order 
23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

41 
val begin_theory: string > string list > (Path.T * bool) list > bool > theory 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

42 
val end_theory: theory > theory 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

44 
val register_theory: theory > unit 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

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

47 

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

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

50 

7099  51 
(** theory loader actions and hooks **) 
52 

53 
datatype action = Update  Outdate  Remove; 

54 
val str_of_action = fn Update => "Update"  Outdate => "Outdate"  Remove => "Remove"; 

55 

56 
local 

57 
val hooks = ref ([]: (action > string > unit) list); 

58 
in 

23939  59 
fun add_hook f = CRITICAL (fn () => change hooks (cons f)); 
15570  60 
fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks); 
7099  61 
end; 
62 

63 

64 

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

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

66 

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

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

68 

23871  69 
fun loader_msg txt [] = "Theory loader: " ^ txt 
70 
 loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names; 

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

71 

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

72 
val show_path = space_implode " via " o map quote; 
9332  73 
fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) []; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

74 

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

75 

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

77 

9327  78 
fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G 
9332  79 
handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

80 

7952  81 
fun upd_deps name entry G = 
19473  82 
fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G 
7952  83 
> Graph.map_node name (K entry); 
3976  84 

23967  85 
fun new_deps name parents entry G = 
7952  86 
(if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G) 
87 
> add_deps name parents; 

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

88 

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

89 

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

90 
(* thy database *) 
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 
type deps = 
24190  93 
{update_time: int, (*symbolic time of update; negative value means outdated*) 
94 
master: (Path.T * File.ident) option, (*master dependencies for thy file*) 

95 
text: string list, (*source text for thy*) 

96 
parents: string list, (*source specification of parents (partially qualified)*) 

97 
(*auxiliary files: source path, physical path + identifier*) 

98 
files: (Path.T * (Path.T * File.ident) option) list}; 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

99 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

100 
fun make_deps update_time master text parents files : deps = 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

101 
{update_time = update_time, master = master, text = text, parents = parents, files = files}; 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

102 

24068  103 
fun init_deps master text parents files = 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

104 
SOME (make_deps ~1 master text parents (map (rpair NONE) files)); 
23871  105 

24190  106 
fun master_dir NONE = Path.current 
107 
 master_dir (SOME (path, _)) = Path.dir path; 

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

108 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

109 
fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d); 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

110 
fun master_dir'' d = the_default Path.current (Option.map master_dir' d); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

111 

23967  112 
fun base_name s = Path.implode (Path.base (Path.explode s)); 
113 

7211  114 

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

116 

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

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

119 
in 
6362  120 
fun get_thys () = ! database; 
23939  121 
fun change_thys f = CRITICAL (fn () => Library.change database f); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

122 
end; 
5209  123 

124 

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

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

126 

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

127 
fun thy_graph f x = f (get_thys ()) x; 
9417  128 

23967  129 
fun get_names () = Graph.topological_order (get_thys ()); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

130 

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

131 

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

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

133 

7935  134 
fun lookup_thy name = 
15531  135 
SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE; 
7935  136 

16047  137 
val known_thy = is_some o lookup_thy; 
7935  138 
fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false); 
139 
fun if_known_thy f name = if check_known_thy name then f name else (); 

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

140 

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

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

142 
(case lookup_thy name of 
15531  143 
SOME thy => thy 
144 
 NONE => error (loader_msg "nothing known about theory" [name])); 

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

145 

23939  146 
fun change_thy name f = CRITICAL (fn () => 
147 
(get_thy name; change_thys (Graph.map_node name f))); 

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

148 

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

149 

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

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

151 

15570  152 
val lookup_deps = Option.map #1 o lookup_thy; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

154 
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

155 

6666  156 
fun is_finished name = is_none (get_deps name); 
7191  157 

158 
fun loaded_files name = 

159 
(case get_deps name of 

15531  160 
NONE => [] 
161 
 SOME {master, files, ...} => 

24190  162 
(case master of SOME (thy_path, _) => [thy_path]  NONE => []) @ 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

163 
(map_filter (Option.map #1 o #2) files)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

164 

23871  165 
fun get_parents name = 
23967  166 
thy_graph Graph.imm_preds name handle Graph.UNDEF _ => 
6654  167 
error (loader_msg "nothing known about theory" [name]); 
168 

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

169 

24563  170 
(* pretty_theory *) 
16047  171 

172 
local 

15633  173 

16047  174 
fun relevant_names names = 
175 
let 

176 
val (finished, unfinished) = 

19305  177 
List.filter (fn name => name = Context.draftN orelse known_thy name) names 
178 
> List.partition (fn name => name <> Context.draftN andalso is_finished name); 

16047  179 
in (if not (null finished) then [List.last finished] else []) @ unfinished end; 
15633  180 

16047  181 
in 
15633  182 

16454  183 
fun pretty_theory thy = 
184 
Pretty.str_list "{" "}" (relevant_names (Context.names_of thy)); 

15633  185 

16047  186 
end; 
187 

15633  188 

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

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

190 

7687  191 
fun lookup_theory name = 
192 
(case lookup_thy name of 

15531  193 
SOME (_, SOME thy) => SOME thy 
194 
 _ => NONE); 

7288  195 

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

196 
fun get_theory name = 
7288  197 
(case lookup_theory name of 
23871  198 
SOME theory => theory 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

200 

19547  201 
fun the_theory name thy = 
202 
if Context.theory_name thy = name then thy 

203 
else get_theory name; 

204 

22137  205 
val _ = ML_Context.value_antiq "theory" 
206 
(Scan.lift Args.name 

207 
>> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name)) 

22148  208 
 Scan.succeed ("thy", "ML_Context.the_context ()")); 
22137  209 

24696  210 
val _ = ML_Context.value_antiq "theory_ref" 
211 
(Scan.lift Args.name 

212 
>> (fn name => (name ^ "_thy", 

213 
"Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")) 

214 
 Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_context ())")); 

215 

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

216 

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

217 

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

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

219 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

220 
(* check state *) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

221 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

222 
fun check_unfinished fail name = 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

223 
if known_thy name andalso is_finished name then 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

224 
fail (loader_msg "cannot update finished theory" [name]) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

225 
else (); 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

226 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

227 
fun check_files name = 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

228 
let 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

229 
val files = (case get_deps name of SOME {files, ...} => files  NONE => []); 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

230 
val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path)  _ => NONE) files; 
24190  231 
val _ = null missing_files orelse 
232 
error (loader_msg "unresolved dependencies of theory" [name] ^ 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

233 
" on file(s): " ^ commas_quote missing_files); 
24190  234 
in () end; 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

235 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

236 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

237 
(* maintain update_time *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

238 

7099  239 
local 
240 

6241  241 
fun is_outdated name = 
242 
(case lookup_deps name of 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

243 
SOME (SOME {update_time, ...}) => update_time < 0 
6241  244 
 _ => false); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

245 

24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

246 
fun check_unfinished name = 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

247 
if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE) 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

248 
else SOME name; 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

249 

d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

250 
in 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

251 

6241  252 
fun outdate_thy name = 
7099  253 
if is_finished name orelse is_outdated name then () 
23939  254 
else CRITICAL (fn () => 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

255 
(change_deps name (Option.map (fn {master, text, parents, files, ...} => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

256 
make_deps ~1 master text parents files)); perform Outdate name)); 
7099  257 

7910  258 
fun touch_thys names = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

259 
List.app outdate_thy (thy_graph Graph.all_succs (map_filter check_unfinished names)); 
7910  260 

261 
fun touch_thy name = touch_thys [name]; 

262 
fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name); 

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

263 

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

265 

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

266 

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

268 

7191  269 
local 
270 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

271 
fun provide path name info (deps as SOME {update_time, master, text, parents, files}) = 
23871  272 
(if AList.defined (op =) files path then () 
7941  273 
else warning (loader_msg "undeclared dependency of theory" [name] ^ 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

274 
" on file: " ^ quote (Path.implode path)); 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

275 
SOME (make_deps update_time master text parents 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

276 
(AList.update (op =) (path, SOME info) files))) 
15531  277 
 provide _ _ _ NONE = NONE; 
7941  278 

279 
fun run_file path = 

22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
22086
diff
changeset

280 
(case Option.map (Context.theory_name o Context.the_theory) (ML_Context.get_context ()) of 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

281 
NONE => (ThyLoad.load_ml Path.current path; ()) 
23871  282 
 SOME name => 
283 
(case lookup_deps name of 

284 
SOME deps => 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

285 
change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path)) 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

286 
 NONE => (ThyLoad.load_ml Path.current path; ()))); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

287 

7191  288 
in 
289 

24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

290 
fun load_file time path = 
7941  291 
if time then 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

292 
let val name = Path.implode path in 
7244  293 
timeit (fn () => 
9778  294 
(priority ("\n**** Starting file " ^ quote name ^ " ****"); 
9036  295 
run_file path; 
9778  296 
priority ("**** Finished file " ^ quote name ^ " ****\n"))) 
7244  297 
end 
24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

298 
else run_file path; 
7941  299 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

300 
val use = load_file false o Path.explode; 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

301 
val time_use = load_file true o Path.explode; 
7191  302 

303 
end; 

6233  304 

305 

7099  306 
(* load_thy *) 
307 

9490  308 
fun required_by _ [] = "" 
309 
 required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; 

7099  310 

24190  311 
fun load_thy time upd_time initiators dir name = 
7099  312 
let 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

313 
val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators); 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

314 
val (pos, text, files) = 
24068  315 
(case get_deps name of 
24190  316 
SOME {master = SOME (master_path, _), text as _ :: _, files, ...} => 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

317 
(Position.path master_path, text, files) 
24068  318 
 _ => error (loader_msg "corrupted dependency information" [name])); 
319 
val _ = touch_thy name; 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

320 
val _ = CRITICAL (fn () => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

321 
change_deps name (Option.map (fn {master, text, parents, files, ...} => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

322 
make_deps upd_time master text parents files))); 
24190  323 
val _ = ThyLoad.load_thy dir name pos text (time orelse ! Output.timing); 
7099  324 
in 
23939  325 
CRITICAL (fn () => 
326 
(change_deps name 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

327 
(Option.map (fn {update_time, master, parents, files, ...} => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

328 
make_deps update_time master [] parents files)); 
23939  329 
perform Update name)) 
7099  330 
end; 
331 

332 

24209  333 
(* scheduling loader tasks *) 
334 

335 
datatype task = Task of (unit > unit)  Finished  Running; 

336 
fun task_finished Finished = true  task_finished _ = false; 

337 

338 
local 

339 

24230  340 
fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m)) 
24229
4b5306c36bd9
schedule_tasks: alphabetical order for equivalent tasks;
wenzelm
parents:
24209
diff
changeset

341 
 max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) = 
4b5306c36bd9
schedule_tasks: alphabetical order for equivalent tasks;
wenzelm
parents:
24209
diff
changeset

342 
if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task' 
24209  343 
 max_task _ task' = task'; 
344 

345 
fun next_task G = 

346 
let 

347 
val tasks = Graph.minimals G > map (fn name => 

348 
(name, (Graph.get_node G name, length (Graph.imm_succs G name)))); 

349 
val finished = filter (task_finished o fst o snd) tasks; 

350 
in 

351 
if not (null finished) then next_task (Graph.del_nodes (map fst finished) G) 

352 
else if null tasks then (Multithreading.Terminate, G) 

353 
else 

354 
(case fold max_task tasks NONE of 

355 
NONE => (Multithreading.Wait, G) 

356 
 SOME (name, (body, _)) => 

357 
(Multithreading.Task {body = body, cont = Graph.del_nodes [name], fail = K Graph.empty}, 

358 
Graph.map_node name (K Running) G)) 

359 
end; 

360 

361 
fun schedule_seq tasks = 

362 
Graph.topological_order tasks 

363 
> List.app (fn name => (case Graph.get_node tasks name of Task body => body ()  _ => ())); 

364 

365 
in 

366 

367 
fun schedule_tasks tasks n = 

368 
let val m = ! Multithreading.max_threads in 

369 
if m <= 1 orelse n <= 1 then schedule_seq tasks 

370 
else if Multithreading.self_critical () then 

371 
(warning (loader_msg "no multithreading within critical section" []); 

372 
schedule_seq tasks) 

373 
else 

374 
(case Multithreading.schedule (Int.min (m, n)) next_task tasks of 

375 
[] => () 

376 
 exns => raise Exn.EXCEPTIONS (exns, "")) 

377 
end; 

378 

379 
end; 

380 

381 

23967  382 
(* require_thy  checking database entries wrt. the filesystem *) 
15065  383 

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

385 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

386 
fun check_ml master (src_path, info) = 
23871  387 
let val info' = 
388 
(case info of NONE => NONE 

389 
 SOME (_, id) => 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

390 
(case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE 
23871  391 
 SOME (path', id') => if id <> id' then NONE else SOME (path', id'))) 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

392 
in (src_path, info') end; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

393 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

394 
fun check_deps dir name = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

395 
(case lookup_deps name of 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

396 
SOME NONE => (true, NONE, get_parents name) 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

397 
 NONE => 
24190  398 
let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name 
24068  399 
in (false, init_deps (SOME master) text parents files, parents) end 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

400 
 SOME (deps as SOME {update_time, master, text, parents, files}) => 
24190  401 
let 
402 
val (thy_path, thy_id) = ThyLoad.check_thy dir name; 

403 
val master' = SOME (thy_path, thy_id); 

404 
in 

405 
if Option.map #2 master <> SOME thy_id then 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

406 
let val {text = text', imports = parents', uses = files', ...} = 
24190  407 
ThyLoad.deps_thy dir name; 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

408 
in (false, init_deps master' text' parents' files', parents') end 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

409 
else 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

410 
let 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

411 
val files' = map (check_ml master') files; 
24307
434c9fbc1787
check_deps: ensure that theory is actually present, not just update_time > 1;
wenzelm
parents:
24230
diff
changeset

412 
val current = update_time >= 0 andalso can get_theory name 
434c9fbc1787
check_deps: ensure that theory is actually present, not just update_time > 1;
wenzelm
parents:
24230
diff
changeset

413 
andalso forall (is_some o snd) files'; 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

414 
val update_time' = if current then update_time else ~1; 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

415 
val text' = if current then text else explode (File.read thy_path); 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

416 
val deps' = SOME (make_deps update_time' master' text' parents files'); 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

417 
in (current, deps', parents) end 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

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

419 

23967  420 
in 
421 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

422 
fun require_thys time initiators dir strs tasks = 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

423 
fold_map (require_thy time initiators dir) strs tasks >> forall I 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

424 
and require_thy time initiators dir str tasks = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

425 
let 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

426 
val path = Path.expand (Path.explode str); 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

427 
val name = Path.implode (Path.base path); 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

428 
val dir' = Path.append dir (Path.dir path); 
23871  429 
val _ = member (op =) initiators name andalso error (cycle_msg initiators); 
7066  430 
in 
23974  431 
(case try (Graph.get_node (fst tasks)) name of 
24209  432 
SOME task => (task_finished task, tasks) 
23967  433 
 NONE => 
434 
let 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

435 
val (current, deps, parents) = check_deps dir' name 
23967  436 
handle ERROR msg => cat_error msg 
437 
(loader_msg "the error(s) above occurred while examining theory" [name] ^ 

438 
required_by "\n" initiators); 

439 
val parent_names = map base_name parents; 

23871  440 

23974  441 
val (parents_current, (tasks_graph', tasks_len')) = 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

442 
require_thys time (name :: initiators) 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

443 
(Path.append dir (master_dir' deps)) parents tasks; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

444 

23967  445 
val all_current = current andalso parents_current; 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

446 
val theory = if all_current then SOME (get_theory name) else NONE; 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

447 
val _ = if not all_current andalso known_thy name then outdate_thy name else (); 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

448 
val _ = change_thys (new_deps name parent_names (deps, theory)); 
23967  449 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

450 
val upd_time = serial (); 
23974  451 
val tasks_graph'' = tasks_graph' > new_deps name parent_names 
24209  452 
(if all_current then Finished 
453 
else Task (fn () => load_thy time upd_time initiators dir' name)); 

23974  454 
val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1; 
455 
in (all_current, (tasks_graph'', tasks_len'')) end) 

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

457 

23967  458 
end; 
459 

460 

24209  461 
(* use_thy etc. *) 
23967  462 

463 
local 

464 

24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

465 
fun gen_use_thy' req dir arg = 
24209  466 
let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0) 
467 
in schedule_tasks tasks n end; 

6241  468 

23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

469 
fun gen_use_thy req str = 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

470 
let val name = base_name str in 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

471 
check_unfinished warning name; 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

472 
gen_use_thy' req Path.current str; 
24071  473 
CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (get_theory name)))) 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

474 
end; 
7244  475 

7211  476 
in 
477 

24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

478 
val use_thys_dir = gen_use_thy' (require_thys false); 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

479 
val use_thys = use_thys_dir Path.current; 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

480 
val use_thy = gen_use_thy (require_thy false); 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

481 
val time_use_thy = gen_use_thy (require_thy true); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

482 

7211  483 
end; 
484 

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

485 

6666  486 
(* remove_thy *) 
487 

488 
fun remove_thy name = 

7910  489 
if is_finished name then error (loader_msg "cannot remove finished theory" [name]) 
6666  490 
else 
491 
let val succs = thy_graph Graph.all_succs [name] in 

9778  492 
priority (loader_msg "removing" succs); 
23939  493 
CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs))) 
6666  494 
end; 
495 

496 

24563  497 
(* update_time *) 
498 

499 
structure UpdateTime = TheoryDataFun 

500 
( 

501 
type T = int; 

502 
val empty = 0; 

503 
val copy = I; 

504 
fun extend _ = empty; 

505 
fun merge _ _ = empty; 

506 
); 

507 

508 
val thy_ord = int_ord o pairself UpdateTime.get; 

509 

510 

7066  511 
(* begin / end theory *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

512 

23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

513 
fun begin_theory name parents uses int = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

514 
let 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

515 
val parent_names = map base_name parents; 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

516 
val dir = master_dir'' (lookup_deps name); 
7244  517 
val _ = check_unfinished error name; 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

518 
val _ = if int then use_thys_dir dir parents else (); 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

519 
(* FIXME tmp *) 
24071  520 
val _ = CRITICAL (fn () => 
521 
ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names))))); 

17365  522 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

523 
val theory = Theory.begin_theory name (map get_theory parent_names); 
23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

524 

7952  525 
val deps = 
526 
if known_thy name then get_deps name 

24068  527 
else init_deps NONE [] parents (map #1 uses); 
23967  528 
val _ = change_thys (new_deps name parent_names (deps, NONE)); 
9451  529 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

530 
val update_time = (case deps of NONE => 0  SOME {update_time, ...} => update_time); 
24563  531 
val update_time = if update_time > 0 then update_time else serial (); 
532 
val theory' = theory 

533 
> UpdateTime.put update_time 

534 
> Present.begin_theory update_time dir uses; 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

535 

23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

536 
val uses_now = map_filter (fn (x, true) => SOME x  _ => NONE) uses; 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

537 
val ((), theory'') = 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

538 
ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now 
22086  539 
> Context.the_theory; 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

540 
in theory'' end; 
7244  541 

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

542 
fun end_theory theory = 
7099  543 
let 
16454  544 
val name = Context.theory_name theory; 
24190  545 
val _ = check_files name; 
16504  546 
val theory' = Theory.end_theory theory; 
23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

547 
val _ = change_thy name (fn (deps, _) => (deps, SOME theory')); 
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

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

549 

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

550 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

552 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

553 
fun register_thy name = 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

554 
let 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

555 
val _ = priority ("Registering theory " ^ quote name); 
24563  556 
val thy = get_theory name; 
24096  557 
val _ = map get_theory (get_parents name); 
558 
val _ = check_unfinished error name; 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

559 
val _ = touch_thy name; 
24190  560 
val master = #master (ThyLoad.deps_thy Path.current name); 
24563  561 
val upd_time = UpdateTime.get thy; 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

562 
in 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

563 
CRITICAL (fn () => 
24190  564 
(change_deps name (Option.map 
565 
(fn {parents, files, ...} => make_deps upd_time (SOME master) [] parents files)); 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

566 
perform Update name)) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

568 

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

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

570 
let 
16454  571 
val name = Context.theory_name theory; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

572 
val parents = Theory.parents_of theory; 
16454  573 
val parent_names = map Context.theory_name parents; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

574 

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

575 
fun err txt bads = 
23871  576 
error (loader_msg txt bads ^ "\ncannot register theory " ^ quote name); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

577 

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

579 
fun get_variant (x, y_name) = 
15531  580 
if Theory.eq_thy (x, get_theory y_name) then NONE 
581 
else SOME y_name; 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

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

583 

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

584 
fun register G = 
15531  585 
(Graph.new_node (name, (NONE, SOME theory)) G 
9327  586 
handle Graph.DUP _ => err "duplicate theory entry" []) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

588 
in 
6666  589 
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

590 
else if not (null variants) then err "different versions of parent theories" variants 
23939  591 
else CRITICAL (fn () => (change_thys register; perform Update name)) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

593 

15801  594 
val _ = register_theory ProtoPure.thy; 
595 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

596 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

597 
(* finish all theories *) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

598 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

599 
fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry))); 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

600 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

601 

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

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

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

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

605 

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

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

607 

5209  608 
structure BasicThyInfo: BASIC_THY_INFO = ThyInfo; 
609 
open BasicThyInfo; 