--- a/src/Pure/Thy/thy_info.ML Tue Nov 04 09:27:32 1997 +0100
+++ b/src/Pure/Thy/thy_info.ML Tue Nov 04 12:03:48 1997 +0100
@@ -2,71 +2,44 @@
ID: $Id$
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
-Theory loader info database.
+Theory loader database.
*)
-(* 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};
-
-
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};
+ theory: theory option};
(*
- 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
- like Pure or theories without a ML file)
- theory = None theory has not been read yet
+ path: directory where theory's files are located
+ (* FIXME do not store absolute path!!! *)
- parents: While 'children' contains all theories the theory depends
- on (i.e. also ones quoted in the .thy file),
- 'parents' only contains the theories which were used to form
- the base of this theory.
+ 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
+ like Pure or theories without a ML file)
+ theory = None theory has not been read yet
- methods: three methods for each user defined data;
- merge: merges data of ancestor theories
- put: retrieves data from loaded_thys and stores it somewhere
- get: retrieves data from somewhere and stores it
- in loaded_thys
- data: user defined data; exn is used to allow arbitrary types;
- first element of pairs contains result that get returned after
- thy file was read, second element after ML file was read;
- 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
+ parents: While 'children' contains all theories the theory depends
+ on (i.e. also ones quoted in the .thy file),
+ 'parents' only contains the theories which were used to form
+ the base of this theory.
*)
signature THY_INFO =
sig
- val loaded_thys : thy_info Symtab.table ref
- val store_theory : theory * string -> unit
-
- val theory_of : string -> theory
- val theory_of_sign : Sign.sg -> theory
- val theory_of_thm : thm -> theory
- val children_of : string -> string list
+ val loaded_thys: thy_info Symtab.table ref
+ val get_thyinfo: string -> thy_info option
+ val store_theory: theory * string -> unit
+ val path_of: string -> string
+ val children_of: string -> string list
val parents_of_name: string -> string list
val thyinfo_of_sign: Sign.sg -> string * thy_info
-
- val add_thydata : string -> string * thy_methods -> unit
- val get_thydata : string -> string -> exn option
- val put_thydata : bool -> string -> unit
- val set_current_thy: string -> unit
- val get_thyinfo : string -> thy_info option
-
- val path_of : string -> string
+ val theory_of: string -> theory
+ val theory_of_sign: Sign.sg -> theory
+ val theory_of_thm: thm -> theory
end;
@@ -76,10 +49,8 @@
(* 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);
+ (name, {path = "", children = children, parents = parents,
+ thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
(*preloaded theories*)
val loaded_thys =
@@ -122,72 +93,33 @@
(*get all direct descendants of a theory*)
fun children_of t =
(case get_thyinfo t of
- Some ({children, ...}) => children
+ Some {children, ...} => children
| None => []);
(*get all direct ancestors of a theory*)
fun parents_of_name t =
(case get_thyinfo t of
- Some ({parents, ...}) => parents
+ 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
+ Some {theory = Some t, ...} => t
| _ => err_not_stored name);
-(*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 ({methods, data, ...}) =>
- (methods, Symtab.dest ((if first then fst else snd) data))
- | None => err_not_stored tname;
-
- fun put_data (id, date) =
- case Symtab.lookup (methods, id) of
- Some (ThyMethods {put, ...}) => put date
- | None => error ("No method defined for theory data \"" ^
- id ^ "\"");
- in seq put_data data end;
-
-
-val set_current_thy = put_thydata false;
-
+(* store_theory *)
-(*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 ({path, children, parents, thy_time, ml_time, thms,
- methods, data, ...}) =>
- {path = path, children = children, parents = parents,
- thy_time = thy_time, ml_time = ml_time,
- theory = Some thy, thms = thms,
- methods = methods, data = data}
- | None => error ("store_theory: theory " ^ tname ^ " not found");
- in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
-
-
-(*** Misc functions ***)
-
-(*Add data handling methods to theory*)
-fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
- 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}),
- !loaded_thys)
+fun store_theory (thy, name) =
+ let
+ val {path, children, parents, thy_time, ml_time, theory = _} =
+ the_thyinfo name;
+ val info = {path = path, children = children, parents = parents,
+ thy_time = thy_time, ml_time = ml_time, theory = Some thy};
+ in
+ loaded_thys := Symtab.update ((name, info), ! loaded_thys)
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 Tue Nov 04 09:27:32 1997 +0100
+++ b/src/Pure/Thy/thy_read.ML Tue Nov 04 12:03:48 1997 +0100
@@ -154,11 +154,9 @@
(*Remove theory from all child lists in loaded_thys *)
fun unlink_thy tname =
- let fun remove ({path, children, parents, thy_time, ml_time,
- theory, thms, methods, data}) =
+ 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,
- thms = thms, methods = methods, data = data}
+ thy_time = thy_time, ml_time = ml_time, theory = theory}
in loaded_thys := Symtab.map remove (!loaded_thys) end;
@@ -171,12 +169,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 ({path, children, parents, theory, thms,
- methods, data, ...}) =>
+ 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, thms = thms,
- methods = methods, data = data}
+ 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;
@@ -217,15 +212,13 @@
(*Set absolute path for loaded theory *)
fun set_path () =
- let val {children, parents, thy_time, ml_time, theory, thms,
- methods, data, ...} =
+ 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, thms = thms,
- methods = methods, data = data}),
+ theory = theory}),
!loaded_thys)
end;
@@ -242,36 +235,11 @@
seq mark_outdated present
end;
- (*Invoke every get method stored in the methods table and store result in
- data table*)
- fun save_data thy_only =
- let val {path, children, parents, thy_time, ml_time,
- theory, thms, methods, data} = the (get_thyinfo tname);
-
- fun get_data [] data = data
- | get_data ((id, ThyMethods {get, ...}) :: ms) data =
- get_data ms (Symtab.update ((id, get ()), data));
-
- val new_data = get_data (Symtab.dest methods) Symtab.null;
-
- 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, {path = path,
- children = children, parents = parents,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory, thms = thms,
- methods = methods, data = data'}),
- !loaded_thys)
- 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, thms = Symtab.null,
- methods = Symtab.null,
- data = (Symtab.null, Symtab.null)};
+ theory = None};
in if is_some (get_thyinfo tname) then ()
else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
end;
@@ -284,7 +252,6 @@
init_thyinfo ();
read_thy tname thy_file;
SymbolInput.use (out_name tname);
- save_data true;
if not (!delete_tmpfiles) then ()
else OS.FileSys.remove (out_name tname);
@@ -298,7 +265,6 @@
if ml_file = "" then ()
else (writeln ("Reading \"" ^ name ^ ".ML\"");
SymbolInput.use ml_file);
- save_data false;
(*Store theory again because it could have been redefined*)
use_strings
@@ -417,17 +383,14 @@
let val tinfo =
case Symtab.lookup (!loaded_thys, base) of
Some ({path, children, parents, thy_time, ml_time,
- theory, thms, methods, data}) =>
+ theory}) =>
{path = path,
children = child ins children, parents = parents,
thy_time = thy_time, ml_time = ml_time,
- theory = theory, thms = thms,
- methods = methods, data = data}
+ theory = theory}
| None => {path = "", children = [child], parents = [],
thy_time = None, ml_time = None,
- theory = None, thms = Symtab.null,
- methods = Symtab.null,
- data = (Symtab.null, Symtab.null)};
+ theory = None};
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
(*Load a base theory if not already done
@@ -466,75 +429,16 @@
if null mergelist then ProtoPure.thy
else Theory.prep_ext_merge (map theory_of mergelist));
- val datas =
- let fun get_data 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 {methods, ...} = the (get_thyinfo t)
- in methods end;
-
- val ms = map get_methods mergelist;
- in if null ms then Symtab.null
- else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms)
- end;
-
- (*merge two sorted association lists*)
- fun merge_two ([], d2) = d2
- | merge_two (d1, []) = d1
- | merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s),
- l2 as ((p2 as (id2, d2)) :: d2s)) =
- if id1 < id2 then
- p1 :: merge_two (d1s, l2)
- else
- p2 :: merge_two (l1, d2s);
-
- (*Merge multiple occurence of data; also call put for each merged list*)
- fun merge_multi [] None = []
- | merge_multi [] (Some (id, ds)) =
- let val ThyMethods {merge, put, ...} =
- the (Symtab.lookup (methods, id));
- in put (merge ds); [id] end
- | merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d]))
- | merge_multi ((id, d) :: ds) (Some (id2, d2s)) =
- if id = id2 then
- merge_multi ds (Some (id2, d :: d2s))
- else
- let val ThyMethods {merge, put, ...} =
- the (Symtab.lookup (methods, id2));
- in put (merge d2s);
- id2 :: merge_multi ds (Some (id, [d]))
- end;
-
- val merged =
- if null datas then []
- else merge_multi (foldl merge_two (hd datas, tl datas)) None;
-
- val dummy =
- let val unmerged = map fst (Symtab.dest methods) \\ merged;
-
- fun put_empty id =
- let val ThyMethods {merge, put, ...} =
- the (Symtab.lookup (methods, id));
- in put (merge []) end;
- in seq put_empty unmerged end;
-
val dummy =
let val tinfo = case Symtab.lookup (!loaded_thys, child) of
- Some ({path, children, thy_time, ml_time, theory, thms,
- data, ...}) =>
- {path = path,
- children = children, parents = mergelist,
- thy_time = thy_time, ml_time = ml_time,
- theory = theory, thms = thms,
- methods = methods, data = data}
- | None => error ("set_parents: theory " ^ child ^ " not found");
+ 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;
+ in
+ cur_thyname := child;
base_thy
end;