src/Pure/Thy/thy_info.ML

tuned;

(*  Title:      Pure/Thy/thy_info.ML
    ID:         $Id$
    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen

Theory loader info database.
*)

(* FIXME wipe out! *)
(*Functions to handle arbitrary data added by the user; type "exn" is used
  to store data*)
datatype thy_methods =
  ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};


type thy_info =
  {path: string,
    children: string list, parents: string list,
    thy_time: string option, ml_time: string option,
    theory: theory option, thms: thm Symtab.table,
    methods: thy_methods Symtab.table,
    data: exn Symtab.table * exn Symtab.table};

(*
        path: directory where theory's files are located

        thy_time, ml_time = None     theory file has not been read yet
                          = Some ""  theory was read but has either been marked
                                     as outdated or there is no such file for
                                     this theory (see e.g. 'virtual' theories
                                     like Pure or theories without a ML file)
        theory = None  theory has not been read yet

        parents: While 'children' contains all theories the theory depends
                 on (i.e. also ones quoted in the .thy file),
                 'parents' only contains the theories which were used to form
                 the base of this theory.

        methods: three methods for each user defined data;
                 merge: merges data of ancestor theories
                 put: retrieves data from loaded_thys and stores it somewhere
                 get: retrieves data from somewhere and stores it
                      in loaded_thys
        data: user defined data; exn is used to allow arbitrary types;
              first element of pairs contains result that get returned after
              thy file was read, second element after ML file was read;
              if ML files has not been read, second element is identical to
              first one because get_thydata, which is meant to return the
              latest data, always accesses the 2nd element
*)

signature THY_INFO =
sig
  val loaded_thys    : thy_info Symtab.table ref
  val store_theory   : theory * string -> unit

  val theory_of      : string -> theory
  val theory_of_sign : Sign.sg -> theory
  val theory_of_thm  : thm -> theory
  val children_of    : string -> string list
  val parents_of_name: string -> string list
  val thyinfo_of_sign: Sign.sg -> string * thy_info

  val add_thydata    : string -> string * thy_methods -> unit
  val get_thydata    : string -> string -> exn option
  val put_thydata    : bool -> string -> unit
  val set_current_thy: string -> unit
  val get_thyinfo    : string -> thy_info option

  val path_of        : string -> string
end;


structure ThyInfo: THY_INFO =
struct

(* loaded theories *)

fun mk_info (name, children, parents, theory) =
  (name,
    {path = "", children = children, parents = parents, thy_time = Some "",
      ml_time = Some "", theory = Some theory, thms = Symtab.null,
      methods = Symtab.null, data = (Symtab.null, Symtab.null)}: thy_info);

(*preloaded theories*)
val loaded_thys =
  ref (Symtab.make (map mk_info
    [("ProtoPure", ["Pure", "CPure"], [], Theory.proto_pure),
     ("Pure", [], ["ProtoPure"], Theory.pure),
     ("CPure", [], ["ProtoPure"], Theory.cpure)]));


(* retrieve info *)

fun err_not_stored name =
  error ("Theory " ^ name ^ " not stored by loader");

fun get_thyinfo name = Symtab.lookup (! loaded_thys, name);

fun the_thyinfo name =
  (case get_thyinfo name of
    Some info => info
  | None => err_not_stored name);

fun thyinfo_of_sign sg =
  let val name = Sign.name_of sg
  in (name, the_thyinfo name) end;


(*path where theory's files are located*)
val path_of = #path o the_thyinfo;


(*try to get the theory object corresponding to a given signature*)
fun theory_of_sign sg =
  (case thyinfo_of_sign sg of
    (_, {theory = Some thy, ...}) => thy
  | _ => sys_error "theory_of_sign");

(*try to get the theory object corresponding to a given theorem*)
val theory_of_thm = theory_of_sign o #sign o rep_thm;

(*get all direct descendants of a theory*)
fun children_of t =
  (case get_thyinfo t of
    Some ({children, ...}) => children
  | None => []);

(*get all direct ancestors of a theory*)
fun parents_of_name t =
  (case get_thyinfo t of
    Some ({parents, ...}) => parents
  | None => []);

(*get theory object for a loaded theory*)
fun theory_of name =
  (case get_thyinfo name of
    Some ({theory = Some t, ...}) => t
  | _ => err_not_stored name);


(*invoke every put method stored in a theory's methods table to initialize
  the state of user defined variables*)
fun put_thydata first tname =
  let val (methods, data) = 
        case get_thyinfo tname of
            Some ({methods, data, ...}) =>
              (methods, Symtab.dest ((if first then fst else snd) data))
          | None => err_not_stored tname;

      fun put_data (id, date) =
            case Symtab.lookup (methods, id) of
                Some (ThyMethods {put, ...}) => put date
              | None => error ("No method defined for theory data \"" ^
                               id ^ "\"");
  in seq put_data data end;


val set_current_thy = put_thydata false;


(*Change theory object for an existent item of loaded_thys*)
fun store_theory (thy, tname) =
  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
               Some ({path, children, parents, thy_time, ml_time, thms,
                              methods, data, ...}) =>
                 {path = path, children = children, parents = parents,
                          thy_time = thy_time, ml_time = ml_time,
                          theory = Some thy, thms = thms,
                          methods = methods, data = data}
             | None => error ("store_theory: theory " ^ tname ^ " not found");
  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;


(*** Misc functions ***)

(*Add data handling methods to theory*)
fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =
  let val {path, children, parents, thy_time, ml_time, theory,
                   thms, methods, data} = the_thyinfo tname;
  in loaded_thys := Symtab.update ((tname, {path = path,
       children = children, parents = parents, thy_time = thy_time,
       ml_time = ml_time, theory = theory, thms = thms,
       methods = Symtab.update (new_methods, methods), data = data}),
       !loaded_thys)
  end;


(*retrieve data associated with theory*)
fun get_thydata name id =
  Symtab.lookup (snd (#data (the_thyinfo name)), id);


end;