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: February 2017
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. |
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
Algebraic data type to represent integers.
Constructors:
Successor, O(n)
|
Addition, O(max (m, n))
|
Multiplication by 2
|
Multiplication, O(m*n)
|
Modulo by 2
|
Quotient and remainder. |
Less-than-or-equal on BinInt |
Comparison on BinInt, O(min (m, n)) |
Unary minus. Usually written as "- e".
|
Multiplies two BinInts.
|
Quotient and Remainder, truncated against zero |
Quotient and Remainder, truncated against negative infinity |
Integer divisor, truncated towards negative infinity. |
Integer modulo, truncated towards negative infinity. |
Integer quotient, truncated towards zero. |
Integer remainder, truncated towards zero. |