Data.Number.Nat1

The implementations of all functions are supposed to be as non-strict as possible. This is non-trivial as for example a naive implementation of (*) yields O _|_ for the application I _|_ * O IHi while a least-strict version yields O (I _|_). Also the naive / standard implementations of (-), compare, (<), (<=), (>), (>=) are more strict than necessary.

Datatype

data Nat1

A binary representation of natural numbers which starts with the least significant bit.

Constructors

IHi

This constructor represents the most significant bit. There are no leading zero bits.

O Nat1

A zero bit

I Nat1

A one bit

Instances

Enum Nat1

Eq Nat1

Num Nat1

Ord Nat1

Read Nat1

Real Nat1

Show Nat1

Helper Functions

cmpNat1LT :: Nat1 -> Nat1 -> Ordering

This function is used to implement lazy instances of compare and (<), (<=), (>), (>=). It is used to transfer information to more significant bits. Instead of yielding EQ it yields LT if the numbers are equal.

invOrd :: Ordering -> Ordering

Maps LT to GT and GT to LT. It is used instead of defining a function cmpNat1GT.

minusNat1 :: Nat1 -> Nat1 -> Nat1

minusNat1 x y yields x - y + 1. This is used to implement (-) for natural numbers.

fromNat1 :: Num n => Nat1 -> n

This is used for the implementation of toInteger and fromEnum.

toNat1 :: (Integral n, Num n) => n -> Nat1

This is used for the implementation of fromInteger and toEnum.