Moved functions for theory information storage / retrieval
from thy_read.ML to thy_info.ML .
(* 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
Functions for storing and retrieving arbitrary theory information.
*)
(*Types for theory storage*)
(*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
= 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
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.
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
*)
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 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
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
end;
structure ThyInfo: THY_INFO =
struct
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)})
]);
(*Get thy_info for a loaded theory *)
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
(*Get path where theory's files are located*)
fun path_of tname =
let val ThyInfo {path, ...} = the (get_thyinfo tname)
in path 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;
(*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
| _ => 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;
(*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
the state of user defined variables*)
fun put_thydata first tname =
let val (methods, data) =
case get_thyinfo tname of
Some (ThyInfo {methods, data, ...}) =>
(methods, Symtab.dest ((if first then fst else snd) data))
| None => error ("Theory " ^ tname ^ " not stored by loader");
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;
(*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,
methods, data, ...}) =>
ThyInfo {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 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,
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)
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;
end;