7 subsection "Constant Propagation" |
7 subsection "Constant Propagation" |
8 |
8 |
9 datatype const = Const val | Any |
9 datatype const = Const val | Any |
10 |
10 |
11 fun \<gamma>_const where |
11 fun \<gamma>_const where |
12 "\<gamma>_const (Const n) = {n}" | |
12 "\<gamma>_const (Const i) = {i}" | |
13 "\<gamma>_const (Any) = UNIV" |
13 "\<gamma>_const (Any) = UNIV" |
14 |
14 |
15 fun plus_const where |
15 fun plus_const where |
16 "plus_const (Const m) (Const n) = Const(m+n)" | |
16 "plus_const (Const i) (Const j) = Const(i+j)" | |
17 "plus_const _ _ = Any" |
17 "plus_const _ _ = Any" |
18 |
18 |
19 lemma plus_const_cases: "plus_const a1 a2 = |
19 lemma plus_const_cases: "plus_const a1 a2 = |
20 (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)" |
20 (case (a1,a2) of (Const i, Const j) \<Rightarrow> Const(i+j) | _ \<Rightarrow> Any)" |
21 by(auto split: prod.split const.split) |
21 by(auto split: prod.split const.split) |
22 |
22 |
23 instantiation const :: semilattice |
23 instantiation const :: semilattice |
24 begin |
24 begin |
25 |
25 |
26 fun less_eq_const where |
26 fun less_eq_const where "x \<le> y = (y = Any | x=y)" |
27 "_ \<le> Any = True" | |
|
28 "Const n \<le> Const m = (n=m)" | |
|
29 "Any \<le> Const _ = False" |
|
30 |
27 |
31 definition "a < (b::const) = (a \<le> b & ~ b \<le> a)" |
28 definition "x < (y::const) = (x \<le> y & \<not> y \<le> x)" |
32 |
29 |
33 fun sup_const where |
30 fun sup_const where |
34 "Const m \<squnion> Const n = (if n=m then Const m else Any)" | |
31 "Const i \<squnion> Const j = (if i=j then Const i else Any)" | |
35 "_ \<squnion> _ = Any" |
32 "_ \<squnion> _ = Any" |
36 |
33 |
37 definition "\<top> = Any" |
34 definition "\<top> = Any" |
38 |
35 |
39 instance |
36 instance |