| author | ibm-PC\ibm <xingyuanzhang@126.com> |
| Fri, 12 Sep 2014 00:41:17 +0800 | |
| changeset 23 | 452e8b557b63 |
| parent 0 | 1378b654acde |
| permissions | -rw-r--r-- |
|
0
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
theory Data_slot |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
imports Main |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
begin |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
ML {*
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
fun ML_exec prog = ML_Compiler.eval true Position.none |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
(ML_Lex.tokenize prog) |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
fun prog_data_slot name tp empty = |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
"structure " ^ name ^ " = Theory_Data ( " ^ |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
"type T = "^ tp ^" " ^ |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
"val empty = " ^ empty ^ " ; "^ |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
"val extend = I; "^ |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
"fun merge (x, y) = x) "^ |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
"fun "^ name ^ "_store v = Context.>>(Context.map_theory (" ^ name ^".map (fn x => v))) "^
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
"fun "^ name ^ "_get () = Context.>>>(Context.map_theory_result (fn th => "^ |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
" ("^ name ^".get th, th))) "
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
fun data_slot name tp empty = ML_exec (prog_data_slot name tp empty) |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
val empty_term = @{term "x"}
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
val empty_cterm = @{cterm "x"}
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
val empty_thm = @{thm ext}
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
*} |
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
|
|
1378b654acde
initial commit for Isabelle 2013-1
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
end |