src/Pure/Thy/thy_info.ML
author wenzelm
Thu Sep 28 11:53:55 2017 +0200 (21 months ago)
changeset 66711 80fa1401cf76
parent 66377 753eb5b83370
child 66873 9953ae603a23
permissions -rw-r--r--
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
     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           warning ("Cannot present theory with skipped proofs: " ^ quote name)
   271         else
   272           let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
   273           in if document then Present.theory_output thy tex_source else () end
   274       end;
   275 
   276   in (thy, present, size text) end;
   277 
   278 
   279 (* require_thy -- checking database entries wrt. the file-system *)
   280 
   281 local
   282 
   283 fun required_by _ [] = ""
   284   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   285 
   286 fun load_thy document symbols last_timing
   287     initiators update_time deps text (name, pos) keywords parents =
   288   let
   289     val _ = remove_thy name;
   290     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
   291     val _ = Output.try_protocol_message (Markup.loading_theory name) [];
   292 
   293     val {master = (thy_path, _), imports} = deps;
   294     val dir = Path.dir thy_path;
   295     val header = Thy_Header.make (name, pos) imports keywords;
   296 
   297     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   298 
   299     val exec_id = Document_ID.make ();
   300     val _ =
   301       Execution.running Document_ID.none exec_id [] orelse
   302         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
   303 
   304     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
   305     val (theory, present, weight) =
   306       eval_thy document symbols last_timing update_time dir header text_pos text
   307         (if name = Context.PureN then [Context.the_global_context ()] else parents);
   308     fun commit () = update_thy deps theory;
   309   in
   310     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   311   end;
   312 
   313 fun check_deps dir name =
   314   (case lookup_deps name of
   315     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   316   | NONE =>
   317       let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
   318       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   319   | SOME (SOME {master, ...}) =>
   320       let
   321         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
   322           keywords = keywords'} = Resources.check_thy dir name;
   323         val deps' = SOME (make_deps master' imports', text');
   324         val current =
   325           #2 master = #2 master' andalso
   326             (case lookup_theory name of
   327               NONE => false
   328             | SOME theory => Resources.loaded_files_current theory);
   329       in (current, deps', theory_pos', imports', keywords') end);
   330 
   331 in
   332 
   333 fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
   334       fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
   335       |>> forall I
   336 and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   337   let
   338     val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   339   in
   340     (case try (String_Graph.get_node tasks) theory_name of
   341       SOME task => (task_finished task, tasks)
   342     | NONE =>
   343         let
   344           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
   345 
   346           val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
   347             handle ERROR msg =>
   348               cat_error msg
   349                 ("The error(s) above occurred for theory " ^ quote theory_name ^
   350                   Position.here require_pos ^ required_by "\n" initiators);
   351 
   352           val qualifier' = Resources.theory_qualifier theory_name;
   353           val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
   354 
   355           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
   356           val (parents_current, tasks') =
   357             require_thys document symbols last_timing (theory_name :: initiators)
   358               qualifier' dir' imports tasks;
   359 
   360           val all_current = current andalso parents_current;
   361           val task =
   362             if all_current then Finished (get_theory theory_name)
   363             else
   364               (case deps of
   365                 NONE => raise Fail "Malformed deps"
   366               | SOME (dep, text) =>
   367                   let
   368                     val update_time = serial ();
   369                     val load =
   370                       load_thy document symbols last_timing initiators update_time dep
   371                         text (theory_name, theory_pos) keywords;
   372                   in Task (parents, load) end);
   373 
   374           val tasks'' = new_entry theory_name parents task tasks';
   375         in (all_current, tasks'') end)
   376   end;
   377 
   378 end;
   379 
   380 
   381 (* use theories *)
   382 
   383 fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
   384   let
   385     val (_, tasks) =
   386       require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
   387   in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
   388 
   389 fun use_thy name =
   390   use_theories
   391     {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
   392      qualifier = Resources.default_qualifier, master_dir = Path.current}
   393     [(name, Position.none)];
   394 
   395 
   396 (* toplevel scripting -- without maintaining database *)
   397 
   398 fun script_thy pos txt thy =
   399   let
   400     val trs =
   401       Outer_Syntax.parse thy pos txt
   402       |> map (Toplevel.modify_init (K thy));
   403     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   404     val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   405   in Toplevel.end_theory end_pos end_state end;
   406 
   407 
   408 (* register theory *)
   409 
   410 fun register_thy theory =
   411   let
   412     val name = Context.theory_long_name theory;
   413     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
   414     val imports = Resources.imports_of theory;
   415   in
   416     change_thys (fn thys =>
   417       let
   418         val thys' = remove name thys;
   419         val _ = writeln ("Registering theory " ^ quote name);
   420       in update (make_deps master imports) theory thys' end)
   421   end;
   422 
   423 
   424 (* finish all theories *)
   425 
   426 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
   427 
   428 end;
   429 
   430 fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);