--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_read.ML Thu May 19 16:30:56 1994 +0200
@@ -0,0 +1,456 @@
+(* Title: Pure/Thy/thy_read.ML
+ ID: $Id$
+ Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson
+ Copyright 1993 TU Muenchen
+
+Reading and writing the theory definition files.
+
+For theory XXX, the input file is called XXX.thy
+ the output file is called .XXX.thy.ML
+ and it then tries to read XXX.ML
+*)
+
+datatype thy_info = ThyInfo of {name: string, path: string,
+ children: string list,
+ thy_info: string option, ml_info: string option,
+ theory: Thm.theory option};
+
+signature THY_READ =
+sig
+ datatype basetype = Thy of string
+ | File of string
+
+ val loaded_thys : thy_info list ref
+ val loadpath : string list ref
+ val delete_tmpfiles: bool ref
+
+ val use_thy : string -> unit
+ val update : unit -> unit
+ val time_use_thy : string -> unit
+ val unlink_thy : string -> unit
+ val base_on : basetype list -> string -> Thm.theory
+ val store_theory : string -> Thm.theory -> unit
+end;
+
+
+functor ThyReadFun(structure ThyParse: THY_PARSE): THY_READ =
+struct
+
+datatype basetype = Thy of string
+ | File of string;
+
+val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [],
+ thy_info = Some "", ml_info = Some "",
+ theory = Some Thm.pure_thy}];
+
+val loadpath = ref ["."]; (*default search path for theory files *)
+
+val delete_tmpfiles = ref true; (*remove temporary files after use *)
+
+(*Make name of the output ML file for a theory *)
+fun out_name thy = "." ^ thy ^ ".thy.ML";
+
+(*Read a file specified by thy_file containing theory thy *)
+fun read_thy thy thy_file =
+ let
+ open ThyParse;
+ val instream = open_in thy_file;
+ val outstream = open_out (out_name thy);
+ in
+ output (outstream, parse_thy pure_syntax (input (instream, 999999)));
+ close_out outstream;
+ close_in instream
+ end;
+
+fun file_exists file =
+ let val instream = open_in file in close_in instream; true end
+ handle Io _ => false;
+
+(*Get thy_info for a loaded theory *)
+fun get_thyinfo thy =
+ let fun do_search (t :: loaded : thy_info list) =
+ let val ThyInfo {name, ...} = t
+ in if name = thy then Some t else do_search loaded end
+ | do_search [] = None
+ in do_search (!loaded_thys) end;
+
+(*Replace an item by the result of make_change *)
+fun change_thyinfo make_change =
+ let fun search (t :: loaded) =
+ let val ThyInfo {name, path, children, thy_info, ml_info,
+ theory} = t
+ val (new_t, continue) = make_change name path children thy_info
+ ml_info theory
+ in if continue then
+ new_t :: (search loaded)
+ else
+ new_t :: loaded
+ end
+ | search [] = []
+ in loaded_thys := search (!loaded_thys) end;
+
+(*Check if a theory was already loaded *)
+fun already_loaded thy =
+ let val t = get_thyinfo thy
+ in if is_none t then false
+ else let val ThyInfo {thy_info, ml_info, ...} = the t
+ in if is_none thy_info orelse is_none ml_info then false
+ else true 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 =
+ let val t = get_thyinfo thy
+ in if is_some t then
+ let val ThyInfo {thy_info, ml_info, ...} = the t
+ val tn = is_none thy_info;
+ val mn = is_none ml_info
+ in if not tn andalso not mn then
+ ((file_info thy_file = the thy_info),
+ (file_info ml_file = the ml_info))
+ else if not tn andalso mn then (true, false)
+ else (false, false)
+ end
+ else (false, false)
+ end;
+
+exception FILE_NOT_FOUND; (*raised by find_file *)
+
+(*Find a file using a list of paths if no absolute or relative path is
+ specified.*)
+fun find_file "" name =
+ let fun find_it (curr :: paths) =
+ if file_exists (tack_on curr name) then
+ tack_on curr name
+ else
+ find_it paths
+ | find_it [] = ""
+ in find_it (!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_filenames path name =
+ let fun make_absolute file =
+ if file = "" then "" else
+ if hd (explode file) = "/" then file else tack_on (pwd ()) file;
+
+ fun new_filename () =
+ let val found = find_file path (name ^ ".thy")
+ handle FILE_NOT_FOUND => "";
+ val thy_file = make_absolute found;
+ val (thy_path, _) = split_filename thy_file;
+ val found = find_file path (name ^ ".ML");
+ val ml_file = if thy_file = "" then make_absolute 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 (!loadpath) else [path]
+ in if thy_file = "" andalso ml_file = "" then
+ error ("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 thy = get_thyinfo name
+ in if is_some thy andalso path = "" then
+ let val ThyInfo {path = abs_path, ...} = the thy;
+ 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
+ (writeln ("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;
+
+(*Remove theory from all child lists in loaded_thys *)
+fun unlink_thy thy =
+ let fun remove name path children thy_info ml_info theory =
+ (ThyInfo {name = name, path = path, children = children \ thy,
+ thy_info = thy_info, ml_info = ml_info,
+ theory = theory}, true)
+ in change_thyinfo remove end;
+
+(*Remove a theory from loaded_thys *)
+fun remove_thy thy =
+ let fun remove (t :: ts) =
+ let val ThyInfo {name, ...} = t
+ in if name = thy then ts
+ else t :: (remove ts)
+ end
+ | remove [] = []
+ in loaded_thys := remove (!loaded_thys) end;
+
+(*Change thy_info and ml_info for an existent item *)
+fun set_info thy_new ml_new thy =
+ let fun change name path children thy_info ml_info theory =
+ if name = thy then
+ (ThyInfo {name = name, path = path, children = children,
+ thy_info = Some thy_new, ml_info = Some ml_new,
+ theory = theory}, false)
+ else
+ (ThyInfo {name = name, path = path, children = children,
+ thy_info = thy_info, ml_info = ml_info,
+ theory = theory}, true)
+ in change_thyinfo change end;
+
+(*Mark theory as changed since last read if it has been completly read *)
+fun mark_outdated thy =
+ if already_loaded thy then set_info "" "" thy
+ else ();
+
+(*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.
+ If a theory changed since its last use its children are marked as changed *)
+fun use_thy name =
+ let val (path, thy_name) = split_filename name;
+ val (thy_file, ml_file) = get_filenames path thy_name;
+ val (abs_path, _) = if thy_file = "" then split_filename ml_file
+ else split_filename thy_file;
+ val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name
+ thy_file ml_file;
+
+ (*Set absolute path for loaded theory *)
+ fun set_path () =
+ let fun change name path children thy_info ml_info theory =
+ if name = thy_name then
+ (ThyInfo {name = name, path = abs_path, children = children,
+ thy_info = thy_info, ml_info = ml_info,
+ theory = theory}, false)
+ else
+ (ThyInfo {name = name, path = path, children = children,
+ thy_info = thy_info, ml_info = ml_info,
+ theory = theory}, true)
+ in change_thyinfo change end;
+
+ (*Mark all direct descendants of a theory as changed *)
+ fun mark_children thy =
+ let val ThyInfo {children, ...} = the (get_thyinfo thy)
+ val loaded = filter already_loaded children
+ in if loaded <> [] then
+ (writeln ("The following children of theory " ^ (quote thy)
+ ^ " are now out-of-date: "
+ ^ (quote (space_implode "\",\"" loaded)));
+ seq mark_outdated loaded
+ )
+ else ()
+ end
+
+ in if thy_uptodate andalso ml_uptodate then ()
+ else
+ (
+ if thy_uptodate orelse thy_file = "" then ()
+ else (writeln ("Reading \"" ^ name ^ ".thy\"");
+ read_thy thy_name thy_file;
+ use (out_name thy_name)
+ );
+
+ if ml_file = "" then ()
+ else (writeln ("Reading \"" ^ name ^ ".ML\"");
+ use ml_file);
+
+ use_string ("store_theory " ^ quote thy_name ^ " "
+ ^ thy_name ^ ".thy");
+
+ (*Now set the correct info*)
+ set_info (file_info thy_file) (file_info ml_file) thy_name;
+ set_path ();
+
+ (*Mark theories that have to be reloaded*)
+ mark_children thy_name;
+
+ (*Remove temporary files*)
+ if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate
+ then ()
+ else delete_file (out_name thy_name)
+ )
+ end;
+
+fun time_use_thy tname = timeit(fn()=>
+ (writeln("\n**** Starting Theory " ^ tname ^ " ****");
+ use_thy tname;
+ writeln("\n**** Finished Theory " ^ tname ^ " ****"))
+ );
+
+(*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 *)
+ fun load_order [] result = result
+ | load_order thys result =
+ let fun next_level (t :: ts) =
+ let val thy = get_thyinfo t
+ in if is_some thy then
+ let val ThyInfo {children, ...} = the thy
+ in children union (next_level ts)
+ end
+ else next_level ts
+ end
+ | next_level [] = [];
+
+ val children = next_level thys
+ in load_order children ((result \\ children) @ children) end;
+
+ fun reload_changed (t :: ts) =
+ let val thy = get_thyinfo t;
+
+ fun abspath () =
+ if is_some thy then
+ let val ThyInfo {path, ...} = the thy in path end
+ else "";
+
+ 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 ()
+ else use_thy t;
+ reload_changed ts
+ end
+ | reload_changed [] = ();
+
+ (*Remove all theories that are no descendants of Pure.
+ If there are still children in the deleted theory's list
+ schedule them for reloading *)
+ fun collect_garbage not_garbage =
+ let fun collect (t :: ts) =
+ let val ThyInfo {name, children, ...} = t
+ in if name mem not_garbage then collect ts
+ else (writeln("Theory \"" ^ name
+ ^ "\" is no longer linked with Pure - removing it.");
+ remove_thy name;
+ seq mark_outdated children
+ )
+ end
+ | collect [] = ()
+
+ in collect (!loaded_thys) end
+
+ in collect_garbage ("Pure" :: (load_order ["Pure"] []));
+ reload_changed (load_order ["Pure"] [])
+ end;
+
+(*Merge theories to build a base for a new theory.
+ Base members are only loaded if they are missing. *)
+fun base_on bases child =
+ let (*List all descendants of a theory list *)
+ fun list_descendants (t :: ts) =
+ let val tinfo = get_thyinfo t
+ in if is_some tinfo then
+ let val ThyInfo {children, ...} = the tinfo
+ in children union (list_descendants (ts union children))
+ end
+ else []
+ end
+ | list_descendants [] = [];
+
+ (*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 ThyInfo {children, ...} = the tinfo
+ in seq (find_it ("->" ^ curr ^ result)) children
+ end
+ else ()
+ end
+ in find_it "" child end;
+
+ (*Check if a cycle will be created by add_child *)
+ fun find_cycle base =
+ if base mem (list_descendants [child]) then show_cycle base
+ else ();
+
+ (*Add child to child list of base *)
+ fun add_child base =
+ let fun add (t :: loaded) =
+ let val ThyInfo {name, path, children,
+ thy_info, ml_info, theory} = t
+ in if name = base then
+ ThyInfo {name = name, path = path,
+ children = child ins children,
+ thy_info = thy_info, ml_info = ml_info,
+ theory = theory} :: loaded
+ else
+ t :: (add loaded)
+ end
+ | add [] =
+ [ThyInfo {name = base, path = "", children = [child],
+ thy_info = None, ml_info = None, theory = None}]
+ in loaded_thys := add (!loaded_thys) end;
+
+ (*Load a base theory if not already done
+ and no cycle would be created *)
+ fun load base =
+ let val thy_present = 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_present then ()
+ else (writeln ("Autoloading theory " ^ (quote base)
+ ^ " (used by " ^ (quote child) ^ ")");
+ use_thy 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 merge_theories' parameter *)
+ | load_base [] = [];
+
+ (*Get theory object for a loaded theory *)
+ fun get_theory name =
+ let val ThyInfo {theory, ...} = the (get_thyinfo name)
+ in the theory end;
+
+ val mergelist = (unlink_thy child;
+ load_base bases);
+ val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist
+ (*we have to return something *)
+ in writeln ("Loading theory " ^ (quote child));
+ foldl Thm.merge_theories (get_theory t, map get_theory ts) end;
+
+(*Change theory object for an existent item of loaded_thys
+ or create a new item *)
+fun store_theory thy_name thy =
+ let fun make_change (t :: loaded) =
+ let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t
+ in if name = thy_name then
+ ThyInfo {name = name, path = path, children = children,
+ thy_info = thy_info, ml_info = ml_info,
+ theory = Some thy} :: loaded
+ else
+ t :: (make_change loaded)
+ end
+ | make_change [] =
+ [ThyInfo {name = thy_name, path = "", children = [],
+ thy_info = Some "", ml_info = Some "",
+ theory = Some thy}]
+ in loaded_thys := make_change (!loaded_thys) end;
+
+end;
+