src/Pure/Thy/thy_info.ML
changeset 3976 1030dd79720b
parent 3604 6bf9f09f3d61
child 3997 42062f636bdf
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Oct 23 12:13:15 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Oct 23 12:43:07 1997 +0200
     1.3 @@ -1,27 +1,29 @@
     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 +    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    1.10  
    1.11 -Functions for storing and retrieving arbitrary theory information.
    1.12 +Theory loader info database.
    1.13  *)
    1.14  
    1.15 -(*Types for theory storage*)
    1.16 -
    1.17 +(* FIXME wipe out! *)
    1.18  (*Functions to handle arbitrary data added by the user; type "exn" is used
    1.19    to store data*)
    1.20  datatype thy_methods =
    1.21    ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    1.22  
    1.23 -datatype thy_info =
    1.24 -  ThyInfo of {path: string,
    1.25 -              children: string list, parents: string list,
    1.26 -              thy_time: string option, ml_time: string option,
    1.27 -              theory: theory option, thms: thm Symtab.table,
    1.28 -              methods: thy_methods Symtab.table,
    1.29 -              data: exn Symtab.table * exn Symtab.table};
    1.30 -      (*thy_time, ml_time = None     theory file has not been read yet
    1.31 +
    1.32 +type thy_info =
    1.33 +  {path: string,
    1.34 +    children: string list, parents: string list,
    1.35 +    thy_time: string option, ml_time: string option,
    1.36 +    theory: theory option, thms: thm Symtab.table,
    1.37 +    methods: thy_methods Symtab.table,
    1.38 +    data: exn Symtab.table * exn Symtab.table};
    1.39 +
    1.40 +(*
    1.41 +        path: directory where theory's files are located
    1.42 +
    1.43 +        thy_time, ml_time = None     theory file has not been read yet
    1.44                            = Some ""  theory was read but has either been marked
    1.45                                       as outdated or there is no such file for
    1.46                                       this theory (see e.g. 'virtual' theories
    1.47 @@ -44,8 +46,7 @@
    1.48                if ML files has not been read, second element is identical to
    1.49                first one because get_thydata, which is meant to return the
    1.50                latest data, always accesses the 2nd element
    1.51 -       *)
    1.52 -
    1.53 +*)
    1.54  
    1.55  signature THY_INFO =
    1.56  sig
    1.57 @@ -57,7 +58,6 @@
    1.58    val theory_of_thm  : thm -> theory
    1.59    val children_of    : string -> string list
    1.60    val parents_of_name: string -> string list
    1.61 -  val thyname_of_sign: Sign.sg -> string
    1.62    val thyinfo_of_sign: Sign.sg -> string * thy_info
    1.63  
    1.64    val add_thydata    : string -> string * thy_methods -> unit
    1.65 @@ -70,111 +70,82 @@
    1.66  end;
    1.67  
    1.68  
    1.69 -
    1.70  structure ThyInfo: THY_INFO =
    1.71  struct
    1.72  
    1.73 +(* loaded theories *)
    1.74  
    1.75 +fun mk_info (name, children, parents, theory) =
    1.76 +  (name,
    1.77 +    {path = "", children = children, parents = parents, thy_time = Some "",
    1.78 +      ml_time = Some "", theory = Some theory, thms = Symtab.null,
    1.79 +      methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info);
    1.80 +
    1.81 +(*preloaded theories*)
    1.82  val loaded_thys =
    1.83 -  ref (Symtab.make [("ProtoPure",
    1.84 -                     ThyInfo {path = "",
    1.85 -                              children = ["Pure", "CPure"], parents = [],
    1.86 -                              thy_time = Some "", ml_time = Some "",
    1.87 -                              theory = Some proto_pure_thy,
    1.88 -                              thms = Symtab.null, methods = Symtab.null,
    1.89 -                              data = (Symtab.null, Symtab.null)}),
    1.90 -                    ("Pure",
    1.91 -                     ThyInfo {path = "", children = [],
    1.92 -                              parents = ["ProtoPure"],
    1.93 -                              thy_time = Some "", ml_time = Some "",
    1.94 -                              theory = Some pure_thy, thms = Symtab.null,
    1.95 -                              methods = Symtab.null,
    1.96 -                              data = (Symtab.null, Symtab.null)}),
    1.97 -                    ("CPure",
    1.98 -                     ThyInfo {path = "",
    1.99 -                              children = [], parents = ["ProtoPure"],
   1.100 -                              thy_time = Some "", ml_time = Some "",
   1.101 -                              theory = Some cpure_thy,
   1.102 -                              thms = Symtab.null,
   1.103 -                              methods = Symtab.null,
   1.104 -                              data = (Symtab.null, Symtab.null)})
   1.105 -                   ]);
   1.106 +  ref (Symtab.make (map mk_info
   1.107 +    [("ProtoPure", ["Pure", "CPure"], [], Theory.proto_pure),
   1.108 +     ("Pure", [], ["ProtoPure"], Theory.pure),
   1.109 +     ("CPure", [], ["ProtoPure"], Theory.cpure)]));
   1.110  
   1.111  
   1.112 -(*Get thy_info for a loaded theory *)
   1.113 -fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
   1.114 +(* retrieve info *)
   1.115 +
   1.116 +fun err_not_stored name =
   1.117 +  error ("Theory " ^ name ^ " not stored by loader");
   1.118 +
   1.119 +fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
   1.120  
   1.121 -(*Get path where theory's files are located*)
   1.122 -fun path_of tname =
   1.123 -  let val ThyInfo {path, ...} = the (get_thyinfo tname)
   1.124 -  in path end;
   1.125 +fun the_thyinfo name =
   1.126 +  (case get_thyinfo name of
   1.127 +    Some info => info
   1.128 +  | None => err_not_stored name);
   1.129 +
   1.130 +fun thyinfo_of_sign sg =
   1.131 +  let val name = Sign.name_of sg
   1.132 +  in (name, the_thyinfo name) end;
   1.133  
   1.134  
   1.135 -(*Guess the name of a theory object
   1.136 -  (First the quick way by looking at the stamps; if that doesn't work,
   1.137 -   we search loaded_thys for the first theory which fits.)
   1.138 -*)
   1.139 -fun thyname_of_sign sg =
   1.140 -  let val ref xname = hd (#stamps (Sign.rep_sg sg));
   1.141 -      val opt_info = get_thyinfo xname;
   1.142 -
   1.143 -    fun eq_sg (ThyInfo {theory = None, ...}) = false
   1.144 -      | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
   1.145 -
   1.146 -    val show_sg = Pretty.str_of o Sign.pretty_sg;
   1.147 -  in
   1.148 -    if is_some opt_info andalso eq_sg (the opt_info) then xname
   1.149 -    else
   1.150 -      (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
   1.151 -        Some (name, _) => name
   1.152 -      | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
   1.153 -  end;
   1.154 -
   1.155 -
   1.156 -(*Guess to which theory a signature belongs and return it's thy_info*)
   1.157 -fun thyinfo_of_sign sg =
   1.158 -  let val name = thyname_of_sign sg;
   1.159 -  in (name, the (get_thyinfo name)) end;
   1.160 +(*path where theory's files are located*)
   1.161 +val path_of = #path o the_thyinfo;
   1.162  
   1.163  
   1.164 -(*Try to get the theory object corresponding to a given signature*)
   1.165 +(*try to get the theory object corresponding to a given signature*)
   1.166  fun theory_of_sign sg =
   1.167    (case thyinfo_of_sign sg of
   1.168 -    (_, ThyInfo {theory = Some thy, ...}) => thy
   1.169 +    (_, {theory = Some thy, ...}) => thy
   1.170    | _ => sys_error "theory_of_sign");
   1.171  
   1.172 +(*try to get the theory object corresponding to a given theorem*)
   1.173 +val theory_of_thm = theory_of_sign o #sign o rep_thm;
   1.174  
   1.175 -(*Try to get the theory object corresponding to a given theorem*)
   1.176 -val theory_of_thm = theory_of_sign o #sign o rep_thm;
   1.177 +(*get all direct descendants of a theory*)
   1.178 +fun children_of t =
   1.179 +  (case get_thyinfo t of
   1.180 +    Some ({children, ...}) => children
   1.181 +  | None => []);
   1.182 +
   1.183 +(*get all direct ancestors of a theory*)
   1.184 +fun parents_of_name t =
   1.185 +  (case get_thyinfo t of
   1.186 +    Some ({parents, ...}) => parents
   1.187 +  | None => []);
   1.188 +
   1.189 +(*get theory object for a loaded theory*)
   1.190 +fun theory_of name =
   1.191 +  (case get_thyinfo name of
   1.192 +    Some ({theory = Some t, ...}) => t
   1.193 +  | _ => err_not_stored name);
   1.194  
   1.195  
   1.196 -(*Get all direct descendants of a theory*)
   1.197 -fun children_of t =
   1.198 -  case get_thyinfo t of Some (ThyInfo {children, ...}) => children
   1.199 -                      | None => [];
   1.200 -
   1.201 -
   1.202 -(*Get all direct ancestors of a theory*)
   1.203 -fun parents_of_name t =
   1.204 -  case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
   1.205 -                      | None => [];
   1.206 -
   1.207 -
   1.208 -(*Get theory object for a loaded theory *)
   1.209 -fun theory_of name =
   1.210 -  case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
   1.211 -                         | _ => error ("Theory " ^ name ^
   1.212 -                                       " not stored by loader");
   1.213 -
   1.214 -
   1.215 -(*Invoke every put method stored in a theory's methods table to initialize
   1.216 +(*invoke every put method stored in a theory's methods table to initialize
   1.217    the state of user defined variables*)
   1.218  fun put_thydata first tname =
   1.219    let val (methods, data) = 
   1.220          case get_thyinfo tname of
   1.221 -            Some (ThyInfo {methods, data, ...}) => 
   1.222 +            Some ({methods, data, ...}) =>
   1.223                (methods, Symtab.dest ((if first then fst else snd) data))
   1.224 -          | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.225 +          | None => err_not_stored tname;
   1.226  
   1.227        fun put_data (id, date) =
   1.228              case Symtab.lookup (methods, id) of
   1.229 @@ -190,9 +161,9 @@
   1.230  (*Change theory object for an existent item of loaded_thys*)
   1.231  fun store_theory (thy, tname) =
   1.232    let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   1.233 -               Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
   1.234 +               Some ({path, children, parents, thy_time, ml_time, thms,
   1.235                                methods, data, ...}) =>
   1.236 -                 ThyInfo {path = path, children = children, parents = parents,
   1.237 +                 {path = path, children = children, parents = parents,
   1.238                            thy_time = thy_time, ml_time = ml_time,
   1.239                            theory = Some thy, thms = thms,
   1.240                            methods = methods, data = data}
   1.241 @@ -204,12 +175,9 @@
   1.242  
   1.243  (*Add data handling methods to theory*)
   1.244  fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
   1.245 -  let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
   1.246 -                   thms, methods, data} =
   1.247 -        case get_thyinfo tname of
   1.248 -            Some ti => ti
   1.249 -          | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.250 -  in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
   1.251 +  let val {path, children, parents, thy_time, ml_time, theory,
   1.252 +                   thms, methods, data} = the_thyinfo tname;
   1.253 +  in loaded_thys := Symtab.update ((tname, {path = path,
   1.254         children = children, parents = parents, thy_time = thy_time,
   1.255         ml_time = ml_time, theory = theory, thms = thms,
   1.256         methods = Symtab.update (new_methods, methods), data = data}),
   1.257 @@ -217,11 +185,9 @@
   1.258    end;
   1.259  
   1.260  
   1.261 -(*Retrieve data associated with theory*)
   1.262 -fun get_thydata tname id =
   1.263 -  let val d2 = case get_thyinfo tname of
   1.264 -                   Some (ThyInfo {data, ...}) => snd data
   1.265 -                 | None => error ("Theory " ^ tname ^ " not stored by loader");
   1.266 -  in Symtab.lookup (d2, id) end;
   1.267 +(*retrieve data associated with theory*)
   1.268 +fun get_thydata name id =
   1.269 +  Symtab.lookup (snd (#data (the_thyinfo name)), id);
   1.270 +
   1.271  
   1.272  end;