src/Pure/Thy/thy_info.ML
author wenzelm
Tue, 28 Jul 1998 17:03:12 +0200
changeset 5209 a69fe5a61b6c
parent 4975 20b89fcd90a7
child 5211 c02b0c727780
permissions -rw-r--r--
theory_of renamed to theory (and made public);
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$
3976
wenzelm
parents: 3604
diff changeset
     3
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
     4
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
     5
Theory loader database.
3604
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
3976
wenzelm
parents: 3604
diff changeset
     8
type thy_info =
wenzelm
parents: 3604
diff changeset
     9
  {path: string,
wenzelm
parents: 3604
diff changeset
    10
    children: string list, parents: string list,
wenzelm
parents: 3604
diff changeset
    11
    thy_time: string option, ml_time: string option,
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    12
    theory: theory option};
3976
wenzelm
parents: 3604
diff changeset
    13
wenzelm
parents: 3604
diff changeset
    14
(*
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    15
  path: directory where theory's files are located
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    16
	(* FIXME do not store absolute path!!! *)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    17
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    18
  thy_time, ml_time = None     theory file has not been read yet
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    19
                    = Some ""  theory was read but has either been marked
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    20
                               as outdated or there is no such file for
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    21
                               this theory (see e.g. 'virtual' theories
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    22
                               like Pure or theories without a ML file)
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    23
  theory = None  theory has not been read yet
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    24
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    25
  parents: While 'children' contains all theories the theory depends
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    26
           on (i.e. also ones quoted in the .thy file),
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    27
           'parents' only contains the theories which were used to form
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    28
           the base of this theory.
3976
wenzelm
parents: 3604
diff changeset
    29
*)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    30
5209
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
    31
signature BASIC_THY_INFO =
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
    32
sig
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
    33
  val theory: string -> theory
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
    34
end
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
    35
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    36
signature THY_INFO =
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    37
sig
5209
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
    38
  include BASIC_THY_INFO
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    39
  val loaded_thys: thy_info Symtab.table ref
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    40
  val get_thyinfo: string -> thy_info option
4964
bbe9065edf8a tuned store_theory: theory -> unit;
wenzelm
parents: 4111
diff changeset
    41
  val store_theory: theory -> unit
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    42
  val path_of: string -> string
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    43
  val children_of: string -> string list
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    44
  val parents_of_name: string -> string list
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    45
  val thyinfo_of_sign: Sign.sg -> string * thy_info
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    46
  val theory_of_sign: Sign.sg -> theory
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    47
  val theory_of_thm: thm -> theory
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    48
end;
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
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    51
structure ThyInfo: THY_INFO =
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    52
struct
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    53
3976
wenzelm
parents: 3604
diff changeset
    54
(* loaded theories *)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    55
3976
wenzelm
parents: 3604
diff changeset
    56
fun mk_info (name, children, parents, theory) =
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    57
  (name, {path = "", children = children, parents = parents,
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
    58
    thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
3976
wenzelm
parents: 3604
diff changeset
    59
wenzelm
parents: 3604
diff changeset
    60
(*preloaded theories*)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    61
val loaded_thys =
3976
wenzelm
parents: 3604
diff changeset
    62
  ref (Symtab.make (map mk_info
3997
42062f636bdf ProtoPure.thy etc.;
wenzelm
parents: 3976
diff changeset
    63
    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
42062f636bdf ProtoPure.thy etc.;
wenzelm
parents: 3976
diff changeset
    64
     ("Pure", [], ["ProtoPure"], Pure.thy),
42062f636bdf ProtoPure.thy etc.;
wenzelm
parents: 3976
diff changeset
    65
     ("CPure", [], ["ProtoPure"], CPure.thy)]));
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    66
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    67
3976
wenzelm
parents: 3604
diff changeset
    68
(* retrieve info *)
wenzelm
parents: 3604
diff changeset
    69
wenzelm
parents: 3604
diff changeset
    70
fun err_not_stored name =
4975
20b89fcd90a7 tuned error msg;
wenzelm
parents: 4964
diff changeset
    71
  error ("Theory " ^ quote name ^ " not stored by loader");
3976
wenzelm
parents: 3604
diff changeset
    72
wenzelm
parents: 3604
diff changeset
    73
fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    74
3976
wenzelm
parents: 3604
diff changeset
    75
fun the_thyinfo name =
wenzelm
parents: 3604
diff changeset
    76
  (case get_thyinfo name of
wenzelm
parents: 3604
diff changeset
    77
    Some info => info
wenzelm
parents: 3604
diff changeset
    78
  | None => err_not_stored name);
wenzelm
parents: 3604
diff changeset
    79
wenzelm
parents: 3604
diff changeset
    80
fun thyinfo_of_sign sg =
wenzelm
parents: 3604
diff changeset
    81
  let val name = Sign.name_of sg
wenzelm
parents: 3604
diff changeset
    82
  in (name, the_thyinfo name) end;
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    83
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    84
3976
wenzelm
parents: 3604
diff changeset
    85
(*path where theory's files are located*)
wenzelm
parents: 3604
diff changeset
    86
val path_of = #path o the_thyinfo;
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    87
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    88
3976
wenzelm
parents: 3604
diff changeset
    89
(*try to get the theory object corresponding to a given signature*)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    90
fun theory_of_sign sg =
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    91
  (case thyinfo_of_sign sg of
3976
wenzelm
parents: 3604
diff changeset
    92
    (_, {theory = Some thy, ...}) => thy
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    93
  | _ => sys_error "theory_of_sign");
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    94
3976
wenzelm
parents: 3604
diff changeset
    95
(*try to get the theory object corresponding to a given theorem*)
wenzelm
parents: 3604
diff changeset
    96
val theory_of_thm = theory_of_sign o #sign o rep_thm;
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
    97
3976
wenzelm
parents: 3604
diff changeset
    98
(*get all direct descendants of a theory*)
wenzelm
parents: 3604
diff changeset
    99
fun children_of t =
wenzelm
parents: 3604
diff changeset
   100
  (case get_thyinfo t of
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   101
    Some {children, ...} => children
3976
wenzelm
parents: 3604
diff changeset
   102
  | None => []);
wenzelm
parents: 3604
diff changeset
   103
wenzelm
parents: 3604
diff changeset
   104
(*get all direct ancestors of a theory*)
wenzelm
parents: 3604
diff changeset
   105
fun parents_of_name t =
wenzelm
parents: 3604
diff changeset
   106
  (case get_thyinfo t of
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   107
    Some {parents, ...} => parents
3976
wenzelm
parents: 3604
diff changeset
   108
  | None => []);
wenzelm
parents: 3604
diff changeset
   109
wenzelm
parents: 3604
diff changeset
   110
(*get theory object for a loaded theory*)
5209
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
   111
fun theory name =
3976
wenzelm
parents: 3604
diff changeset
   112
  (case get_thyinfo name of
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   113
    Some {theory = Some t, ...} => t
3976
wenzelm
parents: 3604
diff changeset
   114
  | _ => err_not_stored name);
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   115
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   116
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   117
(* store_theory *)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   118
4964
bbe9065edf8a tuned store_theory: theory -> unit;
wenzelm
parents: 4111
diff changeset
   119
fun store_theory thy =
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   120
  let
4964
bbe9065edf8a tuned store_theory: theory -> unit;
wenzelm
parents: 4111
diff changeset
   121
    val name = PureThy.get_name thy;
4111
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   122
    val {path, children, parents, thy_time, ml_time, theory = _} =
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   123
      the_thyinfo name;
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   124
    val info = {path = path, children = children, parents = parents,
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   125
      thy_time = thy_time, ml_time = ml_time, theory = Some thy};
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   126
  in
93baba60ece2 removed old thy data stuff;
wenzelm
parents: 3997
diff changeset
   127
    loaded_thys := Symtab.update ((name, info), ! loaded_thys)
3604
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   128
  end;
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   129
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   130
6bf9f09f3d61 Moved functions for theory information storage / retrieval
berghofe
parents:
diff changeset
   131
end;
5209
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
   132
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
   133
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
   134
structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
a69fe5a61b6c theory_of renamed to theory (and made public);
wenzelm
parents: 4975
diff changeset
   135
open BasicThyInfo;