src/Pure/Thy/thy_info.ML
author wenzelm
Wed Feb 03 20:25:53 1999 +0100 (1999-02-03)
changeset 6219 b360065c2b07
parent 6211 43d0efafa025
child 6233 9cc37487f995
permissions -rw-r--r--
check_thy: include ML stamp;
     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 *)
    21 
    22 signature BASIC_THY_INFO =
    23 sig
    24   val theory: string -> theory
    25   val theory_of_sign: Sign.sg -> theory
    26   val theory_of_thm: thm -> theory
    27   val touch_thy: string -> unit
    28   val use_thy: string -> unit
    29   val update_thy: string -> unit
    30   val time_use_thy: string -> unit
    31 end;
    32 
    33 signature THY_INFO =
    34 sig
    35   include BASIC_THY_INFO
    36   val verbose: bool ref
    37   val names: unit -> string list
    38   val get_theory: string -> theory
    39   val put_theory: theory -> unit
    40   val load_file: Path.T -> unit
    41   val use_thy_only: string -> unit
    42   val begin_theory: string -> string list -> theory
    43   val end_theory: theory -> theory
    44   val finish_all: unit -> unit
    45   val register_theory: theory -> unit
    46 end;
    47 
    48 signature PRIVATE_THY_INFO =
    49 sig
    50   include THY_INFO
    51 (* FIXME
    52   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
    53     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> unit
    54   val print_data: Object.kind -> string -> unit
    55   val get_data: Object.kind -> (Object.T -> 'a) -> string -> 'a
    56   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> unit
    57 *)
    58 end;
    59 
    60 structure ThyInfo: PRIVATE_THY_INFO =
    61 struct
    62 
    63 
    64 (** thy database **)
    65 
    66 (* messages *)
    67 
    68 val verbose = ref false;
    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 (* derived graph operations *)		(* FIXME more abstract (!?) *)
    80 
    81 fun add_deps name parents G =
    82   foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
    83     handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
    84 
    85 fun del_deps name G =           (* FIXME GC (!?!?) *)
    86   foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name);
    87 
    88 fun update_node name parents entry G =
    89   add_deps name parents
    90     (if can (Graph.get_node G) name then del_deps name G else Graph.new_node (name, entry) G);
    91 
    92 
    93 (* thy database *)
    94 
    95 type deps =
    96   {present: bool, outdated: bool,
    97     master: File.info option, files: (Path.T * File.info option) list} option;
    98 
    99 fun make_depends present outdated master files =
   100   Some {present = present, outdated = outdated, master = master, files = files}: deps;
   101 
   102 type thy = deps * (theory * Object.T Symtab.table) option;
   103 type kind = Object.kind * (Object.T * (Object.T -> unit));
   104 
   105 
   106 local
   107   val database = ref (Graph.empty: thy Graph.T, Symtab.empty: kind Symtab.table);
   108 in
   109 
   110 fun get_thys () = #1 (! database);
   111 fun get_kinds () = #2 (! database);
   112 fun change_thys f = database := (f (get_thys ()), get_kinds ());
   113 fun change_kinds f = database := (get_thys (), f (get_kinds ()));
   114 
   115 end;
   116 
   117 
   118 (* access thy graph *)
   119 
   120 fun thy_graph f x = f (get_thys ()) x;
   121 fun get_names () = map #1 (Graph.get_nodes (get_thys ()));
   122 
   123 
   124 (* access thy *)
   125 
   126 fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
   127 
   128 fun get_thy name =
   129   (case lookup_thy name of
   130     Some thy => thy
   131   | None => error (loader_msg "nothing known about theory" [name]));
   132 
   133 fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
   134 
   135 
   136 (* access deps *)
   137 
   138 val lookup_deps = apsome #1 o lookup_thy;
   139 val get_deps = #1 o get_thy;
   140 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
   141 
   142 fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
   143 fun is_finished name = is_none (get_deps name);
   144 
   145 
   146 (* access theory *)
   147 
   148 fun get_theory name =
   149   (case get_thy name of
   150     (_, Some (theory, _)) => theory
   151   | _ => error (loader_msg "undefined theory entry for" [name]));
   152 
   153 val theory_of_sign = get_theory o Sign.name_of;
   154 val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
   155 
   156 fun put_theory theory =
   157   change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, (Some (theory, Symtab.empty))));
   158 
   159 
   160 
   161 (** thy data **)  (* FIXME *)
   162 
   163 
   164 
   165 (** thy operations **)
   166 
   167 fun FIXME msg = writeln ("DEBUG:\n" ^ msg);
   168 
   169 
   170 (* touch_thy -- mark as outdated *)
   171 
   172 fun touch_thy name = change_deps name
   173   (fn None => (warning (loader_msg "tried to touch finished theory" [name]); None)
   174     | Some {present, outdated = _, master, files} =>
   175         make_depends present true 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 on file(s) " ^ commas_quote missing_files ^
   196       "\nfor theory") [name]);
   197     change_deps name (fn _ => make_depends true false (Some master) files)
   198   end;
   199 
   200 
   201 (* load_file *)
   202 
   203 fun load_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             make_depends present outdated master (overwrite (files, (path, Some info)))
   208           else (warning (loader_msg ("undeclared dependency on file " ^ quote (Path.pack path) ^
   209             "\nfor theory") [name]); 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 
   220 (* require_thy *)
   221 
   222 fun init_deps master files = make_depends false false master (map (rpair None) files);
   223 
   224 fun load_deps name ml =
   225   let val (master, (parents, files)) = ThyLoad.deps_thy name ml
   226   in (Some (init_deps (Some master) files), parents) end;
   227 
   228 fun file_current (_, None) = false
   229   | file_current (path, info) = info = ThyLoad.check_file path;
   230 
   231 fun current_deps ml strict name =
   232   (case lookup_deps name of
   233     None => (false, load_deps name ml)
   234   | Some deps =>
   235       let val same_deps = (None, thy_graph Graph.imm_preds name) in
   236         (case deps of
   237           None => (true, same_deps)
   238         | Some {present, outdated, master, files} =>
   239             if present andalso not strict then (true, same_deps)
   240             else
   241               let val master' = Some (ThyLoad.check_thy name ml) in
   242                 if master <> master' then (false, load_deps name ml)
   243                 else (not outdated andalso forall file_current files, same_deps)
   244               end)
   245       end);
   246 
   247 fun outdated name =
   248   (case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false);
   249 
   250 fun untouch None = None
   251   | untouch (Some {present, outdated = _, master, files}) =
   252       make_depends present false master files;
   253 
   254 fun require_thy ml time strict keep_strict initiators name =
   255   let
   256     val require_parent =
   257       require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
   258     val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
   259       error (loader_msg "The error(s) above occurred while examining theory" [name] ^ "\n" ^
   260         required_by initiators);
   261     val pre_outdated = outdated name;
   262   in
   263     seq require_parent parents;
   264     if current andalso pre_outdated = outdated name then ()	(* FIXME ?? *)
   265     else
   266       ((case new_deps of
   267         Some deps => change_thys (update_node name parents (untouch deps, None))
   268       | None => ()); load_thy ml time initiators name parents)
   269   end;
   270 
   271 val weak_use_thy = require_thy true false false false [];
   272 val use_thy      = require_thy true false true false [];
   273 val update_thy   = require_thy true false true true [];
   274 val time_use_thy = require_thy true true true false [];
   275 val use_thy_only = require_thy false false true false [];
   276 
   277 
   278 (* begin / end theory *)		(* FIXME tune *)
   279 
   280 fun begin_theory name parents =
   281   let
   282     val _ = seq weak_use_thy parents;
   283     val theory = PureThy.begin_theory name (map get_theory parents);
   284     val _ = change_thys (update_node name parents (init_deps None [], Some (theory, Symtab.empty)));
   285   in theory end;
   286 
   287 fun end_theory theory =
   288   let val theory' = PureThy.end_theory theory
   289   in put_theory theory'; theory' end;
   290 
   291 
   292 (* finish entries *)
   293 
   294 (* FIXME
   295 fun finishs names =
   296   let
   297     fun err txt bads =
   298       error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot mark" names ^ " as finished");
   299 
   300     val all_preds = thy_graph Graph.all_preds names;
   301     val noncurrent = filter_out is_current all_preds;
   302     val unfinished = filter_out is_finished (all_preds \\ names);
   303   in
   304     if not (null noncurrent) then err "non-current theories" noncurrent
   305     else if not (null unfinished) then err "unfinished ancestor theories" unfinished
   306     else seq (fn name => change_thy name (apfst (K Finished)))
   307   end;
   308 
   309 fun finish name = finishs [name];
   310 *)
   311 
   312 fun update_all () = ();         (* FIXME fake *)
   313 
   314 fun finish_all () = (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
   315 
   316 
   317 (* register existing theories *)
   318 
   319 fun register_theory theory =
   320   let
   321     val name = PureThy.get_name theory;
   322     val parents = Theory.parents_of theory;
   323     val parent_names = map PureThy.get_name parents;
   324 
   325     fun err txt bads =
   326       error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]);
   327 
   328     val unfinished = filter_out is_finished parent_names;
   329     fun get_variant (x, y_name) =
   330       if Theory.eq_thy (x, get_theory y_name) then None
   331       else Some y_name;
   332     val variants = mapfilter get_variant (parents ~~ parent_names);
   333 
   334     fun register G =
   335       (Graph.new_node (name, (None, Some (theory, Symtab.empty))) G
   336         handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
   337       |> add_deps name parent_names;
   338   in
   339     if not (null unfinished) then err "unfinished parent theories" unfinished
   340     else if not (null variants) then err "different versions of parent theories" variants
   341     else change_thys register
   342   end;
   343 
   344 
   345 (*final declarations of this structure*)
   346 val theory = get_theory;
   347 val names = get_names;
   348 
   349 end;
   350 
   351 structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
   352 open BasicThyInfo;