Implement unbounded ints/rationals in the Rust backend

[shadaj]

Implement unbounded ints/rationals in the Rust backend

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT
license.

---

Stack created with Sapling. Best reviewed with ReviewStack.

• Fix Rust compilation errors for unused types and constant fields #4450
• -> Implement unbounded ints/rationals in the Rust backend #4438

[keyboardDrummer]

One question that I have, which doesn't necessarily relate to this PR, but to the approach taken in Compiler-dafny.cs, is whether you've considered not just using ConcreteSyntaxTree instead of string, but to immediately generate the desired AST nodes.

I made a PR with a prototype of a SinglePassCompiler that doesn't use ConcreteSyntaxTree or string here: #3396

The idea is that SinglePassCompiler is made generic:

public abstract class GenericSinglePassCompiler<TExpression, TStatements, TStatement, TType, etc...>

Existing backends that want to use ConcreteSyntaxTree/ICanRender will inherit from a new type ConcreteSinglePassCompiler:

public abstract class ConcreteSinglePassCompiler 
  : GenericSinglePassCompiler<ICanRender, ConcreteSyntaxTree, ICanRender, ICanRender>, Plugins.Compiler

I think it does require more refactoring of SinglePassCompiler then you're currently doing though, although I haven't taken the time yet to understand the BuilderSyntaxTree<T> technique that you're currently using. For the GenericSinglePassCompiler approach, many methods have to be refactored so that the argument that is currently ConcreteSyntaxTree becomes a result value instead, so these functions can return AST nodes.

Maybe such as refactoring is not the best investment of your time, but I think it would be awesome to have what's currently SinglePassCompiler in a state where it doesn't relate to string or ConcreteSyntaxTree.

[shadaj]

@keyboardDrummer yeah, making SinglePassCompiler generic wrt ConcreteSyntaxTree would be quite nice. Even for our approach, there are situations where the compiler internally creates new ConcreteSyntaxTrees that cause trouble, so many of the refactoring steps have been to eliminate that. Would also be nice to eliminate assumptions about parenthesizing expressions, or how function calls are generated (right now the compiler unnecessarily assumes an order of receiver, then name, then args).

It's effectively what the Dafny-implemented backends look like, since there we have similar methods to generate statements/expressions/etc but the implementation is free to generate strings or its own representations of the target syntax.

[shadaj]

Because of the code blowup in the Dafny-to-C# compilation, instrumentation hangs and causes the CI to timeout. Since we ignore coverage of generated code anyways, this is safe.