Rational.idr

module Main

%default total

data Rational = MkRational Nat Nat

numerator : Rational -> Nat
numerator (MkRational n d) = n

denominator : Rational -> Nat
denominator (MkRational n d) = d

instance Show Rational where 
  show (MkRational num denom)  = "[" ++ (show num) ++ "/" ++ (show denom) ++ "]"

cmp : Rational -> Rational -> ( Nat -> Nat -> Bool ) -> Bool
cmp r1 r2 f = (mult (numerator r1) (denominator r2)) `f` (mult (numerator r2) (denominator r1))

soCmp : (r1:Rational) -> 
        (r2:Rational) -> 
        ( f : Nat -> Nat -> Bool ) -> 
        so (cmp r1 r2 f) -> 
        Bool
soCmp r1 r2 f p = True

instance Eq Rational where
  (==) r1 r2 = cmp r1 r2 (==)

---- Trying to move the proof check inside the RatLT function so it can fit the Ord Typeclass
-- RatLT : Rational -> Rational -> Bool
-- RatLT r1 r2 = soCmp r1 r2 (<) oh

RatGT : (r1:Rational) -> (r2:Rational) -> so (cmp r1 r2 (>) ) -> Bool
RatGT (MkRational n1 d1) (MkRational n2 d2) p = True

RatLTE : (r1:Rational) -> (r2:Rational) -> so (cmp r1 r2 (<=)) -> Bool
RatLTE (MkRational n1 d1) (MkRational n2 d2) p = True

RatGTE : (r1:Rational) -> (r2:Rational) -> so (cmp r1 r2 (>=)) -> Bool
RatGTE (MkRational n1 d1) (MkRational n2 d2) p = True

RatMult : Rational -> Rational -> Rational
RatMult (MkRational n1 d1) (MkRational n2 d2) = 
  MkRational (n1 * n2) (d1 * d2)

RatAdd : Rational -> Rational -> Rational
RatAdd (MkRational n1 d1) (MkRational n2 d2) = 
  MkRational (d2 * n1 + n2 * d1) (d1 * d2)

{-
RatMax : Rational -> Rational -> Rational
RatMax r1 r2 = if (RatGT r1 r2 oh) then r1 else r2

RatMin : Rational -> Rational -> Rational
RatMin r1 r2 = if (RatGT r1 r2 oh) then r2 else r1

instance Ord (Rational) where
  r1 < r2 = RatLT r1 r2 oh
  r1 > r2 = RatGT r1 r2 oh
  r1 <= r2 = RatLTE r1 r2 oh
  r1 >= r2 = RatGTE r1 r2 oh
  compare l r = if l < r then LT
                else if l > r then GT
                else EQ



-- RatReduce : Rational -> Rational
-- RatReduce (MkRational num denom) = ?something



instance Ord Rational where
  (<) = RatLT
  (>) = RatGT
  (<=) = RatLTE
  (>=) = RatGTE
  compare l r = if l < r then LT
                else if l > r then GT
                else EQ

-}

----------------------------------------------------
-- testing 

main : IO ()
main = do
  putStr $ "3/4 == 120/160 => "
  putStrLn $ show $ (MkRational 3 4) == (MkRational 120 160)

  putStr $ "3/4 > 2/3 => "
  putStrLn $ show $ RatGT (MkRational 3 4) (MkRational 2 3) oh

  putStr $ "1/4 + 1/4 = 1/2 => "
  putStrLn $ show $ RatAdd (MkRational 1 4) (MkRational 1 4) == (MkRational 1 2)