|
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 |