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

doc-src/IsarImplementation/Thy/Integration.thy

author | wenzelm |

Fri Aug 12 22:10:49 2011 +0200 (2011-08-12) | |

changeset 44163 | 32e0c150c010 |

parent 40149 | 4c35be108990 |

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

normalized theory dependencies wrt. file_store;

1 theory Integration

2 imports Base

3 begin

5 chapter {* System integration *}

7 section {* Isar toplevel \label{sec:isar-toplevel} *}

9 text {* The Isar toplevel may be considered the centeral hub of the

10 Isabelle/Isar system, where all key components and sub-systems are

11 integrated into a single read-eval-print loop of Isar commands,

12 which also incorporates the underlying ML compiler.

14 Isabelle/Isar departs from the original ``LCF system architecture''

15 where ML was really The Meta Language for defining theories and

16 conducting proofs. Instead, ML now only serves as the

17 implementation language for the system (and user extensions), while

18 the specific Isar toplevel supports the concepts of theory and proof

19 development natively. This includes the graph structure of theories

20 and the block structure of proofs, support for unlimited undo,

21 facilities for tracing, debugging, timing, profiling etc.

23 \medskip The toplevel maintains an implicit state, which is

24 transformed by a sequence of transitions -- either interactively or

25 in batch-mode. In interactive mode, Isar state transitions are

26 encapsulated as safe transactions, such that both failure and undo

27 are handled conveniently without destroying the underlying draft

28 theory (cf.~\secref{sec:context-theory}). In batch mode,

29 transitions operate in a linear (destructive) fashion, such that

30 error conditions abort the present attempt to construct a theory or

31 proof altogether.

33 The toplevel state is a disjoint sum of empty @{text toplevel}, or

34 @{text theory}, or @{text proof}. On entering the main Isar loop we

35 start with an empty toplevel. A theory is commenced by giving a

36 @{text \<THEORY>} header; within a theory we may issue theory

37 commands such as @{text \<DEFINITION>}, or state a @{text

38 \<THEOREM>} to be proven. Now we are within a proof state, with a

39 rich collection of Isar proof commands for structured proof

40 composition, or unstructured proof scripts. When the proof is

41 concluded we get back to the theory, which is then updated by

42 storing the resulting fact. Further theory declarations or theorem

43 statements with proofs may follow, until we eventually conclude the

44 theory development by issuing @{text \<END>}. The resulting theory

45 is then stored within the theory database and we are back to the

46 empty toplevel.

48 In addition to these proper state transformations, there are also

49 some diagnostic commands for peeking at the toplevel state without

50 modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},

51 \isakeyword{print-cases}).

52 *}

54 text %mlref {*

55 \begin{mldecls}

56 @{index_ML_type Toplevel.state} \\

57 @{index_ML Toplevel.UNDEF: "exn"} \\

58 @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\

59 @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\

60 @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\

61 @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\

62 @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\

63 @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\

64 \end{mldecls}

66 \begin{description}

68 \item Type @{ML_type Toplevel.state} represents Isar toplevel

69 states, which are normally manipulated through the concept of

70 toplevel transitions only (\secref{sec:toplevel-transition}). Also

71 note that a raw toplevel state is subject to the same linearity

72 restrictions as a theory context (cf.~\secref{sec:context-theory}).

74 \item @{ML Toplevel.UNDEF} is raised for undefined toplevel

75 operations. Many operations work only partially for certain cases,

76 since @{ML_type Toplevel.state} is a sum type.

78 \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty

79 toplevel state.

81 \item @{ML Toplevel.theory_of}~@{text "state"} selects the

82 background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}

83 for an empty toplevel state.

85 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof

86 state if available, otherwise raises @{ML Toplevel.UNDEF}.

88 \item @{ML "Toplevel.debug := true"} makes the toplevel print further

89 details about internal error conditions, exceptions being raised

90 etc.

92 \item @{ML "Toplevel.timing := true"} makes the toplevel print timing

93 information for each Isar command being executed.

95 \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls

96 low-level profiling of the underlying ML runtime system. For

97 Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space

98 profiling.

100 \end{description}

101 *}

103 text %mlantiq {*

104 \begin{matharray}{rcl}

105 @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\

106 \end{matharray}

108 \begin{description}

110 \item @{text "@{Isar.state}"} refers to Isar toplevel state at that

111 point --- as abstract value.

113 This only works for diagnostic ML commands, such as @{command

114 ML_val} or @{command ML_command}.

116 \end{description}

117 *}

120 subsection {* Toplevel transitions \label{sec:toplevel-transition} *}

122 text {*

123 An Isar toplevel transition consists of a partial function on the

124 toplevel state, with additional information for diagnostics and

125 error reporting: there are fields for command name, source position,

126 optional source text, as well as flags for interactive-only commands

127 (which issue a warning in batch-mode), printing of result state,

128 etc.

130 The operational part is represented as the sequential union of a

131 list of partial functions, which are tried in turn until the first

132 one succeeds. This acts like an outer case-expression for various

133 alternative state transitions. For example, \isakeyword{qed} works

134 differently for a local proofs vs.\ the global ending of the main

135 proof.

137 Toplevel transitions are composed via transition transformers.

138 Internally, Isar commands are put together from an empty transition

139 extended by name and source position. It is then left to the

140 individual command parser to turn the given concrete syntax into a

141 suitable transition transformer that adjoins actual operations on a

142 theory or proof state etc.

143 *}

145 text %mlref {*

146 \begin{mldecls}

147 @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\

148 @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\

149 @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->

150 Toplevel.transition -> Toplevel.transition"} \\

151 @{index_ML Toplevel.theory: "(theory -> theory) ->

152 Toplevel.transition -> Toplevel.transition"} \\

153 @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->

154 Toplevel.transition -> Toplevel.transition"} \\

155 @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->

156 Toplevel.transition -> Toplevel.transition"} \\

157 @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->

158 Toplevel.transition -> Toplevel.transition"} \\

159 @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->

160 Toplevel.transition -> Toplevel.transition"} \\

161 \end{mldecls}

163 \begin{description}

165 \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which

166 causes the toplevel loop to echo the result state (in interactive

167 mode).

169 \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the

170 transition should never show timing information, e.g.\ because it is

171 a diagnostic command.

173 \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic

174 function.

176 \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory

177 transformer.

179 \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global

180 goal function, which turns a theory into a proof state. The theory

181 may be changed before entering the proof; the generic Isar goal

182 setup includes an argument that specifies how to apply the proven

183 result to the theory, when the proof is finished.

185 \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic

186 proof command, with a singleton result.

188 \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof

189 command, with zero or more result states (represented as a lazy

190 list).

192 \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding

193 proof command, that returns the resulting theory, after storing the

194 resulting facts in the context etc.

196 \end{description}

197 *}

200 section {* Theory database \label{sec:theory-database} *}

202 text {*

203 The theory database maintains a collection of theories, together

204 with some administrative information about their original sources,

205 which are held in an external store (i.e.\ some directory within the

206 regular file system).

208 The theory database is organized as a directed acyclic graph;

209 entries are referenced by theory name. Although some additional

210 interfaces allow to include a directory specification as well, this

211 is only a hint to the underlying theory loader. The internal theory

212 name space is flat!

214 Theory @{text A} is associated with the main theory file @{text

215 A}\verb,.thy,, which needs to be accessible through the theory

216 loader path. Any number of additional ML source files may be

217 associated with each theory, by declaring these dependencies in the

218 theory header as @{text \<USES>}, and loading them consecutively

219 within the theory context. The system keeps track of incoming ML

220 sources and associates them with the current theory.

222 The basic internal actions of the theory database are @{text

223 "update"} and @{text "remove"}:

225 \begin{itemize}

227 \item @{text "update A"} introduces a link of @{text "A"} with a

228 @{text "theory"} value of the same name; it asserts that the theory

229 sources are now consistent with that value;

231 \item @{text "remove A"} deletes entry @{text "A"} from the theory

232 database.

234 \end{itemize}

236 These actions are propagated to sub- or super-graphs of a theory

237 entry as expected, in order to preserve global consistency of the

238 state of all loaded theories with the sources of the external store.

239 This implies certain causalities between actions: @{text "update"}

240 or @{text "remove"} of an entry will @{text "remove"} all

241 descendants.

243 \medskip There are separate user-level interfaces to operate on the

244 theory database directly or indirectly. The primitive actions then

245 just happen automatically while working with the system. In

246 particular, processing a theory header @{text "\<THEORY> A

247 \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the

248 sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}

249 is up-to-date, too. Earlier theories are reloaded as required, with

250 @{text update} actions proceeding in topological order according to

251 theory dependencies. There may be also a wave of implied @{text

252 remove} actions for derived theory nodes until a stable situation

253 is achieved eventually.

254 *}

256 text %mlref {*

257 \begin{mldecls}

258 @{index_ML use_thy: "string -> unit"} \\

259 @{index_ML use_thys: "string list -> unit"} \\

260 @{index_ML Thy_Info.get_theory: "string -> theory"} \\

261 @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]

262 @{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]

263 @{ML_text "datatype action = Update | Remove"} \\

264 @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\

265 \end{mldecls}

267 \begin{description}

269 \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully

270 up-to-date wrt.\ the external file store, reloading outdated

271 ancestors as required. In batch mode, the simultaneous @{ML

272 use_thys} should be used exclusively.

274 \item @{ML use_thys} is similar to @{ML use_thy}, but handles

275 several theories simultaneously. Thus it acts like processing the

276 import header of a theory, without performing the merge of the

277 result. By loading a whole sub-graph of theories like that, the

278 intrinsic parallelism can be exploited by the system, to speedup

279 loading.

281 \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value

282 presently associated with name @{text A}. Note that the result

283 might be outdated.

285 \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all

286 descendants from the theory database.

288 \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an

289 existing theory value with the theory loader database and updates

290 source version information according to the current file-system

291 state.

293 \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text

294 f} as a hook for theory database actions. The function will be

295 invoked with the action and theory name being involved; thus derived

296 actions may be performed in associated system components, e.g.\

297 maintaining the state of an editor for the theory sources.

299 The kind and order of actions occurring in practice depends both on

300 user interactions and the internal process of resolving theory

301 imports. Hooks should not rely on a particular policy here! Any

302 exceptions raised by the hook are ignored.

304 \end{description}

305 *}

307 end