Skip to content
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

[FEATURE] Extending operator declarations with type annotations #263

Closed
konnov opened this issue Oct 9, 2020 · 1 comment
Closed

[FEATURE] Extending operator declarations with type annotations #263

konnov opened this issue Oct 9, 2020 · 1 comment
Assignees
Labels
FTC-Snowcat Feature: Fully-functional type checker Snowcat new New issue to be triaged.

Comments

@konnov
Copy link
Collaborator

konnov commented Oct 9, 2020

This topic pops up from time to time. Sometimes, we have to annotate operators, e.g., with types or the sets of assigned variables, #226 and #261.

It looks to me that annotating expressions is a too fine-grained approach. On the other hand, we can annotate operator definitions. I see two options:

  1. Add annotations directly in TlaOperDecl,
  2. Similar to TlaEx, introduce a uid in TlaOperDecl and store annotations as maps from uid to whatever.

I think the second approach is more flexible and extendable, but we will have to extend TransformationListener.

@Kukovec what is your opinion?

@konnov konnov added the new New issue to be triaged. label Oct 9, 2020
@konnov konnov self-assigned this Oct 9, 2020
@konnov konnov added this to the v0.9.0-tool-typecheck milestone Oct 9, 2020
@konnov
Copy link
Collaborator Author

konnov commented Oct 14, 2020

Duplicate of #262

@konnov konnov marked this as a duplicate of #262 Oct 14, 2020
@konnov konnov closed this as completed Oct 14, 2020
@konnov konnov added the FTC-Snowcat Feature: Fully-functional type checker Snowcat label Dec 6, 2020
@konnov konnov modified the milestones: v0.9.0-tool-typecheck, backlog2020 Dec 11, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
FTC-Snowcat Feature: Fully-functional type checker Snowcat new New issue to be triaged.
Projects
None yet
Development

No branches or pull requests

1 participant