author | wenzelm |
Tue, 16 Feb 2010 14:08:39 +0100 | |
changeset 35145 | f132a4fd8679 |
parent 35113 | 1a0c129bb2e0 |
child 41229 | d797baa3d57c |
permissions | -rw-r--r-- |
13099 | 1 |
header {* \section{Concrete Syntax} *} |
13020 | 2 |
|
15425 | 3 |
theory RG_Syntax |
4 |
imports RG_Hoare Quote_Antiquote |
|
5 |
begin |
|
13020 | 6 |
|
35107 | 7 |
abbreviation Skip :: "'a com" ("SKIP") |
8 |
where "SKIP \<equiv> Basic id" |
|
9 |
||
10 |
notation Seq ("(_;;/ _)" [60,61] 60) |
|
11 |
||
13020 | 12 |
syntax |
13 |
"_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
|
14 |
"_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61) |
|
15 |
"_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0IF _ THEN _ FI)" [0,0] 56) |
|
16 |
"_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0WHILE _ /DO _ /OD)" [0, 0] 61) |
|
17 |
"_Await" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0AWAIT _ /THEN /_ /END)" [0,0] 61) |
|
18 |
"_Atom" :: "'a com \<Rightarrow> 'a com" ("(\<langle>_\<rangle>)" 61) |
|
19 |
"_Wait" :: "'a bexp \<Rightarrow> 'a com" ("(0WAIT _ END)" 61) |
|
20 |
||
21 |
translations |
|
35107 | 22 |
"\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>" |
35113 | 23 |
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2" |
13020 | 24 |
"IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI" |
35113 | 25 |
"WHILE b DO c OD" \<rightharpoonup> "CONST While .{b}. c" |
26 |
"AWAIT b THEN c END" \<rightleftharpoons> "CONST Await .{b}. c" |
|
27 |
"\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT CONST True THEN c END" |
|
13020 | 28 |
"WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END" |
29 |
||
30 |
nonterminals |
|
31 |
prgs |
|
32 |
||
33 |
syntax |
|
34 |
"_PAR" :: "prgs \<Rightarrow> 'a" ("COBEGIN//_//COEND" 60) |
|
35 |
"_prg" :: "'a \<Rightarrow> prgs" ("_" 57) |
|
36 |
"_prgs" :: "['a, prgs] \<Rightarrow> prgs" ("_//\<parallel>//_" [60,57] 57) |
|
37 |
||
38 |
translations |
|
39 |
"_prg a" \<rightharpoonup> "[a]" |
|
40 |
"_prgs a ps" \<rightharpoonup> "a # ps" |
|
41 |
"_PAR ps" \<rightharpoonup> "ps" |
|
42 |
||
43 |
syntax |
|
44 |
"_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57) |
|
45 |
||
46 |
translations |
|
34940 | 47 |
"_prg_scheme j i k c" \<rightleftharpoons> "(CONST map (\<lambda>i. c) [j..<k])" |
13020 | 48 |
|
49 |
text {* Translations for variables before and after a transition: *} |
|
50 |
||
51 |
syntax |
|
52 |
"_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_") |
|
53 |
"_after" :: "id \<Rightarrow> 'a" ("\<ordfeminine>_") |
|
54 |
||
55 |
translations |
|
35107 | 56 |
"\<ordmasculine>x" \<rightleftharpoons> "x \<acute>CONST fst" |
57 |
"\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd" |
|
13020 | 58 |
|
59 |
print_translation {* |
|
60 |
let |
|
61 |
fun quote_tr' f (t :: ts) = |
|
35113 | 62 |
Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts) |
13020 | 63 |
| quote_tr' _ _ = raise Match; |
64 |
||
35113 | 65 |
val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); |
13020 | 66 |
|
35107 | 67 |
fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
13020 | 68 |
quote_tr' (Syntax.const name) (t :: ts) |
69 |
| bexp_tr' _ _ = raise Match; |
|
70 |
||
35107 | 71 |
fun K_tr' (Abs (_, _, t)) = |
72 |
if null (loose_bnos t) then t else raise Match |
|
73 |
| K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = |
|
74 |
if null (loose_bnos t) then t else raise Match |
|
25706 | 75 |
| K_tr' _ = raise Match; |
76 |
||
77 |
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
|
35145
f132a4fd8679
moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents:
35113
diff
changeset
|
78 |
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) |
25706 | 79 |
(Abs (x, dummyT, K_tr' k) :: ts) |
13020 | 80 |
| assign_tr' _ = raise Match; |
81 |
in |
|
35107 | 82 |
[(@{const_syntax Collect}, assert_tr'), |
83 |
(@{const_syntax Basic}, assign_tr'), |
|
35113 | 84 |
(@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), |
85 |
(@{const_syntax While}, bexp_tr' @{syntax_const "_While"})] |
|
13020 | 86 |
end |
87 |
*} |
|
88 |
||
89 |
end |