Moved functions for theory information storage / retrieval
authorberghofe
Wed Aug 06 00:26:19 1997 +0200 (1997-08-06)
changeset 36046bf9f09f3d61
parent 3603 5eef2ff0eb72
child 3605 d372fb6ec393
Moved functions for theory information storage / retrieval
from thy_read.ML to thy_info.ML .
src/Pure/Thy/thy_info.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 06 00:26:19 1997 +0200
     1.3 @@ -0,0 +1,227 @@
     1.4 +(*  Title:      Pure/Thy/thy_info.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
     1.7 +                Tobias Nipkow and L C Paulson
     1.8 +    Copyright   1994 TU Muenchen
     1.9 +
    1.10 +Functions for storing and retrieving arbitrary theory information.
    1.11 +*)
    1.12 +
    1.13 +(*Types for theory storage*)
    1.14 +
    1.15 +(*Functions to handle arbitrary data added by the user; type "exn" is used
    1.16 +  to store data*)
    1.17 +datatype thy_methods =
    1.18 +  ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    1.19 +
    1.20 +datatype thy_info =
    1.21 +  ThyInfo of {path: string,
    1.22 +              children: string list, parents: string list,
    1.23 +              thy_time: string option, ml_time: string option,
    1.24 +              theory: theory option, thms: thm Symtab.table,
    1.25 +              methods: thy_methods Symtab.table,
    1.26 +              data: exn Symtab.table * exn Symtab.table};
    1.27 +      (*thy_time, ml_time = None     theory file has not been read yet
    1.28 +                          = Some ""  theory was read but has either been marked
    1.29 +                                     as outdated or there is no such file for
    1.30 +                                     this theory (see e.g. 'virtual' theories
    1.31 +                                     like Pure or theories without a ML file)
    1.32 +        theory = None  theory has not been read yet
    1.33 +
    1.34 +        parents: While 'children' contains all theories the theory depends
    1.35 +                 on (i.e. also ones quoted in the .thy file),
    1.36 +                 'parents' only contains the theories which were used to form
    1.37 +                 the base of this theory.
    1.38 +
    1.39 +        methods: three methods for each user defined data;
    1.40 +                 merge: merges data of ancestor theories
    1.41 +                 put: retrieves data from loaded_thys and stores it somewhere
    1.42 +                 get: retrieves data from somewhere and stores it
    1.43 +                      in loaded_thys
    1.44 +        data: user defined data; exn is used to allow arbitrary types;
    1.45 +              first element of pairs contains result that get returned after
    1.46 +              thy file was read, second element after ML file was read;
    1.47 +              if ML files has not been read, second element is identical to
    1.48 +              first one because get_thydata, which is meant to return the
    1.49 +              latest data, always accesses the 2nd element
    1.50 +       *)
    1.51 +
    1.52 +
    1.53 +signature THY_INFO =
    1.54 +sig
    1.55 +  val loaded_thys    : thy_info Symtab.table ref
    1.56 +  val store_theory   : theory * string -> unit
    1.57 +
    1.58 +  val theory_of      : string -> theory
    1.59 +  val theory_of_sign : Sign.sg -> theory
    1.60 +  val theory_of_thm  : thm -> theory
    1.61 +  val children_of    : string -> string list
    1.62 +  val parents_of_name: string -> string list
    1.63 +  val thyname_of_sign: Sign.sg -> string
    1.64 +  val thyinfo_of_sign: Sign.sg -> string * thy_info
    1.65 +
    1.66 +  val add_thydata    : string -> string * thy_methods -> unit
    1.67 +  val get_thydata    : string -> string -> exn option
    1.68 +  val put_thydata    : bool -> string -> unit
    1.69 +  val set_current_thy: string -> unit
    1.70 +  val get_thyinfo    : string -> thy_info option
    1.71 +
    1.72 +  val path_of        : string -> string
    1.73 +end;
    1.74 +
    1.75 +
    1.76 +
    1.77 +structure ThyInfo: THY_INFO =
    1.78 +struct
    1.79 +
    1.80 +
    1.81 +val loaded_thys =
    1.82 +  ref (Symtab.make [("ProtoPure",
    1.83 +                     ThyInfo {path = "",
    1.84 +                              children = ["Pure", "CPure"], parents = [],
    1.85 +                              thy_time = Some "", ml_time = Some "",
    1.86 +                              theory = Some proto_pure_thy,
    1.87 +                              thms = Symtab.null, methods = Symtab.null,
    1.88 +                              data = (Symtab.null, Symtab.null)}),
    1.89 +                    ("Pure",
    1.90 +                     ThyInfo {path = "", children = [],
    1.91 +                              parents = ["ProtoPure"],
    1.92 +                              thy_time = Some "", ml_time = Some "",
    1.93 +                              theory = Some pure_thy, thms = Symtab.null,
    1.94 +                              methods = Symtab.null,
    1.95 +                              data = (Symtab.null, Symtab.null)}),
    1.96 +                    ("CPure",
    1.97 +                     ThyInfo {path = "",
    1.98 +                              children = [], parents = ["ProtoPure"],
    1.99 +                              thy_time = Some "", ml_time = Some "",
   1.100 +                              theory = Some cpure_thy,
   1.101 +                              thms = Symtab.null,
   1.102 +                              methods = Symtab.null,
   1.103 +                              data = (Symtab.null, Symtab.null)})
   1.104 +                   ]);
   1.105 +
   1.106 +
   1.107 +(*Get thy_info for a loaded theory *)
   1.108 +fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
   1.109 +
   1.110 +(*Get path where theory's files are located*)
   1.111 +fun path_of tname =
   1.112 +  let val ThyInfo {path, ...} = the (get_thyinfo tname)
   1.113 +  in path end;
   1.114 +
   1.115 +
   1.116 +(*Guess the name of a theory object
   1.117 +  (First the quick way by looking at the stamps; if that doesn't work,
   1.118 +   we search loaded_thys for the first theory which fits.)
   1.119 +*)
   1.120 +fun thyname_of_sign sg =
   1.121 +  let val ref xname = hd (#stamps (Sign.rep_sg sg));
   1.122 +      val opt_info = get_thyinfo xname;
   1.123 +
   1.124 +    fun eq_sg (ThyInfo {theory = None, ...}) = false
   1.125 +      | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
   1.126 +
   1.127 +    val show_sg = Pretty.str_of o Sign.pretty_sg;
   1.128 +  in
   1.129 +    if is_some opt_info andalso eq_sg (the opt_info) then xname
   1.130 +    else
   1.131 +      (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
   1.132 +        Some (name, _) => name
   1.133 +      | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
   1.134 +  end;
   1.135 +
   1.136 +
   1.137 +(*Guess to which theory a signature belongs and return it's thy_info*)
   1.138 +fun thyinfo_of_sign sg =
   1.139 +  let val name = thyname_of_sign sg;
   1.140 +  in (name, the (get_thyinfo name)) end;
   1.141 +
   1.142 +
   1.143 +(*Try to get the theory object corresponding to a given signature*)
   1.144 +fun theory_of_sign sg =
   1.145 +  (case thyinfo_of_sign sg of
   1.146 +    (_, ThyInfo {theory = Some thy, ...}) => thy
   1.147 +  | _ => sys_error "theory_of_sign");
   1.148 +
   1.149 +
   1.150 +(*Try to get the theory object corresponding to a given theorem*)
   1.151 +val theory_of_thm = theory_of_sign o #sign o rep_thm;
   1.152 +
   1.153 +
   1.154 +(*Get all direct descendants of a theory*)
   1.155 +fun children_of t =
   1.156 +  case get_thyinfo t of Some (ThyInfo {children, ...}) => children
   1.157 +                      | None => [];
   1.158 +
   1.159 +
   1.160 +(*Get all direct ancestors of a theory*)
   1.161 +fun parents_of_name t =
   1.162 +  case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
   1.163 +                      | None => [];
   1.164 +
   1.165 +
   1.166 +(*Get theory object for a loaded theory *)
   1.167 +fun theory_of name =
   1.168 +  case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
   1.169 +                         | _ => error ("Theory " ^ name ^
   1.170 +                                       " not stored by loader");
   1.171 +
   1.172 +
   1.173 +(*Invoke every put method stored in a theory's methods table to initialize
   1.174 +  the state of user defined variables*)
   1.175 +fun put_thydata first tname =
   1.176 +  let val (methods, data) = 
   1.177 +        case get_thyinfo tname of
   1.178 +            Some (ThyInfo {methods, data, ...}) => 
   1.179 +              (methods, Symtab.dest ((if first then fst else snd) data))
   1.180 +          | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.181 +
   1.182 +      fun put_data (id, date) =
   1.183 +            case Symtab.lookup (methods, id) of
   1.184 +                Some (ThyMethods {put, ...}) => put date
   1.185 +              | None => error ("No method defined for theory data \"" ^
   1.186 +                               id ^ "\"");
   1.187 +  in seq put_data data end;
   1.188 +
   1.189 +
   1.190 +val set_current_thy = put_thydata false;
   1.191 +
   1.192 +
   1.193 +(*Change theory object for an existent item of loaded_thys*)
   1.194 +fun store_theory (thy, tname) =
   1.195 +  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   1.196 +               Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
   1.197 +                              methods, data, ...}) =>
   1.198 +                 ThyInfo {path = path, children = children, parents = parents,
   1.199 +                          thy_time = thy_time, ml_time = ml_time,
   1.200 +                          theory = Some thy, thms = thms,
   1.201 +                          methods = methods, data = data}
   1.202 +             | None => error ("store_theory: theory " ^ tname ^ " not found");
   1.203 +  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   1.204 +
   1.205 +
   1.206 +(*** Misc functions ***)
   1.207 +
   1.208 +(*Add data handling methods to theory*)
   1.209 +fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
   1.210 +  let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
   1.211 +                   thms, methods, data} =
   1.212 +        case get_thyinfo tname of
   1.213 +            Some ti => ti
   1.214 +          | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.215 +  in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
   1.216 +       children = children, parents = parents, thy_time = thy_time,
   1.217 +       ml_time = ml_time, theory = theory, thms = thms,
   1.218 +       methods = Symtab.update (new_methods, methods), data = data}),
   1.219 +       !loaded_thys)
   1.220 +  end;
   1.221 +
   1.222 +
   1.223 +(*Retrieve data associated with theory*)
   1.224 +fun get_thydata tname id =
   1.225 +  let val d2 = case get_thyinfo tname of
   1.226 +                   Some (ThyInfo {data, ...}) => snd data
   1.227 +                 | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.228 +  in Symtab.lookup (d2, id) end;
   1.229 +
   1.230 +end;