src/Pure/Thy/thy_info.ML
author wenzelm
Fri Mar 12 18:48:51 1999 +0100 (1999-03-12)
changeset 6362 bbbea7fecb93
parent 6329 bbd03b119f36
child 6377 e7b051fae849
permissions -rw-r--r--
removed obsolete user data stuff;
removed junk;
     1 (*  Title:      Pure/Thy/thy_info.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Theory loader database, including theory and file dependencies.
     6 
     7 TODO:
     8   - remove operation (GC!?);
     9   - update_all operation (!?);
    10   - put_theory:
    11       . allow for undef entry only;
    12       . elim (via theory_ref);
    13   - stronger handling of missing files (!?!?);
    14   - register_theory: do not require final parents (!?) (no?);
    15   - observe verbose flag;
    16 *)
    17 
    18 signature BASIC_THY_INFO =
    19 sig
    20   val theory: string -> theory
    21   val theory_of_sign: Sign.sg -> theory
    22   val theory_of_thm: thm -> theory
    23 (*val use: string -> unit*)             (*exported later*)
    24   val time_use: string -> unit
    25   val touch_thy: string -> unit
    26   val use_thy: string -> unit
    27   val update_thy: string -> unit
    28   val time_use_thy: string -> unit
    29 end;
    30 
    31 signature THY_INFO =
    32 sig
    33   include BASIC_THY_INFO
    34   val verbose: bool ref
    35   val names: unit -> string list
    36   val get_theory: string -> theory
    37   val put_theory: theory -> unit
    38   val loaded_files: string -> (Path.T * File.info) list
    39   val load_file: bool -> Path.T -> unit
    40   val use_path: Path.T -> unit
    41   val use: string -> unit
    42   val use_thy_only: string -> unit
    43   val begin_theory: string -> string list -> (Path.T * bool) list -> theory
    44   val end_theory: theory -> theory
    45   val finalize_all: unit -> unit
    46   val register_theory: theory -> unit
    47 end;
    48 
    49 structure ThyInfo: THY_INFO =
    50 struct
    51 
    52 
    53 (** thy database **)
    54 
    55 (* messages *)
    56 
    57 fun gen_msg txt [] = txt
    58   | gen_msg txt names = txt ^ " " ^ commas_quote names;
    59 
    60 fun loader_msg txt names = gen_msg ("Theory loader: " ^ txt) names;
    61 
    62 val show_path = space_implode " via " o map quote;
    63 fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
    64 
    65 
    66 (* verbose mode *)
    67 
    68 val verbose = ref false;
    69 
    70 fun if_verbose f x = if ! verbose then f x else ();
    71 
    72 
    73 (* derived graph operations *)          (* FIXME more abstract (!?) *)
    74 
    75 fun add_deps name parents G =
    76   foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
    77     handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
    78 
    79 fun del_deps name G =           (* FIXME GC (!?!?) *)
    80   foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name);
    81 
    82 fun update_node name parents entry G =
    83   add_deps name parents
    84     (if can (Graph.get_node G) name then del_deps name G else Graph.new_node (name, entry) G);
    85 
    86 
    87 (* thy database *)
    88 
    89 type deps =
    90   {present: bool, outdated: bool,
    91     master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list};
    92 
    93 fun make_deps present outdated master files =
    94   {present = present, outdated = outdated, master = master, files = files}: deps;
    95 
    96 type thy = deps option * theory option;
    97 
    98 local
    99   val database = ref (Graph.empty: thy Graph.T);
   100 in
   101   fun get_thys () = ! database;
   102   fun change_thys f = database := (f (! database));
   103 end;
   104 
   105 
   106 (* access thy graph *)
   107 
   108 fun thy_graph f x = f (get_thys ()) x;
   109 fun get_names () = map #1 (Graph.get_nodes (get_thys ()));
   110 
   111 
   112 (* access thy *)
   113 
   114 fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
   115 
   116 fun get_thy name =
   117   (case lookup_thy name of
   118     Some thy => thy
   119   | None => error (loader_msg "nothing known about theory" [name]));
   120 
   121 fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
   122 
   123 
   124 (* access deps *)
   125 
   126 val lookup_deps = apsome #1 o lookup_thy;
   127 val get_deps = #1 o get_thy;
   128 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
   129 
   130 fun is_final name = is_none (get_deps name);
   131 fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
   132 val loaded_files = mapfilter #2 o get_files;
   133 
   134 
   135 (* access theory *)
   136 
   137 fun get_theory name =
   138   (case get_thy name of
   139     (_, Some theory) => theory
   140   | _ => error (loader_msg "undefined theory entry for" [name]));
   141 
   142 val theory_of_sign = get_theory o Sign.name_of;
   143 val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
   144 
   145 fun put_theory theory =
   146   change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, Some theory));
   147 
   148 
   149 
   150 (** thy operations **)
   151 
   152 (* maintain 'outdated' flag *)
   153 
   154 fun is_outdated name =
   155   (case lookup_deps name of
   156     Some (Some {outdated, ...}) => outdated
   157   | _ => false);
   158 
   159 fun outdate_thy name =
   160   if is_final name then ()
   161   else change_deps name (apsome (fn {present, outdated = _, master, files} =>
   162     make_deps present true master files));
   163 
   164 fun touch_thy name =
   165   if is_outdated name then ()
   166   else if is_final name then warning (loader_msg "tried to touch final theory" [name])
   167   else
   168     (case filter_out is_outdated (thy_graph Graph.all_succs [name]) \ name of
   169       [] => outdate_thy name
   170     | names =>
   171        (warning (loader_msg "the following theories become out-of-date:" names);
   172         seq outdate_thy names; outdate_thy name));
   173 
   174 val untouch_deps = apsome (fn {present, outdated = _, master, files}: deps =>
   175   make_deps present false master files);
   176 
   177 
   178 (* load_thy *)
   179 
   180 fun required_by [] = ""
   181   | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
   182 
   183 fun load_thy ml time initiators name parents =
   184   let
   185     val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
   186     val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
   187 
   188     val _ = seq touch_thy (thy_graph Graph.all_succs [name]);
   189     val master = ThyLoad.load_thy name ml time;
   190 
   191     val files = get_files name;
   192     val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
   193   in
   194     if null missing_files then ()
   195     else warning (loader_msg "unresolved dependencies of theory" [name] ^
   196       "\nfile(s): " ^ commas_quote missing_files);
   197     change_deps name (fn _ => Some (make_deps true false master files))
   198   end;
   199 
   200 
   201 (* load_file *)
   202 
   203 fun run_file path =
   204   let
   205     fun provide name info (deps as Some {present, outdated, master, files}) =
   206           if exists (equal path o #1) files then
   207             Some (make_deps present outdated master (overwrite (files, (path, Some info))))
   208           else (warning (loader_msg "undeclared dependency of theory" [name] ^
   209             "\nfile: " ^ quote (Path.pack path)); deps)
   210       | provide _ _ None = None;
   211   in
   212     (case apsome PureThy.get_name (Context.get_context ()) of
   213       None => (ThyLoad.load_file path; ())
   214     | Some name =>
   215         if is_some (lookup_thy name) then change_deps name (provide name (ThyLoad.load_file path))
   216         else (ThyLoad.load_file path; ()))
   217   end;
   218 
   219 fun load_file false path = run_file path
   220   | load_file true path =
   221       let val name = Path.pack path in
   222         timeit (fn () =>
   223          (writeln ("\n**** Starting file " ^ quote name ^ " ****");
   224           run_file path;
   225           writeln ("**** Finished file " ^ quote name ^ " ****\n")))
   226       end;
   227 
   228 val use_path = load_file false;
   229 val use = use_path o Path.unpack;
   230 val time_use = load_file true o Path.unpack;
   231 
   232 
   233 (* require_thy *)
   234 
   235 fun init_deps master files = Some (make_deps false false master (map (rpair None) files));
   236 
   237 fun load_deps name ml =
   238   let val (master, (parents, files)) = ThyLoad.deps_thy name ml
   239   in (Some (init_deps master files), parents) end;
   240 
   241 fun file_current (_, None) = false
   242   | file_current (path, info) = info = ThyLoad.check_file path;
   243 
   244 fun current_deps ml strict name =
   245   (case lookup_deps name of
   246     None => (false, load_deps name ml)
   247   | Some deps =>
   248       let val same_deps = (None, thy_graph Graph.imm_preds name) in
   249         (case deps of
   250           None => (true, same_deps)
   251         | Some {present, outdated, master, files} =>
   252             if present andalso not strict then (true, same_deps)
   253             else
   254               let val master' = ThyLoad.check_thy name ml in
   255                 if master <> master' then (false, load_deps name ml)
   256                 else (not outdated andalso forall file_current files, same_deps)
   257               end)
   258       end);
   259 
   260 fun require_thy ml time strict keep_strict initiators name =
   261   let
   262     val require_parent =
   263       require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
   264     val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
   265       error (loader_msg "The error(s) above occurred while examining theory" [name] ^
   266         (if null initiators then "" else "\n" ^ required_by initiators));
   267     val parents_current = map require_parent parents;
   268   in
   269     if current andalso forall I parents_current then true
   270     else
   271       ((case new_deps of
   272         Some deps => change_thys (update_node name parents (untouch_deps deps, None))
   273       | None => ());
   274         load_thy ml time initiators name parents;
   275         false)
   276   end;
   277 
   278 fun gen_use_thy f name = (f name; Context.context (get_theory name));
   279 
   280 val weak_use_thy = gen_use_thy (require_thy true false false false []);
   281 val use_thy      = gen_use_thy (require_thy true false true false []);
   282 val update_thy   = gen_use_thy (require_thy true false true true []);
   283 val time_use_thy = gen_use_thy (require_thy true true true false []);
   284 val use_thy_only = gen_use_thy (require_thy false false true false []);
   285 
   286 
   287 (* begin / end theory *)                (* FIXME tune *) (* FIXME files vs. paths (!?!?) *)
   288 
   289 fun begin_theory name parents paths =
   290   let
   291     val _ = seq weak_use_thy parents;
   292     val theory = PureThy.begin_theory name (map get_theory parents);
   293     val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
   294     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
   295   in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
   296 
   297 fun end_theory theory =
   298   let val theory' = PureThy.end_theory theory
   299   in put_theory theory'; theory' end;
   300 
   301 
   302 (* finalize entries *)
   303 
   304 fun update_all () = ();         (* FIXME fake *)
   305 
   306 fun finalize_all () =
   307   (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
   308 
   309 
   310 (* register existing theories *)
   311 
   312 fun register_theory theory =
   313   let
   314     val name = PureThy.get_name theory;
   315     val parents = Theory.parents_of theory;
   316     val parent_names = map PureThy.get_name parents;
   317 
   318     fun err txt bads =
   319       error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]);
   320 
   321     val nonfinal = filter_out is_final parent_names;
   322     fun get_variant (x, y_name) =
   323       if Theory.eq_thy (x, get_theory y_name) then None
   324       else Some y_name;
   325     val variants = mapfilter get_variant (parents ~~ parent_names);
   326 
   327     fun register G =
   328       (Graph.new_node (name, (None, Some theory)) G
   329         handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
   330       |> add_deps name parent_names;
   331   in
   332     if not (null nonfinal) then err "non-final parent theories" nonfinal
   333     else if not (null variants) then err "different versions of parent theories" variants
   334     else change_thys register
   335   end;
   336 
   337 
   338 (*final declarations of this structure*)
   339 val theory = get_theory;
   340 val names = get_names;
   341 
   342 end;
   343 
   344 structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
   345 open BasicThyInfo;