author  wenzelm 
Fri, 03 Oct 2008 21:06:38 +0200  
changeset 28490  40c3f900c457 
parent 24604  d5c5d2e13fbf 
child 29564  f8b933a62151 
permissions  rwrr 
24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/proper_int.ML 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

4 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

5 
SML basis with type int representing proper integers, not machine 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

6 
words. 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

7 
*) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

8 

24597  9 
val ml_system_fix_ints = true; 
10 

24140
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

11 
val mk_int = IntInf.fromInt: Int.int > IntInf.int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

12 
val dest_int = IntInf.toInt: IntInf.int > Int.int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

13 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

14 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

15 
(* Int *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

16 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

17 
structure OrigInt = Int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

18 
structure OrigIntInf = IntInf; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

19 
type int = IntInf.int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

20 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

21 
structure IntInf = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

22 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

23 
open IntInf; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

24 
fun fromInt (a: int) = a; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

25 
fun toInt (a: int) = a; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

26 
val log2 = mk_int o IntInf.log2; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

27 
val sign = mk_int o IntInf.sign; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

28 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

29 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

30 
structure Int = IntInf; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

31 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

32 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

33 
(* List *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

34 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

35 
structure List = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

36 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

37 
open List; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

38 
fun length a = mk_int (List.length a); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

39 
fun nth (a, b) = List.nth (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

40 
fun take (a, b) = List.take (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

41 
fun drop (a, b) = List.drop (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

42 
fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

43 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

44 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

45 
val length = List.length; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

46 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

47 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

48 
(* Array *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

49 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

50 
structure Array = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

51 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

52 
open Array; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

53 
val maxLen = mk_int Array.maxLen; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

54 
fun array (a, b) = Array.array (dest_int a, b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

55 
fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

56 
fun length a = mk_int (Array.length a); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

57 
fun sub (a, b) = Array.sub (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

58 
fun update (a, b, c) = Array.update (a, dest_int b, c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

59 
fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di}; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

60 
fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di}; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

61 
fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

62 
fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

63 
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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

64 
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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

65 
fun findi a b = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

66 
(case Array.findi (fn (x, y) => a (mk_int x, y)) b of 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

67 
NONE => NONE 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

68 
 SOME (c, d) => SOME (mk_int c, d)); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

69 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

70 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

71 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

72 
(* Vector *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

73 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

74 
structure Vector = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

75 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

76 
open Vector; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

77 
val maxLen = mk_int Vector.maxLen; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

78 
fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

79 
fun length a = mk_int (Vector.length a); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

80 
fun sub (a, b) = Vector.sub (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

81 
fun update (a, b, c) = Vector.update (a, dest_int b, c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

82 
fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

83 
fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

84 
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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

85 
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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

86 
fun findi a b = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

87 
(case Vector.findi (fn (x, y) => a (mk_int x, y)) b of 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

88 
NONE => NONE 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

89 
 SOME (c, d) => SOME (mk_int c, d)); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

90 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

91 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

92 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

93 
(* Char *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

94 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

95 
structure Char = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

96 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

97 
open Char; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

98 
val maxOrd = mk_int Char.maxOrd; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

99 
val chr = Char.chr o dest_int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

100 
val ord = mk_int o Char.ord; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

101 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

102 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

103 
val chr = Char.chr; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

104 
val ord = Char.ord; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

105 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

106 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

107 
(* String *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

108 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

109 
structure String = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

110 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

111 
open String; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

112 
val maxSize = mk_int String.maxSize; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

113 
val size = mk_int o String.size; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

114 
fun sub (a, b) = String.sub (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

115 
fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

116 
fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

117 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

118 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

119 
val size = String.size; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

120 
val substring = String.substring; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

121 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

122 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

123 
(* Substring *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

124 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

125 
structure Substring = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

126 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

127 
open Substring; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

128 
fun sub (a, b) = Substring.sub (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

129 
val size = mk_int o Substring.size; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

130 
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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

131 
fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

132 
fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

133 
fun triml a b = Substring.triml (dest_int a) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

134 
fun trimr a b = Substring.trimr (dest_int a) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

135 
fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

136 
fun splitAt (a, b) = Substring.splitAt (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

137 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

138 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

139 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

140 
(* Word *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

141 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

142 
structure Word = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

143 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

144 
open Word; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

145 
val wordSize = mk_int Word.wordSize; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

146 
val toInt = mk_int o Word.toInt; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

147 
val toIntX = mk_int o Word.toIntX; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

148 
val fromInt = Word.fromInt o dest_int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

149 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

150 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

151 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

152 
(* Real *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

153 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

154 
structure Real = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

155 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

156 
open Real; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

157 
val radix = mk_int Real.radix; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

158 
val precision = mk_int Real.precision; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

159 
fun sign a = mk_int (Real.sign a); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

160 
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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

161 
fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp}; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

162 
val ceil = mk_int o Real.ceil; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

163 
val floor = mk_int o Real.floor; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

164 
val real = Real.fromInt o dest_int; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

165 
val round = mk_int o Real.round; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

166 
val trunc = mk_int o Real.trunc; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

167 
fun toInt a b = mk_int (Real.toInt a b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

168 
fun fromInt a = Real.fromInt (dest_int a); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

169 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

170 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

171 
val ceil = Real.ceil; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

172 
val floor = Real.floor; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

173 
val real = Real.real; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

174 
val round = Real.round; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

175 
val trunc = Real.trunc; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

176 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

177 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

178 
(* TextIO *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

179 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

180 
structure TextIO = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

181 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

182 
open TextIO; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

183 
fun inputN (a, b) = TextIO.inputN (a, dest_int b); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

184 
fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b)); 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

185 
end; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

186 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

187 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

188 
(* Time *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

189 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

190 
structure Time = 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

191 
struct 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

192 
open Time; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

193 
fun fmt a b = Time.fmt (dest_int a) b; 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

194 
end; 
24604  195 