author | wenzelm |
Thu, 10 Jan 2013 13:02:06 +0100 | |
changeset 50801 | b8ff6d1ee56c |
parent 45067 | d5156aa8556d |
child 52277 | 2bbeab01c0ea |
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 |
|
45067 | 88 |
(* Word8VectorSlice *) |
89 |
||
90 |
structure Word8VectorSlice = |
|
91 |
struct |
|
92 |
open Word8VectorSlice; |
|
93 |
val length = mk_int o Word8VectorSlice.length; |
|
94 |
fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c); |
|
95 |
end; |
|
96 |
||
97 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
98 |
(* Char *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
99 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
100 |
structure Char = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
101 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
102 |
open Char; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
103 |
val maxOrd = mk_int Char.maxOrd; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
104 |
val chr = Char.chr o dest_int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
105 |
val ord = mk_int o Char.ord; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
106 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
107 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
108 |
val chr = Char.chr; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
109 |
val ord = Char.ord; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
110 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
111 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
112 |
(* String *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
113 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
114 |
structure String = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
115 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
116 |
open String; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
117 |
val maxSize = mk_int String.maxSize; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
118 |
val size = mk_int o String.size; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
123 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
124 |
val size = String.size; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
125 |
val substring = String.substring; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
126 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
127 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
128 |
(* Substring *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
129 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
130 |
structure Substring = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
131 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
132 |
open Substring; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
133 |
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
|
134 |
val size = mk_int o Substring.size; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
143 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
144 |
|
32566 | 145 |
(* StringCvt *) |
146 |
||
147 |
structure StringCvt = |
|
148 |
struct |
|
149 |
open StringCvt; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
150 |
datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option; |
32566 | 151 |
fun realfmt fmt = Real.fmt |
152 |
(case fmt of |
|
153 |
EXACT => StringCvt.EXACT |
|
154 |
| FIX NONE => StringCvt.FIX NONE |
|
155 |
| FIX (SOME b) => StringCvt.FIX (SOME (dest_int b)) |
|
156 |
| GEN NONE => StringCvt.GEN NONE |
|
157 |
| GEN (SOME b) => StringCvt.GEN (SOME (dest_int b)) |
|
158 |
| SCI NONE => StringCvt.SCI NONE |
|
159 |
| SCI (SOME b) => StringCvt.SCI (SOME (dest_int b))); |
|
160 |
end; |
|
161 |
||
162 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
163 |
(* Word *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
164 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
165 |
structure Word = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
166 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
167 |
open Word; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
168 |
val wordSize = mk_int Word.wordSize; |
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
169 |
val toInt = Word.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
170 |
val toIntX = Word.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
171 |
val fromInt = Word.fromLargeInt; |
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
172 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
173 |
|
40747 | 174 |
structure Word8 = |
175 |
struct |
|
176 |
open Word8; |
|
177 |
val wordSize = mk_int Word8.wordSize; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
178 |
val toInt = Word8.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
179 |
val toIntX = Word8.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
180 |
val fromInt = Word8.fromLargeInt; |
40747 | 181 |
end; |
182 |
||
35627 | 183 |
structure Word32 = |
184 |
struct |
|
185 |
open Word32; |
|
186 |
val wordSize = mk_int Word32.wordSize; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
187 |
val toInt = Word32.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
188 |
val toIntX = Word32.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
189 |
val fromInt = Word32.fromLargeInt; |
35627 | 190 |
end; |
191 |
||
40747 | 192 |
structure LargeWord = |
193 |
struct |
|
194 |
open LargeWord; |
|
195 |
val wordSize = mk_int LargeWord.wordSize; |
|
41619
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
196 |
val toInt = LargeWord.toLargeInt; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
197 |
val toIntX = LargeWord.toLargeIntX; |
6cac9f48f96a
Word: direct conversion wrt. LargeInt to bypass exception Overflow;
wenzelm
parents:
40747
diff
changeset
|
198 |
val fromInt = LargeWord.fromLargeInt; |
40747 | 199 |
end; |
200 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
201 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
202 |
(* Real *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
203 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
204 |
structure Real = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
205 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
206 |
open Real; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
207 |
val radix = mk_int Real.radix; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
208 |
val precision = mk_int Real.precision; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
209 |
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
|
210 |
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
|
211 |
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
|
212 |
val ceil = mk_int o Real.ceil; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
213 |
val floor = mk_int o Real.floor; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
214 |
val real = Real.fromInt o dest_int; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
215 |
val round = mk_int o Real.round; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
216 |
val trunc = mk_int o Real.trunc; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
217 |
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
|
218 |
fun fromInt a = Real.fromInt (dest_int a); |
32566 | 219 |
val fmt = StringCvt.realfmt; |
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
220 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
221 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
222 |
val ceil = Real.ceil; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
223 |
val floor = Real.floor; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
224 |
val real = Real.real; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
225 |
val round = Real.round; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
226 |
val trunc = Real.trunc; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
227 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
228 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
229 |
(* TextIO *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
230 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
231 |
structure TextIO = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
232 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
233 |
open TextIO; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
234 |
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
|
235 |
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
|
236 |
end; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
237 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
238 |
|
45030 | 239 |
(* BinIO *) |
240 |
||
241 |
structure BinIO = |
|
242 |
struct |
|
243 |
open BinIO; |
|
244 |
fun inputN (a, b) = BinIO.inputN (a, dest_int b); |
|
245 |
fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b)); |
|
246 |
end; |
|
247 |
||
248 |
||
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
249 |
(* Time *) |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
250 |
|
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
251 |
structure Time = |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
252 |
struct |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
253 |
open Time; |
0683a2fc4041
moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML;
wenzelm
parents:
diff
changeset
|
254 |
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
|
255 |
end; |
24604 | 256 |
|
45030 | 257 |
|
258 |
(* Sockets *) |
|
259 |
||
260 |
structure INetSock = |
|
261 |
struct |
|
262 |
open INetSock; |
|
263 |
fun toAddr (a, b) = INetSock.toAddr (a, dest_int b); |
|
264 |
fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end; |
|
265 |
end; |
|
266 |