Dafny compiler plugin to mangle extern arguments

[robin-aws]

Follow-up from dafny-lang/dafny#2952, where we collectively decided it didn't make sense for Dafny itself to do this, but it was a reasonable external customization.

The Smithy-to-Dafny code generation will create extern declarations like the following:

module {:extern "Dafny.Aws.EncryptionSdk.Core"} Aws.Crypto {
  // ...
}

The issue is that this assumes a single extern declaration will work for every target language, but Dafny doesn't really guarantee that, and in practice {:extern} needs to be customized per target language. In particular, Go modules can't have periods in them.

It is reasonable, instead, for a polymorph user to provide a compiler plugin that will replace "Dafny.Aws.EncryptionSdk.Core" with "Dafny_mAws_mEncryptionSdk_mCore" when compiling the Dafny to Go, for example. There's a good chance more of the functionality of polymorph could find it's way into such a plugin in the future as well.

[texastony]

Interesting.
I have brought up this issue internally before.
I was going to suggest using regular expressions so we could convert all the extern references,
Polymorph generated or otherwise,
as is done in an internal project.

[robin-aws]

#528 is the better way to go here