Generalize utility functions previously used for a single purpose #34
Conversation
|
Please give this PR a more descriptive name, and write PR description. Also, when stacking PRs it's best to keep this one in draft mode, and only request a review here after the other one gets merged, to avoid double reviewing the same code |
Equilibris
changed the title
Qpf/Macro/Data/Constructors.lean
Outdated
| Add convenient constructor functions to the environment | ||
| -/ | ||
| def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do | ||
| def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Ident) (ty : Term) := do |
There was a problem hiding this comment.
I'd prefer the return type (presumably CommandElabM Unit?) to be explicit.
Also, please write a docstring to explain what this does (and crucially, how it differs from mkConstructors).
Finally, I like to limit lines to 100 chars wide, just like in Mathlib. This line feels like it might be too long (but I haven't checked, we really should set up a linter of some sort)
Qpf/Macro/Data/Constructors.lean
Outdated
| Add convenient constructor functions to the environment | ||
| -/ | ||
| def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do | ||
| def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Ident) (ty : Term) := do |
There was a problem hiding this comment.
| def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Ident) (ty : Term) := do | |
| def mkConstructorsWithNameAndType (view : DataView) (shape : Name) (nameGen : CtorView → Name) (ty : Term) := do |
I feel like having the argument generate a Name is cleaner than making it generate Idents
Qpf/Macro/Data/View.lean
Outdated
| @@ -122,11 +122,15 @@ def DataView.addDeclNameSuffix (view : DataView) (suffix : String) : DataView | |||
|
|
|||
|
|
|||
| /-- Returns the fully applied form of the type to be defined -/ | |||
| def DataView.getExpectedType (view : DataView) : Term | |||
| := Syntax.mkApp (mkIdent view.shortDeclName) ( | |||
| def DataView.getExpectedTypeWithId (view : DataView) (id : Ident) : Term | |||
There was a problem hiding this comment.
Please explain in the docstring what id does, also, here, too I feel Name is more appropriate
| def DataView.getExpectedTypeWithId (view : DataView) (id : Ident) : Term | |
| def DataView.getExpectedTypeWithId (view : DataView) (id : Name) : Term |
Qpf/Macro/Data/View.lean
Outdated
| def DataView.getExpectedType (view : DataView) : Term | ||
| := view.getExpectedTypeWithId (mkIdent view.shortDeclName) |
There was a problem hiding this comment.
The style is to have := on the same line as the type
| def DataView.getExpectedType (view : DataView) : Term | |
| := view.getExpectedTypeWithId (mkIdent view.shortDeclName) | |
| def DataView.getExpectedType (view : DataView) : Term := | |
| view.getExpectedTypeWithId (mkIdent view.shortDeclName) |
Qpf/Macro/Data/View.lean
Outdated
| /-- Returns the fully applied, explicit (`@`) form of the type to be defined -/ | ||
| def DataView.getExplicitExpectedType (view : DataView) : CommandElabM Term | ||
| := let args := Macro.getBinderIdents view.binders.getArgs true |
There was a problem hiding this comment.
This function also has the wrong style, the := should be on the same line as CommandElabM Term
(This is code you haven't touched in this PR, though, so feel free to ignore.
Also, I don't remember if I wrote this, but it is very possible. I wrote a bunch of this stuff before I knew what the style should've been, so it's not necessarily good to just mimic the style of what's already there. Sorry 'bout that)
Make
mkConstructorsandgetExpectedTypemore versatile, this is done by extraction constants and turning them into arguments. This is done so they can be reused later at other points where a similar functionality is wanted.This should in practice be non-functional in the greater context of the code, but it allows for these functions that can be hooked into for more fine-grained control without requiring more boilerplate code.