author | wenzelm |
Sun, 09 Nov 2014 14:08:00 +0100 | |
changeset 58956 | a816aa3ff391 |
parent 53980 | 7e6a82c593f4 |
permissions | -rw-r--r-- |
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/proper_int.ML |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
4 |
SML basis with type int representing proper integers, not machine |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
5 |
words. |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
6 |
*) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
7 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
8 |
val mk_int = IntInf.fromInt: Int.int -> IntInf.int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
9 |
val dest_int = IntInf.toInt: IntInf.int -> Int.int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
10 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
11 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
12 |
(* Int *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
13 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
14 |
type int = IntInf.int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
15 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
16 |
structure IntInf = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
17 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
18 |
open IntInf; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
19 |
fun fromInt (a: int) = a; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
20 |
fun toInt (a: int) = a; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
21 |
val log2 = mk_int o IntInf.log2; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
22 |
val sign = mk_int o IntInf.sign; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
23 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
24 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
25 |
structure Int = IntInf; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
26 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
27 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
28 |
(* List *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
29 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
30 |
structure List = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
31 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
32 |
open List; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
33 |
fun length a = mk_int (List.length a); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
34 |
fun nth (a, b) = List.nth (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
35 |
fun take (a, b) = List.take (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
36 |
fun drop (a, b) = List.drop (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
37 |
fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
38 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
39 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
40 |
val length = List.length; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
41 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
42 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
43 |
(* Array *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
44 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
45 |
structure Array = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
46 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
47 |
open Array; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
48 |
val maxLen = mk_int Array.maxLen; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
49 |
fun array (a, b) = Array.array (dest_int a, b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
50 |
fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
51 |
fun length a = mk_int (Array.length a); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
52 |
fun sub (a, b) = Array.sub (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
53 |
fun update (a, b, c) = Array.update (a, dest_int b, c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
54 |
fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di}; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
55 |
fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di}; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
56 |
fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
57 |
fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
58 |
fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
59 |
fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
60 |
fun findi a b = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
61 |
(case Array.findi (fn (x, y) => a (mk_int x, y)) b of |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
62 |
NONE => NONE |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
63 |
| SOME (c, d) => SOME (mk_int c, d)); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
64 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
65 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
66 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
67 |
(* Vector *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
68 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
69 |
structure Vector = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
70 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
71 |
open Vector; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
72 |
val maxLen = mk_int Vector.maxLen; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
73 |
fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
74 |
fun length a = mk_int (Vector.length a); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
75 |
fun sub (a, b) = Vector.sub (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
76 |
fun update (a, b, c) = Vector.update (a, dest_int b, c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
77 |
fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
78 |
fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
79 |
fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
80 |
fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
81 |
fun findi a b = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
82 |
(case Vector.findi (fn (x, y) => a (mk_int x, y)) b of |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
83 |
NONE => NONE |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
84 |
| SOME (c, d) => SOME (mk_int c, d)); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
85 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
86 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
87 |
|
52277 | 88 |
(* CharVector *) |
89 |
||
90 |
structure CharVector = |
|
91 |
struct |
|
92 |
open CharVector; |
|
93 |
fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int); |
|
94 |
end; |
|
95 |
||
96 |
||
45067 | 97 |
(* Word8VectorSlice *) |
98 |
||
99 |
structure Word8VectorSlice = |
|
100 |
struct |
|
101 |
open Word8VectorSlice; |
|
102 |
val length = mk_int o Word8VectorSlice.length; |
|
103 |
fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c); |
|
104 |
end; |
|
105 |
||
106 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
107 |
(* Char *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
108 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
109 |
structure Char = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
110 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
111 |
open Char; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
112 |
val maxOrd = mk_int Char.maxOrd; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
113 |
val chr = Char.chr o dest_int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
114 |
val ord = mk_int o Char.ord; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
115 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
116 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
117 |
val chr = Char.chr; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
118 |
val ord = Char.ord; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
119 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
120 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
121 |
(* String *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
122 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
123 |
structure String = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
124 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
125 |
open String; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
126 |
val maxSize = mk_int String.maxSize; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
127 |
val size = mk_int o String.size; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
128 |
fun sub (a, b) = String.sub (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
129 |
fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
130 |
fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
131 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
132 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
133 |
val size = String.size; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
134 |
val substring = String.substring; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
135 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
136 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
137 |
(* Substring *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
138 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
139 |
structure Substring = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
140 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
141 |
open Substring; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
142 |
fun sub (a, b) = Substring.sub (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
143 |
val size = mk_int o Substring.size; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
144 |
fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
145 |
fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
146 |
fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
147 |
fun triml a b = Substring.triml (dest_int a) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
148 |
fun trimr a b = Substring.trimr (dest_int a) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
149 |
fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
150 |
fun splitAt (a, b) = Substring.splitAt (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
151 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
152 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
153 |
|
32566 | 154 |
(* StringCvt *) |
155 |
||
156 |
structure StringCvt = |
|
157 |
struct |
|
158 |
open StringCvt; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
159 |
datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option; |
32566 | 160 |
fun realfmt fmt = Real.fmt |
161 |
(case fmt of |
|
162 |
EXACT => StringCvt.EXACT |
|
163 |
| FIX NONE => StringCvt.FIX NONE |
|
164 |
| FIX (SOME b) => StringCvt.FIX (SOME (dest_int b)) |
|
165 |
| GEN NONE => StringCvt.GEN NONE |
|
166 |
| GEN (SOME b) => StringCvt.GEN (SOME (dest_int b)) |
|
167 |
| SCI NONE => StringCvt.SCI NONE |
|
168 |
| SCI (SOME b) => StringCvt.SCI (SOME (dest_int b))); |
|
52277 | 169 |
fun padRight a b c = StringCvt.padRight a (dest_int b) c; |
170 |
fun padLeft a b c = StringCvt.padLeft a (dest_int b) c; |
|
32566 | 171 |
end; |
172 |
||
173 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
174 |
(* Word *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
175 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
176 |
structure Word = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
177 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
178 |
open Word; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
179 |
val wordSize = mk_int Word.wordSize; |
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
180 |
val toInt = Word.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
181 |
val toIntX = Word.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
182 |
val fromInt = Word.fromLargeInt; |
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
183 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
184 |
|
40747 | 185 |
structure Word8 = |
186 |
struct |
|
187 |
open Word8; |
|
188 |
val wordSize = mk_int Word8.wordSize; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
189 |
val toInt = Word8.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
190 |
val toIntX = Word8.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
191 |
val fromInt = Word8.fromLargeInt; |
40747 | 192 |
end; |
193 |
||
35627 | 194 |
structure Word32 = |
195 |
struct |
|
196 |
open Word32; |
|
197 |
val wordSize = mk_int Word32.wordSize; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
198 |
val toInt = Word32.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
199 |
val toIntX = Word32.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
200 |
val fromInt = Word32.fromLargeInt; |
35627 | 201 |
end; |
202 |
||
40747 | 203 |
structure LargeWord = |
204 |
struct |
|
205 |
open LargeWord; |
|
206 |
val wordSize = mk_int LargeWord.wordSize; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
207 |
val toInt = LargeWord.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
208 |
val toIntX = LargeWord.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
209 |
val fromInt = LargeWord.fromLargeInt; |
40747 | 210 |
end; |
211 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
212 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
213 |
(* Real *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
214 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
215 |
structure Real = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
216 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
217 |
open Real; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
218 |
val radix = mk_int Real.radix; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
219 |
val precision = mk_int Real.precision; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
220 |
fun sign a = mk_int (Real.sign a); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
221 |
fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
222 |
fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp}; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
223 |
val ceil = mk_int o Real.ceil; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
224 |
val floor = mk_int o Real.floor; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
225 |
val real = Real.fromInt o dest_int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
226 |
val round = mk_int o Real.round; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
227 |
val trunc = mk_int o Real.trunc; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
228 |
fun toInt a b = mk_int (Real.toInt a b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
229 |
fun fromInt a = Real.fromInt (dest_int a); |
32566 | 230 |
val fmt = StringCvt.realfmt; |
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
231 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
232 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
233 |
val ceil = Real.ceil; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
234 |
val floor = Real.floor; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
235 |
val real = Real.real; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
236 |
val round = Real.round; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
237 |
val trunc = Real.trunc; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
238 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
239 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
240 |
(* TextIO *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
241 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
242 |
structure TextIO = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
243 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
244 |
open TextIO; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
245 |
fun inputN (a, b) = TextIO.inputN (a, dest_int b); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
246 |
fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b)); |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
247 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
248 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
249 |
|
45030 | 250 |
(* BinIO *) |
251 |
||
252 |
structure BinIO = |
|
253 |
struct |
|
254 |
open BinIO; |
|
255 |
fun inputN (a, b) = BinIO.inputN (a, dest_int b); |
|
256 |
fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b)); |
|
257 |
end; |
|
258 |
||
259 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
260 |
(* Time *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
261 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
262 |
structure Time = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
263 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
264 |
open Time; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
265 |
fun fmt a b = Time.fmt (dest_int a) b; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
266 |
end; |
24604 | 267 |
|
45030 | 268 |
|
269 |
(* Sockets *) |
|
270 |
||
271 |
structure INetSock = |
|
272 |
struct |
|
273 |
open INetSock; |
|
274 |
fun toAddr (a, b) = INetSock.toAddr (a, dest_int b); |
|
275 |
fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end; |
|
276 |
end; |
|
277 |
||
53980
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
278 |
|
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
279 |
(* OS.FileSys *) |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
280 |
|
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
281 |
structure OS = |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
282 |
struct |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
283 |
open OS; |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
284 |
structure FileSys = |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
285 |
struct |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
286 |
open FileSys; |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
287 |
fun fileSize a = mk_int (FileSys.fileSize a); |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
288 |
end; |
7e6a82c593f4
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
wenzelm
parents:
52277
diff
changeset
|
289 |
end; |