8 syntax |
8 syntax |
9 "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(\<acute>_ :=/ _)" [70, 65] 61) |
9 "_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) |
10 "_AnnAssign" :: "'a assn \<Rightarrow> idt \<Rightarrow> 'b \<Rightarrow> 'a com" ("(_ \<acute>_ :=/ _)" [90,70,65] 61) |
11 |
11 |
12 translations |
12 translations |
13 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>" |
13 "\<acute>\<spacespace>x := a" \<rightharpoonup> "Basic \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>" |
14 "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (K_record a))\<guillemotright>" |
14 "r \<acute>\<spacespace>x := a" \<rightharpoonup> "AnnBasic r \<guillemotleft>\<acute>\<spacespace>(_update_name x (CONST K_record a))\<guillemotright>" |
15 |
15 |
16 syntax |
16 syntax |
17 "_AnnSkip" :: "'a assn \<Rightarrow> 'a ann_com" ("_//SKIP" [90] 63) |
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) |
18 "_AnnSeq" :: "'a ann_com \<Rightarrow> 'a ann_com \<Rightarrow> 'a ann_com" ("_;;/ _" [60,61] 60) |
19 |
19 |
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 assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = |
108 fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) = |
109 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
109 quote_tr' (Syntax.const "_Assign" $ update_name_tr' f) |
110 (Abs (x, dummyT, t) :: ts) |
110 (Abs (x, dummyT, t) :: ts) |
111 | assign_tr' _ = raise Match; |
111 | assign_tr' _ = raise Match; |
112 |
112 |
113 fun annassign_tr' (r :: Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) = |
113 fun annassign_tr' (r :: Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) = |
114 quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f) |
114 quote_tr' (Syntax.const "_AnnAssign" $ r $ update_name_tr' f) |
115 (Abs (x, dummyT, t) :: ts) |
115 (Abs (x, dummyT, t) :: ts) |
116 | annassign_tr' _ = raise Match; |
116 | annassign_tr' _ = raise Match; |
117 |
117 |
118 fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] = |
118 fun Parallel_PAR [(Const ("Cons",_) $ (Const ("Pair",_) $ (Const ("Some",_) $ t1 ) $ t2) $ Const ("Nil",_))] = |