|
1 header {* \section{Concrete Syntax} *} |
|
2 |
|
3 theory RG_Syntax |
|
4 imports RG_Hoare Quote_Antiquote |
|
5 begin |
|
6 |
|
7 syntax |
|
8 "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
|
9 "_skip" :: "'a com" ("SKIP") |
|
10 "_Seq" :: "'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(_;;/ _)" [60,61] 60) |
|
11 "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61) |
|
12 "_Cond2" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0IF _ THEN _ FI)" [0,0] 56) |
|
13 "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0WHILE _ /DO _ /OD)" [0, 0] 61) |
|
14 "_Await" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0AWAIT _ /THEN /_ /END)" [0,0] 61) |
|
15 "_Atom" :: "'a com \<Rightarrow> 'a com" ("(\<langle>_\<rangle>)" 61) |
|
16 "_Wait" :: "'a bexp \<Rightarrow> 'a com" ("(0WAIT _ END)" 61) |
|
17 |
|
18 translations |
|
19 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (\<lambda>_. a))\<guillemotright>" |
|
20 "SKIP" \<rightleftharpoons> "Basic id" |
|
21 "c1;; c2" \<rightleftharpoons> "Seq c1 c2" |
|
22 "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2" |
|
23 "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI" |
|
24 "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c" |
|
25 "AWAIT b THEN c END" \<rightleftharpoons> "Await .{b}. c" |
|
26 "\<langle>c\<rangle>" \<rightleftharpoons> "AWAIT True THEN c END" |
|
27 "WAIT b END" \<rightleftharpoons> "AWAIT b THEN SKIP END" |
|
28 |
|
29 nonterminals |
|
30 prgs |
|
31 |
|
32 syntax |
|
33 "_PAR" :: "prgs \<Rightarrow> 'a" ("COBEGIN//_//COEND" 60) |
|
34 "_prg" :: "'a \<Rightarrow> prgs" ("_" 57) |
|
35 "_prgs" :: "['a, prgs] \<Rightarrow> prgs" ("_//\<parallel>//_" [60,57] 57) |
|
36 |
|
37 translations |
|
38 "_prg a" \<rightharpoonup> "[a]" |
|
39 "_prgs a ps" \<rightharpoonup> "a # ps" |
|
40 "_PAR ps" \<rightharpoonup> "ps" |
|
41 |
|
42 syntax |
|
43 "_prg_scheme" :: "['a, 'a, 'a, 'a] \<Rightarrow> prgs" ("SCHEME [_ \<le> _ < _] _" [0,0,0,60] 57) |
|
44 |
|
45 translations |
|
46 "_prg_scheme j i k c" \<rightleftharpoons> "(map (\<lambda>i. c) [j..<k])" |
|
47 |
|
48 text {* Translations for variables before and after a transition: *} |
|
49 |
|
50 syntax |
|
51 "_before" :: "id \<Rightarrow> 'a" ("\<ordmasculine>_") |
|
52 "_after" :: "id \<Rightarrow> 'a" ("\<ordfeminine>_") |
|
53 |
|
54 translations |
|
55 "\<ordmasculine>x" \<rightleftharpoons> "x \<acute>fst" |
|
56 "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>snd" |
|
57 |
|
58 print_translation {* |
|
59 let |
|
60 fun quote_tr' f (t :: ts) = |
|
61 Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts) |
|
62 | quote_tr' _ _ = raise Match; |
|
63 |
|
64 val assert_tr' = quote_tr' (Syntax.const "_Assert"); |
|
65 |
|
66 fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) = |
|
67 quote_tr' (Syntax.const name) (t :: ts) |
|
68 | bexp_tr' _ _ = raise Match; |
|
69 |
|
70 fun upd_tr' (x_upd, T) = |
|
71 (case try (unsuffix Record.updateN) x_upd of |
|
72 SOME x => (x, if T = dummyT then T else Term.domain_type T) |
|
73 | NONE => raise Match); |
|
74 |
|
75 fun update_name_tr' (Free x) = Free (upd_tr' x) |
|
76 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |
|
77 c $ Free (upd_tr' x) |
|
78 | update_name_tr' (Const x) = Const (upd_tr' x) |
|
79 | update_name_tr' _ = raise Match; |
|
80 |
|
81 fun K_tr' (Abs (_,_,t)) = if null (loose_bnos t) then t else raise Match |
|
82 | K_tr' (Abs (_,_,Abs (_,_,t)$Bound 0)) = if null (loose_bnos t) then t else raise Match |
|
83 | K_tr' _ = raise Match; |
|
84 |
|
85 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
|
86 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
|
87 (Abs (x, dummyT, K_tr' k) :: ts) |
|
88 | assign_tr' _ = raise Match; |
|
89 in |
|
90 [("Collect", assert_tr'), ("Basic", assign_tr'), |
|
91 ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")] |
|
92 end |
|
93 *} |
|
94 |
|
95 end |