module HyperReal where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Level renaming ( suc to succ ; zero to Zero )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Binary.Definitions

hnzero : (ℕ → ℕ) → Set
hnzero f = (x : ℕ) → ¬ ( x ≡ zero )

data HyperReal : Set where
   hnat :  (ℕ → ℕ) → HyperReal
   hadd :  HyperReal → (x : ℕ → ℕ ) → HyperReal
   hsub :  HyperReal → (x : ℕ → ℕ ) → HyperReal
   hdiv :  HyperReal → (x : ℕ → ℕ ) → hnzero x → HyperReal

data Rational : Set where
   rat :  ℕ → ℕ → (z : ℕ) → ¬ (z ≡ zero)  → Rational  -- (x - y ) / z

prat : Rational → ℕ
prat (rat x _ _ _ ) = x

mrat : Rational → ℕ
mrat (rat _ y _ _ ) = y

drat : Rational → ℕ
drat (rat _ _ z _ ) = z

zrat : (r : Rational ) → ¬ (drat r ≡ zero) 
zrat (rat _ _ z ne ) = ne

HyRa←R : HyperReal → (ℕ → Rational)
HyRa←R (hnat x) i = rat (x i) 0 1 (λ ())
HyRa←R (hadd x y) i with HyRa←R x i
... | rat w v z ne = rat (w + z * (y i)) v z ne
HyRa←R (hsub x y) i  with HyRa←R x i
... | rat w v z ne = rat w (v + z * (y i)) z ne
HyRa←R (hdiv x y nz) i with HyRa←R x i
... | rat w v z ne = rat w v (z * (y i)) {!!}

HyR←Ra :  (ℕ → Rational) → HyperReal
HyR←Ra r = hdiv (hsub (hnat (λ i → prat (r i))) (λ i → mrat (r i))) (λ i → drat (r i)) {!!}