src/Pure/Thy/thy_info.ML
author wenzelm
Thu Oct 23 12:43:07 1997 +0200 (1997-10-23)
changeset 3976 1030dd79720b
parent 3604 6bf9f09f3d61
child 3997 42062f636bdf
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Thy/thy_info.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     4 
     5 Theory loader info database.
     6 *)
     7 
     8 (* FIXME wipe out! *)
     9 (*Functions to handle arbitrary data added by the user; type "exn" is used
    10   to store data*)
    11 datatype thy_methods =
    12   ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};
    13 
    14 
    15 type thy_info =
    16   {path: string,
    17     children: string list, parents: string list,
    18     thy_time: string option, ml_time: string option,
    19     theory: theory option, thms: thm Symtab.table,
    20     methods: thy_methods Symtab.table,
    21     data: exn Symtab.table * exn Symtab.table};
    22 
    23 (*
    24         path: directory where theory's files are located
    25 
    26         thy_time, ml_time = None     theory file has not been read yet
    27                           = Some ""  theory was read but has either been marked
    28                                      as outdated or there is no such file for
    29                                      this theory (see e.g. 'virtual' theories
    30                                      like Pure or theories without a ML file)
    31         theory = None  theory has not been read yet
    32 
    33         parents: While 'children' contains all theories the theory depends
    34                  on (i.e. also ones quoted in the .thy file),
    35                  'parents' only contains the theories which were used to form
    36                  the base of this theory.
    37 
    38         methods: three methods for each user defined data;
    39                  merge: merges data of ancestor theories
    40                  put: retrieves data from loaded_thys and stores it somewhere
    41                  get: retrieves data from somewhere and stores it
    42                       in loaded_thys
    43         data: user defined data; exn is used to allow arbitrary types;
    44               first element of pairs contains result that get returned after
    45               thy file was read, second element after ML file was read;
    46               if ML files has not been read, second element is identical to
    47               first one because get_thydata, which is meant to return the
    48               latest data, always accesses the 2nd element
    49 *)
    50 
    51 signature THY_INFO =
    52 sig
    53   val loaded_thys    : thy_info Symtab.table ref
    54   val store_theory   : theory * string -> unit
    55 
    56   val theory_of      : string -> theory
    57   val theory_of_sign : Sign.sg -> theory
    58   val theory_of_thm  : thm -> theory
    59   val children_of    : string -> string list
    60   val parents_of_name: string -> string list
    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 structure ThyInfo: THY_INFO =
    74 struct
    75 
    76 (* loaded theories *)
    77 
    78 fun mk_info (name, children, parents, theory) =
    79   (name,
    80     {path = "", children = children, parents = parents, thy_time = Some "",
    81       ml_time = Some "", theory = Some theory, thms = Symtab.null,
    82       methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info);
    83 
    84 (*preloaded theories*)
    85 val loaded_thys =
    86   ref (Symtab.make (map mk_info
    87     [("ProtoPure", ["Pure", "CPure"], [], Theory.proto_pure),
    88      ("Pure", [], ["ProtoPure"], Theory.pure),
    89      ("CPure", [], ["ProtoPure"], Theory.cpure)]));
    90 
    91 
    92 (* retrieve info *)
    93 
    94 fun err_not_stored name =
    95   error ("Theory " ^ name ^ " not stored by loader");
    96 
    97 fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
    98 
    99 fun the_thyinfo name =
   100   (case get_thyinfo name of
   101     Some info => info
   102   | None => err_not_stored name);
   103 
   104 fun thyinfo_of_sign sg =
   105   let val name = Sign.name_of sg
   106   in (name, the_thyinfo name) end;
   107 
   108 
   109 (*path where theory's files are located*)
   110 val path_of = #path o the_thyinfo;
   111 
   112 
   113 (*try to get the theory object corresponding to a given signature*)
   114 fun theory_of_sign sg =
   115   (case thyinfo_of_sign sg of
   116     (_, {theory = Some thy, ...}) => thy
   117   | _ => sys_error "theory_of_sign");
   118 
   119 (*try to get the theory object corresponding to a given theorem*)
   120 val theory_of_thm = theory_of_sign o #sign o rep_thm;
   121 
   122 (*get all direct descendants of a theory*)
   123 fun children_of t =
   124   (case get_thyinfo t of
   125     Some ({children, ...}) => children
   126   | None => []);
   127 
   128 (*get all direct ancestors of a theory*)
   129 fun parents_of_name t =
   130   (case get_thyinfo t of
   131     Some ({parents, ...}) => parents
   132   | None => []);
   133 
   134 (*get theory object for a loaded theory*)
   135 fun theory_of name =
   136   (case get_thyinfo name of
   137     Some ({theory = Some t, ...}) => t
   138   | _ => err_not_stored name);
   139 
   140 
   141 (*invoke every put method stored in a theory's methods table to initialize
   142   the state of user defined variables*)
   143 fun put_thydata first tname =
   144   let val (methods, data) = 
   145         case get_thyinfo tname of
   146             Some ({methods, data, ...}) =>
   147               (methods, Symtab.dest ((if first then fst else snd) data))
   148           | None => err_not_stored tname;
   149 
   150       fun put_data (id, date) =
   151             case Symtab.lookup (methods, id) of
   152                 Some (ThyMethods {put, ...}) => put date
   153               | None => error ("No method defined for theory data \"" ^
   154                                id ^ "\"");
   155   in seq put_data data end;
   156 
   157 
   158 val set_current_thy = put_thydata false;
   159 
   160 
   161 (*Change theory object for an existent item of loaded_thys*)
   162 fun store_theory (thy, tname) =
   163   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
   164                Some ({path, children, parents, thy_time, ml_time, thms,
   165                               methods, data, ...}) =>
   166                  {path = path, children = children, parents = parents,
   167                           thy_time = thy_time, ml_time = ml_time,
   168                           theory = Some thy, thms = thms,
   169                           methods = methods, data = data}
   170              | None => error ("store_theory: theory " ^ tname ^ " not found");
   171   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
   172 
   173 
   174 (*** Misc functions ***)
   175 
   176 (*Add data handling methods to theory*)
   177 fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
   178   let val {path, children, parents, thy_time, ml_time, theory,
   179                    thms, methods, data} = the_thyinfo tname;
   180   in loaded_thys := Symtab.update ((tname, {path = path,
   181        children = children, parents = parents, thy_time = thy_time,
   182        ml_time = ml_time, theory = theory, thms = thms,
   183        methods = Symtab.update (new_methods, methods), data = data}),
   184        !loaded_thys)
   185   end;
   186 
   187 
   188 (*retrieve data associated with theory*)
   189 fun get_thydata name id =
   190   Symtab.lookup (snd (#data (the_thyinfo name)), id);
   191 
   192 
   193 end;