From c65a13377b45871079ed19e2bc6352f19e81fbc0 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/3] Wave front edit distance invariant --- src/Data/Algorithm/Diff.hs | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs index 2173751..fa681ad 100644 --- a/src/Data/Algorithm/Diff.hs +++ b/src/Data/Algorithm/Diff.hs @@ -1,3 +1,4 @@ +{-@ LIQUID "--ple" @-} ----------------------------------------------------------------------------- -- | -- Module : Data.Algorithm.Diff @@ -145,6 +146,13 @@ data DL = DL -- 'S' steps are stored. } deriving (Show, Eq) +-- This refinement type alias represents a 'DL' value with a fixed /D-length/, +-- which we call a "D-path location node". +{-@ type DLN D = { x : DL | len (path x) = D } @-} + +-- A wave front is a list of 'DL' nodes, all at the same edit distance @D@. +{-@ type WaveFront D = [DLN D] @-} + -- | Select the furthest-reaching candidate of two 'DL' nodes competing for the -- same k-diagonal, as required by the Myers algorithm. -- @@ -159,6 +167,7 @@ data DL = DL -- and both argument nodes are within the same wave front, -- -- > length (path x) == length (path y) +{-@ furthestReaching :: x : DL -> y : DL -> {v : DL | v = x || v = y} @-} furthestReaching :: DL -> DL -> DL furthestReaching x y | poi x >= poi y = x @@ -203,21 +212,28 @@ canDiag eq as bs lena lenb = \ i j -> {-@ dstep :: (Nat -> Nat -> Bool) - -> {nodes : [DL] | len nodes > 0} - -> {v : [DL] | len v = len nodes + 1} + -> d : Nat + -> {nodes : WaveFront d | len nodes > 0} + -> {v : WaveFront (d + 1) | len v = len nodes + 1} @-} dstep :: (Int -> Int -> Bool) -- ^ Diagonal predicate + -> Int -- ^ The current D-length; used for the static check of wave front invariant. -> [DL] -- ^ A non-empty wave front of nodes at edit distance D -> [DL] -- ^ A non-empty wave front of nodes at edit distance D+1 -dstep _ [] = error "dstep: Cannot perform expansion on an empty list of nodes" -dstep cd (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls +dstep _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes" +dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls where + {-@ hStep :: DLN _d -> DLN (_d + 1) @-} hStep node = node {poi = poi node + 1, path = F : path node} + {-@ vStep :: DLN _d -> DLN (_d + 1) @-} vStep node = node {poj = poj node + 1, path = S : path node} -- Merge vertical step of previous node with horizontal step of next node, -- selecting the furthest-reaching candidate for each shared k-diagonal, -- and extend it along matching elements. + {-@ stepAndMerge :: prev : DLN _d + -> rest : WaveFront _d + -> {v : WaveFront (_d + 1) | len v = len rest + 1} / [len rest] @-} stepAndMerge :: DL -> [DL] -> [DL] stepAndMerge prev [] = [addsnake cd $ vStep prev] stepAndMerge prev (next:rest) = @@ -270,10 +286,11 @@ addsnake cd dl -- unchanged. ses :: (a -> b -> Bool) -> [a] -> [b] -> [DI] ses eq as bs = path . head . dropWhile (\dl -> poi dl /= lena || poj dl /= lenb) . - concat . iterate (dstep cd) . (:[]) . addsnake cd $ + concat . iterate (uncurry (dstep cd) . withD) . (:[]) . addsnake cd $ DL {poi=0,poj=0,path=[]} where cd = canDiag eq as bs lena lenb lena = length as; lenb = length bs + withD xs = (length . path . head $ xs, xs) -- | Takes two lists and returns a list of differences between them. This is -- 'getDiffBy' with '==' used as predicate. From b6ea9b26f4d8dad36df22d5028da9ea225d7108c 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 2/3] Wave front diagonals invariant --- src/Data/Algorithm/Diff.hs | 37 ++++++++++++++++++++++++++++--------- 1 file changed, 28 insertions(+), 9 deletions(-) diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs index fa681ad..7aac346 100644 --- a/src/Data/Algorithm/Diff.hs +++ b/src/Data/Algorithm/Diff.hs @@ -150,8 +150,24 @@ data DL = DL -- which we call a "D-path location node". {-@ type DLN D = { x : DL | len (path x) = D } @-} --- A wave front is a list of 'DL' nodes, all at the same edit distance @D@. -{-@ type WaveFront D = [DLN D] @-} +{-@ inline _kdiag @-} +-- | Computes the k-diagonal of a node. +-- Used in LiquidHaskell logic as an expression. +_kdiag :: DL -> Int +_kdiag dl = poi dl - poj dl + +{-@ reflect _wfDiags @-} +{-@ _wfDiags :: Int -> xs : [DL] -> Bool / [len xs] @-} +-- | Checks if succesive nodes of a wave front lie within k-diagonals +-- differing by 2 as described in the Myers algorithm. +-- Used in LiquidHaskell logic as a predicate. +_wfDiags :: Int -> [DL] -> Bool +_wfDiags _ [] = True +_wfDiags k (dl:dls) = poi dl - poj dl == k && _wfDiags (k - 2) dls + +-- A wave front is a list of 'DL' nodes, all at the same edit distance @D@, +-- with k-diagonals @D@, @D−2@, …, @-D+2@, @-D@. +{-@ type WaveFront D = {xs : [DLN D] | _wfDiags D xs} @-} -- | Select the furthest-reaching candidate of two 'DL' nodes competing for the -- same k-diagonal, as required by the Myers algorithm. @@ -167,7 +183,9 @@ data DL = DL -- and both argument nodes are within the same wave front, -- -- > length (path x) == length (path y) -{-@ furthestReaching :: x : DL -> y : DL -> {v : DL | v = x || v = y} @-} +{-@ furthestReaching :: x : DL + -> {y : DL | _kdiag x = _kdiag y} + -> {v : DL | v = x || v = y} @-} furthestReaching :: DL -> DL -> DL furthestReaching x y | poi x >= poi y = x @@ -224,16 +242,17 @@ dstep dstep _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes" dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls where - {-@ hStep :: DLN _d -> DLN (_d + 1) @-} + {-@ hStep :: x : DLN _d -> {v : DLN (_d + 1) | _kdiag v = _kdiag x + 1} @-} hStep node = node {poi = poi node + 1, path = F : path node} - {-@ vStep :: DLN _d -> DLN (_d + 1) @-} + {-@ vStep :: x : DLN _d -> {v : DLN (_d + 1) | _kdiag v = _kdiag x - 1} @-} vStep node = node {poj = poj node + 1, path = S : path node} -- Merge vertical step of previous node with horizontal step of next node, -- selecting the furthest-reaching candidate for each shared k-diagonal, -- and extend it along matching elements. - {-@ stepAndMerge :: prev : DLN _d - -> rest : WaveFront _d - -> {v : WaveFront (_d + 1) | len v = len rest + 1} / [len rest] @-} + {-@ stepAndMerge :: prev : DLN _d + -> {rest : [DLN _d] | _wfDiags (_kdiag prev - 2) rest} + -> {v : [DLN (_d+1)] | _wfDiags (_kdiag prev - 1) v && len v = len rest + 1} + / [len rest] @-} stepAndMerge :: DL -> [DL] -> [DL] stepAndMerge prev [] = [addsnake cd $ vStep prev] stepAndMerge prev (next:rest) = @@ -248,7 +267,7 @@ dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls -- @(poi dl, poj dl)@, this function advances both 'poi' and 'poj' as long -- as consecutive elements match, leaving 'path' unchanged (diagonal moves -- are not recorded as edit steps). -{-@ addsnake :: (Nat -> Nat -> Bool) -> x : DL -> {v : DL | path v == path x } @-} +{-@ addsnake :: (Nat -> Nat -> Bool) -> x : DL -> {v : DL | path v == path x && _kdiag v = _kdiag x} @-} addsnake :: (Int -> Int -> Bool) -> DL -> DL addsnake cd dl | cd pi pj = addsnake cd $ From 7f6ad23ce16cd3640beb74b66289a313feb77cd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Xavier=20G=C3=B3ngora?= Date: Thu, 9 Jul 2026 11:27:59 -0600 Subject: [PATCH 3/3] Document phantom parameter and postconditions --- src/Data/Algorithm/Diff.hs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Data/Algorithm/Diff.hs b/src/Data/Algorithm/Diff.hs index 7aac346..576c04b 100644 --- a/src/Data/Algorithm/Diff.hs +++ b/src/Data/Algorithm/Diff.hs @@ -226,7 +226,10 @@ canDiag eq as bs lena lenb = \ i j -> -- next higher diagonal while an 'S' edge retreats to the next lower one, so the -- two members of each pair straddle the same diagonal from opposite sides. -- --- Precondition: The node list must be non-empty. +-- Precondition: The node list must be a non-empty @WaveFront@. +-- +-- Postcondition: The node list must be a non-empty @WaveFront@ +-- with one more node than the input. {-@ dstep :: (Nat -> Nat -> Bool) @@ -239,6 +242,10 @@ dstep -> Int -- ^ The current D-length; used for the static check of wave front invariant. -> [DL] -- ^ A non-empty wave front of nodes at edit distance D -> [DL] -- ^ A non-empty wave front of nodes at edit distance D+1 +-- NOTE: @_d@ is a phantom (apparently unused) parameter required by local LiquidHaskell specifications. +-- This parameter sits at the first equation as a workaround +-- to GHC removing it when desugaring multi-equation definitions. +-- See https://github.com/ucsd-progsys/liquidhaskell/issues/2704 dstep _ _d [] = error "dstep: Cannot perform expansion on an empty list of nodes" dstep cd _ (dl:dls) = addsnake cd (hStep dl) : stepAndMerge dl dls where