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