3 begin |
3 begin |
4 |
4 |
5 text{* Syntax for commands and for assertions and boolean expressions in |
5 text{* Syntax for commands and for assertions and boolean expressions in |
6 commands @{text com} and annotated commands @{text ann_com}. *} |
6 commands @{text com} and annotated commands @{text ann_com}. *} |
7 |
7 |
|
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 |
8 syntax |
18 syntax |
9 "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
19 "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
10 "_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61) |
20 "_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61) |
11 |
21 |
12 translations |
22 translations |
13 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>" |
23 "\<acute>x := a" \<rightharpoonup> "CONST Basic \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>" |
14 "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>" |
24 "r \<acute>x := a" \<rightharpoonup> "CONST AnnBasic r \<guillemotleft>\<acute>(_update_name x (\<lambda>_. a))\<guillemotright>" |
15 |
25 |
16 syntax |
26 syntax |
17 "_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63) |
|
18 "_AnnSeq" :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" ("_;;/ _" [60,61] 60) |
|
19 |
|
20 "_AnnCond1" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
27 "_AnnCond1" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
21 ("_ //IF _ /THEN _ /ELSE _ /FI" [90,0,0,0] 61) |
28 ("_ //IF _ /THEN _ /ELSE _ /FI" [90,0,0,0] 61) |
22 "_AnnCond2" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
29 "_AnnCond2" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
23 ("_ //IF _ /THEN _ /FI" [90,0,0] 61) |
30 ("_ //IF _ /THEN _ /FI" [90,0,0] 61) |
24 "_AnnWhile" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
31 "_AnnWhile" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" |
26 "_AnnAwait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" |
33 "_AnnAwait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" |
27 ("_ //AWAIT _ /THEN /_ /END" [90,0,0] 61) |
34 ("_ //AWAIT _ /THEN /_ /END" [90,0,0] 61) |
28 "_AnnAtom" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" ("_//\<langle>_\<rangle>" [90,0] 61) |
35 "_AnnAtom" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a ann_com" ("_//\<langle>_\<rangle>" [90,0] 61) |
29 "_AnnWait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com" ("_//WAIT _ END" [90,0] 61) |
36 "_AnnWait" :: "'a assn \<Rightarrow> 'a bexp \<Rightarrow> 'a ann_com" ("_//WAIT _ END" [90,0] 61) |
30 |
37 |
31 "_Skip" :: "'a com" ("SKIP" 63) |
|
32 "_Seq" :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("_,,/ _" [55, 56] 55) |
|
33 "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" |
38 "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" |
34 ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) |
39 ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) |
35 "_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("IF _ THEN _ FI" [0,0] 56) |
40 "_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("IF _ THEN _ FI" [0,0] 56) |
36 "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" |
41 "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com" |
37 ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) |
42 ("(0WHILE _/ INV _ //DO _ /OD)" [0, 0, 0] 61) |
38 "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" |
43 "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" |
39 ("(0WHILE _ //DO _ /OD)" [0, 0] 61) |
44 ("(0WHILE _ //DO _ /OD)" [0, 0] 61) |
40 |
45 |
41 translations |
46 translations |
42 "SKIP" \<rightleftharpoons> "Basic id" |
47 "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond .{b}. c1 c2" |
43 "c_1,, c_2" \<rightleftharpoons> "Seq c_1 c_2" |
|
44 |
|
45 "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2" |
|
46 "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI" |
48 "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI" |
47 "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c" |
49 "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c" |
48 "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD" |
50 "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD" |
49 |
51 |
50 "r SKIP" \<rightleftharpoons> "AnnBasic r id" |
52 "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST AnnCond1 r .{b}. c1 c2" |
51 "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2" |
53 "r IF b THEN c FI" \<rightharpoonup> "CONST AnnCond2 r .{b}. c" |
52 "r IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "AnnCond1 r .{b}. c1 c2" |
54 "r WHILE b INV i DO c OD" \<rightharpoonup> "CONST AnnWhile r .{b}. i c" |
53 "r IF b THEN c FI" \<rightharpoonup> "AnnCond2 r .{b}. c" |
55 "r AWAIT b THEN c END" \<rightharpoonup> "CONST AnnAwait r .{b}. c" |
54 "r WHILE b INV i DO c OD" \<rightharpoonup> "AnnWhile r .{b}. i c" |
|
55 "r AWAIT b THEN c END" \<rightharpoonup> "AnnAwait r .{b}. c" |
|
56 "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT True THEN c END" |
56 "r \<langle>c\<rangle>" \<rightleftharpoons> "r AWAIT True THEN c END" |
57 "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END" |
57 "r WAIT b END" \<rightleftharpoons> "r AWAIT b THEN SKIP END" |
58 |
58 |
59 nonterminals |
59 nonterminals |
60 prgs |
60 prgs |
66 |
66 |
67 "_prg_scheme" :: "['a, 'a, 'a, 'a, 'a] \<Rightarrow> prgs" |
67 "_prg_scheme" :: "['a, 'a, 'a, 'a, 'a] \<Rightarrow> prgs" |
68 ("SCHEME [_ \<le> _ < _] _// _" [0,0,0,60, 90] 57) |
68 ("SCHEME [_ \<le> _ < _] _// _" [0,0,0,60, 90] 57) |
69 |
69 |
70 translations |
70 translations |
71 "_prg c q" \<rightleftharpoons> "[(Some c, q)]" |
71 "_prg c q" \<rightleftharpoons> "[(CONST Some c, q)]" |
72 "_prgs c q ps" \<rightleftharpoons> "(Some c, q) # ps" |
72 "_prgs c q ps" \<rightleftharpoons> "(CONST Some c, q) # ps" |
73 "_PAR ps" \<rightleftharpoons> "Parallel ps" |
73 "_PAR ps" \<rightleftharpoons> "CONST Parallel ps" |
74 |
74 |
75 "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (Some c, q)) [j..<k]" |
75 "_prg_scheme j i k c q" \<rightleftharpoons> "CONST map (\<lambda>i. (CONST Some c, q)) [j..<k]" |
76 |
76 |
77 print_translation {* |
77 print_translation {* |
78 let |
78 let |
79 fun quote_tr' f (t :: ts) = |
79 fun quote_tr' f (t :: ts) = |
80 Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts) |
80 Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts) |
84 Term.list_comb (f $ r $ Syntax.quote_tr' "_antiquote" t, ts) |
84 Term.list_comb (f $ r $ Syntax.quote_tr' "_antiquote" t, ts) |
85 | annquote_tr' _ _ = raise Match; |
85 | annquote_tr' _ _ = raise Match; |
86 |
86 |
87 val assert_tr' = quote_tr' (Syntax.const "_Assert"); |
87 val assert_tr' = quote_tr' (Syntax.const "_Assert"); |
88 |
88 |
89 fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) = |
89 fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
90 quote_tr' (Syntax.const name) (t :: ts) |
90 quote_tr' (Syntax.const name) (t :: ts) |
91 | bexp_tr' _ _ = raise Match; |
91 | bexp_tr' _ _ = raise Match; |
92 |
92 |
93 fun annbexp_tr' name (r :: (Const ("Collect", _) $ t) :: ts) = |
93 fun annbexp_tr' name (r :: (Const (@{const_syntax Collect}, _) $ t) :: ts) = |
94 annquote_tr' (Syntax.const name) (r :: t :: ts) |
94 annquote_tr' (Syntax.const name) (r :: t :: ts) |
95 | annbexp_tr' _ _ = raise Match; |
95 | annbexp_tr' _ _ = raise Match; |
96 |
96 |
97 fun upd_tr' (x_upd, T) = |
97 fun upd_tr' (x_upd, T) = |
98 (case try (unsuffix Record.updateN) x_upd of |
98 (case try (unsuffix Record.updateN) x_upd of |
103 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |
103 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |
104 c $ Free (upd_tr' x) |
104 c $ Free (upd_tr' x) |
105 | update_name_tr' (Const x) = Const (upd_tr' x) |
105 | update_name_tr' (Const x) = Const (upd_tr' x) |
106 | update_name_tr' _ = raise Match; |
106 | update_name_tr' _ = raise Match; |
107 |
107 |
108 fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match |
108 fun K_tr' (Abs (_, _, t)) = |
109 | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match |
109 if null (loose_bnos t) then t else raise Match |
|
110 | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) = |
|
111 if null (loose_bnos t) then t else raise Match |
110 | K_tr' _ = raise Match; |
112 | K_tr' _ = raise Match; |
111 |
113 |
112 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
114 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
113 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
115 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
114 (Abs (x, dummyT, K_tr' k) :: ts) |
116 (Abs (x, dummyT, K_tr' k) :: ts) |
117 fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = |
119 fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) = |
118 quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f) |
120 quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f) |
119 (Abs (x, dummyT, K_tr' k) :: ts) |
121 (Abs (x, dummyT, K_tr' k) :: ts) |
120 | annassign_tr' _ = raise Match; |
122 | annassign_tr' _ = raise Match; |
121 |
123 |
122 fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] = |
124 fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $ |
123 (Syntax.const "_prg" $ t1 $ t2) |
125 (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some},_) $ t1 ) $ t2) $ |
124 | Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1) $ t2) $ ts)] = |
126 Const (@{const_syntax Nil}, _))] = Syntax.const "_prg" $ t1 $ t2 |
125 (Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts]) |
127 | Parallel_PAR [(Const (@{const_syntax Cons}, _) $ |
|
128 (Const (@{const_syntax Pair}, _) $ (Const (@{const_syntax Some}, _) $ t1) $ t2) $ ts)] = |
|
129 Syntax.const "_prgs" $ t1 $ t2 $ Parallel_PAR [ts] |
126 | Parallel_PAR _ = raise Match; |
130 | Parallel_PAR _ = raise Match; |
127 |
131 |
128 fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts; |
132 fun Parallel_tr' ts = Syntax.const "_PAR" $ Parallel_PAR ts; |
129 in |
133 in |
130 [("Collect", assert_tr'), ("Basic", assign_tr'), |
134 [(@{const_syntax Collect}, assert_tr'), |
131 ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv"), |
135 (@{const_syntax Basic}, assign_tr'), |
132 ("AnnBasic", annassign_tr'), |
136 (@{const_syntax Cond}, bexp_tr' "_Cond"), |
133 ("AnnWhile", annbexp_tr' "_AnnWhile"), ("AnnAwait", annbexp_tr' "_AnnAwait"), |
137 (@{const_syntax While}, bexp_tr' "_While_inv"), |
134 ("AnnCond1", annbexp_tr' "_AnnCond1"), ("AnnCond2", annbexp_tr' "_AnnCond2")] |
138 (@{const_syntax AnnBasic}, annassign_tr'), |
135 |
139 (@{const_syntax AnnWhile}, annbexp_tr' "_AnnWhile"), |
136 end |
140 (@{const_syntax AnnAwait}, annbexp_tr' "_AnnAwait"), |
137 |
141 (@{const_syntax AnnCond1}, annbexp_tr' "_AnnCond1"), |
|
142 (@{const_syntax AnnCond2}, annbexp_tr' "_AnnCond2")] |
|
143 end; |
138 *} |
144 *} |
139 |
145 |
140 end |
146 end |