src/Pure/Thy/thy_info.ML
author wenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21 ago)
changeset 65532 febfd9f78bd4
parent 65505 741fad555d82
child 66371 26735fab7a8f
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
     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     (*toplevel proofs and diags*)
   158     val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
   159     (*fully nested proofs*)
   160     val res = Exn.capture Thm.consolidate_theory theory;
   161   in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
   162 
   163 datatype task =
   164   Task of Path.T * string list * (theory list -> result) |
   165   Finished of theory;
   166 
   167 fun task_finished (Task _) = false
   168   | task_finished (Finished _) = true;
   169 
   170 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
   171 
   172 local
   173 
   174 val schedule_seq =
   175   String_Graph.schedule (fn deps => fn (_, task) =>
   176     (case task of
   177       Task (_, parents, body) =>
   178         let
   179           val result = body (task_parents deps parents);
   180           val _ = Par_Exn.release_all (join_theory result);
   181           val _ = result_present result ();
   182           val _ = result_commit result ();
   183         in result_theory result end
   184     | Finished thy => thy)) #> ignore;
   185 
   186 val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   187   let
   188     val futures = tasks
   189       |> String_Graph.schedule (fn deps => fn (name, task) =>
   190         (case task of
   191           Task (_, parents, body) =>
   192             (singleton o Future.forks)
   193               {name = "theory:" ^ name, group = NONE,
   194                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
   195               (fn () =>
   196                 (case filter (not o can Future.join o #2) deps of
   197                   [] => body (map (result_theory o Future.join) (task_parents deps parents))
   198                 | bad =>
   199                     error
   200                       ("Failed to load theory " ^ quote name ^
   201                         " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
   202         | Finished theory => Future.value (theory_result theory)));
   203 
   204     val results1 = futures
   205       |> maps (fn future =>
   206           (case Future.join_result future of
   207             Exn.Res result => join_theory result
   208           | Exn.Exn exn => [Exn.Exn exn]));
   209 
   210     val results2 = futures
   211       |> map_filter (Exn.get_res o Future.join_result)
   212       |> sort result_ord
   213       |> Par_List.map (fn result => Exn.capture (result_present result) ());
   214 
   215     (* FIXME more precise commit order (!?) *)
   216     val results3 = futures
   217       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
   218 
   219     (* FIXME avoid global Execution.reset (!??) *)
   220     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
   221 
   222     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   223   in () end);
   224 
   225 in
   226 
   227 fun schedule_tasks tasks =
   228   if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
   229 
   230 end;
   231 
   232 
   233 (* eval theory *)
   234 
   235 fun excursion keywords master_dir last_timing init elements =
   236   let
   237     fun prepare_span st span =
   238       Command_Span.content span
   239       |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
   240       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
   241 
   242     fun element_result span_elem (st, _) =
   243       let
   244         val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
   245         val (results, st') = Toplevel.element_result keywords elem st;
   246         val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
   247       in (results, (st', pos')) end;
   248 
   249     val (results, (end_state, end_pos)) =
   250       fold_map element_result elements (Toplevel.toplevel, Position.none);
   251 
   252     val thy = Toplevel.end_theory end_pos end_state;
   253   in (results, thy) end;
   254 
   255 fun eval_thy document symbols last_timing update_time master_dir header text_pos text parents =
   256   let
   257     val (name, _) = #name header;
   258     val keywords =
   259       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
   260         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
   261 
   262     val toks = Token.explode keywords text_pos text;
   263     val spans = Outer_Syntax.parse_spans toks;
   264     val elements = Thy_Syntax.parse_elements keywords spans;
   265 
   266     fun init () =
   267       Resources.begin_theory master_dir header parents
   268       |> Present.begin_theory update_time
   269         (fn () => implode (map (HTML.present_span symbols keywords) spans));
   270 
   271     val (results, thy) =
   272       cond_timeit true ("theory " ^ quote name)
   273         (fn () => excursion keywords master_dir last_timing init elements);
   274 
   275     fun present () =
   276       let
   277         val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
   278       in
   279         if exists (Toplevel.is_skipped_proof o #2) res then
   280           warning ("Cannot present theory with skipped proofs: " ^ quote name)
   281         else
   282           let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
   283           in if document then Present.theory_output thy tex_source else () end
   284       end;
   285 
   286   in (thy, present, size text) end;
   287 
   288 
   289 (* require_thy -- checking database entries wrt. the file-system *)
   290 
   291 local
   292 
   293 fun required_by _ [] = ""
   294   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   295 
   296 fun load_thy document symbols last_timing
   297     initiators update_time deps text (name, pos) keywords parents =
   298   let
   299     val _ = remove_thy name;
   300     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
   301     val _ = Output.try_protocol_message (Markup.loading_theory name) [];
   302 
   303     val {master = (thy_path, _), imports} = deps;
   304     val dir = Path.dir thy_path;
   305     val header = Thy_Header.make (name, pos) imports keywords;
   306 
   307     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   308 
   309     val exec_id = Document_ID.make ();
   310     val _ =
   311       Execution.running Document_ID.none exec_id [] orelse
   312         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
   313 
   314     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
   315     val (theory, present, weight) =
   316       eval_thy document symbols last_timing update_time dir header text_pos text
   317         (if name = Context.PureN then [Context.the_global_context ()] else parents);
   318     fun commit () = update_thy deps theory;
   319   in
   320     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   321   end;
   322 
   323 fun check_deps dir name =
   324   (case lookup_deps name of
   325     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   326   | NONE =>
   327       let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
   328       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   329   | SOME (SOME {master, ...}) =>
   330       let
   331         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
   332           keywords = keywords'} = Resources.check_thy dir name;
   333         val deps' = SOME (make_deps master' imports', text');
   334         val current =
   335           #2 master = #2 master' andalso
   336             (case lookup_theory name of
   337               NONE => false
   338             | SOME theory => Resources.loaded_files_current theory);
   339       in (current, deps', theory_pos', imports', keywords') end);
   340 
   341 in
   342 
   343 fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
   344       fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
   345       |>> forall I
   346 and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   347   let
   348     val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
   349     fun check_entry (Task (node_name', _, _)) =
   350           if op = (apply2 File.platform_path (node_name, node_name'))
   351           then ()
   352           else
   353             error ("Incoherent imports for theory " ^ quote theory_name ^
   354               Position.here require_pos ^ ":\n" ^
   355               "  " ^ Path.print node_name ^ "\n" ^
   356               "  " ^ Path.print node_name')
   357       | check_entry _ = ();
   358   in
   359     (case try (String_Graph.get_node tasks) theory_name of
   360       SOME task => (check_entry task; (task_finished task, tasks))
   361     | NONE =>
   362         let
   363           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
   364 
   365           val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
   366             handle ERROR msg =>
   367               cat_error msg
   368                 ("The error(s) above occurred for theory " ^ quote theory_name ^
   369                   Position.here require_pos ^ required_by "\n" initiators);
   370 
   371           val qualifier' = Resources.theory_qualifier theory_name;
   372           val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
   373 
   374           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
   375           val (parents_current, tasks') =
   376             require_thys document symbols last_timing (theory_name :: initiators)
   377               qualifier' dir' imports tasks;
   378 
   379           val all_current = current andalso parents_current;
   380           val task =
   381             if all_current then Finished (get_theory theory_name)
   382             else
   383               (case deps of
   384                 NONE => raise Fail "Malformed deps"
   385               | SOME (dep, text) =>
   386                   let
   387                     val update_time = serial ();
   388                     val load =
   389                       load_thy document symbols last_timing initiators update_time dep
   390                         text (theory_name, theory_pos) keywords;
   391                   in Task (node_name, parents, load) end);
   392 
   393           val tasks'' = new_entry theory_name parents task tasks';
   394         in (all_current, tasks'') end)
   395   end;
   396 
   397 end;
   398 
   399 
   400 (* use theories *)
   401 
   402 fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
   403   let
   404     val (_, tasks) =
   405       require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
   406   in schedule_tasks tasks end;
   407 
   408 fun use_thy name =
   409   use_theories
   410     {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
   411      qualifier = Resources.default_qualifier, master_dir = Path.current}
   412     [(name, Position.none)];
   413 
   414 
   415 (* toplevel scripting -- without maintaining database *)
   416 
   417 fun script_thy pos txt thy =
   418   let
   419     val trs =
   420       Outer_Syntax.parse thy pos txt
   421       |> map (Toplevel.modify_init (K thy));
   422     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   423     val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   424   in Toplevel.end_theory end_pos end_state end;
   425 
   426 
   427 (* register theory *)
   428 
   429 fun register_thy theory =
   430   let
   431     val name = Context.theory_long_name theory;
   432     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
   433     val imports = Resources.imports_of theory;
   434   in
   435     change_thys (fn thys =>
   436       let
   437         val thys' = remove name thys;
   438         val _ = writeln ("Registering theory " ^ quote name);
   439       in update (make_deps master imports) theory thys' end)
   440   end;
   441 
   442 
   443 (* finish all theories *)
   444 
   445 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
   446 
   447 end;
   448 
   449 fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);