cryptol-saw-core: Basic FLiteral support

[RyanGlScott]

Fixes #3045.

[RyanGlScott]

Oops, I forgot to add an implementation of PFLiteral for TCFloat (mirroring PLiteralFloat). I'll do that shortly.

[sauclovian-g]

Is there any reason not to put all four arguments in? Unless it comes unstuck that seems preferable when someone goes to actually implement it...

[sauclovian-g]

(also, what do the arguments mean? the only documentation I can find is GaloisInc/cryptol#1654, which isn't very explicit)

[RyanGlScott]

I originally punted on making PFLiteral actually use the arguments, since other parts of SAW will choke on Rational/Float values anyway. But fair enough, I might as well fill this part in while I'm in the neighborhood. I've pushed a new version of the PR which does this.

(also, what do the arguments mean? the only documentation I can find is GaloisInc/cryptol#1654, which isn't very explicit)

These are explained in the docstring for the FLiteral class (here).

[sauclovian-g]

Thanks!

[sauclovian-g]

also I don't think this is right any more

[RyanGlScott]

This is correct. The type of PFLiteral is still sort 0 -> sort 0, so we only need to supply it with a single argument. The remaining three arguments (m, n, and r) are only used when actually invoking a PFLiteral dictionary to construct a fractional value, as seen in the implementations of things like PFLiteralRational.