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

Generalize utility functions previously used for a single purpose #34

Merged
merged 10 commits into from
Aug 14, 2024
Merged

Generalize utility functions previously used for a single purpose #34

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
d904907
refactor: extract ctors
Jul 25, 2024
05a9195
refactor: genralize utils
Jul 25, 2024
e5710e7
docs: why replacePrefix2 is different
Aug 8, 2024
0dc4cb3
refactor: use Lean's replacePrefix
Aug 8, 2024
c9a2348
Merge branch 'codef-1' into codef-2
Aug 8, 2024
83ef0a8
chore: style changes
Aug 8, 2024
432649e
Merge branch 'codef-1' into codef-2
Aug 8, 2024
456bfa6
Merge remote-tracking branch 'origin/master' into codef-2
Aug 13, 2024
da244f2
chore: fix ws
Equilibris Aug 13, 2024
7ac7a05
fix: comments
Aug 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 13 additions & 11 deletions Qpf/Macro/Data/Constructors.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
import Qpf.Macro.Data.Replace
import Qpf.Macro.Data.View

open Lean Meta Elab.Command
open Lean Meta Elab Elab.Command
open PrettyPrinter (delab)

namespace Data.Command
Expand All @@ -13,11 +13,7 @@ partial def countConstructorArgs : Syntax → Nat
| Syntax.node _ ``Term.arrow #[_, _, tail] => 1 + (countConstructorArgs tail)
| _ => 0

open Elab
/--
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
Copy link
Owner

@alexkeizer alexkeizer Aug 14, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

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)

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
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

for ctor in view.ctors do
trace[QPF] "mkConstructors\n{ctor.declName} : {ctor.type?}"
let n_args := (ctor.type?.map countConstructorArgs).getD 0
Expand All @@ -34,18 +30,15 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
else
`(fun $args:ident* => $pointConstructor ($shapeCtor $args:ident*))

let explicit ← view.getExplicitExpectedType
let type : Term := TSyntax.mk <|
(ctor.type?.map fun type =>
Replace.replaceAllStx view.getExpectedType explicit type
).getD explicit
(ctor.type?.map fun type => Replace.replaceAllStx view.getExpectedType ty type).getD ty
let modifiers : Modifiers := {
isNoncomputable := view.modifiers.isNoncomputable
attrs := #[{
name := `matchPattern
}]
}
let declId := mkIdent <| ctor.declName.replacePrefix (←getCurrNamespace) .anonymous
let declId := nameGen ctor

let cmd ← `(
$(quote modifiers):declModifiers
Expand All @@ -56,4 +49,13 @@ def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
elabCommand cmd
return ()

/--
Add convenient constructor functions to the environment
-/
def mkConstructors (view : DataView) (shape : Name) : CommandElabM Unit := do
let explicit ← view.getExplicitExpectedType
let nameGen := (mkIdent <| ·.declName.replacePrefix (←getCurrNamespace) .anonymous)

mkConstructorsWithNameAndType view shape nameGen explicit

end Data.Command
8 changes: 6 additions & 2 deletions Qpf/Macro/Data/View.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Owner

Choose a reason for hiding this comment

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

Please explain in the docstring what id does, also, here, too I feel Name is more appropriate

Suggested change
def DataView.getExpectedTypeWithId (view : DataView) (id : Ident) : Term
def DataView.getExpectedTypeWithId (view : DataView) (id : Name) : Term

:= Syntax.mkApp id (
(Macro.getBinderIdents view.binders.getArgs false)
)

/-- Returns the fully applied form of the type to be defined -/
def DataView.getExpectedType (view : DataView) : Term
:= view.getExpectedTypeWithId (mkIdent view.shortDeclName)
Copy link
Owner

Choose a reason for hiding this comment

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

The style is to have := on the same line as the type

Suggested change
def DataView.getExpectedType (view : DataView) : Term
:= view.getExpectedTypeWithId (mkIdent view.shortDeclName)
def DataView.getExpectedType (view : DataView) : Term :=
view.getExpectedTypeWithId (mkIdent view.shortDeclName)


/-- 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
Copy link
Owner

Choose a reason for hiding this comment

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

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)

Expand Down
Loading