5 text{* Tweak code generation to work with sets of non-equality types: *} |
5 text{* Tweak code generation to work with sets of non-equality types: *} |
6 declare insert_code[code del] union_coset_filter[code del] |
6 declare insert_code[code del] union_coset_filter[code del] |
7 lemma insert_code [code]: "insert x (set xs) = set (x#xs)" |
7 lemma insert_code [code]: "insert x (set xs) = set (x#xs)" |
8 by simp |
8 by simp |
9 |
9 |
|
10 text{* In order to display commands annotated with state sets, |
|
11 states must be translated into a printable format as lists of pairs, |
|
12 for a given set of variable names. This is what @{text show_acom} does: *} |
|
13 |
|
14 definition show_acom :: |
|
15 "vname list \<Rightarrow> state set acom \<Rightarrow> (vname*val)list set acom" where |
|
16 "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. map (\<lambda>x. (x, s x)) xs) ` S)" |
|
17 |
|
18 |
10 text{* The example: *} |
19 text{* The example: *} |
11 definition "c = WHILE Less (V ''x'') (N 3) |
20 definition "c = WHILE Less (V ''x'') (N 3) |
12 DO ''x'' ::= Plus (V ''x'') (N 2)" |
21 DO ''x'' ::= Plus (V ''x'') (N 2)" |
13 definition C0 :: "state set acom" where "C0 = anno {} c" |
22 definition C0 :: "state set acom" where "C0 = anno {} c" |
14 |
|
15 definition "show_acom xs = map_acom (\<lambda>S. (\<lambda>s. [(x,s x). x \<leftarrow> xs]) ` S)" |
|
16 |
23 |
17 text{* Collecting semantics: *} |
24 text{* Collecting semantics: *} |
18 |
25 |
19 value "show_acom [''x''] (((step {<>}) ^^ 1) C0)" |
26 value "show_acom [''x''] (((step {<>}) ^^ 1) C0)" |
20 value "show_acom [''x''] (((step {<>}) ^^ 2) C0)" |
27 value "show_acom [''x''] (((step {<>}) ^^ 2) C0)" |