--- a/src/Pure/Thy/read.ML Tue Nov 16 14:13:11 1993 +0100
+++ b/src/Pure/Thy/read.ML Tue Nov 16 14:23:19 1993 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Thy/read
ID: $Id$
Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson
- Copyright 1992 TU Muenchen
+ Copyright 1993 TU Muenchen
Reading and writing the theory definition files.
@@ -10,39 +10,43 @@
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 READTHY =
sig
- type thy_info
- datatype BaseType = Thy of string
+ datatype basetype = Thy of string
| File of string
+ 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 base_on : BaseType list -> string -> Thm.theory
+ val unlink_thy : string -> unit
+ val base_on : basetype list -> string -> Thm.theory
val store_theory : string -> Thm.theory -> unit
val list_loaded : unit -> thy_info list
val set_loaded : thy_info list -> unit
- val set_loadpath : string list -> unit
- val relations : string -> unit
end;
functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY =
struct
-datatype thy_info = ThyInfo of {name: string, children: string list,
- thy_info: string, ml_info: string,
- theory: Thm.theory};
-
-datatype BaseType = Thy of string
+datatype basetype = Thy of string
| File of string;
-val loaded_thys = ref [ThyInfo {name = "pure", children = [], thy_info = "",
- ml_info = "", theory = Thm.pure_thy}];
+val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [],
+ thy_info = Some "", ml_info = Some "",
+ theory = Some Thm.pure_thy}];
-val loadpath = ref ["."];
+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";
@@ -60,7 +64,56 @@
let val instream = open_in file in close_in instream; true end
handle Io _ => false;
-exception FILE_NOT_FOUND; (*raised by find_file *)
+(*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.*)
@@ -70,41 +123,85 @@
tack_on curr name
else
find_it paths
- | find_it [] = raise FILE_NOT_FOUND
+ | find_it [] = ""
in find_it (!loadpath) end
| find_file path name =
if file_exists (tack_on path name) then tack_on path name
- else raise FILE_NOT_FOUND;
+ else "";
+
+(*Get absolute pathnames for a new or already loaded theory *)
+fun get_filenames path name =
+ let fun new_filename () =
+ let val thyl = to_lower name;
+ val found = find_file path (thyl ^ ".thy")
+ handle FILE_NOT_FOUND => "";
+ val thy_file = if found = "" then "" else tack_on (pwd ()) found;
+ val (thy_path, _) = split_filename thy_file;
+ val found = find_file path (thyl ^ ".ML");
+ val ml_file = if thy_file = ""
+ then if found = "" then "" else tack_on (pwd ()) found
+ else if file_exists (tack_on thy_path (thyl ^ ".ML"))
+ then tack_on thy_path (thyl ^ ".ML")
+ else ""
+ in if thy_file = "" andalso ml_file = "" then
+ error ("Could find no .thy or .ML file for theory " ^ name)
+ else ();
+ (thy_file, ml_file)
+ end;
-(*Check if a theory was already loaded *)
-fun already_loaded thy =
- let fun do_search ((ThyInfo {name, ...}) :: loaded) =
- if name = thy then true else do_search loaded
- | do_search [] = false
- in do_search (!loaded_thys) end;
+ val thy = get_thyinfo name
+ in if is_some thy then
+ let val thyl = to_lower name;
+ val ThyInfo {path = abs_path, ...} = the thy;
+ val (thy_file, ml_file) = if abs_path = "" then new_filename ()
+ else (find_file abs_path (thyl ^ ".thy"),
+ find_file abs_path (thyl ^ ".ML"))
+ in if thy_file = "" andalso ml_file = "" then
+ (writeln ("Warning: File \"" ^ (tack_on path thyl)
+ ^ ".thy\"\ncontaining theory \"" ^ name
+ ^ "\" no longer exists.");
+ new_filename ()
+ )
+ else (thy_file, ml_file)
+ end
+ else new_filename ()
+ end;
-(*Get thy_info for a loaded theory *)
-fun get_thyinfo thy =
- let fun do_search (t :: loaded : thy_info list) =
+(*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 t else do_search loaded end
- | do_search [] = error ("Internal error (get_thyinfo): theory "
- ^ thy ^ " not found.")
- in do_search (!loaded_thys) end;
+ in if name = thy then ts
+ else t :: (remove ts)
+ end
+ | remove [] = []
+ in loaded_thys := remove (!loaded_thys) 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 =
- if already_loaded thy then
- let val ThyInfo {thy_info, ml_info, ...} = get_thyinfo thy
- in ((file_info (thy_file) = thy_info), (file_info (ml_file) = ml_info))
- end
- else (false, false);
+(*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;
-(*Get theory object for a loaded theory *)
-fun get_theory name =
- let val ThyInfo {theory, ...} = get_thyinfo name
- in theory 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;
@@ -113,60 +210,34 @@
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 = to_lower thy_name;
- val thy_file = (find_file path (thy ^ ".thy")
- handle FILE_NOT_FOUND => "");
- val (thy_path, _) = split_filename thy_file;
- val ml_file = if thy_file = ""
- then (find_file path (thy ^ ".ML")
- handle FILE_NOT_FOUND =>
- error ("Could find no .thy or .ML file for theory "
- ^ thy_name))
- else if file_exists (thy_path ^ thy ^ ".ML")
- then thy_path ^ thy ^ ".ML"
- else ""
- val (thy_uptodate, ml_uptodate) = thy_unchanged thy thy_file ml_file;
+ val thyl = to_lower thy_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;
- (*Remove theory from all child lists in loaded_thys.
- Afterwards add_child should be called for the (new) base theories *)
- fun remove_child thy =
- let fun do_remove (ThyInfo {name, children, thy_info, ml_info, theory}
- :: loaded) result =
- do_remove loaded
- (ThyInfo {name = name, children = children \ thy,
- thy_info = thy_info, ml_info = ml_info,
- theory = theory} :: result)
- | do_remove [] result = result;
- in loaded_thys := do_remove (!loaded_thys) [] end;
-
- exception THY_NOT_FOUND; (*Raised by set_info *)
+ (*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;
- (*Change thy_info and ml_info for an existent item or create
- a new item with empty child list *)
- fun set_info thy_new ml_new thy =
- let fun make_change (t :: loaded) =
- let val ThyInfo {name, children, theory, ...} = t
- in if name = thy then
- ThyInfo {name = name, children = children,
- thy_info = thy_new, ml_info = ml_new,
- theory = theory} :: loaded
- else
- t :: (make_change loaded)
- end
- | make_change [] = raise THY_NOT_FOUND
- in loaded_thys := make_change (!loaded_thys) end;
-
- (*Mark all direct and indirect descendants of a theory as changed *)
+ (*Mark all direct descendants of a theory as changed *)
fun mark_children thy =
- let val ThyInfo {children, ...} = get_thyinfo thy
+ let val ThyInfo {children, ...} = the (get_thyinfo thy)
in if children <> [] then
(writeln ("The following children of theory " ^ (quote thy)
- ^ " are now out-of-date: \""
- ^ (space_implode "\",\"" children) ^ "\"");
- seq (set_info "" "") children
- handle THY_NOT_FOUND => ()
- (*If this theory was automatically loaded by a child
- then the child cannot be found in loaded_thys *)
+ ^ " are now out-of-date: "
+ ^ (quote (space_implode "\",\"" children)));
+ seq mark_outdated children
)
else ()
end
@@ -175,43 +246,32 @@
else
(
writeln ("Loading theory " ^ (quote name));
- if thy_uptodate orelse (thy_file = "") then ()
- else
- (
- (*Allow dependency lists to be rebuild completely *)
- remove_child thy;
-
- read_thy thy thy_file
- );
+ if thy_uptodate orelse thy_file = "" then ()
+ else (read_thy thyl thy_file;
+ use (out_name thyl)
+ );
- (*Actually read files!*)
- if thy_uptodate orelse (thy_file = "") then ()
- else use (out_name thy);
- if (thy_file = "") then (*theory object created in .ML file*)
- (
- use ml_file;
- let val outstream = open_out (".tmp.ML")
- in
- output (outstream, "store_theory " ^ quote thy_name ^ " "
- ^ thy_name ^ ".thy;\n");
- close_out outstream
- end;
- use ".tmp.ML";
- delete_file ".tmp.ML"
- )
- else if ml_file <> "" then use ml_file
- else ();
+ if ml_file = "" then () else use ml_file;
+
+ let val outstream = open_out ".tmp.ML"
+ in
+ output (outstream, "store_theory " ^ quote thy_name ^ " "
+ ^ thy_name ^ ".thy;\n");
+ close_out outstream
+ end;
+ use ".tmp.ML";
+ delete_file ".tmp.ML";
(*Now set the correct info.*)
- (set_info (file_info thy_file) (file_info ml_file) thy
- handle THY_NOT_FOUND => error ("Could not find theory \"" ^ thy
- ^ "\" (wrong filename?)"));
+ set_info (file_info thy_file) (file_info ml_file) thy_name;
+ set_path ();
(*Mark theories that have to be reloaded.*)
- mark_children thy;
+ mark_children thy_name;
- delete_file (out_name thy)
- )
+ if !delete_tmpfiles then delete_file (out_name thyl)
+ else ()
+ )
end;
fun time_use_thy tname = timeit(fn()=>
@@ -227,8 +287,12 @@
fun load_order [] result = result
| load_order thys result =
let fun next_level (t :: ts) =
- let val ThyInfo {children, ...} = get_thyinfo t
- in children union (next_level 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 []
end
| next_level [] = [];
@@ -236,123 +300,150 @@
in load_order children ((result \\ children) @ children) end;
fun reload_changed (t :: ts) =
- let val curr = get_thyinfo t;
- val thy_file = (find_file "" (t ^ ".thy")
- handle FILE_NOT_FOUND => "");
- val (thy_path, _) = split_filename thy_file;
- val ml_file = if thy_file = ""
- then (find_file "" (t ^ ".ML")
- handle FILE_NOT_FOUND =>
- error ("Could find no .thy or .ML file for theory "
- ^ t))
- else if file_exists (thy_path ^ t ^ ".ML")
- then thy_path ^ t ^ ".ML"
- else ""
+ 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;
-
+ 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 [] = ()
- in reload_changed (load_order ["pure"] []) 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 val childl = to_lower child;
-
- (*List all descendants of a theory list *)
+ let (*List all descendants of a theory list *)
fun list_descendants (t :: ts) =
- if already_loaded t then
- let val ThyInfo {children, ...} = get_thyinfo t
- in children union
- (list_descendants (ts union children))
- end
- else []
+ 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 =
- if base = curr then
- error ("Cyclic dependency of theories: "
- ^ childl ^ "->" ^ base ^ result)
- else if already_loaded curr then
- let val ThyInfo {children, ...} = get_thyinfo curr
- in seq (find_it ("->" ^ curr ^ result)) children
- end
- else ()
- in find_it "" childl end;
+ 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 [childl]) then show_cycle base
+ if base mem (list_descendants [child]) then show_cycle base
else ();
(*Add child to child list of base *)
- fun add_child (t :: loaded) base =
- let val ThyInfo {name, children, thy_info, ml_info, theory} = t
- in if name = base then
- ThyInfo {name = name,
- children = childl ins children,
- thy_info = thy_info, ml_info = ml_info,
- theory = theory} :: loaded
- else
- t :: (add_child loaded base)
- end
- | add_child [] base =
- [ThyInfo {name = base, children = [childl],
- thy_info = "", ml_info = "",
- theory = Thm.pure_thy}];
- (*Thm.pure_thy is used as a dummy *)
+ 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;
- fun do_load thy =
- let val basel = to_lower thy;
-
- val thy_present = already_loaded basel
+ (*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 childl = basel then
+ if child = base then
error ("Cyclic dependency of theories: " ^ child
^ "->" ^ child)
else
- (find_cycle thy;
- loaded_thys := add_child (!loaded_thys) basel;
+ (find_cycle base;
+ add_child base;
if thy_present then ()
- else (writeln ("Autoloading theory " ^ (quote thy)
+ else (writeln ("Autoloading theory " ^ (quote base)
^ " (used by " ^ (quote child) ^ ")");
- use_thy thy)
+ use_thy base)
)
end;
+ (*Load all needed files and make a list of all real theories *)
fun load_base (Thy b :: bs) =
- (do_load b;
- (to_lower b) :: (load_base bs))
+ (load b;
+ b :: (load_base bs))
| load_base (File b :: bs) =
- (do_load b;
- load_base bs) (*don't add it to merge_theories' parameter *)
+ (load b;
+ load_base bs) (*don't add it to merge_theories' parameter *)
| load_base [] = [];
-
- val (t :: ts) = load_base bases
+
+ (*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 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, children, thy_info, ml_info, ...} = t
- in if name = (to_lower thy_name) then
- ThyInfo {name = name, children = children,
+ 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 = thy} :: loaded
+ theory = Some thy} :: loaded
else
t :: (make_change loaded)
end
| make_change [] =
- [ThyInfo {name = (to_lower thy_name), children = [], thy_info = "",
- ml_info = "", theory = thy}]
+ [ThyInfo {name = thy_name, path = "", children = [],
+ thy_info = Some "", ml_info = Some "",
+ theory = Some thy}]
in loaded_thys := make_change (!loaded_thys) end;
(*Create a list of all theories loaded by this structure *)
@@ -360,22 +451,11 @@
(*Change the list of loaded theories *)
fun set_loaded [] =
- loaded_thys := [ThyInfo {name = "pure", children = [], thy_info = "",
- ml_info = "", theory = Thm.pure_thy}]
+ loaded_thys := [ThyInfo {name = "Pure", path = "", children = [],
+ thy_info = Some "", ml_info = Some "",
+ theory = Some Thm.pure_thy}]
| set_loaded ts =
loaded_thys := ts;
-(*Change the path list that is to be searched for .thy and .ML files *)
-fun set_loadpath new_path =
- loadpath := new_path;
+end
-(*This function is for debugging purposes only *)
-fun relations thy =
- let val ThyInfo {children, ...} = get_thyinfo thy
- in
- writeln (thy ^ ": " ^ (space_implode ", " children));
- seq relations children
- end
-
-end;
-