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