src/Pure/Thy/thy_info.ML
author wenzelm
Mon May 25 21:25:04 1998 +0200 (1998-05-25)
changeset 4964 bbe9065edf8a
parent 4111 93baba60ece2
child 4975 20b89fcd90a7
permissions -rw-r--r--
tuned store_theory: theory -> unit;
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
berghofe@3604
    31
signature THY_INFO =
berghofe@3604
    32
sig
wenzelm@4111
    33
  val loaded_thys: thy_info Symtab.table ref
wenzelm@4111
    34
  val get_thyinfo: string -> thy_info option
wenzelm@4964
    35
  val store_theory: theory -> unit
wenzelm@4111
    36
  val path_of: string -> string
wenzelm@4111
    37
  val children_of: string -> string list
berghofe@3604
    38
  val parents_of_name: string -> string list
berghofe@3604
    39
  val thyinfo_of_sign: Sign.sg -> string * thy_info
wenzelm@4111
    40
  val theory_of: string -> theory
wenzelm@4111
    41
  val theory_of_sign: Sign.sg -> theory
wenzelm@4111
    42
  val theory_of_thm: thm -> theory
berghofe@3604
    43
end;
berghofe@3604
    44
berghofe@3604
    45
berghofe@3604
    46
structure ThyInfo: THY_INFO =
berghofe@3604
    47
struct
berghofe@3604
    48
wenzelm@3976
    49
(* loaded theories *)
berghofe@3604
    50
wenzelm@3976
    51
fun mk_info (name, children, parents, theory) =
wenzelm@4111
    52
  (name, {path = "", children = children, parents = parents,
wenzelm@4111
    53
    thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
wenzelm@3976
    54
wenzelm@3976
    55
(*preloaded theories*)
berghofe@3604
    56
val loaded_thys =
wenzelm@3976
    57
  ref (Symtab.make (map mk_info
wenzelm@3997
    58
    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),
wenzelm@3997
    59
     ("Pure", [], ["ProtoPure"], Pure.thy),
wenzelm@3997
    60
     ("CPure", [], ["ProtoPure"], CPure.thy)]));
berghofe@3604
    61
berghofe@3604
    62
wenzelm@3976
    63
(* retrieve info *)
wenzelm@3976
    64
wenzelm@3976
    65
fun err_not_stored name =
wenzelm@3976
    66
  error ("Theory " ^ name ^ " not stored by loader");
wenzelm@3976
    67
wenzelm@3976
    68
fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
berghofe@3604
    69
wenzelm@3976
    70
fun the_thyinfo name =
wenzelm@3976
    71
  (case get_thyinfo name of
wenzelm@3976
    72
    Some info => info
wenzelm@3976
    73
  | None => err_not_stored name);
wenzelm@3976
    74
wenzelm@3976
    75
fun thyinfo_of_sign sg =
wenzelm@3976
    76
  let val name = Sign.name_of sg
wenzelm@3976
    77
  in (name, the_thyinfo name) end;
berghofe@3604
    78
berghofe@3604
    79
wenzelm@3976
    80
(*path where theory's files are located*)
wenzelm@3976
    81
val path_of = #path o the_thyinfo;
berghofe@3604
    82
berghofe@3604
    83
wenzelm@3976
    84
(*try to get the theory object corresponding to a given signature*)
berghofe@3604
    85
fun theory_of_sign sg =
berghofe@3604
    86
  (case thyinfo_of_sign sg of
wenzelm@3976
    87
    (_, {theory = Some thy, ...}) => thy
berghofe@3604
    88
  | _ => sys_error "theory_of_sign");
berghofe@3604
    89
wenzelm@3976
    90
(*try to get the theory object corresponding to a given theorem*)
wenzelm@3976
    91
val theory_of_thm = theory_of_sign o #sign o rep_thm;
berghofe@3604
    92
wenzelm@3976
    93
(*get all direct descendants of a theory*)
wenzelm@3976
    94
fun children_of t =
wenzelm@3976
    95
  (case get_thyinfo t of
wenzelm@4111
    96
    Some {children, ...} => children
wenzelm@3976
    97
  | None => []);
wenzelm@3976
    98
wenzelm@3976
    99
(*get all direct ancestors of a theory*)
wenzelm@3976
   100
fun parents_of_name t =
wenzelm@3976
   101
  (case get_thyinfo t of
wenzelm@4111
   102
    Some {parents, ...} => parents
wenzelm@3976
   103
  | None => []);
wenzelm@3976
   104
wenzelm@3976
   105
(*get theory object for a loaded theory*)
wenzelm@3976
   106
fun theory_of name =
wenzelm@3976
   107
  (case get_thyinfo name of
wenzelm@4111
   108
    Some {theory = Some t, ...} => t
wenzelm@3976
   109
  | _ => err_not_stored name);
berghofe@3604
   110
berghofe@3604
   111
wenzelm@4111
   112
(* store_theory *)
berghofe@3604
   113
wenzelm@4964
   114
fun store_theory thy =
wenzelm@4111
   115
  let
wenzelm@4964
   116
    val name = PureThy.get_name thy;
wenzelm@4111
   117
    val {path, children, parents, thy_time, ml_time, theory = _} =
wenzelm@4111
   118
      the_thyinfo name;
wenzelm@4111
   119
    val info = {path = path, children = children, parents = parents,
wenzelm@4111
   120
      thy_time = thy_time, ml_time = ml_time, theory = Some thy};
wenzelm@4111
   121
  in
wenzelm@4111
   122
    loaded_thys := Symtab.update ((name, info), ! loaded_thys)
berghofe@3604
   123
  end;
berghofe@3604
   124
berghofe@3604
   125
berghofe@3604
   126
end;