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

Adding type aliases #704

Merged
merged 14 commits into from
Apr 1, 2021
Merged

Adding type aliases #704

merged 14 commits into from
Apr 1, 2021

Conversation

konnov
Copy link
Collaborator

@konnov konnov commented Mar 31, 2021

Per popular request this PR adds type aliases of the form:

@typeAlias FOO = [a: Int, b: Bool];

This closes #703.

  • Tests added for any new code
  • Ran make fmt-fix (or had formatting run automatically on all files edited)
  • Documentation added for any new functionality
  • Entry added to UNRELEASED.md for any new functionality

typeVar ::= <a single letter from [a-z]>

alias ::= <an identifier that matches [a-zA-Z_][a-zA-Z0-9_]* and
is neither typeConst, nor typeVar >
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since these patterns overlap, does this mean "is neither a (predefined) typeConst or typeVar"? If so, I'm not clear how the typeVar case applies, since typeVar's aren't defined previously, but just identified syntactically. Should you perhaps constrain aliases to being [A-Z_][a-zA-Z0-9_]* so there's no possibility of confusing a type variable for a type alias?

docs/src/adr/002adr-types.md Outdated Show resolved Hide resolved
Comment on lines +124 to +125
* `Proc` and `Faulty` are sets of the same type.
Their type is `Set(PID)`.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

where does PID come from? What does it mean?

Comment on lines 129 to 130
We extend the type grammar of `T` with one more rule that introduces a type
alias:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
We extend the type grammar of `T` with one more rule that introduces a type
alias:
We extend the type grammar of `T` with one more rule that introduces type
aliases:

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This intro to the section doesn't make sense to me, because the type alias is specified in the grammar to begin with, not added as an extensions here (the way the current document is written). Perhaps just say "kthe grammer of T includes a rule" rather than "we extend"?

docs/src/adr/002adr-types.md Outdated Show resolved Hide resolved
@@ -1,44 +0,0 @@
package at.forsyte.apalache.tla.typecheck
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this change related to the feature added in this PR?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. Caching is not consistent with type aliases. If we want to cache parsing results, we have to take the aliases into account. That seems to be too difficult. There is no good use case for caching anyways.

@konnov
Copy link
Collaborator Author

konnov commented Apr 1, 2021

The first solution to aliases was not working well:

  • It was introducing a new level of complexity in the type grammar.
  • It was sensitive to the order of declarations, which could change with the topological sort (done by the importer).

Here is a new solution. We just let the user redefine a constant type as an alias:

\* @typeAlias: ENTRY = Str;
\* @type: Int -> ENTRY;

I find this approach much more elegant. It also gives us another use for the type constants.

@konnov
Copy link
Collaborator Author

konnov commented Apr 1, 2021

@shonfeder, if you have time, please have a look at it.

@konnov konnov merged commit 1b897d9 into unstable Apr 1, 2021
@konnov konnov deleted the igor/type-aliases703 branch April 1, 2021 16:48
@apalache-bot apalache-bot mentioned this pull request Apr 5, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

[FEATURE] Introduce type aliases in Snowcat
2 participants