src/Pure/Thy/thy_info.ML
author wenzelm
Wed Oct 01 12:00:05 2008 +0200 (2008-10-01)
changeset 28445 526b8adcd117
parent 28435 97de495414e8
child 28449 b6c57eb0fc39
permissions -rw-r--r--
more robust treatment of Interrupt (cf. exn.ML);
future_schedule: group each theory separately;
     1 (*  Title:      Pure/Thy/thy_info.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Main part of theory loader database, including handling of theory and
     6 file dependencies.
     7 *)
     8 
     9 signature THY_INFO =
    10 sig
    11   datatype action = Update | Outdate | Remove
    12   val str_of_action: action -> string
    13   val add_hook: (action -> string -> unit) -> unit
    14   val get_names: unit -> string list
    15   val known_thy: string -> bool
    16   val check_known_thy: string -> bool
    17   val if_known_thy: (string -> unit) -> string -> unit
    18   val lookup_theory: string -> theory option
    19   val get_theory: string -> theory
    20   val the_theory: string -> theory -> theory
    21   val is_finished: string -> bool
    22   val master_directory: string -> Path.T
    23   val loaded_files: string -> Path.T list
    24   val get_parents: string -> string list
    25   val touch_thy: string -> unit
    26   val touch_child_thys: string -> unit
    27   val provide_file: Path.T -> string -> unit
    28   val load_file: bool -> Path.T -> unit
    29   val exec_file: bool -> Path.T -> Context.generic -> Context.generic
    30   val use: string -> unit
    31   val time_use: string -> unit
    32   val use_thys: string list -> unit
    33   val use_thy: string -> unit
    34   val time_use_thy: string -> unit
    35   val remove_thy: string -> unit
    36   val kill_thy: string -> unit
    37   val thy_ord: theory * theory -> order
    38   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
    39   val end_theory: theory -> unit
    40   val register_thy: string -> unit
    41   val register_theory: theory -> unit
    42   val finish: unit -> unit
    43 end;
    44 
    45 structure ThyInfo: THY_INFO =
    46 struct
    47 
    48 (** theory loader actions and hooks **)
    49 
    50 datatype action = Update | Outdate | Remove;
    51 val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
    52 
    53 local
    54   val hooks = ref ([]: (action -> string -> unit) list);
    55 in
    56   fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    57   fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
    58 end;
    59 
    60 
    61 
    62 (** thy database **)
    63 
    64 (* messages *)
    65 
    66 fun loader_msg txt [] = "Theory loader: " ^ txt
    67   | loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names;
    68 
    69 val show_path = space_implode " via " o map quote;
    70 fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) [];
    71 
    72 
    73 (* derived graph operations *)
    74 
    75 fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
    76   handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
    77 
    78 fun upd_deps name entry G =
    79   fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
    80   |> Graph.map_node name (K entry);
    81 
    82 fun new_deps name parents entry G =
    83   (if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G)
    84   |> add_deps name parents;
    85 
    86 
    87 (* thy database *)
    88 
    89 type deps =
    90   {update_time: int,                      (*symbolic time of update; negative value means outdated*)
    91     master: (Path.T * File.ident) option, (*master dependencies for thy file*)
    92     text: string list,                    (*source text for thy*)
    93     parents: string list,                 (*source specification of parents (partially qualified)*)
    94       (*auxiliary files: source path, physical path + identifier*)
    95     files: (Path.T * (Path.T * File.ident) option) list};
    96 
    97 fun make_deps update_time master text parents files : deps =
    98   {update_time = update_time, master = master, text = text, parents = parents, files = files};
    99 
   100 fun init_deps master text parents files =
   101   SOME (make_deps ~1 master text parents (map (rpair NONE) files));
   102 
   103 fun master_dir NONE = Path.current
   104   | master_dir (SOME (path, _)) = Path.dir path;
   105 
   106 fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d);
   107 fun master_dir'' d = the_default Path.current (Option.map master_dir' d);
   108 
   109 fun base_name s = Path.implode (Path.base (Path.explode s));
   110 
   111 
   112 type thy = deps option * theory option;
   113 
   114 local
   115   val database = ref (Graph.empty: thy Graph.T);
   116 in
   117   fun get_thys () = ! database;
   118   fun change_thys f = CRITICAL (fn () => Library.change database f);
   119 end;
   120 
   121 
   122 (* access thy graph *)
   123 
   124 fun thy_graph f x = f (get_thys ()) x;
   125 
   126 fun get_names () = Graph.topological_order (get_thys ());
   127 
   128 
   129 (* access thy *)
   130 
   131 fun lookup_thy name =
   132   SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
   133 
   134 val known_thy = is_some o lookup_thy;
   135 fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
   136 fun if_known_thy f name = if check_known_thy name then f name else ();
   137 
   138 fun get_thy name =
   139   (case lookup_thy name of
   140     SOME thy => thy
   141   | NONE => error (loader_msg "nothing known about theory" [name]));
   142 
   143 fun change_thy name f = CRITICAL (fn () =>
   144   (get_thy name; change_thys (Graph.map_node name f)));
   145 
   146 
   147 (* access deps *)
   148 
   149 val lookup_deps = Option.map #1 o lookup_thy;
   150 val get_deps = #1 o get_thy;
   151 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
   152 
   153 val is_finished = is_none o get_deps;
   154 val master_directory = master_dir' o get_deps;
   155 
   156 fun loaded_files name =
   157   (case get_deps name of
   158     NONE => []
   159   | SOME {master, files, ...} =>
   160       (case master of SOME (thy_path, _) => [thy_path] | NONE => []) @
   161       (map_filter (Option.map #1 o #2) files));
   162 
   163 fun get_parents name =
   164   thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
   165     error (loader_msg "nothing known about theory" [name]);
   166 
   167 
   168 (* access theory *)
   169 
   170 fun lookup_theory name =
   171   (case lookup_thy name of
   172     SOME (_, SOME thy) => SOME thy
   173   | _ => NONE);
   174 
   175 fun get_theory name =
   176   (case lookup_theory name of
   177     SOME theory => theory
   178   | _ => error (loader_msg "undefined theory entry for" [name]));
   179 
   180 fun the_theory name thy =
   181   if Context.theory_name thy = name then thy
   182   else get_theory name;
   183 
   184 
   185 
   186 (** thy operations **)
   187 
   188 (* check state *)
   189 
   190 fun check_unfinished fail name =
   191   if known_thy name andalso is_finished name then
   192     fail (loader_msg "cannot update finished theory" [name])
   193   else ();
   194 
   195 fun check_files name =
   196   let
   197     val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
   198     val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
   199     val _ = null missing_files orelse
   200       error (loader_msg "unresolved dependencies of theory" [name] ^
   201         " on file(s): " ^ commas_quote missing_files);
   202   in () end;
   203 
   204 
   205 (* maintain update_time *)
   206 
   207 local
   208 
   209 fun is_outdated name =
   210   (case lookup_deps name of
   211     SOME (SOME {update_time, ...}) => update_time < 0
   212   | _ => false);
   213 
   214 fun unfinished name =
   215   if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE)
   216   else SOME name;
   217 
   218 in
   219 
   220 fun outdate_thy name =
   221   if is_finished name orelse is_outdated name then ()
   222   else CRITICAL (fn () =>
   223    (change_deps name (Option.map (fn {master, text, parents, files, ...} =>
   224     make_deps ~1 master text parents files)); perform Outdate name));
   225 
   226 fun touch_thys names =
   227   List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
   228 
   229 fun touch_thy name = touch_thys [name];
   230 fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
   231 
   232 end;
   233 
   234 
   235 (* load_file *)
   236 
   237 local
   238 
   239 fun provide path name info (deps as SOME {update_time, master, text, parents, files}) =
   240      (if AList.defined (op =) files path then ()
   241       else warning (loader_msg "undeclared dependency of theory" [name] ^
   242         " on file: " ^ quote (Path.implode path));
   243       SOME (make_deps update_time master text parents
   244         (AList.update (op =) (path, SOME info) files)))
   245   | provide _ _ _ NONE = NONE;
   246 
   247 fun run_file path =
   248   (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
   249     NONE => (ThyLoad.load_ml Path.current path; ())
   250   | SOME name =>
   251       (case lookup_deps name of
   252         SOME deps =>
   253           change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path))
   254       | NONE => (ThyLoad.load_ml Path.current path; ())));
   255 
   256 in
   257 
   258 fun provide_file path name =
   259   let
   260     val dir = master_directory name;
   261     val _ = check_unfinished error name;
   262   in
   263     (case ThyLoad.check_file dir path of
   264       SOME path_info => change_deps name (provide path name path_info)
   265     | NONE => error ("Could not find file " ^ quote (Path.implode path)))
   266   end;
   267 
   268 fun load_file time path =
   269   if time then
   270     let val name = Path.implode path in
   271       timeit (fn () =>
   272        (priority ("\n**** Starting file " ^ quote name ^ " ****");
   273         run_file path;
   274         priority ("**** Finished file " ^ quote name ^ " ****\n")))
   275     end
   276   else run_file path;
   277 
   278 fun exec_file time path = ML_Context.exec (fn () => load_file time path);
   279 
   280 val use = load_file false o Path.explode;
   281 val time_use = load_file true o Path.explode;
   282 
   283 end;
   284 
   285 
   286 (* load_thy *)
   287 
   288 fun required_by _ [] = ""
   289   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   290 
   291 fun load_thy time upd_time initiators name =
   292   let
   293     val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
   294     val (pos, text, files) =
   295       (case get_deps name of
   296         SOME {master = SOME (master_path, _), text as _ :: _, files, ...} =>
   297           (Path.position master_path, text, files)
   298       | _ => error (loader_msg "corrupted dependency information" [name]));
   299     val _ = touch_thy name;
   300     val _ = CRITICAL (fn () =>
   301       change_deps name (Option.map (fn {master, text, parents, files, ...} =>
   302         make_deps upd_time master text parents files)));
   303     val _ = OuterSyntax.load_thy name pos text (time orelse ! Output.timing);
   304   in
   305     CRITICAL (fn () =>
   306      (change_deps name
   307         (Option.map (fn {update_time, master, parents, files, ...} =>
   308           make_deps update_time master [] parents files));
   309       perform Update name))
   310   end;
   311 
   312 
   313 (* scheduling loader tasks *)
   314 
   315 datatype task = Task of (unit -> unit) | Finished | Running;
   316 fun task_finished Finished = true | task_finished _ = false;
   317 
   318 fun future_schedule task_graph =
   319   let
   320     val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
   321       (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
   322 
   323     fun future (name, body) tab =
   324       let
   325         val group = TaskQueue.new_group ();
   326         val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
   327         val x = Future.future (SOME group) deps true body;
   328       in (x, Symtab.update (name, Future.task_of x) tab) end;
   329   in
   330     #1 (fold_map future tasks Symtab.empty)
   331     |> uninterruptible (fn _ => Future.join_results)
   332     |> Exn.release_all
   333     |> ignore
   334   end;
   335 
   336 local
   337 
   338 fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
   339   | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
   340       if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
   341   | max_task _ task' = task';
   342 
   343 fun next_task G =
   344   let
   345     val tasks = Graph.minimals G |> map (fn name =>
   346       (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
   347     val finished = filter (task_finished o fst o snd) tasks;
   348   in
   349     if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
   350     else if null tasks then (Schedule.Terminate, G)
   351     else
   352       (case fold max_task tasks NONE of
   353         NONE => (Schedule.Wait, G)
   354       | SOME (name, (body, _)) =>
   355          (Schedule.Task {body = PrintMode.closure body,
   356            cont = Graph.del_nodes [name], fail = K Graph.empty},
   357           Graph.map_node name (K Running) G))
   358   end;
   359 
   360 fun schedule_seq tasks =
   361   Graph.topological_order tasks
   362   |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
   363 
   364 in
   365 
   366 fun schedule_tasks tasks n =
   367   let val m = Multithreading.max_threads_value () in
   368     if m <= 1 then schedule_seq tasks
   369     else if Multithreading.self_critical () then
   370      (warning (loader_msg "no multithreading within critical section" []);
   371       schedule_seq tasks)
   372     else if ! future_scheduler then future_schedule tasks
   373     else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
   374   end;
   375 
   376 end;
   377 
   378 
   379 (* require_thy -- checking database entries wrt. the file-system *)
   380 
   381 local
   382 
   383 fun check_ml master (src_path, info) =
   384   let val info' =
   385     (case info of NONE => NONE
   386     | SOME (_, id) =>
   387         (case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE
   388         | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
   389   in (src_path, info') end;
   390 
   391 fun check_deps dir name =
   392   (case lookup_deps name of
   393     SOME NONE => (true, NONE, get_parents name)
   394   | NONE =>
   395       let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
   396       in (false, init_deps (SOME master) text parents files, parents) end
   397   | SOME (deps as SOME {update_time, master, text, parents, files}) =>
   398       let
   399         val (thy_path, thy_id) = ThyLoad.check_thy dir name;
   400         val master' = SOME (thy_path, thy_id);
   401       in
   402         if Option.map #2 master <> SOME thy_id then
   403           let val {text = text', imports = parents', uses = files', ...} =
   404             ThyLoad.deps_thy dir name;
   405           in (false, init_deps master' text' parents' files', parents') end
   406         else
   407           let
   408             val files' = map (check_ml master') files;
   409             val current = update_time >= 0 andalso can get_theory name
   410               andalso forall (is_some o snd) files';
   411             val update_time' = if current then update_time else ~1;
   412             val deps' = SOME (make_deps update_time' master' text parents files');
   413           in (current, deps', parents) end
   414       end);
   415 
   416 fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
   417   SOME (make_deps update_time master (explode (File.read path)) parents files);
   418 
   419 in
   420 
   421 fun require_thys time initiators dir strs tasks =
   422       fold_map (require_thy time initiators dir) strs tasks |>> forall I
   423 and require_thy time initiators dir str tasks =
   424   let
   425     val path = Path.expand (Path.explode str);
   426     val name = Path.implode (Path.base path);
   427     val dir' = Path.append dir (Path.dir path);
   428     val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   429   in
   430     (case try (Graph.get_node (fst tasks)) name of
   431       SOME task => (task_finished task, tasks)
   432     | NONE =>
   433         let
   434           val (current, deps, parents) = check_deps dir' name
   435             handle ERROR msg => cat_error msg
   436               (loader_msg "the error(s) above occurred while examining theory" [name] ^
   437                 required_by "\n" initiators);
   438           val parent_names = map base_name parents;
   439 
   440           val (parents_current, (tasks_graph', tasks_len')) =
   441             require_thys time (name :: initiators)
   442               (Path.append dir (master_dir' deps)) parents tasks;
   443 
   444           val all_current = current andalso parents_current;
   445           val _ = if not all_current andalso known_thy name then outdate_thy name else ();
   446           val entry =
   447             if all_current then (deps, SOME (get_theory name))
   448             else (read_text deps, NONE);
   449           val _ = change_thys (new_deps name parent_names entry);
   450 
   451           val upd_time = serial ();
   452           val tasks_graph'' = tasks_graph' |> new_deps name parent_names
   453            (if all_current then Finished
   454             else Task (fn () => load_thy time upd_time initiators name));
   455           val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
   456         in (all_current, (tasks_graph'', tasks_len'')) end)
   457   end;
   458 
   459 end;
   460 
   461 
   462 (* use_thy etc. *)
   463 
   464 local
   465 
   466 fun gen_use_thy' req dir arg =
   467   let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0)
   468   in schedule_tasks tasks n end;
   469 
   470 fun gen_use_thy req str =
   471   let val name = base_name str in
   472     check_unfinished warning name;
   473     gen_use_thy' req Path.current str
   474   end;
   475 
   476 in
   477 
   478 val use_thys_dir = gen_use_thy' (require_thys false);
   479 val use_thys = use_thys_dir Path.current;
   480 val use_thy = gen_use_thy (require_thy false);
   481 val time_use_thy = gen_use_thy (require_thy true);
   482 
   483 end;
   484 
   485 
   486 (* remove theory *)
   487 
   488 fun remove_thy name =
   489   if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   490   else
   491     let val succs = thy_graph Graph.all_succs [name] in
   492       priority (loader_msg "removing" succs);
   493       CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
   494     end;
   495 
   496 val kill_thy = if_known_thy remove_thy;
   497 
   498 
   499 (* update_time *)
   500 
   501 structure UpdateTime = TheoryDataFun
   502 (
   503   type T = int;
   504   val empty = 0;
   505   val copy = I;
   506   fun extend _ = empty;
   507   fun merge _ _ = empty;
   508 );
   509 
   510 val thy_ord = int_ord o pairself UpdateTime.get;
   511 
   512 
   513 (* begin / end theory *)
   514 
   515 fun begin_theory name parents uses int =
   516   let
   517     val parent_names = map base_name parents;
   518     val dir = master_dir'' (lookup_deps name);
   519     val _ = check_unfinished error name;
   520     val _ = if int then use_thys_dir dir parents else ();
   521 
   522     val theory = Theory.begin_theory name (map get_theory parent_names);
   523 
   524     val deps =
   525       if known_thy name then get_deps name
   526       else init_deps NONE [] parents (map #1 uses);
   527     val _ = change_thys (new_deps name parent_names (deps, NONE));
   528 
   529     val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
   530     val update_time = if update_time > 0 then update_time else serial ();
   531     val theory' = theory
   532       |> UpdateTime.put update_time
   533       |> Present.begin_theory update_time dir uses;
   534 
   535     val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
   536     val theory'' =
   537       fold (fn x => Context.theory_map (exec_file false x) o Theory.checkpoint) uses_now theory';
   538   in theory'' end;
   539 
   540 fun end_theory theory =
   541   let
   542     val name = Context.theory_name theory;
   543     val _ = check_files name;
   544     val theory' = Theory.end_theory theory;
   545     val _ = change_thy name (fn (deps, _) => (deps, SOME theory'));
   546   in () end;
   547 
   548 
   549 (* register existing theories *)
   550 
   551 fun register_thy name =
   552   let
   553     val _ = priority ("Registering theory " ^ quote name);
   554     val thy = get_theory name;
   555     val _ = map get_theory (get_parents name);
   556     val _ = check_unfinished error name;
   557     val _ = touch_thy name;
   558     val master = #master (ThyLoad.deps_thy Path.current name);
   559     val upd_time = UpdateTime.get thy;
   560   in
   561     CRITICAL (fn () =>
   562      (change_deps name (Option.map
   563        (fn {parents, files, ...} => make_deps upd_time (SOME master) [] parents files));
   564       perform Update name))
   565   end;
   566 
   567 fun register_theory theory =
   568   let
   569     val name = Context.theory_name theory;
   570     val parents = Theory.parents_of theory;
   571     val parent_names = map Context.theory_name parents;
   572 
   573     fun err txt bads =
   574       error (loader_msg txt bads ^ "\ncannot register theory " ^ quote name);
   575 
   576     val nonfinished = filter_out is_finished parent_names;
   577     fun get_variant (x, y_name) =
   578       if Theory.eq_thy (x, get_theory y_name) then NONE
   579       else SOME y_name;
   580     val variants = map_filter get_variant (parents ~~ parent_names);
   581 
   582     fun register G =
   583       (Graph.new_node (name, (NONE, SOME theory)) G
   584         handle Graph.DUP _ => err "duplicate theory entry" [])
   585       |> add_deps name parent_names;
   586   in
   587     if not (null nonfinished) then err "non-finished parent theories" nonfinished
   588     else if not (null variants) then err "different versions of parent theories" variants
   589     else CRITICAL (fn () => (change_thys register; perform Update name))
   590   end;
   591 
   592 
   593 (* finish all theories *)
   594 
   595 fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
   596 
   597 end;