src/Pure/Thy/thy_info.ML
author wenzelm
Wed Jul 29 15:38:08 1998 +0200 (1998-07-29)
changeset 5211 c02b0c727780
parent 5209 a69fe5a61b6c
child 6211 43d0efafa025
permissions -rw-r--r--
late setup of Pure and CPure;
     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 mk_info: string * string list * string list * theory -> string * thy_info
    40   val loaded_thys: thy_info Symtab.table ref
    41   val get_thyinfo: string -> thy_info option
    42   val store_theory: theory -> unit
    43   val path_of: string -> string
    44   val children_of: string -> string list
    45   val parents_of_name: string -> string list
    46   val thyinfo_of_sign: Sign.sg -> string * thy_info
    47   val theory_of_sign: Sign.sg -> theory
    48   val theory_of_thm: thm -> theory
    49 end;
    50 
    51 
    52 structure ThyInfo: THY_INFO =
    53 struct
    54 
    55 (* loaded theories *)
    56 
    57 fun mk_info (name, children, parents, theory) =
    58   (name, {path = "", children = children, parents = parents,
    59     thy_time = Some "", ml_time = Some "", theory = Some theory}: thy_info);
    60 
    61 (*preloaded theories*)
    62 val loaded_thys = ref (Symtab.empty: thy_info Symtab.table);
    63 
    64 
    65 (* retrieve info *)
    66 
    67 fun err_not_stored name =
    68   error ("Theory " ^ quote name ^ " not stored by loader");
    69 
    70 fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);
    71 
    72 fun the_thyinfo name =
    73   (case get_thyinfo name of
    74     Some info => info
    75   | None => err_not_stored name);
    76 
    77 fun thyinfo_of_sign sg =
    78   let val name = Sign.name_of sg
    79   in (name, the_thyinfo name) end;
    80 
    81 
    82 (*path where theory's files are located*)
    83 val path_of = #path o the_thyinfo;
    84 
    85 
    86 (*try to get the theory object corresponding to a given signature*)
    87 fun theory_of_sign sg =
    88   (case thyinfo_of_sign sg of
    89     (_, {theory = Some thy, ...}) => thy
    90   | _ => sys_error "theory_of_sign");
    91 
    92 (*try to get the theory object corresponding to a given theorem*)
    93 val theory_of_thm = theory_of_sign o #sign o rep_thm;
    94 
    95 (*get all direct descendants of a theory*)
    96 fun children_of t =
    97   (case get_thyinfo t of
    98     Some {children, ...} => children
    99   | None => []);
   100 
   101 (*get all direct ancestors of a theory*)
   102 fun parents_of_name t =
   103   (case get_thyinfo t of
   104     Some {parents, ...} => parents
   105   | None => []);
   106 
   107 (*get theory object for a loaded theory*)
   108 fun theory name =
   109   (case get_thyinfo name of
   110     Some {theory = Some t, ...} => t
   111   | _ => err_not_stored name);
   112 
   113 
   114 (* store_theory *)
   115 
   116 fun store_theory thy =
   117   let
   118     val name = PureThy.get_name thy;
   119     val {path, children, parents, thy_time, ml_time, theory = _} =
   120       the_thyinfo name;
   121     val info = {path = path, children = children, parents = parents,
   122       thy_time = thy_time, ml_time = ml_time, theory = Some thy};
   123   in
   124     loaded_thys := Symtab.update ((name, info), ! loaded_thys)
   125   end;
   126 
   127 
   128 end;
   129 
   130 
   131 structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
   132 open BasicThyInfo;