--- a/src/Pure/Thy/browser_info.ML Thu Oct 23 12:13:15 1997 +0200
+++ b/src/Pure/Thy/browser_info.ML Thu Oct 23 12:43:07 1997 +0200
@@ -173,7 +173,7 @@
(*Make list of all theories and all theories that own a .thy file*)
fun list_theories [] theories thy_files = (theories, thy_files)
- | list_theories ((tname, ThyInfo {thy_time, ...}) :: ts)
+ | list_theories ((tname, {thy_time, ...}: thy_info) :: ts)
theories thy_files =
list_theories ts (tname :: theories)
(if is_some thy_time andalso the thy_time <> "" then
@@ -741,7 +741,7 @@
fun mk_graph tname abs_path = if not (!make_graph) then () else
let val parents =
map (fn (t, _) => tack_on (path_of t) t)
- (filter (fn (_, ThyInfo {children,...}) => tname mem children)
+ (filter (fn (_, {children,...}) => tname mem children)
(Symtab.dest(!loaded_thys)));
val dir_name = relative_path
--- a/src/Pure/Thy/thm_database.ML Thu Oct 23 12:13:15 1997 +0200
+++ b/src/Pure/Thy/thm_database.ML Thu Oct 23 12:43:07 1997 +0200
@@ -273,7 +273,7 @@
and in the theory's HTML file*)
fun store_thm (name, thm) =
let
- val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time,
+ val (thy_name, {path, children, parents, thy_time, ml_time,
theory, thms, methods, data}) =
thyinfo_of_sign (#sign (rep_thm thm))
@@ -290,7 +290,7 @@
val thm' = Thm.name_thm (name, thm)
in
loaded_thys := Symtab.update
- ((thy_name, ThyInfo {path = path, children = children, parents = parents,
+ ((thy_name, {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms',
methods = methods, data = data}),
@@ -329,12 +329,12 @@
(*Get all theorems belonging to a given theory*)
fun thmtab_of_thy thy =
- let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
+ let val (_, {thms, ...}) = thyinfo_of_sign (sign_of thy);
in thms end;
fun thmtab_of_name name =
- let val ThyInfo {thms, ...} = the (get_thyinfo name);
+ let val {thms, ...} = the (get_thyinfo name);
in thms end;
@@ -361,15 +361,15 @@
fun delete_thms tname =
let
val tinfo = case get_thyinfo tname of
- Some (ThyInfo {path, children, parents, thy_time, ml_time, theory,
+ Some ({path, children, parents, thy_time, ml_time, theory,
methods, data, ...}) =>
- ThyInfo {path = path, children = children, parents = parents,
+ {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = Symtab.null,
methods = methods, data = data}
| None => error ("Theory " ^ tname ^ " not stored by loader");
- val ThyInfo {theory, ...} = tinfo;
+ val {theory, ...} = tinfo;
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
case theory of
Some t => delete_thm_db t
--- a/src/Pure/Thy/thy_info.ML Thu Oct 23 12:13:15 1997 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Oct 23 12:43:07 1997 +0200
@@ -1,27 +1,29 @@
(* Title: Pure/Thy/thy_info.ML
ID: $Id$
- Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
- Tobias Nipkow and L C Paulson
- Copyright 1994 TU Muenchen
+ Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
-Functions for storing and retrieving arbitrary theory information.
+Theory loader info database.
*)
-(*Types for theory storage*)
-
+(* FIXME wipe out! *)
(*Functions to handle arbitrary data added by the user; type "exn" is used
to store data*)
datatype thy_methods =
ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
-datatype thy_info =
- ThyInfo of {path: string,
- children: string list, parents: string list,
- thy_time: string option, ml_time: string option,
- theory: theory option, thms: thm Symtab.table,
- methods: thy_methods Symtab.table,
- data: exn Symtab.table * exn Symtab.table};
- (*thy_time, ml_time = None theory file has not been read yet
+
+type thy_info =
+ {path: string,
+ children: string list, parents: string list,
+ thy_time: string option, ml_time: string option,
+ theory: theory option, thms: thm Symtab.table,
+ methods: thy_methods Symtab.table,
+ data: exn Symtab.table * exn Symtab.table};
+
+(*
+ path: directory where theory's files are located
+
+ 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
@@ -44,8 +46,7 @@
if ML files has not been read, second element is identical to
first one because get_thydata, which is meant to return the
latest data, always accesses the 2nd element
- *)
-
+*)
signature THY_INFO =
sig
@@ -57,7 +58,6 @@
val theory_of_thm : thm -> theory
val children_of : string -> string list
val parents_of_name: string -> string list
- val thyname_of_sign: Sign.sg -> string
val thyinfo_of_sign: Sign.sg -> string * thy_info
val add_thydata : string -> string * thy_methods -> unit
@@ -70,111 +70,82 @@
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, thms = Symtab.null,
+ methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info);
+
+(*preloaded theories*)
val loaded_thys =
- ref (Symtab.make [("ProtoPure",
- ThyInfo {path = "",
- children = ["Pure", "CPure"], parents = [],
- thy_time = Some "", ml_time = Some "",
- theory = Some proto_pure_thy,
- thms = Symtab.null, methods = Symtab.null,
- data = (Symtab.null, Symtab.null)}),
- ("Pure",
- ThyInfo {path = "", children = [],
- parents = ["ProtoPure"],
- thy_time = Some "", ml_time = Some "",
- theory = Some pure_thy, thms = Symtab.null,
- methods = Symtab.null,
- data = (Symtab.null, Symtab.null)}),
- ("CPure",
- ThyInfo {path = "",
- children = [], parents = ["ProtoPure"],
- thy_time = Some "", ml_time = Some "",
- theory = Some cpure_thy,
- thms = Symtab.null,
- methods = Symtab.null,
- data = (Symtab.null, Symtab.null)})
- ]);
+ ref (Symtab.make (map mk_info
+ [("ProtoPure", ["Pure", "CPure"], [], Theory.proto_pure),
+ ("Pure", [], ["ProtoPure"], Theory.pure),
+ ("CPure", [], ["ProtoPure"], Theory.cpure)]));
-(*Get thy_info for a loaded theory *)
-fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
+(* retrieve info *)
+
+fun err_not_stored name =
+ error ("Theory " ^ name ^ " not stored by loader");
+
+fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
-(*Get path where theory's files are located*)
-fun path_of tname =
- let val ThyInfo {path, ...} = the (get_thyinfo tname)
- in path end;
+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;
-(*Guess the name of a theory object
- (First the quick way by looking at the stamps; if that doesn't work,
- we search loaded_thys for the first theory which fits.)
-*)
-fun thyname_of_sign sg =
- let val ref xname = hd (#stamps (Sign.rep_sg sg));
- val opt_info = get_thyinfo xname;
-
- fun eq_sg (ThyInfo {theory = None, ...}) = false
- | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
-
- val show_sg = Pretty.str_of o Sign.pretty_sg;
- in
- if is_some opt_info andalso eq_sg (the opt_info) then xname
- else
- (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
- Some (name, _) => name
- | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
- end;
-
-
-(*Guess to which theory a signature belongs and return it's thy_info*)
-fun thyinfo_of_sign sg =
- let val name = thyname_of_sign sg;
- in (name, the (get_thyinfo name)) end;
+(*path where theory's files are located*)
+val path_of = #path o the_thyinfo;
-(*Try to get the theory object corresponding to a given signature*)
+(*try to get the theory object corresponding to a given signature*)
fun theory_of_sign sg =
(case thyinfo_of_sign sg of
- (_, ThyInfo {theory = Some thy, ...}) => thy
+ (_, {theory = Some thy, ...}) => thy
| _ => sys_error "theory_of_sign");
+(*try to get the theory object corresponding to a given theorem*)
+val theory_of_thm = theory_of_sign o #sign o rep_thm;
-(*Try to get the theory object corresponding to a given theorem*)
-val theory_of_thm = theory_of_sign o #sign o rep_thm;
+(*get all direct descendants of a theory*)
+fun children_of t =
+ (case get_thyinfo t of
+ Some ({children, ...}) => children
+ | None => []);
+
+(*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_of name =
+ (case get_thyinfo name of
+ Some ({theory = Some t, ...}) => t
+ | _ => err_not_stored name);
-(*Get all direct descendants of a theory*)
-fun children_of t =
- case get_thyinfo t of Some (ThyInfo {children, ...}) => children
- | None => [];
-
-
-(*Get all direct ancestors of a theory*)
-fun parents_of_name t =
- case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
- | None => [];
-
-
-(*Get theory object for a loaded theory *)
-fun theory_of name =
- case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
- | _ => error ("Theory " ^ name ^
- " not stored by loader");
-
-
-(*Invoke every put method stored in a theory's methods table to initialize
+(*invoke every put method stored in a theory's methods table to initialize
the state of user defined variables*)
fun put_thydata first tname =
let val (methods, data) =
case get_thyinfo tname of
- Some (ThyInfo {methods, data, ...}) =>
+ Some ({methods, data, ...}) =>
(methods, Symtab.dest ((if first then fst else snd) data))
- | None => error ("Theory " ^ tname ^ " not stored by loader");
+ | None => err_not_stored tname;
fun put_data (id, date) =
case Symtab.lookup (methods, id) of
@@ -190,9 +161,9 @@
(*Change theory object for an existent item of loaded_thys*)
fun store_theory (thy, tname) =
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
- Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
+ Some ({path, children, parents, thy_time, ml_time, thms,
methods, data, ...}) =>
- ThyInfo {path = path, children = children, parents = parents,
+ {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = Some thy, thms = thms,
methods = methods, data = data}
@@ -204,12 +175,9 @@
(*Add data handling methods to theory*)
fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
- let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
- thms, methods, data} =
- case get_thyinfo tname of
- Some ti => ti
- | None => error ("Theory " ^ tname ^ " not stored by loader");
- in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
+ let val {path, children, parents, thy_time, ml_time, theory,
+ thms, methods, data} = the_thyinfo tname;
+ in loaded_thys := Symtab.update ((tname, {path = path,
children = children, parents = parents, thy_time = thy_time,
ml_time = ml_time, theory = theory, thms = thms,
methods = Symtab.update (new_methods, methods), data = data}),
@@ -217,11 +185,9 @@
end;
-(*Retrieve data associated with theory*)
-fun get_thydata tname id =
- let val d2 = case get_thyinfo tname of
- Some (ThyInfo {data, ...}) => snd data
- | None => error ("Theory " ^ tname ^ " not stored by loader");
- in Symtab.lookup (d2, id) end;
+(*retrieve data associated with theory*)
+fun get_thydata name id =
+ Symtab.lookup (snd (#data (the_thyinfo name)), id);
+
end;
--- a/src/Pure/Thy/thy_read.ML Thu Oct 23 12:13:15 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML Thu Oct 23 12:43:07 1997 +0200
@@ -66,7 +66,7 @@
fun already_loaded thy =
let val t = get_thyinfo thy
in if is_none t then false
- else let val ThyInfo {thy_time, ml_time, ...} = the t
+ else let val {thy_time, ml_time, ...} = the t
in is_some thy_time andalso is_some ml_time end
end;
@@ -75,7 +75,7 @@
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 (ThyInfo {thy_time, ml_time, ...}) =>
+ 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
@@ -136,7 +136,7 @@
val tinfo = get_thyinfo name;
in if is_some tinfo andalso path = "" then
- let val ThyInfo {path = abs_path, ...} = the tinfo;
+ 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"))
@@ -154,9 +154,9 @@
(*Remove theory from all child lists in loaded_thys *)
fun unlink_thy tname =
- let fun remove (ThyInfo {path, children, parents, thy_time, ml_time,
+ let fun remove ({path, children, parents, thy_time, ml_time,
theory, thms, methods, data}) =
- ThyInfo {path = path, children = children \ tname, parents = parents,
+ {path = path, children = children \ tname, parents = parents,
thy_time = thy_time, ml_time = ml_time, theory = theory,
thms = thms, methods = methods, data = data}
in loaded_thys := Symtab.map remove (!loaded_thys) end;
@@ -171,9 +171,9 @@
(*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 (ThyInfo {path, children, parents, theory, thms,
+ Some ({path, children, parents, theory, thms,
methods, data, ...}) =>
- ThyInfo {path = path, children = children, parents = parents,
+ {path = path, children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
methods = methods, data = data}
@@ -186,7 +186,7 @@
let val t = get_thyinfo tname;
in if is_none t then ()
else
- let val ThyInfo {thy_time, ml_time, ...} = the t
+ 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
@@ -217,11 +217,11 @@
(*Set absolute path for loaded theory *)
fun set_path () =
- let val ThyInfo {children, parents, thy_time, ml_time, theory, thms,
+ let val {children, parents, thy_time, ml_time, theory, thms,
methods, data, ...} =
the (Symtab.lookup (!loaded_thys, tname));
in loaded_thys := Symtab.update ((tname,
- ThyInfo {path = abs_path,
+ {path = abs_path,
children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
@@ -245,7 +245,7 @@
(*Invoke every get method stored in the methods table and store result in
data table*)
fun save_data thy_only =
- let val ThyInfo {path, children, parents, thy_time, ml_time,
+ let val {path, children, parents, thy_time, ml_time,
theory, thms, methods, data} = the (get_thyinfo tname);
fun get_data [] data = data
@@ -257,7 +257,7 @@
val data' = (if thy_only then new_data else fst data, new_data)
(* 2nd component must be up to date *)
in loaded_thys := Symtab.update
- ((tname, ThyInfo {path = path,
+ ((tname, {path = path,
children = children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
@@ -267,7 +267,7 @@
(*Make sure that loaded_thys contains an entry for tname*)
fun init_thyinfo () =
- let val tinfo = ThyInfo {path = "", children = [], parents = [],
+ let val tinfo = {path = "", children = [], parents = [],
thy_time = None, ml_time = None,
theory = None, thms = Symtab.null,
methods = Symtab.null,
@@ -372,7 +372,7 @@
fun reload_changed (t :: ts) =
let val abspath = case get_thyinfo t of
- Some (ThyInfo {path, ...}) => path
+ Some ({path, ...}) => path
| None => "";
val (thy_file, ml_file) = get_filenames abspath t;
@@ -388,7 +388,7 @@
If there are still children in the deleted theory's list
schedule them for reloading *)
fun collect_garbage no_garbage =
- let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
+ 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.");
@@ -413,7 +413,7 @@
error ("Cyclic dependency of theories: "
^ child ^ "->" ^ base ^ result)
else if is_some tinfo then
- let val ThyInfo {children, ...} = the tinfo
+ let val {children, ...} = the tinfo
in seq (find_it ("->" ^ curr ^ result)) children
end
else ()
@@ -429,14 +429,14 @@
fun add_child base =
let val tinfo =
case Symtab.lookup (!loaded_thys, base) of
- Some (ThyInfo {path, children, parents, thy_time, ml_time,
+ Some ({path, children, parents, thy_time, ml_time,
theory, thms, methods, data}) =>
- ThyInfo {path = path,
+ {path = path,
children = child ins children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,
methods = methods, data = data}
- | None => ThyInfo {path = "", children = [child], parents = [],
+ | None => {path = "", children = [child], parents = [],
thy_time = None, ml_time = None,
theory = None, thms = Symtab.null,
methods = Symtab.null,
@@ -480,13 +480,13 @@
val datas =
let fun get_data t =
- let val ThyInfo {data, ...} = the (get_thyinfo t)
+ let val {data, ...} = the (get_thyinfo t)
in snd data end;
in map (Symtab.dest o get_data) mergelist end;
val methods =
let fun get_methods t =
- let val ThyInfo {methods, ...} = the (get_thyinfo t)
+ let val {methods, ...} = the (get_thyinfo t)
in methods end;
val ms = map get_methods mergelist;
@@ -536,9 +536,9 @@
val dummy =
let val tinfo = case Symtab.lookup (!loaded_thys, child) of
- Some (ThyInfo {path, children, thy_time, ml_time, theory, thms,
+ Some ({path, children, thy_time, ml_time, theory, thms,
data, ...}) =>
- ThyInfo {path = path,
+ {path = path,
children = children, parents = mergelist,
thy_time = thy_time, ml_time = ml_time,
theory = theory, thms = thms,