src/Pure/Thy/thy_info.ML
author wenzelm
Sat Mar 09 23:57:07 2019 +0100 (2 months ago ago)
changeset 70067 0cb8753bdb50
parent 70064 f8293bf510a0
child 70072 def3ec9cdb7e
permissions -rw-r--r--
clarified signature;
     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   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
    30 end;
    31 
    32 structure Thy_Info: THY_INFO =
    33 struct
    34 
    35 (** presentation of consolidated theory **)
    36 
    37 type presentation_context =
    38   {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
    39     segments: Thy_Output.segment list};
    40 
    41 structure 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 
    49 fun apply_presentation (context: presentation_context) thy =
    50   ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
    51 
    52 fun add_presentation f = Presentation.map (cons (f, stamp ()));
    53 
    54 val _ =
    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 (Path.explode "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 
    80 val show_path = space_implode " via " o map quote;
    81 
    82 fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
    83 
    84 
    85 (* derived graph operations *)
    86 
    87 fun 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 
    90 fun new_entry name parents entry =
    91   String_Graph.new_node (name, entry) #> add_deps name parents;
    92 
    93 
    94 (* global thys *)
    95 
    96 type 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 
   100 fun make_deps master imports : deps = {master = master, imports = imports};
   101 
   102 fun master_dir_deps (d: deps option) =
   103   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
   104 
   105 local
   106   val global_thys =
   107     Synchronized.var "Thy_Info.thys"
   108       (String_Graph.empty: (deps option * theory option) String_Graph.T);
   109 in
   110   fun get_thys () = Synchronized.value global_thys;
   111   fun change_thys f = Synchronized.change global_thys f;
   112 end;
   113 
   114 fun get_names () = String_Graph.topological_order (get_thys ());
   115 
   116 
   117 (* access thy *)
   118 
   119 fun lookup thys name = try (String_Graph.get_node thys) name;
   120 fun lookup_thy name = lookup (get_thys ()) name;
   121 
   122 fun 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 
   127 fun get_thy name = get (get_thys ()) name;
   128 
   129 
   130 (* access deps *)
   131 
   132 val lookup_deps = Option.map #1 o lookup_thy;
   133 
   134 val master_directory = master_dir_deps o #1 o get_thy;
   135 
   136 
   137 (* access theory *)
   138 
   139 fun lookup_theory name =
   140   (case lookup_thy name of
   141     SOME (_, SOME theory) => SOME theory
   142   | _ => NONE);
   143 
   144 fun get_theory name =
   145   (case lookup_theory name of
   146     SOME theory => theory
   147   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
   148 
   149 val get_imports = Resources.imports_of o get_theory;
   150 
   151 
   152 
   153 (** thy operations **)
   154 
   155 (* remove *)
   156 
   157 fun 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 
   167 val remove_thy = change_thys o remove;
   168 
   169 
   170 (* update *)
   171 
   172 fun 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 
   181 fun update_thy deps theory = change_thys (update deps theory);
   182 
   183 
   184 (* context *)
   185 
   186 type context =
   187   {options: Options.T,
   188    symbols: HTML.symbols,
   189    bibtex_entries: string list,
   190    last_timing: Toplevel.transition -> Time.time};
   191 
   192 fun 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 
   201 datatype result =
   202   Result of {theory: theory, exec_id: Document_ID.exec,
   203     present: unit -> unit, commit: unit -> unit, weight: int};
   204 
   205 fun theory_result theory =
   206   Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
   207 
   208 fun result_theory (Result {theory, ...}) = theory;
   209 fun result_present (Result {present, ...}) = present;
   210 fun result_commit (Result {commit, ...}) = commit;
   211 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
   212 
   213 fun 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 
   220 datatype task =
   221   Task of string list * (theory list -> result) |
   222   Finished of theory;
   223 
   224 fun task_finished (Task _) = false
   225   | task_finished (Finished _) = true;
   226 
   227 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
   228 
   229 val 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 
   241 val 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 
   283 fun 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.timing (last_timing tr) tr);
   289 
   290     fun element_result span_elem (st, _) =
   291       let
   292         val elem = Thy_Element.map_element (prepare_span st) span_elem;
   293         val (results, st') = Toplevel.element_result keywords elem st;
   294         val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
   295       in (results, (st', pos')) end;
   296 
   297     val (results, (end_state, end_pos)) =
   298       fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
   299 
   300     val thy = Toplevel.end_theory end_pos end_state;
   301   in (results, thy) end;
   302 
   303 fun 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_Element.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 
   335 local
   336 
   337 fun required_by _ [] = ""
   338   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   339 
   340 fun 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 
   373 fun 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 
   391 in
   392 
   393 fun require_thys context initiators qualifier dir strs tasks =
   394       fold_map (require_thy context initiators qualifier dir) strs tasks |>> forall I
   395 and 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 
   436 end;
   437 
   438 
   439 (* use theories *)
   440 
   441 fun 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 
   445 fun 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 
   452 fun 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.init_toplevel ());
   459   in Toplevel.end_theory end_pos end_state end;
   460 
   461 
   462 (* register theory *)
   463 
   464 fun 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 
   480 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
   481 
   482 end;
   483 
   484 fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);