Natural numbers n-ary representations

nat-r.agda

-- tested with Agda 2.6.0.1
module nat-r where

----------------------------------------------------------------------
-- unary representation
----------------------------------------------------------------------

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- syntax
infixl 10 _*_
infixl 9 _+_

inc : ℕ → ℕ
inc zero = suc zero
inc (suc n) = suc (inc n)

-- operation addition
_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

-- operation multiplication
_*_ : ℕ → ℕ → ℕ
zero  * n = zero
suc m * n = n + (m * n)

-- pragmas
{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}

----------------------------------------------------------------------
-- binary representation
----------------------------------------------------------------------

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

incBin : Bin → Bin
incBin nil = x1 nil
incBin (x0 n) = x1 n
incBin (x1 n) = x0 incBin n

toBin   : ℕ → Bin
toBin zero = x0 nil
toBin (suc n) = incBin (toBin n)

-- compute normal form for
-- toBin 92

fromBin : Bin → ℕ
fromBin nil = zero
fromBin (x0 n) = zero + ((fromBin n) * suc(suc zero))
fromBin (x1 n) = suc zero + ((fromBin n) * suc(suc zero))

-- compute normal form for
-- fromBin (x0 x0 x1 x1 x1 x0 x1 nil)

----------------------------------------------------------------------
-- ternary representation
----------------------------------------------------------------------

data Ter : Set where
  nil : Ter
  x0_ : Ter → Ter
  x1_ : Ter → Ter
  x2_ : Ter → Ter

incTer : Ter → Ter
incTer nil = x1 nil
incTer (x0 n) = x1 n
incTer (x1 n) = x2 n
incTer (x2 n) = x0 incTer n

toTer  : ℕ → Ter
toTer zero = x0 nil
toTer (suc n) = incTer (toTer n)

----------------------------------------------------------------------
-- decimal representation
----------------------------------------------------------------------

data Dec : Set where
  nil : Dec
  x0_ : Dec → Dec
  x1_ : Dec → Dec
  x2_ : Dec → Dec
  x3_ : Dec → Dec
  x4_ : Dec → Dec
  x5_ : Dec → Dec
  x6_ : Dec → Dec
  x7_ : Dec → Dec
  x8_ : Dec → Dec
  x9_ : Dec → Dec

incDec : Dec → Dec
incDec nil = x1 nil
incDec (x0 n) = x1 n
incDec (x1 n) = x2 n
incDec (x2 n) = x3 n
incDec (x3 n) = x4 n
incDec (x4 n) = x5 n
incDec (x5 n) = x6 n
incDec (x6 n) = x7 n
incDec (x7 n) = x8 n
incDec (x8 n) = x9 n
incDec (x9 n) = x0 incDec n

toDec  : ℕ → Dec
toDec zero = x0 nil
toDec (suc n) = incDec (toDec n)

-- data ℕr : ℕ → Set where
--  unary : ℕr
--  nary : ℕr → ℕr