1(* Author: Michael Norrish *)
2
3structure Arbintcore :> Arbintcore =
4struct
5
6type num = Arbnumcore.num
7type int = bool * num
8
9(* representation has first component true if the integer is >= 0 *)
10
11infix ++ -- ** <<
12infix 7 ddiv mmod
13
14val op ++ = Arbnumcore.+
15val op -- = Arbnumcore.-
16val op ** = Arbnumcore.*
17val op << = Arbnumcore.<
18val op ddiv = Arbnumcore.div
19val op mmod = Arbnumcore.mod
20val AZ = Arbnumcore.zero
21
22val zero = (true, Arbnumcore.zero)
23val one = (true, Arbnumcore.one)
24val two = (true, Arbnumcore.two)
25
26fun norm_zeros (i as (b,n)) = if not b andalso n = AZ then (true, AZ) else i
27
28fun ((true, n1) + (true, n2)) = (true, n1 ++ n2)
29  | ((true, n1) + (false, n2)) = if n1 << n2 then (false, n2 -- n1) else (true, n1 -- n2)
30  | ((false, n1) + (true, n2)) = if n2 << n1 then (false, n1 -- n2) else (true, n2 -- n1)
31  | ((false, n1) + (false, n2)) = (false, n1 ++ n2)
32
33fun negate (true, n) = if n = AZ then (true, n) else (false, n)
34  | negate (false, n) = (true, n)
35val op~ = negate
36
37fun i - j = i + negate j
38
39fun ((true, n1) * (true, n2)) = (true, n1 ** n2)
40  | ((true, n1) * (false, n2)) = if n1 = AZ then (true, AZ) else (false, n1 ** n2)
41  | ((false, n1) * (true, n2)) = if n2 = AZ then (true, AZ) else (false, n1 ** n2)
42  | ((false, n1) * (false, n2)) = (true, n1 ** n2)
43
44fun ((true, n1) div (true, n2)) = (true, n1 ddiv n2)
45  | ((true, n1) div (false, n2)) = let val (q,r) = Arbnumcore.divmod(n1, n2)
46                                   in if r <> Arbnumcore.zero then
47                                        (false, q ++ Arbnumcore.one)
48                                      else norm_zeros (false, q)
49                                   end
50  | ((false, n1) div (true, n2)) = let val (q,r) = Arbnumcore.divmod(n1, n2)
51                                   in if r <> Arbnumcore.zero then
52                                        (false, q ++ Arbnumcore.one)
53                                      else norm_zeros (false, q)
54                                   end
55  | ((false, n1) div (false, n2)) = (true, n1 ddiv n2)
56
57fun ((true, n1) mod (true, n2)) = (true, n1 mmod n2)
58  | ((true, n1) mod (false, n2)) = let val m = n1 mmod n2
59                                   in
60                                     if m = AZ then zero else (false, n2 -- m)
61                                   end
62  | ((false, n1) mod (true, n2)) = let val m = n1 mmod n2
63                                   in
64                                     if m = AZ then zero else (true, n2 -- m)
65                                   end
66  | ((false, n1) mod (false, n2)) = norm_zeros (false, n1 mmod n2)
67
68infix 7 quot rem
69
70fun ((true, n1) quot (true, n2)) = (true, n1 ddiv n2)
71  | ((true, n1) quot (false, n2)) = norm_zeros (false, n1 ddiv n2)
72  | ((false, n1) quot (true, n2)) = norm_zeros (false, n1 ddiv n2)
73  | ((false, n1) quot (false, n2)) = (true, n1 ddiv n2)
74
75fun ((true, n1) rem (true, n2)) = (true, n1 mmod n2)
76  | ((true, n1) rem (false, n2)) = norm_zeros (false, n1 mmod n2)
77  | ((false, n1) rem (true, n2)) = norm_zeros (false, n1 mmod n2)
78  | ((false, n1) rem (false, n2)) = (true, n1 mmod n2)
79
80fun quotrem(i,j) = (i quot j, i rem j)
81
82fun (true, n1) < (true, n2) = n1 << n2
83  | (true, _) < (false, _) = false
84  | (false, _) < (true, _) = true
85  | (false, n1) < (false, n2) = n2 << n1
86fun i <= j = i = j orelse i < j
87fun i > j = j < i
88fun i >= j = i = j orelse i > j
89
90fun compare(i,j) = if i < j then LESS
91                   else if i = j then EQUAL
92                        else GREATER
93
94fun divmod (i, j) = (i div j, i mod j)
95
96fun toString (true, n) = Arbnumcore.toString n ^ "i"
97  | toString (false, n) = "-" ^ Arbnumcore.toString n ^ "i"
98
99fun fromString s = let
100  open Substring
101  val (pfx, rest) = splitl (fn c => c = #"-" orelse c = #"~") (full s)
102  val is_positive = Int.mod(size pfx, 2) = 0
103in
104  (is_positive, Arbnumcore.fromString (string rest))
105end
106
107fun toInt (true, n) = Arbnumcore.toInt n
108  | toInt (false, n) = Int.-(0, Arbnumcore.toInt n)
109fun toNat (true, n) = n
110  | toNat (false, _) = raise Fail "Attempt to make negative integer a nat"
111fun fromInt n =
112  if (Int.<(n,0)) then (false, Arbnumcore.fromInt(Int.-(0, n)))
113  else (true, Arbnumcore.fromInt n)
114
115
116fun min (i,j) = if i < j then i else j
117fun max (i,j) = if i < j then j else i
118
119fun abs (_, n) = (true, n)
120
121fun fromNat n = (true, n)
122
123end
124