-
Notifications
You must be signed in to change notification settings - Fork 38
Implement namespaced constructors and operations #1092
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
base: master
Are you sure you want to change the base?
Conversation
@timsueberkrueb there is a LSP Server test failing:
Can I just update the number or do we want the change the behavior in the server? |
@timsueberkrueb Could you double check w.r.t. to the "outline" and holes panel? In particular, I am afraid that operations might now show up twice (once in the namespace and once outside). |
def consume(b: Bars) = b match { | ||
case Foo(Foo::Bar()) => 1 | ||
case Boo(Boo::Bar()) => 2 | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here you can see that we now can also disambiguate equally named constructors in patterns.
Yes, they do indeed occur twice now. ![]() |
I discussed this with @timsueberkrueb: Ideally, the semantics of
is
so the unprefixed constructors (and operations) should be listed as imports, not bindings. |
I implemented it, but it isn't that simple. Assume two files with the import semantics:
and
then the "generated" |
So, backtracking, the semantics implemented previously (and which I plan to go with for now) is
Since |
Constructors and operations are now defined in a namespace, named after the type.
For instance:
defines the constructor
TrafficLight::Red
, but also imports it asRed
. The same holds for operations, which can now (in principle) be disambiguated likecap.Nondet::flip()
.As a drive-by, I simplify the way operations are looked up and drop the unused effect on
Do
, which was in preparation fordo Nondet.flip()
, which now isdo Nondet::flip()
.