src/Pure/Thy/thy_info.ML
author berghofe
Wed Aug 06 00:26:19 1997 +0200 (1997-08-06)
changeset 3604 6bf9f09f3d61
child 3976 1030dd79720b
permissions -rw-r--r--
Moved functions for theory information storage / retrieval
from thy_read.ML to thy_info.ML .
     1 (*  Title:      Pure/Thy/thy_info.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and
     4                 Tobias Nipkow and L C Paulson
     5     Copyright   1994 TU Muenchen
     6 
     7 Functions for storing and retrieving arbitrary theory information.
     8 *)
     9 
    10 (*Types for theory storage*)
    11 
    12 (*Functions to handle arbitrary data added by the user; type "exn" is used
    13   to store data*)
    14 datatype thy_methods =
    15   ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    16 
    17 datatype thy_info =
    18   ThyInfo of {path: string,
    19               children: string list, parents: string list,
    20               thy_time: string option, ml_time: string option,
    21               theory: theory option, thms: thm Symtab.table,
    22               methods: thy_methods Symtab.table,
    23               data: exn Symtab.table * exn Symtab.table};
    24       (*thy_time, ml_time = None     theory file has not been read yet
    25                           = Some ""  theory was read but has either been marked
    26                                      as outdated or there is no such file for
    27                                      this theory (see e.g. 'virtual' theories
    28                                      like Pure or theories without a ML file)
    29         theory = None  theory has not been read yet
    30 
    31         parents: While 'children' contains all theories the theory depends
    32                  on (i.e. also ones quoted in the .thy file),
    33                  'parents' only contains the theories which were used to form
    34                  the base of this theory.
    35 
    36         methods: three methods for each user defined data;
    37                  merge: merges data of ancestor theories
    38                  put: retrieves data from loaded_thys and stores it somewhere
    39                  get: retrieves data from somewhere and stores it
    40                       in loaded_thys
    41         data: user defined data; exn is used to allow arbitrary types;
    42               first element of pairs contains result that get returned after
    43               thy file was read, second element after ML file was read;
    44               if ML files has not been read, second element is identical to
    45               first one because get_thydata, which is meant to return the
    46               latest data, always accesses the 2nd element
    47        *)
    48 
    49 
    50 signature THY_INFO =
    51 sig
    52   val loaded_thys    : thy_info Symtab.table ref
    53   val store_theory   : theory * string -> unit
    54 
    55   val theory_of      : string -> theory
    56   val theory_of_sign : Sign.sg -> theory
    57   val theory_of_thm  : thm -> theory
    58   val children_of    : string -> string list
    59   val parents_of_name: string -> string list
    60   val thyname_of_sign: Sign.sg -> string
    61   val thyinfo_of_sign: Sign.sg -> string * thy_info
    62 
    63   val add_thydata    : string -> string * thy_methods -> unit
    64   val get_thydata    : string -> string -> exn option
    65   val put_thydata    : bool -> string -> unit
    66   val set_current_thy: string -> unit
    67   val get_thyinfo    : string -> thy_info option
    68 
    69   val path_of        : string -> string
    70 end;
    71 
    72 
    73 
    74 structure ThyInfo: THY_INFO =
    75 struct
    76 
    77 
    78 val loaded_thys =
    79   ref (Symtab.make [("ProtoPure",
    80                      ThyInfo {path = "",
    81                               children = ["Pure", "CPure"], parents = [],
    82                               thy_time = Some "", ml_time = Some "",
    83                               theory = Some proto_pure_thy,
    84                               thms = Symtab.null, methods = Symtab.null,
    85                               data = (Symtab.null, Symtab.null)}),
    86                     ("Pure",
    87                      ThyInfo {path = "", children = [],
    88                               parents = ["ProtoPure"],
    89                               thy_time = Some "", ml_time = Some "",
    90                               theory = Some pure_thy, thms = Symtab.null,
    91                               methods = Symtab.null,
    92                               data = (Symtab.null, Symtab.null)}),
    93                     ("CPure",
    94                      ThyInfo {path = "",
    95                               children = [], parents = ["ProtoPure"],
    96                               thy_time = Some "", ml_time = Some "",
    97                               theory = Some cpure_thy,
    98                               thms = Symtab.null,
    99                               methods = Symtab.null,
   100                               data = (Symtab.null, Symtab.null)})
   101                    ]);
   102 
   103 
   104 (*Get thy_info for a loaded theory *)
   105 fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname);
   106 
   107 (*Get path where theory's files are located*)
   108 fun path_of tname =
   109   let val ThyInfo {path, ...} = the (get_thyinfo tname)
   110   in path end;
   111 
   112 
   113 (*Guess the name of a theory object
   114   (First the quick way by looking at the stamps; if that doesn't work,
   115    we search loaded_thys for the first theory which fits.)
   116 *)
   117 fun thyname_of_sign sg =
   118   let val ref xname = hd (#stamps (Sign.rep_sg sg));
   119       val opt_info = get_thyinfo xname;
   120 
   121     fun eq_sg (ThyInfo {theory = None, ...}) = false
   122       | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);
   123 
   124     val show_sg = Pretty.str_of o Sign.pretty_sg;
   125   in
   126     if is_some opt_info andalso eq_sg (the opt_info) then xname
   127     else
   128       (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of
   129         Some (name, _) => name
   130       | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))
   131   end;
   132 
   133 
   134 (*Guess to which theory a signature belongs and return it's thy_info*)
   135 fun thyinfo_of_sign sg =
   136   let val name = thyname_of_sign sg;
   137   in (name, the (get_thyinfo name)) end;
   138 
   139 
   140 (*Try to get the theory object corresponding to a given signature*)
   141 fun theory_of_sign sg =
   142   (case thyinfo_of_sign sg of
   143     (_, ThyInfo {theory = Some thy, ...}) => thy
   144   | _ => sys_error "theory_of_sign");
   145 
   146 
   147 (*Try to get the theory object corresponding to a given theorem*)
   148 val theory_of_thm = theory_of_sign o #sign o rep_thm;
   149 
   150 
   151 (*Get all direct descendants of a theory*)
   152 fun children_of t =
   153   case get_thyinfo t of Some (ThyInfo {children, ...}) => children
   154                       | None => [];
   155 
   156 
   157 (*Get all direct ancestors of a theory*)
   158 fun parents_of_name t =
   159   case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents
   160                       | None => [];
   161 
   162 
   163 (*Get theory object for a loaded theory *)
   164 fun theory_of name =
   165   case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t
   166                          | _ => error ("Theory " ^ name ^
   167                                        " not stored by loader");
   168 
   169 
   170 (*Invoke every put method stored in a theory's methods table to initialize
   171   the state of user defined variables*)
   172 fun put_thydata first tname =
   173   let val (methods, data) = 
   174         case get_thyinfo tname of
   175             Some (ThyInfo {methods, data, ...}) => 
   176               (methods, Symtab.dest ((if first then fst else snd) data))
   177           | None => error ("Theory " ^ tname ^ " not stored by loader");
   178 
   179       fun put_data (id, date) =
   180             case Symtab.lookup (methods, id) of
   181                 Some (ThyMethods {put, ...}) => put date
   182               | None => error ("No method defined for theory data \"" ^
   183                                id ^ "\"");
   184   in seq put_data data end;
   185 
   186 
   187 val set_current_thy = put_thydata false;
   188 
   189 
   190 (*Change theory object for an existent item of loaded_thys*)
   191 fun store_theory (thy, tname) =
   192   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   193                Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,
   194                               methods, data, ...}) =>
   195                  ThyInfo {path = path, children = children, parents = parents,
   196                           thy_time = thy_time, ml_time = ml_time,
   197                           theory = Some thy, thms = thms,
   198                           methods = methods, data = data}
   199              | None => error ("store_theory: theory " ^ tname ^ " not found");
   200   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   201 
   202 
   203 (*** Misc functions ***)
   204 
   205 (*Add data handling methods to theory*)
   206 fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
   207   let val ThyInfo {path, children, parents, thy_time, ml_time, theory,
   208                    thms, methods, data} =
   209         case get_thyinfo tname of
   210             Some ti => ti
   211           | None => error ("Theory " ^ tname ^ " not stored by loader");
   212   in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,
   213        children = children, parents = parents, thy_time = thy_time,
   214        ml_time = ml_time, theory = theory, thms = thms,
   215        methods = Symtab.update (new_methods, methods), data = data}),
   216        !loaded_thys)
   217   end;
   218 
   219 
   220 (*Retrieve data associated with theory*)
   221 fun get_thydata tname id =
   222   let val d2 = case get_thyinfo tname of
   223                    Some (ThyInfo {data, ...}) => snd data
   224                  | None => error ("Theory " ^ tname ^ " not stored by loader");
   225   in Symtab.lookup (d2, id) end;
   226 
   227 end;