# HG changeset patch # User haftmann # Date 1129898989 -7200 # Node ID 00eccd84608fecae216ce41326391e89329b1ff6 # Parent ff954cc338c796be80d7f9248d8fcdb59813bdee abandoned rational number functions in favor of General/rat.ML diff -r ff954cc338c7 -r 00eccd84608f src/Pure/library.ML --- a/src/Pure/library.ML Fri Oct 21 14:49:04 2005 +0200 +++ b/src/Pure/library.ML Fri Oct 21 14:49:49 2005 +0200 @@ -4,7 +4,7 @@ Author: Markus Wenzel, TU Muenchen Basic library: functions, options, pairs, booleans, lists, integers, -rational numbers, strings, lists as sets, association lists, generic +strings, lists as sets, association lists, generic tables, balanced trees, orders, current directory, misc. *) @@ -145,23 +145,6 @@ val read_int: string list -> int * string list val oct_char: string -> string - (*rational numbers*) - type rat - exception RAT of string - val rep_rat: rat -> IntInf.int * IntInf.int - val ratge0: rat -> bool - val ratgt0: rat -> bool - val ratle: rat * rat -> bool - val ratlt: rat * rat -> bool - val ratadd: rat * rat -> rat - val ratmul: rat * rat -> rat - val ratinv: rat -> rat - val int_ratdiv: IntInf.int * IntInf.int -> rat - val ratneg: rat -> rat - val rat_of_int: int -> rat - val rat_of_intinf: IntInf.int -> rat - val rat0: rat - (*strings*) val nth_elem_string: int * string -> string val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a @@ -1176,61 +1159,6 @@ val pwd = OS.FileSys.getDir; - -(** rational numbers **) -(* Keep them normalized! *) - -datatype rat = Rat of bool * IntInf.int * IntInf.int - -exception RAT of string; - -fun rep_rat(Rat(a,p,q)) = (if a then p else ~p,q) - -fun ratnorm(a,p,q) = if p=0 then Rat(a,0,1) else - let val absp = abs p - val m = gcd(absp,q) - in Rat(a = (0 <= p), absp div m, q div m) end; - -fun ratcommon(p,q,r,s) = - let val den = lcm(q,s) - in (p*(den div q), r*(den div s), den) end - -fun ratge0(Rat(a,p,q)) = a; -fun ratgt0(Rat(a,p,q)) = a andalso p > 0; - -fun ratle(Rat(a,p,q),Rat(b,r,s)) = - not a andalso b orelse - a = b andalso - let val (p,r,_) = ratcommon(p,q,r,s) - in if a then p <= r else r <= p end - -fun ratlt(Rat(a,p,q),Rat(b,r,s)) = - not a andalso b orelse - a = b andalso - let val (p,r,_) = ratcommon(p,q,r,s) - in if a then p < r else r < p end - -fun ratadd(Rat(a,p,q),Rat(b,r,s)) = - let val (p,r,den) = ratcommon(p,q,r,s) - val num = (if a then p else ~p) + (if b then r else ~r) - in ratnorm(true,num,den) end; - -fun ratmul(Rat(a,p,q),Rat(b,r,s)) = ratnorm(a=b,p*r,q*s) - -fun ratinv(Rat(a,p,q)) = if p=0 then raise RAT "ratinv" else Rat(a,q,p) - -fun int_ratdiv(p,q) = - if q=0 then raise RAT "int_ratdiv" else ratnorm(0<=q, p, abs q) - -fun ratneg(Rat(b,p,q)) = Rat(not b,p,q); - -fun rat_of_intinf i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1); - -fun rat_of_int i = rat_of_intinf (IntInf.fromInt i); - -val rat0 = rat_of_int 0; - - (** misc **) (*Partition list into elements that satisfy predicate and those that don't.