-
Exported names:
-
Imported modules:
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:
Exported operations:
|
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. |