|
25
|
1 |
theory Data_slot
|
|
|
2 |
imports Main
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
ML {*
|
|
|
6 |
fun ML_exec prog = ML_Compiler.eval true Position.none
|
|
|
7 |
(ML_Lex.tokenize prog)
|
|
|
8 |
|
|
|
9 |
fun prog_data_slot name tp empty =
|
|
|
10 |
"structure " ^ name ^ " = Theory_Data ( " ^
|
|
|
11 |
"type T = "^ tp ^" " ^
|
|
|
12 |
"val empty = " ^ empty ^ " ; "^
|
|
|
13 |
"val extend = I; "^
|
|
|
14 |
"fun merge (x, y) = x) "^
|
|
|
15 |
"fun "^ name ^ "_store v = Context.>>(Context.map_theory (" ^ name ^".map (fn x => v))) "^
|
|
|
16 |
"fun "^ name ^ "_get () = Context.>>>(Context.map_theory_result (fn th => "^
|
|
|
17 |
" ("^ name ^".get th, th))) "
|
|
|
18 |
|
|
|
19 |
fun data_slot name tp empty = ML_exec (prog_data_slot name tp empty)
|
|
|
20 |
val empty_term = @{term "x"}
|
|
|
21 |
val empty_cterm = @{cterm "x"}
|
|
|
22 |
val empty_thm = @{thm ext}
|
|
|
23 |
*}
|
|
|
24 |
|
|
|
25 |
end
|