src/Pure/Thy/thy_info.ML
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59366 e94df7f6b608
child 60937 51425cbe8ce9
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     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 master_directory: string -> Path.T
    14   val remove_thy: string -> unit
    15   val use_theories:
    16     {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
    17     (string * Position.T) list -> unit
    18   val use_thys: (string * Position.T) list -> unit
    19   val use_thy: string * Position.T -> unit
    20   val script_thy: Position.T -> string -> theory -> theory
    21   val register_thy: theory -> unit
    22   val finish: unit -> unit
    23 end;
    24 
    25 structure Thy_Info: THY_INFO =
    26 struct
    27 
    28 (** thy database **)
    29 
    30 (* messages *)
    31 
    32 val show_path = space_implode " via " o map quote;
    33 
    34 fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
    35 
    36 
    37 (* derived graph operations *)
    38 
    39 fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
    40   handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
    41 
    42 fun new_entry name parents entry =
    43   String_Graph.new_node (name, entry) #> add_deps name parents;
    44 
    45 
    46 (* global thys *)
    47 
    48 type deps =
    49  {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
    50   imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
    51 
    52 fun make_deps master imports : deps = {master = master, imports = imports};
    53 
    54 fun master_dir (d: deps option) =
    55   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
    56 
    57 fun base_name s = Path.implode (Path.base (Path.explode s));
    58 
    59 local
    60   val global_thys =
    61     Synchronized.var "Thy_Info.thys"
    62       (String_Graph.empty: (deps option * theory option) String_Graph.T);
    63 in
    64   fun get_thys () = Synchronized.value global_thys;
    65   fun change_thys f = Synchronized.change global_thys f;
    66 end;
    67 
    68 fun get_names () = String_Graph.topological_order (get_thys ());
    69 
    70 
    71 (* access thy *)
    72 
    73 fun lookup thys name = try (String_Graph.get_node thys) name;
    74 fun lookup_thy name = lookup (get_thys ()) name;
    75 
    76 fun get thys name =
    77   (case lookup thys name of
    78     SOME thy => thy
    79   | NONE => error ("Theory loader: nothing known about theory " ^ quote name));
    80 
    81 fun get_thy name = get (get_thys ()) name;
    82 
    83 
    84 (* access deps *)
    85 
    86 val lookup_deps = Option.map #1 o lookup_thy;
    87 
    88 val master_directory = master_dir o #1 o get_thy;
    89 
    90 
    91 (* access theory *)
    92 
    93 fun lookup_theory name =
    94   (case lookup_thy name of
    95     SOME (_, SOME theory) => SOME theory
    96   | _ => NONE);
    97 
    98 fun get_theory name =
    99   (case lookup_theory name of
   100     SOME theory => theory
   101   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
   102 
   103 val get_imports = Resources.imports_of o get_theory;
   104 
   105 
   106 
   107 (** thy operations **)
   108 
   109 (* remove *)
   110 
   111 fun remove name thys =
   112   (case lookup thys name of
   113     NONE => thys
   114   | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name)
   115   | SOME _ =>
   116       let
   117         val succs = String_Graph.all_succs thys [name];
   118         val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
   119       in fold String_Graph.del_node succs thys end);
   120 
   121 val remove_thy = change_thys o remove;
   122 
   123 
   124 (* update *)
   125 
   126 fun update deps theory thys =
   127   let
   128     val name = Context.theory_name theory;
   129     val parents = map Context.theory_name (Theory.parents_of theory);
   130 
   131     val thys' = remove name thys;
   132     val _ = map (get thys') parents;
   133   in new_entry name parents (SOME deps, SOME theory) thys' end;
   134 
   135 fun update_thy deps theory = change_thys (update deps theory);
   136 
   137 
   138 (* scheduling loader tasks *)
   139 
   140 datatype result =
   141   Result of {theory: theory, exec_id: Document_ID.exec,
   142     present: unit -> unit, commit: unit -> unit, weight: int};
   143 
   144 fun theory_result theory =
   145   Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
   146 
   147 fun result_theory (Result {theory, ...}) = theory;
   148 fun result_present (Result {present, ...}) = present;
   149 fun result_commit (Result {commit, ...}) = commit;
   150 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
   151 
   152 fun join_theory (Result {theory, exec_id, ...}) =
   153   let
   154     (*toplevel proofs and diags*)
   155     val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
   156     (*fully nested proofs*)
   157     val res = Exn.capture Thm.join_theory_proofs theory;
   158   in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
   159 
   160 datatype task =
   161   Task of Path.T * string list * (theory list -> result) |
   162   Finished of theory;
   163 
   164 fun task_finished (Task _) = false
   165   | task_finished (Finished _) = true;
   166 
   167 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
   168 
   169 local
   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 = 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 in
   223 
   224 fun schedule_tasks tasks =
   225   if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
   226 
   227 end;
   228 
   229 
   230 (* require_thy -- checking database entries wrt. the file-system *)
   231 
   232 local
   233 
   234 fun required_by _ [] = ""
   235   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   236 
   237 fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents =
   238   let
   239     val _ = remove_thy name;
   240     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
   241     val _ = Output.try_protocol_message (Markup.loading_theory name) [];
   242 
   243     val {master = (thy_path, _), imports} = deps;
   244     val dir = Path.dir thy_path;
   245     val header = Thy_Header.make (name, pos) imports keywords;
   246 
   247     val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   248 
   249     val exec_id = Document_ID.make ();
   250     val _ =
   251       Execution.running Document_ID.none exec_id [] orelse
   252         raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
   253 
   254     val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
   255     val (theory, present, weight) =
   256       Resources.load_thy document last_timing update_time dir header text_pos text
   257         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
   258     fun commit () = update_thy deps theory;
   259   in
   260     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   261   end;
   262 
   263 fun check_deps dir name =
   264   (case lookup_deps name of
   265     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   266   | NONE =>
   267       let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
   268       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   269   | SOME (SOME {master, ...}) =>
   270       let
   271         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
   272           keywords = keywords'} = Resources.check_thy dir name;
   273         val deps' = SOME (make_deps master' imports', text');
   274         val current =
   275           #2 master = #2 master' andalso
   276             (case lookup_theory name of
   277               NONE => false
   278             | SOME theory => Resources.loaded_files_current theory);
   279       in (current, deps', theory_pos', imports', keywords') end);
   280 
   281 in
   282 
   283 fun require_thys document last_timing initiators dir strs tasks =
   284       fold_map (require_thy document last_timing initiators dir) strs tasks |>> forall I
   285 and require_thy document last_timing initiators dir (str, require_pos) tasks =
   286   let
   287     val path = Path.expand (Path.explode str);
   288     val name = Path.implode (Path.base path);
   289     val node_name = File.full_path dir (Resources.thy_path path);
   290     fun check_entry (Task (node_name', _, _)) =
   291           if node_name = node_name' then ()
   292           else
   293             error ("Incoherent imports for theory " ^ quote name ^
   294               Position.here require_pos ^ ":\n" ^
   295               "  " ^ Path.print node_name ^ "\n" ^
   296               "  " ^ Path.print node_name')
   297       | check_entry _ = ();
   298   in
   299     (case try (String_Graph.get_node tasks) name of
   300       SOME task => (check_entry task; (task_finished task, tasks))
   301     | NONE =>
   302         let
   303           val dir' = Path.append dir (Path.dir path);
   304           val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   305 
   306           val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
   307             handle ERROR msg =>
   308               cat_error msg
   309                 ("The error(s) above occurred for theory " ^ quote name ^
   310                   Position.here require_pos ^ required_by "\n" initiators);
   311 
   312           val parents = map (base_name o #1) imports;
   313           val (parents_current, tasks') =
   314             require_thys document last_timing (name :: initiators)
   315               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
   316 
   317           val all_current = current andalso parents_current;
   318           val task =
   319             if all_current then Finished (get_theory name)
   320             else
   321               (case deps of
   322                 NONE => raise Fail "Malformed deps"
   323               | SOME (dep, text) =>
   324                   let
   325                     val update_time = serial ();
   326                     val load =
   327                       load_thy document last_timing initiators update_time dep
   328                         text (name, theory_pos) keywords;
   329                   in Task (node_name, parents, load) end);
   330 
   331           val tasks'' = new_entry name parents task tasks';
   332         in (all_current, tasks'') end)
   333   end;
   334 
   335 end;
   336 
   337 
   338 (* use_thy *)
   339 
   340 fun use_theories {document, last_timing, master_dir} imports =
   341   schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty));
   342 
   343 val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
   344 val use_thy = use_thys o single;
   345 
   346 
   347 (* toplevel scripting -- without maintaining database *)
   348 
   349 fun script_thy pos txt thy =
   350   let
   351     val trs =
   352       Outer_Syntax.parse thy pos txt
   353       |> map (Toplevel.modify_init (K thy));
   354     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
   355     val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
   356   in Toplevel.end_theory end_pos end_state end;
   357 
   358 
   359 (* register theory *)
   360 
   361 fun register_thy theory =
   362   let
   363     val name = Context.theory_name theory;
   364     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
   365     val imports = Resources.imports_of theory;
   366   in
   367     change_thys (fn thys =>
   368       let
   369         val thys' = remove name thys;
   370         val _ = writeln ("Registering theory " ^ quote name);
   371       in update (make_deps master imports) theory thys' end)
   372   end;
   373 
   374 
   375 (* finish all theories *)
   376 
   377 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
   378 
   379 end;