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.

Sign up for GitHub

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

Jump to bottom

Refactor datatypes #338

Closed
wants to merge 6 commits into from
Closed

Refactor datatypes #338

wants to merge 6 commits into from

Conversation

janvrany
Copy link
Collaborator

@janvrany janvrany commented Aug 7, 2024

My stab on refactoring datatypes. Not finished.

@janvrany
[Z3] Remove unused ctx instvar from Z3Datatype
c0f3e47
@janvrany
[Z3]: Refactor Z3Datatype class >> createDatatypes:
ca52a53 
Use more descriptive variable names and replace unnecessary `#collect:`
with `#do:` to improve readability.
@janvrany
[Z3] Implement Object >> toDatatype:
a126fe3
@janvrany
[Z3] Add Z3DatatypeComponent
d981f77 
Instances if datatype component keep constructor, recognizer and accessor
functions.
@janvrany
[Z3] Add "instance creation API" to Z3DatatypeComponent
c42d3c7 
This allows one to instantiate datatype like

   listSort cons with:1 with: listSort nil new
@janvrany
[Z3] Implement Datatype >> is:
e91e630 
This allow for tests like:

   someList is: listSort cons
@shingarov shingarov linked an issue Aug 8, 2024 that may be closed by this pull request
Idiomatic Smalltalk API for Z3 Datatypes #339
Open
@shingarov shingarov added the backburner TODO at some future date label Aug 8, 2024
@shingarov
Copy link
Owner

For the time being, MonomorphizedDataDecl appears to serve reasonably well. I am not 100% pleased by this API shape, because the multiple levels of create entail multiple levels of the Hotel, just for datatype induction. Maybe this intermediate level is best replaced by biting the bullet and going from DataDecl to the C API directly, but the current code seems to work fine so let's keep it that now.

@shingarov shingarov closed this Nov 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
backburner TODO at some future date
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Idiomatic Smalltalk API for Z3 Datatypes
2 participants
@janvrany @shingarov