src/Pure/General/rat.ML
changeset 63203 c1b15830549e
parent 63202 e77481be5c97
child 63206 13b67739af09
equal deleted inserted replaced
63202:e77481be5c97 63203:c1b15830549e
    23   val abs: rat -> rat
    23   val abs: rat -> rat
    24   val add: rat -> rat -> rat
    24   val add: rat -> rat -> rat
    25   val mult: rat -> rat -> rat
    25   val mult: rat -> rat -> rat
    26   val neg: rat -> rat
    26   val neg: rat -> rat
    27   val inv: rat -> rat
    27   val inv: rat -> rat
    28   val rounddown: rat -> rat
    28   val round_down: rat -> rat
    29   val roundup: rat -> rat
    29   val round_up: rat -> rat
    30 end;
    30 end;
    31 
    31 
    32 structure Rat : RAT =
    32 structure Rat : RAT =
    33 struct
    33 struct
    34 
    34 
    89   (case Integer.sign p of
    89   (case Integer.sign p of
    90     LESS => Rat (~ q, ~ p)
    90     LESS => Rat (~ q, ~ p)
    91   | EQUAL => raise DIVZERO
    91   | EQUAL => raise DIVZERO
    92   | GREATER => Rat (q, p));
    92   | GREATER => Rat (q, p));
    93 
    93 
    94 fun rounddown (Rat (p, q)) = Rat (p div q, 1);
    94 fun round_down (Rat (p, q)) = Rat (p div q, 1);
    95 
    95 
    96 fun roundup (Rat (p, q)) =
    96 fun round_up (Rat (p, q)) =
    97   (case Integer.div_mod p q of
    97   (case Integer.div_mod p q of
    98     (m, 0) => Rat (m, 1)
    98     (m, 0) => Rat (m, 1)
    99   | (m, _) => Rat (m + 1, 1));
    99   | (m, _) => Rat (m + 1, 1));
   100 
   100 
   101 end;
   101 end;