|
5377
|
1 |
Ifexpr = Main +
|
|
|
2 |
datatype boolex = Const bool | Var nat
|
|
|
3 |
| Neg boolex | And boolex boolex
|
|
|
4 |
consts value :: boolex => (nat => bool) => bool
|
|
|
5 |
primrec
|
|
|
6 |
"value (Const b) env = b"
|
|
|
7 |
"value (Var x) env = env x"
|
|
|
8 |
"value (Neg b) env = (~ value b env)"
|
|
|
9 |
"value (And b c) env = (value b env & value c env)"
|
|
|
10 |
datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
|
|
|
11 |
consts valif :: ifex => (nat => bool) => bool
|
|
|
12 |
primrec
|
|
|
13 |
"valif (CIF b) env = b"
|
|
|
14 |
"valif (VIF x) env = env x"
|
|
|
15 |
"valif (IF b t e) env = (if valif b env then valif t env
|
|
|
16 |
else valif e env)"
|
|
|
17 |
consts bool2if :: boolex => ifex
|
|
|
18 |
primrec
|
|
|
19 |
"bool2if (Const b) = CIF b"
|
|
|
20 |
"bool2if (Var x) = VIF x"
|
|
|
21 |
"bool2if (Neg b) = IF (bool2if b) (CIF False) (CIF True)"
|
|
|
22 |
"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)"
|
|
|
23 |
consts normif :: ifex => ifex => ifex => ifex
|
|
|
24 |
primrec
|
|
|
25 |
"normif (CIF b) t e = IF (CIF b) t e"
|
|
|
26 |
"normif (VIF x) t e = IF (VIF x) t e"
|
|
|
27 |
"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"
|
|
|
28 |
consts norm :: ifex => ifex
|
|
|
29 |
primrec
|
|
|
30 |
"norm (CIF b) = CIF b"
|
|
|
31 |
"norm (VIF x) = VIF x"
|
|
|
32 |
"norm (IF b t e) = normif b (norm t) (norm e)"
|
|
|
33 |
consts normal :: ifex => bool
|
|
|
34 |
primrec
|
|
|
35 |
"normal(CIF b) = True"
|
|
|
36 |
"normal(VIF x) = True"
|
|
|
37 |
"normal(IF b t e) = (normal t & normal e &
|
|
|
38 |
(case b of CIF b => True | VIF x => True | IF x y z => False))"
|
|
|
39 |
end
|