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] Parse annotations from the SANY comments #226

Closed
konnov opened this issue Sep 23, 2020 · 2 comments
Closed

[FEATURE] Parse annotations from the SANY comments #226

konnov opened this issue Sep 23, 2020 · 2 comments
Assignees
Labels
FTC-Snowcat Feature: Fully-functional type checker Snowcat new New issue to be triaged.

Comments

@konnov
Copy link
Collaborator

konnov commented Sep 23, 2020

As discussed in #162, it should be possible to write type annotations in comments:

VARIABLE
  \* type: Set(Int)
  S

\* type: (Int) => Bool
Mem(e) == \E x \in S: x = e

We should integrate annotations in SanyImporter and propagate them to the type checker.

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

konnov commented Nov 8, 2020

It is actually a good idea to hide the annotations in comments. Our current approach with extending the Apalache module introduces an additional dependency.

@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, backlog2021 Dec 11, 2020
@konnov konnov modified the milestones: backlog2021, January iteration Jan 4, 2021
@konnov
Copy link
Collaborator Author

konnov commented Jan 28, 2021

This is implemented in #503.

@konnov konnov closed this as completed Jan 28, 2021
This was referenced Feb 1, 2021
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