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

Automatic generation of constructors #10

Open
wants to merge 15 commits into
base: master
Choose a base branch
from

Conversation

edusporto
Copy link

This PR adds automatic generation of ADT constructors that could not be found by the book loading system.

Two points of discussion remain:

  1. If an ADT does not type check, it will still (wrongly) generate its constructors and save them into their files, since type checking happens after detection of unbound names. When the ADT is fixed by the user, the previously generated constructor will be bound and thus ignored by the construction generation system, forcing the user to manually delete the old constructors so new ones can be generated. What should be the intended behavior?
  2. If a constructor is unbound but a file with its name already exists, the file is overwritten by the new constructor. Should we keep this behavior or change it?

Suggestions are welcome!

edusporto added 12 commits April 5, 2024 19:58
TODO: fix constructor name comparison
TODO: Add new constructor to book and create file
TODO: Test for all of the `book`
TODO: Test with current `book`
TODO: deal with cases like this:
```
assertion `left == right` failed
  left: "λn ~λP λsucc λzero (succ n)"
 right: "λpred ~λP λsucc λzero (succ pred)"
```
TODO: Change test to loop through the entire book
A few modules were selected to compare their constructors with the generated ones.
@edusporto edusporto marked this pull request as ready for review April 11, 2024 00:47
@@ -128,7 +128,7 @@ impl Show {
},
Style::Glue => {
for (i, c) in child.iter().enumerate() {
if i > 0 {
if i > 0 && !c.is_empty() {
Copy link
Author

Choose a reason for hiding this comment

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

Need to check with Taelin that this won't break anything

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.

1 participant