`showHexa` from `Data.Word64.Show` blows up when normalizing from Emacs

[bkomuves]

The function Data.Word64.Show.showHexa blows up when I try to normalize for example showHexa (fromℕ 0xdeadcafe) in Emacs.

The reason for this presumably is that it uses Data.Nat.Show.showInBase, which in turn uses Data.Digit.toDigits, which produces a proof term too, not only the result.

(The same holds for Data.Word8.Show.showHexa, but as those numbers are small, the effect is less pronounced.)

On the other hand, Data.Nat.Show.show does not suffer from the same problem, because it never tries to build a proof term behind the scene.

The simplest fix would be to change the implementation of showHexa to be more similar to Data.Nat.Show.show. Here is one possible way to do that:

open import Data.Bool
open import Data.Nat
open import Data.List using ( List )
open import Data.String 
open import Data.Word64

open import Data.Nat.Show as ℕ
open import Data.Digit using ( toNatDigits )
open import Data.Char as Char
open import Function.Base using ( _$_ ; _∘′_ )

toHexDigitChar : ℕ → Char
toHexDigitChar n with n <ᵇ 10
toHexDigitChar n | true  = Char.fromℕ (n      + Char.toℕ '0')
toHexDigitChar n | false = Char.fromℕ (n ∸ 10 + Char.toℕ 'a')

toHexadecimalChars : ℕ → List Char
toHexadecimalChars = Data.List.map toHexDigitChar ∘′ toNatDigits 16

showHexa : Word64 -> Strings
showHexa w 
  = "0x" ++_
  $ padLeft '0' 16
  $ Data.String.fromList  
  $ toHexadecimalChars (Data.Word64.toℕ w)

(btw, currently Data.Word64.Show.showHexa pads to 8 digits, but 64 bit numbers require 16 digits... I changed that too above)

[JacquesCarette]

Sounds good to me -- @jmougeot , want to give this a try?

[jamesmckinna]

See also #2218 ?

[jmougeot]

Sure, I can give this a try.

[jamesmckinna]

It's possible that the 'real' problem is with Data.Digit.toDigits being too strict in the second clause of:

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

where the match on refl forces the unification of n and toℕ r + (1 + x) * (2 + k), and hence permits the wf-recursive call.

To make the analysis less strict would require a version of cast (which doesn't evaluate its argument) for the Pred defined there, but it's still not completely obvious to me that the call in Data.Nat.Show.charsInBase would be improved in complexity?

[jamesmckinna]

As to the suggested simplifications, avoiding computing the proof at all, there is a unnecessary/undesirable appeal

toHexDigitChar n with n <ᵇ 10

to with when a simpler if_then_else would suffice... cf. #2123