src/Tools/rat.ML
changeset 24521 9565ac68c3cd
parent 23520 483fe92f00c1
child 24522 ec3e5c1a0479
equal deleted inserted replaced
24520:40b220403257 24521:9565ac68c3cd
    91 fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
    91 fun mult (Rat (p1, q1)) (Rat (p2, q2)) =
    92   rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
    92   rat_of_quotient (Integer.mult p1 p2, Integer.mult q1 q2);
    93 
    93 
    94 fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
    94 fun neg (Rat (p, q)) = Rat (Integer.neg p, q);
    95 
    95 
    96 fun inv (Rat (p, 0)) = raise DIVZERO
    96 fun inv (Rat (p, q)) = case Integer.sign p
    97   | inv (Rat (p, q)) = Rat (q, p);
    97  of LESS => Rat (Integer.neg q, Integer.neg p)
       
    98   | EQAUL => raise DIVZERO
       
    99   | GREATER => Rat (q, p);
    98 
   100 
    99 fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
   101 fun rounddown (Rat (p, q)) = Rat (Integer.div p q, 1);
   100 
   102 
   101 fun roundup (Rat (p, q)) = case Integer.divmod p q
   103 fun roundup (Rat (p, q)) = case Integer.divmod p q
   102  of (m, 0) => Rat (m, 1)
   104  of (m, 0) => Rat (m, 1)