ValidLineRange static check for diffToLineRanges - #34
Merged
Conversation
ninioArtillero
force-pushed
the
xg/output-checks
branch
from
July 21, 2026 22:36
8e57af7 to
9a81d5f
Compare
Contributor
|
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 |
ninioArtillero
force-pushed
the
xg/output-checks
branch
5 times, most recently
from
July 29, 2026 23:05
483117c to
b8bb207
Compare
ninioArtillero
changed the title
LineRange and StringDiff invariants static checksValidLineRange and StringDiff invariant static checks for diffToLineRanges
ninioArtillero
force-pushed
the
xg/output-checks
branch
2 times, most recently
from
July 30, 2026 20:27
8e48a46 to
5cc89a7
Compare
ninioArtillero
changed the title
ValidLineRange and StringDiff invariant static checks for diffToLineRangesValidLineRange static check for diffToLineRanges
The `LineRange`s constructed in `diffToLineRanges` assume non-emptiness of `Diff`'s values; this is checked using the `NonEmtpy` type alias. Also, `Nat1` is introduced to account for the fact that line numbers start from 1. Both conditions are required in order to check that `ValidLinaRange`s are constructed.
ninioArtillero
force-pushed
the
xg/output-checks
branch
from
July 31, 2026 15:22
5cc89a7 to
b847fe5
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a LiquidHaskell static check to
diffToLineRangesin theDiffOutputmodule, implemented using:LineDiff, a refinement type alias for theDiffvalues with non-empty[String]arguments. This property was an implicit precondition ofdiffToLineRanges.ValidLineRange, a refinement type alias ofLineRangethat requireslrNumbersto be an ordered pair where itslrContentsmust fit, is used for its postcondition.A stronger alternative to
ValidLineRangewould be to directly refine the data declation, like so:{-@ data LineRange = LineRange { lrNumbers :: {range : (Nat, Nat) | fst range <= snd range} , lrContents :: {contents : [String] | snd lrNumbers - fst lrNumbers = len contents - 1} @-}Which would check the corresponding predicates wherever a
LineRangeis inferred by the compiler. Nevertheless, this route was not taken asparsePrettyDiffsimplementation is too permissive for the invariants to hold without an extensive refactoring or the introduction of ad-hoc source checks enforcing them.