not function in float/common.sail should be in prelude.sail?

[Timmmm]

In float/common.sail there is

val      not : forall ('p : Bool). bool('p) -> bool(not('p))
function not(b) = not_bool(b)

This is generic and doesn't really have anything to do with float. Should it really be there? I think it should go in prelude.sail.

Note that the RISC-V model has the exact same function in its prelude.sail, so that would technically be a breaking change I guess... but it seems more sensible than having it in float/common.sail.

If you do move it to Sail's prelude.sail it might make sense to also add a load of the other stuff in RISC-V's prelude.sail, which kind of feel like they should be included by default. E.g:

• ones(), zeros()
• The *_round_zero declarations.
• sign_extend(), zero_extend()
• The >_s etc. operators.

Maybe there's a reason for not including them, but I feel like those things aren't every going to vary by architecture surely?

[Alasdair]

Maybe not should also be an overload so you can use it on bitvectors as well.

I think the reason we didn't want to use them was we were following convention and argument order for ASL when translating the ARM specs so we had ZeroExtend there, and the hand-written RISC-V spec was mostly snake_case function names.

We could add them in separate files that aren't included in the prelude.sail file by default (then add them in later if we want, after they are no-longer defined in the RISC-V model).

[Timmmm]

Maybe not should also be an overload so you can use it on bitvectors as well.

Yeah, I dunno... the RISC-V model uses the ~ operator as an overload for both IIRC. & works for bools and bit vectors in Sail... But it's definitely weird to use ~ for bools, and ~ is weird in general since it's a function so you can't do ~foo. Hmm.

We could add them in separate files that aren't included in the prelude.sail file by default (then add them in later if we want, after they are no-longer defined in the RISC-V model).

Yeah that seems like a very good idea.