1 structure ROOT = |
|
2 struct |
|
3 |
|
4 structure Nat = |
|
5 struct |
|
6 |
|
7 datatype nat = Zero_nat | Suc of nat; |
|
8 |
|
9 end; (*struct Nat*) |
|
10 |
|
11 structure Integer = |
|
12 struct |
|
13 |
|
14 datatype bit = B0 | B1; |
|
15 |
|
16 datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; |
|
17 |
|
18 fun pred (Bit (k, B0)) = Bit (pred k, B1) |
|
19 | pred (Bit (k, B1)) = Bit (k, B0) |
|
20 | pred Min = Bit (Min, B0) |
|
21 | pred Pls = Min; |
|
22 |
|
23 fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) |
|
24 | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) |
|
25 | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) |
|
26 | uminus_int Min = Bit (Pls, B1) |
|
27 | uminus_int Pls = Pls; |
|
28 |
|
29 fun succ (Bit (k, B0)) = Bit (k, B1) |
|
30 | succ (Bit (k, B1)) = Bit (succ k, B0) |
|
31 | succ Min = Pls |
|
32 | succ Pls = Bit (Pls, B1); |
|
33 |
|
34 fun plus_int (Number_of_int v) (Number_of_int w) = |
|
35 Number_of_int (plus_int v w) |
|
36 | plus_int k Min = pred k |
|
37 | plus_int k Pls = k |
|
38 | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) |
|
39 | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) |
|
40 | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) |
|
41 | plus_int Min k = pred k |
|
42 | plus_int Pls k = k; |
|
43 |
|
44 fun minus_int (Number_of_int v) (Number_of_int w) = |
|
45 Number_of_int (plus_int v (uminus_int w)) |
|
46 | minus_int z w = plus_int z (uminus_int w); |
|
47 |
|
48 fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l |
|
49 | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2 |
|
50 | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2 |
|
51 | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2 |
|
52 | less_eq_int (Bit (k, v)) Min = less_eq_int k Min |
|
53 | less_eq_int (Bit (k, B1)) Pls = less_int k Pls |
|
54 | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls |
|
55 | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k |
|
56 | less_eq_int Min (Bit (k, B0)) = less_int Min k |
|
57 | less_eq_int Min Min = true |
|
58 | less_eq_int Min Pls = true |
|
59 | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k |
|
60 | less_eq_int Pls Min = false |
|
61 | less_eq_int Pls Pls = true |
|
62 and less_int (Number_of_int k) (Number_of_int l) = less_int k l |
|
63 | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2 |
|
64 | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2 |
|
65 | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2 |
|
66 | less_int (Bit (k, B1)) Min = less_int k Min |
|
67 | less_int (Bit (k, B0)) Min = less_eq_int k Min |
|
68 | less_int (Bit (k, v)) Pls = less_int k Pls |
|
69 | less_int Min (Bit (k, v)) = less_int Min k |
|
70 | less_int Min Min = false |
|
71 | less_int Min Pls = true |
|
72 | less_int Pls (Bit (k, B1)) = less_eq_int Pls k |
|
73 | less_int Pls (Bit (k, B0)) = less_int Pls k |
|
74 | less_int Pls Min = false |
|
75 | less_int Pls Pls = false; |
|
76 |
|
77 fun nat_aux n i = |
|
78 (if less_eq_int i (Number_of_int Pls) then n |
|
79 else nat_aux (Nat.Suc n) |
|
80 (minus_int i (Number_of_int (Bit (Pls, B1))))); |
|
81 |
|
82 fun nat i = nat_aux Nat.Zero_nat i; |
|
83 |
|
84 end; (*struct Integer*) |
|
85 |
|
86 structure Codegen = |
|
87 struct |
|
88 |
|
89 val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: []; |
|
90 |
|
91 val foobar_set : Nat.nat list = |
|
92 Nat.Zero_nat :: |
|
93 (Nat.Suc Nat.Zero_nat :: |
|
94 (Integer.nat |
|
95 (Integer.Number_of_int |
|
96 (Integer.Bit |
|
97 (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0))) |
|
98 :: [])); |
|
99 |
|
100 end; (*struct Codegen*) |
|
101 |
|
102 end; (*struct ROOT*) |
|