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

fix: prefer longer parse even if unsuccessful #1658

Merged
merged 2 commits into from
Sep 28, 2022
Merged

fix: prefer longer parse even if unsuccessful #1658

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8f2e7da
fix: prefer longer parse even if unsuccessful
Kha Sep 22, 2022
cb9e35f
refactor: `lexOrd` should not be an instance
Kha Sep 28, 2022
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
3 changes: 2 additions & 1 deletion src/Init/Data/Ord.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,8 @@ instance : Ord USize where
instance : Ord Char where
compare x y := compareOfLessAndEq x y

instance lexOrd [Ord α] [Ord β] : Ord (α × β) where
/-- The lexicographic order on pairs. -/
def lexOrd [Ord α] [Ord β] : Ord (α × β) where
compare p1 p2 := match compare p1.1 p2.1 with
| .eq => compare p1.2 p2.2
| o => o
Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Parser/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1424,7 +1424,7 @@ def longestMatchStep (left? : Option Syntax) (startSize startLhsPrec : Nat) (sta
let prevLhsPrec := s.lhsPrec
let s := s.restore prevSize startPos
let s := runLongestMatchParser left? startLhsPrec p c s
match compare previousScore (score s prio) with
match (let _ := @lexOrd; compare previousScore (score s prio)) with
Copy link
Member Author

Choose a reason for hiding this comment

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

Is this the correct idiom then :) ?

Copy link
Collaborator

Choose a reason for hiding this comment

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

You can also do local attribute [instance] lexOrd before the function, or have a type alias Lex A B on which to unconditionally put the instance. But this way is fine too, or (inst := lexOrd) in compare. If this program were subject to proofs I would generally prefer haveI here to avoid creating the additional let binding in the generated term, but for this code that's not really a concern and the compiler will normalize the two variants the same anyway.

Copy link
Member

Choose a reason for hiding this comment

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

I will merge as-is. I think the haveI/letI remark is important, we should discuss it in the next dev-meeting. We also get back to the let vs let dep discussion. It would be great to use the same style for letI (let inl?), and have it as part of the let family: let, let rec, let dep, let mut, ...

| .lt => (s.keepNewError startSize, prio)
| .gt => (s.keepPrevError prevSize prevStopPos prevErrorMsg prevLhsPrec, prevPrio)
| .eq =>
Expand Down