|
25171
|
1 |
(* Title: StateSpaceSyntax.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Norbert Schirmer, TU Muenchen
|
|
|
4 |
*)
|
|
|
5 |
|
|
|
6 |
header {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
|
|
|
7 |
theory StateSpaceSyntax
|
|
|
8 |
imports StateSpaceLocale
|
|
|
9 |
|
|
|
10 |
begin
|
|
|
11 |
|
|
|
12 |
text {* The state space syntax is kept in an extra theory so that you
|
|
|
13 |
can choose if you want to use it or not. *}
|
|
|
14 |
|
|
|
15 |
syntax
|
|
|
16 |
"_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
|
|
|
17 |
"_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
|
|
|
18 |
"_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
|
|
|
19 |
|
|
|
20 |
translations
|
|
|
21 |
"_statespace_updates f (_updbinds b bs)" ==
|
|
|
22 |
"_statespace_updates (_statespace_updates f b) bs"
|
|
|
23 |
"s<x:=y>" == "_statespace_update s x y"
|
|
|
24 |
|
|
|
25 |
|
|
|
26 |
parse_translation (advanced)
|
|
|
27 |
{*
|
|
|
28 |
[("_statespace_lookup",StateSpace.lookup_tr),
|
|
|
29 |
("_get",StateSpace.lookup_tr),
|
|
|
30 |
("_statespace_update",StateSpace.update_tr)]
|
|
|
31 |
*}
|
|
|
32 |
|
|
|
33 |
|
|
|
34 |
print_translation (advanced)
|
|
|
35 |
{*
|
|
|
36 |
[("lookup",StateSpace.lookup_tr'),
|
|
|
37 |
("StateFun.lookup",StateSpace.lookup_tr'),
|
|
|
38 |
("update",StateSpace.update_tr'),
|
|
|
39 |
("StateFun.update",StateSpace.update_tr')]
|
|
|
40 |
*}
|
|
|
41 |
|
|
|
42 |
end |