Use implicit convention for extern function names?

[Timmmm]

I was thinking... instead of this:

val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int

Might it not be better to just have something like

extern val rem_round_zero : (int, int) -> int

And then the names actually used for each backend are constructed by convention. E.g. OCaml gets SailExtern.$name, C gets sail_extern_$name, interpreter gets $name (or sail_extern_$name?, etc.

It's a little bit more "magical" and less greppable/discoverable. But it means the Sail code doesn't have to care about a list of backends any more.

[Alasdair]

This would be nice, but I'm not sure how easy it would be to go back and clean everything up to make this work without causing a lot of backwards-compatibility headaches.

We do also allow:

val f : {c: "some_fast_implementation"} : T

// slow Sail implementation for other backends
function f() = ...

which would be a bit harder with this simpler scheme.

[Timmmm]

Good point. I also saw some declarations like:

val foo = "foo" : T

What does that mean? Is that from a time when there was only one backend or something?

[Alasdair]

That's for when the name is the same in all the backends, it's a shorthand for {_: "foo"}