src/Pure/Thy/thy_info.ML
author wenzelm
Tue Feb 11 17:44:29 2014 +0100 (2014-02-11)
changeset 55431 e0f20a44ff9d
parent 54722 5f5608bfe230
child 55461 ce676a750575
permissions -rw-r--r--
common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;
     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   datatype action = Update | Remove
    11   val add_hook: (action -> string -> unit) -> unit
    12   val get_names: unit -> string list
    13   val lookup_theory: string -> theory option
    14   val get_theory: string -> theory
    15   val is_finished: string -> bool
    16   val master_directory: string -> Path.T
    17   val loaded_files: string -> Path.T list
    18   val remove_thy: string -> unit
    19   val kill_thy: string -> unit
    20   val use_theories:
    21     {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
    22     (string * Position.T) list -> unit
    23   val use_thys: (string * Position.T) list -> unit
    24   val use_thy: string * Position.T -> unit
    25   val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
    26   val register_thy: theory -> unit
    27   val finish: unit -> unit
    28 end;
    29 
    30 structure Thy_Info: THY_INFO =
    31 struct
    32 
    33 (** theory loader actions and hooks **)
    34 
    35 datatype action = Update | Remove;
    36 
    37 local
    38   val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list);
    39 in
    40   fun add_hook f = Synchronized.change hooks (cons f);
    41   fun perform action name =
    42     List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks);
    43 end;
    44 
    45 
    46 
    47 (** thy database **)
    48 
    49 (* messages *)
    50 
    51 fun loader_msg txt [] = "Theory loader: " ^ txt
    52   | loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names;
    53 
    54 val show_path = space_implode " via " o map quote;
    55 fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) [];
    56 
    57 
    58 (* derived graph operations *)
    59 
    60 fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
    61   handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
    62 
    63 fun new_entry name parents entry =
    64   String_Graph.new_node (name, entry) #> add_deps name parents;
    65 
    66 
    67 (* thy database *)
    68 
    69 type deps =
    70  {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
    71   imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
    72 
    73 fun make_deps master imports : deps = {master = master, imports = imports};
    74 
    75 fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
    76 fun base_name s = Path.implode (Path.base (Path.explode s));
    77 
    78 local
    79   val database =
    80     Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T);
    81 in
    82   fun get_thys () = ! database;
    83   fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);
    84 end;
    85 
    86 
    87 (* access thy graph *)
    88 
    89 fun thy_graph f x = f (get_thys ()) x;
    90 
    91 fun get_names () = String_Graph.topological_order (get_thys ());
    92 
    93 
    94 (* access thy *)
    95 
    96 fun lookup_thy name =
    97   SOME (thy_graph String_Graph.get_node name) handle String_Graph.UNDEF _ => NONE;
    98 
    99 val known_thy = is_some o lookup_thy;
   100 
   101 fun get_thy name =
   102   (case lookup_thy name of
   103     SOME thy => thy
   104   | NONE => error (loader_msg "nothing known about theory" [name]));
   105 
   106 
   107 (* access deps *)
   108 
   109 val lookup_deps = Option.map #1 o lookup_thy;
   110 val get_deps = #1 o get_thy;
   111 
   112 val is_finished = is_none o get_deps;
   113 val master_directory = master_dir o get_deps;
   114 
   115 
   116 (* access theory *)
   117 
   118 fun lookup_theory name =
   119   (case lookup_thy name of
   120     SOME (_, SOME theory) => SOME theory
   121   | _ => NONE);
   122 
   123 fun get_theory name =
   124   (case lookup_theory name of
   125     SOME theory => theory
   126   | _ => error (loader_msg "undefined theory entry for" [name]));
   127 
   128 val get_imports = Thy_Load.imports_of o get_theory;
   129 
   130 (*Proof General legacy*)
   131 fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   132   (case get_deps name of
   133     NONE => []
   134   | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name)));
   135 
   136 
   137 
   138 (** thy operations **)
   139 
   140 (* main loader actions *)
   141 
   142 fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   143   if is_finished name then error (loader_msg "cannot update finished theory" [name])
   144   else
   145     let
   146       val succs = thy_graph String_Graph.all_succs [name];
   147       val _ = Output.urgent_message (loader_msg "removing" succs);
   148       val _ = List.app (perform Remove) succs;
   149       val _ = change_thys (fold String_Graph.del_node succs);
   150     in () end);
   151 
   152 fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
   153   if known_thy name then remove_thy name
   154   else ());
   155 
   156 fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () =>
   157   let
   158     val name = Context.theory_name theory;
   159     val parents = map Context.theory_name (Theory.parents_of theory);
   160     val _ = kill_thy name;
   161     val _ = map get_theory parents;
   162     val _ = change_thys (new_entry name parents (SOME deps, SOME theory));
   163     val _ = perform Update name;
   164   in () end);
   165 
   166 
   167 (* scheduling loader tasks *)
   168 
   169 datatype result =
   170   Result of {theory: theory, exec_id: Document_ID.exec,
   171     present: unit -> unit, commit: unit -> unit, weight: int};
   172 
   173 fun theory_result theory =
   174   Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
   175 
   176 fun result_theory (Result {theory, ...}) = theory;
   177 fun result_present (Result {present, ...}) = present;
   178 fun result_commit (Result {commit, ...}) = commit;
   179 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
   180 
   181 fun join_theory (Result {theory, exec_id, ...}) =
   182   let
   183     (*toplevel proofs and diags*)
   184     val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
   185     (*fully nested proofs*)
   186     val res = Exn.capture Thm.join_theory_proofs theory;
   187   in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
   188 
   189 datatype task =
   190   Task of string list * (theory list -> result) |
   191   Finished of theory;
   192 
   193 fun task_finished (Task _) = false
   194   | task_finished (Finished _) = true;
   195 
   196 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
   197 
   198 local
   199 
   200 val schedule_seq =
   201   String_Graph.schedule (fn deps => fn (_, task) =>
   202     (case task of
   203       Task (parents, body) =>
   204         let
   205           val result = body (task_parents deps parents);
   206           val _ = Par_Exn.release_all (join_theory result);
   207           val _ = result_present result ();
   208           val _ = result_commit result ();
   209         in result_theory result end
   210     | Finished thy => thy)) #> ignore;
   211 
   212 val schedule_futures = uninterruptible (fn _ => fn tasks =>
   213   let
   214     val futures = tasks
   215       |> String_Graph.schedule (fn deps => fn (name, task) =>
   216         (case task of
   217           Task (parents, body) =>
   218             (singleton o Future.forks)
   219               {name = "theory:" ^ name, group = NONE,
   220                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
   221               (fn () =>
   222                 (case filter (not o can Future.join o #2) deps of
   223                   [] => body (map (result_theory o Future.join) (task_parents deps parents))
   224                 | bad =>
   225                     error (loader_msg ("failed to load " ^ quote name ^
   226                       " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
   227         | Finished theory => Future.value (theory_result theory)));
   228 
   229     val results1 = futures
   230       |> maps (fn future =>
   231           (case Future.join_result future of
   232             Exn.Res result => join_theory result
   233           | Exn.Exn exn => [Exn.Exn exn]));
   234 
   235     val results2 = futures
   236       |> map_filter (Exn.get_res o Future.join_result)
   237       |> sort result_ord
   238       |> Par_List.map (fn result => Exn.capture (result_present result) ());
   239 
   240     (* FIXME more precise commit order (!?) *)
   241     val results3 = futures
   242       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
   243 
   244     (* FIXME avoid global Execution.reset (!??) *)
   245     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
   246 
   247     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   248   in () end);
   249 
   250 in
   251 
   252 fun schedule_tasks tasks =
   253   if not (Multithreading.enabled ()) then schedule_seq tasks
   254   else if Multithreading.self_critical () then
   255      (warning (loader_msg "no multithreading within critical section" []);
   256       schedule_seq tasks)
   257   else schedule_futures tasks;
   258 
   259 end;
   260 
   261 
   262 (* require_thy -- checking database entries wrt. the file-system *)
   263 
   264 local
   265 
   266 fun required_by _ [] = ""
   267   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   268 
   269 fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
   270   let
   271     val _ = kill_thy name;
   272     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
   273     val _ = Output.try_protocol_message (Markup.loading_theory name) "";
   274 
   275     val {master = (thy_path, _), imports} = deps;
   276     val dir = Path.dir thy_path;
   277     val header = Thy_Header.make (name, pos) imports keywords;
   278 
   279     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   280 
   281     val exec_id = Document_ID.make ();
   282     val _ =
   283       Execution.running Document_ID.none exec_id [] orelse
   284         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
   285 
   286     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
   287     val (theory, present, weight) =
   288       Thy_Load.load_thy document last_timing update_time dir header text_pos text
   289         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
   290     fun commit () = update_thy deps theory;
   291   in
   292     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   293   end;
   294 
   295 fun check_deps dir name =
   296   (case lookup_deps name of
   297     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   298   | NONE =>
   299       let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name
   300       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   301   | SOME (SOME {master, ...}) =>
   302       let
   303         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
   304           keywords = keywords'} = Thy_Load.check_thy dir name;
   305         val deps' = SOME (make_deps master' imports', text');
   306         val current =
   307           #2 master = #2 master' andalso
   308             (case lookup_theory name of
   309               NONE => false
   310             | SOME theory => Thy_Load.loaded_files_current theory);
   311       in (current, deps', theory_pos', imports', keywords') end);
   312 
   313 in
   314 
   315 fun require_thys document last_timing initiators dir strs tasks =
   316       fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
   317 and require_thy document last_timing initiators dir (str, require_pos) tasks =
   318   let
   319     val path = Path.expand (Path.explode str);
   320     val name = Path.implode (Path.base path);
   321   in
   322     (case try (String_Graph.get_node tasks) name of
   323       SOME task => (task_finished task, tasks)
   324     | NONE =>
   325         let
   326           val dir' = Path.append dir (Path.dir path);
   327           val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   328 
   329           val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
   330             handle ERROR msg => cat_error msg
   331               (loader_msg "the error(s) above occurred for theory" [name] ^
   332                 Position.here require_pos ^ required_by "\n" initiators);
   333 
   334           val parents = map (base_name o #1) imports;
   335           val (parents_current, tasks') =
   336             require_thys document last_timing (name :: initiators)
   337               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
   338 
   339           val all_current = current andalso parents_current;
   340           val task =
   341             if all_current then Finished (get_theory name)
   342             else
   343               (case deps of
   344                 NONE => raise Fail "Malformed deps"
   345               | SOME (dep, text) =>
   346                   let
   347                     val update_time = serial ();
   348                     val load =
   349                       load_thy document last_timing initiators update_time dep
   350                         text (name, theory_pos) keywords;
   351                   in Task (parents, load) end);
   352 
   353           val tasks'' = new_entry name parents task tasks';
   354         in (all_current, tasks'') end)
   355   end;
   356 
   357 end;
   358 
   359 
   360 (* use_thy *)
   361 
   362 fun use_theories {document, last_timing, master_dir} imports =
   363   schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
   364 
   365 val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
   366 val use_thy = use_thys o single;
   367 
   368 
   369 (* toplevel begin theory -- without maintaining database *)
   370 
   371 fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
   372   let
   373     val {name = (name, _), imports, ...} = header;
   374     val _ = kill_thy name;
   375     val _ = use_theories {document = false, last_timing = K NONE, master_dir = master_dir} imports;
   376     val _ = Thy_Header.define_keywords header;
   377     val parents = map (get_theory o base_name o fst) imports;
   378   in Thy_Load.begin_theory master_dir header parents end;
   379 
   380 
   381 (* register theory *)
   382 
   383 fun register_thy theory =
   384   let
   385     val name = Context.theory_name theory;
   386     val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
   387     val imports = Thy_Load.imports_of theory;
   388   in
   389     NAMED_CRITICAL "Thy_Info" (fn () =>
   390      (kill_thy name;
   391       Output.urgent_message ("Registering theory " ^ quote name);
   392       update_thy (make_deps master imports) theory))
   393   end;
   394 
   395 
   396 (* finish all theories *)
   397 
   398 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
   399 
   400 end;