# Module Data.BinInt

This library contains data types for a binary representation of natural and integers. It is based on the paper Declaring Numbers by Brassel/Fischer/Huch ENTCS 216, 2008.

The advantage of this algebraic definition in contrast to built-in integers is the possibility to use them also for narrowing, i.e., functional logic programming. Since the operations are also quite efficient compared to a simple Peano representations, this library is also the basis of the implementation of integers in the Curry implementation KiCS2.

Version: December 2020

## Summary of exported operations:

 ```succ :: Nat -> Nat``` Successor, O(n) ```pred :: Nat -> Nat``` Predecessor, O(n) ```(+^) :: Nat -> Nat -> Nat``` Addition, O(max (m, n)) ```(-^) :: Nat -> Nat -> BinInt``` Subtraction ```mult2 :: BinInt -> BinInt``` Multiplication by 2 ```(*^) :: Nat -> Nat -> Nat``` Multiplication, O(m*n) ```div2 :: Nat -> Nat``` Division by 2 ```mod2 :: Nat -> BinInt``` Modulo by 2 ```cmpNat :: Nat -> Nat -> Ordering``` Comparison of natural numbers, O(min (m,n)) ```quotRemNat :: Nat -> Nat -> (BinInt,BinInt)``` Quotient and remainder. ```lteqInteger :: BinInt -> BinInt -> Bool``` Less-than-or-equal on BinInt ```cmpInteger :: BinInt -> BinInt -> Ordering``` Comparison on BinInt, O(min (m, n)) ```neg :: BinInt -> BinInt``` Unary minus. ```inc :: BinInt -> BinInt``` Increment ```dec :: BinInt -> BinInt``` Decrement ```(+#) :: BinInt -> BinInt -> BinInt``` Adds two BinInts. ```(-#) :: BinInt -> BinInt -> BinInt``` Subtracts two BinInts. ```(*#) :: BinInt -> BinInt -> BinInt``` Multiplies two BinInts. ```quotRemInteger :: BinInt -> BinInt -> (BinInt,BinInt)``` Quotient and Remainder, truncated against zero ```divModInteger :: BinInt -> BinInt -> (BinInt,BinInt)``` Quotient and Remainder, truncated against negative infinity ```divInteger :: BinInt -> BinInt -> BinInt``` Integer divisor, truncated towards negative infinity. ```modInteger :: BinInt -> BinInt -> BinInt``` Integer modulo, truncated towards negative infinity. ```quotInteger :: BinInt -> BinInt -> BinInt``` Integer quotient, truncated towards zero. ```remInteger :: BinInt -> BinInt -> BinInt``` Integer remainder, truncated towards zero.

## Exported datatypes:

Nat

Algebraic data type to represent natural numbers.

Constructors:

• ```IHi :: Nat``` : most significant bit
• ```O :: Nat -> Nat``` : multiply with 2
• ```I :: Nat -> Nat``` : multiply with 2 and add 1

BinInt

Algebraic data type to represent integers.

Constructors:

• ```Neg :: Nat -> BinInt```
• ```Zero :: BinInt```
• ```Pos :: Nat -> BinInt```

## Exported operations:

 ```succ :: Nat -> Nat``` Successor, O(n) Further infos: solution complete, i.e., able to compute all solutions
 ```pred :: Nat -> Nat``` Predecessor, O(n)
 ```(+^) :: Nat -> Nat -> Nat``` Addition, O(max (m, n)) Further infos: solution complete, i.e., able to compute all solutions
 ```(-^) :: Nat -> Nat -> BinInt``` Subtraction
 ```mult2 :: BinInt -> BinInt``` Multiplication by 2 Further infos: solution complete, i.e., able to compute all solutions
 ```(*^) :: Nat -> Nat -> Nat``` Multiplication, O(m*n) Further infos: solution complete, i.e., able to compute all solutions
 ```div2 :: Nat -> Nat``` Division by 2
 ```mod2 :: Nat -> BinInt``` Modulo by 2 Further infos: solution complete, i.e., able to compute all solutions
 ```cmpNat :: Nat -> Nat -> Ordering``` Comparison of natural numbers, O(min (m,n))
 ```quotRemNat :: Nat -> Nat -> (BinInt,BinInt)``` Quotient and remainder.
 ```lteqInteger :: BinInt -> BinInt -> Bool``` Less-than-or-equal on BinInt
 ```cmpInteger :: BinInt -> BinInt -> Ordering``` Comparison on BinInt, O(min (m, n))
 ```neg :: BinInt -> BinInt``` Unary minus. Usually written as "- e". Further infos: solution complete, i.e., able to compute all solutions
 ```inc :: BinInt -> BinInt``` Increment
 ```dec :: BinInt -> BinInt``` Decrement
 ```(+#) :: BinInt -> BinInt -> BinInt``` Adds two BinInts.
 ```(-#) :: BinInt -> BinInt -> BinInt``` Subtracts two BinInts.
 ```(*#) :: BinInt -> BinInt -> BinInt``` Multiplies two BinInts. Further infos: solution complete, i.e., able to compute all solutions
 ```quotRemInteger :: BinInt -> BinInt -> (BinInt,BinInt)``` Quotient and Remainder, truncated against zero
 ```divModInteger :: BinInt -> BinInt -> (BinInt,BinInt)``` Quotient and Remainder, truncated against negative infinity
 ```divInteger :: BinInt -> BinInt -> BinInt``` Integer divisor, truncated towards negative infinity.
 ```modInteger :: BinInt -> BinInt -> BinInt``` Integer modulo, truncated towards negative infinity.
 ```quotInteger :: BinInt -> BinInt -> BinInt``` Integer quotient, truncated towards zero.
 ```remInteger :: BinInt -> BinInt -> BinInt``` Integer remainder, truncated towards zero.