21190
|
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 |
|
22386
|
11 |
structure Integer =
|
|
12 |
struct
|
|
13 |
|
22798
|
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 |
|
22386
|
77 |
fun nat_aux n i =
|
22798
|
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)))));
|
22386
|
81 |
|
|
82 |
fun nat i = nat_aux Nat.Zero_nat i;
|
|
83 |
|
|
84 |
end; (*struct Integer*)
|
|
85 |
|
21190
|
86 |
structure Codegen =
|
|
87 |
struct
|
|
88 |
|
22015
|
89 |
val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
|
21190
|
90 |
|
|
91 |
val foobar_set : Nat.nat list =
|
22015
|
92 |
Nat.Zero_nat ::
|
22798
|
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 |
:: []));
|
21190
|
99 |
|
|
100 |
end; (*struct Codegen*)
|
|
101 |
|
|
102 |
end; (*struct ROOT*)
|