diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML +++ b/src/Pure/Thy/thy_info.ML @@ -1,367 +1,389 @@ (* Title: Pure/Thy/thy_info.ML Author: Markus Wenzel, TU Muenchen Global theory info database, with auto-loading according to theory and file dependencies. *) signature THY_INFO = sig datatype action = Update | Remove val add_hook: (action -> string -> unit) -> unit val get_names: unit -> string list val lookup_theory: string -> theory option val get_theory: string -> theory val is_finished: string -> bool val master_directory: string -> Path.T val loaded_files: string -> Path.T list val remove_thy: string -> unit val kill_thy: string -> unit val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} -> (string * Position.T) list -> unit val use_thys: (string * Position.T) list -> unit val use_thy: string * Position.T -> unit val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory val register_thy: theory -> unit val finish: unit -> unit end; structure Thy_Info: THY_INFO = struct (** theory loader actions and hooks **) datatype action = Update | Remove; local val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list); in fun add_hook f = Synchronized.change hooks (cons f); fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks); end; (** thy database **) (* messages *) fun loader_msg txt [] = "Theory loader: " ^ txt | loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names; val show_path = space_implode " via " o map quote; fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) []; (* derived graph operations *) fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = String_Graph.new_node (name, entry) #> add_deps name parents; (* thy database *) type deps = {master: (Path.T * SHA1.digest), (*master dependencies for thy file*) imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) fun make_deps master imports : deps = {master = master, imports = imports}; fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); fun base_name s = Path.implode (Path.base (Path.explode s)); local val database = Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = ! database; fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f); end; (* access thy graph *) fun thy_graph f x = f (get_thys ()) x; fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup_thy name = SOME (thy_graph String_Graph.get_node name) handle String_Graph.UNDEF _ => NONE; val known_thy = is_some o lookup_thy; fun get_thy name = (case lookup_thy name of SOME thy => thy | NONE => error (loader_msg "nothing known about theory" [name])); (* access deps *) val lookup_deps = Option.map #1 o lookup_thy; val get_deps = #1 o get_thy; val is_finished = is_none o get_deps; val master_directory = master_dir o get_deps; (* access theory *) fun lookup_theory name = (case lookup_thy name of SOME (_, SOME theory) => SOME theory | _ => NONE); fun get_theory name = (case lookup_theory name of SOME theory => theory | _ => error (loader_msg "undefined theory entry for" [name])); val get_imports = Thy_Load.imports_of o get_theory; fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () => (case get_deps name of NONE => [] | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name))); (** thy operations **) (* main loader actions *) fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () => if is_finished name then error (loader_msg "attempt to change finished theory" [name]) else let val succs = thy_graph String_Graph.all_succs [name]; val _ = Output.urgent_message (loader_msg "removing" succs); val _ = List.app (perform Remove) succs; val _ = change_thys (fold String_Graph.del_node succs); in () end); fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () => if known_thy name then remove_thy name else ()); fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () => let val name = Context.theory_name theory; val parents = map Context.theory_name (Theory.parents_of theory); val _ = kill_thy name; val _ = map get_theory parents; val _ = change_thys (new_entry name parents (SOME deps, SOME theory)); val _ = perform Update name; in () end); (* scheduling loader tasks *) datatype result = - Result of {theory: theory, id: serial, present: unit future, commit: unit -> unit}; + Result of {theory: theory, id: serial, present: unit -> unit, commit: unit -> unit, weight: int}; + +fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0}; fun result_theory (Result {theory, ...}) = theory; -fun theory_result theory = Result {theory = theory, id = 0, present = Future.value (), commit = I}; +fun result_present (Result {present, ...}) = present; +fun result_commit (Result {commit, ...}) = commit; +fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); + +fun join_proofs (Result {theory, id, present, ...}) = + let + val result1 = Exn.capture Thm.join_theory_proofs theory; + val results2 = Future.join_results (Goal.peek_futures id); + in result1 :: results2 end; + datatype task = Task of string list * (theory list -> result) | Finished of theory; fun task_finished (Task _) = false | task_finished (Finished _) = true; fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; local -fun finish_thy (Result {theory, id, present, commit}) = - let - val result1 = Exn.capture Thm.join_theory_proofs theory; - val results2 = Future.join_results (Goal.peek_futures id); - val result3 = Future.join_result present; - val _ = Par_Exn.release_all (result1 :: results2 @ [result3]); - val _ = commit (); - in theory end; - val schedule_seq = String_Graph.schedule (fn deps => fn (_, task) => (case task of - Task (parents, body) => finish_thy (body (task_parents deps parents)) + Task (parents, body) => + let + val result = body (task_parents deps parents); + val _ = Par_Exn.release_all (join_proofs result); + val _ = result_present result (); + val _ = result_commit result (); + in result_theory result end | Finished thy => thy)) #> ignore; val schedule_futures = uninterruptible (fn _ => fn tasks => let - val results1 = tasks + val futures = tasks |> String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) {name = "theory:" ^ name, group = NONE, deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} (fn () => (case filter (not o can Future.join o #2) deps of [] => body (map (result_theory o Future.join) (task_parents deps parents)) | bad => error (loader_msg ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote (map #1 bad) ^ ")") []))) - | Finished theory => Future.value (theory_result theory))) - |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]); + | Finished theory => Future.value (theory_result theory))); + + val results1 = futures + |> maps (fn future => + (case Future.join_result future of + Exn.Res result => join_proofs result + | Exn.Exn exn => [Exn.Exn exn])); + + val results2 = futures + |> map_filter (Exn.get_res o Future.join_result) + |> sort result_ord + |> Par_List.map (fn result => Exn.capture (result_present result) ()); + + (* FIXME more precise commit order (!?) *) + val results3 = futures + |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); (* FIXME avoid global reset_futures (!??) *) - val results2 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ())); + val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ())); - val _ = Par_Exn.release_all (rev (results2 @ results1)); + val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); in () end); in fun schedule_tasks tasks = if not (Multithreading.enabled ()) then schedule_seq tasks else if Multithreading.self_critical () then (warning (loader_msg "no multithreading within critical section" []); schedule_seq tasks) else schedule_futures tasks; end; (* require_thy -- checking database entries wrt. the file-system *) local fun required_by _ [] = "" | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents = let val _ = kill_thy name; val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => (); val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val header = Thy_Header.make (name, pos) imports keywords; val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); val id = serial (); val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path); - val (theory, present) = + val (theory, present, weight) = Thy_Load.load_thy last_timing update_time dir header text_pos text (if name = Context.PureN then [ML_Context.the_global_context ()] else parents); fun commit () = update_thy deps theory; - in Result {theory = theory, id = id, present = present, commit = commit} end; + in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end; fun check_deps dir name = (case lookup_deps name of SOME NONE => (true, NONE, Position.none, get_imports name, []) | NONE => let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end | SOME (SOME {master, ...}) => let val {master = master', text = text', theory_pos = theory_pos', imports = imports', keywords = keywords'} = Thy_Load.check_thy dir name; val deps' = SOME (make_deps master' imports', text'); val current = #2 master = #2 master' andalso (case lookup_theory name of NONE => false | SOME theory => Thy_Load.load_current theory); in (current, deps', theory_pos', imports', keywords') end); in fun require_thys last_timing initiators dir strs tasks = fold_map (require_thy last_timing initiators dir) strs tasks |>> forall I and require_thy last_timing initiators dir (str, require_pos) tasks = let val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); in (case try (String_Graph.get_node tasks) name of SOME task => (task_finished task, tasks) | NONE => let val dir' = Path.append dir (Path.dir path); val _ = member (op =) initiators name andalso error (cycle_msg initiators); val (current, deps, theory_pos, imports, keywords) = check_deps dir' name handle ERROR msg => cat_error msg (loader_msg "the error(s) above occurred while examining theory" [name] ^ Position.here require_pos ^ required_by "\n" initiators); val parents = map (base_name o #1) imports; val (parents_current, tasks') = require_thys last_timing (name :: initiators) (Path.append dir (master_dir (Option.map #1 deps))) imports tasks; val all_current = current andalso parents_current; val task = if all_current then Finished (get_theory name) else (case deps of NONE => raise Fail "Malformed deps" | SOME (dep, text) => let val update_time = serial (); val load = load_thy last_timing initiators update_time dep text (name, theory_pos) keywords; in Task (parents, load) end); val tasks'' = new_entry name parents task tasks'; in (all_current, tasks'') end) end; end; (* use_thy *) fun use_theories {last_timing, master_dir} imports = schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty)); val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current}; val use_thy = use_thys o single; (* toplevel begin theory -- without maintaining database *) fun toplevel_begin_theory master_dir (header: Thy_Header.header) = let val {name = (name, _), imports, ...} = header; val _ = kill_thy name; val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports; val _ = Thy_Header.define_keywords header; val parents = map (get_theory o base_name o fst) imports; in Thy_Load.begin_theory master_dir header parents end; (* register theory *) fun register_thy theory = let val name = Context.theory_name theory; val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; val imports = Thy_Load.imports_of theory; in NAMED_CRITICAL "Thy_Info" (fn () => (kill_thy name; Output.urgent_message ("Registering theory " ^ quote name); update_thy (make_deps master imports) theory)) end; (* finish all theories *) fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end; diff --git a/src/Pure/Thy/thy_load.ML b/src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML +++ b/src/Pure/Thy/thy_load.ML @@ -1,303 +1,302 @@ (* Title: Pure/Thy/thy_load.ML Author: Makarius Loading files that contribute to a theory. Global master path for TTY loop. *) signature THY_LOAD = sig val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val thy_path: Path.T -> Path.T val parse_files: string -> (theory -> Token.file list) parser val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val provide: Path.T * SHA1.digest -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string val use_file: Path.T -> theory -> string * theory val loaded_files: theory -> Path.T list val load_current: theory -> bool val use_ml: Path.T -> unit val exec_ml: Path.T -> generic_theory -> generic_theory val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val load_thy: (Toplevel.transition -> Time.time) -> int -> Path.T -> Thy_Header.header -> - Position.T -> string -> theory list -> theory * unit future + Position.T -> string -> theory list -> theory * (unit -> unit) * int val set_master_path: Path.T -> unit val get_master_path: unit -> Path.T end; structure Thy_Load: THY_LOAD = struct (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun extend _ = empty; fun merge _ = empty; ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, [])); (* inlined files *) fun check_file dir file = File.check_file (File.full_path dir file); fun read_files cmd dir (path, pos) = let fun make_file file = let val _ = Position.report pos (Markup.path (Path.implode file)); val full_path = check_file dir file; in {src_path = file, text = File.read full_path, pos = Path.position full_path} end; val paths = (case Keyword.command_files cmd of [] => [path] | exts => map (fn ext => Path.ext ext path) exts); in map make_file paths end; fun parse_files cmd = Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => (case Token.get_files tok of SOME files => files | NONE => read_files cmd (master_directory thy) (Path.explode name, Token.position_of tok))); local fun clean ((i1, t1) :: (i2, t2) :: toks) = if Token.keyword_with (fn s => s = "%" orelse s = "--") t1 then clean toks else (i1, t1) :: clean ((i2, t2) :: toks) | clean toks = toks; fun clean_tokens toks = ((0 upto length toks - 1) ~~ toks) |> filter (fn (_, tok) => Token.is_proper tok) |> clean; fun find_file toks = rev (clean_tokens toks) |> get_first (fn (i, tok) => if Token.is_name tok then SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok)) handle ERROR msg => error (msg ^ Token.pos_of tok) else NONE); in fun resolve_files master_dir span = (case span of Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks) => if Keyword.is_theory_load cmd then (case find_file toks of NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos) | SOME (i, path) => let val toks' = toks |> map_index (fn (j, tok) => if i = j then Token.put_files (read_files cmd master_dir path) tok else tok); in Thy_Syntax.Span (Thy_Syntax.Command (cmd, pos), toks') end) else span | span => span); end; (* check files *) val thy_path = Path.ext "thy"; fun check_thy dir thy_name = let val path = thy_path (Path.basic thy_name); val master_file = check_file dir path; val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_name <> name andalso error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_parse_files cmd = parse_files cmd >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, text, ...} => provide (src_path, SHA1.digest text)) fs thy; in (fs, thy') end); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun use_file src_path thy = let val ((_, id), text) = load_file thy src_path; val thy' = provide (src_path, id) thy; in (text, thy') end; fun loaded_files thy = let val {master_dir, provided, ...} = Files.get thy in map (File.full_path master_dir o #1) provided end; fun load_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* provide files *) fun eval_file path text = ML_Context.eval_text true (Path.position path) text; fun use_ml src_path = if is_none (Context.thread_data ()) then let val path = check_file Path.current src_path in eval_file path (File.read path) end else let val thy = ML_Context.the_global_context (); val ((path, id), text) = load_file thy src_path; val _ = eval_file path text; val _ = Context.>> Local_Theory.propagate_ml_env; val provide = provide (src_path, id); val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide)); in () end; fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); (* load_thy *) fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> put_deps master_dir imports |> fold Thy_Header.declare_keyword keywords |> Theory.checkpoint; fun excursion last_timing init elements = let fun prepare_span span = Thy_Syntax.span_content span |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) |> Toplevel.modify_init init |> (fn tr => Toplevel.put_timing (last_timing tr) tr); fun element_result span_elem (st, _) = let val elem = Thy_Syntax.map_element prepare_span span_elem; val (results, st') = Toplevel.element_result elem st; val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.toplevel, Position.none); val thy = Toplevel.end_theory end_pos end_state; in (results, thy) end; fun load_thy last_timing update_time master_dir header text_pos text parents = let val time = ! Toplevel.timing; val {name = (name, _), ...} = header; val _ = Thy_Header.define_keywords header; val _ = Present.init_theory name; fun init () = begin_theory master_dir header parents |> Present.begin_theory update_time master_dir; val lexs = Keyword.get_lexicons (); val toks = Thy_Syntax.parse_tokens lexs text_pos text; val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks); val elements = Thy_Syntax.parse_elements spans; val _ = Present.theory_source name (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements); val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); - val present = - Future.flat results |> Future.map (fn res0 => - let - val res = filter_out (Toplevel.is_ignored o #1) res0; - val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax (); - in - Thy_Output.present_thy minor Keyword.command_tags - (Outer_Syntax.is_markup outer_syntax) res toks - |> Buffer.content - |> Present.theory_output name - end); + fun present () = + let + val res = filter_out (Toplevel.is_ignored o #1) (flat (Future.joins results)); + val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax (); + in + Thy_Output.present_thy minor Keyword.command_tags + (Outer_Syntax.is_markup outer_syntax) res toks + |> Buffer.content + |> Present.theory_output name + end; - in (thy, present) end; + in (thy, present, size text) end; (* document antiquotation *) val _ = Context.>> (Context.map_theory (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path)) (fn {context = ctxt, ...} => fn (name, pos) => let val dir = master_directory (Proof_Context.theory_of ctxt); val path = Path.append dir (Path.explode name); val _ = if File.exists path then () else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos); val _ = Position.report pos (Markup.path name); in Thy_Output.verb_text name end))); (* global master path *) local val master_path = Unsynchronized.ref Path.current; in fun set_master_path path = master_path := path; fun get_master_path () = ! master_path; end; end;