summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/Thy/thy_info.ML

author | berghofe |

Wed Aug 06 00:26:19 1997 +0200 (1997-08-06) | |

changeset 3604 | 6bf9f09f3d61 |

child 3976 | 1030dd79720b |

permissions | -rw-r--r-- |

Moved functions for theory information storage / retrieval

from thy_read.ML to thy_info.ML .

from thy_read.ML to thy_info.ML .

1 (* Title: Pure/Thy/thy_info.ML

2 ID: $Id$

3 Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and

4 Tobias Nipkow and L C Paulson

5 Copyright 1994 TU Muenchen

7 Functions for storing and retrieving arbitrary theory information.

8 *)

10 (*Types for theory storage*)

12 (*Functions to handle arbitrary data added by the user; type "exn" is used

13 to store data*)

14 datatype thy_methods =

15 ThyMethods of {merge: exn list -> exn, put: exn -> unit, get: unit -> exn};

17 datatype thy_info =

18 ThyInfo of {path: string,

19 children: string list, parents: string list,

20 thy_time: string option, ml_time: string option,

21 theory: theory option, thms: thm Symtab.table,

22 methods: thy_methods Symtab.table,

23 data: exn Symtab.table * exn Symtab.table};

24 (*thy_time, ml_time = None theory file has not been read yet

25 = Some "" theory was read but has either been marked

26 as outdated or there is no such file for

27 this theory (see e.g. 'virtual' theories

28 like Pure or theories without a ML file)

29 theory = None theory has not been read yet

31 parents: While 'children' contains all theories the theory depends

32 on (i.e. also ones quoted in the .thy file),

33 'parents' only contains the theories which were used to form

34 the base of this theory.

36 methods: three methods for each user defined data;

37 merge: merges data of ancestor theories

38 put: retrieves data from loaded_thys and stores it somewhere

39 get: retrieves data from somewhere and stores it

40 in loaded_thys

41 data: user defined data; exn is used to allow arbitrary types;

42 first element of pairs contains result that get returned after

43 thy file was read, second element after ML file was read;

44 if ML files has not been read, second element is identical to

45 first one because get_thydata, which is meant to return the

46 latest data, always accesses the 2nd element

47 *)

50 signature THY_INFO =

51 sig

52 val loaded_thys : thy_info Symtab.table ref

53 val store_theory : theory * string -> unit

55 val theory_of : string -> theory

56 val theory_of_sign : Sign.sg -> theory

57 val theory_of_thm : thm -> theory

58 val children_of : string -> string list

59 val parents_of_name: string -> string list

60 val thyname_of_sign: Sign.sg -> string

61 val thyinfo_of_sign: Sign.sg -> string * thy_info

63 val add_thydata : string -> string * thy_methods -> unit

64 val get_thydata : string -> string -> exn option

65 val put_thydata : bool -> string -> unit

66 val set_current_thy: string -> unit

67 val get_thyinfo : string -> thy_info option

69 val path_of : string -> string

70 end;

74 structure ThyInfo: THY_INFO =

75 struct

78 val loaded_thys =

79 ref (Symtab.make [("ProtoPure",

80 ThyInfo {path = "",

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

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

83 theory = Some proto_pure_thy,

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

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

86 ("Pure",

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

88 parents = ["ProtoPure"],

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

90 theory = Some pure_thy, thms = Symtab.null,

91 methods = Symtab.null,

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

93 ("CPure",

94 ThyInfo {path = "",

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

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

97 theory = Some cpure_thy,

98 thms = Symtab.null,

99 methods = Symtab.null,

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

101 ]);

104 (*Get thy_info for a loaded theory *)

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

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

108 fun path_of tname =

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

110 in path end;

113 (*Guess the name of a theory object

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

115 we search loaded_thys for the first theory which fits.)

116 *)

117 fun thyname_of_sign sg =

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

119 val opt_info = get_thyinfo xname;

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

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

124 val show_sg = Pretty.str_of o Sign.pretty_sg;

125 in

126 if is_some opt_info andalso eq_sg (the opt_info) then xname

127 else

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

129 Some (name, _) => name

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

131 end;

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

135 fun thyinfo_of_sign sg =

136 let val name = thyname_of_sign sg;

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

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

141 fun theory_of_sign sg =

142 (case thyinfo_of_sign sg of

143 (_, ThyInfo {theory = Some thy, ...}) => thy

144 | _ => sys_error "theory_of_sign");

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

148 val theory_of_thm = theory_of_sign o #sign o rep_thm;

151 (*Get all direct descendants of a theory*)

152 fun children_of t =

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

154 | None => [];

157 (*Get all direct ancestors of a theory*)

158 fun parents_of_name t =

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

160 | None => [];

163 (*Get theory object for a loaded theory *)

164 fun theory_of name =

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

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

167 " not stored by loader");

170 (*Invoke every put method stored in a theory's methods table to initialize

171 the state of user defined variables*)

172 fun put_thydata first tname =

173 let val (methods, data) =

174 case get_thyinfo tname of

175 Some (ThyInfo {methods, data, ...}) =>

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

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

179 fun put_data (id, date) =

180 case Symtab.lookup (methods, id) of

181 Some (ThyMethods {put, ...}) => put date

182 | None => error ("No method defined for theory data \"" ^

183 id ^ "\"");

184 in seq put_data data end;

187 val set_current_thy = put_thydata false;

190 (*Change theory object for an existent item of loaded_thys*)

191 fun store_theory (thy, tname) =

192 let val tinfo = case Symtab.lookup (!loaded_thys, tname) of

193 Some (ThyInfo {path, children, parents, thy_time, ml_time, thms,

194 methods, data, ...}) =>

195 ThyInfo {path = path, children = children, parents = parents,

196 thy_time = thy_time, ml_time = ml_time,

197 theory = Some thy, thms = thms,

198 methods = methods, data = data}

199 | None => error ("store_theory: theory " ^ tname ^ " not found");

200 in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;

203 (*** Misc functions ***)

205 (*Add data handling methods to theory*)

206 fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) =

207 let val ThyInfo {path, children, parents, thy_time, ml_time, theory,

208 thms, methods, data} =

209 case get_thyinfo tname of

210 Some ti => ti

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

212 in loaded_thys := Symtab.update ((tname, ThyInfo {path = path,

213 children = children, parents = parents, thy_time = thy_time,

214 ml_time = ml_time, theory = theory, thms = thms,

215 methods = Symtab.update (new_methods, methods), data = data}),

216 !loaded_thys)

217 end;

220 (*Retrieve data associated with theory*)

221 fun get_thydata tname id =

222 let val d2 = case get_thyinfo tname of

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

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

225 in Symtab.lookup (d2, id) end;

227 end;