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