03bd8847dc
This PR fixes the termination checker reporting errors at the wrong recursive call site when a function contains structurally-identical recursive calls at different source locations. The `_recApp` `MData` attached to recursive applications carried the attached `Syntax`, but two structurally-equal `MData` wrappers could be merged by hashconsing/simplification, so the syntax of the first call ended up associated with both call sites. We now also store the source byte position as `_recAppPos`, which keeps the wrappers distinct. Closes #13444.
110 lines
3 KiB
Text
110 lines
3 KiB
Text
Inferred termination measure:
|
|
termination_by n - i
|
|
Inferred termination measure:
|
|
termination_by xs.size - i
|
|
Inferred termination measure:
|
|
termination_by xs.size - i
|
|
Inferred termination measure:
|
|
termination_by (xs.size - i, ys.size - j)
|
|
Inferred termination measure:
|
|
termination_by (xs.size - i, i - j)
|
|
Inferred termination measure:
|
|
termination_by (xs.size - i, i)
|
|
guessLexDiff.lean:84:4-84:11: error: fail to show termination for
|
|
failure
|
|
with errors
|
|
failed to infer structural recursion:
|
|
Not considering parameter xs of failure:
|
|
it is unchanged in the recursive calls
|
|
Cannot use parameter i:
|
|
failed to eliminate recursive application
|
|
_root_.failure xs i
|
|
|
|
|
|
Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
i #1 #2 i + 1 0 - i #3 i + i
|
|
1) 85:26-38 = = = = = = =
|
|
2) 85:58-76 ? < _ _ _ _ _
|
|
3) 86:30-42 = = = = = = =
|
|
4) 88:26-42 _ < _ _ _ _ _
|
|
5) 89:20-36 ? ≤ ≤ ? ≤ ≤ ?
|
|
6) 90:21-37 _ < _ _ _ _ _
|
|
7) 91:26-42 _ < _ _ _ _ _
|
|
8) 92:25-41 _ < _ _ _ _ _
|
|
9) 97:8-20 _ < _ _ _ _ _
|
|
|
|
#1: xs.size - i
|
|
#2: xs.size - (i + 1)
|
|
#3: 42 - i
|
|
|
|
Please use `termination_by` to specify a decreasing measure.
|
|
guessLexDiff.lean:102:4-102:18: error: fail to show termination for
|
|
mutual_failure
|
|
mutual_failure2
|
|
with errors
|
|
failed to infer structural recursion:
|
|
Not considering parameter xs of mutual_failure:
|
|
it is unchanged in the recursive calls
|
|
Not considering parameter xs of mutual_failure2:
|
|
it is unchanged in the recursive calls
|
|
Cannot use parameters i of mutual_failure and i of mutual_failure2:
|
|
failed to eliminate recursive application
|
|
mutual_failure2 xs i
|
|
|
|
|
|
Could not find a decreasing measure.
|
|
The basic measures relate at each recursive call as follows:
|
|
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
|
Call from mutual_failure to mutual_failure2 at 104:4-24:
|
|
i #1 #2 i + 1
|
|
i = ? ? <
|
|
#3 ? = ? ?
|
|
Call from mutual_failure to mutual_failure2 at 104:52-78:
|
|
i #1 #2 i + 1
|
|
i ? _ _ =
|
|
#3 _ < _ _
|
|
Call from mutual_failure to mutual_failure2 at 107:4-24:
|
|
i #1 #2 i + 1
|
|
i _ _ _ <
|
|
#3 _ = _ _
|
|
Call from mutual_failure to mutual_failure2 at 111:4-28:
|
|
i #1 #2 i + 1
|
|
i _ _ _ =
|
|
#3 _ < _ _
|
|
Call from mutual_failure to mutual_failure2 at 117:8-28:
|
|
i #1 #2 i + 1
|
|
i _ _ _ <
|
|
#3 _ ? _ _
|
|
Call from mutual_failure2 to mutual_failure at 123:4-23:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 ? _
|
|
Call from mutual_failure2 to mutual_failure at 123:50-75:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 _ _
|
|
Call from mutual_failure2 to mutual_failure at 127:4-27:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 _ _
|
|
Call from mutual_failure2 to mutual_failure at 133:8-27:
|
|
i #3
|
|
i _ _
|
|
#1 _ _
|
|
#2 _ _
|
|
i + 1 _ _
|
|
|
|
|
|
#1: xs.size - i
|
|
#2: xs.size - (i + 1)
|
|
#3: xs.size - i
|
|
|
|
Please use `termination_by` to specify a decreasing measure.
|