equal
deleted
inserted
replaced
14 "_Await" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(0AWAIT _ /THEN /_ /END)" [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) |
15 "_Atom" :: "'a com \<Rightarrow> 'a com" ("(\<langle>_\<rangle>)" 61) |
16 "_Wait" :: "'a bexp \<Rightarrow> 'a com" ("(0WAIT _ END)" 61) |
16 "_Wait" :: "'a bexp \<Rightarrow> 'a com" ("(0WAIT _ END)" 61) |
17 |
17 |
18 translations |
18 translations |
19 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>" |
19 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>" |
20 "SKIP" \<rightleftharpoons> "Basic id" |
20 "SKIP" \<rightleftharpoons> "Basic id" |
21 "c1;; c2" \<rightleftharpoons> "Seq c1 c2" |
21 "c1;; c2" \<rightleftharpoons> "Seq c1 c2" |
22 "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. 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" |
23 "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI" |
24 "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c" |
24 "WHILE b DO c OD" \<rightharpoonup> "While .{b}. c" |
76 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |
76 | update_name_tr' ((c as Const ("_free", _)) $ Free x) = |
77 c $ Free (upd_tr' x) |
77 c $ Free (upd_tr' x) |
78 | update_name_tr' (Const x) = Const (upd_tr' x) |
78 | update_name_tr' (Const x) = Const (upd_tr' x) |
79 | update_name_tr' _ = raise Match; |
79 | update_name_tr' _ = raise Match; |
80 |
80 |
81 fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = |
81 fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"}, _)$t) $ Bound 0) :: ts) = |
82 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
82 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
83 (Abs (x, dummyT, t) :: ts) |
83 (Abs (x, dummyT, t) :: ts) |
84 | assign_tr' _ = raise Match; |
84 | assign_tr' _ = raise Match; |
85 in |
85 in |
86 [("Collect", assert_tr'), ("Basic", assign_tr'), |
86 [("Collect", assert_tr'), ("Basic", assign_tr'), |