5851
|
1 |
ABexp = Main +
|
|
2 |
datatype
|
|
3 |
'a aexp = IF ('a bexp) ('a aexp) ('a aexp)
|
|
4 |
| Sum ('a aexp) ('a aexp)
|
|
5 |
| Diff ('a aexp) ('a aexp)
|
|
6 |
| Var 'a
|
|
7 |
| Num nat
|
|
8 |
and 'a bexp = Less ('a aexp) ('a aexp)
|
|
9 |
| And ('a bexp) ('a bexp)
|
|
10 |
| Neg ('a bexp)
|
|
11 |
consts evala :: ('a => nat) => 'a aexp => nat
|
|
12 |
evalb :: ('a => nat) => 'a bexp => bool
|
|
13 |
primrec
|
|
14 |
"evala env (IF b a1 a2) =
|
|
15 |
(if evalb env b then evala env a1 else evala env a2)"
|
|
16 |
"evala env (Sum a1 a2) = evala env a1 + evala env a2"
|
|
17 |
"evala env (Diff a1 a2) = evala env a1 - evala env a2"
|
|
18 |
"evala env (Var v) = env v"
|
|
19 |
"evala env (Num n) = n"
|
|
20 |
"evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
|
|
21 |
"evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"
|
|
22 |
"evalb env (Neg b) = (~ evalb env b)"
|
|
23 |
consts substa :: ('a => 'b aexp) => 'a aexp => 'b aexp
|
|
24 |
substb :: ('a => 'b aexp) => 'a bexp => 'b bexp
|
|
25 |
primrec
|
|
26 |
"substa s (IF b a1 a2) =
|
|
27 |
IF (substb s b) (substa s a1) (substa s a2)"
|
|
28 |
"substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
|
|
29 |
"substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
|
|
30 |
"substa s (Var v) = s v"
|
|
31 |
"substa s (Num n) = Num n"
|
|
32 |
"substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
|
|
33 |
"substb s (And b1 b2) = And (substb s b1) (substb s b2)"
|
|
34 |
"substb s (Neg b) = Neg (substb s b)"
|
|
35 |
end
|