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

Make handling of names in mlang nominal #810

Merged
merged 35 commits into from
Dec 12, 2023

Conversation

elegios
Copy link
Contributor

@elegios elegios commented Nov 30, 2023

This PR replaces #809, to be able to separately merge the nominal changes without the updates because of the new type-checker.

In this PR:

  • Nominal handling
  • Merging of definitions using with, though this excludes renaming presently; it's only allowed if all things getting merged have the same original string name.
  • Fixing the compiler and the test suite such that it compiles under this slightly more strict handling of things.

Not included, but previously discussed:

  • Typechecker-related changes, these will be presented in a separate PR
  • Renaming of declarations/definitions from extended language fragments (as mentioned above; merging things with different string names requires a rename along the way).

Important: The changes here should be checked against the other dependent repositories as well. We believe we found and fixed everything before the paper deadline, but those PRs haven't necessarily been merged yet:

Finally, it's worth mentioning that the PRs in the dependent repos can be merged before this one; the required changes should be fully backwards-compatible.

@david-broman david-broman merged commit cd3d917 into miking-lang:develop Dec 12, 2023
2 checks passed
@elegios elegios deleted the only-nominal branch May 10, 2024 11:54
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.

5 participants