--- 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
--- 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;
--- 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
--- 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
--- 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
--- 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));
--- 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));
--- 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 ()
--- 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
--- 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;
--- 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 = Rat.lt a b;
fun a <=/ b = Rat.le a b;
fun a >/ b = b </ a;