(*  Title:      Pure/Thy/thy_info.ML

    ID:         $Id$

    Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen

Theory loader database.

*)

type thy_info =

  {path: string,

    children: string list, parents: string list,

    thy_time: string option, ml_time: string option,

    theory: theory option};

(*

  path: directory where theory's files are located

	(* FIXME do not store absolute path!!! *)

  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.

*)

signature BASIC_THY_INFO =

sig

  val theory: string -> theory

end

signature THY_INFO =

sig

  include BASIC_THY_INFO

  val loaded_thys: thy_info Symtab.table ref

  val get_thyinfo: string -> thy_info option

  val store_theory: theory -> unit

  val path_of: string -> string

  val children_of: string -> string list

  val parents_of_name: string -> string list

  val thyinfo_of_sign: Sign.sg -> string * thy_info

  val theory_of_sign: Sign.sg -> theory

  val theory_of_thm: thm -> theory

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}: thy_info);

(*preloaded theories*)

val loaded_thys =

  ref (Symtab.make (map mk_info

    [("ProtoPure", ["Pure", "CPure"], [], ProtoPure.thy),

     ("Pure", [], ["ProtoPure"], Pure.thy),

     ("CPure", [], ["ProtoPure"], CPure.thy)]));

(* retrieve info *)

fun err_not_stored name =

  error ("Theory " ^ quote 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 name =

  (case get_thyinfo name of

    Some {theory = Some t, ...} => t

  | _ => err_not_stored name);

(* store_theory *)

fun store_theory thy =

  let

    val name = PureThy.get_name thy;

    val {path, children, parents, thy_time, ml_time, theory = _} =

      the_thyinfo name;

    val info = {path = path, children = children, parents = parents,

      thy_time = thy_time, ml_time = ml_time, theory = Some thy};

  in

    loaded_thys := Symtab.update ((name, info), ! loaded_thys)

  end;

end;

structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;

open BasicThyInfo;