Real.idr

import Data.Colist

InfiniteBits : Type
InfiniteBits = Colist Bool

-- 1.bits << n
record RealData where
    constructor MkRealData
    n: Int 
    bits: InfiniteBits

data Real : Type where
    Zero : Real
    Positive : RealData -> Real
    Negative : RealData -> Real


partial
compare_bits : InfiniteBits -> InfiniteBits -> Ordering
compare_bits Nil Nil = EQ
compare_bits (True :: _) (False :: _) = GT
compare_bits (False :: _) (True :: _) = LT
compare_bits (True :: xs0) (True :: xs1) = compare_bits xs0 xs1
compare_bits (False :: xs0) (False :: xs1) = compare_bits xs0 xs1
compare_bits (True :: _) [] = GT
compare_bits (False :: xs) [] = compare_bits xs []
compare_bits [] (True :: _) = LT
compare_bits [] (False :: xs) = compare_bits xs []

compare : RealData -> RealData -> Ordering
compare (MkRealData n0 b0) (MkRealData n1 b1) =
    case compare n0 n1 of
        LT => LT
        GT => GT
        EQ => compare_bits b0 b1

Eq Real where
    (==) Zero Zero = True
    (==) (Positive n) (Positive m) = compare n m == EQ
    (==) (Negative n) (Negative m) = compare n m == EQ
    (==) _ _ = False

Ord Real where
    compare Zero Zero = EQ
    compare Zero (Positive _) = LT
    compare Zero (Negative _) = GT
    compare (Positive _) (Negative _) = GT
    compare (Positive _) Zero = GT
    compare (Positive m) (Positive n) = compare m n
    compare (Negative m) (Positive n) = LT
    compare (Negative m) Zero = LT
    compare (Negative m) (Negative n) = compare n m