(*  Title:      Pure/Thy/thy_info.ML

    ID:         $Id$

    Author:     Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and

                Tobias Nipkow and L C Paulson

    Copyright   1994 TU Muenchen

Functions for storing and retrieving arbitrary theory information.

*)

(*Types for theory storage*)

(*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};

datatype thy_info =

  ThyInfo of {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};

      (*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 thyname_of_sign: Sign.sg -> string

  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

val loaded_thys =

  ref (Symtab.make [("ProtoPure",

                     ThyInfo {path = "",

                              children = ["Pure", "CPure"], parents = [],

                              thy_time = Some "", ml_time = Some "",

                              theory = Some proto_pure_thy,

                              thms = Symtab.null, methods = Symtab.null,

                              data = (Symtab.null, Symtab.null)}),

                    ("Pure",

                     ThyInfo {path = "", children = [],

                              parents = ["ProtoPure"],

                              thy_time = Some "", ml_time = Some "",

                              theory = Some pure_thy, thms = Symtab.null,

                              methods = Symtab.null,

                              data = (Symtab.null, Symtab.null)}),

                    ("CPure",

                     ThyInfo {path = "",

                              children = [], parents = ["ProtoPure"],

                              thy_time = Some "", ml_time = Some "",

                              theory = Some cpure_thy,

                              thms = Symtab.null,

                              methods = Symtab.null,

                              data = (Symtab.null, Symtab.null)})

                   ]);

(*Get thy_info for a loaded theory *)

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

(*Get path where theory's files are located*)

fun path_of tname =

  let val ThyInfo {path, ...} = the (get_thyinfo tname)

  in path end;

(*Guess the name of a theory object

  (First the quick way by looking at the stamps; if that doesn't work,

   we search loaded_thys for the first theory which fits.)

*)

fun thyname_of_sign sg =

  let val ref xname = hd (#stamps (Sign.rep_sg sg));

      val opt_info = get_thyinfo xname;

    fun eq_sg (ThyInfo {theory = None, ...}) = false

      | eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy);

    val show_sg = Pretty.str_of o Sign.pretty_sg;

  in

    if is_some opt_info andalso eq_sg (the opt_info) then xname

    else

      (case Symtab.find_first (eq_sg o snd) (!loaded_thys) of

        Some (name, _) => name

      | None => error ("Theory " ^ show_sg sg ^ " not stored by loader"))

  end;

(*Guess to which theory a signature belongs and return it's thy_info*)

fun thyinfo_of_sign sg =

  let val name = thyname_of_sign sg;

  in (name, the (get_thyinfo name)) end;

(*Try to get the theory object corresponding to a given signature*)

fun theory_of_sign sg =

  (case thyinfo_of_sign sg of

    (_, ThyInfo {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 (ThyInfo {children, ...}) => children

                      | None => [];

(*Get all direct ancestors of a theory*)

fun parents_of_name t =

  case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents

                      | None => [];

(*Get theory object for a loaded theory *)

fun theory_of name =

  case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t

                         | _ => error ("Theory " ^ name ^

                                       " not stored by loader");

(*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 (ThyInfo {methods, data, ...}) => 

              (methods, Symtab.dest ((if first then fst else snd) data))

          | None => error ("Theory " ^ tname ^ " not stored by loader");

      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 (ThyInfo {path, children, parents, thy_time, ml_time, thms,

                              methods, data, ...}) =>

                 ThyInfo {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 ThyInfo {path, children, parents, thy_time, ml_time, theory,

                   thms, methods, data} =

        case get_thyinfo tname of

            Some ti => ti

          | None => error ("Theory " ^ tname ^ " not stored by loader");

  in loaded_thys := Symtab.update ((tname, ThyInfo {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 tname id =

  let val d2 = case get_thyinfo tname of

                   Some (ThyInfo {data, ...}) => snd data

                 | None => error ("Theory " ^ tname ^ " not stored by loader");

  in Symtab.lookup (d2, id) end;

end;