module MiniLibrary.Rational where

open import MiniLibrary.Base
open import MiniLibrary.Nat
open import MiniLibrary.Natplus
open import MiniLibrary.Integer
open import MiniLibrary.DivMod
open import MiniLibrary.Gcd


infix 4 _<Ratb_ _<Rat_ _≤Ratb_ _≤Rat_ _==Ratb_ _==Rat_
infix  6 _-Rat_
infixl 6 _+Rat_
infixl 7 _*Rat_

data Rat : Set where
  _/_ :  -> ℕ+ -> Rat

_<Ratb_ : Rat  Rat  Bool
(z / n+) <Ratb (z' / m+) = (z *ℤℕ+ m+) <ℤb (z' *ℤℕ+ n+)

_<Rat_ : Rat  Rat  Set
n <Rat m = True (n <Ratb m)

_≤Ratb_ : Rat  Rat  Bool
(z / n+)  ≤Ratb (z' / m+) = (z *ℤℕ+ m+) ≤ℤb (z' *ℤℕ+ n+)

_≤Rat_ : Rat  Rat  Set
n ≤Rat m = True (n ≤Ratb m)

_≥Ratb_ : Rat  -> Rat    Bool
z ≥Ratb z' = z' ≤Ratb z


_≥Rat_ : Rat  -> Rat  -> Set
z ≥Rat z' = z' ≤Rat z


_>Rat_ : Rat  Rat  Set
n >Rat m = m <Rat n



_==Ratb_ : Rat  Rat  Bool
(z / n+) ==Ratb (z' / m+) = (z *ℤℕ+ m+) ==ℤb (z' *ℤℕ+ n+)


_==Rat_ : Rat  Rat  Set
n ==Rat m = True (n ==Ratb m)


decideRat : (z z' : Rat)  z <Rat   z'  z ==Rat  z'  z' <Rat  z
decideRat (z / n+) (z' / m+) = decideℤ  (z *ℤℕ+ m+) (z' *ℤℕ+ n+)

decideRat≤  : (z z' : Rat)  z ≤Rat   z'  z' ≤Rat  z
decideRat≤  (z / n+) (z' / m+) = decideℤ≤   (z *ℤℕ+ m+) (z' *ℤℕ+ n+)


_+Rat_ : Rat  Rat  Rat 
(z / n+) +Rat (z' / m+) = ((z *ℤℕ+  m+) +ℤ (z' *ℤℕ+  n+)) / (n+ *ℕ+ m+)

minusRat : Rat  Rat 
minusRat (z / n+)  = (minusℤ  z) / n+

_-Rat_ : Rat  Rat  Rat 
q -Rat q' = q +Rat (minusRat q')


_*Rat_ : Rat  Rat  Rat 
(z / n+)  *Rat (z' / m+) = (z *ℤ  z')  / (n+ *ℕ+ m+)

{- assumption is that argument k is the gcd of the denominators -}
normaliseaux : Rat  ℕ+  Rat
normaliseaux ((+ (suc n)) / (suc m)) g =  (+ ((suc n) divℕ+   g) / ((suc m) divℕ+ g))
normaliseaux (zero        / n+     ) g = zero / suc 0
normaliseaux ((- (suc n)) / (suc m)) g =  (- ((suc n) divℕ+   g) / ((suc m) divℕ+ g))


normalise : Rat  Rat
normalise ((+ (suc n)) / (suc m)) = normaliseaux ((+ (suc n)) / (suc m)) (gcdℕ+ (suc n) (suc m))
normalise (zero        / n+     ) = zero / suc 0
normalise ((- (suc n)) / (suc m)) = normaliseaux ((- (suc n)) / (suc m)) (gcdℕ+ (suc n) (suc m))


_+Ratnor_ : Rat  Rat  Rat
q +Ratnor q' = normalise (q +Rat q')

_*Ratnor_ : Rat  Rat  Rat
q *Ratnor q' = normalise (q *Rat q')




0Rat: Rat
0Rat  = zero / 1ℕ+

1Rat: Rat
1Rat  = 1ℤ / 1ℕ+

2Rat: Rat
2Rat  = 2ℤ / 1ℕ+

-1Rat: Rat
-1Rat  = -1ℤ / 1ℕ+


1/2Rat : Rat
1/2Rat = 1ℤ / 2ℕ+ 

1/3Rat : Rat
1/3Rat = 1ℤ / 3ℕ+ 

1/4Rat : Rat
1/4Rat = 1ℤ / 4ℕ+ 

-1/2Rat : Rat
-1/2Rat = -1ℤ / 2ℕ+ 

-1/3Rat : Rat
-1/3Rat = -1ℤ / 3ℕ+ 

-1/4Rat : Rat
-1/4Rat = -1ℤ / 4ℕ+ 


data _∈[-1,1]Rat (q : Rat) : Set where
  intro : -1Rat ≤Rat q  q ≤Rat 1Rat  q ∈[-1,1]Rat

1/2Rat∈[-1,1] : 1/2Rat ∈[-1,1]Rat
1/2Rat∈[-1,1] = intro triv triv

1/3Rat∈[-1,1] : 1/3Rat ∈[-1,1]Rat
1/3Rat∈[-1,1] = intro triv triv

1/4Rat∈[-1,1] : 1/4Rat ∈[-1,1]Rat
1/4Rat∈[-1,1] = intro triv triv

-1/4Rat∈[-1,1] : -1/4Rat ∈[-1,1]Rat
-1/4Rat∈[-1,1] = intro triv triv

-1/3Rat∈[-1,1] : -1/3Rat ∈[-1,1]Rat
-1/3Rat∈[-1,1] = intro triv triv

data ShowRat : Set where
  +_/'_ :     ShowRat
  0/'_  :   ShowRat
  -_/'_ :     ShowRat

show : Rat  ShowRat
show (+ (suc n) / (suc m)) = + (suc n) /' (suc m)
show (- (suc n) / (suc m)) = - (suc n) /' (suc m)
show (zero / (suc m))        = 0/' (suc m)