author | wenzelm |
Sun, 11 Feb 2018 12:51:23 +0100 | |
changeset 67593 | 5efb88c90051 |
parent 62390 | 842917225d56 |
child 69216 | 1a52baa70aed |
permissions | -rw-r--r-- |
15425 | 1 |
theory OG_Syntax |
2 |
imports OG_Tactics Quote_Antiquote |
|
3 |
begin |
|
13020 | 4 |
|
59189 | 5 |
text\<open>Syntax for commands and for assertions and boolean expressions in |
62042 | 6 |
commands \<open>com\<close> and annotated commands \<open>ann_com\<close>.\<close> |
13020 | 7 |
|
35107 | 8 |
abbreviation Skip :: "'a com" ("SKIP" 63) |
9 |
where "SKIP \<equiv> Basic id" |
|
10 |
||
11 |
abbreviation AnnSkip :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63) |
|
12 |
where "r SKIP \<equiv> AnnBasic r id" |
|
13 |
||
14 |
notation |
|
15 |
Seq ("_,,/ _" [55, 56] 55) and |
|
16 |
AnnSeq ("_;;/ _" [60,61] 60) |
|
17 |
||
13020 | 18 |
syntax |
19 |
"_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
|
20 |
"_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61) |
|
21 |
||
22 |
translations |
|
35107 | 23 |
"\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>" |
24 |
"r \<acute>x := a" \<rightharpoonup> "CONST AnnBasic r \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>" |
|
13020 | 25 |
|
26 |
syntax |
|
27 |
"_AnnCond1" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
|
28 |
("_ //IF _ /THEN _ /ELSE _ /FI" [90,0,0,0] 61) |
|
29 |
"_AnnCond2" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
|
30 |
("_ //IF _ /THEN _ /FI" [90,0,0] 61) |
|
59189 | 31 |
"_AnnWhile" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
13020 | 32 |
("_ //WHILE _ /INV _ //DO _//OD" [90,0,0,0] 61) |
33 |
"_AnnAwait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" |
|
34 |
("_ //AWAIT _ /THEN /_ /END" [90,0,0] 61) |
|
35 |
"_AnnAtom" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" ("_//\<langle>_\<rangle>" [90,0] 61) |
|
36 |
"_AnnWait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com" ("_//WAIT _ END" [90,0] 61) |
|
37 |
||
59189 | 38 |
"_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" |
13020 | 39 |
("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) |
40 |
"_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("IF _ THEN _ FI" [0,0] 56) |
|
41 |
"_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" |
|
42 |
("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) |
|
43 |
"_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" |
|
44 |
("(0WHILE _ //DO _ /OD)" [0, 0] 61) |
|
45 |
||
46 |
translations |
|
53241 | 47 |
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2" |
13020 | 48 |
"IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI" |
53241 | 49 |
"WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c" |
28524 | 50 |
"WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD" |
13020 | 51 |
|
53241 | 52 |
"r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r \<lbrace>b\<rbrace> c1 c2" |
53 |
"r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r \<lbrace>b\<rbrace> c" |
|
54 |
"r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r \<lbrace>b\<rbrace> i c" |
|
55 |
"r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r \<lbrace>b\<rbrace> c" |
|
35113 | 56 |
"r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT CONST True THEN c END" |
13020 | 57 |
"r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END" |
59189 | 58 |
|
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
35145
diff
changeset
|
59 |
nonterminal prgs |
13020 | 60 |
|
61 |
syntax |
|
62 |
"_PAR" :: "prgs \<Rightarrow> 'a" ("COBEGIN//_//COEND" [57] 56) |
|
63 |
"_prg" :: "['a, 'a] \<Rightarrow> prgs" ("_//_" [60, 90] 57) |
|
64 |
"_prgs" :: "['a, 'a, prgs] \<Rightarrow> prgs" ("_//_//\<parallel>//_" [60,90,57] 57) |
|
65 |
||
59189 | 66 |
"_prg_scheme" :: "['a, 'a, 'a, 'a, 'a] \<Rightarrow> prgs" |
13020 | 67 |
("SCHEME [_ \<le> _ < _] _// _" [0,0,0,60, 90] 57) |
68 |
||
69 |
translations |
|
35107 | 70 |
"_prg c q" \<rightleftharpoons> "[(CONST Some c, q)]" |
71 |
"_prgs c q ps" \<rightleftharpoons> "(CONST Some c, q) # ps" |
|
72 |
"_PAR ps" \<rightleftharpoons> "CONST Parallel ps" |
|
13020 | 73 |
|
35107 | 74 |
"_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (CONST Some c, q)) [j..<k]" |
13020 | 75 |
|
59189 | 76 |
print_translation \<open> |
13020 | 77 |
let |
78 |
fun quote_tr' f (t :: ts) = |
|
42284 | 79 |
Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) |
13020 | 80 |
| quote_tr' _ _ = raise Match; |
81 |
||
82 |
fun annquote_tr' f (r :: t :: ts) = |
|
42284 | 83 |
Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) |
13020 | 84 |
| annquote_tr' _ _ = raise Match; |
85 |
||
35113 | 86 |
val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); |
13020 | 87 |
|
35107 | 88 |
fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
13020 | 89 |
quote_tr' (Syntax.const name) (t :: ts) |
90 |
| bexp_tr' _ _ = raise Match; |
|
91 |
||
35107 | 92 |
fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) = |
13020 | 93 |
annquote_tr' (Syntax.const name) (r :: t :: ts) |
94 |
| annbexp_tr' _ _ = raise Match; |
|
95 |
||
25706 | 96 |
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
42284 | 97 |
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) |
98 |
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) |
|
13020 | 99 |
| assign_tr' _ = raise Match; |
100 |
||
25706 | 101 |
fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = |
42284 | 102 |
quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f) |
103 |
(Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) |
|
13020 | 104 |
| annassign_tr' _ = raise Match; |
105 |
||
35107 | 106 |
fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $ |
107 |
(Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $ |
|
35113 | 108 |
Const (@{const_syntax Nil}, _))] = Syntax.const @{syntax_const "_prg"} $ t1 $ t2 |
35107 | 109 |
| Parallel_PAR [(Const (@{const_syntax Cons}, _) $ |
110 |
(Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some}, _) $ t1) $ t2) $ ts)] = |
|
35113 | 111 |
Syntax.const @{syntax_const "_prgs"} $ t1 $ t2 $ Parallel_PAR [ts] |
13020 | 112 |
| Parallel_PAR _ = raise Match; |
113 |
||
35113 | 114 |
fun Parallel_tr' ts = Syntax.const @{syntax_const "_PAR"} $ Parallel_PAR ts; |
13020 | 115 |
in |
52143 | 116 |
[(@{const_syntax Collect}, K assert_tr'), |
117 |
(@{const_syntax Basic}, K assign_tr'), |
|
118 |
(@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})), |
|
119 |
(@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"})), |
|
120 |
(@{const_syntax AnnBasic}, K annassign_tr'), |
|
121 |
(@{const_syntax AnnWhile}, K (annbexp_tr' @{syntax_const "_AnnWhile"})), |
|
122 |
(@{const_syntax AnnAwait}, K (annbexp_tr' @{syntax_const "_AnnAwait"})), |
|
123 |
(@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})), |
|
124 |
(@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))] |
|
35107 | 125 |
end; |
59189 | 126 |
\<close> |
13020 | 127 |
|
62390 | 128 |
end |