Dafny version

4.2.0

Code to produce this issue

module AnyName {

    class B {
        const i := 1;
        constructor() {}
    }

    class AnyName {
        const j: B

        constructor ()
        {
            this.j := new B();
        }
    }
}

Command to run and resulting output

dafny build --target:py AnyName.dfy

cd AnyName-py/
python3
Python 3.11.2 (main, Aug 10 2023, 11:27:00) [Clang 14.0.3 (clang-1403.0.22.14.1)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> import AnyName
>>> a = AnyName.AnyName()
>>> a.ctor__()
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/Users/lucmcdon/Desktop/AnyName-py/AnyName.py", line 36, in ctor__
    nw0_ = AnyName.B()
           ^^^^^^^^^
AttributeError: type object 'AnyName' has no attribute 'B'

What happened?

In the generated Python, the AnyName class calls AnyName.B() in its ctor__ function.

However, AnyName is ambiguous within this function, as it is assigned twice:

• Once as the Dafny module on ~line 11: AnyName = sys.modules[__name__]
• A second time as the Dafny class on ~line 28: class AnyName:

I suspect the generated Python thinks that in AnyName.B(), AnyName is referring to the module, and not the class. However, during execution, AnyName actually refers to the class here, and the call fails.

I would expect to be able to write a class that shares the same name as the module and use other classes within that module.

One workaround might be to append some uncommon string to variable containing the result of the sys.modules call, e.g. AnyName_moduleref = sys.modules[__name__] to differentiate generated references to the module from any references to classes. I modified Dafny-generated code locally to make this change and was able to run the ctor__ function.

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

Mac