|
61
|
1 |
theory StoringData
|
|
|
2 |
imports "../Base"
|
|
|
3 |
begin
|
|
|
4 |
|
211
d5accbc67e1b
more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
5 |
section {* Storing Data (TBD)\label{rec:storingdata} *}
|
|
61
|
6 |
|
|
|
7 |
|
|
|
8 |
text {*
|
|
|
9 |
{\bf Problem:}
|
|
68
|
10 |
Your tool needs to manage data.\smallskip
|
|
61
|
11 |
|
|
|
12 |
{\bf Solution:} This can be achieved using a generic data slot.\smallskip
|
|
|
13 |
|
|
|
14 |
Every generic data slot may keep data of any kind which is stored in the
|
|
|
15 |
context.
|
|
|
16 |
|
|
|
17 |
*}
|
|
|
18 |
|
|
69
|
19 |
ML{*local
|
|
61
|
20 |
|
|
|
21 |
structure Data = GenericDataFun
|
|
68
|
22 |
( type T = int Symtab.table
|
|
|
23 |
val empty = Symtab.empty
|
|
|
24 |
val extend = I
|
|
|
25 |
fun merge _ = Symtab.merge (K true)
|
|
|
26 |
)
|
|
61
|
27 |
|
|
|
28 |
in
|
|
69
|
29 |
val lookup = Symtab.lookup o Data.get
|
|
|
30 |
fun update k v = Data.map (Symtab.update (k, v))
|
|
63
|
31 |
end *}
|
|
61
|
32 |
|
|
|
33 |
setup {* Context.theory_map (update "foo" 1) *}
|
|
|
34 |
|
|
68
|
35 |
text {*
|
|
|
36 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
@{ML_response [display,gray] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"}
|
|
68
|
38 |
|
|
|
39 |
|
|
|
40 |
*}
|
|
61
|
41 |
|
|
|
42 |
text {*
|
|
|
43 |
alternatives: TheoryDataFun, ProofDataFun
|
|
|
44 |
Code: Pure/context.ML *}
|
|
|
45 |
|
|
|
46 |
end |