--- a/src/Pure/Thy/thy_read.ML Fri Jul 15 12:24:05 1994 +0200
+++ b/src/Pure/Thy/thy_read.ML Fri Jul 15 13:30:42 1994 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/Thy/thy_read.ML
ID: $Id$
Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson / Carsten Clasohm
- Copyright 1993 TU Muenchen
+ Copyright 1994 TU Muenchen
Reading and writing the theory definition files.
@@ -10,17 +10,19 @@
and it then tries to read XXX.ML
*)
-datatype thy_info = ThyInfo of {name: string, path: string,
+datatype thy_info = ThyInfo of {path: string,
children: string list,
- thy_info: string option, ml_info: string option,
- theory: Thm.theory option};
+ thy_time: string option,
+ ml_time: string option,
+ theory: Thm.theory option,
+ thms: thm Symtab.table};
signature READTHY =
sig
datatype basetype = Thy of string
| File of string
- val loaded_thys : thy_info list ref
+ val loaded_thys : thy_info Symtab.table ref
val loadpath : string list ref
val delete_tmpfiles: bool ref
@@ -28,35 +30,42 @@
val update : unit -> unit
val time_use_thy : string -> unit
val unlink_thy : string -> unit
- val base_on : basetype list -> string -> bool -> Thm.theory
- val store_theory : string -> Thm.theory -> unit
+ val base_on : basetype list -> string -> bool -> theory
+ val store_theory : theory * string -> unit
+
+ val store_thm : thm * string -> thm
+ val qed : string -> unit
+ val get_thm : theory -> string -> thm
+ val get_thms : theory -> (string * thm) list
end;
functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
struct
+open Symtab;
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 loaded_thys = ref (make [("Pure", ThyInfo {path = "", children = [],
+ thy_time = Some "", ml_time = Some "",
+ theory = Some pure_thy,
+ thms = null})]);
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";
+fun out_name tname = "." ^ tname ^ ".thy.ML";
(*Read a file specified by thy_file containing theory thy *)
-fun read_thy thy thy_file =
+fun read_thy tname thy_file =
let
val instream = open_in thy_file;
- val outstream = open_out (out_name thy);
+ val outstream = open_out (out_name tname);
in
- output (outstream, ThySyn.parse (input (instream, 999999)));
+ output (outstream, ThySyn.parse tname (input (instream, 999999)));
close_out outstream;
close_in instream
end;
@@ -66,35 +75,16 @@
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;
+fun get_thyinfo tname = lookup (!loaded_thys, tname);
(*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
+ else let val ThyInfo {thy_time, ml_time, ...} = the t
+ in if is_none thy_time orelse is_none ml_time then false
+ else true
+ end
end;
(*Check if a theory file has changed since its last use.
@@ -102,12 +92,12 @@
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
+ let val ThyInfo {thy_time, ml_time, ...} = the t
+ 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_info),
- (file_info ml_file = the ml_info))
+ ((file_info thy_file = the thy_time),
+ (file_info ml_file = the ml_time))
else if not tn andalso mn then (true, false)
else (false, false)
end
@@ -156,9 +146,9 @@
(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 tinfo = get_thyinfo name;
+ in if is_some tinfo andalso path = "" then
+ let val ThyInfo {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"))
@@ -174,40 +164,31 @@
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;
+fun unlink_thy tname =
+ let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms}) =
+ ThyInfo {path = path, children = children \ tname,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms}
+ in loaded_thys := mapst remove (!loaded_thys) 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;
+fun remove_thy tname =
+ loaded_thys := make (filter_out (fn (id, _) => id = tname)
+ (alist_of (!loaded_thys)));
-(*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;
+(*Change thy_time and ml_time for an existent item *)
+fun set_info thy_time ml_time tname =
+ let val ThyInfo {path, children, theory, thms, ...} =
+ the (lookup (!loaded_thys, tname));
+ in loaded_thys := update ((tname,
+ ThyInfo {path = path, children = children,
+ thy_time = Some thy_time, ml_time = Some ml_time,
+ theory = theory, thms = thms}), !loaded_thys)
+ 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 ();
+fun mark_outdated tname =
+ if already_loaded tname then set_info "" "" tname else ();
(*Read .thy and .ML files that haven't been read yet or have changed since
they were last read;
@@ -215,25 +196,23 @@
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;
+ let val (path, tname) = split_filename name;
+ 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 thy_name
+ val (thy_uptodate, ml_uptodate) = thy_unchanged tname
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;
+ let val ThyInfo {children, thy_time, ml_time, theory, thms, ...} =
+ the (lookup (!loaded_thys, tname));
+ in loaded_thys := update ((tname,
+ ThyInfo {path = abs_path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms}),
+ !loaded_thys)
+ end;
(*Mark all direct descendants of a theory as changed *)
fun mark_children thy =
@@ -246,35 +225,47 @@
seq mark_outdated loaded
)
else ()
- end
+ end;
+ (*Remove all theorems associated with a theory*)
+ fun delete_thms () =
+ let val tinfo = case lookup (!loaded_thys, tname) of
+ Some (ThyInfo {path, children, thy_time, ml_time, theory, ...}) =>
+ ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = null}
+ | None => ThyInfo {path = "", children = [],
+ thy_time = None, ml_time = None,
+ theory = None, thms = null};
+ in loaded_thys := update ((tname, tinfo), !loaded_thys) end;
in if thy_uptodate andalso ml_uptodate then ()
else
(
+ delete_thms ();
+
if thy_uptodate orelse thy_file = "" then ()
else (writeln ("Reading \"" ^ name ^ ".thy\"");
- read_thy thy_name thy_file;
- use (out_name thy_name)
+ read_thy tname thy_file;
+ use (out_name tname)
);
if ml_file = "" then ()
else (writeln ("Reading \"" ^ name ^ ".ML\"");
use ml_file);
- use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name
- ^ ".thy;"];
+ use_string ["store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
(*Now set the correct info*)
- set_info (file_info thy_file) (file_info ml_file) thy_name;
+ set_info (file_info thy_file) (file_info ml_file) tname;
set_path ();
(*Mark theories that have to be reloaded*)
- mark_children thy_name;
+ mark_children tname;
(*Remove temporary files*)
if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate
then ()
- else delete_file (out_name thy_name)
+ else delete_file (out_name tname)
)
end;
@@ -294,13 +285,12 @@
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
+ in children union (next_level ts) end
else next_level ts
end
| next_level [] = [];
- val children = next_level thys
+ val children = next_level thys;
in load_order children ((result \\ children) @ children) end;
fun reload_changed (t :: ts) =
@@ -324,19 +314,15 @@
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
+ let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
+ if tname mem not_garbage then collect ts
+ else (writeln ("Theory \"" ^ tname
+ ^ "\" is no longer linked with Pure - removing it.");
+ remove_thy tname;
+ seq mark_outdated children)
| collect [] = ()
- in collect (!loaded_thys) end
-
+ in collect (alist_of (!loaded_thys)) end;
in collect_garbage ("Pure" :: (load_order ["Pure"] []));
reload_changed (load_order ["Pure"] [])
end;
@@ -370,28 +356,24 @@
end
in find_it "" child end;
- (*Check if a cycle will be created by add_child *)
+ (*Check if a cycle would 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;
+ let val tinfo =
+ case lookup (!loaded_thys, base) of
+ Some (ThyInfo {path, children, thy_time, ml_time,
+ theory, thms}) =>
+ ThyInfo {path = path, children = child ins children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory, thms = thms}
+ | None => ThyInfo {path = "", children = [child],
+ thy_time = None, ml_time = None,
+ theory = None, thms = null};
+ in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
(*Load a base theory if not already done
and no cycle would be created *)
@@ -433,21 +415,60 @@
(*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;
+fun store_theory (thy, tname) =
+ let val tinfo = case lookup (!loaded_thys, tname) of
+ Some (ThyInfo {path, children, thy_time, ml_time, thms, ...}) =>
+ ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = Some thy, thms = thms}
+ | None => ThyInfo {path = "", children = [],
+ thy_time = Some "", ml_time = Some "",
+ theory = Some thy, thms = null};
+ in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
+
+(*Store a theorem in the ThyInfo of the theory it is associated with*)
+fun store_thm (thm, tname) =
+ let val thy_name = !(hd (stamps_of_thm thm));
+
+ val ThyInfo {path, children, thy_time, ml_time, theory, thms} =
+ case get_thyinfo thy_name of
+ Some tinfo => tinfo
+ | None => error ("store_thm: Theory \"" ^ thy_name
+ ^ "\" is not stored in loaded_thys");
+ in loaded_thys :=
+ Symtab.update ((thy_name, ThyInfo {path = path, children = children,
+ thy_time = thy_time, ml_time = ml_time,
+ theory = theory,
+ thms = Symtab.update ((tname, thm), thms)}),
+ !loaded_thys);
+ thm
+ end;
+(*Store theorem in loaded_thys and a ML variable*)
+fun qed name = use_string ["val " ^ name ^ " = store_thm (result(), "
+ ^ quote name ^ ");"];
+
+fun name_of_thy thy = !(hd (stamps_of_thy thy));
+
+(*Retrieve a theorem specified by theory and name*)
+fun get_thm thy tname =
+ let val thy_name = name_of_thy thy;
+
+ val ThyInfo {thms, ...} =
+ case get_thyinfo thy_name of
+ Some tinfo => tinfo
+ | None => error ("get_thm: Theory \"" ^ thy_name
+ ^ "\" is not stored in loaded_thys");
+ in the (lookup (thms, tname)) end;
+
+(*Retrieve all theorems belonging to the specified theory*)
+fun get_thms thy =
+ let val thy_name = name_of_thy thy;
+
+ val ThyInfo {thms, ...} =
+ case get_thyinfo thy_name of
+ Some tinfo => tinfo
+ | None => error ("get_thms: Theory \"" ^ thy_name
+ ^ "\" is not stored in loaded_thys");
+ in alist_of thms end;
end;
-