Binary numbers in Idris

Bin.idr

module Bin

import Data.Nat

data Bit = O | I

Eq Bit where
    (O == O) = True
    (I == I) = True
    (_ == _) = False

data Bin = Nil | (::) Bit Bin


halfAdd : Bit -> Bit -> (Bit, Bit)
halfAdd O O = (O, O)
halfAdd O I = (I, O)
halfAdd I O = (I, O)
halfAdd I I = (O, I)

fullAdd : Bit -> Bit -> Bit -> (Bit, Bit)
fullAdd O O O = (O, O)
fullAdd O O I = (I, O)
fullAdd O I O = (I, O)
fullAdd O I I = (O, I)
fullAdd I O O = (I, O)
fullAdd I O I = (O, I)
fullAdd I I O = (O, I)
fullAdd I I I = (I, I)


addBin : Bit -> Bin -> Bin -> Bin
addBin O [] ys = ys
addBin O xs [] = xs
addBin I [] [] = [I]
addBin I [] (y :: ys)
    = let (sum, carry) = halfAdd I y in
          sum :: addBin carry [] ys
addBin I (x :: xs) []
    = let (sum, carry) = halfAdd I x in
          sum :: addBin carry xs []
addBin c (x :: xs) (y :: ys)
    = let (sum, carry) = fullAdd c x y in
          sum :: addBin carry xs ys


timesTwo : Bin -> Bin
timesTwo [] = []
timesTwo xs = O :: xs

mulBin : Bin -> Bin -> Bin
mulBin [] ys = []
mulBin (I :: xs) ys = addBin O ys (timesTwo (mulBin xs ys))
mulBin (O :: xs) ys = timesTwo (mulBin xs ys)


binFromNat : Nat -> Bin
binFromNat 0 = []
binFromNat (S k) = addBin I [] (binFromNat k)


evenBin : Bin -> Bool
evenBin [] = True
evenBin (O :: _) = True
evenBin (I :: _) = False

zeroBin : Bin -> Bool
zeroBin [] = True
zeroBin (I :: _) = False
zeroBin (O :: xs) = zeroBin xs

sameBin : Bin -> Bin -> Bool
sameBin [] [] = True
sameBin xs [] = zeroBin xs
sameBin [] ys = zeroBin ys
sameBin (x :: xs) (y :: ys) = x == y && sameBin xs ys


Eq Bin where
    (==) = sameBin


Num Bin where
    (a + b) = addBin O a b
    (a * b) = mulBin a b
    fromInteger x = binFromNat (cast x)