# HG changeset patch # User haftmann # Date 1129875825 -7200 # Node ID 3706c254d29691109101604d7c1af1e83a271216 # Parent 3925ab7b8a18c0eb171eeb8c3a2612bbf4a3a5ed added rounding functions diff -r 3925ab7b8a18 -r 3706c254d296 src/Pure/General/rat.ML --- a/src/Pure/General/rat.ML Fri Oct 21 02:57:22 2005 +0200 +++ b/src/Pure/General/rat.ML Fri Oct 21 08:23:45 2005 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Author: Tobias Nipkow, TU Muenchen -Canonical implementation of exact rational numbers +Canonical implementation of exact rational numbers. *) signature RAT = @@ -25,6 +25,8 @@ val inv: rat -> rat val ge0: rat -> bool val gt0: rat -> bool + val roundup: rat -> rat + val rounddown: rat -> rat end; structure Rat: RAT = @@ -46,7 +48,7 @@ fun rat_of_int i = rat_of_intinf (IntInf.fromInt i); fun norm (a, 0, q) = - Rat (true, 0, 1) (* is that intentional? *) + Rat (true, 0, 1) (*is that intentional?*) | norm (a, p, q) = let val absp = abs p @@ -68,19 +70,28 @@ let val (p, q) = quotient_of_rat r in IntInf.toString p ^ "/" ^ IntInf.toString 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 + +fun le (Rat (false, _, _), Rat (true, _, _)) = true + | le (Rat (true, _, _), Rat (false, _, _)) = false + | le (Rat (a, p1, q1), Rat (_, p2, q2)) = + let val (r1, r2, _) = common (p1, q1, p2, q2) + in if a then r1 <= r2 else r2 <= r1 end; + +fun lt (Rat (false, _, _), Rat (true, _, _)) = true + | lt (Rat (true, _, _), Rat (false, _, _)) = false + | lt (Rat (a, p1, q1), Rat (_, p2, q2)) = + let val (r1, r2, _) = common (p1, q1, p2, q2) + in if a then r1 <= r2 else r2 <= r1 end; + fun ord (Rat (false, _, _), Rat (true, _, _)) = LESS | ord (Rat (true, _, _), Rat (false, _, _)) = GREATER | ord (Rat (a, p1, q1), Rat (_, p2, q2)) = - if p1 = p2 andalso q1 = q2 then EQUAL - else let val (r1, r2, _) = common (p1, q1, p2, q2) + let val (r1, r2, _) = common (p1, q1, p2, q2) in if a then IntInf.compare (r1, r2) else IntInf.compare (r2, r1) end; -fun eq r = (ord r = EQUAL); - -fun le r = not (ord r = GREATER); - -fun lt r = (ord r = LESS); - fun add (Rat (a1, p1, q1), Rat(a2, p2, q2)) = let val (r1, r2, den) = common (p1, q1, p2, q2) @@ -102,4 +113,19 @@ fun ge0 (Rat (a, _, _)) = a; fun gt0 (Rat (a, p, _)) = a andalso p > 0; +fun roundup (r as Rat (_, _, 1)) = r + | roundup (Rat (a, p, q)) = + let + fun round true q = Rat (true, q+1, 1) + | round false 0 = Rat (true, 0 ,1) + | round false q = Rat (false, q, 1) + in round a (p div q) end; + +fun rounddown (r as Rat (_, _, 1)) = r + | rounddown (Rat (a, p, q)) = + let + fun round true q = Rat (true, q, 1) + | round false q = Rat (false, q+1, 1) + in round a (p div q) end; + end;