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