------------------------------------------------------------------------
-- The Agda standard library
--
-- Digits and digit expansions
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Digit where

open import Data.Nat.Base
open import Data.Nat.Properties using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n)
open import Data.Nat.Solver using (module +-*-Solver)
open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ)
open import Data.Bool.Base using (Bool; true; false)
open import Data.Char.Base using (Char)
open import Data.List.Base
open import Data.Product.Base using (; _,_)
open import Data.Vec.Base as Vec using (Vec; _∷_; [])
open import Data.Nat.DivMod
open import Data.Nat.Induction
open import Relation.Nullary.Decidable using (True; does; toWitness)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
open import Function.Base using (_$_)

------------------------------------------------------------------------
-- Digits

-- Digit b is the type of digits in base b.

Digit :   Set
Digit b = Fin b

-- Some specific digit kinds.

Decimal = Digit 10
Bit     = Digit 2

-- Some named digits.

0b : Bit
0b = zero

1b : Bit
1b = suc zero

------------------------------------------------------------------------
-- Converting between `ℕ` and `expansions of ℕ`

toNatDigits : (base : ) {base≤16 : True (1 ≤? base)}    List 
toNatDigits base@(suc zero)    n = replicate n 1
toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
  where
  aux : {n : }  Acc _<_ n  List   List 
  aux {zero}        _      xs =  (0  xs)
  aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
  ... | false = (n % base)  xs
  ... | true  = aux (wf (n / base) q<n) ((n % base)  xs)
    where
    q<n : n / base < n
    q<n = m/n<m n base (s<s z<s)

------------------------------------------------------------------------
-- Converting between `ℕ` and expansions of `Digit base`

Expansion :   Set
Expansion base = List (Digit base)

-- fromDigits takes a digit expansion of a natural number, starting
-- with the _least_ significant digit, and returns the corresponding
-- natural number.

fromDigits :  {base}  Expansion base  
fromDigits        []       = 0
fromDigits {base} (d  ds) = toℕ d + fromDigits ds * base

-- toDigits b n yields the digits of n, in base b, starting with the
-- _least_ significant digit.
--
-- Note that the list of digits is always non-empty.

toDigits : (base : ) {base≥2 : True (2 ≤? base)} (n : ) 
            λ (ds : Expansion base)  fromDigits ds  n
toDigits base@(suc (suc k)) n = <′-rec Pred helper n
  where

  Pred = λ n   λ ds  fromDigits ds  n

  cons :  {m} (r : Digit base)  Pred m  Pred (toℕ r + m * base)
  cons r (ds , eq) = (r  ds , P.cong  i  toℕ r + i * base) eq)

  open ≤-Reasoning
  open +-*-Solver

  lem :  x k r  2 + x ≤′ r + (1 + x) * (2 + k)
  lem x k r = ≤⇒≤′ $ begin
    2 + x
      ≤⟨ m≤m+n _ _ 
    2 + x + (x + (1 + x) * k + r)
      ≡⟨ solve 3  x r k  con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r)
                              :=
                            r :+ (con 1 :+ x) :* (con 2 :+ k))
                 refl x r k 
    r + (1 + x) * (2 + k)
      

  helper :  n  <′-Rec Pred n  Pred n
  helper n                       rec with n divMod base
  helper .(toℕ r + 0     * base) rec | result zero    r refl = ([ r ] , refl)
  helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
    cons r (rec (suc x) (lem x k (toℕ r)))

------------------------------------------------------------------------
-- Showing digits

-- The characters used to show the first 16 digits.

digitChars : Vec Char 16
digitChars =
  '0'  '1'  '2'  '3'  '4'  '5'  '6'  '7'  '8'  '9' 
  'a'  'b'  'c'  'd'  'e'  'f'  []

-- showDigit shows digits in base ≤ 16.

showDigit :  {base} {base≤16 : True (base ≤? 16)}  Digit base  Char
showDigit {base≤16 = base≤16} d =
  Vec.lookup digitChars (Fin.inject≤ d (toWitness base≤16))