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 all commits
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
5 changes: 5 additions & 0 deletions src/Init/Data/Ord.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,11 @@ instance : Ord USize where
instance : Ord Char where
compare x y := compareOfLessAndEq x y

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

def ltOfOrd [Ord α] : LT α where
lt a b := compare a b == Ordering.lt
Expand Down
32 changes: 14 additions & 18 deletions src/Lean/Parser/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1358,9 +1358,9 @@ def keepNewError (s : ParserState) (oldStackSize : Nat) : ParserState :=
match s with
| ⟨stack, lhsPrec, pos, cache, err⟩ => ⟨keepTop stack oldStackSize, lhsPrec, pos, cache, err⟩

def keepPrevError (s : ParserState) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option Error) : ParserState :=
def keepPrevError (s : ParserState) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option Error) (oldLhsPrec : Nat) : ParserState :=
match s with
| ⟨stack, lhsPrec, _, cache, _⟩ => ⟨stack.shrink oldStackSize, lhsPrec, oldStopPos, cache, oldError⟩
| ⟨stack, _, _, cache, _⟩ => ⟨stack.shrink oldStackSize, oldLhsPrec, oldStopPos, cache, oldError⟩

def mergeErrors (s : ParserState) (oldStackSize : Nat) (oldError : Error) : ParserState :=
match s with
Expand Down Expand Up @@ -1415,28 +1415,24 @@ def runLongestMatchParser (left? : Option Syntax) (startLhsPrec : Nat) (p : Pars

def longestMatchStep (left? : Option Syntax) (startSize startLhsPrec : Nat) (startPos : String.Pos) (prevPrio : Nat) (prio : Nat) (p : ParserFn)
: ParserContext → ParserState → ParserState × Nat := fun c s =>
let score (s : ParserState) (prio : Nat) :=
(s.pos.byteIdx, if s.errorMsg.isSome then (0 : Nat) else 1, prio)
let previousScore := score s prevPrio
let prevErrorMsg := s.errorMsg
let prevStopPos := s.pos
let prevSize := s.stackSize
let prevLhsPrec := s.lhsPrec
let s := s.restore prevSize startPos
let s := runLongestMatchParser left? startLhsPrec p c s
match prevErrorMsg, s.errorMsg with
| none, none => -- both succeeded
if s.pos > prevStopPos || (s.pos == prevStopPos && prio > prevPrio) then (s.replaceLongest startSize, prio)
else if s.pos < prevStopPos || (s.pos == prevStopPos && prio < prevPrio) then ({ s.restore prevSize prevStopPos with lhsPrec := prevLhsPrec }, prevPrio) -- keep prev
-- it is not clear what the precedence of a choice node should be, so we conservatively take the minimum
else ({s with lhsPrec := s.lhsPrec.min prevLhsPrec }, prio)
| none, some _ => -- prev succeeded, current failed
({ s.restore prevSize prevStopPos with lhsPrec := prevLhsPrec }, prevPrio)
| some oldError, some _ => -- both failed
if s.pos > prevStopPos || (s.pos == prevStopPos && prio > prevPrio) then (s.keepNewError startSize, prio)
else if s.pos < prevStopPos || (s.pos == prevStopPos && prio < prevPrio) then (s.keepPrevError prevSize prevStopPos prevErrorMsg, prevPrio)
else (s.mergeErrors prevSize oldError, prio)
| some _, none => -- prev failed, current succeeded
let successNode := s.stxStack.back
let s := s.shrinkStack startSize -- restore stack to initial size to make sure (failure) nodes are removed from the stack
(s.pushSyntax successNode, prio) -- put successNode back on the stack
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 =>
match prevErrorMsg with
| none =>
-- it is not clear what the precedence of a choice node should be, so we conservatively take the minimum
({s with lhsPrec := s.lhsPrec.min prevLhsPrec }, prio)
| some oldError => (s.mergeErrors prevSize oldError, prio)

def longestMatchMkResult (startSize : Nat) (s : ParserState) : ParserState :=
if s.stackSize > startSize + 1 then s.mkNode choiceKind startSize else s
Expand Down
3 changes: 3 additions & 0 deletions tests/lean/longestParsePrio.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
syntax "have" ":" term : tactic
example : False := by
have : True := by simp [ -- should *not* parse the shorter `have` syntax and then fail on `:=`
4 changes: 4 additions & 0 deletions tests/lean/longestParsePrio.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
longestParsePrio.lean:4:0: error: unexpected end of input; expected ']'
longestParsePrio.lean:2:19-3:26: error: unsolved goals
this : True
⊢ False