src/Pure/library.ML
changeset 17952 00eccd84608f
parent 17822 3830b0a41d51
child 18011 685d95c793ff
     1.1 --- a/src/Pure/library.ML	Fri Oct 21 14:49:04 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Oct 21 14:49:49 2005 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Basic library: functions, options, pairs, booleans, lists, integers,
     1.7 -rational numbers, strings, lists as sets, association lists, generic
     1.8 +strings, lists as sets, association lists, generic
     1.9  tables, balanced trees, orders, current directory, misc.
    1.10  *)
    1.11  
    1.12 @@ -145,23 +145,6 @@
    1.13    val read_int: string list -> int * string list
    1.14    val oct_char: string -> string
    1.15  
    1.16 -  (*rational numbers*)
    1.17 -  type rat
    1.18 -  exception RAT of string
    1.19 -  val rep_rat: rat -> IntInf.int * IntInf.int
    1.20 -  val ratge0: rat -> bool
    1.21 -  val ratgt0: rat -> bool
    1.22 -  val ratle: rat * rat -> bool
    1.23 -  val ratlt: rat * rat -> bool
    1.24 -  val ratadd: rat * rat -> rat
    1.25 -  val ratmul: rat * rat -> rat
    1.26 -  val ratinv: rat -> rat
    1.27 -  val int_ratdiv: IntInf.int * IntInf.int -> rat
    1.28 -  val ratneg: rat -> rat
    1.29 -  val rat_of_int: int -> rat
    1.30 -  val rat_of_intinf: IntInf.int -> rat
    1.31 -  val rat0: rat
    1.32 -
    1.33    (*strings*)
    1.34    val nth_elem_string: int * string -> string
    1.35    val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
    1.36 @@ -1176,61 +1159,6 @@
    1.37  val pwd = OS.FileSys.getDir;
    1.38  
    1.39  
    1.40 -
    1.41 -(** rational numbers **)
    1.42 -(* Keep them normalized! *)
    1.43 -
    1.44 -datatype rat = Rat of bool * IntInf.int * IntInf.int
    1.45 -
    1.46 -exception RAT of string;
    1.47 -
    1.48 -fun rep_rat(Rat(a,p,q)) = (if a then p else ~p,q)
    1.49 -
    1.50 -fun ratnorm(a,p,q) = if p=0 then Rat(a,0,1) else
    1.51 -  let val absp = abs p
    1.52 -      val m = gcd(absp,q)
    1.53 -  in Rat(a = (0 <= p), absp div m, q div m) end;
    1.54 -
    1.55 -fun ratcommon(p,q,r,s) =
    1.56 -  let val den = lcm(q,s)
    1.57 -  in (p*(den div q), r*(den div s), den) end
    1.58 -
    1.59 -fun ratge0(Rat(a,p,q)) = a;
    1.60 -fun ratgt0(Rat(a,p,q)) = a andalso p > 0;
    1.61 -
    1.62 -fun ratle(Rat(a,p,q),Rat(b,r,s)) =
    1.63 -  not a andalso b orelse
    1.64 -  a = b andalso
    1.65 -    let val (p,r,_) = ratcommon(p,q,r,s)
    1.66 -    in if a then p <= r else r <= p end
    1.67 -
    1.68 -fun ratlt(Rat(a,p,q),Rat(b,r,s)) =
    1.69 -  not a andalso b orelse
    1.70 -  a = b andalso
    1.71 -    let val (p,r,_) = ratcommon(p,q,r,s)
    1.72 -    in if a then p < r else r < p end
    1.73 -
    1.74 -fun ratadd(Rat(a,p,q),Rat(b,r,s)) =
    1.75 -  let val (p,r,den) = ratcommon(p,q,r,s)
    1.76 -      val num = (if a then p else ~p) + (if b then r else ~r)
    1.77 -  in ratnorm(true,num,den) end;
    1.78 -
    1.79 -fun ratmul(Rat(a,p,q),Rat(b,r,s)) = ratnorm(a=b,p*r,q*s)
    1.80 -
    1.81 -fun ratinv(Rat(a,p,q)) = if p=0 then raise RAT "ratinv" else Rat(a,q,p)
    1.82 -
    1.83 -fun int_ratdiv(p,q) =
    1.84 -  if q=0 then raise RAT "int_ratdiv" else ratnorm(0<=q, p, abs q)
    1.85 -
    1.86 -fun ratneg(Rat(b,p,q)) = Rat(not b,p,q);
    1.87 -
    1.88 -fun rat_of_intinf i = if i < 0 then Rat(false,abs i,1) else Rat(true,i,1);
    1.89 -
    1.90 -fun rat_of_int i = rat_of_intinf (IntInf.fromInt i);
    1.91 -
    1.92 -val rat0 = rat_of_int 0;
    1.93 -
    1.94 -
    1.95  (** misc **)
    1.96  
    1.97  (*Partition list into elements that satisfy predicate and those that don't.