# HG changeset patch # User berghofe # Date 870819979 -7200 # Node ID 6bf9f09f3d61816de7a5e11af5c2a82e868477cd # Parent 5eef2ff0eb72df49dd8fdf80867bdeabe1a8c8ca Moved functions for theory information storage / retrieval from thy_read.ML to thy_info.ML . diff -r 5eef2ff0eb72 -r 6bf9f09f3d61 src/Pure/Thy/thy_info.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 06 00:26:19 1997 +0200 @@ -0,0 +1,227 @@ +(* 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;