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