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