From 9a81d5fe5875a355f4399bcd93b8a52d1a0f676e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= Date: Wed, 22 Apr 2026 13:25:15 -0600 Subject: [PATCH 1/2] `StringDiff` and `LineRange` invariants --- src/Data/Algorithm/DiffOutput.hs | 119 ++++++++++++++++++++++++------- 1 file changed, 92 insertions(+), 27 deletions(-) diff --git a/src/Data/Algorithm/DiffOutput.hs b/src/Data/Algorithm/DiffOutput.hs index 3da26a7..feedbc9 100644 --- a/src/Data/Algorithm/DiffOutput.hs +++ b/src/Data/Algorithm/DiffOutput.hs @@ -1,3 +1,14 @@ +-- With PLE (Proof by Logical Evaluation) reflected predicates like +-- '_coherentDiff' are automatically unfolded when verifying refinement types. +-- Without it, LiquidHaskell cannot prove obligations like @_coherentDiff (Both x x) = True@ +-- because the reflected function's definition is not instantiated in the SMT context. +-- For example, the following check would fail: +-- +-- {-@ good :: StringDiff @-} +-- good = Both ["hello"] ["hello"] +-- +-- without PLE. +{-@ LIQUID "--ple" @-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.DiffOutput @@ -16,16 +27,38 @@ import Text.PrettyPrint hiding ((<>)) import Data.Char import Data.List +-- Non-empty lists as refinements of regular lists. +{-@ type NonEmpty a = {xs : [a] | len xs >0}@-} + +{-@ reflect _coherentDiff @-} +-- | This functions checks that both contents match whenever we have a 'Both' value. +-- Used in LiquidHaskell logic as a predicate. +_coherentDiff :: Eq c => Diff c -> Bool +_coherentDiff (Both x y) = x == y +_coherentDiff (First _) = True +_coherentDiff (Second _) = True + +-- This refinement type synonym encodes the invariants on the 'Diff' type +-- that we expect throughout this module. Namely: +-- +-- * They have non-empty contents +-- * 'Both' values have equal arguments +{-@ type StringDiff = {d : Diff (NonEmpty String) | _coherentDiff d} @-} + -- | Converts 'Diff's to 'DiffOperation's. 'First' and 'Second' -- ocurrances are converted to 'Addition' and 'Deletion', respectively, while -- consecutive ocurrances of them are replaced by a 'Change'. +{-@ diffToLineRanges :: [StringDiff] -> [DiffOperation LineRange] @-} diffToLineRanges :: [Diff [String]] -> [DiffOperation LineRange] diffToLineRanges = toLineRange 1 1 where -- | In @toLineRange x y ds@, @x@ is the index of the current string in the -- left input of the diff @ds@, and @y@ is the index of the corresponding -- string in the right input of the diff @ds@. - {-@ toLineRange :: Int -> Int -> diffs : [Diff[String]] -> [DiffOperation LineRange] / [len diffs, 0] @-} + {-@ toLineRange :: {l : Int | l >= 1} + -> {r : Int | r >= 1} + -> diffs : [StringDiff] + -> [DiffOperation LineRange] / [len diffs, 0] @-} toLineRange :: Int -> Int -> [Diff [String]] -> [DiffOperation LineRange] toLineRange _ _ []=[] -- If the lines are the same, we just move forward. @@ -33,22 +66,32 @@ diffToLineRanges = toLineRange 1 1 let lins=length ls 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) = toChange leftLine rightLine lsF lsS rs - toLineRange leftLine rightLine (First lsF:Second lsS:rs)= + toLineRange leftLine rightLine (First lsF@(_:_) : Second lsS@(_:_) : rs) = toChange leftLine rightLine lsF lsS rs -- Introduce 'Addition's. - toLineRange leftLine rightLine (Second lsS:rs)= - let linesS=length lsS - diff=Addition (LineRange (rightLine,rightLine+linesS-1) lsS) (leftLine-1) - in diff : toLineRange leftLine (rightLine+linesS) rs + toLineRange leftLine rightLine (Second lsS@(_:_) : rs) = + let diff = Addition (mkLineRange rightLine lsS) (leftLine-1) + in diff : toLineRange leftLine (rightLine + length lsS) rs -- Introduce 'Deletion's. - toLineRange leftLine rightLine (First lsF:rs)= - let linesF=length lsF - diff=Deletion (LineRange (leftLine,leftLine+linesF-1) lsF) (rightLine-1) - in diff: toLineRange(leftLine+linesF) rightLine rs + toLineRange leftLine rightLine (First lsF@(_:_) : rs)= + 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. + toLineRange leftLine rightLine (Second [] : rs) = + toLineRange leftLine rightLine rs + toLineRange leftLine rightLine (First [] : rs) = + toLineRange leftLine rightLine rs -- | Build 'Change's from adjacent additions and deletions. - {-@ toChange :: Int -> Int -> [String] -> [String] -> diffs : [Diff [String]] -> [DiffOperation LineRange] / [len diffs, 1] @-} + {-@ toChange :: {l : Int | l >= 1} + -> {r : Int | r >= 1} + -> {lf : [String] | len lf > 0} + -> {ls : [String] | len ls > 0} + -> diffs : [StringDiff] + -> [DiffOperation LineRange] + / [len diffs, 1] @-} toChange :: Int -- ^ Current left line number. -> Int -- ^ Current right line number. -> [String] -- ^ Lines from the 'First' list (corresponding to deletions). @@ -56,11 +99,10 @@ diffToLineRanges = toLineRange 1 1 -> [Diff [String]] -- ^ Remaining 'Diff's. -> [DiffOperation LineRange] toChange leftLine rightLine lsF lsS rs= - let linesS=length lsS - linesF=length lsF - in Change (LineRange (leftLine,leftLine+linesF-1) lsF) (LineRange (rightLine,rightLine+linesS-1) lsS) - : toLineRange (leftLine+linesF) (rightLine+linesS) rs + Change (mkLineRange leftLine lsF) (mkLineRange rightLine lsS) + : toLineRange (leftLine + length lsF) (rightLine + length lsS) rs +{-@ ppDiff :: [StringDiff] -> String @-} -- | Pretty print the differences. The output is similar to the output of the @diff@ utility. -- -- > > putStr (ppDiff (getGroupedDiff ["a","b","c","d","e"] ["a","c","d","f"])) @@ -114,6 +156,7 @@ parsePrettyDiffs = reverse . doParse [] . lines Just nd -> doParse (nd:acc) r _ -> doParse acc r + {-@ parseDiff :: s:{[String] | len s > 0} -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) < len s} @-} parseDiff :: [String] -> (Maybe (DiffOperation LineRange), [String]) parseDiff [] = (Nothing,[]) parseDiff (h:rs) = let @@ -128,38 +171,47 @@ parsePrettyDiffs = reverse . doParse [] . lines ('c':hrs2) -> parseChange r1 hrs2 rs _ -> (Nothing,rs) + {-@ parseDel :: (Nat, Nat) -> String -> rs:[String] -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) <= len rs} @-} parseDel :: (LineNo, LineNo) -> String -> [String] -> (Maybe (DiffOperation LineRange), [String]) parseDel r1 hrs2 rs = let - -- NOTE: the wildcard should correspond to the end of line, - -- but is ignored for simplicity. (r2,_) = parseRange hrs2 (ls,rs2) = span (isPrefixOf "<") rs - in (Just $ Deletion (LineRange r1 (map (drop 2) ls)) (fst r2), rs2) + contents = map (drop 2) ls + in case contents of + (_:_) -> (Just $ Deletion (mkLineRange (fst r1) contents) (fst r2), rs2) + _ -> (Nothing, rs2) + {-@ parseAdd :: (Nat, Nat) -> String -> rs:[String] -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) <= len rs} @-} parseAdd :: (LineNo, LineNo) -> String -> [String] -> (Maybe (DiffOperation LineRange), [String]) parseAdd r1 hrs2 rs = let - -- NOTE: the wildcard should correspond to the end of line, - -- but is ignored for simplicity. (r2,_) = parseRange hrs2 (ls,rs2) = span (isPrefixOf ">") rs - in (Just $ Addition (LineRange r2 (map (drop 2) ls)) (fst r1), rs2) + contents = map (drop 2) ls + in case contents of + (_:_) -> (Just $ Addition (mkLineRange (fst r2) contents) (fst r1), rs2) + _ -> (Nothing, rs2) + {-@ parseChange :: (Nat, Nat) -> String -> rs:[String] -> {v:(Maybe (DiffOperation LineRange), [String]) | len (snd v) <= len rs} @-} parseChange :: (LineNo, LineNo) -> String -> [String] -> (Maybe (DiffOperation LineRange), [String]) parseChange r1 hrs2 rs = let - -- NOTE: the wildcard should correspond to the end of line, - -- but is ignored for simplicity. (r2,_) = parseRange hrs2 (ls1,rs2) = span (isPrefixOf "<") rs in case rs2 of -- The left and right diff of a 'Change' are separated by a "---" line. ("---":rs3) -> let (ls2,rs4) = span (isPrefixOf ">") rs3 - in (Just $ Change (LineRange r1 (map (drop 2) ls1)) (LineRange r2 (map (drop 2) ls2)), rs4) + contents1 = map (drop 2) ls1 + contents2 = map (drop 2) ls2 + in case (contents1, contents2) of + (_:_, _:_) -> (Just $ Change (mkLineRange (fst r1) contents1) (mkLineRange (fst r2) contents2), rs4) + _ -> (Nothing, rs4) _ -> (Nothing,rs2) - parseRange :: String -> ((LineNo, LineNo),String) + {-@ parseRange :: String -> {v : ((Nat, Nat), String) | fst (fst v) <= snd (fst v)} @-} + parseRange :: String -> ((LineNo, LineNo), String) parseRange l = let (fstLine,rs) = span isDigit l + a = max 0 (read fstLine) (sndLine,rs3) = case rs of -- The comma is used to separate -- the start and end line numbers in a range, @@ -167,7 +219,8 @@ parsePrettyDiffs = reverse . doParse [] . lines -- i.e. the range is a single line. (',':rs2) -> span isDigit rs2 _ -> (fstLine,rs) - in ((read fstLine,read sndLine),rs3) + b = max a (read sndLine) + in ((a, b), rs3) -- | Line number alias. Always non-negative. type LineNo = Int @@ -180,11 +233,23 @@ type LineNo = Int -- > snd lrNumbers - fst lrNumbers + 1 == length lrContents -- -- which imply @lrContents@ cannot be empty. +{-@ +data LineRange = LineRange { lrNumbers :: {range : (Nat, Nat) | fst range <= snd range} + , lrContents :: {contents : [String] | snd lrNumbers - fst lrNumbers = len contents - 1} + } +@-} data LineRange = LineRange { lrNumbers :: (LineNo, LineNo) , lrContents :: [String] } deriving (Show, Read, Eq, Ord) +-- | Smart constructor for 'LineRange' that computes the end line from the +-- start line and the content length, guaranteeing that its content length and +-- range match. +{-@ mkLineRange :: start:Nat -> contents:{[String] | len contents > 0} -> LineRange @-} +mkLineRange :: Int -> [String] -> LineRange +mkLineRange start contents = LineRange (start, start + length contents - 1) contents + -- | Diff operation representing changes to apply. data DiffOperation a = Deletion a LineNo -- ^ Element deleted on the left input, line number From d5e616d94991e8c68749ccdc3864f010c410b0ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= Date: Tue, 21 Jul 2026 20:35:33 -0600 Subject: [PATCH 2/2] Remove unneeded case split --- src/Data/Algorithm/DiffOutput.hs | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/Data/Algorithm/DiffOutput.hs b/src/Data/Algorithm/DiffOutput.hs index feedbc9..8654872 100644 --- a/src/Data/Algorithm/DiffOutput.hs +++ b/src/Data/Algorithm/DiffOutput.hs @@ -66,24 +66,18 @@ diffToLineRanges = toLineRange 1 1 let lins=length ls 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) = toChange leftLine rightLine lsF lsS rs - toLineRange leftLine rightLine (First lsF@(_:_) : Second lsS@(_:_) : rs) = + toLineRange leftLine rightLine (First lsF : Second lsS : rs) = toChange leftLine rightLine lsF lsS rs -- Introduce 'Addition's. - toLineRange leftLine rightLine (Second lsS@(_:_) : rs) = + toLineRange leftLine rightLine (Second lsS : rs) = let diff = Addition (mkLineRange rightLine lsS) (leftLine-1) in diff : toLineRange leftLine (rightLine + length lsS) rs -- Introduce 'Deletion's. - toLineRange leftLine rightLine (First lsF@(_:_) : rs)= + toLineRange leftLine rightLine (First lsF : rs)= 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. - toLineRange leftLine rightLine (Second [] : rs) = - toLineRange leftLine rightLine rs - toLineRange leftLine rightLine (First [] : rs) = - toLineRange leftLine rightLine rs -- | Build 'Change's from adjacent additions and deletions. {-@ toChange :: {l : Int | l >= 1} -> {r : Int | r >= 1}