# HG changeset patch # User haftmann # Date 1181063970 -7200 # Node ID 85f27f79232f12b2a69d493af61cffa0393b94c3 # Parent eb6d86fb7ed38d642ff49e4c24c3926fb963ab6f tuned integers diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Library/comm_ring.ML --- a/src/HOL/Library/comm_ring.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/HOL/Library/comm_ring.ML Tue Jun 05 19:19:30 2007 +0200 @@ -46,7 +46,7 @@ in if i = 0 then pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T) - else pol_Pinj T $ HOLogic.mk_nat (Intt.int i) + else pol_Pinj T $ HOLogic.mk_nat (Integer.int i) $ (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)) end diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Jun 05 19:19:30 2007 +0200 @@ -14,8 +14,8 @@ val approx_vector : int -> (float -> float) -> vector -> term * term val approx_matrix : int -> (float -> float) -> matrix -> term * term - val mk_spvec_entry : Intt.int -> float -> term - val mk_spmat_entry : Intt.int -> term -> term + val mk_spvec_entry : integer -> float -> term + val mk_spmat_entry : integer -> term -> term val spvecT: typ val spmatT: typ @@ -64,7 +64,7 @@ fun app (index, s) (lower, upper) = let val (flower, fupper) = approx_value prec pprt s - val index = HOLogic.mk_number HOLogic.natT (Intt.int index) + val index = HOLogic.mk_number HOLogic.natT (Integer.int index) val elower = HOLogic.mk_prod (index, flower) val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; @@ -77,7 +77,7 @@ fun app (index, v) (lower, upper) = let val (flower, fupper) = approx_vector prec pprt v - val index = HOLogic.mk_number HOLogic.natT (Intt.int index) + val index = HOLogic.mk_number HOLogic.natT (Integer.int index) val elower = HOLogic.mk_prod (index, flower) val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Tue Jun 05 19:19:30 2007 +0200 @@ -207,8 +207,8 @@ fun test_1 (lower, upper) = if lower = upper then - (if Float.eq (lower, (Intt.int ~1, Intt.zero)) then ~1 - else if Float.eq (lower, (Intt.int 1, Intt.zero)) then 1 + (if Float.eq (lower, (Integer.int ~1, Integer.zero)) then ~1 + else if Float.eq (lower, (Integer.int 1, Integer.zero)) then 1 else 0) else 0 @@ -288,7 +288,7 @@ val b1 = case Inttab.lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x val b2 = case Inttab.lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x val abs_max = Float.max (Float.neg (Float.negative_part b1)) (Float.positive_part b2) - val i' = Intt.int index + val i' = Integer.int index in (add_row_entry r i' abs_max, (add_row_entry r12_1 i' b1, add_row_entry r12_2 i' b2)) end diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Real/ferrante_rackoff_proof.ML --- a/src/HOL/Real/ferrante_rackoff_proof.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML Tue Jun 05 19:19:30 2007 +0200 @@ -310,7 +310,7 @@ prove_bysimp thy (simpset_of thy) (HOLogic.mk_eq(HOLogic.mk_binop @{const_name HOL.plus} (mk_real m,mk_real n),mk_real (m+n))); fun provediv thy m n = - let val g = gcd (m,n) + let val g = Integer.gcd m n val m' = m div g val n'= n div g in @@ -391,7 +391,7 @@ val ts = prove_naddh thy vs (t,s) in [nm,ts] MRS nadd_cong_same end - else let val l = lcm (m,n) + else let val l = Integer.lcm m n val m' = l div m val n' = l div n val mml = proveprod thy m' m diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Real/float_arith.ML --- a/src/HOL/Real/float_arith.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/HOL/Real/float_arith.ML Tue Jun 05 19:19:30 2007 +0200 @@ -9,7 +9,7 @@ val destruct_floatstr: (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string exception Floating_point of string - val approx_dec_by_bin: Intt.int -> Float.float -> Float.float * Float.float + val approx_dec_by_bin: integer -> Float.float -> Float.float * Float.float val approx_decstr_by_bin: int -> string -> Float.float * Float.float val mk_float: Float.float -> term @@ -85,39 +85,39 @@ exception Floating_point of string; val ln2_10 = Math.ln 10.0 / Math.ln 2.0; -val exp5 = Intt.pow (Intt.int 5); -val exp10 = Intt.pow (Intt.int 10); +val exp5 = Integer.pow (Integer.int 5); +val exp10 = Integer.pow (Integer.int 10); -fun intle a b = not (Intt.cmp (a, b) = GREATER); -fun intless a b = Intt.cmp (a, b) = LESS; +fun intle a b = not (Integer.cmp (a, b) = GREATER); +fun intless a b = Integer.cmp (a, b) = LESS; fun find_most_significant q r = let fun int2real i = - case (Real.fromString o Intt.string_of_int) i of + case (Real.fromString o Integer.string_of_int) i of SOME r => r | NONE => raise (Floating_point "int2real") fun subtract (q, r) (q', r') = if intle r r' then - (Intt.sub q (Intt.mult q' (exp10 (Intt.sub r' r))), r) + (Integer.sub q (Integer.mult q' (exp10 (Integer.sub r' r))), r) else - (Intt.sub (Intt.mult q (exp10 (Intt.sub r r'))) q', r') + (Integer.sub (Integer.mult q (exp10 (Integer.sub r r'))) q', r') fun bin2dec d = - if intle Intt.zero d then - (Intt.exp d, Intt.zero) + if intle Integer.zero d then + (Integer.exp d, Integer.zero) else - (exp5 (Intt.neg d), d) + (exp5 (Integer.neg d), d) - val L = Intt.int (Real.floor (int2real (Intt.log q) + int2real r * ln2_10)) - val L1 = Intt.inc L + val L = Integer.int (Real.floor (int2real (Integer.log q) + int2real r * ln2_10)) + val L1 = Integer.inc L val (q1, r1) = subtract (q, r) (bin2dec L1) in - if intle Intt.zero q1 then + if intle Integer.zero q1 then let - val (q2, r2) = subtract (q, r) (bin2dec (Intt.inc L1)) + val (q2, r2) = subtract (q, r) (bin2dec (Integer.inc L1)) in - if intle Intt.zero q2 then + if intle Integer.zero q2 then raise (Floating_point "find_most_significant") else (L1, (q1, r1)) @@ -126,7 +126,7 @@ let val (q0, r0) = subtract (q, r) (bin2dec L) in - if intle Intt.zero q0 then + if intle Integer.zero q0 then (L, (q0, r0)) else raise (Floating_point "find_most_significant") @@ -136,13 +136,13 @@ fun approx_dec_by_bin n (q,r) = let fun addseq acc d' [] = acc - | addseq acc d' (d::ds) = addseq (Intt.add acc (Intt.exp (Intt.sub d d'))) d' ds + | addseq acc d' (d::ds) = addseq (Integer.add acc (Integer.exp (Integer.sub d d'))) d' ds - fun seq2bin [] = (Intt.zero, Intt.zero) - | seq2bin (d::ds) = (Intt.inc (addseq Intt.zero d ds), d) + fun seq2bin [] = (Integer.zero, Integer.zero) + | seq2bin (d::ds) = (Integer.inc (addseq Integer.zero d ds), d) fun approx d_seq d0 precision (q,r) = - if q = Intt.zero then + if q = Integer.zero then let val x = seq2bin d_seq in (x, x) end @@ -150,13 +150,13 @@ let val (d, (q', r')) = find_most_significant q r in - if intless precision (Intt.sub d0 d) then + if intless precision (Integer.sub d0 d) then let - val d' = Intt.sub d0 precision + val d' = Integer.sub d0 precision val x1 = seq2bin (d_seq) - val x2 = (Intt.inc - (Intt.mult (fst x1) - (Intt.exp (Intt.sub (snd x1) d'))), d') (* = seq2bin (d'::d_seq) *) + val x2 = (Integer.inc + (Integer.mult (fst x1) + (Integer.exp (Integer.sub (snd x1) d'))), d') (* = seq2bin (d'::d_seq) *) in (x1, x2) end @@ -165,47 +165,47 @@ end fun approx_start precision (q, r) = - if q = Intt.zero then - ((Intt.zero, Intt.zero), (Intt.zero, Intt.zero)) + if q = Integer.zero then + ((Integer.zero, Integer.zero), (Integer.zero, Integer.zero)) else let val (d, (q', r')) = find_most_significant q r in - if intle precision Intt.zero then + if intle precision Integer.zero then let val x1 = seq2bin [d] in - if q' = Intt.zero then + if q' = Integer.zero then (x1, x1) else - (x1, seq2bin [Intt.inc d]) + (x1, seq2bin [Integer.inc d]) end else approx [d] d precision (q', r') end in - if intle Intt.zero q then + if intle Integer.zero q then approx_start n (q,r) else let - val ((a1,b1), (a2, b2)) = approx_start n (Intt.neg q, r) + val ((a1,b1), (a2, b2)) = approx_start n (Integer.neg q, r) in - ((Intt.neg a2, b2), (Intt.neg a1, b1)) + ((Integer.neg a2, b2), (Integer.neg a1, b1)) end end fun approx_decstr_by_bin n decstr = let - fun str2int s = the_default Intt.zero (Intt.int_of_string s); - fun signint p x = if p then x else Intt.neg x + fun str2int s = the_default Integer.zero (Integer.int_of_string s); + fun signint p x = if p then x else Integer.neg x val (p, d1, d2, ep, e) = destruct_floatstr Char.isDigit (fn e => e = #"e" orelse e = #"E") decstr - val s = Intt.int (size d2) + val s = Integer.int (size d2) - val q = signint p (Intt.add (Intt.mult (str2int d1) (exp10 s)) (str2int d2)) - val r = Intt.sub (signint ep (str2int e)) s + val q = signint p (Integer.add (Integer.mult (str2int d1) (exp10 s)) (str2int d2)) + val r = Integer.sub (signint ep (str2int e)) s in - approx_dec_by_bin (Intt.int n) (q,r) + approx_dec_by_bin (Integer.int n) (q,r) end fun mk_float (a, b) = @{term "float"} $ @@ -213,7 +213,7 @@ fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) = pairself (snd o HOLogic.dest_number) (a, b) - | dest_float t = ((snd o HOLogic.dest_number) t, Intt.zero); + | dest_float t = ((snd o HOLogic.dest_number) t, Integer.zero); fun approx_float prec f value = let diff -r eb6d86fb7ed3 -r 85f27f79232f src/HOL/Tools/Presburger/cooper_dec.ML --- a/src/HOL/Tools/Presburger/cooper_dec.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML Tue Jun 05 19:19:30 2007 +0200 @@ -222,7 +222,6 @@ (* ------------------------------------------------------------------------- *) (*gcd calculates gcd (a,b) and helps lcm_num calculating lcm (a,b)*) -(*BEWARE: replaces Library.gcd!! There is also Library.lcm!*) fun gcd (a:IntInf.int) b = if a=0 then b else gcd (b mod a) a ; fun lcm_num a b = (abs a*b) div (gcd (abs a) (abs b)); diff -r eb6d86fb7ed3 -r 85f27f79232f src/Provers/Arith/cancel_factor.ML --- a/src/Provers/Arith/cancel_factor.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/Provers/Arith/cancel_factor.ML Tue Jun 05 19:19:30 2007 +0200 @@ -14,8 +14,9 @@ val dest_bal: term -> term * term (*rules*) val prove_conv: tactic -> tactic -> Proof.context -> term * term -> thm - val norm_tac: tactic (*AC0 etc.*) - val multiply_tac: IntInf.int -> tactic (*apply a ~~ b == k * a ~~ k * b (for k > 0)*) + val norm_tac: tactic (*AC0 etc.*) + val multiply_tac: integer -> tactic + (*apply a ~~ b == k * a ~~ k * b (for k > 0)*) end; signature CANCEL_FACTOR = @@ -28,14 +29,6 @@ struct -(* greatest common divisor *) - -fun gcd (0, n) = n - | gcd (m, n) = gcd (n mod m, m); - -val gcds = foldl gcd; - - (* count terms *) fun ins_term (t, []) = [(t, 1)] @@ -48,8 +41,8 @@ (* divide sum *) -fun div_sum d tks = - Data.mk_sum (flat (map (fn (t, k) => replicate (k div d) t) tks)); +fun div_sum d = + Data.mk_sum o maps (fn (t, k) => replicate (k div d) t); (* the simplification procedure *) @@ -64,12 +57,15 @@ | ts_us => let val (tks, uks) = pairself count_terms ts_us; - val d = gcds (gcds (0, map snd tks), map snd uks); + val d = 0 + |> fold (Integer.gcd o snd) tks + |> fold (Integer.gcd o snd) uks; + val d' = Integer.machine_int d; in if d = 0 orelse d = 1 then NONE else SOME (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss) - (t, Data.mk_bal (div_sum d tks, div_sum d uks))) + (t, Data.mk_bal (div_sum d' tks, div_sum d' uks))) end)); diff -r eb6d86fb7ed3 -r 85f27f79232f src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Tue Jun 05 19:19:30 2007 +0200 @@ -57,7 +57,7 @@ and (m2, t2') = Data.dest_coeff t2 val d = (*if both are negative, also divide through by ~1*) if (m1<0 andalso m2<=0) orelse - (m1<=0 andalso m2<0) then ~ (abs(gcd(m1,m2))) else abs (gcd(m1,m2)) + (m1<=0 andalso m2<0) then ~ (abs (Integer.gcd m1 m2)) else abs (Integer.gcd m1 m2) val _ = if d=1 then (*trivial, so do nothing*) raise TERM("cancel_numeral_factor", []) else () diff -r eb6d86fb7ed3 -r 85f27f79232f src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Jun 05 19:19:30 2007 +0200 @@ -308,7 +308,7 @@ fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = let val c1 = nth l1 v and c2 = nth l2 v - val m = lcm(abs c1, abs c2) + val m = Integer.lcm (abs c1) (abs c2) val m1 = m div (abs c1) and m2 = m div (abs c2) val (n1,n2) = if (c1 >= 0) = (c2 >= 0) @@ -498,10 +498,10 @@ end end; -fun coeff poly atom : IntInf.int = - AList.lookup (op =) poly atom |> the_default 0; +fun coeff poly atom = + AList.lookup (op =) poly atom |> the_default Integer.zero; -fun lcms (is : IntInf.int list) : IntInf.int = Library.foldl lcm (1, is); +fun lcms ks = fold Integer.lcm ks Integer.one; fun integ(rlhs,r,rel,rrhs,s,d) = let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s diff -r eb6d86fb7ed3 -r 85f27f79232f src/Tools/float.ML --- a/src/Tools/float.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/Tools/float.ML Tue Jun 05 19:19:30 2007 +0200 @@ -7,7 +7,7 @@ signature FLOAT = sig - type float = Intt.int * Intt.int + type float = integer * integer val zero: float val eq: float * float -> bool val cmp: float * float -> order @@ -25,27 +25,27 @@ structure Float : FLOAT = struct -type float = Intt.int * Intt.int; +type float = integer * integer; -val zero = (Intt.zero, Intt.zero); +val zero = (Integer.zero, Integer.zero); fun add (a1, b1) (a2, b2) = - if Intt.cmp (b1, b2) = LESS then - (Intt.add a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1) + if Integer.cmp (b1, b2) = LESS then + (a1 +% a2 *% Integer.exp (b2 -% b1), b1) else - (Intt.add (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2); + (a1 *% Integer.exp (b1 -% b2) +% a2, b2); fun sub (a1, b1) (a2, b2) = - if Intt.cmp (b1, b2) = LESS then - (Intt.sub a1 (Intt.mult a2 (Intt.exp (Intt.sub b2 b1))), b1) + if Integer.cmp (b1, b2) = LESS then + (a1 -% a2 *% Integer.exp (b2 -% b1), b1) else - (Intt.sub (Intt.mult a1 (Intt.exp (Intt.sub b1 b2))) a2, b2); + (a1 *% Integer.exp (b1 -% b2) -% a2, b2); -fun neg (a, b) = (Intt.neg a, b); +fun neg (a, b) = (Integer.neg a, b); -fun mult (a1, b1) (a2, b2) = (Intt.mult a1 a2, Intt.add b1 b2); +fun mult (a1, b1) (a2, b2) = (a1 *% a2, b1 +% b2); -fun cmp_zero (a, b) = Intt.cmp_zero a; +fun cmp_zero (a, b) = Integer.cmp_zero a; fun cmp (r, s) = cmp_zero (sub r s); @@ -54,7 +54,7 @@ fun min r s = case cmp (r, s) of LESS => r | _ => s; fun max r s = case cmp (r, s) of LESS => s | _ => r; -fun positive_part (a, b) = (Intt.max Intt.zero a, b); -fun negative_part (a, b) = (Intt.min Intt.zero a, b); +fun positive_part (a, b) = (Integer.max Integer.zero a, b); +fun negative_part (a, b) = (Integer.min Integer.zero a, b); end; diff -r eb6d86fb7ed3 -r 85f27f79232f src/Tools/rat.ML --- a/src/Tools/rat.ML Tue Jun 05 18:36:10 2007 +0200 +++ b/src/Tools/rat.ML Tue Jun 05 19:19:30 2007 +0200 @@ -12,9 +12,9 @@ val zero: rat val one: rat val two: rat - val rat_of_int: Intt.int -> rat - val rat_of_quotient: Intt.int * Intt.int -> rat - val quotient_of_rat: rat -> Intt.int * Intt.int + val rat_of_int: integer -> rat + val rat_of_quotient: integer * integer -> rat + val quotient_of_rat: rat -> integer * integer val string_of_rat: rat -> string val eq: rat * rat -> bool val cmp: rat * rat -> order @@ -32,53 +32,59 @@ structure Rat : RAT = struct -datatype rat = Rat of bool * Intt.int * Intt.int; +datatype rat = Rat of bool * integer * integer; exception DIVZERO; -val zero = Rat (true, Intt.int 0, Intt.int 1); -val one = Rat (true, Intt.int 1, Intt.int 1); -val two = Rat (true, Intt.int 2, Intt.int 1); +val zero = Rat (true, Integer.zero, Integer.one); +val one = Rat (true, Integer.one, Integer.one); +val two = Rat (true, Integer.two, Integer.one); fun rat_of_int i = - if i < Intt.int 0 - then Rat (false, ~i, Intt.int 1) - else Rat (true, i, Intt.int 1); + let + val (a, p) = Integer.signabs i + in Rat (a, p, Integer.one) end; fun norm (a, p, q) = - if p = Intt.int 0 then Rat (true, Intt.int 0, Intt.int 1) + if Integer.cmp_zero p = EQUAL then Rat (true, Integer.zero, Integer.one) else let - val absp = abs p - val m = gcd (absp, q) - in Rat(a = (Intt.int 0 <= p), absp div m, q div m) end; + val (b, absp) = Integer.signabs p; + val m = Integer.gcd absp q; + in Rat (a = b, Integer.div absp m, Integer.div q m) end; fun common (p1, q1, p2, q2) = - let val q' = lcm (q1, q2) - in (p1 * (q' div q1), p2 * (q' div q2), q') end + let + val q' = Integer.lcm q1 q2; + in (p1 *% (Integer.div q' q1), p2 *% (Integer.div q' q2), q') end fun rat_of_quotient (p, q) = - if q = Intt.int 0 then raise DIVZERO - else norm (Intt.int 0 <= q, p, abs q); + let + val (a, absq) = Integer.signabs q; + in + if Integer.cmp_zero absq = EQUAL then raise DIVZERO + else norm (a, p, absq) + end; -fun quotient_of_rat (Rat (a, p, q)) = (if a then p else ~p, q); +fun quotient_of_rat (Rat (a, p, q)) = (if a then p else Integer.neg p, q); fun string_of_rat r = - let val (p, q) = quotient_of_rat r - in Intt.string_of_int p ^ "/" ^ Intt.string_of_int q end; + let + val (p, q) = quotient_of_rat r; + in Integer.string_of_int p ^ "/" ^ Integer.string_of_int q end; fun eq (Rat (false, _, _), Rat (true, _, _)) = false | eq (Rat (true, _, _), Rat (false, _, _)) = false - | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 = p2 andalso q1 = q2 + | eq (Rat (_, p1, q1), Rat (_, p2, q2)) = p1 =% p2 andalso q1 =% q2; fun cmp (Rat (false, _, _), Rat (true, _, _)) = LESS | cmp (Rat (true, _, _), Rat (false, _, _)) = GREATER | cmp (Rat (a, p1, q1), Rat (_, p2, q2)) = let val (r1, r2, _) = common (p1, q1, p2, q2) - in if a then Intt.cmp (r1, r2) else Intt.cmp (r2, r1) end; + in if a then Integer.cmp (r1, r2) else Integer.cmp (r2, r1) end; fun le a b = let val order = cmp (a, b) in order = LESS orelse order = EQUAL end; -fun lt a b = cmp (a, b) = LESS; +fun lt a b = (cmp (a, b) = LESS); fun cmp_zero (Rat (false, _, _)) = LESS | cmp_zero (Rat (_, 0, _)) = EQUAL @@ -86,53 +92,50 @@ fun add (Rat (a1, p1, q1)) (Rat(a2, p2, q2)) = let - val (r1, r2, den) = common (p1, q1, p2, q2) - val num = (if a1 then r1 else ~r1) + (if a2 then r2 else ~r2) + val (r1, r2, den) = common (p1, q1, p2, q2); + val num = (if a1 then r1 else Integer.neg r1) + +% (if a2 then r2 else Integer.neg r2); in norm (true, num, den) end; fun mult (Rat (a1, p1, q1)) (Rat (a2, p2, q2)) = - norm (a1=a2, p1*p2, q1*q2); + norm (a1 = a2, p1 *% p2, q1 *% q2); fun neg (r as Rat (b, p, q)) = - if p = Intt.int 0 then r + if Integer.cmp_zero p = EQUAL then r else Rat (not b, p, q); fun inv (Rat (a, p, q)) = - if p = Intt.int 0 then raise DIVZERO + if Integer.cmp_zero q = EQUAL then raise DIVZERO else Rat (a, q, p); fun roundup (r as Rat (a, p, q)) = - if q = Intt.int 1 then r + if q = Integer.one then r else let - fun round true q = Rat (true, q + Intt.int 1, Intt.int 1) + fun round true q = Rat (true, Integer.inc q, Integer.one) | round false q = - if q = Intt.int 0 - then Rat (true, Intt.int 0, Intt.int 1) - else Rat (false, q, Intt.int 1); - in round a (p div q) end; + Rat (Integer.cmp_zero q = EQUAL, Integer.int 0, Integer.int 1); + in round a (Integer.div p q) end; fun rounddown (r as Rat (a, p, q)) = - if q = Intt.int 1 then r + if q = Integer.one then r else let - fun round true q = Rat (true, q, Intt.int 1) - | round false q = Rat (false, q + Intt.int 1, Intt.int 1) - in round a (p div q) end; + fun round true q = Rat (true, q, Integer.one) + | round false q = Rat (false, Integer.inc q, Integer.one) + in round a (Integer.div p q) end; end; -infix 5 +/; -infix 5 -/; -infix 7 */; -infix 7 //; +infix 7 */ //; +infix 6 +/ -/; infix 4 =/ / >=/ <>/; fun a +/ b = Rat.add a b; fun a -/ b = a +/ Rat.neg b; fun a */ b = Rat.mult a b; fun a // b = a */ Rat.inv b; -fun a =/ b = Rat.eq (a,b); +fun a =/ b = Rat.eq (a, b); fun a / b = b