Why does `OfScientific.ofScientific` take `e : ℕ`?

Stream: lean4

[Eric Wieser]

I'm a bit surprised the contract is

ofScientific (mantissa : Nat) (exponentSign : Bool) (decimalExponent : Nat)

instead of

ofScientific (mantissa : Nat) (decimalExponent : Int)

is there some reason relating to IEEE 754 why we permit both 1e0 and 1e-0 and allocate them different Exprs?

#check 1e0  -- 1e0
#check 1e-0 -- 1.0
#eval  1e0  -- 1.000000
#eval  1e-0 -- 1.000000

[Ruben Van de Velde]

Possibly this is trying to support all possible float bit patterns?

[Eric Wieser]

https://en.wikipedia.org/wiki/IEEE_754#/media/File:Float_example.svg doesn't have this exponentSign bit though

[Eric Wieser]

(it only has a regular sign bit, but that's handled by ofScientific m e vs -ofScientific m e)

[Ruben Van de Velde]

Oh right. Huh.

[Mario Carneiro]

I think this is just the natural result of parsing

[Mario Carneiro]

it's agnostic as to the way the data is stored in the target type or whether +0 and -0 are distinguished etc

[Eric Wieser]

I don't think the +0 vs -0 distinction would be relevant here even if it weren't agnostic, this is about $10^0$ vs $10^{-0}$ which not even floats distinguish

[Eric Wieser]

Mario Carneiro said:

I think this is just the natural result of parsing

I guess because there is no integer parser in the first place?

[Mario Carneiro]

Although, the mantissa being a Nat instead of a Nat plus exponent offset means that you can't really differentiate +0 and -0 anyway

[Mario Carneiro]

that is, 1.0e1 is interpreted as 10e+0 and 1.0e0 is the same as 10e-1, this is effectively an offset computed in Int and so e-0 is not a possible output

[Mario Carneiro]

Oh but there is also another consideration, which is that ofScientific takes raw Nat arguments

[Eric Wieser]

That sounds like the compelling one. Should we have some kind of RawNat type synonym to make that obvious from the docs?

[Eric Wieser]

Presumably that also means that lemmas which expand ofScientific should be inserting ofNats?

[Mario Carneiro]

simp does this already

[Eric Wieser]

Does rw?

[Mario Carneiro]

We could use "raw Int arguments" but currently core has no conception of this (norm_num does though)

[Mario Carneiro]

I'm not sure, you should check how ofNat is expanded in e.g. Nat.cast lemmas