[Python] `function method` externs are generated with odd syntax

[lucasmcdonald3]

Dafny version

4.3.0 (specifically after commit ba3bac3)

Code to produce this issue

module {:extern "AnyModule"} Any.Module {

    method {:extern "AnyModule", "anyMethod"} anyMethod() {
        print("Any method");
    }

    function method {:extern "AnyModule", "anyFunctionMethod"} anyFunctionMethod() : string {
        "s"
    }

    method callExterns() {
        anyMethod();
        var a := anyFunctionMethod();
    }
}

Command to run and resulting output

dafny AnyModule.dfy -compileTarget:py -functionSyntax:3

Resulting generated code snippet:

AnyModule.anyMethod()
d_0_a_: _dafny.Seq
d_0_a_ = AnyModule_anyFunctionMethod()

What happened?

The syntax AnyModule_anyFunctionMethod() is strange; I would expect AnyModule.anyFunctionMethod. That syntax is more idiomatic and the same as extern methods.

I'm wondering if this is a subtle unintended regression that was introduced in the linked commit, or is this an intentional change?

If it's a regression, it's easy to work around for now. The impact is that I have to write externs for function methods in non-idiomatic ways.

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

I'm wondering if this is a subtle unintended regression that was introduced in the linked commit, or is this an intentional change?

The former, but it's not something that we should fix by reverting a previous change because that would also revert the improvement from there.

Improving the behavior as you suggest would require more changes. If there's a particular urgency in doing this, please let us know !