src/Pure/Thy/thy_info.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 9332 ff3a86a00ea5
child 9417 c4f7c959eaee
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
     1 (*  Title:      Pure/Thy/thy_info.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Theory loader database, including theory and file dependencies.
     7 *)
     8 
     9 signature BASIC_THY_INFO =
    10 sig
    11   val theory: string -> theory
    12   val theory_of_sign: Sign.sg -> theory
    13   val theory_of_thm: thm -> theory
    14 (*val use: string -> unit*)             (*exported later*)
    15   val time_use: string -> unit
    16   val touch_thy: string -> unit
    17   val use_thy: string -> unit
    18   val update_thy: string -> unit
    19   val remove_thy: string -> unit
    20   val time_use_thy: string -> unit
    21   val use_thy_only: string -> unit
    22   val update_thy_only: string -> unit
    23 end;
    24 
    25 signature THY_INFO =
    26 sig
    27   include BASIC_THY_INFO
    28   datatype action = Update | Outdate | Remove
    29   val str_of_action: action -> string
    30   val add_hook: (action -> string -> unit) -> unit
    31   val names: unit -> string list
    32   val known_thy: string -> bool
    33   val check_known_thy: string -> bool
    34   val if_known_thy: (string -> unit) -> string -> unit
    35   val lookup_theory: string -> theory option
    36   val get_theory: string -> theory
    37   val get_preds: string -> string list
    38   val loaded_files: string -> Path.T list
    39   val touch_child_thys: string -> unit
    40   val touch_all_thys: unit -> unit
    41   val load_file: bool -> Path.T -> unit
    42   val use: string -> unit
    43   val quiet_update_thy: bool -> string -> unit
    44   val begin_theory: (string -> string list -> (Path.T * bool) list -> theory -> theory) ->
    45     bool -> string -> string list -> (Path.T * bool) list -> theory
    46   val end_theory: theory -> theory
    47   val finish: unit -> unit
    48   val register_theory: theory -> unit
    49 end;
    50 
    51 structure ThyInfo: THY_INFO =
    52 struct
    53 
    54 
    55 (** theory loader actions and hooks **)
    56 
    57 datatype action = Update | Outdate | Remove;
    58 val str_of_action = fn Update => "Update" | Outdate => "Outdate" | Remove => "Remove";
    59 
    60 local
    61   val hooks = ref ([]: (action -> string -> unit) list);
    62 in
    63   fun add_hook f = hooks := f :: ! hooks;
    64   fun perform action name = seq (fn f => (try (fn () => f action name) (); ())) (! hooks);
    65 end;
    66 
    67 
    68 
    69 (** thy database **)
    70 
    71 (* messages *)
    72 
    73 fun gen_msg txt [] = txt
    74   | gen_msg txt names = txt ^ " " ^ commas_quote names;
    75 
    76 fun loader_msg txt names = gen_msg ("Theory loader: " ^ txt) names;
    77 
    78 val show_path = space_implode " via " o map quote;
    79 fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) [];
    80 
    81 
    82 (* derived graph operations *)
    83 
    84 fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
    85   handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
    86 
    87 fun upd_deps name entry G =
    88   foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name)
    89   |> Graph.map_node name (K entry);
    90 
    91 fun update_node name parents entry G =
    92   (if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G)
    93   |> add_deps name parents;
    94    
    95 
    96 
    97 (* thy database *)
    98 
    99 type deps =
   100   {present: bool, outdated: bool,
   101     master: ThyLoad.master option, files: (Path.T * (Path.T * File.info) option) list};
   102 
   103 fun make_deps present outdated master files =
   104   {present = present, outdated = outdated, master = master, files = files}: deps;
   105 
   106 fun init_deps master files = Some (make_deps false true master (map (rpair None) files));
   107 
   108 
   109 type thy = deps option * theory option;
   110 
   111 local
   112   val database = ref (Graph.empty: thy Graph.T);
   113 in
   114   fun get_thys () = ! database;
   115   val change_thys = Library.change database;
   116 end;
   117 
   118 
   119 (* access thy graph *)
   120 
   121 fun thy_graph f x = f (get_thys ()) x;
   122 fun get_names () = Graph.keys (get_thys ());
   123 
   124 
   125 (* access thy *)
   126 
   127 fun lookup_thy name =
   128   Some (thy_graph Graph.get_node name) handle Graph.UNDEF _ => None;
   129 
   130 val known_thy = is_some o lookup_thy;
   131 fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
   132 fun if_known_thy f name = if check_known_thy name then f name else ();
   133 
   134 fun get_thy name =
   135   (case lookup_thy name of
   136     Some thy => thy
   137   | None => error (loader_msg "nothing known about theory" [name]));
   138 
   139 fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
   140 
   141 
   142 (* access deps *)
   143 
   144 val lookup_deps = apsome #1 o lookup_thy;
   145 val get_deps = #1 o get_thy;
   146 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
   147 
   148 fun is_finished name = is_none (get_deps name);
   149 fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
   150 
   151 fun loaded_files name =
   152   (case get_deps name of
   153     None => []
   154   | Some {master, files, ...} =>
   155       (case master of Some m => [#1 (ThyLoad.get_thy m)] | None => []) @
   156       (mapfilter (apsome #1 o #2) files));
   157 
   158 fun get_preds name =
   159   (thy_graph Graph.imm_preds name) handle Graph.UNDEF _ =>
   160     error (loader_msg "nothing known about theory" [name]);
   161 
   162 
   163 (* access theory *)
   164 
   165 fun lookup_theory name =
   166   (case lookup_thy name of
   167     Some (_, Some thy) => Some thy
   168   | _ => None);
   169 
   170 fun get_theory name =
   171   (case lookup_theory name of
   172     (Some theory) => theory
   173   | _ => error (loader_msg "undefined theory entry for" [name]));
   174 
   175 val theory_of_sign = get_theory o Sign.name_of;
   176 val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
   177 
   178 fun put_theory name theory = change_thy name (fn (deps, _) => (deps, Some theory));
   179 
   180 
   181 
   182 (** thy operations **)
   183 
   184 (* maintain 'outdated' flag *)
   185 
   186 local
   187 
   188 fun is_outdated name =
   189   (case lookup_deps name of
   190     Some (Some {outdated, ...}) => outdated
   191   | _ => false);
   192 
   193 fun outdate_thy name =
   194   if is_finished name orelse is_outdated name then ()
   195   else (change_deps name (apsome (fn {present, outdated = _, master, files} =>
   196     make_deps present true master files)); perform Outdate name);
   197 
   198 fun check_unfinished name =
   199   if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); None)
   200   else Some name;
   201 
   202 in
   203 
   204 fun touch_thys names =
   205   seq outdate_thy (thy_graph Graph.all_succs (mapfilter check_unfinished names));
   206 
   207 fun touch_thy name = touch_thys [name];
   208 fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
   209 
   210 fun touch_all_thys () = seq outdate_thy (get_names ());
   211 
   212 end;
   213 
   214 
   215 (* check 'finished' state *)
   216 
   217 fun check_unfinished fail name =
   218   if known_thy name andalso is_finished name then
   219     fail (loader_msg "cannot update finished theory" [name])
   220   else ();
   221 
   222 
   223 (* load_file *)
   224 
   225 local
   226 
   227 fun provide path name info (deps as Some {present, outdated, master, files}) =
   228      (if exists (equal path o #1) files then ()
   229       else warning (loader_msg "undeclared dependency of theory" [name] ^
   230         " on file: " ^ quote (Path.pack path));
   231       Some (make_deps present outdated master (overwrite (files, (path, Some info)))))
   232   | provide _ _ _ None = None;
   233 
   234 fun run_file path =
   235   (case apsome PureThy.get_name (Context.get_context ()) of
   236     None => (ThyLoad.load_file path; ())
   237   | Some name =>
   238       if known_thy name then change_deps name (provide path name (ThyLoad.load_file path))
   239       else (ThyLoad.load_file path; ()));
   240 
   241 in
   242 
   243 fun load_file time path =
   244   if time then
   245     let val name = Path.pack path in
   246       timeit (fn () =>
   247        (writeln ("\n**** Starting file " ^ quote name ^ " ****");
   248         run_file path;
   249         writeln ("**** Finished file " ^ quote name ^ " ****\n")))
   250     end
   251   else run_file path;
   252 
   253 val use = load_file false o Path.unpack;
   254 val time_use = load_file true o Path.unpack;
   255 
   256 end;
   257 
   258 
   259 (* load_thy *)
   260 
   261 fun required_by [] = ""
   262   | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
   263 
   264 fun load_thy ml time initiators dir name parents =
   265   let
   266     val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
   267 
   268     val _ = touch_thy name;
   269     val master = ThyLoad.load_thy dir name ml time;
   270 
   271     val files = get_files name;
   272     val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
   273   in
   274     if null missing_files then ()
   275     else warning (loader_msg "unresolved dependencies of theory" [name] ^
   276       " on file(s): " ^ commas_quote missing_files);
   277     change_deps name (fn _ => Some (make_deps true false (Some master) files));
   278     perform Update name
   279   end;
   280 
   281 
   282 (* require_thy *)
   283 
   284 local
   285 
   286 fun load_deps ml dir name =
   287   let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml
   288   in (Some (init_deps (Some master) files), parents) end;
   289 
   290 fun file_current (_, None) = false
   291   | file_current (path, info) = (info = ThyLoad.check_file path);
   292 
   293 fun current_deps ml strict dir name =
   294   (case lookup_deps name of
   295     None => (false, load_deps ml dir name)
   296   | Some deps =>
   297       let val same_deps = (None, thy_graph Graph.imm_preds name) in
   298         (case deps of
   299           None => (true, same_deps)
   300         | Some {present, outdated, master, files} =>
   301             if present andalso not strict then (true, same_deps)
   302             else
   303               let val master' = Some (ThyLoad.check_thy dir name ml) in
   304                 if master <> master' then (false, load_deps ml dir name)
   305                 else (not outdated andalso forall file_current files, same_deps)
   306               end)
   307       end);
   308 
   309 fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
   310   let
   311     val path = Path.expand (Path.unpack str);
   312     val name = Path.pack (Path.base path);
   313   in
   314     if name mem_string initiators then error (cycle_msg initiators) else ();
   315     if known_thy name andalso is_finished name orelse name mem_string visited then
   316       (visited, (true, name))
   317     else
   318       let
   319         val dir = Path.append prfx (Path.dir path);
   320         val req_parent =
   321           require_thy true time (strict andalso keep_strict) keep_strict (name :: initiators) dir;
   322 
   323         val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
   324           error (loader_msg "the error(s) above occurred while examining theory" [name] ^
   325             (if null initiators then "" else "\n" ^ required_by initiators));
   326         val (visited', parent_results) = foldl_map req_parent (name :: visited, parents);
   327 
   328         val result =
   329           if current andalso forall #1 parent_results then true
   330           else
   331             ((case new_deps of
   332               Some deps => change_thys (update_node name parents (deps, None))
   333             | None => ());
   334              load_thy ml (time orelse ! Library.timing) initiators dir name parents;
   335              false);
   336       in (visited', (result, name)) end
   337   end;
   338 
   339 fun gen_use_thy req s =
   340   let val (_, (_, name)) = req [] Path.current ([], s)
   341   in Context.context (get_theory name) end;
   342 
   343 fun warn_finished f name = (check_unfinished warning name; f name);
   344 
   345 in
   346 
   347 val weak_use_thy        = gen_use_thy (require_thy true false false false);
   348 fun quiet_update_thy ml = gen_use_thy (require_thy ml false true true);
   349 
   350 val use_thy          = warn_finished (gen_use_thy (require_thy true false true false));
   351 val time_use_thy     = warn_finished (gen_use_thy (require_thy true true true false));
   352 val use_thy_only     = warn_finished (gen_use_thy (require_thy false false true false));
   353 val update_thy       = warn_finished (gen_use_thy (require_thy true false true true));
   354 val update_thy_only  = warn_finished (gen_use_thy (require_thy false false true true));
   355 
   356 end;
   357 
   358 
   359 (* remove_thy *)
   360 
   361 fun remove_thy name =
   362   if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   363   else
   364     let val succs = thy_graph Graph.all_succs [name] in
   365       writeln (loader_msg "removing" succs);
   366       seq (perform Remove) succs;
   367       change_thys (Graph.del_nodes succs)
   368     end;
   369 
   370 
   371 (* begin / end theory *)
   372 
   373 fun begin_theory present upd name parents paths =
   374   let
   375     val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
   376     val _ = check_unfinished error name;
   377     val _ = (map Path.basic parents; seq assert_thy parents);
   378     val theory = PureThy.begin_theory name (map get_theory parents);
   379     val deps =
   380       if known_thy name then get_deps name
   381       else (init_deps None (map #1 paths));   (*records additional ML files only!*)
   382     val _ = change_thys (update_node name parents (deps, Some theory));
   383     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
   384     val theory' = theory |> present name parents paths;
   385     val ((), theory'') = Context.pass_theory theory' (seq (load_file false)) use_paths;
   386   in theory'' end;
   387 
   388 fun end_theory theory =
   389   let
   390     val theory' = PureThy.end_theory theory;
   391     val name = PureThy.get_name theory;
   392   in put_theory name theory'; theory' end;
   393 
   394 
   395 (* finish all theories *)
   396 
   397 fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (None, entry)));
   398 
   399 
   400 (* register existing theories *)
   401 
   402 fun register_theory theory =
   403   let
   404     val name = PureThy.get_name theory;
   405     val parents = Theory.parents_of theory;
   406     val parent_names = map PureThy.get_name parents;
   407 
   408     fun err txt bads =
   409       error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]);
   410 
   411     val nonfinished = filter_out is_finished parent_names;
   412     fun get_variant (x, y_name) =
   413       if Theory.eq_thy (x, get_theory y_name) then None
   414       else Some y_name;
   415     val variants = mapfilter get_variant (parents ~~ parent_names);
   416 
   417     fun register G =
   418       (Graph.new_node (name, (None, Some theory)) G
   419         handle Graph.DUP _ => err "duplicate theory entry" [])
   420       |> add_deps name parent_names;
   421   in
   422     if not (null nonfinished) then err "non-finished parent theories" nonfinished
   423     else if not (null variants) then err "different versions of parent theories" variants
   424     else (change_thys register; perform Update name)
   425   end;
   426 
   427 
   428 (*final declarations of this structure*)
   429 val theory = get_theory;
   430 val names = get_names;
   431 
   432 end;
   433 
   434 structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
   435 open BasicThyInfo;