K float regex vs Plutus spec float regex

[ayberkt]

In the lexical grammar specification of Plutus Core, the following regex is given for floats:

[+-]?[0-9]+(\.[0-9]+e?|e)

This differs from the regex for K's builtin Float sort. Since we most certainly do not want to re-implement float operations, we need to consider how we will hook this one to the built-in one.

This issue is not of extreme urgency as the K Float sort should be able to parse all Plutus floats. We should, however, still consider how we will handle this in the long term.

[daejunpark]

@ayberkt You may want to take a look at what KJS does: https://github.com/kframework/javascript-semantics/blob/master/js-orig-syntax.k#L95-L96 while it uses the old K parser though.

[ayberkt]

Thanks @daejunpark! This was the kind of thing I was looking for.