|
1 (* Title: Pure/ML-Systems/proper_int.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 SML basis with type int representing proper integers, not machine |
|
6 words. |
|
7 *) |
|
8 |
|
9 val mk_int = IntInf.fromInt: Int.int -> IntInf.int; |
|
10 val dest_int = IntInf.toInt: IntInf.int -> Int.int; |
|
11 |
|
12 |
|
13 (* Int *) |
|
14 |
|
15 structure OrigInt = Int; |
|
16 structure OrigIntInf = IntInf; |
|
17 type int = IntInf.int; |
|
18 |
|
19 structure IntInf = |
|
20 struct |
|
21 open IntInf; |
|
22 fun fromInt (a: int) = a; |
|
23 fun toInt (a: int) = a; |
|
24 val log2 = mk_int o IntInf.log2; |
|
25 val sign = mk_int o IntInf.sign; |
|
26 end; |
|
27 |
|
28 structure Int = IntInf; |
|
29 |
|
30 |
|
31 (* List *) |
|
32 |
|
33 structure List = |
|
34 struct |
|
35 open List; |
|
36 fun length a = mk_int (List.length a); |
|
37 fun nth (a, b) = List.nth (a, dest_int b); |
|
38 fun take (a, b) = List.take (a, dest_int b); |
|
39 fun drop (a, b) = List.drop (a, dest_int b); |
|
40 fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int); |
|
41 end; |
|
42 |
|
43 val length = List.length; |
|
44 |
|
45 |
|
46 (* Array *) |
|
47 |
|
48 structure Array = |
|
49 struct |
|
50 open Array; |
|
51 val maxLen = mk_int Array.maxLen; |
|
52 fun array (a, b) = Array.array (dest_int a, b); |
|
53 fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int); |
|
54 fun length a = mk_int (Array.length a); |
|
55 fun sub (a, b) = Array.sub (a, dest_int b); |
|
56 fun update (a, b, c) = Array.update (a, dest_int b, c); |
|
57 fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di}; |
|
58 fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di}; |
|
59 fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b; |
|
60 fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b; |
|
61 fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c; |
|
62 fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c; |
|
63 fun findi a b = |
|
64 (case Array.findi (fn (x, y) => a (mk_int x, y)) b of |
|
65 NONE => NONE |
|
66 | SOME (c, d) => SOME (mk_int c, d)); |
|
67 end; |
|
68 |
|
69 |
|
70 (* Vector *) |
|
71 |
|
72 structure Vector = |
|
73 struct |
|
74 open Vector; |
|
75 val maxLen = mk_int Vector.maxLen; |
|
76 fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int); |
|
77 fun length a = mk_int (Vector.length a); |
|
78 fun sub (a, b) = Vector.sub (a, dest_int b); |
|
79 fun update (a, b, c) = Vector.update (a, dest_int b, c); |
|
80 fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b; |
|
81 fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b; |
|
82 fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c; |
|
83 fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c; |
|
84 fun findi a b = |
|
85 (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of |
|
86 NONE => NONE |
|
87 | SOME (c, d) => SOME (mk_int c, d)); |
|
88 end; |
|
89 |
|
90 |
|
91 (* Char *) |
|
92 |
|
93 structure Char = |
|
94 struct |
|
95 open Char; |
|
96 val maxOrd = mk_int Char.maxOrd; |
|
97 val chr = Char.chr o dest_int; |
|
98 val ord = mk_int o Char.ord; |
|
99 end; |
|
100 |
|
101 val chr = Char.chr; |
|
102 val ord = Char.ord; |
|
103 |
|
104 |
|
105 (* String *) |
|
106 |
|
107 structure String = |
|
108 struct |
|
109 open String; |
|
110 val maxSize = mk_int String.maxSize; |
|
111 val size = mk_int o String.size; |
|
112 fun sub (a, b) = String.sub (a, dest_int b); |
|
113 fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c); |
|
114 fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c); |
|
115 end; |
|
116 |
|
117 val size = String.size; |
|
118 val substring = String.substring; |
|
119 |
|
120 |
|
121 (* Substring *) |
|
122 |
|
123 structure Substring = |
|
124 struct |
|
125 open Substring; |
|
126 fun sub (a, b) = Substring.sub (a, dest_int b); |
|
127 val size = mk_int o Substring.size; |
|
128 fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end; |
|
129 fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c); |
|
130 fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c); |
|
131 fun triml a b = Substring.triml (dest_int a) b; |
|
132 fun trimr a b = Substring.trimr (dest_int a) b; |
|
133 fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c); |
|
134 fun splitAt (a, b) = Substring.splitAt (a, dest_int b); |
|
135 end; |
|
136 |
|
137 |
|
138 (* Word *) |
|
139 |
|
140 structure Word = |
|
141 struct |
|
142 open Word; |
|
143 val wordSize = mk_int Word.wordSize; |
|
144 val toInt = mk_int o Word.toInt; |
|
145 val toIntX = mk_int o Word.toIntX; |
|
146 val fromInt = Word.fromInt o dest_int; |
|
147 end; |
|
148 |
|
149 |
|
150 (* Real *) |
|
151 |
|
152 structure Real = |
|
153 struct |
|
154 open Real; |
|
155 val radix = mk_int Real.radix; |
|
156 val precision = mk_int Real.precision; |
|
157 fun sign a = mk_int (Real.sign a); |
|
158 fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end; |
|
159 fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp}; |
|
160 val ceil = mk_int o Real.ceil; |
|
161 val floor = mk_int o Real.floor; |
|
162 val real = Real.fromInt o dest_int; |
|
163 val round = mk_int o Real.round; |
|
164 val trunc = mk_int o Real.trunc; |
|
165 fun toInt a b = mk_int (Real.toInt a b); |
|
166 fun fromInt a = Real.fromInt (dest_int a); |
|
167 end; |
|
168 |
|
169 val ceil = Real.ceil; |
|
170 val floor = Real.floor; |
|
171 val real = Real.real; |
|
172 val round = Real.round; |
|
173 val trunc = Real.trunc; |
|
174 |
|
175 |
|
176 (* TextIO *) |
|
177 |
|
178 structure TextIO = |
|
179 struct |
|
180 open TextIO; |
|
181 fun inputN (a, b) = TextIO.inputN (a, dest_int b); |
|
182 fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b)); |
|
183 end; |
|
184 |
|
185 |
|
186 (* Time *) |
|
187 |
|
188 structure Time = |
|
189 struct |
|
190 open Time; |
|
191 fun fmt a b = Time.fmt (dest_int a) b; |
|
192 end; |