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  _<Ratb_ _<Rat_ _≤Ratb_ _≤Rat_ _==Ratb_ _==Rat_
infix   _-Rat_
infixl  _+Rat_
infixl  _*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 
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 
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)