1(* Title: Pure/Thy/thy_info.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Global theory info database, with auto-loading according to theory and 5file dependencies. 6*) 7 8signature THY_INFO = 9sig 10 type presentation_context = 11 {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, 12 segments: Thy_Output.segment list} 13 val apply_presentation: presentation_context -> theory -> unit 14 val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory 15 val get_names: unit -> string list 16 val lookup_theory: string -> theory option 17 val get_theory: string -> theory 18 val master_directory: string -> Path.T 19 val remove_thy: string -> unit 20 type context = 21 {options: Options.T, 22 symbols: HTML.symbols, 23 bibtex_entries: string list, 24 last_timing: Toplevel.transition -> Time.time} 25 val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit 26 val use_thy: string -> unit 27 val script_thy: Position.T -> string -> theory -> theory 28 val register_thy: theory -> unit 29 val finish: unit -> unit 30end; 31 32structure Thy_Info: THY_INFO = 33struct 34 35(** presentation of consolidated theory **) 36 37type presentation_context = 38 {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, 39 segments: Thy_Output.segment list}; 40 41structure Presentation = Theory_Data 42( 43 type T = ((presentation_context -> theory -> unit) * stamp) list; 44 val empty = []; 45 val extend = I; 46 fun merge data : T = Library.merge (eq_snd op =) data; 47); 48 49fun apply_presentation (context: presentation_context) thy = 50 ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy)); 51 52fun add_presentation f = Presentation.map (cons (f, stamp ())); 53 54val _ = 55 Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => 56 if exists (Toplevel.is_skipped_proof o #state) segments then () 57 else 58 let 59 val body = Thy_Output.present_thy options thy segments; 60 val option = Present.document_option options; 61 in 62 if #disabled option then () 63 else 64 let 65 val latex = Latex.isabelle_body (Context.theory_name thy) body; 66 val output = [Latex.output_text latex, Latex.output_positions file_pos latex]; 67 val _ = 68 if Options.bool options "export_document" 69 then Export.export thy "document.tex" output else (); 70 val _ = if #enabled option then Present.theory_output thy output else (); 71 in () end 72 end)); 73 74 75 76(** thy database **) 77 78(* messages *) 79 80val show_path = space_implode " via " o map quote; 81 82fun cycle_msg names = "Cyclic dependency of " ^ show_path names; 83 84 85(* derived graph operations *) 86 87fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G 88 handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); 89 90fun new_entry name parents entry = 91 String_Graph.new_node (name, entry) #> add_deps name parents; 92 93 94(* global thys *) 95 96type deps = 97 {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) 98 imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) 99 100fun make_deps master imports : deps = {master = master, imports = imports}; 101 102fun master_dir_deps (d: deps option) = 103 the_default Path.current (Option.map (Path.dir o #1 o #master) d); 104 105local 106 val global_thys = 107 Synchronized.var "Thy_Info.thys" 108 (String_Graph.empty: (deps option * theory option) String_Graph.T); 109in 110 fun get_thys () = Synchronized.value global_thys; 111 fun change_thys f = Synchronized.change global_thys f; 112end; 113 114fun get_names () = String_Graph.topological_order (get_thys ()); 115 116 117(* access thy *) 118 119fun lookup thys name = try (String_Graph.get_node thys) name; 120fun lookup_thy name = lookup (get_thys ()) name; 121 122fun get thys name = 123 (case lookup thys name of 124 SOME thy => thy 125 | NONE => error ("Theory loader: nothing known about theory " ^ quote name)); 126 127fun get_thy name = get (get_thys ()) name; 128 129 130(* access deps *) 131 132val lookup_deps = Option.map #1 o lookup_thy; 133 134val master_directory = master_dir_deps o #1 o get_thy; 135 136 137(* access theory *) 138 139fun lookup_theory name = 140 (case lookup_thy name of 141 SOME (_, SOME theory) => SOME theory 142 | _ => NONE); 143 144fun get_theory name = 145 (case lookup_theory name of 146 SOME theory => theory 147 | _ => error ("Theory loader: undefined entry for theory " ^ quote name)); 148 149val get_imports = Resources.imports_of o get_theory; 150 151 152 153(** thy operations **) 154 155(* remove *) 156 157fun remove name thys = 158 (case lookup thys name of 159 NONE => thys 160 | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) 161 | SOME _ => 162 let 163 val succs = String_Graph.all_succs thys [name]; 164 val _ = writeln ("Theory loader: removing " ^ commas_quote succs); 165 in fold String_Graph.del_node succs thys end); 166 167val remove_thy = change_thys o remove; 168 169 170(* update *) 171 172fun update deps theory thys = 173 let 174 val name = Context.theory_long_name theory; 175 val parents = map Context.theory_long_name (Theory.parents_of theory); 176 177 val thys' = remove name thys; 178 val _ = map (get thys') parents; 179 in new_entry name parents (SOME deps, SOME theory) thys' end; 180 181fun update_thy deps theory = change_thys (update deps theory); 182 183 184(* context *) 185 186type context = 187 {options: Options.T, 188 symbols: HTML.symbols, 189 bibtex_entries: string list, 190 last_timing: Toplevel.transition -> Time.time}; 191 192fun default_context (): context = 193 {options = Options.default (), 194 symbols = HTML.no_symbols, 195 bibtex_entries = [], 196 last_timing = K Time.zeroTime}; 197 198 199(* scheduling loader tasks *) 200 201datatype result = 202 Result of {theory: theory, exec_id: Document_ID.exec, 203 present: unit -> unit, commit: unit -> unit, weight: int}; 204 205fun theory_result theory = 206 Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; 207 208fun result_theory (Result {theory, ...}) = theory; 209fun result_present (Result {present, ...}) = present; 210fun result_commit (Result {commit, ...}) = commit; 211fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); 212 213fun join_theory (Result {theory, exec_id, ...}) = 214 let 215 val _ = Execution.join [exec_id]; 216 val res = Exn.capture Thm.consolidate_theory theory; 217 val exns = maps Task_Queue.group_status (Execution.peek exec_id); 218 in res :: map Exn.Exn exns end; 219 220datatype task = 221 Task of string list * (theory list -> result) | 222 Finished of theory; 223 224fun task_finished (Task _) = false 225 | task_finished (Finished _) = true; 226 227fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; 228 229val schedule_seq = 230 String_Graph.schedule (fn deps => fn (_, task) => 231 (case task of 232 Task (parents, body) => 233 let 234 val result = body (task_parents deps parents); 235 val _ = Par_Exn.release_all (join_theory result); 236 val _ = result_present result (); 237 val _ = result_commit result (); 238 in result_theory result end 239 | Finished thy => thy)) #> ignore; 240 241val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks => 242 let 243 val futures = tasks 244 |> String_Graph.schedule (fn deps => fn (name, task) => 245 (case task of 246 Task (parents, body) => 247 (singleton o Future.forks) 248 {name = "theory:" ^ name, group = NONE, 249 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} 250 (fn () => 251 (case filter (not o can Future.join o #2) deps of 252 [] => body (map (result_theory o Future.join) (task_parents deps parents)) 253 | bad => 254 error 255 ("Failed to load theory " ^ quote name ^ 256 " (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) 257 | Finished theory => Future.value (theory_result theory))); 258 259 val results1 = futures 260 |> maps (fn future => 261 (case Future.join_result future of 262 Exn.Res result => join_theory result 263 | Exn.Exn exn => [Exn.Exn exn])); 264 265 val results2 = futures 266 |> map_filter (Exn.get_res o Future.join_result) 267 |> sort result_ord 268 |> Par_List.map (fn result => Exn.capture (result_present result) ()); 269 270 (* FIXME more precise commit order (!?) *) 271 val results3 = futures 272 |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); 273 274 (* FIXME avoid global Execution.reset (!??) *) 275 val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); 276 277 val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); 278 in () end); 279 280 281(* eval theory *) 282 283fun excursion keywords master_dir last_timing init elements = 284 let 285 fun prepare_span st span = 286 Command_Span.content span 287 |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) 288 |> (fn tr => Toplevel.put_timing (last_timing tr) tr); 289 290 fun element_result span_elem (st, _) = 291 let 292 val elem = Thy_Syntax.map_element (prepare_span st) span_elem; 293 val (results, st') = Toplevel.element_result keywords elem st; 294 val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); 295 in (results, (st', pos')) end; 296 297 val (results, (end_state, end_pos)) = 298 fold_map element_result elements (Toplevel.toplevel, Position.none); 299 300 val thy = Toplevel.end_theory end_pos end_state; 301 in (results, thy) end; 302 303fun eval_thy (context: context) update_time master_dir header text_pos text parents = 304 let 305 val {options, symbols, bibtex_entries, last_timing} = context; 306 val (name, _) = #name header; 307 val keywords = 308 fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents 309 (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); 310 311 val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text); 312 val elements = Thy_Syntax.parse_elements keywords spans; 313 314 fun init () = 315 Resources.begin_theory master_dir header parents 316 |> Present.begin_theory bibtex_entries update_time 317 (fn () => implode (map (HTML.present_span symbols keywords) spans)); 318 319 val (results, thy) = 320 cond_timeit true ("theory " ^ quote name) 321 (fn () => excursion keywords master_dir last_timing init elements); 322 323 fun present () = 324 let 325 val segments = (spans ~~ maps Toplevel.join_results results) 326 |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'}); 327 val context: presentation_context = 328 {options = options, file_pos = text_pos, adjust_pos = I, segments = segments}; 329 in apply_presentation context thy end; 330 in (thy, present, size text) end; 331 332 333(* require_thy -- checking database entries wrt. the file-system *) 334 335local 336 337fun required_by _ [] = "" 338 | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; 339 340fun load_thy context initiators update_time deps text (name, pos) keywords parents = 341 let 342 val _ = remove_thy name; 343 val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); 344 val _ = Output.try_protocol_message (Markup.loading_theory name) []; 345 346 val {master = (thy_path, _), imports} = deps; 347 val dir = Path.dir thy_path; 348 val header = Thy_Header.make (name, pos) imports keywords; 349 350 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); 351 352 val exec_id = Document_ID.make (); 353 val _ = 354 Execution.running Document_ID.none exec_id [] orelse 355 raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); 356 357 val timing_start = Timing.start (); 358 359 val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); 360 val (theory, present, weight) = 361 eval_thy context update_time dir header text_pos text 362 (if name = Context.PureN then [Context.the_global_context ()] else parents); 363 364 val timing_result = Timing.result timing_start; 365 val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; 366 val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] 367 368 fun commit () = update_thy deps theory; 369 in 370 Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} 371 end; 372 373fun check_deps dir name = 374 (case lookup_deps name of 375 SOME NONE => (true, NONE, Position.none, get_imports name, []) 376 | NONE => 377 let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name 378 in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end 379 | SOME (SOME {master, ...}) => 380 let 381 val {master = master', text = text', theory_pos = theory_pos', imports = imports', 382 keywords = keywords'} = Resources.check_thy dir name; 383 val deps' = SOME (make_deps master' imports', text'); 384 val current = 385 #2 master = #2 master' andalso 386 (case lookup_theory name of 387 NONE => false 388 | SOME theory => Resources.loaded_files_current theory); 389 in (current, deps', theory_pos', imports', keywords') end); 390 391in 392 393fun require_thys context initiators qualifier dir strs tasks = 394 fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I 395and require_thy context initiators qualifier dir (s, require_pos) tasks = 396 let 397 val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; 398 in 399 (case try (String_Graph.get_node tasks) theory_name of 400 SOME task => (task_finished task, tasks) 401 | NONE => 402 let 403 val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators); 404 405 val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name 406 handle ERROR msg => 407 cat_error msg 408 ("The error(s) above occurred for theory " ^ quote theory_name ^ 409 Position.here require_pos ^ required_by "\n" initiators); 410 411 val qualifier' = Resources.theory_qualifier theory_name; 412 val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); 413 414 val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports; 415 val (parents_current, tasks') = 416 require_thys context (theory_name :: initiators) qualifier' dir' imports tasks; 417 418 val all_current = current andalso parents_current; 419 val task = 420 if all_current then Finished (get_theory theory_name) 421 else 422 (case deps of 423 NONE => raise Fail "Malformed deps" 424 | SOME (dep, text) => 425 let 426 val update_time = serial (); 427 val load = 428 load_thy context initiators update_time 429 dep text (theory_name, theory_pos) keywords; 430 in Task (parents, load) end); 431 432 val tasks'' = new_entry theory_name parents task tasks'; 433 in (all_current, tasks'') end) 434 end; 435 436end; 437 438 439(* use theories *) 440 441fun use_theories context qualifier master_dir imports = 442 let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty 443 in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; 444 445fun use_thy name = 446 use_theories (default_context ()) Resources.default_qualifier 447 Path.current [(name, Position.none)]; 448 449 450(* toplevel scripting -- without maintaining database *) 451 452fun script_thy pos txt thy = 453 let 454 val trs = 455 Outer_Syntax.parse thy pos txt 456 |> map (Toplevel.modify_init (K thy)); 457 val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); 458 val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel; 459 in Toplevel.end_theory end_pos end_state end; 460 461 462(* register theory *) 463 464fun register_thy theory = 465 let 466 val name = Context.theory_long_name theory; 467 val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; 468 val imports = Resources.imports_of theory; 469 in 470 change_thys (fn thys => 471 let 472 val thys' = remove name thys; 473 val _ = writeln ("Registering theory " ^ quote name); 474 in update (make_deps master imports) theory thys' end) 475 end; 476 477 478(* finish all theories *) 479 480fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); 481 482end; 483 484fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); 485