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