[CakeML-dev] large_int

[Magnus Myreen]

On 5 March 2017 at 05:48, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> The comment next to the number here
>
> val large_int = ``268435457:int`` (* 2**28-1 *)
>
> https://github.com/CakeML/cakeml/blob/master/compiler/backend/bvl_to_bviScript.sml#L22
>
> does not match. (2**28-1 = 268435455).
>
> Which is correct?

I think it could even be (2**29)-1.

> Can this number be defined somewhere?

It is defined. It is defined there in bvl_to_bvi.

> And verified (connected to some
> proof)? Would backend_common be preferable for the definition than
> bvl_to_bvi?

It is meant to be a number that's large enough into fit a smallint
when all the tag bits and sign bits are taken into account. I needed
the number there in bvl_to_bvi, but I don't have access to the machine
size then. It seemed like too much effort to propagate the machine
size into the BVI semantics (and bvl_to_bvi compiler).

It doesn't matter if this number is a bit smaller than necessary, and
the number might disappear if we compile large numbers more
efficiently in the future.

I wouldn't worry about it, since there are much bigger issues to deal
with: I'll send a message in a little bit about max_app.

Cheers,
Magnus