Extracting transpile_rust and polymorph_rust makefile targets from a couple of one-off spots into SmithyDafnyMakefile.mk.
Since the Dafny to Rust code generator is still under development, leverages the existing support for patch files and applies them to translated code as well. This does mean that the build process has to do transpile_rust before polymorph_rust, whereas up to now there was no dependency.
Changed the layout of the SimpleString generation target to put the Dafny-generated code into a separate dafny_impl sub-crate (and hence renames crate::implementation_from_dafny to ::simple_string_dafny in Rust code). This seems to be a better way to organize the code and support clean patching, since Rust doesn't have any built-in support for multiple equivalent source directories the way (for example) Gradle does, which we use to separate the Java code into dafny-generated, smithy-generated, and java (manually-written) source folders.
Populated rust patches for both StandardLibrary and SimpleString. The diffs are especially huge since the generated code is not well formatted yet, but it's a start for incremental improvement. :) The patches also add minimal tests, which are good to have on top of Dafny-generated tests once we get there.
Took advantage of the SRC_INDEX and TEST_INDEX variables to only attempt to translate a subset of code to Rust - the mechanism was intended more for replaceable modules, but also lets us get at least some testing coverage for Rust.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Description of changes:
Extracting
transpile_rustandpolymorph_rustmakefile targets from a couple of one-off spots intoSmithyDafnyMakefile.mk.transpile_rustbeforepolymorph_rust, whereas up to now there was no dependency.dafny_implsub-crate (and hence renamescrate::implementation_from_dafnyto::simple_string_dafnyin Rust code). This seems to be a better way to organize the code and support clean patching, since Rust doesn't have any built-in support for multiple equivalent source directories the way (for example) Gradle does, which we use to separate the Java code intodafny-generated,smithy-generated, andjava(manually-written) source folders.StandardLibraryandSimpleString. The diffs are especially huge since the generated code is not well formatted yet, but it's a start for incremental improvement. :) The patches also add minimal tests, which are good to have on top of Dafny-generated tests once we get there.SRC_INDEXandTEST_INDEXvariables to only attempt to translate a subset of code to Rust - the mechanism was intended more for replaceable modules, but also lets us get at least some testing coverage for Rust.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.