|
5377
|
1 |
Exercise = Main +
|
|
|
2 |
datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
|
|
|
3 |
consts valif :: ifex => (nat => bool) => bool
|
|
|
4 |
primrec valif ifex
|
|
|
5 |
"valif (CIF b) env = b"
|
|
|
6 |
"valif (VIF x) env = env x"
|
|
|
7 |
"valif (IF b t e) env = (if valif b env then valif t env
|
|
|
8 |
else valif e env)"
|
|
|
9 |
consts normif :: ifex => ifex => ifex => ifex
|
|
|
10 |
primrec normif ifex
|
|
|
11 |
"normif (CIF b) t e = (if b then t else e)"
|
|
|
12 |
"normif (VIF x) t e = IF (VIF x) t e"
|
|
|
13 |
"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
|
|
|
14 |
consts norm :: ifex => ifex
|
|
|
15 |
primrec norm ifex
|
|
|
16 |
"norm (CIF b) = CIF b"
|
|
|
17 |
"norm (VIF x) = VIF x"
|
|
|
18 |
"norm (IF b t e) = normif b (norm t) (norm e)"
|
|
|
19 |
consts normal :: ifex => bool
|
|
|
20 |
primrec normal ifex
|
|
|
21 |
"normal(CIF b) = True"
|
|
|
22 |
"normal(VIF x) = True"
|
|
|
23 |
"normal(IF b t e) = (normal t & normal e &
|
|
|
24 |
(case b of CIF b => False | VIF x => True | IF x y z => False))"
|
|
|
25 |
end
|