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 module pyk.kore #2696

Merged
merged 52 commits into from
Jul 22, 2022
Merged

Add module pyk.kore #2696

merged 52 commits into from
Jul 22, 2022

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Jul 1, 2022

Closes #2626

This PR introduces the pyk.kore module. It contains:

  • Class hierarchy for the Kore abstract syntax
  • Parsing and unparsing in textual Kore format
  • Parsing and unparsing in JSON format

Currently, only syntactic validation is performed on the AST (e.g. identifiers are lexically correct), semantic validation rules described in https://github.com/runtimeverification/haskell-backend/blob/master/docs/kore-syntax.md#validity are not implemented.

@tothtamas28 tothtamas28 added the pyk label Jul 1, 2022
@tothtamas28 tothtamas28 self-assigned this Jul 1, 2022
@tothtamas28 tothtamas28 force-pushed the pyk-kore branch 6 times, most recently from c9655ff to da871a4 Compare July 8, 2022 15:48
@tothtamas28 tothtamas28 force-pushed the pyk-kore branch 6 times, most recently from 6d5e359 to acdd454 Compare July 18, 2022 13:44
@tothtamas28 tothtamas28 marked this pull request as ready for review July 19, 2022 13:13
Copy link
Contributor

@radumereuta radumereuta left a comment

Choose a reason for hiding this comment

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

These parser files are very large. I don't feel confident reviewing them. At least not by myself.
Are they generated by any chance?

@tothtamas28
Copy link
Contributor Author

Are they generated by any chance?

No. Since the Kore grammar is relatively simple, I wrote the parser manually.

@ehildenb
Copy link
Member

Looks fine to me on first glance (no deep review of the Kore). I'm sure we'll find problems as we test, but no need to hang up the first version of it too long.

@ehildenb
Copy link
Member

We likely will want to use some faster parser eventually, but we can cross that bridge when we come to it, and by then we'll have more test-cases we can use.

@rv-jenkins rv-jenkins merged commit 1e28381 into master Jul 22, 2022
@rv-jenkins rv-jenkins deleted the pyk-kore branch July 22, 2022 07:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Kore data-structures and parser in pyk
4 participants