LineRange and StringDiff invariants static checks - #34
Conversation
8e57af7 to
9a81d5f
Compare
| let diff = Deletion (mkLineRange leftLine lsF) (rightLine-1) | ||
| in diff : toLineRange (leftLine + length lsF) rightLine rs | ||
| -- Skip empty 'Second' and 'First' entries. | ||
| -- NOTE: Both these cases are unreachable. |
There was a problem hiding this comment.
Well, they are unreachable if the caller respects the invariants of StringDiff, right?
Invalid input could cause these equations to be reached, and diffToLineRanges is exported, so it may be used in unchecked ways.
There was a problem hiding this comment.
Indeed, some wishful thinking here: got carried away expecting inputs to always come from the output of Diff.getGroupedDiff... but downstream users might have other ideas.
I have merged the case back so that everything is handled homogeneously.
| in toLineRange (leftLine+lins) (rightLine+lins) rs | ||
| -- A 'Change' is introduced when an addition is followed by a deletion, or vice versa. | ||
| toLineRange leftLine rightLine (Second lsS:First lsF:rs)= | ||
| toLineRange leftLine rightLine (Second lsS@(_:_) : First lsF@(_:_) : rs) = |
There was a problem hiding this comment.
What is the need to pattern match on the lists lsS and lsF?
There was a problem hiding this comment.
I remember that without the pattern match verification would fail, but now I just removed all the pattern matches, along with the unreachable empty value case below, and verification passes. Seems like an artifact from a previous specification approach, or maybe it became unnecessary after some recent upstream change 🤔 .
| _ -> (fstLine,rs) | ||
| in ((read fstLine,read sndLine),rs3) | ||
| b = max a (read sndLine) | ||
| in ((a, b), rs3) |
There was a problem hiding this comment.
Looks like this is changing behavior of parseRange.
Before parseRange "3,2abc" == ((3, 2), "abc").
After parseRange "3,2abc" == ((3, 3), "abc").
| in case contents of | ||
| (_:_) -> (Just $ Deletion (mkLineRange (fst r1) contents) (fst r2), rs2) | ||
| _ -> (Nothing, rs2) |
There was a problem hiding this comment.
This is changing behavior of parseDel.
Before parseDel (a, b) "1,2" [] == (Just (Deletion (LineRange (a, a - 1) []) 1), []).
After parseDel (a, b) "1,2" [] == (Nothing, "").
The other parsing functions are modified in a similar way.
|
It is looking to me like the changes of behavior need more of a justification, and they would be easier to spot if they were put in separate commits. The refactoring of |
2 participants
This PR adds LiquidHaskell static checks to the
DiffOutputmodule based on:StringDiffrefinement for theDiffvalues of this module by its implicit invariants, namely: they are always non-empty and have coherentBothvalues.LineRangehas been refined to make to makelrNumbersan ordered pair where itslrContentsmust fit.The smart constructor
mkLineRangewas introduced to factor out the correctness check of mostLineRanges.Finally,
parsePrettyDiffsare checked to reduce their input.