author  wenzelm 
Sun, 31 May 2009 14:51:21 +0200  
changeset 31312  1c00e4ff3c99 
parent 29564  f8b933a62151 
child 32566  e6b66a59bed6 
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 
Author: Makarius 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

3 

0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/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/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

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

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

7 

24597  8 
val ml_system_fix_ints = true; 
9 

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

10 
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

11 
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

12 

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 
(* Int *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

15 

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

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

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

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

19 

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

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

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

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

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

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

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

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

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

28 

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

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

30 

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 
(* List *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

33 

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

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

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

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

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

38 
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

39 
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

40 
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

41 
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

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

43 

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

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

45 

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 
(* Array *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

48 

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

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

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

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

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

53 
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

54 
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

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

56 
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

57 
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

58 
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

59 
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

60 
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

61 
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

62 
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

63 
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

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

65 
(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

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

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

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

69 

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 
(* Vector *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

72 

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

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

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

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

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

77 
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

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

79 
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

80 
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

81 
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

82 
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

83 
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

84 
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

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

86 
(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

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

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

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

90 

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 
(* Char *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

93 

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

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

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

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

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

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

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

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

101 

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

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

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

104 

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 
(* String *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

107 

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

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

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

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

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

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

113 
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

114 
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

115 
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

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

117 

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

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

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

120 

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 
(* Substring *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

123 

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

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

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

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

127 
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

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

129 
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

130 
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

131 
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

132 
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

133 
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

134 
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

135 
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

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

137 

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 
(* Word *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

140 

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

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

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

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

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

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

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

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

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

149 

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 
(* Real *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

152 

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

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

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

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

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

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

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

159 
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

160 
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

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

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

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

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

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

166 
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

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

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

169 

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

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

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

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

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

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

175 

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 
(* TextIO *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

178 

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

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

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

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

182 
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

183 
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

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

185 

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 
(* Time *) 
0683a2fc4041
moved Admin/proper_int.ML to Pure/MLSystems/proper_int.ML;
wenzelm
parents:
diff
changeset

188 

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

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

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

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

192 
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

193 
end; 
24604  194 