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

feat: generalize constructor generation further #40

Merged
merged 6 commits into from
Aug 19, 2024

Conversation

Equilibris
Copy link
Collaborator

We need a more general notion of constructor generation. The features we need are:

  • The ability to change the output type to the desired type
  • The ability to control what a recursive type should be able to be replaces with (for DeepThunk generation)
  • The ability to add required binders used in for-example explicit types (in the case of DeepThunk this is the recall parameter)

In this PR we add these features while keeping the behaviour for the specialized case unchanged. This PR is non-functional in place of current code

Copy link
Contributor

@AtticusKuhn AtticusKuhn left a comment

Choose a reason for hiding this comment

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

Looks good to me.

let recType := view.getExpectedType
let forms := RecursionForm.extract ctor recType

let x := forms.map $ RecursionForm.replaceRec view.getExpectedType argTy
Copy link
Contributor

Choose a reason for hiding this comment

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

I would prefer a more descriptive name than "x".

Qpf/Macro/Data/Constructors.lean Outdated Show resolved Hide resolved
Co-authored-by: Atticus Kuhn <52258164+AtticusKuhn@users.noreply.github.com>
@alexkeizer
Copy link
Owner

alexkeizer commented Aug 16, 2024

This PR is non-functional in place of current code

I guess what you mean here is that you generalize a bunch of things, but don't use the extra general capabilities, leaving the existing behaviour unchanged? I would reserve the claim "non-functional change" for PRs that really only move around definitions, or change the way somethings is phrased to an alternative, but 100% equivalent statement.

Here, I would instead flag it as something akin to: "we don't yet use the more general capabilities (but require them for a future PR), so the behaviour of existing code is unchanged".

Copy link
Owner

@alexkeizer alexkeizer left a comment

Choose a reason for hiding this comment

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

I agree with Atticus' comment about having a more descriptive name, and would like you to phrase the docstring a bit more clearly.

Otherwise, LGTM

@@ -17,9 +18,13 @@ partial def countConstructorArgs : Syntax → Nat
Add definitions for constructors
that are generic across two input types shape and name.
Additionally we allow the user to control how names are generated.
The binders param allows for adding constant binders to an expression.
Copy link
Owner

Choose a reason for hiding this comment

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

Suggested change
The binders param allows for adding constant binders to an expression.
Any binders passed in `binders` are added as parameters to the generated constructor

def mkConstructorsWithNameAndType
(view : DataView) (shape : Name)
(nameGen : CtorView → Name) (argTy retTy : Term)
(binders : TSyntaxArray ``Parser.Term.bracketedBinder)
Copy link
Owner

Choose a reason for hiding this comment

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

Suggested change
(binders : TSyntaxArray ``Parser.Term.bracketedBinder)
(binders : TSyntaxArray ``Parser.Term.bracketedBinder := #[])

This seems like a good place to use a default value (but feel free to ignore if you disagree)

William Sørensen added 2 commits August 19, 2024 13:06
@Equilibris Equilibris changed the base branch from extract-rec-form-handling to master August 19, 2024 12:08
@Equilibris Equilibris merged commit 5ace7ca into master Aug 19, 2024
2 checks passed
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.

3 participants