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

Add support for sum types in the simulator #1242

Merged
merged 7 commits into from
Nov 10, 2023
Merged

Conversation

shonfeder
Copy link
Contributor

@shonfeder shonfeder commented Nov 8, 2023

Closes #1033

Adds support for sum types to the compiler (and so the simulator):

  • Generalizes the REPL so it can compile all the declarations parsed out of its
    input, instead of just the last one (required to enable sum type declarations
    to be entered in the REPL).
  • Adds graphics for pretty printing variants.
  • Adds evaluation of constructors, requiring a new runtime value to represent
    variants.
  • Adds evaluation of match expressions, which eliminate variants.

The history is clean enough that it would probably help to review by commit.

  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality
  • Feature table on README.md updated for any listed functionality

@shonfeder shonfeder marked this pull request as draft November 8, 2023 22:00
@shonfeder shonfeder changed the title WIP: Add support for sum types in the simulator Add support for sum types in the simulator Nov 10, 2023
Shon Feder added 6 commits November 9, 2023 23:06
This is required in order to support sum type declarations in the REPL.

Sum type declarations work like this this: When a type alias for a sum
is declared, e.g., `type T = A | B`, the parser expands this into 3 declarations:

```
type T = A | B

val A : T = variant("A", {})
val B : T = variant("B", {})
```

However, the previous implementation the read and eval parts of the REPL
took the input read, ran it thru the parser, then took only the *last*
declaration, ignoring anything else. As a result, the type annotation
sealing the generated operators with the proper sum type was in the
context during type checking.

This behavior of dropping all but the last declaration is completely
unnecessary, so this change generalizes the read and eval to work on any
sequence of declarations that are parsed out of the input.
@shonfeder shonfeder force-pushed the 1033/sum-types-in-simulator branch from 6abf740 to 58984c1 Compare November 10, 2023 04:07
@shonfeder shonfeder marked this pull request as ready for review November 10, 2023 04:07
@shonfeder shonfeder requested review from bugarela and konnov November 10, 2023 04:12
Copy link
Collaborator

@bugarela bugarela left a comment

Choose a reason for hiding this comment

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

Looks great, I'm super excited to try it out! I only have some comments on the pluralization of some methods 😄

quint/src/quintAnalyzer.ts Outdated Show resolved Hide resolved
quint/src/repl.ts Outdated Show resolved Hide resolved
@shonfeder
Copy link
Contributor Author

Thanks for the review and corrections! I fixed the plurals :)

@shonfeder shonfeder enabled auto-merge November 10, 2023 13:47
@shonfeder shonfeder merged commit c60ff77 into main Nov 10, 2023
15 checks passed
@shonfeder shonfeder deleted the 1033/sum-types-in-simulator branch November 10, 2023 13:55
@konnov
Copy link
Contributor

konnov commented Nov 10, 2023

I am too late with the review. This is amazing :)

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.

Support sum types in the simulator
3 participants