199 text {* |
199 text {* |
200 Contexts are arguably more important than theories, even though they only |
200 Contexts are arguably more important than theories, even though they only |
201 contain ``short-term memory data''. The reason is that a vast number of |
201 contain ``short-term memory data''. The reason is that a vast number of |
202 functions in Isabelle depend in one way or another on contexts. Even such |
202 functions in Isabelle depend in one way or another on contexts. Even such |
203 mundane operations like printing out a term make essential use of contexts. |
203 mundane operations like printing out a term make essential use of contexts. |
204 For this consider the following contrived proof-snippet whose only purpose is to |
204 For this consider the following contrived proof-snippet whose purpose is to |
205 fix two variables: |
205 fix two variables: |
206 *} |
206 *} |
207 |
207 |
208 lemma "True" |
208 lemma "True" |
209 proof - |
209 proof - |
216 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
216 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
217 |
217 |
218 text {* |
218 text {* |
219 The interesting point in this proof is that we injected ML-code before and after |
219 The interesting point in this proof is that we injected ML-code before and after |
220 the variables are fixed. For this remember that ML-code inside a proof |
220 the variables are fixed. For this remember that ML-code inside a proof |
221 needs to be enclosed in \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"}, |
221 needs to be enclosed inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"}, |
222 not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function |
222 not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function |
223 @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes |
223 @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes |
224 a context and returns all its currently fixed variable (names). That |
224 a context and returns all its currently fixed variable (names). That |
225 means a context has a dataslot containing information about fixed variables. |
225 means a context has a dataslot containing information about fixed variables. |
226 The ML-antiquotation @{text "@{context}"} points to the context that is |
226 The ML-antiquotation @{text "@{context}"} points to the context that is |
227 active at that point of the theory. Consequently, in the first call to |
227 active at that point of the theory. Consequently, in the first call to |
228 @{ML dest_fixes in Variable} this dataslot is empty; in the second it is |
228 @{ML dest_fixes in Variable} this dataslot is empty; in the second it is |
229 filled with @{text x} and @{text y}. What is interesting is that contexts |
229 filled with @{text x} and @{text y}. What is interesting is that contexts |
230 can be stacked. For this consider the following proof fragment |
230 can be stacked. For this consider the following proof fragment: |
231 *} |
231 *} |
232 |
232 |
233 lemma "True" |
233 lemma "True" |
234 proof - |
234 proof - |
235 fix x y |
235 fix x y |
252 ML{*val ctxt0 = @{context}; |
252 ML{*val ctxt0 = @{context}; |
253 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
253 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
254 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
254 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
255 |
255 |
256 text {* |
256 text {* |
257 Now let us come back to the point about printing terms. |
257 where the function @{ML_ind add_fixes in Variable} fixes a list of variables |
|
258 specified by strings. Let us come back to the point about printing terms. Consider |
|
259 printing out the term @{text "(x, y, z, w)"} using the function @{ML_ind pretty_term}. |
|
260 This function takes a term and a context as argument. |
258 *} |
261 *} |
259 |
262 |
260 ML {* |
263 ML {* |
261 let |
264 let |
262 val trm = @{term "x y z w"} |
265 val trm = @{term "(x, y, z, w)"} |
263 in |
266 in |
264 pwriteln (Pretty.chunks |
267 pwriteln (Pretty.chunks |
265 [ pretty_term ctxt0 trm, |
268 [ pretty_term ctxt0 trm, |
266 pretty_term ctxt1 trm, |
269 pretty_term ctxt1 trm, |
267 pretty_term ctxt2 trm ]) |
270 pretty_term ctxt2 trm ]) |
268 end |
271 end |
269 *} |
272 *} |
270 |
273 |
271 |
274 |
272 text {* |
275 text {* |
273 |
276 The term we are printing is in all three cases the same---a tuple containing four |
|
277 free variables. As you can see in case of @{ML "ctxt0"}, however, all variables are highlighted |
|
278 indicating a problem, while in case of @{ML "ctxt1"} @{text x} and @{text y} are printed |
|
279 as normal (blue) free variables, but not @{text z} and @{text w}. In the last case all |
|
280 variables are printed as expected. The point is that the context contains the information |
|
281 which variables are fixed, and designates all other free variables as being alien or faulty. |
|
282 While this seems like a minor feat, the concept of making the context aware of |
|
283 fixed variables is actually quite useful. For example it prevents us from fixing a |
|
284 variable twice |
|
285 |
|
286 @{ML_response_fake [gray, display] |
|
287 "@{context} |
|
288 |> Variable.add_fixes [\"x\", \"y\"] |
|
289 ||>> Variable.add_fixes [\"x\", \"y\"]" |
|
290 "Duplicate fixed variable(s): \"x\""} |
274 *} |
291 *} |
275 |
292 |
276 |
293 |
277 (* |
294 (* |
278 ML{*Proof_Context.debug := true*} |
295 ML{*Proof_Context.debug := true*} |