12 Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | |
12 Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | |
13 Aseq acom acom ("_;;/ _" [60, 61] 60) | |
13 Aseq acom acom ("_;;/ _" [60, 61] 60) | |
14 Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | |
14 Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | |
15 Awhile assn bexp acom ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61) |
15 Awhile assn bexp acom ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61) |
16 |
16 |
|
17 notation com.SKIP ("SKIP") |
17 |
18 |
18 text{* Strip annotations: *} |
19 text{* Strip annotations: *} |
19 |
20 |
20 fun strip :: "acom \<Rightarrow> com" where |
21 fun strip :: "acom \<Rightarrow> com" where |
21 "strip SKIP = com.SKIP" | |
22 "strip SKIP = SKIP" | |
22 "strip (x ::= a) = (x ::= a)" | |
23 "strip (x ::= a) = (x ::= a)" | |
23 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | |
24 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | |
24 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" | |
25 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" | |
25 "strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
26 "strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
26 |
27 |