--- a/src/Pure/Thy/thy_info.ML Wed Feb 03 17:29:12 1999 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Feb 03 17:29:48 1999 +0100
@@ -1,132 +1,350 @@
(* Title: Pure/Thy/thy_info.ML
ID: $Id$
- Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
-
-Theory loader database.
-*)
+ Author: Markus Wenzel, TU Muenchen
-type thy_info =
- {path: string,
- children: string list, parents: string list,
- thy_time: string option, ml_time: string option,
- theory: theory option};
+Theory loader database: theory and file dependencies, theory values
+and user data.
-(*
- path: directory where theory's files are located
- (* FIXME do not store absolute path!!! *)
-
- thy_time, ml_time = None theory file has not been read yet
- = Some "" theory was read but has either been marked
- as outdated or there is no such file for
- this theory (see e.g. 'virtual' theories
- like Pure or theories without a ML file)
- theory = None theory has not been read yet
-
- parents: While 'children' contains all theories the theory depends
- on (i.e. also ones quoted in the .thy file),
- 'parents' only contains the theories which were used to form
- the base of this theory.
+TODO:
+ - check_thy: include ML stamp (!?!?);
+ - check all these versions of 'use' (!!);
+ - errors during require etc.: include initiators (!?);
+ - data: ThyInfoFun;
+ - remove operation (GC!?);
+ - update_all operation (!?);
+ - put_theory:
+ . include data;
+ . allow for undef entry only;
+ . elim (via theory_ref);
+ - stronger handling of missing files (!?!?);
+ - register_theory: do not require finished parents (!?) (no?);
+ - observe verbose flag;
*)
signature BASIC_THY_INFO =
sig
val theory: string -> theory
-end
+ val theory_of_sign: Sign.sg -> theory
+ val theory_of_thm: thm -> theory
+ val touch_thy: string -> unit
+ val use_thy: string -> unit
+ val update_thy: string -> unit
+ val time_use_thy: string -> unit
+end;
signature THY_INFO =
sig
include BASIC_THY_INFO
- val mk_info: string * string list * string list * theory -> string * thy_info
- val loaded_thys: thy_info Symtab.table ref
- val get_thyinfo: string -> thy_info option
- val store_theory: theory -> unit
- val path_of: string -> string
- val children_of: string -> string list
- val parents_of_name: string -> string list
- val thyinfo_of_sign: Sign.sg -> string * thy_info
- val theory_of_sign: Sign.sg -> theory
- val theory_of_thm: thm -> theory
+ val verbose: bool ref
+ val names: unit -> string list
+ val get_theory: string -> theory
+ val put_theory: theory -> unit
+ val load_file: Path.T -> unit
+ val use_thy_only: string -> unit
+ val begin_theory: string -> string list -> theory
+ val end_theory: theory -> theory
+ val finish_all: unit -> unit
+ val register_theory: theory -> unit
end;
-
-structure ThyInfo: THY_INFO =
-struct
-
-(* loaded theories *)
-
-fun mk_info (name, children, parents, theory) =
- (name, {path = "", children = children, parents = parents,
- thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
-
-(*preloaded theories*)
-val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
-
+signature PRIVATE_THY_INFO =
+sig
+ include THY_INFO
+(* FIXME
+ val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
+ (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> unit
+ val print_data: Object.kind -> string -> unit
+ val get_data: Object.kind -> (Object.T -> 'a) -> string -> 'a
+ val put_data: Object.kind -> ('a -> Object.T) -> 'a -> unit
+*)
+end;
-(* retrieve info *)
-
-fun err_not_stored name =
- error ("Theory " ^ quote name ^ " not stored by loader");
-
-fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
-
-fun the_thyinfo name =
- (case get_thyinfo name of
- Some info => info
- | None => err_not_stored name);
-
-fun thyinfo_of_sign sg =
- let val name = Sign.name_of sg
- in (name, the_thyinfo name) end;
+structure ThyInfo: PRIVATE_THY_INFO =
+struct
-(*path where theory's files are located*)
-val path_of = #path o the_thyinfo;
+(** thy database **)
+
+(* messages *)
+
+val verbose = ref false;
+
+fun gen_msg txt [] = txt
+ | gen_msg txt names = txt ^ " " ^ commas_quote names;
+
+fun loader_msg txt names = gen_msg ("Theory loader: " ^ txt) names;
+
+val show_path = space_implode " via " o map quote;
+fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
-(*try to get the theory object corresponding to a given signature*)
-fun theory_of_sign sg =
- (case thyinfo_of_sign sg of
- (_, {theory = Some thy, ...}) => thy
- | _ => sys_error "theory_of_sign");
+(* derived graph operations *) (* FIXME more abstract (!?) *)
-(*try to get the theory object corresponding to a given theorem*)
-val theory_of_thm = theory_of_sign o #sign o rep_thm;
+fun add_deps name parents G =
+ foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
+ handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));
-(*get all direct descendants of a theory*)
-fun children_of t =
- (case get_thyinfo t of
- Some {children, ...} => children
- | None => []);
+fun del_deps name G = (* FIXME GC (!?!?) *)
+ foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name);
-(*get all direct ancestors of a theory*)
-fun parents_of_name t =
- (case get_thyinfo t of
- Some {parents, ...} => parents
- | None => []);
-
-(*get theory object for a loaded theory*)
-fun theory name =
- (case get_thyinfo name of
- Some {theory = Some t, ...} => t
- | _ => err_not_stored name);
+fun update_node name parents entry G =
+ add_deps name parents
+ (if can (Graph.get_node G) name then del_deps name G else Graph.new_node (name, entry) G);
-(* store_theory *)
+(* thy database *)
+
+type deps =
+ {present: bool, outdated: bool,
+ master: File.info option, files: (Path.T * File.info option) list} option;
+
+fun make_depends present outdated master files =
+ Some {present = present, outdated = outdated, master = master, files = files}: deps;
-fun store_theory thy =
- let
- val name = PureThy.get_name thy;
- val {path, children, parents, thy_time, ml_time, theory = _} =
- the_thyinfo name;
- val info = {path = path, children = children, parents = parents,
- thy_time = thy_time, ml_time = ml_time, theory = Some thy};
- in
- loaded_thys := Symtab.update ((name, info), ! loaded_thys)
- end;
+type thy = deps * (theory * Object.T Symtab.table) option;
+type kind = Object.kind * (Object.T * (Object.T -> unit));
+
+local
+ val database = ref (Graph.empty: thy Graph.T, Symtab.empty: kind Symtab.table);
+in
+
+fun get_thys () = #1 (! database);
+fun get_kinds () = #2 (! database);
+fun change_thys f = database := (f (get_thys ()), get_kinds ());
+fun change_kinds f = database := (get_thys (), f (get_kinds ()));
end;
+(* access thy graph *)
+
+fun thy_graph f x = f (get_thys ()) x;
+fun get_names () = map #1 (Graph.get_nodes (get_thys ()));
+
+
+(* access thy *)
+
+fun lookup_thy name = Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None;
+
+fun get_thy name =
+ (case lookup_thy name of
+ Some thy => thy
+ | None => error (loader_msg "nothing known about theory" [name]));
+
+fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
+
+
+(* access deps *)
+
+val lookup_deps = apsome #1 o lookup_thy;
+val get_deps = #1 o get_thy;
+fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
+
+fun get_files name = (case get_deps name of Some {files, ...} => files | _ => []);
+fun is_finished name = is_none (get_deps name);
+
+
+(* access theory *)
+
+fun get_theory name =
+ (case get_thy name of
+ (_, Some (theory, _)) => theory
+ | _ => error (loader_msg "undefined theory entry for" [name]));
+
+val theory_of_sign = get_theory o Sign.name_of;
+val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
+
+fun put_theory theory =
+ change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, (Some (theory, Symtab.empty))));
+
+
+
+(** thy data **) (* FIXME *)
+
+
+
+(** thy operations **)
+
+fun FIXME msg = writeln ("DEBUG:\n" ^ msg);
+
+
+(* touch_thy -- mark as outdated *)
+
+fun touch_thy name = change_deps name
+ (fn None => (warning (loader_msg "tried to touch finished theory" [name]); None)
+ | Some {present, outdated = _, master, files} =>
+ make_depends present true master files);
+
+
+(* load_thy *)
+
+fun required_by [] = ""
+ | required_by initiators = " (required by " ^ show_path (rev initiators) ^ ")";
+
+fun load_thy ml time initiators name parents =
+ let
+ val _ = if name mem_string initiators then error (cycle_msg name (rev initiators)) else ();
+ val _ = writeln ("Loading theory " ^ quote name ^ required_by initiators);
+
+ val _ = seq touch_thy (thy_graph Graph.all_succs [name]);
+ val master = ThyLoad.load_thy name ml time;
+
+ val files = get_files name;
+ val missing_files = mapfilter (fn (path, None) => Some (Path.pack path) | _ => None) files;
+ in
+ if null missing_files then ()
+ else warning (loader_msg ("unresolved dependencies on file(s) " ^ commas_quote missing_files ^
+ "\nfor theory") [name]);
+ change_deps name (fn _ => make_depends true false (Some master) files)
+ end;
+
+
+(* load_file *)
+
+fun load_file path =
+ let
+ fun provide name info (deps as Some {present, outdated, master, files}) =
+ if exists (equal path o #1) files then
+ make_depends present outdated master (overwrite (files, (path, Some info)))
+ else (warning (loader_msg ("undeclared dependency on file " ^ quote (Path.pack path) ^
+ "\nfor theory") [name]); deps)
+ | provide _ _ None = None;
+ in
+ (case apsome PureThy.get_name (Context.get_context ()) of
+ None => (ThyLoad.load_file path; ())
+ | Some name =>
+ if is_some (lookup_thy name) then change_deps name (provide name (ThyLoad.load_file path))
+ else (ThyLoad.load_file path; ()))
+ end;
+
+
+(* require_thy *)
+
+fun init_deps master files = make_depends false false master (map (rpair None) files);
+
+fun load_deps name ml =
+ let val (master, (parents, files)) = ThyLoad.deps_thy name ml
+ in (Some (init_deps (Some master) files), parents) end;
+
+fun file_current (_, None) = false
+ | file_current (path, info) = info = ThyLoad.check_file path;
+
+fun current_deps ml strict name =
+ (case lookup_deps name of
+ None => (false, load_deps name ml)
+ | Some deps =>
+ let val same_deps = (None, thy_graph Graph.imm_preds name) in
+ (case deps of
+ None => (true, same_deps)
+ | Some {present, outdated, master, files} =>
+ if present andalso not strict then (true, same_deps)
+ else
+ let val master' = Some (ThyLoad.check_thy name) in
+ if master <> master' then (false, load_deps name ml)
+ else (not outdated andalso forall file_current files, same_deps)
+ end)
+ end);
+
+fun outdated name =
+ (case lookup_deps name of Some (Some {outdated, ...}) => outdated | _ => false);
+
+fun require_thy ml time strict keep_strict initiators name =
+ let
+ val require_parent =
+ require_thy ml time (strict andalso keep_strict) keep_strict (name :: initiators);
+ val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
+ error (loader_msg "The error(s) above occurred while examining theory" [name] ^ "\n" ^
+ required_by initiators);
+ val pre_outdated = outdated name;
+ in
+ seq require_parent parents;
+ if current andalso pre_outdated = outdated name then () (* FIXME ?? *)
+ else
+ ((case new_deps of
+ Some deps => change_thys (update_node name parents (deps, None))
+ | None => ()); load_thy ml time initiators name parents)
+ end;
+
+val weak_use_thy = require_thy true false false false [];
+val use_thy = require_thy true false true false [];
+val update_thy = require_thy true false true true [];
+val time_use_thy = require_thy true true true false [];
+val use_thy_only = require_thy false false true false [];
+
+
+(* begin / end theory *) (* FIXME tune *)
+
+fun begin_theory name parents =
+ let
+ val _ = seq weak_use_thy parents;
+ val theory = PureThy.begin_theory name (map get_theory parents);
+ val _ = change_thys (update_node name parents (init_deps None [], Some (theory, Symtab.empty)));
+ in theory end;
+
+fun end_theory theory =
+ let val theory' = PureThy.end_theory theory
+ in put_theory theory'; theory' end;
+
+
+(* finish entries *)
+
+(* FIXME
+fun finishs names =
+ let
+ fun err txt bads =
+ error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot mark" names ^ " as finished");
+
+ val all_preds = thy_graph Graph.all_preds names;
+ val noncurrent = filter_out is_current all_preds;
+ val unfinished = filter_out is_finished (all_preds \\ names);
+ in
+ if not (null noncurrent) then err "non-current theories" noncurrent
+ else if not (null unfinished) then err "unfinished ancestor theories" unfinished
+ else seq (fn name => change_thy name (apfst (K Finished)))
+ end;
+
+fun finish name = finishs [name];
+*)
+
+fun update_all () = (); (* FIXME fake *)
+
+fun finish_all () = (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
+
+
+(* register existing theories *)
+
+fun register_theory theory =
+ let
+ val name = PureThy.get_name theory;
+ val parents = Theory.parents_of theory;
+ val parent_names = map PureThy.get_name parents;
+
+ fun err txt bads =
+ error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot register theory" [name]);
+
+ val unfinished = filter_out is_finished parent_names;
+ fun get_variant (x, y_name) =
+ if Theory.eq_thy (x, get_theory y_name) then None
+ else Some y_name;
+ val variants = mapfilter get_variant (parents ~~ parent_names);
+
+ fun register G =
+ (Graph.new_node (name, (None, Some (theory, Symtab.empty))) G
+ handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
+ |> add_deps name parent_names;
+ in
+ if not (null unfinished) then err "unfinished parent theories" unfinished
+ else if not (null variants) then err "different versions of parent theories" variants
+ else change_thys register
+ end;
+
+
+(*final declarations of this structure*)
+val theory = get_theory;
+val names = get_names;
+
+end;
+
structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
open BasicThyInfo;