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