Module Data.BinInt

Version
April 2025

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.

Exported Datatypes:
BinIntNat
Exported Functions:
*#*^+#+^-#-^cmpIntegercmpNatdecdiv2divIntegerdivModIntegerfromBinIntfromNatfromNat'postinclteqIntegermod2modIntegermult2negpredquotIntegerquotRemIntegerquotRemNatremIntegersucctoBinInttoNattoNat'pre

Exported Datatypes

data 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

Known instances:

data BinInt

Algebraic data type to represent integers.

Constructors:

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

Known instances:

Exported Functions

succ :: Nat -> Nat  Deterministic 

Successor, O(n)

Further infos:
  • solution complete, i.e., able to compute all solutions

pred :: Nat -> Nat  Deterministic 

Predecessor, O(n)

Further infos:
  • partially defined

(+^) :: Nat -> Nat -> Nat  Deterministic 

Addition, O(max (m, n))

Further infos:
  • solution complete, i.e., able to compute all solutions

(-^) :: Nat -> Nat -> BinInt  Deterministic 

Subtraction

mult2 :: BinInt -> BinInt  Deterministic 

Multiplication by 2

Further infos:
  • solution complete, i.e., able to compute all solutions

(*^) :: Nat -> Nat -> Nat  Deterministic 

Multiplication, O(m*n)

Further infos:
  • solution complete, i.e., able to compute all solutions

div2 :: Nat -> Nat  Deterministic 

Division by 2

Further infos:
  • partially defined

mod2 :: Nat -> BinInt  Deterministic 

Modulo by 2

Further infos:
  • solution complete, i.e., able to compute all solutions

cmpNat :: Nat -> Nat -> Ordering  Deterministic 

Comparison of natural numbers, O(min (m,n))

quotRemNat :: Nat -> Nat -> (BinInt, BinInt)  Deterministic 

Quotient and remainder.

Further infos:
  • partially defined

lteqInteger :: BinInt -> BinInt -> Bool  Deterministic 

Less-than-or-equal on BinInt

cmpInteger :: BinInt -> BinInt -> Ordering  Deterministic 

Comparison on BinInt, O(min (m, n))

neg :: BinInt -> BinInt  Deterministic 

Unary minus. Usually written as "- e".

Further infos:
  • solution complete, i.e., able to compute all solutions

inc :: BinInt -> BinInt  Deterministic 

Increment

dec :: BinInt -> BinInt  Deterministic 

Decrement

(+#) :: BinInt -> BinInt -> BinInt  Deterministic 

Adds two BinInts.

(-#) :: BinInt -> BinInt -> BinInt  Deterministic 

Subtracts two BinInts.

(*#) :: BinInt -> BinInt -> BinInt  Deterministic 

Multiplies two BinInts.

Further infos:
  • solution complete, i.e., able to compute all solutions

quotRemInteger :: BinInt -> BinInt -> (BinInt, BinInt)  Deterministic 

Quotient and Remainder, truncated against zero

Further infos:
  • partially defined

divModInteger :: BinInt -> BinInt -> (BinInt, BinInt)  Deterministic 

Quotient and Remainder, truncated against negative infinity

Further infos:
  • partially defined

divInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer divisor, truncated towards negative infinity.

modInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer modulo, truncated towards negative infinity.

quotInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer quotient, truncated towards zero.

remInteger :: BinInt -> BinInt -> BinInt  Deterministic 

Integer remainder, truncated towards zero.

fromNat :: Nat -> Int  Deterministic 

Converts a binary natural number into an integer constant.

fromNat'post :: Nat -> Int -> Bool  Deterministic 

toNat :: Int -> Nat  Deterministic 

Transforms a positive standard integer into a natural number.

Further infos:
  • partially defined

toNat'pre :: Int -> Bool  Deterministic 

fromBinInt :: BinInt -> Int  Deterministic 

Converts a binary integer into an integer constant.

toBinInt :: Int -> BinInt  Deterministic 

Transforms a standard integer into a binary integer.

Further infos:
  • partially defined