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