PAKCS
Exported names: Imported modules:

Module 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: May 2017

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.