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