Skip to content

Import Cryptol enum types as SAWCore datatypes - #3373

Draft
brianhuffman wants to merge 3 commits into
masterfrom
bh/cryptol-enum
Draft

Import Cryptol enum types as SAWCore datatypes#3373
brianhuffman wants to merge 3 commits into
masterfrom
bh/cryptol-enum

Conversation

@brianhuffman

Copy link
Copy Markdown
Contributor

WIP

@brianhuffman

Copy link
Copy Markdown
Contributor Author

The only important test failure is in test3305, introduced in #3307, which tests the support for derived Eq, Cmp and SignedCmp instances for Cryptol enum types.

This PR won't be ready until I implement class dictionaries for enum-derived datatypes. One way to do it would be to define a special "representation" function for each datatype that converts it to the old-style nested-eithers-and-products form. Then we could reuse the existing dictionary constructors added in #3307, and lift them to the datatypes using the rep function.

@RyanGlScott

Copy link
Copy Markdown
Contributor

How is the namespacing for Cryptol-imported enums handled? For instance, if you import two enums named E, one from module A and another from module B, are they disambiguated?

This PR won't be ready until I implement class dictionaries for enum-derived datatypes. One way to do it would be to define a special "representation" function for each datatype that converts it to the old-style nested-eithers-and-products form. Then we could reuse the existing dictionary constructors added in #3307, and lift them to the datatypes using the rep function.

That would work, although I'd be a bit sad to have to still rely on the sum-of-products even after switching to a SAWCore datatype representation---the latter was supposed to subsume it!

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.

2 participants