Using type class methods for arithmetic operators

[krame505]

See #451. This project was started a while back, to change the various host-language operators into forwarding productions. This saves a significant amount of boilerplate in the Silver compiler, as specifying various analyses for these operators (type checking, flow analysis, implicit monad translation, java translation) can be avoided.

This change was done for the ++ and various equality operators, but wasn't quite finished for the remaining Boolean and arithmetic operators.

Supporting overloading for these operators is useful for a few reasons. One possibility is that one can write instances for abstract syntax operator productions in their language, providing a lightweight version of concrete object language syntax - one could write something like var(a) + var(b) * intConst(2). In simple languages, or extensions that introduce a new sort of expression, it may not be feasible to set up an extended version of Silver with quotation for the new expression nonterminal.
Note that this previously wasn't feasible with the need to supply a location annotation when applying these productions, but this is no longer an issue when using origin tracking.

Another motivation is that we currently only support Integer and Float as numeric types. There may be reasons to desire other representations of numbers, e.g. building an interpreter for a language that supports other sorts of numbers. At the moment changing the type checking logic for these operators would be quite annoying, but would be trivial with type classes. I can recall wanting an unlimited-width integer type at one point (but I don't quite remember why.)

One of @ericvanwyk's complaints is that add, sub, neg, etc. are taking names that should be available as the names of operator productions. I personally find addOp, subOp, etc. to be more descriptive names anyway. Or plus, minus, etc. are also options.

One can still define productions with the same name as functions in silver:core - however in other grammars importing the grammar defining these productions, one must import silver:core hiding add, sub, mul, ...;. We may consider improvements to Silver's module system, or name resolution semantics, to be able to state that one imported module should take precedence over another for name conflicts (should explicit imports always shadow silver:core?)

[ericvanwyk]

Using add and others in core is not a big deal, but it is a bit annoying that something common like add is taken and is not commonly used (except as the target of forwarding for the commonly used + symbol).

I'm not sure about addOp - this could be interpreted as the addition operator itself, not the production for an add expression. Or maybe not.

I can't see writing var(a) + var(b) - in a simple language we are probably trying to teach people how to use Silver so this would be inappropriate. In a complex one it seems to hide relevant details.

Can we organize core so that it exports + but not add?

[remexre]

I forget how the rules work exactly; could we have these typeclasses in silver:algebra, which is imported by but not exported from silver:core?

I'm not sure what the concern is for a complex language; assuming it's a term constructor, I don't see the footgun.

---

I think the bigger reason is so that it's less of a pain to add new numeric and numeric-like types; say we want to support warning on C23 code like:

constexpr uint64_t i = (uint64_t)5 + 5;
int xs[10] = { [i] = 4, 0 };

then we better have a type that can hold uint64_ts! (It would also probably not be the worst idea in the world to have the mathematical integers in the standard library.)

---

I think the case where we're overloading + et al to work on ASTs is maybe more palatable if we think of a DSL we're using internally to the compiler, rather than the input language.

For example, I would probably encode the SMT-LIB language (a DSL for talking to SMT solvers) in Silver as a nonterminal like SmtExpr<a>, where a is a Silver type corresponding to an SMT-LIB sort. (This maybe only works well as-is because I only use theories without user-defined types.)

We'd then have instances like BooleanAlgebra SmtExpr<Boolean>, EuclideanRing SmtExpr<Integer>, Ring SmtExpr<BitVec<N32>>, etc. (That's assuming Integer is the mathematical integers and N32 = S<S<S<S<...<Z>...>>>>, or a base-n>1 version of the same.)

[krame505]

The trouble is that silver:core:add always needs to be in scope to be referenced in the forward of +. So just moving it to another grammar doesn't help.

Otherwise, I agree with @remexre's points. Maybe we can chat about this at the meeting on Wednesday, if there is time.

One other point, in response to @ericvanwyk's concerns, is that it is okay if the short name add is shadowed - the full name just needs to be in scope. I went to check how well this works, and found that there are a few issues (and also some bugs with name resolution), but I have a fix that I will push shortly.

Currently, silver:core gets included in the same scope as grammar-level imports, but if instead we put it in another outer scope, then imports can shadow implicitly-imported things from silver:core. So if someone defines a production named add in their lang:host grammar, then other grammars importing lang:host would see their add production.

[ericvanwyk]

This seems reasonable - putting silver:core in an outer scope that can be shadowed.