Converting between strings and natural numbers

EncodeDecode.agda

module EncodeDecode where

open import Agda.Builtin.Char
  using (Char)
  renaming ( primCharToNat to ord
           ; primNatToChar to chr
           )

open import Agda.Builtin.Equality
  using (_≡_ ; refl)

open import Agda.Builtin.List
  using ([] ; _∷_ ; List)

open import Agda.Builtin.Nat
  using (Nat ; zero ; suc ; _+_ ; _*_)

open import Agda.Builtin.String
  using (String)
  renaming ( primStringToList to unpack
           ; primStringFromList to pack
           )

open import Data.List.Base
  using (foldr ; unfold)

open import Data.Maybe.Base
  using (Maybe ; just ; nothing)

open import Data.Fin
  using ()
  renaming (toℕ to nat)

open import Data.Nat.DivMod
  using (DivMod ; _divMod_)

open DivMod
  using ()
  renaming ( quotient to quot
           ; remainder to rem
           )

open import Data.Product
  using (_×_ ; _,_)


encode : String → Nat
encode s = foldr step 0 (unpack s)
  where
    step : Char → Nat → Nat
    step c n = n * 256 + ord c

test-encode : encode "hello, world!" ≡ 2645608968347327576478451524968
test-encode = refl


decode : Nat → String
decode n = pack (unfold (λ _ → Nat) step {n} n)
  where
    step : Nat → Maybe (Char × Nat)
    step zero    = nothing
    step (suc n) = let r = n divMod 256 in
                   just (chr (nat (rem r) + 1) , quot r)

test-decode : decode 2645608968347327576478451524968 ≡ "hello, world!"
test-decode = refl