--- a/src/Pure/Thy/thy_read.ML Wed Feb 03 17:20:35 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,478 +0,0 @@
-(* Title: Pure/Thy/thy_read.ML
- ID: $Id$
- Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
- Tobias Nipkow and L C Paulson
- Copyright 1994 TU Muenchen
-
-Functions for reading theory files.
-*)
-
-signature THY_READ =
-sig
- datatype basetype = Thy of string
- | File of string
-
- val loadpath : string list ref
- val delete_tmpfiles: bool ref
-
- val use_thy : string -> unit
- val time_use_thy : string -> unit
- val use_dir : string -> unit
- val exit_use_dir : string -> unit
- val update : unit -> unit
- val unlink_thy : string -> unit
- val mk_base : basetype list -> string -> theory
-
- (* Additions for Proof General by David Aspinall <da@dcs.ed.ac.uk> *)
- val use_thy_no_topml : string -> unit
- val get_thy_filenames : string -> string -> string * string
- val update_verbose : bool ref
-end;
-
-
-structure ThyRead: THY_READ =
-struct
-
-open ThmDatabase ThyInfo BrowserInfo;
-
-
-datatype basetype = Thy of string
- | File of string;
-
-
-(*Default search path for theory files*)
-val loadpath = ref ["."];
-
-
-(*Directory given as parameter to use_thy. This is temporarily added to
- loadpath while the theory's ancestors are loaded.*)
-val tmp_loadpath = ref [] : string list ref;
-
-
-(*Remove temporary files after use*)
-val delete_tmpfiles = ref true;
-
-
-(*Make name of the TextIO.output ML file for a theory *)
-fun out_name tname = File.tmp_name (tname ^ "_thy.ML");
-
-
-(*Read a file specified by thy_file containing theory tname*)
-fun read_thy tname thy_file =
- let
- val intext = File.read thy_file;
- val outext = ThySyn.parse tname intext;
- in
- File.write (out_name tname) outext
- end;
-
-
-(*Check if a theory was completly loaded *)
-fun already_loaded thy =
- let val t = get_thyinfo thy
- in if is_none t then false
- else let val {thy_time, ml_time, ...} = the t
- in is_some thy_time andalso is_some ml_time end
- end;
-
-
-(*Check if a theory file has changed since its last use.
- Return a pair of boolean values for .thy and for .ML *)
-fun thy_unchanged thy thy_file ml_file =
- case get_thyinfo thy of
- Some {thy_time, ml_time, ...} =>
- let val tn = is_none thy_time;
- val mn = is_none ml_time
- in if not tn andalso not mn then
- ((file_info thy_file = the thy_time),
- (file_info ml_file = the ml_time))
- else if not tn andalso mn then
- (file_info thy_file = the thy_time, false)
- else
- (false, false)
- end
- | None => (false, false)
-
-
-(*Get all descendants of a theory list *)
-fun get_descendants [] = []
- | get_descendants (t :: ts) =
- let val children = children_of t
- in children union (get_descendants (children union ts)) end;
-
-
-(*Find a file using a list of paths if no absolute or relative path is
- specified.*)
-fun find_file "" name =
- let fun find_it (cur :: paths) =
- if File.exists (tack_on cur name) then
- (if cur = "." then name else tack_on cur name)
- else
- find_it paths
- | find_it [] = ""
- in find_it (!tmp_loadpath @ !loadpath) end
- | find_file path name =
- if File.exists (tack_on path name) then tack_on path name
- else "";
-
-
-(*Get absolute pathnames for a new or already loaded theory *)
-fun get_filenames1 give_error_if_none_found path name =
- let fun new_filename () =
- let val found = find_file path (name ^ ".thy");
- val absolute_path = absolute_path (OS.FileSys.getDir ());
- val thy_file = absolute_path found;
- val (thy_path, _) = split_filename thy_file;
- val found = find_file path (name ^ ".ML");
- val ml_file = if thy_file = "" then absolute_path found
- else if File.exists (tack_on thy_path (name ^ ".ML"))
- then tack_on thy_path (name ^ ".ML")
- else "";
- val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath)
- else [path]
- in if thy_file = "" andalso ml_file = "" then
- (if give_error_if_none_found then error else warning)
- ("Could not find file \"" ^ name ^ ".thy\" or \""
- ^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n"
- ^ "in the following directories: \"" ^
- (space_implode "\", \"" searched_dirs) ^ "\"")
- else ();
- (thy_file, ml_file)
- end;
-
- val tinfo = get_thyinfo name;
- in if is_some tinfo andalso path = "" then
- let val {path = abs_path, ...} = the tinfo;
- val (thy_file, ml_file) = if abs_path = "" then new_filename ()
- else (find_file abs_path (name ^ ".thy"),
- find_file abs_path (name ^ ".ML"))
- in if thy_file = "" andalso ml_file = "" then
- (warning ("File \"" ^ (tack_on path name)
- ^ ".thy\"\ncontaining theory \"" ^ name
- ^ "\" no longer exists.");
- new_filename ()
- )
- else (thy_file, ml_file)
- end
- else new_filename ()
- end;
-
-val get_filenames = get_filenames1 true;
-
-val get_thy_filenames = get_filenames1 false;
-
-
-(*Remove theory from all child lists in loaded_thys *)
-fun unlink_thy tname =
- let fun remove ({path, children, parents, thy_time, ml_time, theory}) =
- {path = path, children = children \ tname, parents = parents,
- thy_time = thy_time, ml_time = ml_time, theory = theory}
- in loaded_thys := Symtab.map remove (!loaded_thys) end;
-
-
-(*Remove a theory from loaded_thys *)
-fun remove_thy tname =
- loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
- (Symtab.dest (!loaded_thys)));
-
-
-(*Change thy_time and ml_time for an existent item *)
-fun set_info tname thy_time ml_time =
- let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
- Some ({path, children, parents, theory, thy_time = _, ml_time = _}) =>
- {path = path, children = children, parents = parents,
- thy_time = thy_time, ml_time = ml_time, theory = theory}
- | None => error ("set_info: theory " ^ tname ^ " not found");
- in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
-
-
-(*Mark theory as changed since last read if it has been completly read *)
-fun mark_outdated tname =
- let val t = get_thyinfo tname;
- in if is_none t then ()
- else
- let val {thy_time, ml_time, ...} = the t
- in set_info tname (if is_none thy_time then None else Some "")
- (if is_none ml_time then None else Some "")
- end
- end;
-
-
-(*Read .thy and .ML files that haven't been read yet or have changed since
- they were last read;
- loaded_thys is a thy_info list ref containing all theories that have
- completly been read by this and preceeding use_thy calls.
- tmp_loadpath is temporarily added to loadpath while the ancestors of a
- theory that the user specified as e.g. "ex/Nat" are loaded. Because of
- raised exceptions we cannot guarantee that it's value is always valid.
- Therefore this has to be assured by the first parameter of use_thy1 which
- is "true" if use_thy gets invoked by mk_base and "false" else.
- no_mlfile is a flag which indicates that the ml file for this theory
- should not be read, used to implement use_thy_no_topml.
-*)
-fun use_thy1 no_mlfile tmp_loadpath_valid name =
- let
- val (path, tname) = split_filename name;
- val dummy = (tmp_loadpath :=
- (if not tmp_loadpath_valid then (if path = "" then [] else [path])
- else !tmp_loadpath));
- val (thy_file, ml_file) = get_filenames path tname;
- val (abs_path, _) = if thy_file = "" then split_filename ml_file
- else split_filename thy_file;
- val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
- val old_parents = parents_of_name tname;
-
- (*Set absolute path for loaded theory *)
- fun set_path () =
- let val {path = _, children, parents, thy_time, ml_time, theory} =
- the (Symtab.lookup (!loaded_thys, tname));
- in loaded_thys := Symtab.update ((tname,
- {path = abs_path,
- children = children, parents = parents,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory}),
- !loaded_thys)
- end
-
- (*Mark all direct descendants of a theory as changed *)
- fun mark_children thy =
- let val children = children_of thy;
- val present = filter (is_some o get_thyinfo) children;
- val loaded = filter already_loaded present;
- in if loaded <> [] then
- writeln ("The following children of theory " ^ (quote thy)
- ^ " are now out-of-date: "
- ^ (quote (space_implode "\",\"" loaded)))
- else ();
- seq mark_outdated present
- end
-
- (*Make sure that loaded_thys contains an entry for tname*)
- fun init_thyinfo () =
- let val tinfo = {path = "", children = [], parents = [],
- thy_time = None, ml_time = None,
- theory = None};
- in if is_some (get_thyinfo tname) then ()
- else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
- end
- fun read_thy_file() =
- if thy_file = "" then ()
- else
- (writeln ("Reading \"" ^ name ^ ".thy\"");
- init_thyinfo ();
- read_thy tname thy_file;
- Use.use (out_name tname);
- if not (!delete_tmpfiles) then ()
- else OS.FileSys.remove (out_name tname);
- thyfile2html tname abs_path)
-
- (*Add theory to list of all loaded theories (for index.html)
- and it to its parents' sub-charts*)
- fun add_theory path =
- if path = "" then (*first time theory has been read*)
- (mk_html tname abs_path old_parents;
- mk_graph tname abs_path) (*Add it to graph definition file*)
- else ()
- in if thy_uptodate andalso ml_uptodate then ()
- else
- (read_thy_file();
- set_info tname (Some (file_info thy_file)) None;
- (*mark thy_file as successfully loaded*)
-
- if (no_mlfile orelse ml_file = "") then ()
- else (writeln ("Reading \"" ^ name ^ ".ML\"");
- Use.use ml_file);
-
- (*Store theory again because it could have been redefined*)
- use_text false ("val _ = store_theory " ^ tname ^ ".thy;");
-
- add_theory (path_of tname);
-
- (*Now set the correct info*)
- set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
- set_path ();
- mark_children tname; (*Mark theories that have to be reloaded*)
- close_html () )
- end;
-
-
-val use_thy = use_thy1 false false;
-val use_thy_no_topml = use_thy1 true false;
-
-
-fun time_use_thy tname = timeit(fn()=>
- (writeln("\n**** Starting Theory " ^ tname ^ " ****");
- setmp Goals.proof_timing true use_thy tname;
- writeln("\n**** Finished Theory " ^ tname ^ " ****"))
- );
-
-
-val update_verbose = ref false;
-
-(*Load all thy or ML files that have been changed and also
- all theories that depend on them.*)
-fun update () =
- let (*List theories in the order they have to be loaded in.*)
- fun load_order [] result = result
- | load_order thys result =
- let fun next_level [] = []
- | next_level (t :: ts) =
- let val children = children_of t
- in children union (next_level ts) end;
-
- val descendants = next_level thys;
- in load_order descendants ((result \\ descendants) @ descendants)
- end;
-
- fun reload_changed (t :: ts) =
- let val abspath = case get_thyinfo t of
- Some ({path, ...}) => path
- | None => "";
-
- val (thy_file, ml_file) = get_filenames abspath t;
- val (thy_uptodate, ml_uptodate) =
- thy_unchanged t thy_file ml_file;
- in if thy_uptodate andalso ml_uptodate then
- (if !update_verbose then
- (writeln
- ("Not reading \"" ^ thy_file ^
- "\" (unchanged)" ^
- (if ml_file <> ""
- then "\nNot reading \"" ^ ml_file ^
- "\" (unchanged)"
- else "")))
- else ())
- else use_thy t;
- reload_changed ts
- end
- | reload_changed [] = ();
-
- (*Remove all theories that are no descendants of ProtoPure.
- If there are still children in the deleted theory's list
- schedule them for reloading *)
- fun collect_garbage no_garbage =
- let fun collect ((tname, {children, ...}: thy_info) :: ts) =
- if tname mem no_garbage then collect ts
- else (writeln ("Theory \"" ^ tname ^
- "\" is no longer linked with ProtoPure - removing it.");
- remove_thy tname;
- seq mark_outdated children)
- | collect [] = ()
- in collect (Symtab.dest (!loaded_thys)) end;
- in tmp_loadpath := [];
- collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
- reload_changed (load_order ["Pure", "CPure"] [])
- end;
-
-
-(*Merge theories to build a base for a new theory.
- Base members are only loaded if they are missing.*)
-fun mk_base bases child =
- let (*Show the cycle that would be created by add_child*)
- fun show_cycle base =
- let fun find_it result curr =
- let val tinfo = get_thyinfo curr
- in if base = curr then
- error ("Cyclic dependency of theories: "
- ^ child ^ "->" ^ base ^ result)
- else if is_some tinfo then
- let val {children, ...} = the tinfo
- in seq (find_it ("->" ^ curr ^ result)) children
- end
- else ()
- end
- in find_it "" child end;
-
- (*Check if a cycle would be created by add_child*)
- fun find_cycle base =
- if base mem (get_descendants [child]) then show_cycle base
- else ();
-
- (*Add child to child list of base*)
- fun add_child base =
- let val tinfo =
- case Symtab.lookup (!loaded_thys, base) of
- Some ({path, children, parents, thy_time, ml_time,
- theory}) =>
- {path = path,
- children = child ins children, parents = parents,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory}
- | None => {path = "", children = [child], parents = [],
- thy_time = None, ml_time = None,
- theory = None};
- in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
-
- (*Load a base theory if not already done
- and no cycle would be created *)
- fun load base =
- let val thy_loaded = already_loaded base
- (*test this before child is added *)
- in
- if child = base then
- error ("Cyclic dependency of theories: " ^ child
- ^ "->" ^ child)
- else
- (find_cycle base;
- add_child base;
- if thy_loaded then ()
- else (writeln ("Autoloading theory " ^ quote base
- ^ " (required by " ^ quote child ^ ")");
- (* autoloaded theories always use .ML files too *)
- use_thy1 false true base)
- )
- end;
-
- (*Load all needed files and make a list of all real theories *)
- fun load_base (Thy b :: bs) =
- (load b;
- b :: load_base bs)
- | load_base (File b :: bs) =
- (load b;
- load_base bs) (*don't add it to mergelist *)
- | load_base [] = [];
-
- val dummy = unlink_thy child;
- val mergelist = load_base bases;
-
- val base_thy =
- (writeln ("Loading theory " ^ quote child);
- if null mergelist then ProtoPure.thy
- else Theory.prep_ext_merge (map ThyInfo.theory mergelist));
-
- val dummy =
- let val tinfo = case Symtab.lookup (!loaded_thys, child) of
- Some ({path, children, parents = _, thy_time, ml_time, theory}) =>
- {path = path, children = children, parents = mergelist,
- thy_time = thy_time, ml_time = ml_time, theory = theory}
- | None => sys_error ("set_parents: theory " ^ child ^ " not found");
- in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end;
-
- in
- cur_thyname := child;
- base_thy
- end;
-
-
-(*Temporarily enter a directory and load its ROOT.ML file;
- also do some work for HTML and graph generation*)
-local
-
- fun gen_use_dir use_cmd dirname =
- let val old_dir = OS.FileSys.getDir ();
- in OS.FileSys.chDir dirname;
- if !make_html then init_html() else ();
- if !make_graph then init_graph dirname else ();
- use_cmd "ROOT.ML";
- finish_html();
- OS.FileSys.chDir old_dir
- end;
-
-in
-
- val use_dir = gen_use_dir Use.use;
- val exit_use_dir = gen_use_dir Use.exit_use;
-
-end
-
-end;