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